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