@@ -22,16 +22,20 @@ data Prim = Prim { p_name :: Name,
2222 p_total :: Totality
2323 }
2424
25+ty :: [Const] -> Const -> Type
2526ty [] x = Constant x
2627ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
2728
29+believeTy :: Type
2830believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))
2931 (Bind (UN "b") (Pi (TType (UVar (-2))))
3032 (Bind (UN "x") (Pi (V 1)) (V 1)))
3133
34+total, partial :: Totality
3235total = Total []
33−partial = Partial NotCovering
36+partial = Partial NotCovering
3437
38+primitives :: [Prim]
3539primitives =
3640 -- operators
3741 [Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))
@@ -138,7 +142,7 @@ primitives =
138142 (1, LFloatStr) total,
139143
140144 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)
141− (1, LFExp) total,
145+ (1, LFExp) total,
142146 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)
143147 (1, LFLog) total,
144148 Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)
@@ -181,6 +185,7 @@ primitives =
181185 (3, LNoOp) partial -- ahem
182186 ] ++ concatMap intOps [IT8, IT16, IT32, IT64, ITBig, ITNative]
183187
188+intOps :: IntTy -> [Prim]
184189intOps ity =
185190 [ iCmp ity "lt" (bCmp ity (<)) LLt total
186191 , iCmp ity "lte" (bCmp ity (<=)) LLe total
@@ -216,50 +221,67 @@ intTyName ITNative = "Int"
216221intTyName ITBig = "BigInt"
217222intTyName sized = "B" ++ show (intTyWidth sized)
218223
224+iCmp, iBinOp, iUnOp :: IntTy -> String -> ([Value] -> Maybe Value) -> (IntTy -> PrimFn) -> Totality -> Prim
219225iCmp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) IType) 2 impl (2, irop ity) totality
220226iBinOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) (intTyToConst ity)) 2 impl (2, irop ity) totality
221227iUnOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty [intTyToConst ity] (intTyToConst ity)) 1 impl (1, irop ity) totality
228+
229+iCoerce :: IntTy -> IntTy -> String -> (IntTy -> IntTy -> [Value] -> Maybe Value) -> (IntTy -> IntTy -> PrimFn) -> Prim
222230iCoerce from to op impl irop =
223231 Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)
224232 (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total
225233
234+p_believeMe :: [a] -> Maybe a
226235p_believeMe [_,_,x] = Just x
227236p_believeMe _ = Nothing
228237
238+iUn :: (Int -> Int) -> [Value] -> Maybe Value
229239iUn op [VConstant (I x)] = Just $ VConstant (I (op x))
230240iUn _ _ = Nothing
231241
242+iBin :: (Int -> Int -> Int) -> [Value] -> Maybe Value
232243iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
233244iBin _ _ = Nothing
234245
246+bBin :: (Integer -> Integer -> Integer) -> [Value] -> Maybe Value
235247bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))
236248bBin _ _ = Nothing
237249
250+bBini :: (Integer -> Integer -> Int) -> [Value] -> Maybe Value
238251bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))
239252bBini _ _ = Nothing
240253
254+biBin :: (Int -> Int -> Bool) -> [Value] -> Maybe Value
241255biBin op = iBin (\x y -> if (op x y) then 1 else 0)
256+
257+bbBin :: (Integer -> Integer -> Bool) -> [Value] -> Maybe Value
242258bbBin op = bBini (\x y -> if (op x y) then 1 else 0)
243259
260+fBin :: (Double -> Double -> Double) -> [Value] -> Maybe Value
244261fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))
245262fBin _ _ = Nothing
246263
264+bfBin :: (Double -> Double -> Bool) -> [Value] -> Maybe Value
247265bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in
248266 Just $ VConstant (I i)
249267bfBin _ _ = Nothing
250268
269+bcBin :: (Char -> Char -> Bool) -> [Value] -> Maybe Value
251270bcBin op [VConstant (Ch x), VConstant (Ch y)] = let i = (if op x y then 1 else 0) in
252271 Just $ VConstant (I i)
253272bcBin _ _ = Nothing
254273
255−bsBin op [VConstant (Str x), VConstant (Str y)]
274+bsBin :: (String -> String -> Bool) -> [Value] -> Maybe Value
275+bsBin op [VConstant (Str x), VConstant (Str y)]
256276 = let i = (if op x y then 1 else 0) in
257277 Just $ VConstant (I i)
258278bsBin _ _ = Nothing
259279
280+sBin :: (String -> String -> String) -> [Value] -> Maybe Value
260281sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
261282sBin _ _ = Nothing
262283
284+bsrem :: IntTy -> [Value] -> Maybe Value
263285bsrem IT8 [VConstant (B8 x), VConstant (B8 y)]
264286 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8)))
265287bsrem IT16 [VConstant (B16 x), VConstant (B16 y)]
@@ -271,6 +293,7 @@ bsrem IT64 [VConstant (B64 x), VConstant (B64 y)]
271293bsrem ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `rem` y))
272294bsrem _ _ = Nothing
273295
296+bsdiv :: IntTy -> [Value] -> Maybe Value
274297bsdiv IT8 [VConstant (B8 x), VConstant (B8 y)]
275298 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8)))
276299bsdiv IT16 [VConstant (B16 x), VConstant (B16 y)]
@@ -282,6 +305,7 @@ bsdiv IT64 [VConstant (B64 x), VConstant (B64 y)]
282305bsdiv ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `div` y))
283306bsdiv _ _ = Nothing
284307
308+bashr :: IntTy -> [Value] -> Maybe Value
285309bashr IT8 [VConstant (B8 x), VConstant (B8 y)]
286310 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8)))
287311bashr IT16 [VConstant (B16 x), VConstant (B16 y)]
@@ -320,6 +344,7 @@ bCmp ITBig op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (if (op
320344bCmp ITNative op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
321345bCmp _ _ _ = Nothing
322346
347+toInt :: Integral a => IntTy -> a -> Value
323348toInt IT8 x = VConstant (B8 (fromIntegral x))
324349toInt IT16 x = VConstant (B16 (fromIntegral x))
325350toInt IT32 x = VConstant (B32 (fromIntegral x))
@@ -327,6 +352,7 @@ toInt IT64 x = VConstant (B64 (fromIntegral x))
327352toInt ITBig x = VConstant (BI (fromIntegral x))
328353toInt ITNative x = VConstant (I (fromIntegral x))
329354
355+intToInt :: IntTy -> IntTy -> [Value] -> Maybe Value
330356intToInt IT8 out [VConstant (B8 x)] = Just $ toInt out x
331357intToInt IT16 out [VConstant (B16 x)] = Just $ toInt out x
332358intToInt IT32 out [VConstant (B32 x)] = Just $ toInt out x
@@ -335,12 +361,14 @@ intToInt ITBig out [VConstant (BI x)] = Just $ toInt out x
335361intToInt ITNative out [VConstant (I x)] = Just $ toInt out x
336362intToInt _ _ _ = Nothing
337363
364+zext :: IntTy -> IntTy -> [Value] -> Maybe Value
338365zext from ITBig val = intToInt from ITBig val
339366zext ITBig _ _ = Nothing
340367zext from to val
341368 | intTyWidth from < intTyWidth to = intToInt from to val
342369zext _ _ _ = Nothing
343370
371+sext :: IntTy -> IntTy -> [Value] -> Maybe Value
344372sext IT8 out [VConstant (B8 x)] = Just $ toInt out (fromIntegral x :: Int8)
345373sext IT16 out [VConstant (B16 x)] = Just $ toInt out (fromIntegral x :: Int16)
346374sext IT32 out [VConstant (B32 x)] = Just $ toInt out (fromIntegral x :: Int32)
@@ -348,6 +376,7 @@ sext IT64 out [VConstant (B64 x)] = Just $ toInt out (fromIntegral x :: Int64)
348376sext ITBig _ _ = Nothing
349377sext from to val = intToInt from to val
350378
379+trunc :: IntTy -> IntTy -> [Value] -> Maybe Value
351380trunc ITBig to val = intToInt ITBig to val
352381trunc _ ITBig _ = Nothing
353382trunc from to val | intTyWidth from > intTyWidth to = intToInt from to val
@@ -362,25 +391,31 @@ getInt [VConstant (I x)] = Just . toInteger $ x
362391getInt [VConstant (BI x)] = Just x
363392getInt _ = Nothing
364393
394+intToStr :: [Value] -> Maybe Value
365395intToStr val | Just i <- getInt val = Just $ VConstant (Str (show i))
366396intToStr _ = Nothing
367397
398+strToInt :: IntTy -> [Value] -> Maybe Value
368399strToInt ity [VConstant (Str x)] = case reads x of
369400 [(n,"")] -> Just $ toInt ity (n :: Integer)
370401 _ -> Just $ VConstant (I 0)
371402strToInt _ _ = Nothing
372403
404+intToFloat :: [Value] -> Maybe Value
373405intToFloat val | Just i <- getInt val = Just $ VConstant (Fl (fromIntegral i))
374406intToFloat _ = Nothing
375407
408+floatToInt :: IntTy -> [Value] -> Maybe Value
376409floatToInt ity [VConstant (Fl x)] = Just $ toInt ity (truncate x :: Integer)
377410floatToInt _ _ = Nothing
378411
412+c_intToChar :: [Value] -> Maybe Value
379413c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))
380414c_intToChar _ = Nothing
381415c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))
382416c_charToInt _ = Nothing
383417
418+c_floatToStr :: [Value] -> Maybe Value
384419c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
385420c_floatToStr _ = Nothing
386421c_strToFloat [VConstant (Str x)] = case reads x of
@@ -388,9 +423,11 @@ c_strToFloat [VConstant (Str x)] = case reads x of
388423 _ -> Just $ VConstant (Fl 0)
389424c_strToFloat _ = Nothing
390425
426+p_fPrim :: (Double -> Double) -> [Value] -> Maybe Value
391427p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))
392428p_fPrim f _ = Nothing
393429
430+p_floatExp, p_floatLog, p_floatSin, p_floatCos, p_floatTan, p_floatASin, p_floatACos, p_floatATan, p_floatSqrt, p_floatFloor, p_floatCeil :: [Value] -> Maybe Value
394431p_floatExp = p_fPrim exp
395432p_floatLog = p_fPrim log
396433p_floatSin = p_fPrim sin
@@ -403,13 +440,14 @@ p_floatSqrt = p_fPrim sqrt
403440p_floatFloor = p_fPrim (fromInteger . floor)
404441p_floatCeil = p_fPrim (fromInteger . ceiling)
405442
443+p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev :: [Value] -> Maybe Value
406444p_strLen [VConstant (Str xs)] = Just $ VConstant (I (length xs))
407445p_strLen _ = Nothing
408446p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)
409447p_strHead _ = Nothing
410448p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)
411449p_strTail _ = Nothing
412−p_strIndex [VConstant (Str xs), VConstant (I i)]
450+p_strIndex [VConstant (Str xs), VConstant (I i)]
413451 | i < length xs = Just $ VConstant (Ch (xs!!i))
414452p_strIndex _ = Nothing
415453p_strCons [VConstant (Ch x), VConstant (Str xs)] = Just $ VConstant (Str (x:xs))
@@ -417,17 +455,18 @@ p_strCons _ = Nothing
417455p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))
418456p_strRev _ = Nothing
419457
458+p_cantreduce :: a -> Maybe b
420459p_cantreduce _ = Nothing
421460
422461elabPrim :: Prim -> Idris ()
423−elabPrim (Prim n ty i def sc tot)
462+elabPrim (Prim n ty i def sc tot)
424463 = do updateContext (addOperator n ty i def)
425464 setTotality n tot
426465 i <- getIState
427466 putIState i { idris_scprims = (n, sc) : idris_scprims i }
428467
429468elabPrims :: Idris ()
430−elabPrims = do mapM_ (elabDecl EAll toplevel)
469+elabPrims = do mapM_ (elabDecl EAll toplevel)
431470 (map (PData "" defaultSyntax (FC "builtin" 0) False)
432471 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
433472 mapM_ elabPrim primitives