]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Integer.hs
Fix comment typo.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Integer.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 {-# OPTIONS_GHC -fconstraint-solver-iterations=6 #-}
4 -- | Symantic for 'Integer'.
5 module Language.Symantic.Lib.Integer where
6
7 import Data.Proxy
8 import qualified Data.Text as Text
9 import Data.Type.Equality ((:~:)(Refl))
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
17 -- * Class 'Sym_Integer'
18 class Sym_Integer term where
19 integer :: Integer -> term Integer
20 default integer :: Trans t term => Integer -> t term Integer
21 integer = trans_lift . integer
22
23 type instance Sym_of_Iface (Proxy Integer) = Sym_Integer
24 type instance TyConsts_of_Iface (Proxy Integer) = Proxy Integer ': TyConsts_imported_by Integer
25 type instance TyConsts_imported_by Integer =
26 [ Proxy Enum
27 , Proxy Eq
28 , Proxy Integral
29 , Proxy Num
30 , Proxy Ord
31 , Proxy Real
32 , Proxy Show
33 ]
34
35 instance Sym_Integer HostI where
36 integer = HostI
37 instance Sym_Integer TextI where
38 integer a = TextI $ \_p _v ->
39 Text.pack (show a)
40 instance (Sym_Integer r1, Sym_Integer r2) => Sym_Integer (DupI r1 r2) where
41 integer x = integer x `DupI` integer x
42
43 instance
44 ( Read_TyNameR TyName cs rs
45 , Inj_TyConst cs Integer
46 ) => Read_TyNameR TyName cs (Proxy Integer ': rs) where
47 read_TyNameR _cs (TyName "Integer") k = k (ty @Integer)
48 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
49 instance Show_TyConst cs => Show_TyConst (Proxy Integer ': cs) where
50 show_TyConst TyConstZ{} = "Integer"
51 show_TyConst (TyConstS c) = show_TyConst c
52
53 instance -- Proj_TyConC
54 ( Proj_TyConst cs Integer
55 , Proj_TyConsts cs (TyConsts_imported_by Integer)
56 ) => Proj_TyConC cs (Proxy Integer) where
57 proj_TyConC _ (TyConst q :$ TyConst c)
58 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
59 , Just Refl <- proj_TyConst c (Proxy @Integer)
60 = case () of
61 _ | Just Refl <- proj_TyConst q (Proxy @Enum) -> Just TyCon
62 | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon
63 | Just Refl <- proj_TyConst q (Proxy @Integral) -> Just TyCon
64 | Just Refl <- proj_TyConst q (Proxy @Num) -> Just TyCon
65 | Just Refl <- proj_TyConst q (Proxy @Ord) -> Just TyCon
66 | Just Refl <- proj_TyConst q (Proxy @Real) -> Just TyCon
67 | Just Refl <- proj_TyConst q (Proxy @Show) -> Just TyCon
68 _ -> Nothing
69 proj_TyConC _c _q = Nothing
70 data instance TokenT meta (ts::[*]) (Proxy Integer)
71 = Token_Term_Integer Integer
72 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Integer))
73 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Integer))
74 instance -- CompileI
75 Inj_TyConst (TyConsts_of_Ifaces is) Integer =>
76 CompileI is (Proxy Integer) where
77 compileI tok _ctx k =
78 case tok of
79 Token_Term_Integer i -> k (ty @Integer) $ TermO $ \_c -> integer i
80 instance -- TokenizeT
81 -- Inj_Token meta ts Integer =>
82 TokenizeT meta ts (Proxy Integer)
83 instance -- Gram_Term_AtomsT
84 ( Alt g
85 , Alter g
86 , Gram_Rule g
87 , Gram_Lexer g
88 , Gram_Meta meta g
89 , Inj_Token meta ts Integer
90 ) => Gram_Term_AtomsT meta ts (Proxy Integer) g where
91 term_atomsT _t =
92 [ rule "term_integer" $
93 lexeme $ metaG $
94 (\i meta -> ProTok $ inj_EToken meta $ Token_Term_Integer $ read i)
95 <$> some (choice $ char <$> ['0'..'9'])
96 ]