git.iko.soy/Idris-dev
on 9f65713 help sign in
Idris-dev/src/Idris/Primitives.hs
196 lines 7.8 kB history raw
1{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
3module Idris.Primitives(elabPrims) where
5import Idris.ElabDecls
6import Idris.ElabTerm
7import Idris.AbsSyntax
9import Core.TT
10import Core.Evaluate
12import Epic.Epic hiding (Term, Type, Name, fn)
13import qualified Epic.Epic as E
15data Prim = Prim { p_name :: Name,
16 p_type :: Type,
17 p_arity :: Int,
18 p_def :: [Value] -> Maybe Value,
19 p_epic :: ([E.Name], E.Term)
20 }
22ty [] x = Constant x
23ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
25type ETm = E.Term
26type EOp = E.Op
28fun = E.fn
29ref = E.ref
31eOp :: EOp -> ([E.Name], ETm)
32eOp op = ([E.name "x", E.name "y"], E.op_ op (E.fn "x") (E.fn "y"))
34eOpFn :: E.Type -> E.Type -> String -> ([E.Name], ETm)
35eOpFn ty rty op = ([E.name "x", E.name "y"],
36 foreign_ rty op [(E.fn "x", ty), (E.fn "y", ty)])
38strToInt x = foreign_ tyInt "strToInt" [(x, tyString)]
39intToStr x = foreign_ tyString "intToStr" [(x, tyInt)]
40intToBigInt x = foreign_ tyBigInt "intToBigInt" [(x, tyInt)]
41strToBigInt x = foreign_ tyBigInt "strToBig" [(x, tyString)]
42bigIntToStr x = foreign_ tyString "bigToStr" [(x, tyBigInt)]
43strToFloat x = foreign_ tyFloat "strToFloat" [(x, tyString)]
44floatToStr x = foreign_ tyString "floatToStr" [(x, tyFloat)]
45intToFloat x = foreign_ tyFloat "intToFloat" [(x, tyInt)]
46floatToInt x = foreign_ tyInt "floatToInt" [(x, tyFloat)]
48floatExp x = foreign_ tyFloat "exp" [(x, tyFloat)]
49floatLog x = foreign_ tyFloat "log" [(x, tyFloat)]
51primitives =
52 -- operators
53 [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))
54 (eOp E.plus_),
55 Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))
56 (eOp E.minus_),
57 Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))
58 (eOp E.times_),
59 Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin (div))
60 (eOp E.divide_),
61 Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))
62 (eOp E.eq_),
63 Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))
64 (eOp E.lt_),
65 Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))
66 (eOp E.lte_),
67 Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))
68 (eOp E.gt_),
69 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))
70 (eOp E.gte_),
71 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))
72 (eOpFn tyBigInt tyBigInt "addBig"),
73 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))
74 (eOpFn tyBigInt tyBigInt "subBig"),
75 Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))
76 (eOpFn tyBigInt tyBigInt "mulBig"),
77 Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin (div))
78 (eOpFn tyBigInt tyBigInt "divBig"),
79 Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))
80 (eOpFn tyBigInt tyInt "eqBig"),
81 Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))
82 (eOpFn tyBigInt tyInt "ltBig"),
83 Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))
84 (eOpFn tyBigInt tyInt "leBig"),
85 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))
86 (eOpFn tyBigInt tyInt "gtBig"),
87 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))
88 (eOpFn tyBigInt tyInt "geBig"),
89 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))
90 (eOp E.plusF_),
91 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))
92 (eOp E.minusF_),
93 Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))
94 (eOp E.timesF_),
95 Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))
96 (eOp E.divideF_),
97 Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))
98 (eOp E.eqF_),
99 Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))
100 (eOp E.ltF_),
101 Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))
102 (eOp E.lteF_),
103 Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))
104 (eOp E.gtF_),
105 Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))
106 (eOp E.gteF_),
107 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
108 ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y"),
109 -- Conversions
110 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)
111 ([E.name "x"], strToInt (fun "x")),
112 Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)
113 ([E.name "x"], intToStr (fun "x")),
114 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)
115 ([E.name "x"], intToBigInt (fun "x")),
116 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)
117 ([E.name "x"], strToBigInt (fun "x")),
118 Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)
119 ([E.name "x"], bigIntToStr (fun "x")),
120 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)
121 ([E.name "x"], strToFloat (fun "x")),
122 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)
123 ([E.name "x"], floatToStr (fun "x")),
124 Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)
125 ([E.name "x"], intToFloat (fun "x")),
126 Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)
127 ([E.name "x"], floatToInt (fun "x")),
128 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)
129 ([E.name "x"], floatExp (fun "x")),
130 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)
131 ([E.name "x"], floatLog (fun "x"))
132 ]
134iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
135iBin _ _ = Nothing
137bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))
138bBin _ _ = Nothing
140bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))
141bBini _ _ = Nothing
143biBin op = iBin (\x y -> if (op x y) then 1 else 0)
144bbBin op = bBini (\x y -> if (op x y) then 1 else 0)
146fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))
147fBin _ _ = Nothing
149bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in
150 Just $ VConstant (I i)
151bfBin _ _ = Nothing
153sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
154sBin _ _ = Nothing
156c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))
157c_intToStr _ = Nothing
158c_strToInt [VConstant (Str x)] = Just $ VConstant (I (read x))
159c_strToInt _ = Nothing
161c_intToBigInt [VConstant (I x)] = Just $ VConstant (BI (fromIntegral x))
162c_intToBigInt _ = Nothing
164c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x))
165c_bigIntToStr _ = Nothing
166c_strToBigInt [VConstant (Str x)] = Just $ VConstant (BI (read x))
167c_strToBigInt _ = Nothing
169c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
170c_floatToStr _ = Nothing
171c_strToFloat [VConstant (Str x)] = Just $ VConstant (Fl (read x))
172c_strToFloat _ = Nothing
174c_floatToInt [VConstant (Fl x)] = Just $ VConstant (I (truncate x))
175c_floatToInt _ = Nothing
177c_intToFloat [VConstant (I x)] = Just $ VConstant (Fl (fromIntegral x))
178c_intToFloat _ = Nothing
180p_floatExp [VConstant (Fl x)] = Just $ VConstant (Fl (exp x))
181p_floatExp _ = Nothing
182p_floatLog [VConstant (Fl x)] = Just $ VConstant (Fl (log x))
183p_floatLog _ = Nothing
185elabPrim :: Prim -> Idris ()
186elabPrim (Prim n ty i def epic)
187 = do updateContext (addOperator n ty i def)
188 i <- getIState
189 putIState i { idris_prims = (n, epic) : idris_prims i }
191elabPrims :: Idris ()
192elabPrims = do mapM_ (elabDecl toplevel)
193 (map (PData defaultSyntax (FC "builtin" 0))
194 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
195 mapM_ elabPrim primitives