]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Int.hs
Fix Mono{Foldable,Functor} and {Semi,Is}Sequence constraints.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Int.hs
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
6
7 import Data.Proxy
8 import Data.Type.Equality ((:~:)(Refl))
9 import qualified Data.Text as Text
10
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
16 import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))
17
18 -- * Class 'Sym_Int'
19 class Sym_Int term where
20 int :: Int -> term Int
21 default int :: Trans t term => Int -> t term Int
22 int = trans_lift . int
23
24 type instance Sym_of_Iface (Proxy Int) = Sym_Int
25 type instance TyConsts_of_Iface (Proxy Int) = Proxy Int ': TyConsts_imported_by (Proxy Int)
26 type instance TyConsts_imported_by (Proxy Int) =
27 [ Proxy Bounded
28 , Proxy Enum
29 , Proxy Eq
30 , Proxy Integral
31 , Proxy Num
32 , Proxy Ord
33 , Proxy Real
34 , Proxy Show
35 ]
36
37 instance Sym_Int HostI where
38 int = HostI
39 instance Sym_Int TextI where
40 int a = TextI $ \_p _v ->
41 Text.pack (show a)
42 instance (Sym_Int r1, Sym_Int r2) => Sym_Int (DupI r1 r2) where
43 int x = int x `DupI` int x
44
45 instance
46 ( Read_TyNameR TyName cs rs
47 , Inj_TyConst cs Int
48 ) => Read_TyNameR TyName cs (Proxy Int ': rs) where
49 read_TyNameR _cs (TyName "Int") k = k (ty @Int)
50 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
51 instance Show_TyConst cs => Show_TyConst (Proxy Int ': cs) where
52 show_TyConst TyConstZ{} = "Int"
53 show_TyConst (TyConstS c) = show_TyConst c
54
55 instance Proj_TyFamC cs TyFam_MonoElement Int
56
57 instance -- Proj_TyConC
58 ( Proj_TyConst cs Int
59 , Proj_TyConsts cs (TyConsts_imported_by (Proxy Int))
60 ) => Proj_TyConC cs (Proxy Int) where
61 proj_TyConC _ (TyConst q :$ TyConst c)
62 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
63 , Just Refl <- proj_TyConst c (Proxy @Int)
64 = case () of
65 _ | Just Refl <- proj_TyConst q (Proxy @Bounded) -> Just TyCon
66 | Just Refl <- proj_TyConst q (Proxy @Enum) -> Just TyCon
67 | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon
68 | Just Refl <- proj_TyConst q (Proxy @Integral) -> Just TyCon
69 | Just Refl <- proj_TyConst q (Proxy @Num) -> Just TyCon
70 | Just Refl <- proj_TyConst q (Proxy @Ord) -> Just TyCon
71 | Just Refl <- proj_TyConst q (Proxy @Real) -> Just TyCon
72 | Just Refl <- proj_TyConst q (Proxy @Show) -> Just TyCon
73 _ -> Nothing
74 proj_TyConC _c _q = Nothing
75 data instance TokenT meta (ts::[*]) (Proxy Int)
76 = Token_Term_Int Int
77 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Int))
78 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Int))
79
80 instance -- CompileI
81 Inj_TyConst cs Int =>
82 CompileI cs is (Proxy Int) where
83 compileI tok _ctx k =
84 case tok of
85 Token_Term_Int i -> k (ty @Int) $ TermO $ \_c -> int i
86 instance TokenizeT meta ts (Proxy Int)
87 instance Gram_Term_AtomsT meta ts (Proxy Int) g