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