{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Lib.Integer where
import Data.Eq (Eq)
import Data.Function (($), (.))
import Data.Functor ((<$>))
import Data.Maybe (Maybe(..))
import Data.Ord (Ord)
import Prelude (Enum, Integer, Integral, Num, Real)
import Text.Show (Show(..))
import Text.Read (read)
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 _ (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