1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 {-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
4 -- | Symantic for 'Int'.
5 module Language.Symantic.Lib.Int where
8 import qualified Data.Text as Text
9 import Data.Type.Equality ((:~:)(Refl))
11 import Language.Symantic.Parsing
12 import Language.Symantic.Typing
13 import Language.Symantic.Compiling
14 import Language.Symantic.Interpreting
15 import Language.Symantic.Transforming
18 class Sym_Int term where
19 int :: Int -> term Int
20 default int :: Trans t term => Int -> t term Int
21 int = trans_lift . int
23 type instance Sym_of_Iface (Proxy Int) = Sym_Int
24 type instance Consts_of_Iface (Proxy Int) = Proxy Int ': Consts_imported_by Int
25 type instance Consts_imported_by Int =
36 instance Sym_Int HostI where
38 instance Sym_Int TextI where
39 int a = TextI $ \_p _v ->
41 instance (Sym_Int r1, Sym_Int r2) => Sym_Int (DupI r1 r2) where
42 int x = int x `DupI` int x
45 ( Read_TypeNameR Type_Name cs rs
47 ) => Read_TypeNameR Type_Name cs (Proxy Int ': rs) where
48 read_typenameR _cs (Type_Name "Int") k = k (ty @Int)
49 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
50 instance Show_Const cs => Show_Const (Proxy Int ': cs) where
51 show_const ConstZ{} = "Int"
52 show_const (ConstS c) = show_const c
56 , Proj_Consts cs (Consts_imported_by Int)
57 ) => Proj_ConC cs (Proxy Int) where
58 proj_conC _ (TyConst q :$ TyConst c)
59 | Just Refl <- eq_skind (kind_of_const c) SKiType
60 , Just Refl <- proj_const c (Proxy @Int)
62 _ | Just Refl <- proj_const q (Proxy @Bounded) -> Just Con
63 | Just Refl <- proj_const q (Proxy @Enum) -> Just Con
64 | Just Refl <- proj_const q (Proxy @Eq) -> Just Con
65 | Just Refl <- proj_const q (Proxy @Integral) -> Just Con
66 | Just Refl <- proj_const q (Proxy @Num) -> Just Con
67 | Just Refl <- proj_const q (Proxy @Ord) -> Just Con
68 | Just Refl <- proj_const q (Proxy @Real) -> Just Con
69 | Just Refl <- proj_const q (Proxy @Show) -> Just Con
71 proj_conC _c _q = Nothing
72 data instance TokenT meta (ts::[*]) (Proxy Int)
74 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Int))
75 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Int))
77 Inj_Const (Consts_of_Ifaces is) Int =>
78 CompileI is (Proxy Int) where
81 Token_Term_Int i -> k (ty @Int) $ TermO $ \_c -> int i
82 instance TokenizeT meta ts (Proxy Int)
83 instance Gram_Term_AtomsT meta ts (Proxy Int) g