git.iko.soy/Idris-dev
on 25aef32 help sign in
Idris-dev/src/Idris/Primitives.hs
654 lines 27 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
14import Data.Word
15import Data.Int
17data Prim = Prim { p_name :: Name,
18 p_type :: Type,
19 p_arity :: Int,
20 p_def :: [Value] -> Maybe Value,
21 p_lexp :: (Int, PrimFn),
22 p_total :: Totality
23 }
25ty [] x = Constant x
26ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
28believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))
29 (Bind (UN "b") (Pi (TType (UVar (-2))))
30 (Bind (UN "x") (Pi (V 1)) (V 1)))
32total = Total []
33partial = Partial NotCovering
35primitives =
36 -- operators
37 [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))
38 (2, LPlus) total,
39 Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))
40 (2, LMinus) total,
41 Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))
42 (2, LTimes) total,
43 Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin div)
44 (2, LDiv) partial,
45 Prim (UN "prim__modInt") (ty [IType, IType] IType) 2 (iBin mod)
46 (2, LMod) partial,
47 Prim (UN "prim__andInt") (ty [IType, IType] IType) 2 (iBin (.&.))
48 (2, LAnd) partial,
49 Prim (UN "prim__orInt") (ty [IType, IType] IType) 2 (iBin (.|.))
50 (2, LOr) partial,
51 Prim (UN "prim__xorInt") (ty [IType, IType] IType) 2 (iBin xor)
52 (2, LXOr) partial,
53 Prim (UN "prim__shLInt") (ty [IType, IType] IType) 2 (iBin shiftL)
54 (2, LSHL) partial,
55 Prim (UN "prim__shRInt") (ty [IType, IType] IType) 2 (iBin shiftR)
56 (2, LSHR) partial,
57 Prim (UN "prim__complInt") (ty [IType] IType) 1 (iUn complement)
58 (1, LCompl) partial,
59 Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))
60 (2, LEq) total,
61 Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))
62 (2, LLt) total,
63 Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))
64 (2, LLe) total,
65 Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))
66 (2, LGt) total,
67 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))
68 (2, LGe) total,
69 Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))
70 (2, LEq) total,
71 Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))
72 (2, LLt) total,
73 Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))
74 (2, LLe) total,
75 Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))
76 (2, LGt) total,
77 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))
78 (2, LGe) total,
80 Prim (UN "prim__ltB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (<))
81 (2, LB8Lt) total,
82 Prim (UN "prim__lteB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (<=))
83 (2, LB8Lte) total,
84 Prim (UN "prim__eqB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (==))
85 (2, LB8Eq) total,
86 Prim (UN "prim__gteB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (>))
87 (2, LB8Gte) total,
88 Prim (UN "prim__gtB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (>=))
89 (2, LB8Gt) total,
90 Prim (UN "prim__addB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (+))
91 (2, LB8Plus) total,
92 Prim (UN "prim__subB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (-))
93 (2, LB8Minus) total,
94 Prim (UN "prim__mulB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (*))
95 (2, LB8Times) total,
96 Prim (UN "prim__udivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin div)
97 (2, LB8UDiv) partial,
98 Prim (UN "prim__sdivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8div)
99 (2, LB8SDiv) partial,
100 Prim (UN "prim__uremB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin rem)
101 (2, LB8URem) partial,
102 Prim (UN "prim__sremB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8rem)
103 (2, LB8SRem) partial,
104 Prim (UN "prim__shlB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> shiftL x (fromIntegral y)))
105 (2, LB8Shl) total,
106 Prim (UN "prim__lshrB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> shiftR x (fromIntegral y)))
107 (2, LB8AShr) total,
108 Prim (UN "prim__ashrB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> fromIntegral $
109 shiftR (fromIntegral x :: Int8)
110 (fromIntegral y)))
111 (2, LB8LShr) total,
112 Prim (UN "prim__andB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (.&.))
113 (2, LB8And) total,
114 Prim (UN "prim__orB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (.|.))
115 (2, LB8Or) total,
116 Prim (UN "prim__xorB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin xor)
117 (2, LB8Xor) total,
118 Prim (UN "prim__complB8") (ty [B8Type] B8Type) 1 (b8Un complement)
119 (1, LB8Compl) total,
120 Prim (UN "prim__zextB8_16") (ty [B8Type] B16Type) 1 zext8_16
121 (1, LB8Z16) total,
122 Prim (UN "prim__zextB8_32") (ty [B8Type] B32Type) 1 zext8_32
123 (1, LB8Z32) total,
124 Prim (UN "prim__zextB8_64") (ty [B8Type] B64Type) 1 zext8_64
125 (1, LB8Z64) total,
126 Prim (UN "prim__sextB8_16") (ty [B8Type] B16Type) 1 sext8_16
127 (1, LB8Z16) total,
128 Prim (UN "prim__sextB8_32") (ty [B8Type] B32Type) 1 sext8_32
129 (1, LB8Z32) total,
130 Prim (UN "prim__sextB8_64") (ty [B8Type] B64Type) 1 sext8_64
131 (1, LB8Z64) total,
133 Prim (UN "prim__ltB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (<))
134 (2, LB16Lt) total,
135 Prim (UN "prim__lteB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (<=))
136 (2, LB16Lte) total,
137 Prim (UN "prim__eqB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (==))
138 (2, LB16Eq) total,
139 Prim (UN "prim__gteB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (>))
140 (2, LB16Gte) total,
141 Prim (UN "prim__gtB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (>=))
142 (2, LB16Gt) total,
143 Prim (UN "prim__addB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (+))
144 (2, LB16Plus) total,
145 Prim (UN "prim__subB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (-))
146 (2, LB16Minus) total,
147 Prim (UN "prim__mulB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (*))
148 (2, LB16Times) total,
149 Prim (UN "prim__udivB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin div)
150 (2, LB16UDiv) partial,
151 Prim (UN "prim__sdivB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin s16div)
152 (2, LB16SDiv) partial,
153 Prim (UN "prim__uremB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin rem)
154 (2, LB16URem) partial,
155 Prim (UN "prim__sremB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin s16rem)
156 (2, LB16SRem) partial,
157 Prim (UN "prim__shlB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> shiftL x (fromIntegral y)))
158 (2, LB16Shl) total,
159 Prim (UN "prim__lshrB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> shiftR x (fromIntegral y)))
160 (2, LB16AShr) total,
161 Prim (UN "prim__ashrB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> fromIntegral $
162 shiftR (fromIntegral x :: Int16)
163 (fromIntegral y)))
164 (2, LB16LShr) total,
165 Prim (UN "prim__andB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (.&.))
166 (2, LB16And) total,
167 Prim (UN "prim__orB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (.|.))
168 (2, LB16Or) total,
169 Prim (UN "prim__xorB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin xor)
170 (2, LB16Xor) total,
171 Prim (UN "prim__complB16") (ty [B16Type] B16Type) 1 (b16Un complement)
172 (1, LB16Compl) total,
173 Prim (UN "prim__zextB16_32") (ty [B16Type] B32Type) 1 zext16_32
174 (1, LB16Z32) total,
175 Prim (UN "prim__zextB16_64") (ty [B16Type] B64Type) 1 zext16_64
176 (1, LB16Z64) total,
177 Prim (UN "prim__sextB16_32") (ty [B16Type] B32Type) 1 sext16_32
178 (1, LB16Z32) total,
179 Prim (UN "prim__sextB16_64") (ty [B16Type] B64Type) 1 sext16_64
180 (1, LB16Z64) total,
181 Prim (UN "prim__truncB16_8") (ty [B16Type] B8Type) 1 trunc16_8
182 (1, LB16T8) total,
184 Prim (UN "prim__ltB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (<))
185 (2, LB32Lt) total,
186 Prim (UN "prim__lteB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (<=))
187 (2, LB32Lte) total,
188 Prim (UN "prim__eqB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (==))
189 (2, LB32Eq) total,
190 Prim (UN "prim__gteB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (>))
191 (2, LB32Gte) total,
192 Prim (UN "prim__gtB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (>=))
193 (2, LB32Gt) total,
194 Prim (UN "prim__addB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (+))
195 (2, LB32Plus) total,
196 Prim (UN "prim__subB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (-))
197 (2, LB32Minus) total,
198 Prim (UN "prim__mulB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (*))
199 (2, LB32Times) total,
200 Prim (UN "prim__udivB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin div)
201 (2, LB32UDiv) partial,
202 Prim (UN "prim__sdivB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin s32div)
203 (2, LB32SDiv) partial,
204 Prim (UN "prim__uremB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin rem)
205 (2, LB32URem) partial,
206 Prim (UN "prim__sremB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin s32rem)
207 (2, LB32SRem) partial,
208 Prim (UN "prim__shlB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> shiftL x (fromIntegral y)))
209 (2, LB32Shl) total,
210 Prim (UN "prim__lshrB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> shiftR x (fromIntegral y)))
211 (2, LB32AShr) total,
212 Prim (UN "prim__ashrB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> fromIntegral $
213 shiftR (fromIntegral x :: Int32)
214 (fromIntegral y)))
215 (2, LB32LShr) total,
216 Prim (UN "prim__andB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (.&.))
217 (2, LB32And) total,
218 Prim (UN "prim__orB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (.|.))
219 (2, LB32Or) total,
220 Prim (UN "prim__xorB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin xor)
221 (2, LB32Xor) total,
222 Prim (UN "prim__complB32") (ty [B32Type] B32Type) 1 (b32Un complement)
223 (1, LB32Compl) total,
224 Prim (UN "prim__zextB32_64") (ty [B32Type] B64Type) 1 zext32_64
225 (1, LB32Z64) total,
226 Prim (UN "prim__sextB32_64") (ty [B32Type] B64Type) 1 sext32_64
227 (1, LB32Z64) total,
228 Prim (UN "prim__truncB32_8") (ty [B32Type] B8Type) 1 trunc32_8
229 (1, LB32T8) total,
230 Prim (UN "prim__truncB32_16") (ty [B32Type] B16Type) 1 trunc32_16
231 (1, LB32T16) total,
233 Prim (UN "prim__ltB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (<))
234 (2, LB64Lt) total,
235 Prim (UN "prim__lteB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (<=))
236 (2, LB64Lte) total,
237 Prim (UN "prim__eqB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (==))
238 (2, LB64Eq) total,
239 Prim (UN "prim__gteB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (>))
240 (2, LB64Gte) total,
241 Prim (UN "prim__gtB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (>=))
242 (2, LB64Gt) total,
243 Prim (UN "prim__addB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (+))
244 (2, LB64Plus) total,
245 Prim (UN "prim__subB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (-))
246 (2, LB64Minus) total,
247 Prim (UN "prim__mulB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (*))
248 (2, LB64Times) total,
249 Prim (UN "prim__udivB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin div)
250 (2, LB64UDiv) partial,
251 Prim (UN "prim__sdivB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin s64div)
252 (2, LB64SDiv) partial,
253 Prim (UN "prim__uremB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin rem)
254 (2, LB64URem) partial,
255 Prim (UN "prim__sremB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin s64rem)
256 (2, LB64SRem) partial,
257 Prim (UN "prim__shlB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> shiftL x (fromIntegral y)))
258 (2, LB64Shl) total,
259 Prim (UN "prim__lshrB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> shiftR x (fromIntegral y)))
260 (2, LB64AShr) total,
261 Prim (UN "prim__ashrB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> fromIntegral $
262 shiftR (fromIntegral x :: Int64)
263 (fromIntegral y)))
264 (2, LB64LShr) total,
265 Prim (UN "prim__andB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (.&.))
266 (2, LB64And) total,
267 Prim (UN "prim__orB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (.|.))
268 (2, LB64Or) total,
269 Prim (UN "prim__xorB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin xor)
270 (2, LB64Xor) total,
271 Prim (UN "prim__complB64") (ty [B64Type] B64Type) 1 (b64Un complement)
272 (1, LB64Compl) total,
273 Prim (UN "prim__truncB64_8") (ty [B64Type] B8Type) 1 trunc64_8
274 (1, LB64T8) total,
275 Prim (UN "prim__truncB64_16") (ty [B64Type] B16Type) 1 trunc64_16
276 (1, LB64T16) total,
277 Prim (UN "prim__truncB64_32") (ty [B64Type] B32Type) 1 trunc64_32
278 (1, LB64T32) total,
280 Prim (UN "prim__intToB8") (ty [IType] B8Type) 1 intToBits8
281 (1, LIntB8) total,
282 Prim (UN "prim__intToB16") (ty [IType] B16Type) 1 intToBits16
283 (1, LIntB16) total,
284 Prim (UN "prim__intToB32") (ty [IType] B32Type) 1 intToBits32
285 (1, LIntB32) total,
286 Prim (UN "prim__intToB64") (ty [IType] B64Type) 1 intToBits64
287 (1, LIntB64) total,
288 Prim (UN "prim__B32ToInt") (ty [B32Type] IType) 1 bits32ToInt
289 (1, LB32Int) total,
291 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))
292 (2, LBPlus) total,
293 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))
294 (2, LBMinus) total,
295 Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))
296 (2, LBTimes) total,
297 Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin div)
298 (2, LBDiv) partial,
299 Prim (UN "prim__modBigInt") (ty [BIType, BIType] BIType) 2 (bBin mod)
300 (2, LBMod) partial,
301 Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))
302 (2, LBEq) total,
303 Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))
304 (2, LBLt) total,
305 Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))
306 (2, LBLe) total,
307 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))
308 (2, LBGt) total,
309 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))
310 (2, LBGe) total,
311 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))
312 (2, LFPlus) total,
313 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))
314 (2, LFMinus) total,
315 Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))
316 (2, LFTimes) total,
317 Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))
318 (2, LFDiv) total,
319 Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))
320 (2, LFEq) total,
321 Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))
322 (2, LFLt) total,
323 Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))
324 (2, LFLe) total,
325 Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))
326 (2, LFGt) total,
327 Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))
328 (2, LFGe) total,
329 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
330 (2, LStrConcat) total,
331 Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))
332 (2, LStrEq) total,
333 Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))
334 (2, LStrLt) total,
335 Prim (UN "prim_lenString") (ty [StrType] IType) 1 (p_strLen)
336 (1, LStrLen) total,
337 -- Conversions
338 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)
339 (1, LStrInt) total,
340 Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)
341 (1, LIntStr) total,
342 Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)
343 (1, LChInt) total,
344 Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)
345 (1, LIntCh) total,
346 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)
347 (1, LIntBig) total,
348 Prim (UN "prim__bigIntToInt") (ty [BIType] IType) 1 (c_bigIntToInt)
349 (1, LBigInt) total,
350 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)
351 (1, LStrBig) total,
352 Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)
353 (1, LBigStr) total,
354 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)
355 (1, LStrFloat) total,
356 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)
357 (1, LFloatStr) total,
358 Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)
359 (1, LIntFloat) total,
360 Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)
361 (1, LFloatInt) total,
363 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)
364 (1, LFExp) total,
365 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)
366 (1, LFLog) total,
367 Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)
368 (1, LFSin) total,
369 Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos)
370 (1, LFCos) total,
371 Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan)
372 (1, LFTan) total,
373 Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin)
374 (1, LFASin) total,
375 Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos)
376 (1, LFACos) total,
377 Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan)
378 (1, LFATan) total,
379 Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt)
380 (1, LFSqrt) total,
381 Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor)
382 (1, LFFloor) total,
383 Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil)
384 (1, LFCeil) total,
386 Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)
387 (1, LStrHead) partial,
388 Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)
389 (1, LStrTail) partial,
390 Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)
391 (2, LStrCons) total,
392 Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)
393 (2, LStrIndex) partial,
394 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)
395 (1, LStrRev) total,
396 Prim (UN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)
397 (1, LReadStr) partial,
398 Prim (UN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)
399 (0, LVMPtr) total,
400 -- Streams
401 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)
402 (0, LStdIn) partial,
403 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)
404 (3, LNoOp) partial -- ahem
405 ]
407p_believeMe [_,_,x] = Just x
408p_believeMe _ = Nothing
410iUn op [VConstant (I x)] = Just $ VConstant (I (op x))
411iUn _ _ = Nothing
413iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
414iBin _ _ = Nothing
416bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))
417bBin _ _ = Nothing
419bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))
420bBini _ _ = Nothing
422biBin op = iBin (\x y -> if (op x y) then 1 else 0)
423bbBin op = bBini (\x y -> if (op x y) then 1 else 0)
425fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))
426fBin _ _ = Nothing
428bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in
429 Just $ VConstant (I i)
430bfBin _ _ = Nothing
432bcBin op [VConstant (Ch x), VConstant (Ch y)] = let i = (if op x y then 1 else 0) in
433 Just $ VConstant (I i)
434bcBin _ _ = Nothing
436bsBin op [VConstant (Str x), VConstant (Str y)]
437 = let i = (if op x y then 1 else 0) in
438 Just $ VConstant (I i)
439bsBin _ _ = Nothing
441sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
442sBin _ _ = Nothing
444s8div :: Word8 -> Word8 -> Word8
445s8div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int8)
447s16div :: Word16 -> Word16 -> Word16
448s16div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int16)
450s32div :: Word32 -> Word32 -> Word32
451s32div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int32)
453s64div :: Word64 -> Word64 -> Word64
454s64div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int64)
456s8rem :: Word8 -> Word8 -> Word8
457s8rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8)
459s16rem :: Word16 -> Word16 -> Word16
460s16rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16)
462s32rem :: Word32 -> Word32 -> Word32
463s32rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32)
465s64rem :: Word64 -> Word64 -> Word64
466s64rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64)
468b8Bin op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (B8 (op x y))
469b8Bin _ _ = Nothing
471b8Un op [VConstant (B8 x)] = Just $ VConstant (B8 (op x))
472b8Un _ _ = Nothing
474b16Bin op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (B16 (op x y))
475b16Bin _ _ = Nothing
477b16Un op [VConstant (B16 x)] = Just $ VConstant (B16 (op x))
478b16Un _ _ = Nothing
480b32Bin op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (B32 (op x y))
481b32Bin _ _ = Nothing
483b32Un op [VConstant (B32 x)] = Just $ VConstant (B32 (op x))
484b32Un _ _ = Nothing
486b64Bin op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (B64 (op x y))
487b64Bin _ _ = Nothing
489b64Un op [VConstant (B64 x)] = Just $ VConstant (B64 (op x))
490b64Un _ _ = Nothing
492b8Cmp op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
493b8Cmp _ _ = Nothing
495b16Cmp op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
496b16Cmp _ _ = Nothing
498b32Cmp op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
499b32Cmp _ _ = Nothing
501b64Cmp op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
502b64Cmp _ _ = Nothing
504toB8 x = VConstant (B8 (fromIntegral x))
505toB16 x = VConstant (B16 (fromIntegral x))
506toB32 x = VConstant (B32 (fromIntegral x))
507toB64 x = VConstant (B64 (fromIntegral x))
509zext8_16 [VConstant (B8 x)] = Just $ toB16 x
510zext8_16 _ = Nothing
512zext8_32 [VConstant (B8 x)] = Just $ toB32 x
513zext8_32 _ = Nothing
515zext8_64 [VConstant (B8 x)] = Just $ toB64 x
516zext8_64 _ = Nothing
518sext8_16 [VConstant (B8 x)] = Just $ toB16 (fromIntegral x :: Int8)
519sext8_16 _ = Nothing
521sext8_32 [VConstant (B8 x)] = Just $ toB32 (fromIntegral x :: Int8)
522sext8_32 _ = Nothing
524sext8_64 [VConstant (B8 x)] = Just $ toB64 (fromIntegral x :: Int8)
525sext8_64 _ = Nothing
527zext16_32 [VConstant (B16 x)] = Just $ toB32 x
528zext16_32 _ = Nothing
530zext16_64 [VConstant (B16 x)] = Just $ toB64 x
531zext16_64 _ = Nothing
533sext16_32 [VConstant (B16 x)] = Just $ toB32 (fromIntegral x :: Int16)
534sext16_32 _ = Nothing
536sext16_64 [VConstant (B16 x)] = Just $ toB64 (fromIntegral x :: Int16)
537sext16_64 _ = Nothing
539trunc16_8 [VConstant (B16 x)] = Just $ toB8 x
540trunc16_8 _ = Nothing
542zext32_64 [VConstant (B32 x)] = Just $ toB64 x
543zext32_64 _ = Nothing
545sext32_64 [VConstant (B32 x)] = Just $ toB64 (fromIntegral x :: Int32)
546sext32_64 _ = Nothing
548trunc32_8 [VConstant (B32 x)] = Just $ toB8 x
549trunc32_8 _ = Nothing
551trunc32_16 [VConstant (B32 x)] = Just $ toB16 x
552trunc32_16 _ = Nothing
554trunc64_8 [VConstant (B64 x)] = Just $ toB8 x
555trunc64_8 _ = Nothing
557trunc64_16 [VConstant (B64 x)] = Just $ toB16 x
558trunc64_16 _ = Nothing
560trunc64_32 [VConstant (B64 x)] = Just $ toB32 x
561trunc64_32 _ = Nothing
563intToBits8 [VConstant (I x)] = Just $ toB8 x
564intToBits8 _ = Nothing
565intToBits16 [VConstant (I x)] = Just $ toB16 x
566intToBits16 _ = Nothing
567intToBits32 [VConstant (I x)] = Just $ toB32 x
568intToBits32 _ = Nothing
569intToBits64 [VConstant (I x)] = Just $ toB64 x
570intToBits64 _ = Nothing
572bits32ToInt [VConstant (B32 x)] = Just $ VConstant (I (fromIntegral x))
573bits32ToInt _ = Nothing
575c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))
576c_intToStr _ = Nothing
577c_strToInt [VConstant (Str x)] = case reads x of
578 [(n,"")] -> Just $ VConstant (I n)
579 _ -> Just $ VConstant (I 0)
580c_strToInt _ = Nothing
582c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))
583c_intToChar _ = Nothing
584c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))
585c_charToInt _ = Nothing
587c_intToBigInt [VConstant (I x)] = Just $ VConstant (BI (fromIntegral x))
588c_intToBigInt _ = Nothing
589c_bigIntToInt [VConstant (BI x)] = Just $ VConstant (I (fromInteger x))
590c_bigIntToInt _ = Nothing
592c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x))
593c_bigIntToStr _ = Nothing
594c_strToBigInt [VConstant (Str x)] = case reads x of
595 [(n,"")] -> Just $ VConstant (BI n)
596 _ -> Just $ VConstant (BI 0)
597c_strToBigInt _ = Nothing
599c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
600c_floatToStr _ = Nothing
601c_strToFloat [VConstant (Str x)] = case reads x of
602 [(n,"")] -> Just $ VConstant (Fl n)
603 _ -> Just $ VConstant (Fl 0)
604c_strToFloat _ = Nothing
606c_floatToInt [VConstant (Fl x)] = Just $ VConstant (I (truncate x))
607c_floatToInt _ = Nothing
609c_intToFloat [VConstant (I x)] = Just $ VConstant (Fl (fromIntegral x))
610c_intToFloat _ = Nothing
612p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))
613p_fPrim f _ = Nothing
615p_floatExp = p_fPrim exp
616p_floatLog = p_fPrim log
617p_floatSin = p_fPrim sin
618p_floatCos = p_fPrim cos
619p_floatTan = p_fPrim tan
620p_floatASin = p_fPrim asin
621p_floatACos = p_fPrim acos
622p_floatATan = p_fPrim atan
623p_floatSqrt = p_fPrim sqrt
624p_floatFloor = p_fPrim (fromInteger . floor)
625p_floatCeil = p_fPrim (fromInteger . ceiling)
627p_strLen [VConstant (Str xs)] = Just $ VConstant (I (length xs))
628p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)
629p_strHead _ = Nothing
630p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)
631p_strTail _ = Nothing
632p_strIndex [VConstant (Str xs), VConstant (I i)]
633 | i < length xs = Just $ VConstant (Ch (xs!!i))
634p_strIndex _ = Nothing
635p_strCons [VConstant (Ch x), VConstant (Str xs)] = Just $ VConstant (Str (x:xs))
636p_strCons _ = Nothing
637p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))
638p_strRev _ = Nothing
640p_cantreduce _ = Nothing
642elabPrim :: Prim -> Idris ()
643elabPrim (Prim n ty i def sc tot)
644 = do updateContext (addOperator n ty i def)
645 setTotality n tot
646 i <- getIState
647 putIState i { idris_scprims = (n, sc) : idris_scprims i }
649elabPrims :: Idris ()
650elabPrims = do mapM_ (elabDecl EAll toplevel)
651 (map (PData "" defaultSyntax (FC "builtin" 0) False)
652 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
653 mapM_ elabPrim primitives