git.iko.soy/Idris-dev
on 45c8eca help sign in
Idris-dev/src/Idris/Primitives.hs
750 lines 35 kB history raw
1{-# LANGUAGE RankNTypes, ScopedTypeVariables, PatternGuards #-}
3module Idris.Primitives(primitives, Prim(..)) where
5import Idris.AbsSyntax
7import IRTS.Lang
9import Idris.Core.TT
10import Idris.Core.Evaluate
11import Data.Bits
12import Data.Word
13import Data.Int
14import Data.Char
15import Data.Function (on)
16import Data.Vector.Unboxed (Vector)
17import qualified Data.Vector.Unboxed as V
19data Prim = Prim { p_name :: Name,
20 p_type :: Type,
21 p_arity :: Int,
22 p_def :: [Const] -> Maybe Const,
23 p_lexp :: (Int, PrimFn),
24 p_total :: Totality
25 }
27ty :: [Const] -> Const -> Type
28ty [] x = Constant x
29ty (t:ts) x = Bind (sMN 0 "T") (Pi (Constant t)) (ty ts x)
31total, partial, iopartial :: Totality
32total = Total []
33partial = Partial NotCovering
34iopartial = Partial ExternalIO
36primitives :: [Prim]
37primitives =
38 -- operators
39 [iCoerce (ITFixed IT8) (ITFixed IT16) "zext" zext LZExt,
40 iCoerce (ITFixed IT8) (ITFixed IT32) "zext" zext LZExt,
41 iCoerce (ITFixed IT8) (ITFixed IT64) "zext" zext LZExt,
42 iCoerce (ITFixed IT8) ITBig "zext" zext LZExt,
43 iCoerce (ITFixed IT8) ITNative "zext" zext LZExt,
44 iCoerce (ITFixed IT16) (ITFixed IT32) "zext" zext LZExt,
45 iCoerce (ITFixed IT16) (ITFixed IT64) "zext" zext LZExt,
46 iCoerce (ITFixed IT16) ITBig "zext" zext LZExt,
47 iCoerce (ITFixed IT16) ITNative "zext" zext LZExt,
48 iCoerce (ITFixed IT32) (ITFixed IT64) "zext" zext LZExt,
49 iCoerce (ITFixed IT32) ITBig "zext" zext LZExt,
50 iCoerce (ITFixed IT32) ITNative "zext" zext LZExt,
51 iCoerce (ITFixed IT64) ITBig "zext" zext LZExt,
52 iCoerce ITNative ITBig "zext" zext LZExt,
53 iCoerce ITNative (ITFixed IT64) "zext" zext LZExt,
54 iCoerce ITNative (ITFixed IT32) "zext" zext LZExt,
55 iCoerce ITNative (ITFixed IT16) "zext" zext LZExt,
56 iCoerce ITChar ITBig "zext" zext LZExt,
58 iCoerce (ITFixed IT8) (ITFixed IT16) "sext" sext LSExt,
59 iCoerce (ITFixed IT8) (ITFixed IT32) "sext" sext LSExt,
60 iCoerce (ITFixed IT8) (ITFixed IT64) "sext" sext LSExt,
61 iCoerce (ITFixed IT8) ITBig "sext" sext LSExt,
62 iCoerce (ITFixed IT8) ITNative "sext" sext LSExt,
63 iCoerce (ITFixed IT16) (ITFixed IT32) "sext" sext LSExt,
64 iCoerce (ITFixed IT16) (ITFixed IT64) "sext" sext LSExt,
65 iCoerce (ITFixed IT16) ITBig "sext" sext LSExt,
66 iCoerce (ITFixed IT16) ITNative "sext" sext LSExt,
67 iCoerce (ITFixed IT32) (ITFixed IT64) "sext" sext LSExt,
68 iCoerce (ITFixed IT32) ITBig "sext" sext LSExt,
69 iCoerce (ITFixed IT32) ITNative "sext" sext LSExt,
70 iCoerce (ITFixed IT64) ITBig "sext" sext LSExt,
71 iCoerce ITNative ITBig "sext" sext LSExt,
72 iCoerce ITNative ITBig "sext" sext LSExt,
73 iCoerce ITNative (ITFixed IT64) "sext" sext LSExt,
74 iCoerce ITNative (ITFixed IT32) "sext" sext LSExt,
75 iCoerce ITNative (ITFixed IT16) "sext" sext LSExt,
76 iCoerce ITChar ITBig "sext" sext LSExt,
78 iCoerce (ITFixed IT16) (ITFixed IT8) "trunc" trunc LTrunc,
79 iCoerce (ITFixed IT32) (ITFixed IT8) "trunc" trunc LTrunc,
80 iCoerce (ITFixed IT64) (ITFixed IT8) "trunc" trunc LTrunc,
81 iCoerce ITBig (ITFixed IT8) "trunc" trunc LTrunc,
82 iCoerce ITNative (ITFixed IT8) "trunc" trunc LTrunc,
83 iCoerce (ITFixed IT32) (ITFixed IT16) "trunc" trunc LTrunc,
84 iCoerce (ITFixed IT64) (ITFixed IT16) "trunc" trunc LTrunc,
85 iCoerce ITBig (ITFixed IT16) "trunc" trunc LTrunc,
86 iCoerce ITNative (ITFixed IT16) "trunc" trunc LTrunc,
87 iCoerce (ITFixed IT64) (ITFixed IT32) "trunc" trunc LTrunc,
88 iCoerce ITBig (ITFixed IT32) "trunc" trunc LTrunc,
89 iCoerce ITNative (ITFixed IT32) "trunc" trunc LTrunc,
90 iCoerce ITBig (ITFixed IT64) "trunc" trunc LTrunc,
91 iCoerce (ITFixed IT16) ITNative "trunc" trunc LTrunc,
92 iCoerce (ITFixed IT32) ITNative "trunc" trunc LTrunc,
93 iCoerce (ITFixed IT64) ITNative "trunc" trunc LTrunc,
94 iCoerce ITBig ITNative "trunc" trunc LTrunc,
95 iCoerce ITNative (ITFixed IT64) "trunc" trunc LTrunc,
96 iCoerce ITBig ITChar "trunc" trunc LTrunc,
98 Prim (sUN "prim__addFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (+))
99 (2, LPlus ATFloat) total,
100 Prim (sUN "prim__subFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (-))
101 (2, LMinus ATFloat) total,
102 Prim (sUN "prim__mulFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (*))
103 (2, LTimes ATFloat) total,
104 Prim (sUN "prim__divFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (/))
105 (2, LSDiv ATFloat) total,
106 Prim (sUN "prim__eqFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (==))
107 (2, LEq ATFloat) total,
108 Prim (sUN "prim__sltFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (<))
109 (2, LSLt ATFloat) total,
110 Prim (sUN "prim__slteFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (<=))
111 (2, LSLe ATFloat) total,
112 Prim (sUN "prim__sgtFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (>))
113 (2, LSGt ATFloat) total,
114 Prim (sUN "prim__sgteFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (>=))
115 (2, LSGe ATFloat) total,
116 Prim (sUN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
117 (2, LStrConcat) total,
118 Prim (sUN "prim__eqString") (ty [StrType, StrType] (AType (ATInt ITNative))) 2 (bsBin (==))
119 (2, LStrEq) total,
120 Prim (sUN "prim__ltString") (ty [StrType, StrType] (AType (ATInt ITNative))) 2 (bsBin (<))
121 (2, LStrLt) total,
122 Prim (sUN "prim_lenString") (ty [StrType] (AType (ATInt ITNative))) 1 (p_strLen)
123 (1, LStrLen) total,
124 -- Conversions
125 Prim (sUN "prim__charToInt") (ty [(AType (ATInt ITChar))] (AType (ATInt ITNative))) 1 (c_charToInt)
126 (1, LChInt ITNative) total,
127 Prim (sUN "prim__intToChar") (ty [(AType (ATInt ITNative))] (AType (ATInt ITChar))) 1 (c_intToChar)
128 (1, LIntCh ITNative) total,
129 Prim (sUN "prim__strToFloat") (ty [StrType] (AType ATFloat)) 1 (c_strToFloat)
130 (1, LStrFloat) total,
131 Prim (sUN "prim__floatToStr") (ty [(AType ATFloat)] StrType) 1 (c_floatToStr)
132 (1, LFloatStr) total,
134 Prim (sUN "prim__floatExp") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatExp)
135 (1, LFExp) total,
136 Prim (sUN "prim__floatLog") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatLog)
137 (1, LFLog) total,
138 Prim (sUN "prim__floatSin") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatSin)
139 (1, LFSin) total,
140 Prim (sUN "prim__floatCos") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatCos)
141 (1, LFCos) total,
142 Prim (sUN "prim__floatTan") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatTan)
143 (1, LFTan) total,
144 Prim (sUN "prim__floatASin") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatASin)
145 (1, LFASin) total,
146 Prim (sUN "prim__floatACos") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatACos)
147 (1, LFACos) total,
148 Prim (sUN "prim__floatATan") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatATan)
149 (1, LFATan) total,
150 Prim (sUN "prim__floatSqrt") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatSqrt)
151 (1, LFSqrt) total,
152 Prim (sUN "prim__floatFloor") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatFloor)
153 (1, LFFloor) total,
154 Prim (sUN "prim__floatCeil") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatCeil)
155 (1, LFCeil) total,
157 Prim (sUN "prim__strHead") (ty [StrType] (AType (ATInt ITChar))) 1 (p_strHead)
158 (1, LStrHead) partial,
159 Prim (sUN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)
160 (1, LStrTail) partial,
161 Prim (sUN "prim__strCons") (ty [(AType (ATInt ITChar)), StrType] StrType) 2 (p_strCons)
162 (2, LStrCons) total,
163 Prim (sUN "prim__strIndex") (ty [StrType, (AType (ATInt ITNative))] (AType (ATInt ITChar))) 2 (p_strIndex)
164 (2, LStrIndex) partial,
165 Prim (sUN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)
166 (1, LStrRev) total,
167 Prim (sUN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)
168 (1, LReadStr) iopartial,
169 Prim (sUN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)
170 (0, LVMPtr) total,
171 -- Streams
172 Prim (sUN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)
173 (0, LStdIn) iopartial,
174 Prim (sUN "prim__stdout") (ty [] PtrType) 0 (p_cantreduce)
175 (0, LStdOut) iopartial,
176 Prim (sUN "prim__stderr") (ty [] PtrType) 0 (p_cantreduce)
177 (0, LStdErr) iopartial,
178 Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)
179 (0, LNullPtr) total,
180 -- Managed pointer registration
181 Prim (sUN "prim__registerPtr") (ty [PtrType, AType (ATInt ITNative)] ManagedPtrType) 2 (p_cantreduce)
182 (2, LRegisterPtr) total,
183 -- Buffers
184 Prim (sUN "prim__allocate") (ty [AType (ATInt (ITFixed IT64))] BufferType) 1 (p_allocate)
185 (1, LAllocate) total,
186 Prim (sUN "prim__appendBuffer") (ty [BufferType, AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), BufferType] BufferType) 6 (p_appendBuffer)
187 (6, LAppendBuffer) partial
188 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]
189 ++ concatMap vecOps vecTypes
190 ++ concatMap fixedOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64] -- ITNative, ITChar, ATFloat ] ++ vecTypes
191 ++ vecBitcasts vecTypes
193vecTypes :: [IntTy]
194vecTypes = [ITVec IT8 16, ITVec IT16 8, ITVec IT32 4, ITVec IT64 2]
196intOps :: IntTy -> [Prim]
197intOps ity = intCmps ity ++ intArith ity ++ intConv ity
199intSCmps :: IntTy -> [Prim]
200intSCmps ity =
201 [ iCmp ity "slt" False (bCmp ity (sCmpOp ity (<))) (LSLt . ATInt) total
202 , iCmp ity "slte" False (bCmp ity (sCmpOp ity (<=))) (LSLe . ATInt) total
203 , iCmp ity "eq" False (bCmp ity (==)) (LEq . ATInt) total
204 , iCmp ity "sgte" False (bCmp ity (sCmpOp ity (>=))) (LSGe . ATInt) total
205 , iCmp ity "sgt" False (bCmp ity (sCmpOp ity (>))) (LSGt . ATInt) total
206 ]
208intCmps :: IntTy -> [Prim]
209intCmps ITNative = intSCmps ITNative
210intCmps ity =
211 intSCmps ity ++
212 [ iCmp ity "lt" False (bCmp ity (cmpOp ity (<))) LLt total
213 , iCmp ity "lte" False (bCmp ity (cmpOp ity (<=))) LLe total
214 , iCmp ity "gte" False (bCmp ity (cmpOp ity (>=))) LGe total
215 , iCmp ity "gt" False (bCmp ity (cmpOp ity (>))) LGt total
216 ]
218intArith :: IntTy -> [Prim]
219intArith ity =
220 [ iBinOp ity "add" (bitBin ity (+)) (LPlus . ATInt) total
221 , iBinOp ity "sub" (bitBin ity (-)) (LMinus . ATInt) total
222 , iBinOp ity "mul" (bitBin ity (*)) (LTimes . ATInt) total
223 , iBinOp ity "udiv" (bitBin ity div) LUDiv partial
224 , iBinOp ity "sdiv" (bsdiv ity) (LSDiv . ATInt) partial
225 , iBinOp ity "urem" (bitBin ity rem) LURem partial
226 , iBinOp ity "srem" (bsrem ity) (LSRem . ATInt) partial
227 , iBinOp ity "shl" (bitBin ity (\x y -> shiftL x (fromIntegral y))) LSHL total
228 , iBinOp ity "lshr" (bitBin ity (\x y -> shiftR x (fromIntegral y))) LLSHR total
229 , iBinOp ity "ashr" (bashr ity) LASHR total
230 , iBinOp ity "and" (bitBin ity (.&.)) LAnd total
231 , iBinOp ity "or" (bitBin ity (.|.)) LOr total
232 , iBinOp ity "xor" (bitBin ity (xor)) LXOr total
233 , iUnOp ity "compl" (bUn ity complement) LCompl total
234 ]
236intConv :: IntTy -> [Prim]
237intConv ity =
238 [ Prim (sUN $ "prim__toStr" ++ intTyName ity) (ty [AType . ATInt $ ity] StrType) 1 intToStr
239 (1, LIntStr ity) total
240 , Prim (sUN $ "prim__fromStr" ++ intTyName ity) (ty [StrType] (AType . ATInt $ ity)) 1 (strToInt ity)
241 (1, LStrInt ity) total
242 , Prim (sUN $ "prim__toFloat" ++ intTyName ity) (ty [AType . ATInt $ ity] (AType ATFloat)) 1 intToFloat
243 (1, LIntFloat ity) total
244 , Prim (sUN $ "prim__fromFloat" ++ intTyName ity) (ty [AType ATFloat] (AType . ATInt $ ity)) 1 (floatToInt ity)
245 (1, LFloatInt ity) total
246 ]
248vecCmps :: IntTy -> [Prim]
249vecCmps ity =
250 [ iCmp ity "slt" True (bCmp ity (<)) (LSLt . ATInt) total
251 , iCmp ity "slte" True (bCmp ity (<=)) (LSLe . ATInt) total
252 , iCmp ity "eq" True (bCmp ity (==)) (LEq . ATInt) total
253 , iCmp ity "sgte" True (bCmp ity (>=)) (LSGe . ATInt) total
254 , iCmp ity "sgt" True (bCmp ity (>)) (LSGt . ATInt) total
255 , iCmp ity "lt" True (bCmp ity (<)) LLt total
256 , iCmp ity "lte" True (bCmp ity (<=)) LLe total
257 , iCmp ity "gte" True (bCmp ity (>=)) LGe total
258 , iCmp ity "gt" True (bCmp ity (>)) LGt total
259 ]
261vecOps :: IntTy -> [Prim]
262vecOps ity@(ITVec elem count) =
263 [ Prim (sUN $ "prim__mk" ++ intTyName ity)
264 (ty (replicate count . AType . ATInt . ITFixed $ elem) (AType . ATInt $ ity))
265 count (mkVecCon elem count) (count, LMkVec elem count) total
266 , Prim (sUN $ "prim__index" ++ intTyName ity)
267 (ty [AType . ATInt $ ity, AType (ATInt (ITFixed IT32))] (AType . ATInt . ITFixed $ elem))
268 2 (mkVecIndex count) (2, LIdxVec elem count) partial -- TODO: Ensure this reduces
269 , Prim (sUN $ "prim__update" ++ intTyName ity)
270 (ty [AType . ATInt $ ity, AType (ATInt (ITFixed IT32)), AType . ATInt . ITFixed $ elem]
271 (AType . ATInt $ ity))
272 3 (mkVecUpdate elem count) (3, LUpdateVec elem count) partial -- TODO: Ensure this reduces
273 ] ++ intArith ity ++ vecCmps ity
275bitcastPrim :: ArithTy -> ArithTy -> (ArithTy -> [Const] -> Maybe Const) -> PrimFn -> Prim
276bitcastPrim from to impl prim =
277 Prim (sUN $ "prim__bitcast" ++ aTyName from ++ "_" ++ aTyName to) (ty [AType from] (AType to)) 1 (impl to)
278 (1, prim) total
280vecBitcasts :: [IntTy] -> [Prim]
281vecBitcasts tys = [bitcastPrim from to bitcastVec (LBitCast from to)
282 | from <- map ATInt vecTypes, to <- map ATInt vecTypes, from /= to]
284fixedOps :: IntTy -> [Prim]
285fixedOps ity@(ITFixed _) =
286 map appendFun endiannesses ++
287 map peekFun endiannesses
288 where
289 endiannesses = [ Native, LE, BE ]
290 tyName = intTyName ity
291 b64 = AType (ATInt (ITFixed IT64))
292 thisTy = AType $ ATInt ity
293 appendFun en = Prim (sUN $ "prim__append" ++ tyName ++ show en)
294 (ty [BufferType, b64, b64, thisTy] BufferType)
295 4 (p_append en) (4, LAppend ity en) partial
296 peekFun en = Prim (sUN $ "prim__peek" ++ tyName ++ show en)
297 (ty [BufferType, b64] thisTy)
298 2 (p_peek ity en) (2, LPeek ity en) partial
300mapHalf :: (V.Unbox a, V.Unbox b) => ((a, a) -> b) -> Vector a -> Vector b
301mapHalf f xs = V.generate (V.length xs `div` 2) (\i -> f (xs V.! (i*2), xs V.! (i*2+1)))
303mapDouble :: (V.Unbox a, V.Unbox b) => (Bool -> a -> b) -> Vector a -> Vector b
304mapDouble f xs = V.generate (V.length xs * 2) (\i -> f (i `rem` 2 == 0) (xs V.! (i `div` 2)))
306concatWord8 :: (Word8, Word8) -> Word16
307concatWord8 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 8)
309concatWord16 :: (Word16, Word16) -> Word32
310concatWord16 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 16)
312concatWord32 :: (Word32, Word32) -> Word64
313concatWord32 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 32)
315truncWord16 :: Bool -> Word16 -> Word8
316truncWord16 True x = fromIntegral (x `shiftR` 8)
317truncWord16 False x = fromIntegral x
319truncWord32 :: Bool -> Word32 -> Word16
320truncWord32 True x = fromIntegral (x `shiftR` 16)
321truncWord32 False x = fromIntegral x
323truncWord64 :: Bool -> Word64 -> Word32
324truncWord64 True x = fromIntegral (x `shiftR` 32)
325truncWord64 False x = fromIntegral x
327bitcastVec :: ArithTy -> [Const] -> Maybe Const
328bitcastVec (ATInt (ITVec IT8 n)) [x@(B8V v)]
329 | V.length v == n = Just x
330bitcastVec (ATInt (ITVec IT16 n)) [B8V v]
331 | V.length v == n*2 = Just . B16V . mapHalf concatWord8 $ v
332bitcastVec (ATInt (ITVec IT32 n)) [B8V v]
333 | V.length v == n*4 = Just . B32V . mapHalf concatWord16 . mapHalf concatWord8 $ v
334bitcastVec (ATInt (ITVec IT64 n)) [B8V v]
335 | V.length v == n*8 = Just . B64V . mapHalf concatWord32 . mapHalf concatWord16 . mapHalf concatWord8 $ v
337bitcastVec (ATInt (ITVec IT8 n)) [B16V v]
338 | V.length v * 2 == n = Just . B8V . mapDouble truncWord16 $ v
339bitcastVec (ATInt (ITVec IT16 n)) [x@(B16V v)]
340 | V.length v == n = Just x
341bitcastVec (ATInt (ITVec IT32 n)) [B16V v]
342 | V.length v == n*2 = Just . B32V . mapHalf concatWord16 $ v
343bitcastVec (ATInt (ITVec IT64 n)) [B16V v]
344 | V.length v == n*4 = Just . B64V . mapHalf concatWord32 . mapHalf concatWord16 $ v
346bitcastVec (ATInt (ITVec IT8 n)) [B32V v]
347 | V.length v * 4 == n = Just . B8V . mapDouble truncWord16 . mapDouble truncWord32 $ v
348bitcastVec (ATInt (ITVec IT16 n)) [B32V v]
349 | V.length v * 2 == n = Just . B16V . mapDouble truncWord32 $ v
350bitcastVec (ATInt (ITVec IT32 n)) [x@(B32V v)]
351 | V.length v == n = Just x
352bitcastVec (ATInt (ITVec IT64 n)) [B32V v]
353 | V.length v == n*2 = Just . B64V . mapHalf concatWord32 $ v
355bitcastVec (ATInt (ITVec IT8 n)) [B64V v]
356 | V.length v * 8 == n = Just . B8V . mapDouble truncWord16 . mapDouble truncWord32 . mapDouble truncWord64 $ v
357bitcastVec (ATInt (ITVec IT16 n)) [B64V v]
358 | V.length v * 4 == n = Just . B16V . mapDouble truncWord32 . mapDouble truncWord64 $ v
359bitcastVec (ATInt (ITVec IT32 n)) [B64V v]
360 | V.length v == n*2 = Just . B32V . mapDouble truncWord64 $ v
361bitcastVec (ATInt (ITVec IT64 n)) [x@(B64V v)]
362 | V.length v == n = Just x
364bitcastVec _ _ = Nothing
366mkVecCon :: NativeTy -> Int -> [Const] -> Maybe Const
367mkVecCon ity count args
368 | length ints == count = Just (mkVec ity count ints)
369 | otherwise = Nothing
370 where
371 ints = getInt args
372 mkVec :: NativeTy -> Int -> [Integer] -> Const
373 mkVec IT8 len values = B8V $ V.generate len (fromInteger . (values !!))
374 mkVec IT16 len values = B16V $ V.generate len (fromInteger . (values !!))
375 mkVec IT32 len values = B32V $ V.generate len (fromInteger . (values !!))
376 mkVec IT64 len values = B64V $ V.generate len (fromInteger . (values !!))
378mkVecIndex count [vec, B32 i] = Just (idxVec vec)
379 where
380 idxVec :: Const -> Const
381 idxVec (B8V v) = B8 $ V.unsafeIndex v (fromIntegral i)
382 idxVec (B16V v) = B16 $ V.unsafeIndex v (fromIntegral i)
383 idxVec (B32V v) = B32 $ V.unsafeIndex v (fromIntegral i)
384 idxVec (B64V v) = B64 $ V.unsafeIndex v (fromIntegral i)
385mkVecIndex _ _ = Nothing
387mkVecUpdate ity count [vec, B32 i, newElem] = updateVec vec newElem
388 where
389 updateVec :: Const -> Const -> Maybe Const
390 updateVec (B8V v) (B8 e) = Just . B8V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))
391 updateVec (B16V v) (B16 e) = Just . B16V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))
392 updateVec (B32V v) (B32 e) = Just . B32V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))
393 updateVec (B64V v) (B64 e) = Just . B64V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))
394 updateVec _ _ = Nothing
395mkVecUpdate _ _ _ = Nothing
397aTyName :: ArithTy -> String
398aTyName (ATInt t) = intTyName t
399aTyName ATFloat = "Float"
401iCmp :: IntTy -> String -> Bool -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim
402iCmp ity op self impl irop totality
403 = Prim (sUN $ "prim__" ++ op ++ intTyName ity)
404 (ty (replicate 2 . AType . ATInt $ ity) (AType (ATInt (if self then ity else ITNative))))
405 2 impl (2, irop ity) totality
407iBinOp, iUnOp :: IntTy -> String -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim
408iBinOp ity op impl irop totality
409 = Prim (sUN $ "prim__" ++ op ++ intTyName ity)
410 (ty (replicate 2 . AType . ATInt $ ity) (AType . ATInt $ ity))
411 2 impl (2, irop ity) totality
412iUnOp ity op impl irop totality
413 = Prim (sUN $ "prim__" ++ op ++ intTyName ity)
414 (ty [AType . ATInt $ ity] (AType . ATInt $ ity))
415 1 impl (1, irop ity) totality
417iCoerce :: IntTy -> IntTy -> String -> (IntTy -> IntTy -> [Const] -> Maybe Const) -> (IntTy -> IntTy -> PrimFn) -> Prim
418iCoerce from to op impl irop =
419 Prim (sUN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)
420 (ty [AType . ATInt $ from] (AType . ATInt $ to)) 1 (impl from to) (1, irop from to) total
422fBin :: (Double -> Double -> Double) -> [Const] -> Maybe Const
423fBin op [Fl x, Fl y] = Just $ Fl (op x y)
424fBin _ _ = Nothing
426bfBin :: (Double -> Double -> Bool) -> [Const] -> Maybe Const
427bfBin op [Fl x, Fl y] = let i = (if op x y then 1 else 0) in
428 Just $ I i
429bfBin _ _ = Nothing
431bcBin :: (Char -> Char -> Bool) -> [Const] -> Maybe Const
432bcBin op [Ch x, Ch y] = let i = (if op x y then 1 else 0) in
433 Just $ I i
434bcBin _ _ = Nothing
436bsBin :: (String -> String -> Bool) -> [Const] -> Maybe Const
437bsBin op [Str x, Str y]
438 = let i = (if op x y then 1 else 0) in
439 Just $ I i
440bsBin _ _ = Nothing
442sBin :: (String -> String -> String) -> [Const] -> Maybe Const
443sBin op [Str x, Str y] = Just $ Str (op x y)
444sBin _ _ = Nothing
446bsrem :: IntTy -> [Const] -> Maybe Const
447bsrem ITBig [BI x, BI y] = Just . BI $ x `rem` y
448bsrem (ITFixed IT8) [B8 x, B8 y]
449 = Just $ B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8))
450bsrem (ITFixed IT16) [B16 x, B16 y]
451 = Just $ B16 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16))
452bsrem (ITFixed IT32) [B32 x, B32 y]
453 = Just $ B32 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32))
454bsrem (ITFixed IT64) [B64 x, B64 y]
455 = Just $ B64 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64))
456bsrem ITNative [I x, I y] = Just $ I (x `rem` y)
457bsrem ITChar [Ch x, Ch y] = Just $ Ch (chr $ (ord x) `rem` (ord y))
458bsrem (ITVec IT8 _) [B8V x, B8V y]
459 = Just . B8V $
460 V.zipWith (\n d -> (fromIntegral (fromIntegral n `rem` fromIntegral d :: Int8))) x y
461bsrem (ITVec IT16 _) [B16V x, B16V y]
462 = Just . B16V $
463 V.zipWith (\n d -> (fromIntegral (fromIntegral n `rem` fromIntegral d :: Int16))) x y
464bsrem (ITVec IT32 _) [B32V x, B32V y]
465 = Just . B32V $
466 V.zipWith (\n d -> (fromIntegral (fromIntegral n `rem` fromIntegral d :: Int64))) x y
467bsrem (ITVec IT64 _) [B64V x, B64V y]
468 = Just . B64V $
469 V.zipWith (\n d -> (fromIntegral (fromIntegral n `rem` fromIntegral d :: Int64))) x y
470bsrem _ _ = Nothing
472bsdiv :: IntTy -> [Const] -> Maybe Const
473bsdiv ITBig [BI x, BI y] = Just . BI $ x `div` y
474bsdiv (ITFixed IT8) [B8 x, B8 y]
475 = Just $ B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8))
476bsdiv (ITFixed IT16) [B16 x, B16 y]
477 = Just $ B16 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int16))
478bsdiv (ITFixed IT32) [B32 x, B32 y]
479 = Just $ B32 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int32))
480bsdiv (ITFixed IT64) [B64 x, B64 y]
481 = Just $ B64 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int64))
482bsdiv ITNative [I x, I y] = Just $ I (x `div` y)
483bsdiv ITChar [Ch x, Ch y] = Just $ Ch (chr $ (ord x) `div` (ord y))
484bsdiv (ITVec IT8 _) [B8V x, B8V y]
485 = Just . B8V $
486 V.zipWith (\n d -> (fromIntegral (fromIntegral n `div` fromIntegral d :: Int8))) x y
487bsdiv (ITVec IT16 _) [B16V x, B16V y]
488 = Just . B16V $
489 V.zipWith (\n d -> (fromIntegral (fromIntegral n `div` fromIntegral d :: Int16))) x y
490bsdiv (ITVec IT32 _) [B32V x, B32V y]
491 = Just . B32V $
492 V.zipWith (\n d -> (fromIntegral (fromIntegral n `div` fromIntegral d :: Int64))) x y
493bsdiv (ITVec IT64 _) [B64V x, B64V y]
494 = Just . B64V $
495 V.zipWith (\n d -> (fromIntegral (fromIntegral n `div` fromIntegral d :: Int64))) x y
496bsdiv _ _ = Nothing
498bashr :: IntTy -> [Const] -> Maybe Const
499bashr ITBig [BI x, BI y] = Just $ BI (x `shiftR` fromIntegral y)
500bashr (ITFixed IT8) [B8 x, B8 y]
501 = Just $ B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8))
502bashr (ITFixed IT16) [B16 x, B16 y]
503 = Just $ B16 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int16))
504bashr (ITFixed IT32) [B32 x, B32 y]
505 = Just $ B32 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int32))
506bashr (ITFixed IT64) [B64 x, B64 y]
507 = Just $ B64 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int64))
508bashr ITNative [I x, I y] = Just $ I (x `shiftR` y)
509bashr ITChar [Ch x, Ch y] = Just $ Ch (chr $ (ord x) `shiftR` (ord y))
510bashr (ITVec IT8 _) [B8V x, B8V y]
511 = Just . B8V $
512 V.zipWith (\n d -> (fromIntegral (fromIntegral n `shiftR` fromIntegral d :: Int8))) x y
513bashr (ITVec IT16 _) [B16V x, B16V y]
514 = Just . B16V $
515 V.zipWith (\n d -> (fromIntegral (fromIntegral n `shiftR` fromIntegral d :: Int16))) x y
516bashr (ITVec IT32 _) [B32V x, B32V y]
517 = Just . B32V $
518 V.zipWith (\n d -> (fromIntegral (fromIntegral n `shiftR` fromIntegral d :: Int64))) x y
519bashr (ITVec IT64 _) [B64V x, B64V y]
520 = Just . B64V $
521 V.zipWith (\n d -> (fromIntegral (fromIntegral n `shiftR` fromIntegral d :: Int64))) x y
522bashr _ _ = Nothing
524bUn :: IntTy -> (forall a. Bits a => a -> a) -> [Const] -> Maybe Const
525bUn (ITFixed IT8) op [B8 x] = Just $ B8 (op x)
526bUn (ITFixed IT16) op [B16 x] = Just $ B16 (op x)
527bUn (ITFixed IT32) op [B32 x] = Just $ B32 (op x)
528bUn (ITFixed IT64) op [B64 x] = Just $ B64 (op x)
529bUn ITBig op [BI x] = Just $ BI (op x)
530bUn ITNative op [I x] = Just $ I (op x)
531bUn ITChar op [Ch x] = Just $ Ch (chr $ op (ord x))
532bUn (ITVec IT8 _) op [B8V x] = Just . B8V $ V.map op x
533bUn (ITVec IT16 _) op [B16V x] = Just . B16V $ V.map op x
534bUn (ITVec IT32 _) op [B32V x] = Just . B32V $ V.map op x
535bUn (ITVec IT64 _) op [B64V x] = Just . B64V $ V.map op x
536bUn _ _ _ = Nothing
538bitBin :: IntTy -> (forall a. (Bits a, Integral a) => a -> a -> a) -> [Const] -> Maybe Const
539bitBin (ITFixed IT8) op [B8 x, B8 y] = Just $ B8 (op x y)
540bitBin (ITFixed IT16) op [B16 x, B16 y] = Just $ B16 (op x y)
541bitBin (ITFixed IT32) op [B32 x, B32 y] = Just $ B32 (op x y)
542bitBin (ITFixed IT64) op [B64 x, B64 y] = Just $ B64 (op x y)
543bitBin ITBig op [BI x, BI y] = Just $ BI (op x y)
544bitBin ITNative op [I x, I y] = Just $ I (op x y)
545bitBin ITChar op [Ch x, Ch y] = Just $ Ch (chr $ op (ord x) (ord y))
546bitBin (ITVec IT8 _) op [B8V x, B8V y] = Just . B8V $ V.zipWith op x y
547bitBin (ITVec IT16 _) op [B16V x, B16V y] = Just . B16V $ V.zipWith op x y
548bitBin (ITVec IT32 _) op [B32V x, B32V y] = Just . B32V $ V.zipWith op x y
549bitBin (ITVec IT64 _) op [B64V x, B64V y] = Just . B64V $ V.zipWith op x y
550bitBin _ _ _ = Nothing
552bCmp :: IntTy -> (forall a. (Integral a, Ord a) => a -> a -> Bool) -> [Const] -> Maybe Const
553bCmp (ITFixed IT8) op [B8 x, B8 y] = Just $ I (if (op x y) then 1 else 0)
554bCmp (ITFixed IT16) op [B16 x, B16 y] = Just $ I (if (op x y) then 1 else 0)
555bCmp (ITFixed IT32) op [B32 x, B32 y] = Just $ I (if (op x y) then 1 else 0)
556bCmp (ITFixed IT64) op [B64 x, B64 y] = Just $ I (if (op x y) then 1 else 0)
557bCmp ITBig op [BI x, BI y] = Just $ I (if (op x y) then 1 else 0)
558bCmp ITNative op [I x, I y] = Just $ I (if (op x y) then 1 else 0)
559bCmp ITChar op [Ch x, Ch y] = Just $ I (if (op (ord x) (ord y)) then 1 else 0)
560bCmp (ITVec IT8 _) op [B8V x, B8V y]
561 = Just . B8V . V.map (\b -> if b then -1 else 0) $ V.zipWith op x y
562bCmp (ITVec IT16 _) op [B16V x, B16V y]
563 = Just . B16V . V.map (\b -> if b then -1 else 0) $ V.zipWith op x y
564bCmp (ITVec IT32 _) op [B32V x, B32V y]
565 = Just . B32V . V.map (\b -> if b then -1 else 0) $ V.zipWith op x y
566bCmp (ITVec IT64 _) op [B64V x, B64V y]
567 = Just . B64V . V.map (\b -> if b then -1 else 0) $ V.zipWith op x y
568bCmp _ _ _ = Nothing
571cmpOp :: (Ord a, Integral a) => IntTy -> (forall b. Ord b => b -> b -> Bool) -> a -> a -> Bool
572cmpOp (ITFixed _) f = f
573cmpOp (ITNative) f = f `on` (fromIntegral :: Integral a => a -> Word)
574cmpOp (ITChar) f = f `on` ((fromIntegral :: Integral a => a -> Word))
575cmpOp _ f = let xor = (/=) in (\ x y -> (f x y) `xor` (x < 0) `xor` (y < 0))
577sCmpOp :: (Ord a, Integral a) => IntTy -> (forall b. Ord b => b -> b -> Bool) -> a -> a -> Bool
578sCmpOp (ITFixed IT8) f = f `on` (fromIntegral :: Integral a => a -> Int8)
579sCmpOp (ITFixed IT16) f = f `on` (fromIntegral :: Integral a => a -> Int16)
580sCmpOp (ITFixed IT32) f = f `on` (fromIntegral :: Integral a => a -> Int32)
581sCmpOp (ITFixed IT64) f = f `on` (fromIntegral :: Integral a => a -> Int64)
582sCmpOp _ f = f
584toInt :: Integral a => IntTy -> a -> Const
585toInt (ITFixed IT8) x = B8 (fromIntegral x)
586toInt (ITFixed IT16) x = B16 (fromIntegral x)
587toInt (ITFixed IT32) x = B32 (fromIntegral x)
588toInt (ITFixed IT64) x = B64 (fromIntegral x)
589toInt ITBig x = BI (fromIntegral x)
590toInt ITNative x = I (fromIntegral x)
591toInt ITChar x = Ch (chr $ fromIntegral x)
593intToInt :: IntTy -> IntTy -> [Const] -> Maybe Const
594intToInt (ITFixed IT8) out [B8 x] = Just $ toInt out x
595intToInt (ITFixed IT16) out [B16 x] = Just $ toInt out x
596intToInt (ITFixed IT32) out [B32 x] = Just $ toInt out x
597intToInt (ITFixed IT64) out [B64 x] = Just $ toInt out x
598intToInt ITBig out [BI x] = Just $ toInt out x
599intToInt ITNative out [I x] = Just $ toInt out x
600intToInt ITChar out [Ch x] = Just $ toInt out (ord x)
601intToInt _ _ _ = Nothing
603zext :: IntTy -> IntTy -> [Const] -> Maybe Const
604zext from ITBig val = intToInt from ITBig val
605zext ITBig _ _ = Nothing
606zext f@(ITFixed from) t@(ITFixed to) val
607 | nativeTyWidth from < nativeTyWidth to = intToInt f t val
608zext ITNative to [I x] = Just $ toInt to (fromIntegral x :: Word)
609zext from ITNative val = intToInt from ITNative val
610zext _ _ _ = Nothing
612sext :: IntTy -> IntTy -> [Const] -> Maybe Const
613sext (ITFixed IT8) out [B8 x] = Just $ toInt out (fromIntegral x :: Int8)
614sext (ITFixed IT16) out [B16 x] = Just $ toInt out (fromIntegral x :: Int16)
615sext (ITFixed IT32) out [B32 x] = Just $ toInt out (fromIntegral x :: Int32)
616sext (ITFixed IT64) out [B64 x] = Just $ toInt out (fromIntegral x :: Int64)
617sext ITBig _ _ = Nothing
618sext from to val = intToInt from to val
620trunc :: IntTy -> IntTy -> [Const] -> Maybe Const
621trunc ITBig to val = intToInt ITBig to val
622trunc _ ITBig _ = Nothing
623trunc f@(ITFixed from) t@(ITFixed to) val | nativeTyWidth from > nativeTyWidth to = intToInt f t val
624trunc ITNative to [I x] = Just $ toInt to x
625trunc from ITNative val = intToInt from ITNative val
626trunc _ _ _ = Nothing
628intToStr :: [Const] -> Maybe Const
629intToStr val | [i] <- getInt val = Just $ Str (show i)
630intToStr _ = Nothing
632getInt :: [Const] -> [Integer]
633getInt (B8 x : xs) = toInteger x : getInt xs
634getInt (B16 x : xs) = toInteger x : getInt xs
635getInt (B32 x : xs) = toInteger x : getInt xs
636getInt (B64 x : xs) = toInteger x : getInt xs
637getInt (I x : xs) = toInteger x : getInt xs
638getInt (BI x : xs) = x : getInt xs
639getInt _ = []
641strToInt :: IntTy -> [Const] -> Maybe Const
642strToInt ity [Str x] = case reads x of
643 [(n,"")] -> Just $ toInt ity (n :: Integer)
644 _ -> Just $ I 0
645strToInt _ _ = Nothing
647intToFloat :: [Const] -> Maybe Const
648intToFloat val | [i] <- getInt val = Just $ Fl (fromIntegral i)
649intToFloat _ = Nothing
651floatToInt :: IntTy -> [Const] -> Maybe Const
652floatToInt ity [Fl x] = Just $ toInt ity (truncate x :: Integer)
653floatToInt _ _ = Nothing
655c_intToChar, c_charToInt :: [Const] -> Maybe Const
656c_intToChar [(I x)] = Just . Ch . toEnum $ x
657c_intToChar _ = Nothing
658c_charToInt [(Ch x)] = Just . I . fromEnum $ x
659c_charToInt _ = Nothing
661c_floatToStr :: [Const] -> Maybe Const
662c_floatToStr [Fl x] = Just $ Str (show x)
663c_floatToStr _ = Nothing
664c_strToFloat [Str x] = case reads x of
665 [(n,"")] -> Just $ Fl n
666 _ -> Just $ Fl 0
667c_strToFloat _ = Nothing
669p_fPrim :: (Double -> Double) -> [Const] -> Maybe Const
670p_fPrim f [Fl x] = Just $ Fl (f x)
671p_fPrim f _ = Nothing
673p_floatExp, p_floatLog, p_floatSin, p_floatCos, p_floatTan, p_floatASin, p_floatACos, p_floatATan, p_floatSqrt, p_floatFloor, p_floatCeil :: [Const] -> Maybe Const
674p_floatExp = p_fPrim exp
675p_floatLog = p_fPrim log
676p_floatSin = p_fPrim sin
677p_floatCos = p_fPrim cos
678p_floatTan = p_fPrim tan
679p_floatASin = p_fPrim asin
680p_floatACos = p_fPrim acos
681p_floatATan = p_fPrim atan
682p_floatSqrt = p_fPrim sqrt
683p_floatFloor = p_fPrim (fromInteger . floor)
684p_floatCeil = p_fPrim (fromInteger . ceiling)
686p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev :: [Const] -> Maybe Const
687p_strLen [Str xs] = Just $ I (length xs)
688p_strLen _ = Nothing
689p_strHead [Str (x:xs)] = Just $ Ch x
690p_strHead _ = Nothing
691p_strTail [Str (x:xs)] = Just $ Str xs
692p_strTail _ = Nothing
693p_strIndex [Str xs, I i]
694 | i < length xs = Just $ Ch (xs!!i)
695p_strIndex _ = Nothing
696p_strCons [Ch x, Str xs] = Just $ Str (x:xs)
697p_strCons _ = Nothing
698p_strRev [Str xs] = Just $ Str (reverse xs)
699p_strRev _ = Nothing
701p_allocate, p_appendBuffer :: [Const] -> Maybe Const
702p_allocate [B64 _] = Just $ B8V V.empty
703p_allocate n = Nothing
704p_appendBuffer [B8V vect1, B64 size1, B64 count, B64 size2, B64 off, B8V vect2] =
705 Just $ B8V (foldl (V.++)
706 (V.slice 0 (fromIntegral size1) vect1)
707 (replicate (fromIntegral count) (V.slice (fromIntegral off) (fromIntegral size2) vect2)))
708p_appendBuffer n = Nothing
709p_append :: Endianness -> [Const] -> Maybe Const
710p_append en [B8V vect, B64 size, B64 count, val] =
711 let bytes = case val of
712 B8 x -> [x]
713 B16 x -> [fromIntegral x, fromIntegral (shiftR x 8)]
714 B32 x -> map (fromIntegral . shiftR x) [0,8..24]
715 B64 x -> map (fromIntegral . shiftR x) [0,8..56]
716 in Just $ B8V (foldl V.snoc
717 (V.slice 0 (fromIntegral size) vect)
718 (concat (replicate (fromIntegral count)
719 (case en of
720 BE -> reverse bytes
721 _ -> bytes))))
722p_append _ _ = Nothing
724p_peek :: IntTy -> Endianness -> [Const] -> Maybe Const
725p_peek (ITFixed IT8) _ [B8V vect, B64 offset] = Just $ B8 (vect V.! fromIntegral offset)
726p_peek (ITFixed IT16) en [B8V vect, B64 offset] =
727 let bytes = [0..1]
728 in Just $ B16 (foldl (\full byte -> shiftL full 8 .|. fromIntegral (vect V.! (fromIntegral offset+byte)))
729 0
730 (case en of
731 BE -> bytes
732 _ -> reverse bytes))
733p_peek (ITFixed IT32) en [B8V vect, B64 offset] =
734 let bytes = [0..1]
735 in Just $ B32 (foldl (\full byte -> shiftL full 8 .|. fromIntegral (vect V.! (fromIntegral offset+byte)))
736 0
737 (case en of
738 BE -> bytes
739 _ -> reverse bytes))
740p_peek (ITFixed IT64) en [B8V vect, B64 offset] =
741 let bytes = [0..1]
742 in Just $ B64 (foldl (\full byte -> shiftL full 8 .|. fromIntegral (vect V.! (fromIntegral offset+byte)))
743 0
744 (case en of
745 BE -> bytes
746 _ -> reverse bytes))
747p_peek _ _ _ = Nothing
749p_cantreduce :: a -> Maybe b
750p_cantreduce _ = Nothing