1{-# LANGUAGE RankNTypes, ScopedTypeVariables, PatternGuards #-}
3module Idris.Primitives(primitives, Prim(..)) where
15data Prim = Prim { p_name :: Name,
18 p_def :: [Const] -> Maybe Const,
19 p_lexp :: (Int, PrimFn),
23ty :: [Const] -> Const -> Type
25ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
27total, partial :: Totality
29partial = Partial NotCovering
34 [Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))
35 (2, LEq ITNative) total,
36 Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))
37 (2, LLt ITNative) total,
38 Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))
39 (2, LLe ITNative) total,
40 Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))
41 (2, LGt ITNative) total,
42 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))
43 (2, LGe ITNative) total,
45 iCoerce IT8 IT16 "zext" zext LZExt,
46 iCoerce IT8 IT32 "zext" zext LZExt,
47 iCoerce IT8 IT64 "zext" zext LZExt,
48 iCoerce IT8 ITBig "zext" zext LZExt,
49 iCoerce IT8 ITNative "zext" zext LZExt,
50 iCoerce IT16 IT32 "zext" zext LZExt,
51 iCoerce IT16 IT64 "zext" zext LZExt,
52 iCoerce IT16 ITBig "zext" zext LZExt,
53 iCoerce IT16 ITNative "zext" zext LZExt,
54 iCoerce IT32 IT64 "zext" zext LZExt,
55 iCoerce IT32 ITBig "zext" zext LZExt,
56 iCoerce IT32 ITNative "zext" zext LZExt,
57 iCoerce IT64 ITBig "zext" zext LZExt,
58 iCoerce ITNative ITBig "zext" zext LZExt,
59 iCoerce ITNative IT64 "zext" zext LZExt,
60 iCoerce ITNative IT32 "zext" zext LZExt,
61 iCoerce ITNative IT16 "zext" zext LZExt,
63 iCoerce IT8 IT16 "sext" sext LSExt,
64 iCoerce IT8 IT32 "sext" sext LSExt,
65 iCoerce IT8 IT64 "sext" sext LSExt,
66 iCoerce IT8 ITBig "sext" sext LSExt,
67 iCoerce IT8 ITNative "sext" sext LSExt,
68 iCoerce IT16 IT32 "sext" sext LSExt,
69 iCoerce IT16 IT64 "sext" sext LSExt,
70 iCoerce IT16 ITBig "sext" sext LSExt,
71 iCoerce IT16 ITNative "sext" sext LSExt,
72 iCoerce IT32 IT64 "sext" sext LSExt,
73 iCoerce IT32 ITBig "sext" sext LSExt,
74 iCoerce IT32 ITNative "sext" sext LSExt,
75 iCoerce IT64 ITBig "sext" sext LSExt,
76 iCoerce ITNative ITBig "sext" sext LSExt,
77 iCoerce ITNative ITBig "sext" sext LSExt,
78 iCoerce ITNative IT64 "sext" sext LSExt,
79 iCoerce ITNative IT32 "sext" sext LSExt,
80 iCoerce ITNative IT16 "sext" sext LSExt,
82 iCoerce IT16 IT8 "trunc" trunc LTrunc,
83 iCoerce IT32 IT8 "trunc" trunc LTrunc,
84 iCoerce IT64 IT8 "trunc" trunc LTrunc,
85 iCoerce ITBig IT8 "trunc" trunc LTrunc,
86 iCoerce ITNative IT8 "trunc" trunc LTrunc,
87 iCoerce IT32 IT16 "trunc" trunc LTrunc,
88 iCoerce IT64 IT16 "trunc" trunc LTrunc,
89 iCoerce ITBig IT16 "trunc" trunc LTrunc,
90 iCoerce ITNative IT16 "trunc" trunc LTrunc,
91 iCoerce IT64 IT32 "trunc" trunc LTrunc,
92 iCoerce ITBig IT32 "trunc" trunc LTrunc,
93 iCoerce ITNative IT32 "trunc" trunc LTrunc,
94 iCoerce ITBig IT64 "trunc" trunc LTrunc,
95 iCoerce IT16 ITNative "trunc" trunc LTrunc,
96 iCoerce IT32 ITNative "trunc" trunc LTrunc,
97 iCoerce IT64 ITNative "trunc" trunc LTrunc,
98 iCoerce ITBig ITNative "trunc" trunc LTrunc,
99 iCoerce ITNative IT64 "trunc" trunc LTrunc,
101 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))
103 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))
105 Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))
107 Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))
109 Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))
111 Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))
113 Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))
115 Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))
117 Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))
119 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
120 (2, LStrConcat) total,
121 Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))
123 Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))
125 Prim (UN "prim_lenString") (ty [StrType] IType) 1 (p_strLen)
128 Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)
129 (1, LChInt ITNative) total,
130 Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)
131 (1, LIntCh ITNative) total,
132 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)
133 (1, LStrFloat) total,
134 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)
135 (1, LFloatStr) total,
137 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)
139 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)
141 Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)
143 Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos)
145 Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan)
147 Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin)
149 Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos)
151 Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan)
153 Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt)
155 Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor)
157 Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil)
160 Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)
161 (1, LStrHead) partial,
162 Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)
163 (1, LStrTail) partial,
164 Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)
166 Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)
167 (2, LStrIndex) partial,
168 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)
170 Prim (UN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)
171 (1, LReadStr) partial,
172 Prim (UN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)
175 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)
177 ] ++ concatMap intOps [IT8, IT16, IT32, IT64, ITBig, ITNative]
179intOps :: IntTy -> [Prim]
181 [ iCmp ity "lt" (bCmp ity (<)) LLt total
182 , iCmp ity "lte" (bCmp ity (<=)) LLe total
183 , iCmp ity "eq" (bCmp ity (==)) LEq total
184 , iCmp ity "gte" (bCmp ity (>=)) LGe total
185 , iCmp ity "gt" (bCmp ity (>)) LGt total
186 , iBinOp ity "add" (bitBin ity (+)) LPlus total
187 , iBinOp ity "sub" (bitBin ity (-)) LMinus total
188 , iBinOp ity "mul" (bitBin ity (*)) LTimes total
189 , iBinOp ity "udiv" (bitBin ity div) LUDiv partial
190 , iBinOp ity "sdiv" (bsdiv ity) LSDiv partial
191 , iBinOp ity "urem" (bitBin ity rem) LURem partial
192 , iBinOp ity "srem" (bsrem ity) LSRem partial
193 , iBinOp ity "shl" (bitBin ity (\x y -> shiftL x (fromIntegral y))) LSHL total
194 , iBinOp ity "lshr" (bitBin ity (\x y -> shiftR x (fromIntegral y))) LLSHR total
195 , iBinOp ity "ashr" (bashr ity) LASHR total
196 , iBinOp ity "and" (bitBin ity (.&.)) LAnd total
197 , iBinOp ity "or" (bitBin ity (.|.)) LOr total
198 , iBinOp ity "xor" (bitBin ity (xor)) LXOr total
199 , iUnOp ity "compl" (bUn ity complement) LCompl total
200 , Prim (UN $ "prim__toStr" ++ intTyName ity) (ty [intTyToConst ity] StrType) 1 intToStr
201 (1, LIntStr ity) total
202 , Prim (UN $ "prim__fromStr" ++ intTyName ity) (ty [StrType] (intTyToConst ity)) 1 (strToInt ity)
203 (1, LStrInt ity) total
204 , Prim (UN $ "prim__toFloat" ++ intTyName ity) (ty [intTyToConst ity] FlType) 1 intToFloat
205 (1, LIntFloat ity) total
206 , Prim (UN $ "prim__fromFloat" ++ intTyName ity) (ty [FlType] (intTyToConst ity)) 1 (floatToInt ity)
207 (1, LFloatInt ity) total
210intTyName :: IntTy -> String
211intTyName ITNative = "Int"
212intTyName ITBig = "BigInt"
213intTyName sized = "B" ++ show (intTyWidth sized)
215iCmp, iBinOp, iUnOp :: IntTy -> String -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim
216iCmp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) IType) 2 impl (2, irop ity) totality
217iBinOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) (intTyToConst ity)) 2 impl (2, irop ity) totality
218iUnOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty [intTyToConst ity] (intTyToConst ity)) 1 impl (1, irop ity) totality
220iCoerce :: IntTy -> IntTy -> String -> (IntTy -> IntTy -> [Const] -> Maybe Const) -> (IntTy -> IntTy -> PrimFn) -> Prim
221iCoerce from to op impl irop =
222 Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)
223 (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total
225iUn :: (Int -> Int) -> [Const] -> Maybe Const
226iUn op [I x] = Just $ I (op x)
229iBin :: (Int -> Int -> Int) -> [Const] -> Maybe Const
230iBin op [I x, I y] = Just $ I (op x y)
233bBin :: (Integer -> Integer -> Integer) -> [Const] -> Maybe Const
234bBin op [BI x, BI y] = Just $ BI (op x y)
237bBini :: (Integer -> Integer -> Int) -> [Const] -> Maybe Const
238bBini op [BI x, BI y] = Just $ I (op x y)
241biBin :: (Int -> Int -> Bool) -> [Const] -> Maybe Const
242biBin op = iBin (\x y -> if (op x y) then 1 else 0)
244bbBin :: (Integer -> Integer -> Bool) -> [Const] -> Maybe Const
245bbBin op = bBini (\x y -> if (op x y) then 1 else 0)
247fBin :: (Double -> Double -> Double) -> [Const] -> Maybe Const
248fBin op [Fl x, Fl y] = Just $ Fl (op x y)
251bfBin :: (Double -> Double -> Bool) -> [Const] -> Maybe Const
252bfBin op [Fl x, Fl y] = let i = (if op x y then 1 else 0) in
256bcBin :: (Char -> Char -> Bool) -> [Const] -> Maybe Const
257bcBin op [Ch x, Ch y] = let i = (if op x y then 1 else 0) in
261bsBin :: (String -> String -> Bool) -> [Const] -> Maybe Const
262bsBin op [Str x, Str y]
263 = let i = (if op x y then 1 else 0) in
267sBin :: (String -> String -> String) -> [Const] -> Maybe Const
268sBin op [Str x, Str y] = Just $ Str (op x y)
271bsrem :: IntTy -> [Const] -> Maybe Const
272bsrem IT8 [B8 x, B8 y]
273 = Just $ B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8))
274bsrem IT16 [B16 x, B16 y]
275 = Just $ B16 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16))
276bsrem IT32 [B32 x, B32 y]
277 = Just $ B32 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32))
278bsrem IT64 [B64 x, B64 y]
279 = Just $ B64 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64))
280bsrem ITNative [I x, I y] = Just $ I (x `rem` y)
283bsdiv :: IntTy -> [Const] -> Maybe Const
284bsdiv IT8 [B8 x, B8 y]
285 = Just $ B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8))
286bsdiv IT16 [B16 x, B16 y]
287 = Just $ B16 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int16))
288bsdiv IT32 [B32 x, B32 y]
289 = Just $ B32 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int32))
290bsdiv IT64 [B64 x, B64 y]
291 = Just $ B64 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int64))
292bsdiv ITNative [I x, I y] = Just $ I (x `div` y)
295bashr :: IntTy -> [Const] -> Maybe Const
296bashr IT8 [B8 x, B8 y]
297 = Just $ B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8))
298bashr IT16 [B16 x, B16 y]
299 = Just $ B16 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int16))
300bashr IT32 [B32 x, B32 y]
301 = Just $ B32 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int32))
302bashr IT64 [B64 x, B64 y]
303 = Just $ B64 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int64))
304bashr ITNative [I x, I y] = Just $ I (x `shiftR` y)
307bUn :: IntTy -> (forall a. Bits a => a -> a) -> [Const] -> Maybe Const
308bUn IT8 op [B8 x] = Just $ B8 (op x)
309bUn IT16 op [B16 x] = Just $ B16 (op x)
310bUn IT32 op [B32 x] = Just $ B32 (op x)
311bUn IT64 op [B64 x] = Just $ B64 (op x)
312bUn ITBig op [BI x] = Just $ BI (op x)
313bUn ITNative op [I x] = Just $ I (op x)
316bitBin :: IntTy -> (forall a. (Bits a, Integral a) => a -> a -> a) -> [Const] -> Maybe Const
317bitBin IT8 op [B8 x, B8 y] = Just $ B8 (op x y)
318bitBin IT16 op [B16 x, B16 y] = Just $ B16 (op x y)
319bitBin IT32 op [B32 x, B32 y] = Just $ B32 (op x y)
320bitBin IT64 op [B64 x, B64 y] = Just $ B64 (op x y)
321bitBin ITBig op [BI x, BI y] = Just $ BI (op x y)
322bitBin ITNative op [I x, I y] = Just $ I (op x y)
323bitBin _ _ _ = Nothing
325bCmp :: IntTy -> (forall a. Ord a => a -> a -> Bool) -> [Const] -> Maybe Const
326bCmp IT8 op [B8 x, B8 y] = Just $ I (if (op x y) then 1 else 0)
327bCmp IT16 op [B16 x, B16 y] = Just $ I (if (op x y) then 1 else 0)
328bCmp IT32 op [B32 x, B32 y] = Just $ I (if (op x y) then 1 else 0)
329bCmp IT64 op [B64 x, B64 y] = Just $ I (if (op x y) then 1 else 0)
330bCmp ITBig op [BI x, BI y] = Just $ I (if (op x y) then 1 else 0)
331bCmp ITNative op [I x, I y] = Just $ I (if (op x y) then 1 else 0)
334toInt :: Integral a => IntTy -> a -> Const
335toInt IT8 x = B8 (fromIntegral x)
336toInt IT16 x = B16 (fromIntegral x)
337toInt IT32 x = B32 (fromIntegral x)
338toInt IT64 x = B64 (fromIntegral x)
339toInt ITBig x = BI (fromIntegral x)
340toInt ITNative x = I (fromIntegral x)
342intToInt :: IntTy -> IntTy -> [Const] -> Maybe Const
343intToInt IT8 out [B8 x] = Just $ toInt out x
344intToInt IT16 out [B16 x] = Just $ toInt out x
345intToInt IT32 out [B32 x] = Just $ toInt out x
346intToInt IT64 out [B64 x] = Just $ toInt out x
347intToInt ITBig out [BI x] = Just $ toInt out x
348intToInt ITNative out [I x] = Just $ toInt out x
349intToInt _ _ _ = Nothing
351zext :: IntTy -> IntTy -> [Const] -> Maybe Const
352zext from ITBig val = intToInt from ITBig val
353zext ITBig _ _ = Nothing
355 | intTyWidth from < intTyWidth to = intToInt from to val
358sext :: IntTy -> IntTy -> [Const] -> Maybe Const
359sext IT8 out [B8 x] = Just $ toInt out (fromIntegral x :: Int8)
360sext IT16 out [B16 x] = Just $ toInt out (fromIntegral x :: Int16)
361sext IT32 out [B32 x] = Just $ toInt out (fromIntegral x :: Int32)
362sext IT64 out [B64 x] = Just $ toInt out (fromIntegral x :: Int64)
363sext ITBig _ _ = Nothing
364sext from to val = intToInt from to val
366trunc :: IntTy -> IntTy -> [Const] -> Maybe Const
367trunc ITBig to val = intToInt ITBig to val
368trunc _ ITBig _ = Nothing
369trunc from to val | intTyWidth from > intTyWidth to = intToInt from to val
372getInt :: [Const] -> Maybe Integer
373getInt [B8 x] = Just . toInteger $ x
374getInt [B16 x] = Just . toInteger $ x
375getInt [B32 x] = Just . toInteger $ x
376getInt [B64 x] = Just . toInteger $ x
377getInt [I x] = Just . toInteger $ x
378getInt [BI x] = Just x
381intToStr :: [Const] -> Maybe Const
382intToStr val | Just i <- getInt val = Just $ Str (show i)
385strToInt :: IntTy -> [Const] -> Maybe Const
386strToInt ity [Str x] = case reads x of
387 [(n,"")] -> Just $ toInt ity (n :: Integer)
389strToInt _ _ = Nothing
391intToFloat :: [Const] -> Maybe Const
392intToFloat val | Just i <- getInt val = Just $ Fl (fromIntegral i)
393intToFloat _ = Nothing
395floatToInt :: IntTy -> [Const] -> Maybe Const
396floatToInt ity [Fl x] = Just $ toInt ity (truncate x :: Integer)
397floatToInt _ _ = Nothing
399c_intToChar, c_charToInt :: [Const] -> Maybe Const
400c_intToChar [(I x)] = Just . Ch . toEnum $ x
401c_intToChar _ = Nothing
402c_charToInt [(Ch x)] = Just . I . fromEnum $ x
403c_charToInt _ = Nothing
405c_floatToStr :: [Const] -> Maybe Const
406c_floatToStr [Fl x] = Just $ Str (show x)
407c_floatToStr _ = Nothing
408c_strToFloat [Str x] = case reads x of
409 [(n,"")] -> Just $ Fl n
411c_strToFloat _ = Nothing
413p_fPrim :: (Double -> Double) -> [Const] -> Maybe Const
414p_fPrim f [Fl x] = Just $ Fl (f x)
417p_floatExp, p_floatLog, p_floatSin, p_floatCos, p_floatTan, p_floatASin, p_floatACos, p_floatATan, p_floatSqrt, p_floatFloor, p_floatCeil :: [Const] -> Maybe Const
418p_floatExp = p_fPrim exp
419p_floatLog = p_fPrim log
420p_floatSin = p_fPrim sin
421p_floatCos = p_fPrim cos
422p_floatTan = p_fPrim tan
423p_floatASin = p_fPrim asin
424p_floatACos = p_fPrim acos
425p_floatATan = p_fPrim atan
426p_floatSqrt = p_fPrim sqrt
427p_floatFloor = p_fPrim (fromInteger . floor)
428p_floatCeil = p_fPrim (fromInteger . ceiling)
430p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev :: [Const] -> Maybe Const
431p_strLen [Str xs] = Just $ I (length xs)
433p_strHead [Str (x:xs)] = Just $ Ch x
435p_strTail [Str (x:xs)] = Just $ Str xs
437p_strIndex [Str xs, I i]
438 | i < length xs = Just $ Ch (xs!!i)
439p_strIndex _ = Nothing
440p_strCons [Ch x, Str xs] = Just $ Str (x:xs)
442p_strRev [Str xs] = Just $ Str (reverse xs)
445p_cantreduce :: a -> Maybe b
446p_cantreduce _ = Nothing
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list