{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# OPTIONS_GHC -fconstraint-solver-iterations=6 #-}
-- | Symantic for 'Integer'.
module Language.Symantic.Lib.Integer where
-import Data.Proxy
import qualified Data.Text as Text
-import Data.Type.Equality ((:~:)(Refl))
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
+import Language.Symantic
+import Language.Symantic.Grammar
-- * Class 'Sym_Integer'
+type instance Sym Integer = Sym_Integer
class Sym_Integer term where
integer :: Integer -> term Integer
- default integer :: Trans t term => Integer -> t term Integer
- integer = trans_lift . integer
+ default integer :: Sym_Integer (UnT term) => Trans term => Integer -> term Integer
+ integer = trans . integer
-type instance Sym_of_Iface (Proxy Integer) = Sym_Integer
-type instance TyConsts_of_Iface (Proxy Integer) = Proxy Integer ': TyConsts_imported_by Integer
-type instance TyConsts_imported_by Integer =
- [ Proxy Enum
- , Proxy Eq
- , Proxy Integral
- , Proxy Num
- , Proxy Ord
- , Proxy Real
- , Proxy Show
- ]
-
-instance Sym_Integer HostI where
- integer = HostI
-instance Sym_Integer TextI where
- integer a = TextI $ \_p _v ->
+-- Interpreting
+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 (DupI r1 r2) where
- integer x = integer x `DupI` integer x
+instance (Sym_Integer r1, Sym_Integer r2) => Sym_Integer (Dup r1 r2) where
+ integer x = integer x `Dup` integer x
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Integer
- ) => Read_TyNameR TyName cs (Proxy Integer ': rs) where
- read_TyNameR _cs (TyName "Integer") k = k (ty @Integer)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Integer ': cs) where
- show_TyConst TyConstZ{} = "Integer"
- show_TyConst (TyConstS c) = show_TyConst c
+-- Transforming
+instance (Sym_Integer term, Sym_Lambda term) => Sym_Integer (BetaT term)
-instance -- Proj_TyConC
- ( Proj_TyConst cs Integer
- , Proj_TyConsts cs (TyConsts_imported_by Integer)
- ) => Proj_TyConC cs (Proxy Integer) where
- proj_TyConC _ (TyConst q :$ TyConst c)
- | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
- , Just Refl <- proj_TyConst c (Proxy @Integer)
+-- Typing
+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_TyConst q (Proxy @Enum) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Integral) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Num) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Ord) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Real) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Show) -> Just TyCon
+ _ | 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
- proj_TyConC _c _q = Nothing
-data instance TokenT meta (ts::[*]) (Proxy Integer)
- = Token_Term_Integer Integer
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Integer))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Integer))
-instance -- CompileI
- Inj_TyConst (TyConsts_of_Ifaces is) Integer =>
- CompileI is (Proxy Integer) where
- compileI tok _ctx k =
- case tok of
- Token_Term_Integer i -> k (ty @Integer) $ TermO $ \_c -> integer i
-instance -- TokenizeT
- -- Inj_Token meta ts Integer =>
- TokenizeT meta ts (Proxy Integer)
-instance -- Gram_Term_AtomsT
- ( Alt g
- , Alter g
+ proveConstraintFor _c _q = Nothing
+instance TypeInstancesFor Integer
+
+-- Compiling
+instance
+ ( Gram_Source src g
+ , Gram_Alt g
+ , Gram_AltApp g
, Gram_Rule g
- , Gram_Lexer g
- , Gram_Meta meta g
- , Inj_Token meta ts Integer
- ) => Gram_Term_AtomsT meta ts (Proxy Integer) g where
- term_atomsT _t =
- [ rule "term_integer" $
- lexeme $ metaG $
- (\i meta -> ProTok $ inj_EToken meta $ Token_Term_Integer $ read i)
+ , 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
+
+-- ** 'Term's
+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
sourcephile / git / haskell / symantic.git / blobdiff