8848ad4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge remote-tracking branch 'upstream/master'

commit8848ad476d1aefaeae09fa3551b8893a16562932 authorDominic Mulligan <dominic.p.mulligan@googlemail.com> dateFri 24 Feb 2012, 14:34 (15 years ago) parent651d3af 2cde01c

3 files changed+12−7

compare with master

unifiedsplit

idris.cabal+1−1 src/Core/Evaluate.hs+6−6 src/Idris/Primitives.hs+5

idris.cabal+1−1

@@ -67,7 +67,7 @@ Executable idris

6767

6868 Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,

6969 containers, process, transformers, filepath, directory,

70− binary, bytestring, epic>=0.9.2

70+ binary, bytestring, epic>=0.9.2.1

7171

7272 Extensions: MultiParamTypeClasses, FunctionalDependencies,

7373 FlexibleInstances, TemplateHaskell

src/Core/Evaluate.hs+6−6

@@ -165,7 +165,7 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

165165 ev ntimes_in stk top env (P Ref n ty)

166166 | (True, ntimes) <- usable n ntimes_in

167167 = do let val = lookupDefAcc Nothing n atRepl ctxt

168− step maxred

168+ when (not atRepl) $ step maxred

169169 case val of

170170 [(Function _ tm, Public)] ->

171171 ev ntimes (n:stk) True env tm

@@ -184,24 +184,24 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

184184 | otherwise = return $ VV i

185185 ev ntimes stk top env (Bind n (Let t v) sc)

186186 = do v' <- ev ntimes stk top env v --(finalise v)

187− step maxred

187+ when (not atRepl) $ step maxred

188188 sc' <- ev ntimes stk top (v' : env) sc

189189 wknV (-1) sc'

190190 ev ntimes stk top env (Bind n (NLet t v) sc)

191191 = do t' <- ev ntimes stk top env (finalise t)

192192 v' <- ev ntimes stk top env (finalise v)

193− step maxred

193+ when (not atRepl) $ step maxred

194194 sc' <- ev ntimes stk top (v' : env) sc

195195 return $ VBind n (Let t' v') (\x -> return sc')

196196 ev ntimes stk top env (Bind n b sc)

197197 = do b' <- vbind env b

198− step maxred

198+ when (not atRepl) $ step maxred

199199 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)

200200 where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t

201201 ev ntimes stk top env (App f a)

202202 = do f' <- ev ntimes stk top env f

203203 a' <- ev ntimes stk False env a

204− step maxred

204+ when (not atRepl) $ step maxred

205205 evApply ntimes stk top env [a'] f'

206206 ev ntimes stk top env (Constant c) = return $ VConstant c

207207 ev ntimes stk top env Erased = return VErased

@@ -209,7 +209,7 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

209209

210210 evApply ntimes stk top env args (VApp f a) =

211211 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

213213 apply ntimes stk top env f args

214214

215215 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)]

4545charToInt x = x

4646intToChar x = x

4747intToBigInt x = foreign_ tyBigInt "intToBigInt" [(x, tyInt)]

48+bigIntToInt x = foreign_ tyInt "bigIntToInt" [(x, tyBigInt)]

4849strToBigInt x = foreign_ tyBigInt "strToBig" [(x, tyString)]

4950bigIntToStr x = foreign_ tyString "bigToStr" [(x, tyBigInt)]

5051strToFloat x = foreign_ tyFloat "strToFloat" [(x, tyString)]

@@ -158,6 +159,8 @@ primitives =

158159 ([E.name "x"], intToChar (fun "x")) total,

159160 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)

160161 ([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,

161164 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)

162165 ([E.name "x"], strToBigInt (fun "x")) total,

163166 Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)

@@ -257,6 +260,8 @@ c_charToInt _ = Nothing

257260

258261c_intToBigInt [VConstant (I x)] = Just $ VConstant (BI (fromIntegral x))

259262c_intToBigInt _ = Nothing

263+c_bigIntToInt [VConstant (BI x)] = Just $ VConstant (I (fromInteger x))

264+c_bigIntToInt _ = Nothing

260265

261266c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x))

262267c_bigIntToStr _ = Nothing