]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Lib/Integer.hs
Move libraries in Lib.
[haskell/symantic.git] / 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 Control.Applicative (Alternative(..))
8 import Data.Proxy
9 import qualified Data.Text as Text
10 import Data.Type.Equality ((:~:)(Refl))
11
12 import Language.Symantic.Parsing
13 import Language.Symantic.Parsing.Grammar
14 import Language.Symantic.Typing
15 import Language.Symantic.Compiling
16 import Language.Symantic.Interpreting
17 import Language.Symantic.Transforming.Trans
18
19 -- * Class 'Sym_Integer'
20 class Sym_Integer term where
21 integer :: Integer -> term Integer
22 default integer :: Trans t term => Integer -> t term Integer
23 integer = trans_lift . integer
24
25 type instance Sym_of_Iface (Proxy Integer) = Sym_Integer
26 type instance Consts_of_Iface (Proxy Integer) = Proxy Integer ': Consts_imported_by Integer
27 type instance Consts_imported_by Integer =
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_Integer HostI where
38 integer = HostI
39 instance Sym_Integer TextI where
40 integer a = TextI $ \_p _v ->
41 Text.pack (show a)
42 instance (Sym_Integer r1, Sym_Integer r2) => Sym_Integer (DupI r1 r2) where
43 integer x = integer x `DupI` integer x
44
45 instance
46 ( Read_TypeNameR Type_Name cs rs
47 , Inj_Const cs Integer
48 ) => Read_TypeNameR Type_Name cs (Proxy Integer ': rs) where
49 read_typenameR _cs (Type_Name "Integer") k = k (ty @Integer)
50 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
51 instance Show_Const cs => Show_Const (Proxy Integer ': cs) where
52 show_const ConstZ{} = "Integer"
53 show_const (ConstS c) = show_const c
54
55 instance -- Proj_ConC
56 ( Proj_Const cs Integer
57 , Proj_Consts cs (Consts_imported_by Integer)
58 ) => Proj_ConC cs (Proxy Integer) where
59 proj_conC _ (TyConst q :$ TyConst c)
60 | Just Refl <- eq_skind (kind_of_const c) SKiType
61 , Just Refl <- proj_const c (Proxy @Integer)
62 = case () of
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
70 _ -> Nothing
71 proj_conC _c _q = Nothing
72 data instance TokenT meta (ts::[*]) (Proxy Integer)
73 = Token_Term_Integer Integer
74 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Integer))
75 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Integer))
76 instance -- CompileI
77 Inj_Const (Consts_of_Ifaces is) Integer =>
78 CompileI is (Proxy Integer) where
79 compileI tok _ctx k =
80 case tok of
81 Token_Term_Integer i -> k (ty @Integer) $ TermO $ \_c -> integer i
82 instance -- TokenizeT
83 -- Inj_Token meta ts Integer =>
84 TokenizeT meta ts (Proxy Integer)
85 instance -- Gram_Term_AtomsT
86 ( Alt g
87 , Alter g
88 , Alternative g
89 , Gram_Rule g
90 , Gram_Lexer g
91 , Gram_Meta meta g
92 , Inj_Token meta ts Integer
93 ) => Gram_Term_AtomsT meta ts (Proxy Integer) g where
94 term_atomsT _t =
95 [ rule "term_integer" $
96 lexeme $ metaG $
97 (\i meta -> ProTok $ inj_etoken meta $ Token_Term_Integer $ read i)
98 <$> some (choice $ char <$> ['0'..'9'])
99 ]