git.iko.soy/Idris-dev
on fb3160e help sign in
Idris-dev/src/Idris/Primitives.hs
309 lines 13 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)
25believeTy = Bind (UN "a") (Pi (Set (UVar (-2))))
26 (Bind (UN "b") (Pi (Set (UVar (-2))))
27 (Bind (UN "x") (Pi (V 1)) (V 1)))
29type ETm = E.Term
30type EOp = E.Op
32fun = E.fn
33ref = E.ref
35eOp :: EOp -> ([E.Name], ETm)
36eOp op = ([E.name "x", E.name "y"], E.op_ op (E.fn "x") (E.fn "y"))
38eOpFn :: E.Type -> E.Type -> String -> ([E.Name], ETm)
39eOpFn ty rty op = ([E.name "x", E.name "y"],
40 foreign_ rty op [(E.fn "x", ty), (E.fn "y", ty)])
42strToInt x = foreign_ tyInt "strToInt" [(x, tyString)]
43intToStr x = foreign_ tyString "intToStr" [(x, tyInt)]
44charToInt x = x
45intToChar x = x
46intToBigInt x = foreign_ tyBigInt "intToBigInt" [(x, tyInt)]
47strToBigInt x = foreign_ tyBigInt "strToBig" [(x, tyString)]
48bigIntToStr x = foreign_ tyString "bigToStr" [(x, tyBigInt)]
49strToFloat x = foreign_ tyFloat "strToFloat" [(x, tyString)]
50floatToStr x = foreign_ tyString "floatToStr" [(x, tyFloat)]
51intToFloat x = foreign_ tyFloat "intToFloat" [(x, tyInt)]
52floatToInt x = foreign_ tyInt "floatToInt" [(x, tyFloat)]
54floatExp x = foreign_ tyFloat "exp" [(x, tyFloat)]
55floatLog x = foreign_ tyFloat "log" [(x, tyFloat)]
56floatSin x = foreign_ tyFloat "sin" [(x, tyFloat)]
57floatCos x = foreign_ tyFloat "cos" [(x, tyFloat)]
58floatTan x = foreign_ tyFloat "tan" [(x, tyFloat)]
59floatASin x = foreign_ tyFloat "asin" [(x, tyFloat)]
60floatACos x = foreign_ tyFloat "acos" [(x, tyFloat)]
61floatATan x = foreign_ tyFloat "atan" [(x, tyFloat)]
62floatFloor x = foreign_ tyFloat "floor" [(x, tyFloat)]
63floatCeil x = foreign_ tyFloat "ceil" [(x, tyFloat)]
64floatSqrt x = foreign_ tyFloat "sqrt" [(x, tyFloat)]
66strIndex x i = foreign_ tyChar "strIndex" [(x, tyString), (i, tyInt)]
67strHead x = foreign_ tyChar "strHead" [(x, tyString)]
68strTail x = foreign_ tyString "strTail" [(x, tyString)]
69strCons x xs = foreign_ tyString "strCons" [(x, tyChar), (xs, tyString)]
70strRev x = foreign_ tyString "strrev" [(x, tyString)]
71strEq x y = foreign_ tyInt "streq" [(x, tyString), (y, tyString)]
72strLt x y = foreign_ tyInt "strlt" [(x, tyString), (y, tyString)]
74primitives =
75 -- operators
76 [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))
77 (eOp E.plus_),
78 Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))
79 (eOp E.minus_),
80 Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))
81 (eOp E.times_),
82 Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin (div))
83 (eOp E.divide_),
84 Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))
85 (eOp E.eq_),
86 Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))
87 (eOp E.lt_),
88 Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))
89 (eOp E.lte_),
90 Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))
91 (eOp E.gt_),
92 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))
93 (eOp E.gte_),
94 Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))
95 (eOp E.eq_),
96 Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))
97 (eOp E.lt_),
98 Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))
99 (eOp E.lte_),
100 Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))
101 (eOp E.gt_),
102 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))
103 (eOp E.gte_),
104 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))
105 (eOpFn tyBigInt tyBigInt "addBig"),
106 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))
107 (eOpFn tyBigInt tyBigInt "subBig"),
108 Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))
109 (eOpFn tyBigInt tyBigInt "mulBig"),
110 Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin (div))
111 (eOpFn tyBigInt tyBigInt "divBig"),
112 Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))
113 (eOpFn tyBigInt tyInt "eqBig"),
114 Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))
115 (eOpFn tyBigInt tyInt "ltBig"),
116 Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))
117 (eOpFn tyBigInt tyInt "leBig"),
118 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))
119 (eOpFn tyBigInt tyInt "gtBig"),
120 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))
121 (eOpFn tyBigInt tyInt "geBig"),
122 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))
123 (eOp E.plusF_),
124 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))
125 (eOp E.minusF_),
126 Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))
127 (eOp E.timesF_),
128 Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))
129 (eOp E.divideF_),
130 Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))
131 (eOp E.eqF_),
132 Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))
133 (eOp E.ltF_),
134 Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))
135 (eOp E.lteF_),
136 Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))
137 (eOp E.gtF_),
138 Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))
139 (eOp E.gteF_),
140 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
141 ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y"),
142 Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))
143 ([E.name "x", E.name "y"], strEq (fun "x") (fun "y")),
144 Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))
145 ([E.name "x", E.name "y"], strLt (fun "x") (fun "y")),
146 -- Conversions
147 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)
148 ([E.name "x"], strToInt (fun "x")),
149 Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)
150 ([E.name "x"], intToStr (fun "x")),
151 Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)
152 ([E.name "x"], charToInt (fun "x")),
153 Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)
154 ([E.name "x"], intToChar (fun "x")),
155 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)
156 ([E.name "x"], intToBigInt (fun "x")),
157 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)
158 ([E.name "x"], strToBigInt (fun "x")),
159 Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)
160 ([E.name "x"], bigIntToStr (fun "x")),
161 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)
162 ([E.name "x"], strToFloat (fun "x")),
163 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)
164 ([E.name "x"], floatToStr (fun "x")),
165 Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)
166 ([E.name "x"], intToFloat (fun "x")),
167 Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)
168 ([E.name "x"], floatToInt (fun "x")),
170 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)
171 ([E.name "x"], floatExp (fun "x")),
172 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)
173 ([E.name "x"], floatLog (fun "x")),
174 Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)
175 ([E.name "x"], floatSin (fun "x")),
176 Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos)
177 ([E.name "x"], floatCos (fun "x")),
178 Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan)
179 ([E.name "x"], floatTan (fun "x")),
180 Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin)
181 ([E.name "x"], floatASin (fun "x")),
182 Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos)
183 ([E.name "x"], floatACos (fun "x")),
184 Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan)
185 ([E.name "x"], floatATan (fun "x")),
186 Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt)
187 ([E.name "x"], floatSqrt (fun "x")),
188 Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor)
189 ([E.name "x"], floatFloor (fun "x")),
190 Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil)
191 ([E.name "x"], floatCeil (fun "x")),
193 Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)
194 ([E.name "x"], strHead (fun "x")),
195 Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)
196 ([E.name "x"], strTail (fun "x")),
197 Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)
198 ([E.name "x", E.name "xs"], strCons (fun "x") (fun "xs")),
199 Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)
200 ([E.name "x", E.name "i"], strIndex (fun "x") (fun "i")),
201 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)
202 ([E.name "x"], strRev (fun "x")),
204 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)
205 ([E.name "a", E.name "b", E.name "x"], fun "x")
206 ]
208p_believeMe [_,_,x] = Just x
209p_believeMe _ = Nothing
211iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
212iBin _ _ = Nothing
214bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))
215bBin _ _ = Nothing
217bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))
218bBini _ _ = Nothing
220biBin op = iBin (\x y -> if (op x y) then 1 else 0)
221bbBin op = bBini (\x y -> if (op x y) then 1 else 0)
223fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))
224fBin _ _ = Nothing
226bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in
227 Just $ VConstant (I i)
228bfBin _ _ = Nothing
230bcBin op [VConstant (Ch x), VConstant (Ch y)] = let i = (if op x y then 1 else 0) in
231 Just $ VConstant (I i)
232bcBin _ _ = Nothing
234bsBin op [VConstant (Str x), VConstant (Str y)]
235 = let i = (if op x y then 1 else 0) in
236 Just $ VConstant (I i)
237bsBin _ _ = Nothing
239sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
240sBin _ _ = Nothing
242c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))
243c_intToStr _ = Nothing
244c_strToInt [VConstant (Str x)] = Just $ VConstant (I (read x))
245c_strToInt _ = Nothing
247c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))
248c_intToChar _ = Nothing
249c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))
250c_charToInt _ = Nothing
252c_intToBigInt [VConstant (I x)] = Just $ VConstant (BI (fromIntegral x))
253c_intToBigInt _ = Nothing
255c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x))
256c_bigIntToStr _ = Nothing
257c_strToBigInt [VConstant (Str x)] = Just $ VConstant (BI (read x))
258c_strToBigInt _ = Nothing
260c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
261c_floatToStr _ = Nothing
262c_strToFloat [VConstant (Str x)] = Just $ VConstant (Fl (read x))
263c_strToFloat _ = Nothing
265c_floatToInt [VConstant (Fl x)] = Just $ VConstant (I (truncate x))
266c_floatToInt _ = Nothing
268c_intToFloat [VConstant (I x)] = Just $ VConstant (Fl (fromIntegral x))
269c_intToFloat _ = Nothing
271p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))
272p_fPrim f _ = Nothing
274p_floatExp = p_fPrim exp
275p_floatLog = p_fPrim log
276p_floatSin = p_fPrim sin
277p_floatCos = p_fPrim cos
278p_floatTan = p_fPrim tan
279p_floatASin = p_fPrim asin
280p_floatACos = p_fPrim acos
281p_floatATan = p_fPrim atan
282p_floatSqrt = p_fPrim sqrt
283p_floatFloor = p_fPrim (fromInteger . floor)
284p_floatCeil = p_fPrim (fromInteger . ceiling)
286p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)
287p_strHead _ = Nothing
288p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)
289p_strTail _ = Nothing
290p_strIndex [VConstant (Str xs), VConstant (I i)]
291 | i < length xs = Just $ VConstant (Ch (xs!!i))
292p_strIndex _ = Nothing
293p_strCons [VConstant (Ch x), VConstant (Str xs)] = Just $ VConstant (Str (x:xs))
294p_strCons _ = Nothing
295p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))
296p_strRev _ = Nothing
298elabPrim :: Prim -> Idris ()
299elabPrim (Prim n ty i def epic)
300 = do updateContext (addOperator n ty i def)
301 i <- getIState
302 putIState i { idris_prims = (n, epic) : idris_prims i }
304elabPrims :: Idris ()
305elabPrims = do mapM_ (elabDecl toplevel)
306 (map (PData defaultSyntax (FC "builtin" 0))
307 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
308 mapM_ elabPrim primitives