@@ -17,7 +17,7 @@ import Data.Int
1717data Prim = Prim { p_name :: Name,
1818 p_type :: Type,
1919 p_arity :: Int,
20− p_def :: [Value] -> Maybe Value,
20+ p_def :: [Const] -> Maybe Const,
2121 p_lexp :: (Int, PrimFn),
2222 p_total :: Totality
2323 }
@@ -221,12 +221,12 @@ intTyName ITNative = "Int"
221221intTyName ITBig = "BigInt"
222222intTyName sized = "B" ++ show (intTyWidth sized)
223223
224−iCmp, iBinOp, iUnOp :: IntTy -> String -> ([Value] -> Maybe Value) -> (IntTy -> PrimFn) -> Totality -> Prim
224+iCmp, iBinOp, iUnOp :: IntTy -> String -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim
225225iCmp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) IType) 2 impl (2, irop ity) totality
226226iBinOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) (intTyToConst ity)) 2 impl (2, irop ity) totality
227227iUnOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty [intTyToConst ity] (intTyToConst ity)) 1 impl (1, irop ity) totality
228228
229−iCoerce :: IntTy -> IntTy -> String -> (IntTy -> IntTy -> [Value] -> Maybe Value) -> (IntTy -> IntTy -> PrimFn) -> Prim
229+iCoerce :: IntTy -> IntTy -> String -> (IntTy -> IntTy -> [Const] -> Maybe Const) -> (IntTy -> IntTy -> PrimFn) -> Prim
230230iCoerce from to op impl irop =
231231 Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)
232232 (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total
@@ -235,199 +235,199 @@ p_believeMe :: [a] -> Maybe a
235235p_believeMe [_,_,x] = Just x
236236p_believeMe _ = Nothing
237237
238−iUn :: (Int -> Int) -> [Value] -> Maybe Value
239−iUn op [VConstant (I x)] = Just $ VConstant (I (op x))
238+iUn :: (Int -> Int) -> [Const] -> Maybe Const
239+iUn op [I x] = Just $ I (op x)
240240iUn _ _ = Nothing
241241
242−iBin :: (Int -> Int -> Int) -> [Value] -> Maybe Value
243−iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
242+iBin :: (Int -> Int -> Int) -> [Const] -> Maybe Const
243+iBin op [I x, I y] = Just $ I (op x y)
244244iBin _ _ = Nothing
245245
246−bBin :: (Integer -> Integer -> Integer) -> [Value] -> Maybe Value
247−bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))
246+bBin :: (Integer -> Integer -> Integer) -> [Const] -> Maybe Const
247+bBin op [BI x, BI y] = Just $ BI (op x y)
248248bBin _ _ = Nothing
249249
250−bBini :: (Integer -> Integer -> Int) -> [Value] -> Maybe Value
251−bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))
250+bBini :: (Integer -> Integer -> Int) -> [Const] -> Maybe Const
251+bBini op [BI x, BI y] = Just $ I (op x y)
252252bBini _ _ = Nothing
253253
254−biBin :: (Int -> Int -> Bool) -> [Value] -> Maybe Value
254+biBin :: (Int -> Int -> Bool) -> [Const] -> Maybe Const
255255biBin op = iBin (\x y -> if (op x y) then 1 else 0)
256256
257−bbBin :: (Integer -> Integer -> Bool) -> [Value] -> Maybe Value
257+bbBin :: (Integer -> Integer -> Bool) -> [Const] -> Maybe Const
258258bbBin op = bBini (\x y -> if (op x y) then 1 else 0)
259259
260−fBin :: (Double -> Double -> Double) -> [Value] -> Maybe Value
261−fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))
260+fBin :: (Double -> Double -> Double) -> [Const] -> Maybe Const
261+fBin op [Fl x, Fl y] = Just $ Fl (op x y)
262262fBin _ _ = Nothing
263263
264−bfBin :: (Double -> Double -> Bool) -> [Value] -> Maybe Value
265−bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in
266− Just $ VConstant (I i)
264+bfBin :: (Double -> Double -> Bool) -> [Const] -> Maybe Const
265+bfBin op [Fl x, Fl y] = let i = (if op x y then 1 else 0) in
266+ Just $ I i
267267bfBin _ _ = Nothing
268268
269−bcBin :: (Char -> Char -> Bool) -> [Value] -> Maybe Value
270−bcBin op [VConstant (Ch x), VConstant (Ch y)] = let i = (if op x y then 1 else 0) in
271− Just $ VConstant (I i)
269+bcBin :: (Char -> Char -> Bool) -> [Const] -> Maybe Const
270+bcBin op [Ch x, Ch y] = let i = (if op x y then 1 else 0) in
271+ Just $ I i
272272bcBin _ _ = Nothing
273273
274−bsBin :: (String -> String -> Bool) -> [Value] -> Maybe Value
275−bsBin op [VConstant (Str x), VConstant (Str y)]
274+bsBin :: (String -> String -> Bool) -> [Const] -> Maybe Const
275+bsBin op [Str x, Str y]
276276 = let i = (if op x y then 1 else 0) in
277− Just $ VConstant (I i)
277+ Just $ I i
278278bsBin _ _ = Nothing
279279
280−sBin :: (String -> String -> String) -> [Value] -> Maybe Value
281−sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
280+sBin :: (String -> String -> String) -> [Const] -> Maybe Const
281+sBin op [Str x, Str y] = Just $ Str (op x y)
282282sBin _ _ = Nothing
283283
284−bsrem :: IntTy -> [Value] -> Maybe Value
285−bsrem IT8 [VConstant (B8 x), VConstant (B8 y)]
286− = Just $ VConstant (B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8)))
287−bsrem IT16 [VConstant (B16 x), VConstant (B16 y)]
288− = Just $ VConstant (B16 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16)))
289−bsrem IT32 [VConstant (B32 x), VConstant (B32 y)]
290− = Just $ VConstant (B32 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32)))
291−bsrem IT64 [VConstant (B64 x), VConstant (B64 y)]
292− = Just $ VConstant (B64 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64)))
293−bsrem ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `rem` y))
284+bsrem :: IntTy -> [Const] -> Maybe Const
285+bsrem IT8 [B8 x, B8 y]
286+ = Just $ B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8))
287+bsrem IT16 [B16 x, B16 y]
288+ = Just $ B16 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16))
289+bsrem IT32 [B32 x, B32 y]
290+ = Just $ B32 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32))
291+bsrem IT64 [B64 x, B64 y]
292+ = Just $ B64 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64))
293+bsrem ITNative [I x, I y] = Just $ I (x `rem` y)
294294bsrem _ _ = Nothing
295295
296−bsdiv :: IntTy -> [Value] -> Maybe Value
297−bsdiv IT8 [VConstant (B8 x), VConstant (B8 y)]
298− = Just $ VConstant (B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8)))
299−bsdiv IT16 [VConstant (B16 x), VConstant (B16 y)]
300− = Just $ VConstant (B16 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int16)))
301−bsdiv IT32 [VConstant (B32 x), VConstant (B32 y)]
302− = Just $ VConstant (B32 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int32)))
303−bsdiv IT64 [VConstant (B64 x), VConstant (B64 y)]
304− = Just $ VConstant (B64 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int64)))
305−bsdiv ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `div` y))
296+bsdiv :: IntTy -> [Const] -> Maybe Const
297+bsdiv IT8 [B8 x, B8 y]
298+ = Just $ B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8))
299+bsdiv IT16 [B16 x, B16 y]
300+ = Just $ B16 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int16))
301+bsdiv IT32 [B32 x, B32 y]
302+ = Just $ B32 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int32))
303+bsdiv IT64 [B64 x, B64 y]
304+ = Just $ B64 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int64))
305+bsdiv ITNative [I x, I y] = Just $ I (x `div` y)
306306bsdiv _ _ = Nothing
307307
308−bashr :: IntTy -> [Value] -> Maybe Value
309−bashr IT8 [VConstant (B8 x), VConstant (B8 y)]
310− = Just $ VConstant (B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8)))
311−bashr IT16 [VConstant (B16 x), VConstant (B16 y)]
312− = Just $ VConstant (B16 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int16)))
313−bashr IT32 [VConstant (B32 x), VConstant (B32 y)]
314− = Just $ VConstant (B32 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int32)))
315−bashr IT64 [VConstant (B64 x), VConstant (B64 y)]
316− = Just $ VConstant (B64 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int64)))
317−bashr ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `shiftR` y))
308+bashr :: IntTy -> [Const] -> Maybe Const
309+bashr IT8 [B8 x, B8 y]
310+ = Just $ B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8))
311+bashr IT16 [B16 x, B16 y]
312+ = Just $ B16 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int16))
313+bashr IT32 [B32 x, B32 y]
314+ = Just $ B32 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int32))
315+bashr IT64 [B64 x, B64 y]
316+ = Just $ B64 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int64))
317+bashr ITNative [I x, I y] = Just $ I (x `shiftR` y)
318318bashr _ _ = Nothing
319319
320−bUn :: IntTy -> (forall a. Bits a => a -> a) -> [Value] -> Maybe Value
321−bUn IT8 op [VConstant (B8 x)] = Just $ VConstant (B8 (op x))
322−bUn IT16 op [VConstant (B16 x)] = Just $ VConstant (B16 (op x))
323−bUn IT32 op [VConstant (B32 x)] = Just $ VConstant (B32 (op x))
324−bUn IT64 op [VConstant (B64 x)] = Just $ VConstant (B64 (op x))
325−bUn ITBig op [VConstant (BI x)] = Just $ VConstant (BI (op x))
326−bUn ITNative op [VConstant (I x)] = Just $ VConstant (I (op x))
327−bUn _ _ _ = Nothing
328−
329−bitBin :: IntTy -> (forall a. (Bits a, Integral a) => a -> a -> a) -> [Value] -> Maybe Value
330−bitBin IT8 op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (B8 (op x y))
331−bitBin IT16 op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (B16 (op x y))
332−bitBin IT32 op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (B32 (op x y))
333−bitBin IT64 op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (B64 (op x y))
334−bitBin ITBig op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))
335−bitBin ITNative op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
336−bitBin _ _ _ = Nothing
337−
338−bCmp :: IntTy -> (forall a. Ord a => a -> a -> Bool) -> [Value] -> Maybe Value
339−bCmp IT8 op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
340−bCmp IT16 op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
341−bCmp IT32 op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
342−bCmp IT64 op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
343−bCmp ITBig op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
344−bCmp ITNative op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
345−bCmp _ _ _ = Nothing
346−
347−toInt :: Integral a => IntTy -> a -> Value
348−toInt IT8 x = VConstant (B8 (fromIntegral x))
349−toInt IT16 x = VConstant (B16 (fromIntegral x))
350−toInt IT32 x = VConstant (B32 (fromIntegral x))
351−toInt IT64 x = VConstant (B64 (fromIntegral x))
352−toInt ITBig x = VConstant (BI (fromIntegral x))
353−toInt ITNative x = VConstant (I (fromIntegral x))
354−
355−intToInt :: IntTy -> IntTy -> [Value] -> Maybe Value
356−intToInt IT8 out [VConstant (B8 x)] = Just $ toInt out x
357−intToInt IT16 out [VConstant (B16 x)] = Just $ toInt out x
358−intToInt IT32 out [VConstant (B32 x)] = Just $ toInt out x
359−intToInt IT64 out [VConstant (B64 x)] = Just $ toInt out x
360−intToInt ITBig out [VConstant (BI x)] = Just $ toInt out x
361−intToInt ITNative out [VConstant (I x)] = Just $ toInt out x
320+bUn :: IntTy -> (forall a. Bits a => a -> a) -> [Const] -> Maybe Const
321+bUn IT8 op [B8 x] = Just $ B8 (op x)
322+bUn IT16 op [B16 x] = Just $ B16 (op x)
323+bUn IT32 op [B32 x] = Just $ B32 (op x)
324+bUn IT64 op [B64 x] = Just $ B64 (op x)
325+bUn ITBig op [BI x] = Just $ BI (op x)
326+bUn ITNative op [I x] = Just $ I (op x)
327+bUn _ _ _ = Nothing
328+
329+bitBin :: IntTy -> (forall a. (Bits a, Integral a) => a -> a -> a) -> [Const] -> Maybe Const
330+bitBin IT8 op [B8 x, B8 y] = Just $ B8 (op x y)
331+bitBin IT16 op [B16 x, B16 y] = Just $ B16 (op x y)
332+bitBin IT32 op [B32 x, B32 y] = Just $ B32 (op x y)
333+bitBin IT64 op [B64 x, B64 y] = Just $ B64 (op x y)
334+bitBin ITBig op [BI x, BI y] = Just $ BI (op x y)
335+bitBin ITNative op [I x, I y] = Just $ I (op x y)
336+bitBin _ _ _ = Nothing
337+
338+bCmp :: IntTy -> (forall a. Ord a => a -> a -> Bool) -> [Const] -> Maybe Const
339+bCmp IT8 op [B8 x, B8 y] = Just $ I (if (op x y) then 1 else 0)
340+bCmp IT16 op [B16 x, B16 y] = Just $ I (if (op x y) then 1 else 0)
341+bCmp IT32 op [B32 x, B32 y] = Just $ I (if (op x y) then 1 else 0)
342+bCmp IT64 op [B64 x, B64 y] = Just $ I (if (op x y) then 1 else 0)
343+bCmp ITBig op [BI x, BI y] = Just $ I (if (op x y) then 1 else 0)
344+bCmp ITNative op [I x, I y] = Just $ I (if (op x y) then 1 else 0)
345+bCmp _ _ _ = Nothing
346+
347+toInt :: Integral a => IntTy -> a -> Const
348+toInt IT8 x = B8 (fromIntegral x)
349+toInt IT16 x = B16 (fromIntegral x)
350+toInt IT32 x = B32 (fromIntegral x)
351+toInt IT64 x = B64 (fromIntegral x)
352+toInt ITBig x = BI (fromIntegral x)
353+toInt ITNative x = I (fromIntegral x)
354+
355+intToInt :: IntTy -> IntTy -> [Const] -> Maybe Const
356+intToInt IT8 out [B8 x] = Just $ toInt out x
357+intToInt IT16 out [B16 x] = Just $ toInt out x
358+intToInt IT32 out [B32 x] = Just $ toInt out x
359+intToInt IT64 out [B64 x] = Just $ toInt out x
360+intToInt ITBig out [BI x] = Just $ toInt out x
361+intToInt ITNative out [I x] = Just $ toInt out x
362362intToInt _ _ _ = Nothing
363363
364−zext :: IntTy -> IntTy -> [Value] -> Maybe Value
364+zext :: IntTy -> IntTy -> [Const] -> Maybe Const
365365zext from ITBig val = intToInt from ITBig val
366366zext ITBig _ _ = Nothing
367367zext from to val
368368 | intTyWidth from < intTyWidth to = intToInt from to val
369369zext _ _ _ = Nothing
370370
371−sext :: IntTy -> IntTy -> [Value] -> Maybe Value
372−sext IT8 out [VConstant (B8 x)] = Just $ toInt out (fromIntegral x :: Int8)
373−sext IT16 out [VConstant (B16 x)] = Just $ toInt out (fromIntegral x :: Int16)
374−sext IT32 out [VConstant (B32 x)] = Just $ toInt out (fromIntegral x :: Int32)
375−sext IT64 out [VConstant (B64 x)] = Just $ toInt out (fromIntegral x :: Int64)
376−sext ITBig _ _ = Nothing
377−sext from to val = intToInt from to val
371+sext :: IntTy -> IntTy -> [Const] -> Maybe Const
372+sext IT8 out [B8 x] = Just $ toInt out (fromIntegral x :: Int8)
373+sext IT16 out [B16 x] = Just $ toInt out (fromIntegral x :: Int16)
374+sext IT32 out [B32 x] = Just $ toInt out (fromIntegral x :: Int32)
375+sext IT64 out [B64 x] = Just $ toInt out (fromIntegral x :: Int64)
376+sext ITBig _ _ = Nothing
377+sext from to val = intToInt from to val
378378
379−trunc :: IntTy -> IntTy -> [Value] -> Maybe Value
379+trunc :: IntTy -> IntTy -> [Const] -> Maybe Const
380380trunc ITBig to val = intToInt ITBig to val
381381trunc _ ITBig _ = Nothing
382382trunc from to val | intTyWidth from > intTyWidth to = intToInt from to val
383383trunc _ _ _ = Nothing
384384
385−getInt :: [Value] -> Maybe Integer
386−getInt [VConstant (B8 x)] = Just . toInteger $ x
387−getInt [VConstant (B16 x)] = Just . toInteger $ x
388−getInt [VConstant (B32 x)] = Just . toInteger $ x
389−getInt [VConstant (B64 x)] = Just . toInteger $ x
390−getInt [VConstant (I x)] = Just . toInteger $ x
391−getInt [VConstant (BI x)] = Just x
392−getInt _ = Nothing
393−
394−intToStr :: [Value] -> Maybe Value
395−intToStr val | Just i <- getInt val = Just $ VConstant (Str (show i))
385+getInt :: [Const] -> Maybe Integer
386+getInt [B8 x] = Just . toInteger $ x
387+getInt [B16 x] = Just . toInteger $ x
388+getInt [B32 x] = Just . toInteger $ x
389+getInt [B64 x] = Just . toInteger $ x
390+getInt [I x] = Just . toInteger $ x
391+getInt [BI x] = Just x
392+getInt _ = Nothing
393+
394+intToStr :: [Const] -> Maybe Const
395+intToStr val | Just i <- getInt val = Just $ Str (show i)
396396intToStr _ = Nothing
397397
398−strToInt :: IntTy -> [Value] -> Maybe Value
399−strToInt ity [VConstant (Str x)] = case reads x of
400− [(n,"")] -> Just $ toInt ity (n :: Integer)
401− _ -> Just $ VConstant (I 0)
398+strToInt :: IntTy -> [Const] -> Maybe Const
399+strToInt ity [Str x] = case reads x of
400+ [(n,"")] -> Just $ toInt ity (n :: Integer)
401+ _ -> Just $ I 0
402402strToInt _ _ = Nothing
403403
404−intToFloat :: [Value] -> Maybe Value
405−intToFloat val | Just i <- getInt val = Just $ VConstant (Fl (fromIntegral i))
404+intToFloat :: [Const] -> Maybe Const
405+intToFloat val | Just i <- getInt val = Just $ Fl (fromIntegral i)
406406intToFloat _ = Nothing
407407
408−floatToInt :: IntTy -> [Value] -> Maybe Value
409−floatToInt ity [VConstant (Fl x)] = Just $ toInt ity (truncate x :: Integer)
408+floatToInt :: IntTy -> [Const] -> Maybe Const
409+floatToInt ity [Fl x] = Just $ toInt ity (truncate x :: Integer)
410410floatToInt _ _ = Nothing
411411
412−c_intToChar :: [Value] -> Maybe Value
413−c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))
412+c_intToChar, c_charToInt :: [Const] -> Maybe Const
413+c_intToChar [(I x)] = Just . Ch . toEnum $ x
414414c_intToChar _ = Nothing
415−c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))
415+c_charToInt [(Ch x)] = Just . I . fromEnum $ x
416416c_charToInt _ = Nothing
417417
418−c_floatToStr :: [Value] -> Maybe Value
419−c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
418+c_floatToStr :: [Const] -> Maybe Const
419+c_floatToStr [Fl x] = Just $ Str (show x)
420420c_floatToStr _ = Nothing
421−c_strToFloat [VConstant (Str x)] = case reads x of
422− [(n,"")] -> Just $ VConstant (Fl n)
423− _ -> Just $ VConstant (Fl 0)
421+c_strToFloat [Str x] = case reads x of
422+ [(n,"")] -> Just $ Fl n
423+ _ -> Just $ Fl 0
424424c_strToFloat _ = Nothing
425425
426−p_fPrim :: (Double -> Double) -> [Value] -> Maybe Value
427−p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))
426+p_fPrim :: (Double -> Double) -> [Const] -> Maybe Const
427+p_fPrim f [Fl x] = Just $ Fl (f x)
428428p_fPrim f _ = Nothing
429429
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
430+p_floatExp, p_floatLog, p_floatSin, p_floatCos, p_floatTan, p_floatASin, p_floatACos, p_floatATan, p_floatSqrt, p_floatFloor, p_floatCeil :: [Const] -> Maybe Const
431431p_floatExp = p_fPrim exp
432432p_floatLog = p_fPrim log
433433p_floatSin = p_fPrim sin
@@ -440,27 +440,32 @@ p_floatSqrt = p_fPrim sqrt
440440p_floatFloor = p_fPrim (fromInteger . floor)
441441p_floatCeil = p_fPrim (fromInteger . ceiling)
442442
443−p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev :: [Value] -> Maybe Value
444−p_strLen [VConstant (Str xs)] = Just $ VConstant (I (length xs))
443+p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev :: [Const] -> Maybe Const
444+p_strLen [Str xs] = Just $ I (length xs)
445445p_strLen _ = Nothing
446−p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)
446+p_strHead [Str (x:xs)] = Just $ Ch x
447447p_strHead _ = Nothing
448−p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)
448+p_strTail [Str (x:xs)] = Just $ Str xs
449449p_strTail _ = Nothing
450−p_strIndex [VConstant (Str xs), VConstant (I i)]
451− | i < length xs = Just $ VConstant (Ch (xs!!i))
450+p_strIndex [Str xs, I i]
451+ | i < length xs = Just $ Ch (xs!!i)
452452p_strIndex _ = Nothing
453−p_strCons [VConstant (Ch x), VConstant (Str xs)] = Just $ VConstant (Str (x:xs))
453+p_strCons [Ch x, Str xs] = Just $ Str (x:xs)
454454p_strCons _ = Nothing
455−p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))
455+p_strRev [Str xs] = Just $ Str (reverse xs)
456456p_strRev _ = Nothing
457457
458458p_cantreduce :: a -> Maybe b
459459p_cantreduce _ = Nothing
460460
461+valuePrim :: ([Const] -> Maybe Const) -> [Value] -> Maybe Value
462+valuePrim prim vals = fmap VConstant (mapM getConst vals >>= prim)
463+ where getConst (VConstant c) = Just c
464+ getConst _ = Nothing
465+
461466elabPrim :: Prim -> Idris ()
462467elabPrim (Prim n ty i def sc tot)
463− = do updateContext (addOperator n ty i def)
468+ = do updateContext (addOperator n ty i (valuePrim def))
464469 setTotality n tot
465470 i <- getIState
466471 putIState i { idris_scprims = (n, sc) : idris_scprims i }