git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:edwinb/Idris-dev
58f3f68Edwin Brady
lib/Data/HVect.idrnew file+63
compare with master
unifiedsplit
@@ -0,0 +1,63 @@
1+module Data.HVect
2+
3+import Data.Vect
4+
5+%access public
6+%default total
7+
8+using (k : Nat, ts : Vect Type k)
9+ data HVect : Vect Type k -> Type where
10+ Nil : HVect []
11+ (::) : t -> HVect ts -> HVect (t::ts)
12+
13+ index : (i : Fin k) -> HVect ts -> index i ts
14+ index fO (x::xs) = x
15+ index (fS j) (x::xs) = index j xs
16+
17+ deleteAt : {us : Vect Type (S l)} -> (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)
18+ deleteAt fO (x::xs) = xs
19+ deleteAt {l = S m} (fS j) (x::xs) = x :: deleteAt j xs
20+ deleteAt _ [] impossible
21+
22+ replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)
23+ replaceAt fO y (x::xs) = y::xs
24+ replaceAt (fS j) y (x::xs) = x :: replaceAt j y xs
25+
26+ updateAt : (i : Fin k) -> (index i ts -> t) -> HVect ts -> HVect (replaceAt i t ts)
27+ updateAt fO f (x::xs) = f x :: xs
28+ updateAt (fS j) f (x::xs) = x :: updateAt j f xs
29+
30+ (++) : {us : Vect Type l} -> HVect ts -> HVect us -> HVect (ts ++ us)
31+ (++) [] ys = ys
32+ (++) (x::xs) ys = x :: (xs ++ ys)
33+
34+ instance Eq (HVect []) where
35+ [] == [] = True
36+
37+ instance (Eq t, Eq (HVect ts)) => Eq (HVect (t::ts)) where
38+ (x::xs) == (y::ys) = x == y && xs == ys
39+
40+ class Shows (k : Nat) (ts : Vect Type k) where
41+ shows : HVect ts -> Vect String k
42+
43+ instance Shows O [] where
44+ shows [] = []
45+
46+ instance (Show t, Shows k ts) => Shows (S k) (t::ts) where
47+ shows (x::xs) = show x :: shows xs
48+
49+ instance (Shows k ts) => Show (HVect ts) where
50+ show xs = show (shows xs)
51+
52+ get : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> HVect ts -> t
53+ get {p = Here} (x::xs) = x
54+ get {p = There p'} (x::xs) = get {p = p'} xs
55+
56+ put : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> t -> HVect ts -> HVect ts
57+ put {p = Here} y (x::xs) = y :: xs
58+ put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
59+
60+ update : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
61+ update {p = Here} f (x::xs) = f x :: xs
62+ update {p = There p'} f (x::xs) = x :: update {p = p'} f xs
63+
lib/Data/Vect.idrnew file+32
@@ -0,0 +1,32 @@
1+module Data.Vect
2+
3+import Language.Reflection
4+
5+%access public
6+%default total
7+
8+--------------------------------------------------------------------------------
9+-- Elem
10+--------------------------------------------------------------------------------
11+
12+data Elem : a -> Vect a k -> Type where
13+ Here : {xs : Vect a k} -> Elem x (x::xs)
14+ There : {xs : Vect a k} -> Elem x xs -> Elem x (y::xs)
15+
16+findElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic
17+findElem O ctxt goal = Refine "Here" `Seq` Solve
18+findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))
19+
20+replaceElem : (xs : Vect t k) -> Elem x xs -> (y : t) -> (ys : Vect t k ** Elem y ys)
21+replaceElem (x::xs) Here y = (y :: xs ** Here)
22+replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)
23+ | (ys ** yinys) = (x :: ys ** There yinys)
24+
25+replaceByElem : (xs : Vect t k) -> Elem x xs -> t -> Vect t k
26+replaceByElem (x::xs) Here y = y :: xs
27+replaceByElem (x::xs) (There xinxs) y = x :: replaceByElem xs xinxs y
28+
29+mapElem : {xs : Vect t k} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs)
30+mapElem Here = Here
31+mapElem (There e) = There (mapElem e)
32+
lib/Prelude/Vect.idr+4
@@ -41,6 +41,10 @@ deleteAt fO (x::xs) = xs
41deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs
41deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs
42deleteAt _ [] impossible
42deleteAt _ [] impossible
43
43
44+replaceAt : Fin n -> t -> Vect t n -> Vect t n
45+replaceAt fO y (x::xs) = y::xs
46+replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs
47+
44--------------------------------------------------------------------------------
48--------------------------------------------------------------------------------
45-- Subvectors
49-- Subvectors
46--------------------------------------------------------------------------------
50--------------------------------------------------------------------------------
lib/base.ipkg+1−1
@@ -25,7 +25,7 @@ modules = Builtins, Prelude, IO, System,
25 Data.Bits, Data.Mod2,
25 Data.Bits, Data.Mod2,
26 Data.Z, Data.Sign,
26 Data.Z, Data.Sign,
27 Data.SortedMap, Data.SortedSet, Data.BoundedList,
27 Data.SortedMap, Data.SortedSet, Data.BoundedList,
28− Data.Vect.Quantifiers,
28+ Data.Vect, Data.HVect, Data.Vect.Quantifiers,
29
29
30 Control.Monad.Identity, Control.Monad.State, Control.Category,
30 Control.Monad.Identity, Control.Monad.State, Control.Category,
31 Control.Arrow,
31 Control.Arrow,
src/Core/CoreParser.hs+10−7
@@ -57,13 +57,16 @@ lexWS = do i <- getInput
57 where
57 where
58
58
59 simpleSpace = skipMany1 (satisfy isSpace)
59 simpleSpace = skipMany1 (satisfy isSpace)
60− oneLineComment = do try (do string ("--")
60+ oneLineComment =
61+ try (void $ string "--\n") <|>
62+ do try (do string "--"
61− satisfy (\x -> x /= '|' && x /= '^'))
63+ satisfy (\x -> x /= '|' && x /= '^'))
62− skipMany (satisfy (/= '\n'))
64+ skipMany (satisfy (/= '\n'))
63− return ()
64− multiLineComment = do try (do string "{-"
65+ multiLineComment =
66+ try (void $ string "{--}") <|>
67+ do try (do string "{-"
65− satisfy (\x -> x /= '|' && x /= '^'))
68+ satisfy (\x -> x /= '|' && x /= '^'))
66− inCommentMulti
69+ inCommentMulti
67
70
68 inCommentMulti
71 inCommentMulti
69 = do{ try (string "-}") ; return () }
72 = do{ try (string "-}") ; return () }
src/Core/Evaluate.hs+1−1
@@ -174,7 +174,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
174 | i < length env && i >= 0 = return $ env !! i
174 | i < length env && i >= 0 = return $ env !! i
175 | otherwise = return $ VV i
175 | otherwise = return $ VV i
176 ev ntimes stk top env (Bind n (Let t v) sc)
176 ev ntimes stk top env (Bind n (Let t v) sc)
177− | not simpl -- || vinstances 0 sc < 2
177+ | not simpl -- - || vinstances 0 sc < 2
178 = do v' <- ev ntimes stk top env v --(finalise v)
178 = do v' <- ev ntimes stk top env v --(finalise v)
179 sc' <- ev ntimes stk top (v' : env) sc
179 sc' <- ev ntimes stk top (v' : env) sc
180 wknV (-1) sc'
180 wknV (-1) sc'
src/IRTS/CodegenC.hs+1−1
@@ -352,7 +352,7 @@ doOp v (LZExt from to) [x]
352 | intTyWidth from < intTyWidth to = bitCoerce v "Z" from to x
352 | intTyWidth from < intTyWidth to = bitCoerce v "Z" from to x
353doOp v (LTrunc ITNative to) [x] = v ++ "idris_b" ++ show (intTyWidth to) ++ "const(vm, GETINT(" ++ creg x ++ "))"
353doOp v (LTrunc ITNative to) [x] = v ++ "idris_b" ++ show (intTyWidth to) ++ "const(vm, GETINT(" ++ creg x ++ "))"
354doOp v (LTrunc from ITNative) [x] = v ++ "MKINT((i_int)" ++ creg x ++ "->info.bits" ++ show (intTyWidth from) ++ ")"
354doOp v (LTrunc from ITNative) [x] = v ++ "MKINT((i_int)" ++ creg x ++ "->info.bits" ++ show (intTyWidth from) ++ ")"
355−doOp v (LTrunc ITBig to) [x] = v ++ "idris_b" ++ show (intTyWidth to) ++ "const(vm, mpz_get_ui(GETMPZ(" ++ creg x ++ "))"
355+doOp v (LTrunc ITBig to) [x] = v ++ "idris_b" ++ show (intTyWidth to) ++ "const(vm, ISINT(" ++ creg x ++ ") ? GETINT(" ++ creg x ++ ") : mpz_get_ui(GETMPZ(" ++ creg x ++ ")))"
356doOp v (LTrunc from to) [x]
356doOp v (LTrunc from to) [x]
357 | intTyWidth from > intTyWidth to = bitCoerce v "T" from to x
357 | intTyWidth from > intTyWidth to = bitCoerce v "T" from to x
358
358
src/Idris/Primitives.hs+45−6
@@ -22,16 +22,20 @@ data Prim = Prim { p_name :: Name,
22 p_total :: Totality
22 p_total :: Totality
23 }
23 }
24
24
25+ty :: [Const] -> Const -> Type
25ty [] x = Constant x
26ty [] x = Constant x
26ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
27ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
27
28
29+believeTy :: Type
28believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))
30believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))
29 (Bind (UN "b") (Pi (TType (UVar (-2))))
31 (Bind (UN "b") (Pi (TType (UVar (-2))))
30 (Bind (UN "x") (Pi (V 1)) (V 1)))
32 (Bind (UN "x") (Pi (V 1)) (V 1)))
31
33
34+total, partial :: Totality
32total = Total []
35total = Total []
33−partial = Partial NotCovering
36+partial = Partial NotCovering
34
37
38+primitives :: [Prim]
35primitives =
39primitives =
36 -- operators
40 -- operators
37 [Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))
41 [Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))
@@ -138,7 +142,7 @@ primitives =
138 (1, LFloatStr) total,
142 (1, LFloatStr) total,
139
143
140 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)
144 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)
141− (1, LFExp) total,
145+ (1, LFExp) total,
142 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)
146 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)
143 (1, LFLog) total,
147 (1, LFLog) total,
144 Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)
148 Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)
@@ -181,6 +185,7 @@ primitives =
181 (3, LNoOp) partial -- ahem
185 (3, LNoOp) partial -- ahem
182 ] ++ concatMap intOps [IT8, IT16, IT32, IT64, ITBig, ITNative]
186 ] ++ concatMap intOps [IT8, IT16, IT32, IT64, ITBig, ITNative]
183
187
188+intOps :: IntTy -> [Prim]
184intOps ity =
189intOps ity =
185 [ iCmp ity "lt" (bCmp ity (<)) LLt total
190 [ iCmp ity "lt" (bCmp ity (<)) LLt total
186 , iCmp ity "lte" (bCmp ity (<=)) LLe total
191 , iCmp ity "lte" (bCmp ity (<=)) LLe total
@@ -216,50 +221,67 @@ intTyName ITNative = "Int"
216intTyName ITBig = "BigInt"
221intTyName ITBig = "BigInt"
217intTyName sized = "B" ++ show (intTyWidth sized)
222intTyName sized = "B" ++ show (intTyWidth sized)
218
223
224+iCmp, iBinOp, iUnOp :: IntTy -> String -> ([Value] -> Maybe Value) -> (IntTy -> PrimFn) -> Totality -> Prim
219iCmp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) IType) 2 impl (2, irop ity) totality
225iCmp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) IType) 2 impl (2, irop ity) totality
220iBinOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) (intTyToConst ity)) 2 impl (2, irop ity) totality
226iBinOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) (intTyToConst ity)) 2 impl (2, irop ity) totality
221iUnOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty [intTyToConst ity] (intTyToConst ity)) 1 impl (1, irop ity) totality
227iUnOp 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
222iCoerce from to op impl irop =
230iCoerce from to op impl irop =
223 Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)
231 Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)
224 (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total
232 (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total
225
233
234+p_believeMe :: [a] -> Maybe a
226p_believeMe [_,_,x] = Just x
235p_believeMe [_,_,x] = Just x
227p_believeMe _ = Nothing
236p_believeMe _ = Nothing
228
237
238+iUn :: (Int -> Int) -> [Value] -> Maybe Value
229iUn op [VConstant (I x)] = Just $ VConstant (I (op x))
239iUn op [VConstant (I x)] = Just $ VConstant (I (op x))
230iUn _ _ = Nothing
240iUn _ _ = Nothing
231
241
242+iBin :: (Int -> Int -> Int) -> [Value] -> Maybe Value
232iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
243iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
233iBin _ _ = Nothing
244iBin _ _ = Nothing
234
245
246+bBin :: (Integer -> Integer -> Integer) -> [Value] -> Maybe Value
235bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))
247bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))
236bBin _ _ = Nothing
248bBin _ _ = Nothing
237
249
250+bBini :: (Integer -> Integer -> Int) -> [Value] -> Maybe Value
238bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))
251bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))
239bBini _ _ = Nothing
252bBini _ _ = Nothing
240
253
254+biBin :: (Int -> Int -> Bool) -> [Value] -> Maybe Value
241biBin op = iBin (\x y -> if (op x y) then 1 else 0)
255biBin op = iBin (\x y -> if (op x y) then 1 else 0)
256+
257+bbBin :: (Integer -> Integer -> Bool) -> [Value] -> Maybe Value
242bbBin op = bBini (\x y -> if (op x y) then 1 else 0)
258bbBin op = bBini (\x y -> if (op x y) then 1 else 0)
243
259
260+fBin :: (Double -> Double -> Double) -> [Value] -> Maybe Value
244fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))
261fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))
245fBin _ _ = Nothing
262fBin _ _ = Nothing
246
263
264+bfBin :: (Double -> Double -> Bool) -> [Value] -> Maybe Value
247bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in
265bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in
248 Just $ VConstant (I i)
266 Just $ VConstant (I i)
249bfBin _ _ = Nothing
267bfBin _ _ = Nothing
250
268
269+bcBin :: (Char -> Char -> Bool) -> [Value] -> Maybe Value
251bcBin op [VConstant (Ch x), VConstant (Ch y)] = let i = (if op x y then 1 else 0) in
270bcBin op [VConstant (Ch x), VConstant (Ch y)] = let i = (if op x y then 1 else 0) in
252 Just $ VConstant (I i)
271 Just $ VConstant (I i)
253bcBin _ _ = Nothing
272bcBin _ _ = Nothing
254
273
274+bsBin :: (String -> String -> Bool) -> [Value] -> Maybe Value
255−bsBin op [VConstant (Str x), VConstant (Str y)]
275+bsBin op [VConstant (Str x), VConstant (Str y)]
256 = let i = (if op x y then 1 else 0) in
276 = let i = (if op x y then 1 else 0) in
257 Just $ VConstant (I i)
277 Just $ VConstant (I i)
258bsBin _ _ = Nothing
278bsBin _ _ = Nothing
259
279
280+sBin :: (String -> String -> String) -> [Value] -> Maybe Value
260sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
281sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
261sBin _ _ = Nothing
282sBin _ _ = Nothing
262
283
284+bsrem :: IntTy -> [Value] -> Maybe Value
263bsrem IT8 [VConstant (B8 x), VConstant (B8 y)]
285bsrem IT8 [VConstant (B8 x), VConstant (B8 y)]
264 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8)))
286 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8)))
265bsrem IT16 [VConstant (B16 x), VConstant (B16 y)]
287bsrem IT16 [VConstant (B16 x), VConstant (B16 y)]
@@ -271,6 +293,7 @@ bsrem IT64 [VConstant (B64 x), VConstant (B64 y)]
271bsrem ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `rem` y))
293bsrem ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `rem` y))
272bsrem _ _ = Nothing
294bsrem _ _ = Nothing
273
295
296+bsdiv :: IntTy -> [Value] -> Maybe Value
274bsdiv IT8 [VConstant (B8 x), VConstant (B8 y)]
297bsdiv IT8 [VConstant (B8 x), VConstant (B8 y)]
275 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8)))
298 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8)))
276bsdiv IT16 [VConstant (B16 x), VConstant (B16 y)]
299bsdiv IT16 [VConstant (B16 x), VConstant (B16 y)]
@@ -282,6 +305,7 @@ bsdiv IT64 [VConstant (B64 x), VConstant (B64 y)]
282bsdiv ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `div` y))
305bsdiv ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `div` y))
283bsdiv _ _ = Nothing
306bsdiv _ _ = Nothing
284
307
308+bashr :: IntTy -> [Value] -> Maybe Value
285bashr IT8 [VConstant (B8 x), VConstant (B8 y)]
309bashr IT8 [VConstant (B8 x), VConstant (B8 y)]
286 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8)))
310 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8)))
287bashr IT16 [VConstant (B16 x), VConstant (B16 y)]
311bashr 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
320bCmp ITNative op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
344bCmp ITNative op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (if (op x y) then 1 else 0))
321bCmp _ _ _ = Nothing
345bCmp _ _ _ = Nothing
322
346
347+toInt :: Integral a => IntTy -> a -> Value
323toInt IT8 x = VConstant (B8 (fromIntegral x))
348toInt IT8 x = VConstant (B8 (fromIntegral x))
324toInt IT16 x = VConstant (B16 (fromIntegral x))
349toInt IT16 x = VConstant (B16 (fromIntegral x))
325toInt IT32 x = VConstant (B32 (fromIntegral x))
350toInt IT32 x = VConstant (B32 (fromIntegral x))
@@ -327,6 +352,7 @@ toInt IT64 x = VConstant (B64 (fromIntegral x))
327toInt ITBig x = VConstant (BI (fromIntegral x))
352toInt ITBig x = VConstant (BI (fromIntegral x))
328toInt ITNative x = VConstant (I (fromIntegral x))
353toInt ITNative x = VConstant (I (fromIntegral x))
329
354
355+intToInt :: IntTy -> IntTy -> [Value] -> Maybe Value
330intToInt IT8 out [VConstant (B8 x)] = Just $ toInt out x
356intToInt IT8 out [VConstant (B8 x)] = Just $ toInt out x
331intToInt IT16 out [VConstant (B16 x)] = Just $ toInt out x
357intToInt IT16 out [VConstant (B16 x)] = Just $ toInt out x
332intToInt IT32 out [VConstant (B32 x)] = Just $ toInt out x
358intToInt IT32 out [VConstant (B32 x)] = Just $ toInt out x
@@ -335,12 +361,14 @@ intToInt ITBig out [VConstant (BI x)] = Just $ toInt out x
335intToInt ITNative out [VConstant (I x)] = Just $ toInt out x
361intToInt ITNative out [VConstant (I x)] = Just $ toInt out x
336intToInt _ _ _ = Nothing
362intToInt _ _ _ = Nothing
337
363
364+zext :: IntTy -> IntTy -> [Value] -> Maybe Value
338zext from ITBig val = intToInt from ITBig val
365zext from ITBig val = intToInt from ITBig val
339zext ITBig _ _ = Nothing
366zext ITBig _ _ = Nothing
340zext from to val
367zext from to val
341 | intTyWidth from < intTyWidth to = intToInt from to val
368 | intTyWidth from < intTyWidth to = intToInt from to val
342zext _ _ _ = Nothing
369zext _ _ _ = Nothing
343
370
371+sext :: IntTy -> IntTy -> [Value] -> Maybe Value
344sext IT8 out [VConstant (B8 x)] = Just $ toInt out (fromIntegral x :: Int8)
372sext IT8 out [VConstant (B8 x)] = Just $ toInt out (fromIntegral x :: Int8)
345sext IT16 out [VConstant (B16 x)] = Just $ toInt out (fromIntegral x :: Int16)
373sext IT16 out [VConstant (B16 x)] = Just $ toInt out (fromIntegral x :: Int16)
346sext IT32 out [VConstant (B32 x)] = Just $ toInt out (fromIntegral x :: Int32)
374sext 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)
348sext ITBig _ _ = Nothing
376sext ITBig _ _ = Nothing
349sext from to val = intToInt from to val
377sext from to val = intToInt from to val
350
378
379+trunc :: IntTy -> IntTy -> [Value] -> Maybe Value
351trunc ITBig to val = intToInt ITBig to val
380trunc ITBig to val = intToInt ITBig to val
352trunc _ ITBig _ = Nothing
381trunc _ ITBig _ = Nothing
353trunc from to val | intTyWidth from > intTyWidth to = intToInt from to val
382trunc from to val | intTyWidth from > intTyWidth to = intToInt from to val
@@ -362,25 +391,31 @@ getInt [VConstant (I x)] = Just . toInteger $ x
362getInt [VConstant (BI x)] = Just x
391getInt [VConstant (BI x)] = Just x
363getInt _ = Nothing
392getInt _ = Nothing
364
393
394+intToStr :: [Value] -> Maybe Value
365intToStr val | Just i <- getInt val = Just $ VConstant (Str (show i))
395intToStr val | Just i <- getInt val = Just $ VConstant (Str (show i))
366intToStr _ = Nothing
396intToStr _ = Nothing
367
397
398+strToInt :: IntTy -> [Value] -> Maybe Value
368strToInt ity [VConstant (Str x)] = case reads x of
399strToInt ity [VConstant (Str x)] = case reads x of
369 [(n,"")] -> Just $ toInt ity (n :: Integer)
400 [(n,"")] -> Just $ toInt ity (n :: Integer)
370 _ -> Just $ VConstant (I 0)
401 _ -> Just $ VConstant (I 0)
371strToInt _ _ = Nothing
402strToInt _ _ = Nothing
372
403
404+intToFloat :: [Value] -> Maybe Value
373intToFloat val | Just i <- getInt val = Just $ VConstant (Fl (fromIntegral i))
405intToFloat val | Just i <- getInt val = Just $ VConstant (Fl (fromIntegral i))
374intToFloat _ = Nothing
406intToFloat _ = Nothing
375
407
408+floatToInt :: IntTy -> [Value] -> Maybe Value
376floatToInt ity [VConstant (Fl x)] = Just $ toInt ity (truncate x :: Integer)
409floatToInt ity [VConstant (Fl x)] = Just $ toInt ity (truncate x :: Integer)
377floatToInt _ _ = Nothing
410floatToInt _ _ = Nothing
378
411
412+c_intToChar :: [Value] -> Maybe Value
379c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))
413c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))
380c_intToChar _ = Nothing
414c_intToChar _ = Nothing
381c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))
415c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))
382c_charToInt _ = Nothing
416c_charToInt _ = Nothing
383
417
418+c_floatToStr :: [Value] -> Maybe Value
384c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
419c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
385c_floatToStr _ = Nothing
420c_floatToStr _ = Nothing
386c_strToFloat [VConstant (Str x)] = case reads x of
421c_strToFloat [VConstant (Str x)] = case reads x of
@@ -388,9 +423,11 @@ c_strToFloat [VConstant (Str x)] = case reads x of
388 _ -> Just $ VConstant (Fl 0)
423 _ -> Just $ VConstant (Fl 0)
389c_strToFloat _ = Nothing
424c_strToFloat _ = Nothing
390
425
426+p_fPrim :: (Double -> Double) -> [Value] -> Maybe Value
391p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))
427p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))
392p_fPrim f _ = Nothing
428p_fPrim f _ = Nothing
393
429
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
394p_floatExp = p_fPrim exp
431p_floatExp = p_fPrim exp
395p_floatLog = p_fPrim log
432p_floatLog = p_fPrim log
396p_floatSin = p_fPrim sin
433p_floatSin = p_fPrim sin
@@ -403,13 +440,14 @@ p_floatSqrt = p_fPrim sqrt
403p_floatFloor = p_fPrim (fromInteger . floor)
440p_floatFloor = p_fPrim (fromInteger . floor)
404p_floatCeil = p_fPrim (fromInteger . ceiling)
441p_floatCeil = p_fPrim (fromInteger . ceiling)
405
442
443+p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev :: [Value] -> Maybe Value
406p_strLen [VConstant (Str xs)] = Just $ VConstant (I (length xs))
444p_strLen [VConstant (Str xs)] = Just $ VConstant (I (length xs))
407p_strLen _ = Nothing
445p_strLen _ = Nothing
408p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)
446p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)
409p_strHead _ = Nothing
447p_strHead _ = Nothing
410p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)
448p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)
411p_strTail _ = Nothing
449p_strTail _ = Nothing
412−p_strIndex [VConstant (Str xs), VConstant (I i)]
450+p_strIndex [VConstant (Str xs), VConstant (I i)]
413 | i < length xs = Just $ VConstant (Ch (xs!!i))
451 | i < length xs = Just $ VConstant (Ch (xs!!i))
414p_strIndex _ = Nothing
452p_strIndex _ = Nothing
415p_strCons [VConstant (Ch x), VConstant (Str xs)] = Just $ VConstant (Str (x:xs))
453p_strCons [VConstant (Ch x), VConstant (Str xs)] = Just $ VConstant (Str (x:xs))
@@ -417,17 +455,18 @@ p_strCons _ = Nothing
417p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))
455p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))
418p_strRev _ = Nothing
456p_strRev _ = Nothing
419
457
458+p_cantreduce :: a -> Maybe b
420p_cantreduce _ = Nothing
459p_cantreduce _ = Nothing
421
460
422elabPrim :: Prim -> Idris ()
461elabPrim :: Prim -> Idris ()
423−elabPrim (Prim n ty i def sc tot)
462+elabPrim (Prim n ty i def sc tot)
424 = do updateContext (addOperator n ty i def)
463 = do updateContext (addOperator n ty i def)
425 setTotality n tot
464 setTotality n tot
426 i <- getIState
465 i <- getIState
427 putIState i { idris_scprims = (n, sc) : idris_scprims i }
466 putIState i { idris_scprims = (n, sc) : idris_scprims i }
428
467
429elabPrims :: Idris ()
468elabPrims :: Idris ()
430−elabPrims = do mapM_ (elabDecl EAll toplevel)
469+elabPrims = do mapM_ (elabDecl EAll toplevel)
431 (map (PData "" defaultSyntax (FC "builtin" 0) False)
470 (map (PData "" defaultSyntax (FC "builtin" 0) False)
432 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
471 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
433 mapM_ elabPrim primitives
472 mapM_ elabPrim primitives
test/test028/expectednew file+1
@@ -0,0 +1 @@
1+hello, world!
test/test028/runnew file+4
@@ -0,0 +1,4 @@
1+#!/bin/bash
2+idris $@ test028.idr -o test028
3+./test028
4+rm -f test028 test028.ibc
test/test028/test028.idrnew file+5
@@ -0,0 +1,5 @@
1+{--}
2+module Main
3+--
4+main : IO ()
5+main = print "hello, world!"