1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Num'.
4 module Language.Symantic.Lib.Num where
6 import Control.Monad (liftM, liftM2)
7 import qualified Data.Function as Fun
9 import Data.Type.Equality ((:~:)(Refl))
10 import qualified Prelude
11 import Prelude hiding (Num(..))
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
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
27 (-) :: Num n => term n -> term n -> term n
28 (*) :: Num n => term n -> term n -> term n
29 fromInteger :: Num n => term Integer -> term n
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
40 negate = trans_map1 negate
41 signum = trans_map1 signum
45 fromInteger = trans_map1 fromInteger
51 type instance Sym_of_Iface (Proxy Num) = Sym_Num
52 type instance Consts_of_Iface (Proxy Num) = Proxy Num ': Consts_imported_by Num
53 type instance Consts_imported_by Num =
57 instance Sym_Num HostI where
58 abs = liftM Prelude.abs
59 negate = liftM Prelude.negate
60 signum = liftM Prelude.signum
61 (+) = liftM2 (Prelude.+)
62 (-) = liftM2 (Prelude.-)
63 (*) = liftM2 (Prelude.*)
64 fromInteger = liftM Prelude.fromInteger
65 instance Sym_Num TextI where
67 negate = textI1 "negate"
68 signum = textI1 "signum"
69 (+) = textI_infix "+" (infixB L 6)
70 (-) = textI_infix "-" (infixL 6)
71 (*) = textI_infix "*" (infixB L 7)
72 fromInteger = textI1 "fromInteger"
73 instance (Sym_Num r1, Sym_Num r2) => Sym_Num (DupI r1 r2) where
74 abs = dupI1 (Proxy @Sym_Num) abs
75 negate = dupI1 (Proxy @Sym_Num) negate
76 signum = dupI1 (Proxy @Sym_Num) signum
77 (+) = dupI2 (Proxy @Sym_Num) (+)
78 (-) = dupI2 (Proxy @Sym_Num) (-)
79 (*) = dupI2 (Proxy @Sym_Num) (*)
80 fromInteger = dupI1 (Proxy @Sym_Num) fromInteger
83 ( Read_TypeNameR Type_Name cs rs
85 ) => Read_TypeNameR Type_Name cs (Proxy Num ': rs) where
86 read_typenameR _cs (Type_Name "Num") k = k (ty @Num)
87 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
88 instance Show_Const cs => Show_Const (Proxy Num ': cs) where
89 show_const ConstZ{} = "Num"
90 show_const (ConstS c) = show_const c
92 instance Proj_ConC cs (Proxy Num)
93 data instance TokenT meta (ts::[*]) (Proxy Num)
94 = Token_Term_Num_abs (EToken meta ts)
95 | Token_Term_Num_negate (EToken meta ts)
96 | Token_Term_Num_signum (EToken meta ts)
97 | Token_Term_Num_add (EToken meta ts)
98 | Token_Term_Num_sub (EToken meta ts)
99 | Token_Term_Num_mul (EToken meta ts)
100 | Token_Term_Num_fromInteger (EToken meta '[Proxy Token_Type])
101 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Num))
102 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Num))
104 ( Read_TypeName Type_Name (Consts_of_Ifaces is)
105 , Inj_Const (Consts_of_Ifaces is) Num
106 , Inj_Const (Consts_of_Ifaces is) (->)
107 , Inj_Const (Consts_of_Ifaces is) Integer
108 , Proj_Con (Consts_of_Ifaces is)
110 ) => CompileI is (Proxy Num) where
113 Token_Term_Num_abs tok_a -> op1_from tok_a abs
114 Token_Term_Num_negate tok_a -> op1_from tok_a negate
115 Token_Term_Num_signum tok_a -> op1_from tok_a signum
116 Token_Term_Num_add tok_a -> op2_from tok_a (+)
117 Token_Term_Num_sub tok_a -> op2_from tok_a (-)
118 Token_Term_Num_mul tok_a -> op2_from tok_a (*)
119 Token_Term_Num_fromInteger tok_ty_a ->
120 -- fromInteger :: Num a => Integer -> a
121 compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
124 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
125 check_con (At (Just tok_ty_a) (ty @Num :$ ty_a)) $ \Con ->
126 k (ty @Integer ~> ty_a) $ TermO $
127 Fun.const $ lam fromInteger
130 (op::forall term a. (Sym_Num term, Num a)
131 => term a -> term a) =
132 -- abs :: Num a => a -> a
133 -- negate :: Num a => a -> a
134 -- signum :: Num a => a -> a
135 compileO tok_a ctx $ \ty_a (TermO x) ->
136 check_con (At (Just tok_a) (ty @Num :$ ty_a)) $ \Con ->
140 (op::forall term a. (Sym_Num term, Num a)
141 => term a -> term a -> term a) =
142 -- (+) :: Num a => a -> a -> a
143 -- (-) :: Num a => a -> a -> a
144 -- (*) :: Num a => a -> a -> a
145 compileO tok_a ctx $ \ty_a (TermO x) ->
146 check_con (At (Just tok_a) (ty @Num :$ ty_a)) $ \Con ->
147 k (ty_a ~> ty_a) $ TermO $
148 \c -> lam $ \y -> op (x c) y
149 instance -- TokenizeT
150 Inj_Token meta ts Num =>
151 TokenizeT meta ts (Proxy Num) where
152 tokenizeT _t = mempty
153 { tokenizers_infix = tokenizeTMod []
154 [ tokenize1 "abs" infixN5 Token_Term_Num_abs
155 , tokenize1 "negate" infixN5 Token_Term_Num_negate
156 , tokenize1 "signum" infixN5 Token_Term_Num_signum
157 , tokenize1 "+" (infixB L 6) Token_Term_Num_add
158 , tokenize1 "-" (infixL 6) Token_Term_Num_sub
159 , tokenize1 "*" (infixB L 7) Token_Term_Num_mul
160 , (Term_Name "fromInteger",) Term_ProTok
161 { term_protok = \meta -> ProTokPi $ \a ->
162 ProTok $ inj_etoken meta $ Token_Term_Num_fromInteger a
163 , term_fixity = infixN5
166 , tokenizers_prefix = tokenizeTMod []
167 [ tokenize1 "-" (Prefix 10) Token_Term_Num_negate
170 instance Gram_Term_AtomsT meta ts (Proxy Num) g