git.iko.soy/Idris-dev
on d16d418 help sign in
Idris-dev/src/Idris/Primitives.hs
702 lines 33 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 :: Totality
32total = Total []
33partial = Partial NotCovering
35primitives :: [Prim]
36primitives =
37 -- operators
38 [iCoerce (ITFixed IT8) (ITFixed IT16) "zext" zext LZExt,
39 iCoerce (ITFixed IT8) (ITFixed IT32) "zext" zext LZExt,
40 iCoerce (ITFixed IT8) (ITFixed IT64) "zext" zext LZExt,
41 iCoerce (ITFixed IT8) ITBig "zext" zext LZExt,
42 iCoerce (ITFixed IT8) ITNative "zext" zext LZExt,
43 iCoerce (ITFixed IT16) (ITFixed IT32) "zext" zext LZExt,
44 iCoerce (ITFixed IT16) (ITFixed IT64) "zext" zext LZExt,
45 iCoerce (ITFixed IT16) ITBig "zext" zext LZExt,
46 iCoerce (ITFixed IT16) ITNative "zext" zext LZExt,
47 iCoerce (ITFixed IT32) (ITFixed IT64) "zext" zext LZExt,
48 iCoerce (ITFixed IT32) ITBig "zext" zext LZExt,
49 iCoerce (ITFixed IT32) ITNative "zext" zext LZExt,
50 iCoerce (ITFixed IT64) ITBig "zext" zext LZExt,
51 iCoerce ITNative ITBig "zext" zext LZExt,
52 iCoerce ITNative (ITFixed IT64) "zext" zext LZExt,
53 iCoerce ITNative (ITFixed IT32) "zext" zext LZExt,
54 iCoerce ITNative (ITFixed IT16) "zext" zext LZExt,
55 iCoerce ITChar ITBig "zext" zext LZExt,
57 iCoerce (ITFixed IT8) (ITFixed IT16) "sext" sext LSExt,
58 iCoerce (ITFixed IT8) (ITFixed IT32) "sext" sext LSExt,
59 iCoerce (ITFixed IT8) (ITFixed IT64) "sext" sext LSExt,
60 iCoerce (ITFixed IT8) ITBig "sext" sext LSExt,
61 iCoerce (ITFixed IT8) ITNative "sext" sext LSExt,
62 iCoerce (ITFixed IT16) (ITFixed IT32) "sext" sext LSExt,
63 iCoerce (ITFixed IT16) (ITFixed IT64) "sext" sext LSExt,
64 iCoerce (ITFixed IT16) ITBig "sext" sext LSExt,
65 iCoerce (ITFixed IT16) ITNative "sext" sext LSExt,
66 iCoerce (ITFixed IT32) (ITFixed IT64) "sext" sext LSExt,
67 iCoerce (ITFixed IT32) ITBig "sext" sext LSExt,
68 iCoerce (ITFixed IT32) ITNative "sext" sext LSExt,
69 iCoerce (ITFixed IT64) ITBig "sext" sext LSExt,
70 iCoerce ITNative ITBig "sext" sext LSExt,
71 iCoerce ITNative ITBig "sext" sext LSExt,
72 iCoerce ITNative (ITFixed IT64) "sext" sext LSExt,
73 iCoerce ITNative (ITFixed IT32) "sext" sext LSExt,
74 iCoerce ITNative (ITFixed IT16) "sext" sext LSExt,
75 iCoerce ITChar ITBig "sext" sext LSExt,
77 iCoerce (ITFixed IT16) (ITFixed IT8) "trunc" trunc LTrunc,
78 iCoerce (ITFixed IT32) (ITFixed IT8) "trunc" trunc LTrunc,
79 iCoerce (ITFixed IT64) (ITFixed IT8) "trunc" trunc LTrunc,
80 iCoerce ITBig (ITFixed IT8) "trunc" trunc LTrunc,
81 iCoerce ITNative (ITFixed IT8) "trunc" trunc LTrunc,
82 iCoerce (ITFixed IT32) (ITFixed IT16) "trunc" trunc LTrunc,
83 iCoerce (ITFixed IT64) (ITFixed IT16) "trunc" trunc LTrunc,
84 iCoerce ITBig (ITFixed IT16) "trunc" trunc LTrunc,
85 iCoerce ITNative (ITFixed IT16) "trunc" trunc LTrunc,
86 iCoerce (ITFixed IT64) (ITFixed IT32) "trunc" trunc LTrunc,
87 iCoerce ITBig (ITFixed IT32) "trunc" trunc LTrunc,
88 iCoerce ITNative (ITFixed IT32) "trunc" trunc LTrunc,
89 iCoerce ITBig (ITFixed IT64) "trunc" trunc LTrunc,
90 iCoerce (ITFixed IT16) ITNative "trunc" trunc LTrunc,
91 iCoerce (ITFixed IT32) ITNative "trunc" trunc LTrunc,
92 iCoerce (ITFixed IT64) ITNative "trunc" trunc LTrunc,
93 iCoerce ITBig ITNative "trunc" trunc LTrunc,
94 iCoerce ITNative (ITFixed IT64) "trunc" trunc LTrunc,
95 iCoerce ITBig ITChar "trunc" trunc LTrunc,
97 Prim (sUN "prim__addFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (+))
98 (2, LPlus ATFloat) total,
99 Prim (sUN "prim__subFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (-))
100 (2, LMinus ATFloat) total,
101 Prim (sUN "prim__mulFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (*))
102 (2, LTimes ATFloat) total,
103 Prim (sUN "prim__divFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (/))
104 (2, LSDiv ATFloat) total,
105 Prim (sUN "prim__eqFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (==))
106 (2, LEq ATFloat) total,
107 Prim (sUN "prim__sltFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (<))
108 (2, LSLt ATFloat) total,
109 Prim (sUN "prim__slteFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (<=))
110 (2, LSLe ATFloat) total,
111 Prim (sUN "prim__sgtFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (>))
112 (2, LSGt ATFloat) total,
113 Prim (sUN "prim__sgteFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (>=))
114 (2, LSGe ATFloat) total,
115 Prim (sUN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
116 (2, LStrConcat) total,
117 Prim (sUN "prim__eqString") (ty [StrType, StrType] (AType (ATInt ITNative))) 2 (bsBin (==))
118 (2, LStrEq) total,
119 Prim (sUN "prim__ltString") (ty [StrType, StrType] (AType (ATInt ITNative))) 2 (bsBin (<))
120 (2, LStrLt) total,
121 Prim (sUN "prim_lenString") (ty [StrType] (AType (ATInt ITNative))) 1 (p_strLen)
122 (1, LStrLen) total,
123 -- Conversions
124 Prim (sUN "prim__charToInt") (ty [(AType (ATInt ITChar))] (AType (ATInt ITNative))) 1 (c_charToInt)
125 (1, LChInt ITNative) total,
126 Prim (sUN "prim__intToChar") (ty [(AType (ATInt ITNative))] (AType (ATInt ITChar))) 1 (c_intToChar)
127 (1, LIntCh ITNative) total,
128 Prim (sUN "prim__strToFloat") (ty [StrType] (AType ATFloat)) 1 (c_strToFloat)
129 (1, LStrFloat) total,
130 Prim (sUN "prim__floatToStr") (ty [(AType ATFloat)] StrType) 1 (c_floatToStr)
131 (1, LFloatStr) total,
133 Prim (sUN "prim__floatExp") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatExp)
134 (1, LFExp) total,
135 Prim (sUN "prim__floatLog") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatLog)
136 (1, LFLog) total,
137 Prim (sUN "prim__floatSin") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatSin)
138 (1, LFSin) total,
139 Prim (sUN "prim__floatCos") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatCos)
140 (1, LFCos) total,
141 Prim (sUN "prim__floatTan") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatTan)
142 (1, LFTan) total,
143 Prim (sUN "prim__floatASin") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatASin)
144 (1, LFASin) total,
145 Prim (sUN "prim__floatACos") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatACos)
146 (1, LFACos) total,
147 Prim (sUN "prim__floatATan") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatATan)
148 (1, LFATan) total,
149 Prim (sUN "prim__floatSqrt") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatSqrt)
150 (1, LFSqrt) total,
151 Prim (sUN "prim__floatFloor") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatFloor)
152 (1, LFFloor) total,
153 Prim (sUN "prim__floatCeil") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatCeil)
154 (1, LFCeil) total,
156 Prim (sUN "prim__strHead") (ty [StrType] (AType (ATInt ITChar))) 1 (p_strHead)
157 (1, LStrHead) partial,
158 Prim (sUN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)
159 (1, LStrTail) partial,
160 Prim (sUN "prim__strCons") (ty [(AType (ATInt ITChar)), StrType] StrType) 2 (p_strCons)
161 (2, LStrCons) total,
162 Prim (sUN "prim__strIndex") (ty [StrType, (AType (ATInt ITNative))] (AType (ATInt ITChar))) 2 (p_strIndex)
163 (2, LStrIndex) partial,
164 Prim (sUN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)
165 (1, LStrRev) total,
166 Prim (sUN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)
167 (1, LReadStr) partial,
168 Prim (sUN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)
169 (0, LVMPtr) total,
170 -- Streams
171 Prim (sUN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)
172 (0, LStdIn) partial,
173 Prim (sUN "prim__stdout") (ty [] PtrType) 0 (p_cantreduce)
174 (0, LStdOut) partial,
175 Prim (sUN "prim__stderr") (ty [] PtrType) 0 (p_cantreduce)
176 (0, LStdErr) partial,
177 Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)
178 (0, LNullPtr) total,
179 -- Managed pointer registration
180 Prim (sUN "prim__registerPtr") (ty [PtrType, AType (ATInt ITNative)] ManagedPtrType) 2 (p_cantreduce)
181 (2, LRegisterPtr) total,
182 -- Buffers
183 Prim (sUN "prim__allocate") (ty [AType (ATInt (ITFixed IT64))] BufferType) 1 (p_cantreduce)
184 (1, LAllocate) total,
185 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_cantreduce)
186 (6, LAppendBuffer) partial
187 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]
188 ++ concatMap vecOps vecTypes
189 ++ concatMap fixedOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64] -- ITNative, ITChar, ATFloat ] ++ vecTypes
190 ++ vecBitcasts vecTypes
192vecTypes :: [IntTy]
193vecTypes = [ITVec IT8 16, ITVec IT16 8, ITVec IT32 4, ITVec IT64 2]
195intOps :: IntTy -> [Prim]
196intOps ity = intCmps ity ++ intArith ity ++ intConv ity
198intSCmps :: IntTy -> [Prim]
199intSCmps ity =
200 [ iCmp ity "slt" False (bCmp ity (sCmpOp ity (<))) (LSLt . ATInt) total
201 , iCmp ity "slte" False (bCmp ity (sCmpOp ity (<=))) (LSLe . ATInt) total
202 , iCmp ity "eq" False (bCmp ity (==)) (LEq . ATInt) total
203 , iCmp ity "sgte" False (bCmp ity (sCmpOp ity (>=))) (LSGe . ATInt) total
204 , iCmp ity "sgt" False (bCmp ity (sCmpOp ity (>))) (LSGt . ATInt) total
205 ]
207intCmps :: IntTy -> [Prim]
208intCmps ITNative = intSCmps ITNative
209intCmps ity =
210 intSCmps ity ++
211 [ iCmp ity "lt" False (bCmp ity (cmpOp ity (<))) LLt total
212 , iCmp ity "lte" False (bCmp ity (cmpOp ity (<=))) LLe total
213 , iCmp ity "gte" False (bCmp ity (cmpOp ity (>=))) LGe total
214 , iCmp ity "gt" False (bCmp ity (cmpOp ity (>))) LGt total
215 ]
217intArith :: IntTy -> [Prim]
218intArith ity =
219 [ iBinOp ity "add" (bitBin ity (+)) (LPlus . ATInt) total
220 , iBinOp ity "sub" (bitBin ity (-)) (LMinus . ATInt) total
221 , iBinOp ity "mul" (bitBin ity (*)) (LTimes . ATInt) total
222 , iBinOp ity "udiv" (bitBin ity div) LUDiv partial
223 , iBinOp ity "sdiv" (bsdiv ity) (LSDiv . ATInt) partial
224 , iBinOp ity "urem" (bitBin ity rem) LURem partial
225 , iBinOp ity "srem" (bsrem ity) (LSRem . ATInt) partial
226 , iBinOp ity "shl" (bitBin ity (\x y -> shiftL x (fromIntegral y))) LSHL total
227 , iBinOp ity "lshr" (bitBin ity (\x y -> shiftR x (fromIntegral y))) LLSHR total
228 , iBinOp ity "ashr" (bashr ity) LASHR total
229 , iBinOp ity "and" (bitBin ity (.&.)) LAnd total
230 , iBinOp ity "or" (bitBin ity (.|.)) LOr total
231 , iBinOp ity "xor" (bitBin ity (xor)) LXOr total
232 , iUnOp ity "compl" (bUn ity complement) LCompl total
233 ]
235intConv :: IntTy -> [Prim]
236intConv ity =
237 [ Prim (sUN $ "prim__toStr" ++ intTyName ity) (ty [AType . ATInt $ ity] StrType) 1 intToStr
238 (1, LIntStr ity) total
239 , Prim (sUN $ "prim__fromStr" ++ intTyName ity) (ty [StrType] (AType . ATInt $ ity)) 1 (strToInt ity)
240 (1, LStrInt ity) total
241 , Prim (sUN $ "prim__toFloat" ++ intTyName ity) (ty [AType . ATInt $ ity] (AType ATFloat)) 1 intToFloat
242 (1, LIntFloat ity) total
243 , Prim (sUN $ "prim__fromFloat" ++ intTyName ity) (ty [AType ATFloat] (AType . ATInt $ ity)) 1 (floatToInt ity)
244 (1, LFloatInt ity) total
245 ]
247vecCmps :: IntTy -> [Prim]
248vecCmps ity =
249 [ iCmp ity "slt" True (bCmp ity (<)) (LSLt . ATInt) total
250 , iCmp ity "slte" True (bCmp ity (<=)) (LSLe . ATInt) total
251 , iCmp ity "eq" True (bCmp ity (==)) (LEq . ATInt) total
252 , iCmp ity "sgte" True (bCmp ity (>=)) (LSGe . ATInt) total
253 , iCmp ity "sgt" True (bCmp ity (>)) (LSGt . ATInt) total
254 , iCmp ity "lt" True (bCmp ity (<)) LLt total
255 , iCmp ity "lte" True (bCmp ity (<=)) LLe total
256 , iCmp ity "gte" True (bCmp ity (>=)) LGe total
257 , iCmp ity "gt" True (bCmp ity (>)) LGt total
258 ]
260vecOps :: IntTy -> [Prim]
261vecOps ity@(ITVec elem count) =
262 [ Prim (sUN $ "prim__mk" ++ intTyName ity)
263 (ty (replicate count . AType . ATInt . ITFixed $ elem) (AType . ATInt $ ity))
264 count (mkVecCon elem count) (count, LMkVec elem count) total
265 , Prim (sUN $ "prim__index" ++ intTyName ity)
266 (ty [AType . ATInt $ ity, AType (ATInt (ITFixed IT32))] (AType . ATInt . ITFixed $ elem))
267 2 (mkVecIndex count) (2, LIdxVec elem count) partial -- TODO: Ensure this reduces
268 , Prim (sUN $ "prim__update" ++ intTyName ity)
269 (ty [AType . ATInt $ ity, AType (ATInt (ITFixed IT32)), AType . ATInt . ITFixed $ elem]
270 (AType . ATInt $ ity))
271 3 (mkVecUpdate elem count) (3, LUpdateVec elem count) partial -- TODO: Ensure this reduces
272 ] ++ intArith ity ++ vecCmps ity
274bitcastPrim :: ArithTy -> ArithTy -> (ArithTy -> [Const] -> Maybe Const) -> PrimFn -> Prim
275bitcastPrim from to impl prim =
276 Prim (sUN $ "prim__bitcast" ++ aTyName from ++ "_" ++ aTyName to) (ty [AType from] (AType to)) 1 (impl to)
277 (1, prim) total
279vecBitcasts :: [IntTy] -> [Prim]
280vecBitcasts tys = [bitcastPrim from to bitcastVec (LBitCast from to)
281 | from <- map ATInt vecTypes, to <- map ATInt vecTypes, from /= to]
283fixedOps :: IntTy -> [Prim]
284fixedOps ity@(ITFixed _) =
285 map appendFun endiannesses ++
286 map peekFun endiannesses
287 where
288 endiannesses = [ Native, LE, BE ]
289 tyName = intTyName ity
290 b64 = AType (ATInt (ITFixed IT64))
291 thisTy = AType $ ATInt ity
292 appendFun en = Prim (sUN $ "prim__append" ++ tyName ++ show en)
293 (ty [BufferType, b64, b64, thisTy] BufferType)
294 4 (p_cantreduce) (4, LAppend ity en) partial
295 peekFun en = Prim (sUN $ "prim__peek" ++ tyName ++ show en)
296 (ty [BufferType, b64] thisTy)
297 2 (p_cantreduce) (2, LPeek ity en) partial
299mapHalf :: (V.Unbox a, V.Unbox b) => ((a, a) -> b) -> Vector a -> Vector b
300mapHalf f xs = V.generate (V.length xs `div` 2) (\i -> f (xs V.! (i*2), xs V.! (i*2+1)))
302mapDouble :: (V.Unbox a, V.Unbox b) => (Bool -> a -> b) -> Vector a -> Vector b
303mapDouble f xs = V.generate (V.length xs * 2) (\i -> f (i `rem` 2 == 0) (xs V.! (i `div` 2)))
305concatWord8 :: (Word8, Word8) -> Word16
306concatWord8 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 8)
308concatWord16 :: (Word16, Word16) -> Word32
309concatWord16 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 16)
311concatWord32 :: (Word32, Word32) -> Word64
312concatWord32 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 32)
314truncWord16 :: Bool -> Word16 -> Word8
315truncWord16 True x = fromIntegral (x `shiftR` 8)
316truncWord16 False x = fromIntegral x
318truncWord32 :: Bool -> Word32 -> Word16
319truncWord32 True x = fromIntegral (x `shiftR` 16)
320truncWord32 False x = fromIntegral x
322truncWord64 :: Bool -> Word64 -> Word32
323truncWord64 True x = fromIntegral (x `shiftR` 32)
324truncWord64 False x = fromIntegral x
326bitcastVec :: ArithTy -> [Const] -> Maybe Const
327bitcastVec (ATInt (ITVec IT8 n)) [x@(B8V v)]
328 | V.length v == n = Just x
329bitcastVec (ATInt (ITVec IT16 n)) [B8V v]
330 | V.length v == n*2 = Just . B16V . mapHalf concatWord8 $ v
331bitcastVec (ATInt (ITVec IT32 n)) [B8V v]
332 | V.length v == n*4 = Just . B32V . mapHalf concatWord16 . mapHalf concatWord8 $ v
333bitcastVec (ATInt (ITVec IT64 n)) [B8V v]
334 | V.length v == n*8 = Just . B64V . mapHalf concatWord32 . mapHalf concatWord16 . mapHalf concatWord8 $ v
336bitcastVec (ATInt (ITVec IT8 n)) [B16V v]
337 | V.length v * 2 == n = Just . B8V . mapDouble truncWord16 $ v
338bitcastVec (ATInt (ITVec IT16 n)) [x@(B16V v)]
339 | V.length v == n = Just x
340bitcastVec (ATInt (ITVec IT32 n)) [B16V v]
341 | V.length v == n*2 = Just . B32V . mapHalf concatWord16 $ v
342bitcastVec (ATInt (ITVec IT64 n)) [B16V v]
343 | V.length v == n*4 = Just . B64V . mapHalf concatWord32 . mapHalf concatWord16 $ v
345bitcastVec (ATInt (ITVec IT8 n)) [B32V v]
346 | V.length v * 4 == n = Just . B8V . mapDouble truncWord16 . mapDouble truncWord32 $ v
347bitcastVec (ATInt (ITVec IT16 n)) [B32V v]
348 | V.length v * 2 == n = Just . B16V . mapDouble truncWord32 $ v
349bitcastVec (ATInt (ITVec IT32 n)) [x@(B32V v)]
350 | V.length v == n = Just x
351bitcastVec (ATInt (ITVec IT64 n)) [B32V v]
352 | V.length v == n*2 = Just . B64V . mapHalf concatWord32 $ v
354bitcastVec (ATInt (ITVec IT8 n)) [B64V v]
355 | V.length v * 8 == n = Just . B8V . mapDouble truncWord16 . mapDouble truncWord32 . mapDouble truncWord64 $ v
356bitcastVec (ATInt (ITVec IT16 n)) [B64V v]
357 | V.length v * 4 == n = Just . B16V . mapDouble truncWord32 . mapDouble truncWord64 $ v
358bitcastVec (ATInt (ITVec IT32 n)) [B64V v]
359 | V.length v == n*2 = Just . B32V . mapDouble truncWord64 $ v
360bitcastVec (ATInt (ITVec IT64 n)) [x@(B64V v)]
361 | V.length v == n = Just x
363bitcastVec _ _ = Nothing
365mkVecCon :: NativeTy -> Int -> [Const] -> Maybe Const
366mkVecCon ity count args
367 | length ints == count = Just (mkVec ity count ints)
368 | otherwise = Nothing
369 where
370 ints = getInt args
371 mkVec :: NativeTy -> Int -> [Integer] -> Const
372 mkVec IT8 len values = B8V $ V.generate len (fromInteger . (values !!))
373 mkVec IT16 len values = B16V $ V.generate len (fromInteger . (values !!))
374 mkVec IT32 len values = B32V $ V.generate len (fromInteger . (values !!))
375 mkVec IT64 len values = B64V $ V.generate len (fromInteger . (values !!))
377mkVecIndex count [vec, B32 i] = Just (idxVec vec)
378 where
379 idxVec :: Const -> Const
380 idxVec (B8V v) = B8 $ V.unsafeIndex v (fromIntegral i)
381 idxVec (B16V v) = B16 $ V.unsafeIndex v (fromIntegral i)
382 idxVec (B32V v) = B32 $ V.unsafeIndex v (fromIntegral i)
383 idxVec (B64V v) = B64 $ V.unsafeIndex v (fromIntegral i)
384mkVecIndex _ _ = Nothing
386mkVecUpdate ity count [vec, B32 i, newElem] = updateVec vec newElem
387 where
388 updateVec :: Const -> Const -> Maybe Const
389 updateVec (B8V v) (B8 e) = Just . B8V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))
390 updateVec (B16V v) (B16 e) = Just . B16V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))
391 updateVec (B32V v) (B32 e) = Just . B32V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))
392 updateVec (B64V v) (B64 e) = Just . B64V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))
393 updateVec _ _ = Nothing
394mkVecUpdate _ _ _ = Nothing
396aTyName :: ArithTy -> String
397aTyName (ATInt t) = intTyName t
398aTyName ATFloat = "Float"
400iCmp :: IntTy -> String -> Bool -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim
401iCmp ity op self impl irop totality
402 = Prim (sUN $ "prim__" ++ op ++ intTyName ity)
403 (ty (replicate 2 . AType . ATInt $ ity) (AType (ATInt (if self then ity else ITNative))))
404 2 impl (2, irop ity) totality
406iBinOp, iUnOp :: IntTy -> String -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim
407iBinOp ity op impl irop totality
408 = Prim (sUN $ "prim__" ++ op ++ intTyName ity)
409 (ty (replicate 2 . AType . ATInt $ ity) (AType . ATInt $ ity))
410 2 impl (2, irop ity) totality
411iUnOp ity op impl irop totality
412 = Prim (sUN $ "prim__" ++ op ++ intTyName ity)
413 (ty [AType . ATInt $ ity] (AType . ATInt $ ity))
414 1 impl (1, irop ity) totality
416iCoerce :: IntTy -> IntTy -> String -> (IntTy -> IntTy -> [Const] -> Maybe Const) -> (IntTy -> IntTy -> PrimFn) -> Prim
417iCoerce from to op impl irop =
418 Prim (sUN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)
419 (ty [AType . ATInt $ from] (AType . ATInt $ to)) 1 (impl from to) (1, irop from to) total
421fBin :: (Double -> Double -> Double) -> [Const] -> Maybe Const
422fBin op [Fl x, Fl y] = Just $ Fl (op x y)
423fBin _ _ = Nothing
425bfBin :: (Double -> Double -> Bool) -> [Const] -> Maybe Const
426bfBin op [Fl x, Fl y] = let i = (if op x y then 1 else 0) in
427 Just $ I i
428bfBin _ _ = Nothing
430bcBin :: (Char -> Char -> Bool) -> [Const] -> Maybe Const
431bcBin op [Ch x, Ch y] = let i = (if op x y then 1 else 0) in
432 Just $ I i
433bcBin _ _ = Nothing
435bsBin :: (String -> String -> Bool) -> [Const] -> Maybe Const
436bsBin op [Str x, Str y]
437 = let i = (if op x y then 1 else 0) in
438 Just $ I i
439bsBin _ _ = Nothing
441sBin :: (String -> String -> String) -> [Const] -> Maybe Const
442sBin op [Str x, Str y] = Just $ Str (op x y)
443sBin _ _ = Nothing
445bsrem :: IntTy -> [Const] -> Maybe Const
446bsrem ITBig [BI x, BI y] = Just . BI $ x `rem` y
447bsrem (ITFixed IT8) [B8 x, B8 y]
448 = Just $ B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8))
449bsrem (ITFixed IT16) [B16 x, B16 y]
450 = Just $ B16 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16))
451bsrem (ITFixed IT32) [B32 x, B32 y]
452 = Just $ B32 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32))
453bsrem (ITFixed IT64) [B64 x, B64 y]
454 = Just $ B64 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64))
455bsrem ITNative [I x, I y] = Just $ I (x `rem` y)
456bsrem ITChar [Ch x, Ch y] = Just $ Ch (chr $ (ord x) `rem` (ord y))
457bsrem (ITVec IT8 _) [B8V x, B8V y]
458 = Just . B8V $
459 V.zipWith (\n d -> (fromIntegral (fromIntegral n `rem` fromIntegral d :: Int8))) x y
460bsrem (ITVec IT16 _) [B16V x, B16V y]
461 = Just . B16V $
462 V.zipWith (\n d -> (fromIntegral (fromIntegral n `rem` fromIntegral d :: Int16))) x y
463bsrem (ITVec IT32 _) [B32V x, B32V y]
464 = Just . B32V $
465 V.zipWith (\n d -> (fromIntegral (fromIntegral n `rem` fromIntegral d :: Int64))) x y
466bsrem (ITVec IT64 _) [B64V x, B64V y]
467 = Just . B64V $
468 V.zipWith (\n d -> (fromIntegral (fromIntegral n `rem` fromIntegral d :: Int64))) x y
469bsrem _ _ = Nothing
471bsdiv :: IntTy -> [Const] -> Maybe Const
472bsdiv ITBig [BI x, BI y] = Just . BI $ x `div` y
473bsdiv (ITFixed IT8) [B8 x, B8 y]
474 = Just $ B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8))
475bsdiv (ITFixed IT16) [B16 x, B16 y]
476 = Just $ B16 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int16))
477bsdiv (ITFixed IT32) [B32 x, B32 y]
478 = Just $ B32 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int32))
479bsdiv (ITFixed IT64) [B64 x, B64 y]
480 = Just $ B64 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int64))
481bsdiv ITNative [I x, I y] = Just $ I (x `div` y)
482bsdiv ITChar [Ch x, Ch y] = Just $ Ch (chr $ (ord x) `div` (ord y))
483bsdiv (ITVec IT8 _) [B8V x, B8V y]
484 = Just . B8V $
485 V.zipWith (\n d -> (fromIntegral (fromIntegral n `div` fromIntegral d :: Int8))) x y
486bsdiv (ITVec IT16 _) [B16V x, B16V y]
487 = Just . B16V $
488 V.zipWith (\n d -> (fromIntegral (fromIntegral n `div` fromIntegral d :: Int16))) x y
489bsdiv (ITVec IT32 _) [B32V x, B32V y]
490 = Just . B32V $
491 V.zipWith (\n d -> (fromIntegral (fromIntegral n `div` fromIntegral d :: Int64))) x y
492bsdiv (ITVec IT64 _) [B64V x, B64V y]
493 = Just . B64V $
494 V.zipWith (\n d -> (fromIntegral (fromIntegral n `div` fromIntegral d :: Int64))) x y
495bsdiv _ _ = Nothing
497bashr :: IntTy -> [Const] -> Maybe Const
498bashr ITBig [BI x, BI y] = Just $ BI (x `shiftR` fromIntegral y)
499bashr (ITFixed IT8) [B8 x, B8 y]
500 = Just $ B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8))
501bashr (ITFixed IT16) [B16 x, B16 y]
502 = Just $ B16 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int16))
503bashr (ITFixed IT32) [B32 x, B32 y]
504 = Just $ B32 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int32))
505bashr (ITFixed IT64) [B64 x, B64 y]
506 = Just $ B64 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int64))
507bashr ITNative [I x, I y] = Just $ I (x `shiftR` y)
508bashr ITChar [Ch x, Ch y] = Just $ Ch (chr $ (ord x) `shiftR` (ord y))
509bashr (ITVec IT8 _) [B8V x, B8V y]
510 = Just . B8V $
511 V.zipWith (\n d -> (fromIntegral (fromIntegral n `shiftR` fromIntegral d :: Int8))) x y
512bashr (ITVec IT16 _) [B16V x, B16V y]
513 = Just . B16V $
514 V.zipWith (\n d -> (fromIntegral (fromIntegral n `shiftR` fromIntegral d :: Int16))) x y
515bashr (ITVec IT32 _) [B32V x, B32V y]
516 = Just . B32V $
517 V.zipWith (\n d -> (fromIntegral (fromIntegral n `shiftR` fromIntegral d :: Int64))) x y
518bashr (ITVec IT64 _) [B64V x, B64V y]
519 = Just . B64V $
520 V.zipWith (\n d -> (fromIntegral (fromIntegral n `shiftR` fromIntegral d :: Int64))) x y
521bashr _ _ = Nothing
523bUn :: IntTy -> (forall a. Bits a => a -> a) -> [Const] -> Maybe Const
524bUn (ITFixed IT8) op [B8 x] = Just $ B8 (op x)
525bUn (ITFixed IT16) op [B16 x] = Just $ B16 (op x)
526bUn (ITFixed IT32) op [B32 x] = Just $ B32 (op x)
527bUn (ITFixed IT64) op [B64 x] = Just $ B64 (op x)
528bUn ITBig op [BI x] = Just $ BI (op x)
529bUn ITNative op [I x] = Just $ I (op x)
530bUn ITChar op [Ch x] = Just $ Ch (chr $ op (ord x))
531bUn (ITVec IT8 _) op [B8V x] = Just . B8V $ V.map op x
532bUn (ITVec IT16 _) op [B16V x] = Just . B16V $ V.map op x
533bUn (ITVec IT32 _) op [B32V x] = Just . B32V $ V.map op x
534bUn (ITVec IT64 _) op [B64V x] = Just . B64V $ V.map op x
535bUn _ _ _ = Nothing
537bitBin :: IntTy -> (forall a. (Bits a, Integral a) => a -> a -> a) -> [Const] -> Maybe Const
538bitBin (ITFixed IT8) op [B8 x, B8 y] = Just $ B8 (op x y)
539bitBin (ITFixed IT16) op [B16 x, B16 y] = Just $ B16 (op x y)
540bitBin (ITFixed IT32) op [B32 x, B32 y] = Just $ B32 (op x y)
541bitBin (ITFixed IT64) op [B64 x, B64 y] = Just $ B64 (op x y)
542bitBin ITBig op [BI x, BI y] = Just $ BI (op x y)
543bitBin ITNative op [I x, I y] = Just $ I (op x y)
544bitBin ITChar op [Ch x, Ch y] = Just $ Ch (chr $ op (ord x) (ord y))
545bitBin (ITVec IT8 _) op [B8V x, B8V y] = Just . B8V $ V.zipWith op x y
546bitBin (ITVec IT16 _) op [B16V x, B16V y] = Just . B16V $ V.zipWith op x y
547bitBin (ITVec IT32 _) op [B32V x, B32V y] = Just . B32V $ V.zipWith op x y
548bitBin (ITVec IT64 _) op [B64V x, B64V y] = Just . B64V $ V.zipWith op x y
549bitBin _ _ _ = Nothing
551bCmp :: IntTy -> (forall a. (Integral a, Ord a) => a -> a -> Bool) -> [Const] -> Maybe Const
552bCmp (ITFixed IT8) op [B8 x, B8 y] = Just $ I (if (op x y) then 1 else 0)
553bCmp (ITFixed IT16) op [B16 x, B16 y] = Just $ I (if (op x y) then 1 else 0)
554bCmp (ITFixed IT32) op [B32 x, B32 y] = Just $ I (if (op x y) then 1 else 0)
555bCmp (ITFixed IT64) op [B64 x, B64 y] = Just $ I (if (op x y) then 1 else 0)
556bCmp ITBig op [BI x, BI y] = Just $ I (if (op x y) then 1 else 0)
557bCmp ITNative op [I x, I y] = Just $ I (if (op x y) then 1 else 0)
558bCmp ITChar op [Ch x, Ch y] = Just $ I (if (op (ord x) (ord y)) then 1 else 0)
559bCmp (ITVec IT8 _) op [B8V x, B8V y]
560 = Just . B8V . V.map (\b -> if b then -1 else 0) $ V.zipWith op x y
561bCmp (ITVec IT16 _) op [B16V x, B16V y]
562 = Just . B16V . V.map (\b -> if b then -1 else 0) $ V.zipWith op x y
563bCmp (ITVec IT32 _) op [B32V x, B32V y]
564 = Just . B32V . V.map (\b -> if b then -1 else 0) $ V.zipWith op x y
565bCmp (ITVec IT64 _) op [B64V x, B64V y]
566 = Just . B64V . V.map (\b -> if b then -1 else 0) $ V.zipWith op x y
567bCmp _ _ _ = Nothing
570cmpOp :: (Ord a, Integral a) => IntTy -> (forall b. Ord b => b -> b -> Bool) -> a -> a -> Bool
571cmpOp (ITFixed _) f = f
572cmpOp (ITNative) f = f `on` (fromIntegral :: Integral a => a -> Word)
573cmpOp (ITChar) f = f `on` ((fromIntegral :: Integral a => a -> Word))
574cmpOp _ f = let xor = (/=) in (\ x y -> (f x y) `xor` (x < 0) `xor` (y < 0))
576sCmpOp :: (Ord a, Integral a) => IntTy -> (forall b. Ord b => b -> b -> Bool) -> a -> a -> Bool
577sCmpOp (ITFixed IT8) f = f `on` (fromIntegral :: Integral a => a -> Int8)
578sCmpOp (ITFixed IT16) f = f `on` (fromIntegral :: Integral a => a -> Int16)
579sCmpOp (ITFixed IT32) f = f `on` (fromIntegral :: Integral a => a -> Int32)
580sCmpOp (ITFixed IT64) f = f `on` (fromIntegral :: Integral a => a -> Int64)
581sCmpOp _ f = f
583toInt :: Integral a => IntTy -> a -> Const
584toInt (ITFixed IT8) x = B8 (fromIntegral x)
585toInt (ITFixed IT16) x = B16 (fromIntegral x)
586toInt (ITFixed IT32) x = B32 (fromIntegral x)
587toInt (ITFixed IT64) x = B64 (fromIntegral x)
588toInt ITBig x = BI (fromIntegral x)
589toInt ITNative x = I (fromIntegral x)
590toInt ITChar x = Ch (chr $ fromIntegral x)
592intToInt :: IntTy -> IntTy -> [Const] -> Maybe Const
593intToInt (ITFixed IT8) out [B8 x] = Just $ toInt out x
594intToInt (ITFixed IT16) out [B16 x] = Just $ toInt out x
595intToInt (ITFixed IT32) out [B32 x] = Just $ toInt out x
596intToInt (ITFixed IT64) out [B64 x] = Just $ toInt out x
597intToInt ITBig out [BI x] = Just $ toInt out x
598intToInt ITNative out [I x] = Just $ toInt out x
599intToInt ITChar out [Ch x] = Just $ toInt out (ord x)
600intToInt _ _ _ = Nothing
602zext :: IntTy -> IntTy -> [Const] -> Maybe Const
603zext from ITBig val = intToInt from ITBig val
604zext ITBig _ _ = Nothing
605zext f@(ITFixed from) t@(ITFixed to) val
606 | nativeTyWidth from < nativeTyWidth to = intToInt f t val
607zext ITNative to [I x] = Just $ toInt to (fromIntegral x :: Word)
608zext from ITNative val = intToInt from ITNative val
609zext _ _ _ = Nothing
611sext :: IntTy -> IntTy -> [Const] -> Maybe Const
612sext (ITFixed IT8) out [B8 x] = Just $ toInt out (fromIntegral x :: Int8)
613sext (ITFixed IT16) out [B16 x] = Just $ toInt out (fromIntegral x :: Int16)
614sext (ITFixed IT32) out [B32 x] = Just $ toInt out (fromIntegral x :: Int32)
615sext (ITFixed IT64) out [B64 x] = Just $ toInt out (fromIntegral x :: Int64)
616sext ITBig _ _ = Nothing
617sext from to val = intToInt from to val
619trunc :: IntTy -> IntTy -> [Const] -> Maybe Const
620trunc ITBig to val = intToInt ITBig to val
621trunc _ ITBig _ = Nothing
622trunc f@(ITFixed from) t@(ITFixed to) val | nativeTyWidth from > nativeTyWidth to = intToInt f t val
623trunc ITNative to [I x] = Just $ toInt to x
624trunc from ITNative val = intToInt from ITNative val
625trunc _ _ _ = Nothing
627intToStr :: [Const] -> Maybe Const
628intToStr val | [i] <- getInt val = Just $ Str (show i)
629intToStr _ = Nothing
631getInt :: [Const] -> [Integer]
632getInt (B8 x : xs) = toInteger x : getInt xs
633getInt (B16 x : xs) = toInteger x : getInt xs
634getInt (B32 x : xs) = toInteger x : getInt xs
635getInt (B64 x : xs) = toInteger x : getInt xs
636getInt (I x : xs) = toInteger x : getInt xs
637getInt (BI x : xs) = x : getInt xs
638getInt _ = []
640strToInt :: IntTy -> [Const] -> Maybe Const
641strToInt ity [Str x] = case reads x of
642 [(n,"")] -> Just $ toInt ity (n :: Integer)
643 _ -> Just $ I 0
644strToInt _ _ = Nothing
646intToFloat :: [Const] -> Maybe Const
647intToFloat val | [i] <- getInt val = Just $ Fl (fromIntegral i)
648intToFloat _ = Nothing
650floatToInt :: IntTy -> [Const] -> Maybe Const
651floatToInt ity [Fl x] = Just $ toInt ity (truncate x :: Integer)
652floatToInt _ _ = Nothing
654c_intToChar, c_charToInt :: [Const] -> Maybe Const
655c_intToChar [(I x)] = Just . Ch . toEnum $ x
656c_intToChar _ = Nothing
657c_charToInt [(Ch x)] = Just . I . fromEnum $ x
658c_charToInt _ = Nothing
660c_floatToStr :: [Const] -> Maybe Const
661c_floatToStr [Fl x] = Just $ Str (show x)
662c_floatToStr _ = Nothing
663c_strToFloat [Str x] = case reads x of
664 [(n,"")] -> Just $ Fl n
665 _ -> Just $ Fl 0
666c_strToFloat _ = Nothing
668p_fPrim :: (Double -> Double) -> [Const] -> Maybe Const
669p_fPrim f [Fl x] = Just $ Fl (f x)
670p_fPrim f _ = Nothing
672p_floatExp, p_floatLog, p_floatSin, p_floatCos, p_floatTan, p_floatASin, p_floatACos, p_floatATan, p_floatSqrt, p_floatFloor, p_floatCeil :: [Const] -> Maybe Const
673p_floatExp = p_fPrim exp
674p_floatLog = p_fPrim log
675p_floatSin = p_fPrim sin
676p_floatCos = p_fPrim cos
677p_floatTan = p_fPrim tan
678p_floatASin = p_fPrim asin
679p_floatACos = p_fPrim acos
680p_floatATan = p_fPrim atan
681p_floatSqrt = p_fPrim sqrt
682p_floatFloor = p_fPrim (fromInteger . floor)
683p_floatCeil = p_fPrim (fromInteger . ceiling)
685p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev :: [Const] -> Maybe Const
686p_strLen [Str xs] = Just $ I (length xs)
687p_strLen _ = Nothing
688p_strHead [Str (x:xs)] = Just $ Ch x
689p_strHead _ = Nothing
690p_strTail [Str (x:xs)] = Just $ Str xs
691p_strTail _ = Nothing
692p_strIndex [Str xs, I i]
693 | i < length xs = Just $ Ch (xs!!i)
694p_strIndex _ = Nothing
695p_strCons [Ch x, Str xs] = Just $ Str (x:xs)
696p_strCons _ = Nothing
697p_strRev [Str xs] = Just $ Str (reverse xs)
698p_strRev _ = Nothing
700p_cantreduce :: a -> Maybe b
701p_cantreduce _ = Nothing