]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Integral.hs
Add compileWithTyCtx.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Integral.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 {-# OPTIONS_GHC -fconstraint-solver-iterations=6 #-}
4 -- | Symantic for 'Integral'.
5 module Language.Symantic.Lib.Integral where
6
7 import Control.Monad (liftM, liftM2)
8 import Data.Proxy
9 import Prelude (Integral)
10 import Prelude hiding (Integral(..))
11 import qualified Prelude
12
13 import Language.Symantic.Parsing
14 import Language.Symantic.Typing
15 import Language.Symantic.Compiling
16 import Language.Symantic.Interpreting
17 import Language.Symantic.Transforming
18 import Language.Symantic.Lib.Lambda
19
20 -- * Class 'Sym_Integral'
21 class Sym_Integral term where
22 quot :: Integral i => term i -> term i -> term i; infixl 7 `quot`
23 rem :: Integral i => term i -> term i -> term i; infixl 7 `rem`
24 div :: Integral i => term i -> term i -> term i; infixl 7 `div`
25 mod :: Integral i => term i -> term i -> term i; infixl 7 `mod`
26 quotRem :: Integral i => term i -> term i -> term (i, i)
27 divMod :: Integral i => term i -> term i -> term (i, i)
28 toInteger :: Integral i => term i -> term Integer
29
30 default quot :: (Trans t term, Integral i) => t term i -> t term i -> t term i
31 default rem :: (Trans t term, Integral i) => t term i -> t term i -> t term i
32 default div :: (Trans t term, Integral i) => t term i -> t term i -> t term i
33 default mod :: (Trans t term, Integral i) => t term i -> t term i -> t term i
34 default quotRem :: (Trans t term, Integral i) => t term i -> t term i -> t term (i, i)
35 default divMod :: (Trans t term, Integral i) => t term i -> t term i -> t term (i, i)
36 default toInteger :: (Trans t term, Integral i) => t term i -> t term Integer
37
38 quot = trans_map2 quot
39 rem = trans_map2 rem
40 div = trans_map2 div
41 mod = trans_map2 mod
42 quotRem = trans_map2 quotRem
43 divMod = trans_map2 divMod
44 toInteger = trans_map1 toInteger
45
46 type instance Sym_of_Iface (Proxy Integral) = Sym_Integral
47 type instance TyConsts_of_Iface (Proxy Integral) = Proxy Integral ': TyConsts_imported_by (Proxy Integral)
48 type instance TyConsts_imported_by (Proxy Integral) =
49 '[ Proxy (,)
50 ]
51
52 instance Sym_Integral HostI where
53 quot = liftM2 Prelude.quot
54 rem = liftM2 Prelude.rem
55 div = liftM2 Prelude.div
56 mod = liftM2 Prelude.mod
57 quotRem = liftM2 Prelude.quotRem
58 divMod = liftM2 Prelude.divMod
59 toInteger = liftM Prelude.toInteger
60 instance Sym_Integral TextI where
61 quot = textI_infix "`quot`" (infixL 7)
62 div = textI_infix "`div`" (infixL 7)
63 rem = textI_infix "`rem`" (infixL 7)
64 mod = textI_infix "`mod`" (infixL 7)
65 quotRem = textI2 "quotRem"
66 divMod = textI2 "divMod"
67 toInteger = textI1 "toInteger"
68 instance (Sym_Integral r1, Sym_Integral r2) => Sym_Integral (DupI r1 r2) where
69 quot = dupI2 @Sym_Integral quot
70 rem = dupI2 @Sym_Integral rem
71 div = dupI2 @Sym_Integral div
72 mod = dupI2 @Sym_Integral mod
73 quotRem = dupI2 @Sym_Integral quotRem
74 divMod = dupI2 @Sym_Integral divMod
75 toInteger = dupI1 @Sym_Integral toInteger
76
77 instance
78 ( Read_TyNameR TyName cs rs
79 , Inj_TyConst cs Integral
80 ) => Read_TyNameR TyName cs (Proxy Integral ': rs) where
81 read_TyNameR _cs (TyName "Integral") k = k (ty @Integral)
82 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
83 instance Show_TyConst cs => Show_TyConst (Proxy Integral ': cs) where
84 show_TyConst TyConstZ{} = "Integral"
85 show_TyConst (TyConstS c) = show_TyConst c
86
87 instance Proj_TyConC cs (Proxy Integral)
88 data instance TokenT meta (ts::[*]) (Proxy Integral)
89 = Token_Term_Integral_quot (EToken meta ts)
90 | Token_Term_Integral_rem (EToken meta ts)
91 | Token_Term_Integral_div (EToken meta ts)
92 | Token_Term_Integral_mod (EToken meta ts)
93 | Token_Term_Integral_quotRem (EToken meta ts)
94 | Token_Term_Integral_divMod (EToken meta ts)
95 | Token_Term_Integral_toInteger (EToken meta ts)
96 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Integral))
97 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Integral))
98
99 instance -- CompileI
100 ( Read_TyName TyName cs
101 , Inj_TyConst cs Integral
102 , Inj_TyConst cs (->)
103 , Inj_TyConst cs (,)
104 , Inj_TyConst cs Integer
105 , Proj_TyCon cs
106 , Compile cs is
107 ) => CompileI cs is (Proxy Integral) where
108 compileI tok ctx k =
109 case tok of
110 Token_Term_Integral_quot tok_a -> op2_from tok_a quot
111 Token_Term_Integral_rem tok_a -> op2_from tok_a rem
112 Token_Term_Integral_div tok_a -> op2_from tok_a div
113 Token_Term_Integral_mod tok_a -> op2_from tok_a mod
114 Token_Term_Integral_quotRem tok_a -> op2t2_from tok_a quotRem
115 Token_Term_Integral_divMod tok_a -> op2t2_from tok_a divMod
116 Token_Term_Integral_toInteger tok_a ->
117 -- toInteger :: Integral a => a -> Integer
118 compile tok_a ctx $ \ty_a (Term a) ->
119 check_TyCon (At (Just tok_a) (ty @Integral :$ ty_a)) $ \TyCon ->
120 k (ty @Integer) $ Term $
121 \c -> toInteger (a c)
122 where
123 op2_from tok_a
124 (op::forall term a. (Sym_Integral term, Integral a)
125 => term a -> term a -> term a) =
126 -- quot :: Integral i => i -> i -> i
127 -- rem :: Integral i => i -> i -> i
128 -- div :: Integral i => i -> i -> i
129 -- mod :: Integral i => i -> i -> i
130 compile tok_a ctx $ \ty_a (Term x) ->
131 check_TyCon (At (Just tok_a) (ty @Integral :$ ty_a)) $ \TyCon ->
132 k (ty_a ~> ty_a) $ Term $
133 \c -> lam $ \y -> op (x c) y
134 op2t2_from tok_a
135 (op::forall term a. (Sym_Integral term, Integral a)
136 => term a -> term a -> term (a, a)) =
137 -- quotRem :: Integral i => i -> i -> (i, i)
138 -- divMod :: Integral i => i -> i -> (i, i)
139 compile tok_a ctx $ \ty_a (Term x) ->
140 check_TyCon (At (Just tok_a) (ty @Integral :$ ty_a)) $ \TyCon ->
141 k (ty_a ~> (ty @(,) :$ ty_a) :$ ty_a) $ Term $
142 \c -> lam $ \y -> op (x c) y
143 instance -- TokenizeT
144 Inj_Token meta ts Integral =>
145 TokenizeT meta ts (Proxy Integral) where
146 tokenizeT _t = mempty
147 { tokenizers_infix = tokenizeTMod []
148 [ tokenize1 "quot" (infixL 7) Token_Term_Integral_quot
149 , tokenize1 "rem" (infixL 7) Token_Term_Integral_rem
150 , tokenize1 "div" (infixL 7) Token_Term_Integral_div
151 , tokenize1 "mod" (infixL 7) Token_Term_Integral_mod
152 , tokenize1 "quotRem" infixN5 Token_Term_Integral_quotRem
153 , tokenize1 "divMod" infixN5 Token_Term_Integral_divMod
154 , tokenize1 "toInteger" infixN5 Token_Term_Integral_toInteger
155 ]
156 }
157 instance Gram_Term_AtomsT meta ts (Proxy Integral) g