]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Integral.hs
Rename Term_Name -> TeName
[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 qualified Prelude
10 import Prelude (Integral)
11 import Prelude hiding (Integral(..))
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 Integral
48 type instance TyConsts_imported_by 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 instance -- CompileI
99 ( Read_TyName TyName cs
100 , Inj_TyConst cs Integral
101 , Inj_TyConst cs (->)
102 , Inj_TyConst cs (,)
103 , Inj_TyConst cs Integer
104 , Proj_TyCon cs
105 , Compile cs is
106 ) => CompileI cs is (Proxy Integral) where
107 compileI tok ctx k =
108 case tok of
109 Token_Term_Integral_quot tok_a -> op2_from tok_a quot
110 Token_Term_Integral_rem tok_a -> op2_from tok_a rem
111 Token_Term_Integral_div tok_a -> op2_from tok_a div
112 Token_Term_Integral_mod tok_a -> op2_from tok_a mod
113 Token_Term_Integral_quotRem tok_a -> op2t2_from tok_a quotRem
114 Token_Term_Integral_divMod tok_a -> op2t2_from tok_a divMod
115 Token_Term_Integral_toInteger tok_a ->
116 -- toInteger :: Integral a => a -> Integer
117 compileO tok_a ctx $ \ty_a (TermO a) ->
118 check_TyCon (At (Just tok_a) (ty @Integral :$ ty_a)) $ \TyCon ->
119 k (ty @Integer) $ TermO $
120 \c -> toInteger (a c)
121 where
122 op2_from tok_a
123 (op::forall term a. (Sym_Integral term, Integral a)
124 => term a -> term a -> term a) =
125 -- quot :: Integral i => i -> i -> i
126 -- rem :: Integral i => i -> i -> i
127 -- div :: Integral i => i -> i -> i
128 -- mod :: Integral i => i -> i -> i
129 compileO tok_a ctx $ \ty_a (TermO x) ->
130 check_TyCon (At (Just tok_a) (ty @Integral :$ ty_a)) $ \TyCon ->
131 k (ty_a ~> ty_a) $ TermO $
132 \c -> lam $ \y -> op (x c) y
133 op2t2_from tok_a
134 (op::forall term a. (Sym_Integral term, Integral a)
135 => term a -> term a -> term (a, a)) =
136 -- quotRem :: Integral i => i -> i -> (i, i)
137 -- divMod :: Integral i => i -> i -> (i, i)
138 compileO tok_a ctx $ \ty_a (TermO x) ->
139 check_TyCon (At (Just tok_a) (ty @Integral :$ ty_a)) $ \TyCon ->
140 k (ty_a ~> (ty @(,) :$ ty_a) :$ ty_a) $ TermO $
141 \c -> lam $ \y -> op (x c) y
142 instance -- TokenizeT
143 Inj_Token meta ts Integral =>
144 TokenizeT meta ts (Proxy Integral) where
145 tokenizeT _t = mempty
146 { tokenizers_infix = tokenizeTMod []
147 [ tokenize1 "quot" (infixL 7) Token_Term_Integral_quot
148 , tokenize1 "rem" (infixL 7) Token_Term_Integral_rem
149 , tokenize1 "div" (infixL 7) Token_Term_Integral_div
150 , tokenize1 "mod" (infixL 7) Token_Term_Integral_mod
151 , tokenize1 "quotRem" infixN5 Token_Term_Integral_quotRem
152 , tokenize1 "divMod" infixN5 Token_Term_Integral_divMod
153 , tokenize1 "toInteger" infixN5 Token_Term_Integral_toInteger
154 ]
155 }
156 instance Gram_Term_AtomsT meta ts (Proxy Integral) g