module Language.Symantic.Lib.Unit where
import Language.Symantic
import Language.Symantic.Grammar
type instance Sym () = Sym_Unit
class Sym_Unit term where
unit :: term ()
default unit :: Sym_Unit (UnT term) => Trans term => term ()
unit = trans unit
instance Sym_Unit Eval where
unit = Eval ()
instance Sym_Unit View where
unit = View $ \_p _v -> "()"
instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (Dup r1 r2) where
unit = unit `Dup` unit
instance (Sym_Unit term, Sym_Lambda term) => Sym_Unit (BetaT term)
instance NameTyOf () where
nameTyOf _c = [] `Mod` ""
instance ClassInstancesFor () where
proveConstraintFor _ (TyConst _ _ q :$ z)
| Just HRefl <- proj_ConstKiTy @_ @() z
= case () of
_ | Just Refl <- proj_Const @Bounded q -> Just Dict
| Just Refl <- proj_Const @Enum q -> Just Dict
| Just Refl <- proj_Const @Eq q -> Just Dict
| Just Refl <- proj_Const @Monoid q -> Just Dict
| Just Refl <- proj_Const @Ord q -> Just Dict
| Just Refl <- proj_Const @Show q -> Just Dict
_ -> Nothing
proveConstraintFor _c _q = Nothing
instance TypeInstancesFor ()
instance
( Gram_Source src g
, Gram_Rule g
, Gram_Comment g
, SymInj ss ()
) => Gram_Term_AtomsFor src ss g () where
g_term_atomsFor =
[ rule "teUnit" $
source $
(\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teUnit)
<$ symbol "("
<* symbol ")"
]
instance ModuleFor src ss ()
tyUnit :: Source src => LenInj vs => Type src vs ()
tyUnit = tyConst @(K ()) @()
teUnit :: TermDef () '[] (() #> ())
teUnit = Term noConstraint tyUnit $ teSym @() $ unit