git.iko.soy/Idris-dev
on 7fefa89 help sign in
Idris-dev/src/Idris/Primitives.hs
340 lines 13 kB history raw
1{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
3module Idris.Primitives(elabPrims) where
5import Idris.ElabDecls
6import Idris.ElabTerm
7import Idris.AbsSyntax
9import IRTS.Lang
11import Core.TT
12import Core.Evaluate
13import Data.Bits
15data Prim = Prim { p_name :: Name,
16 p_type :: Type,
17 p_arity :: Int,
18 p_def :: [Value] -> Maybe Value,
19 p_lexp :: (Int, PrimFn),
20 p_total :: Totality
21 }
23ty [] x = Constant x
24ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
26believeTy = Bind (UN "a") (Pi (Set (UVar (-2))))
27 (Bind (UN "b") (Pi (Set (UVar (-2))))
28 (Bind (UN "x") (Pi (V 1)) (V 1)))
30total = Total []
31partial = Partial NotCovering
33primitives =
34 -- operators
35 [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))
36 (2, LPlus) total,
37 Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))
38 (2, LMinus) total,
39 Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))
40 (2, LTimes) total,
41 Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin div)
42 (2, LDiv) partial,
43 Prim (UN "prim__modInt") (ty [IType, IType] IType) 2 (iBin mod)
44 (2, LMod) partial,
45 Prim (UN "prim__andInt") (ty [IType, IType] IType) 2 (iBin (.&.))
46 (2, LAnd) partial,
47 Prim (UN "prim__orInt") (ty [IType, IType] IType) 2 (iBin (.|.))
48 (2, LOr) partial,
49 Prim (UN "prim__xorInt") (ty [IType, IType] IType) 2 (iBin xor)
50 (2, LXOr) partial,
51 Prim (UN "prim__shLInt") (ty [IType, IType] IType) 2 (iBin shiftL)
52 (2, LSHL) partial,
53 Prim (UN "prim__shRInt") (ty [IType, IType] IType) 2 (iBin shiftR)
54 (2, LSHR) partial,
55 Prim (UN "prim__complInt") (ty [IType] IType) 1 (iUn complement)
56 (1, LCompl) partial,
57 Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))
58 (2, LEq) total,
59 Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))
60 (2, LLt) total,
61 Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))
62 (2, LLe) total,
63 Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))
64 (2, LGt) total,
65 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))
66 (2, LGe) total,
67 Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))
68 (2, LEq) total,
69 Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))
70 (2, LLt) total,
71 Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))
72 (2, LLe) total,
73 Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))
74 (2, LGt) total,
75 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))
76 (2, LGe) total,
78 Prim (UN "prim__addW8") (ty [W8Type, W8Type] W8Type) 2 (w8Bin (+))
79 (2, LW8Plus) total,
80 Prim (UN "prim__subW8") (ty [W8Type, W8Type] W8Type) 2 (w8Bin (-))
81 (2, LW8Minus) total,
82 Prim (UN "prim__mulW8") (ty [W8Type, W8Type] W8Type) 2 (w8Bin (*))
83 (2, LW8Times) total,
85 Prim (UN "prim__addW16") (ty [W16Type, W16Type] W16Type) 2 (w16Bin (+))
86 (2, LW16Plus) total,
87 Prim (UN "prim__subW16") (ty [W16Type, W16Type] W16Type) 2 (w16Bin (-))
88 (2, LW16Minus) total,
89 Prim (UN "prim__mulW16") (ty [W16Type, W16Type] W16Type) 2 (w16Bin (*))
90 (2, LW16Times) total,
92 Prim (UN "prim__intToWord8") (ty [IType] W8Type) 1 intToWord8
93 (1, LW8) total,
94 Prim (UN "prim__intToWord16") (ty [IType] W16Type) 1 intToWord16
95 (1, LW16) total,
97 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))
98 (2, LBPlus) total,
99 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))
100 (2, LBMinus) total,
101 Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))
102 (2, LBTimes) total,
103 Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin div)
104 (2, LBDiv) partial,
105 Prim (UN "prim__modBigInt") (ty [BIType, BIType] BIType) 2 (bBin mod)
106 (2, LBMod) partial,
107 Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))
108 (2, LBEq) total,
109 Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))
110 (2, LBLt) total,
111 Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))
112 (2, LBLe) total,
113 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))
114 (2, LBGt) total,
115 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))
116 (2, LBGe) total,
117 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))
118 (2, LFPlus) total,
119 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))
120 (2, LFMinus) total,
121 Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))
122 (2, LFTimes) total,
123 Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))
124 (2, LFDiv) total,
125 Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))
126 (2, LFEq) total,
127 Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))
128 (2, LFLt) total,
129 Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))
130 (2, LFLe) total,
131 Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))
132 (2, LFGt) total,
133 Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))
134 (2, LFGe) total,
135 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
136 (2, LStrConcat) total,
137 Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))
138 (2, LStrEq) total,
139 Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))
140 (2, LStrLt) total,
141 -- Conversions
142 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)
143 (1, LStrInt) total,
144 Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)
145 (1, LIntStr) total,
146 Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)
147 (1, LNoOp) total,
148 Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)
149 (1, LNoOp) total,
150 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)
151 (1, LIntBig) total,
152 Prim (UN "prim__bigIntToInt") (ty [BIType] IType) 1 (c_bigIntToInt)
153 (1, LBigInt) total,
154 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)
155 (1, LStrBig) total,
156 Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)
157 (1, LBigStr) total,
158 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)
159 (1, LStrFloat) total,
160 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)
161 (1, LFloatStr) total,
162 Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)
163 (1, LIntFloat) total,
164 Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)
165 (1, LFloatInt) total,
167 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)
168 (1, LFExp) total,
169 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)
170 (1, LFLog) total,
171 Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)
172 (1, LFSin) total,
173 Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos)
174 (1, LFCos) total,
175 Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan)
176 (1, LFTan) total,
177 Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin)
178 (1, LFASin) total,
179 Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos)
180 (1, LFACos) total,
181 Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan)
182 (1, LFATan) total,
183 Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt)
184 (1, LFSqrt) total,
185 Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor)
186 (1, LFFloor) total,
187 Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil)
188 (1, LFCeil) total,
190 Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)
191 (1, LStrHead) partial,
192 Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)
193 (1, LStrTail) partial,
194 Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)
195 (2, LStrCons) total,
196 Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)
197 (2, LStrIndex) partial,
198 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)
199 (1, LStrRev) total,
200 Prim (UN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)
201 (1, LReadStr) partial,
202 Prim (UN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)
203 (0, LVMPtr) total,
204 -- Streams
205 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)
206 (0, LStdIn) partial,
207 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)
208 (3, LNoOp) partial -- ahem
209 ]
211p_believeMe [_,_,x] = Just x
212p_believeMe _ = Nothing
214iUn op [VConstant (I x)] = Just $ VConstant (I (op x))
215iUn _ _ = Nothing
217iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
218iBin _ _ = Nothing
220bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))
221bBin _ _ = Nothing
223bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))
224bBini _ _ = Nothing
226biBin op = iBin (\x y -> if (op x y) then 1 else 0)
227bbBin op = bBini (\x y -> if (op x y) then 1 else 0)
229fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))
230fBin _ _ = Nothing
232bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in
233 Just $ VConstant (I i)
234bfBin _ _ = Nothing
236bcBin op [VConstant (Ch x), VConstant (Ch y)] = let i = (if op x y then 1 else 0) in
237 Just $ VConstant (I i)
238bcBin _ _ = Nothing
240bsBin op [VConstant (Str x), VConstant (Str y)]
241 = let i = (if op x y then 1 else 0) in
242 Just $ VConstant (I i)
243bsBin _ _ = Nothing
245sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
246sBin _ _ = Nothing
248w8Bin op [VConstant (W8 x), VConstant (W8 y)] = Just $ VConstant (W8 (op x y))
249w8Bin _ _ = Nothing
251w16Bin op [VConstant (W16 x), VConstant (W16 y)] = Just $ VConstant (W16 (op x y))
252w16Bin _ _ = Nothing
254-- w32Bin op [VConstant (W32 x), VConstant (W32 y)] = Just $ VConstant (W32 (op x y))
255-- w32Bin _ _ = Nothing
257intToWord8 [VConstant (I x)] = Just $ VConstant (W8 $ fromIntegral x)
258intToWord8 _ = Nothing
259intToWord16 [VConstant (I x)] = Just $ VConstant (W16 $ fromIntegral x)
260intToWord16 _ = Nothing
262c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))
263c_intToStr _ = Nothing
264c_strToInt [VConstant (Str x)] = case reads x of
265 [(n,"")] -> Just $ VConstant (I n)
266 _ -> Just $ VConstant (I 0)
267c_strToInt _ = Nothing
269c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))
270c_intToChar _ = Nothing
271c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))
272c_charToInt _ = Nothing
274c_intToBigInt [VConstant (I x)] = Just $ VConstant (BI (fromIntegral x))
275c_intToBigInt _ = Nothing
276c_bigIntToInt [VConstant (BI x)] = Just $ VConstant (I (fromInteger x))
277c_bigIntToInt _ = Nothing
279c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x))
280c_bigIntToStr _ = Nothing
281c_strToBigInt [VConstant (Str x)] = case reads x of
282 [(n,"")] -> Just $ VConstant (BI n)
283 _ -> Just $ VConstant (BI 0)
284c_strToBigInt _ = Nothing
286c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
287c_floatToStr _ = Nothing
288c_strToFloat [VConstant (Str x)] = case reads x of
289 [(n,"")] -> Just $ VConstant (Fl n)
290 _ -> Just $ VConstant (Fl 0)
291c_strToFloat _ = Nothing
293c_floatToInt [VConstant (Fl x)] = Just $ VConstant (I (truncate x))
294c_floatToInt _ = Nothing
296c_intToFloat [VConstant (I x)] = Just $ VConstant (Fl (fromIntegral x))
297c_intToFloat _ = Nothing
299p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))
300p_fPrim f _ = Nothing
302p_floatExp = p_fPrim exp
303p_floatLog = p_fPrim log
304p_floatSin = p_fPrim sin
305p_floatCos = p_fPrim cos
306p_floatTan = p_fPrim tan
307p_floatASin = p_fPrim asin
308p_floatACos = p_fPrim acos
309p_floatATan = p_fPrim atan
310p_floatSqrt = p_fPrim sqrt
311p_floatFloor = p_fPrim (fromInteger . floor)
312p_floatCeil = p_fPrim (fromInteger . ceiling)
314p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)
315p_strHead _ = Nothing
316p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)
317p_strTail _ = Nothing
318p_strIndex [VConstant (Str xs), VConstant (I i)]
319 | i < length xs = Just $ VConstant (Ch (xs!!i))
320p_strIndex _ = Nothing
321p_strCons [VConstant (Ch x), VConstant (Str xs)] = Just $ VConstant (Str (x:xs))
322p_strCons _ = Nothing
323p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))
324p_strRev _ = Nothing
326p_cantreduce _ = Nothing
328elabPrim :: Prim -> Idris ()
329elabPrim (Prim n ty i def sc tot)
330 = do updateContext (addOperator n ty i def)
331 setTotality n tot
332 i <- getIState
333 putIState i { idris_scprims = (n, sc) : idris_scprims i }
335elabPrims :: Idris ()
336elabPrims = do mapM_ (elabDecl EAll toplevel)
337 (map (PData "" defaultSyntax (FC "builtin" 0) False)
338 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
339 mapM_ elabPrim primitives