git.iko.soy/Idris-dev
on master help sign in
Merge remote-tracking branch 'upstream/master'
8848ad4Dominic Mulligan
idris.cabal+1−1
compare with master
unifiedsplit
@@ -67,7 +67,7 @@ Executable idris
67
67
68 Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,
68 Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,
69 containers, process, transformers, filepath, directory,
69 containers, process, transformers, filepath, directory,
70− binary, bytestring, epic>=0.9.2
70+ binary, bytestring, epic>=0.9.2.1
71
71
72 Extensions: MultiParamTypeClasses, FunctionalDependencies,
72 Extensions: MultiParamTypeClasses, FunctionalDependencies,
73 FlexibleInstances, TemplateHaskell
73 FlexibleInstances, TemplateHaskell
src/Core/Evaluate.hs+6−6
@@ -165,7 +165,7 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
165 ev ntimes_in stk top env (P Ref n ty)
165 ev ntimes_in stk top env (P Ref n ty)
166 | (True, ntimes) <- usable n ntimes_in
166 | (True, ntimes) <- usable n ntimes_in
167 = do let val = lookupDefAcc Nothing n atRepl ctxt
167 = do let val = lookupDefAcc Nothing n atRepl ctxt
168− step maxred
168+ when (not atRepl) $ step maxred
169 case val of
169 case val of
170 [(Function _ tm, Public)] ->
170 [(Function _ tm, Public)] ->
171 ev ntimes (n:stk) True env tm
171 ev ntimes (n:stk) True env tm
@@ -184,24 +184,24 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
184 | otherwise = return $ VV i
184 | otherwise = return $ VV i
185 ev ntimes stk top env (Bind n (Let t v) sc)
185 ev ntimes stk top env (Bind n (Let t v) sc)
186 = do v' <- ev ntimes stk top env v --(finalise v)
186 = do v' <- ev ntimes stk top env v --(finalise v)
187− step maxred
187+ when (not atRepl) $ step maxred
188 sc' <- ev ntimes stk top (v' : env) sc
188 sc' <- ev ntimes stk top (v' : env) sc
189 wknV (-1) sc'
189 wknV (-1) sc'
190 ev ntimes stk top env (Bind n (NLet t v) sc)
190 ev ntimes stk top env (Bind n (NLet t v) sc)
191 = do t' <- ev ntimes stk top env (finalise t)
191 = do t' <- ev ntimes stk top env (finalise t)
192 v' <- ev ntimes stk top env (finalise v)
192 v' <- ev ntimes stk top env (finalise v)
193− step maxred
193+ when (not atRepl) $ step maxred
194 sc' <- ev ntimes stk top (v' : env) sc
194 sc' <- ev ntimes stk top (v' : env) sc
195 return $ VBind n (Let t' v') (\x -> return sc')
195 return $ VBind n (Let t' v') (\x -> return sc')
196 ev ntimes stk top env (Bind n b sc)
196 ev ntimes stk top env (Bind n b sc)
197 = do b' <- vbind env b
197 = do b' <- vbind env b
198− step maxred
198+ when (not atRepl) $ step maxred
199 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)
199 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)
200 where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
200 where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
201 ev ntimes stk top env (App f a)
201 ev ntimes stk top env (App f a)
202 = do f' <- ev ntimes stk top env f
202 = do f' <- ev ntimes stk top env f
203 a' <- ev ntimes stk False env a
203 a' <- ev ntimes stk False env a
204− step maxred
204+ when (not atRepl) $ step maxred
205 evApply ntimes stk top env [a'] f'
205 evApply ntimes stk top env [a'] f'
206 ev ntimes stk top env (Constant c) = return $ VConstant c
206 ev ntimes stk top env (Constant c) = return $ VConstant c
207 ev ntimes stk top env Erased = return VErased
207 ev ntimes stk top env Erased = return VErased
@@ -209,7 +209,7 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
209
209
210 evApply ntimes stk top env args (VApp f a) =
210 evApply ntimes stk top env args (VApp f a) =
211 evApply ntimes stk top env (a:args) f
211 evApply ntimes stk top env (a:args) f
212− evApply ntimes stk top env args f = do step maxred
212+ evApply ntimes stk top env args f = do when (not atRepl) $ step maxred
213 apply ntimes stk top env f args
213 apply ntimes stk top env f args
214
214
215 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
215 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
src/Idris/Primitives.hs+5
@@ -45,6 +45,7 @@ intToStr x = foreign_ tyString "intToStr" [(x, tyInt)]
45charToInt x = x
45charToInt x = x
46intToChar x = x
46intToChar x = x
47intToBigInt x = foreign_ tyBigInt "intToBigInt" [(x, tyInt)]
47intToBigInt x = foreign_ tyBigInt "intToBigInt" [(x, tyInt)]
48+bigIntToInt x = foreign_ tyInt "bigIntToInt" [(x, tyBigInt)]
48strToBigInt x = foreign_ tyBigInt "strToBig" [(x, tyString)]
49strToBigInt x = foreign_ tyBigInt "strToBig" [(x, tyString)]
49bigIntToStr x = foreign_ tyString "bigToStr" [(x, tyBigInt)]
50bigIntToStr x = foreign_ tyString "bigToStr" [(x, tyBigInt)]
50strToFloat x = foreign_ tyFloat "strToFloat" [(x, tyString)]
51strToFloat x = foreign_ tyFloat "strToFloat" [(x, tyString)]
@@ -158,6 +159,8 @@ primitives =
158 ([E.name "x"], intToChar (fun "x")) total,
159 ([E.name "x"], intToChar (fun "x")) total,
159 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)
160 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)
160 ([E.name "x"], intToBigInt (fun "x")) total,
161 ([E.name "x"], intToBigInt (fun "x")) total,
162+ Prim (UN "prim__bigIntToInt") (ty [BIType] IType) 1 (c_bigIntToInt)
163+ ([E.name "x"], bigIntToInt (fun "x")) total,
161 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)
164 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)
162 ([E.name "x"], strToBigInt (fun "x")) total,
165 ([E.name "x"], strToBigInt (fun "x")) total,
163 Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)
166 Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)
@@ -257,6 +260,8 @@ c_charToInt _ = Nothing
257
260
258c_intToBigInt [VConstant (I x)] = Just $ VConstant (BI (fromIntegral x))
261c_intToBigInt [VConstant (I x)] = Just $ VConstant (BI (fromIntegral x))
259c_intToBigInt _ = Nothing
262c_intToBigInt _ = Nothing
263+c_bigIntToInt [VConstant (BI x)] = Just $ VConstant (I (fromInteger x))
264+c_bigIntToInt _ = Nothing
260
265
261c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x))
266c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x))
262c_bigIntToStr _ = Nothing
267c_bigIntToStr _ = Nothing