module Language.Symantic.Lib.Integer where
import qualified Data.Text as Text
import Language.Symantic
import Language.Symantic.Grammar
type instance Sym Integer = Sym_Integer
class Sym_Integer term where
integer :: Integer -> term Integer
default integer :: Sym_Integer (UnT term) => Trans term => Integer -> term Integer
integer = trans . integer
instance Sym_Integer Eval where
integer = Eval
instance Sym_Integer View where
integer a = View $ \_p _v ->
Text.pack (show a)
instance (Sym_Integer r1, Sym_Integer r2) => Sym_Integer (Dup r1 r2) where
integer x = integer x `Dup` integer x
instance (Sym_Integer term, Sym_Lambda term) => Sym_Integer (BetaT term)
instance NameTyOf Integer where
nameTyOf _c = ["Integer"] `Mod` "Integer"
instance ClassInstancesFor Integer where
proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
| Just HRefl <- proj_ConstKiTy @_ @Integer z
= case () of
_ | Just Refl <- proj_Const @Enum q -> Just Dict
| Just Refl <- proj_Const @Eq q -> Just Dict
| Just Refl <- proj_Const @Integral q -> Just Dict
| Just Refl <- proj_Const @Num q -> Just Dict
| Just Refl <- proj_Const @Ord q -> Just Dict
| Just Refl <- proj_Const @Real q -> Just Dict
| Just Refl <- proj_Const @Show q -> Just Dict
_ -> Nothing
proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Integer
instance
( Gram_Source src g
, Gram_Alt g
, Gram_AltApp g
, Gram_Rule g
, Gram_Comment g
, SymInj ss Integer
) => Gram_Term_AtomsFor src ss g Integer where
g_term_atomsFor =
[ rule "teinteger" $
lexeme $ source $
(\i src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teInteger $ read i)
<$> some (choice $ char <$> ['0'..'9'])
]
instance ModuleFor src ss Integer
tyInteger :: Source src => LenInj vs => Type src vs Integer
tyInteger = tyConst @(K Integer) @Integer
teInteger :: Source src => SymInj ss Integer => Integer -> Term src ss ts '[] (() #> Integer)
teInteger i = Term noConstraint tyInteger $ teSym @Integer $ integer i