822328b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1038 from david-christiansen/typed-lazy-executor

822328bEdwin Brady13 years ago

.travis.yml+2

@@ -6,6 +6,8 @@ before_install:

6 - sudo apt-get install -qq libghc-unordered-containers-dev libghc-mtl-dev libghc-network-dev libghc-xml-dev libghc-transformers-dev libghc-text-dev libghc-utf8-string-dev libghc-vector-dev libghc-split-dev libghc-ansi-terminal-dev libghc-ansi-wl-pprint-dev

7 # trifecta dependencies

8 - sudo apt-get install -qq libghc-blaze-builder-dev libghc-blaze-html-dev libghc-data-lens-dev libghc-bifunctors-dev libghc-hashable-dev libghc-semigroups-dev libghc-semigroupoids-dev libghc-parallel-dev libghc-comonad-dev libghc-terminfo-dev libghc-keys-dev

9+ # test dependency

10+ - sudo apt-get install -qq expect

9install:

11install:

10 - cabal install -f FFI -f LLVM --only-dependencies --enable-tests

12 - cabal install -f FFI -f LLVM --only-dependencies --enable-tests

11before_script:

13before_script:

src/Idris/Core/Execute.hs+97−135

@@ -47,11 +47,8 @@ readMay s = case reads s of

48data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show

50−data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs

51− , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness

52− , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad

53− , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad

50+newtype ExecState = ExecState { exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad

54− }

51+ }

56data ExecVal = EP NameType Name ExecVal

53data ExecVal = EP NameType Name ExecVal

57 | EV Int

54 | EV Int

@@ -61,20 +58,20 @@ data ExecVal = EP NameType Name ExecVal

61 | EErased

58 | EErased

62 | EConstant Const

59 | EConstant Const

63 | forall a. EPtr (Ptr a)

60 | forall a. EPtr (Ptr a)

64− | EThunk Int

61+ | EThunk Context ExecEnv Term

65 | EHandle Handle

62 | EHandle Handle

67instance Show ExecVal where

64instance Show ExecVal where

68− show (EP _ n _) = show n

65+ show (EP _ n _) = show n

69− show (EV i) = "!!V" ++ show i ++ "!!"

66+ show (EV i) = "!!V" ++ show i ++ "!!"

70− show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"

67+ show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"

71− show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"

68+ show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"

72− show (EType _) = "Type"

69+ show (EType _) = "Type"

73− show EErased = "[__]"

70+ show EErased = "[__]"

74− show (EConstant c) = show c

71+ show (EConstant c) = show c

75− show (EPtr p) = "<<ptr " ++ show p ++ ">>"

72+ show (EPtr p) = "<<ptr " ++ show p ++ ">>"

76− show (EThunk i) = "<<thunk " ++ show i ++ ">>"

73+ show (EThunk _ env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"

77− show (EHandle h) = "<<handle " ++ show h ++ ">>"

74+ show (EHandle h) = "<<handle " ++ show h ++ ">>"

79toTT :: ExecVal -> Exec Term

76toTT :: ExecVal -> Exec Term

80toTT (EP nt n ty) = (P nt n) <$> (toTT ty)

77toTT (EP nt n ty) = (P nt n) <$> (toTT ty)

@@ -82,22 +79,25 @@ toTT (EV i) = return $ V i

82toTT (EBind n b body) = do body' <- body $ EP Bound n EErased

79toTT (EBind n b body) = do body' <- body $ EP Bound n EErased

83 b' <- fixBinder b

80 b' <- fixBinder b

84 Bind n b' <$> toTT body'

81 Bind n b' <$> toTT body'

85− where fixBinder (Lam t) = Lam <$> toTT t

82+ where fixBinder (Lam t) = Lam <$> toTT t

86− fixBinder (Pi t) = Pi <$> toTT t

83+ fixBinder (Pi t) = Pi <$> toTT t

87− fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

84+ fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

88− fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

85+ fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

89− fixBinder (Hole t) = Hole <$> toTT t

86+ fixBinder (Hole t) = Hole <$> toTT t

90 fixBinder (GHole i t) = GHole i <$> toTT t

87 fixBinder (GHole i t) = GHole i <$> toTT t

91− fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2

88+ fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2

92− fixBinder (PVar t) = PVar <$> toTT t

89+ fixBinder (PVar t) = PVar <$> toTT t

93− fixBinder (PVTy t) = PVTy <$> toTT t

90+ fixBinder (PVTy t) = PVTy <$> toTT t

94toTT (EApp e1 e2) = do e1' <- toTT e1

91toTT (EApp e1 e2) = do e1' <- toTT e1

95 e2' <- toTT e2

92 e2' <- toTT e2

96 return $ App e1' e2'

93 return $ App e1' e2'

97toTT (EType u) = return $ TType u

94toTT (EType u) = return $ TType u

98toTT EErased = return Erased

95toTT EErased = return Erased

99toTT (EConstant c) = return (Constant c)

96toTT (EConstant c) = return (Constant c)

100−toTT (EThunk i) = return (P (DCon 0 0) (sMN i "THUNK") Erased) --(force i) >>= toTT

97+toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env

98+ return $ normalise ctxt env' tm

99+ where toBinder (n, v) = do v' <- toTT v

100+ return (n, Let Erased v')

101toTT (EHandle _) = return Erased

102

103unApplyV :: ExecVal -> (ExecVal, [ExecVal])

@@ -111,7 +111,7 @@ mkEApp f (a:args) = mkEApp (EApp f a) args

111

112initState :: Idris ExecState

113initState = do ist <- getIState

114− return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)

114+ return $ ExecState (idris_dynamic_libs ist)

115

116type Exec = ErrorT String (StateT ExecState IO)

117

@@ -130,45 +130,13 @@ execFail = throwError

130execIO :: IO a -> Exec a

131execIO = lift . lift

132

133−delay :: ExecEnv -> Context -> Term -> Exec ExecVal

134−delay env ctxt tm =

135− do st <- getExecState

136− let i = exec_next_thunk st

137− putExecState $ st { exec_thunks = M.insert i (Delayed env ctxt tm) (exec_thunks st)

138− , exec_next_thunk = exec_next_thunk st + 1

139− }

140− return $ EThunk i

141−

142−force :: Int -> Exec ExecVal

143−force i = do st <- getExecState

144− case M.lookup i (exec_thunks st) of

145− Just (Delayed env ctxt tm) -> do tm' <- doExec env ctxt tm

146− case tm' of

147− EThunk i ->

148− do res <- force i

149− update res i

150− return res

151− _ -> do update tm' i

152− return tm'

153− Just (Forced tm) -> return tm

154− Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"

155− where update :: ExecVal -> Int -> Exec ()

156− update tm i = do est <- getExecState

157− putExecState $ est { exec_thunks = M.insert i (Forced tm) (exec_thunks est) }

158−

159−tryForce :: ExecVal -> Exec ExecVal

160−tryForce (EThunk i) = force i

161−tryForce tm = return tm

162−

163−debugThunks :: Exec ()

164−debugThunks = do st <- getExecState

165− execIO $ putStrLn (take 4000 (show (exec_thunks st)))

166

133

167execute :: Term -> Idris Term

134execute :: Term -> Idris Term

168execute tm = do est <- initState

135execute tm = do est <- initState

169 ctxt <- getContext

136 ctxt <- getContext

170− res <- lift . lift $ flip runExec est $ do res <- doExec [] ctxt tm

137+ res <- lift . lift . flip runExec est $

138+ do res <- doExec [] ctxt tm

171− toTT res

139+ toTT res

172 case res of

140 case res of

173 Left err -> fail err

141 Left err -> fail err

174 Right tm' -> return tm'

142 Right tm' -> return tm'

@@ -208,7 +176,18 @@ doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined

208doExec env ctxt tm@(Bind n b body) = return $

176doExec env ctxt tm@(Bind n b body) = return $

209 EBind n (fmap (\_->EErased) b)

177 EBind n (fmap (\_->EErased) b)

210 (\arg -> doExec ((n, arg):env) ctxt body)

178 (\arg -> doExec ((n, arg):env) ctxt body)

211−doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)

179+doExec env ctxt a@(App _ _) =

180+ do let (f, args) = unApply a

181+ f' <- doExec env ctxt f

182+ args' <- case f' of

183+ (EP _ d _) | d == delay ->

184+ case args of

185+ [t,a,tm] -> do t' <- doExec env ctxt t

186+ a' <- doExec env ctxt a

187+ return [t', a', EThunk ctxt env tm]

188+ _ -> mapM (doExec env ctxt) args -- partial applications are fine to evaluate

189+ fun' -> do mapM (doExec env ctxt) args

190+ execApp env ctxt f' args'

212doExec env ctxt (Constant c) = return (EConstant c)

191doExec env ctxt (Constant c) = return (EConstant c)

213doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in

192doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in

214 doExec env ctxt ((x:xs) !! i)

193 doExec env ctxt ((x:xs) !! i)

@@ -216,55 +195,39 @@ doExec env ctxt Erased = return EErased

216doExec env ctxt Impossible = fail "Tried to execute an impossible case"

195doExec env ctxt Impossible = fail "Tried to execute an impossible case"

217doExec env ctxt (TType u) = return (EType u)

196doExec env ctxt (TType u) = return (EType u)

218

197

219−execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal

198+

220−execApp env ctxt (f, args) = do newF <- doExec env ctxt f

221− laziness <- (++ repeat False) <$> (getLaziness newF)

222− newArgs <- mapM argExec (zip args laziness)

223− res <- execApp' env ctxt newF newArgs

224− return res

225− where getLaziness (EP _ l _) | l == sUN "lazy" = return [False, True]

226− getLaziness (EP _ n _) = do est <- getExecState

227− let argInfo = exec_implicits est

228− case lookupCtxtName n argInfo of

229− [] -> return (repeat False)

230− [ps] -> return $ map lazyarg (snd ps)

231− many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)

232− getLaziness _ = return (repeat False) -- ok due to zip above

233− argExec :: (Term, Bool) -> Exec ExecVal

234− argExec (tm, False) = doExec env ctxt tm

235− argExec (tm, True) = delay env ctxt tm

236−

237−

238−execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal

199+execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal

239−execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls

200+execApp env ctxt v [] = return v -- no args is just a constant! can result from function calls

201+execApp env ctxt (EP _ f _) (t:a:delayed:rest)

202+ | f == force

203+ , (_, [_, _, EThunk tmCtxt tmEnv tm]) <- unApplyV delayed =

204+ do tm' <- doExec tmEnv tmCtxt tm

205+ execApp env ctxt tm' rest

240−execApp' env ctxt (EP _ fp _) (ty:action:rest)

206+execApp env ctxt (EP _ fp _) (ty:action:rest)

241 | fp == upio,

207 | fp == upio,

242 (prim__IO, [_, v]) <- unApplyV action

208 (prim__IO, [_, v]) <- unApplyV action

243− = execApp' env ctxt v rest

209+ = execApp env ctxt v rest

244

210

245−execApp' env ctxt (EP _ fp _) args@(_:_:v:k:rest)

211+execApp env ctxt (EP _ fp _) args@(_:_:v:k:rest)

246 | fp == piobind,

212 | fp == piobind,

247 (prim__IO, [_, v']) <- unApplyV v =

213 (prim__IO, [_, v']) <- unApplyV v =

248− do v'' <- tryForce v'

249− res <- execApp' env ctxt k [v''] >>= tryForce

214+ do res <- execApp env ctxt k [v']

250− execApp' env ctxt res rest

215+ execApp env ctxt res rest

251−execApp' env ctxt con@(EP _ fp _) args@(tp:v:rest)

216+execApp env ctxt con@(EP _ fp _) args@(tp:v:rest)

252− | fp == pioret =

253− do v' <- tryForce v

254− execApp' env ctxt (mkEApp con [tp, v']) rest

217+ | fp == pioret = execApp env ctxt (mkEApp con [tp, v]) rest

255

218

256-- Special cases arising from not having access to the C RTS in the interpreter

219-- Special cases arising from not having access to the C RTS in the interpreter

257−execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str arg):_:rest)

220+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str arg):_:rest)

258 | fp == mkfprim,

221 | fp == mkfprim,

259 Just (FFun "putStr" _ _) <- foreignFromTT fn

222 Just (FFun "putStr" _ _) <- foreignFromTT fn

260 = do execIO (putStr arg)

223 = do execIO (putStr arg)

261− execApp' env ctxt ioUnit rest

224+ execApp env ctxt ioUnit rest

262−execApp' env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)

225+execApp env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)

263 | fp == mkfprim,

226 | fp == mkfprim,

264 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn

227 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn

265 = do contents <- execIO $ hGetLine h

228 = do contents <- execIO $ hGetLine h

266− execApp' env ctxt (EConstant (Str (contents ++ "\n"))) rest

229+ execApp env ctxt (EConstant (Str (contents ++ "\n"))) rest

267−execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

230+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

268 | fp == mkfprim,

231 | fp == mkfprim,

269 Just (FFun "fileOpen" _ _) <- foreignFromTT fn

232 Just (FFun "fileOpen" _ _) <- foreignFromTT fn

270 = do f <- execIO $

233 = do f <- execIO $

@@ -283,53 +246,53 @@ execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

283 in return $ Right (ioWrap (EPtr nullPtr), tail rest))

246 in return $ Right (ioWrap (EPtr nullPtr), tail rest))

284 case f of

247 case f of

285 Left err -> execFail err

248 Left err -> execFail err

286− Right (res, rest) -> execApp' env ctxt res rest

249+ Right (res, rest) -> execApp env ctxt res rest

287

250

288−execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

251+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

289 | fp == mkfprim,

252 | fp == mkfprim,

290 Just (FFun "fileEOF" _ _) <- foreignFromTT fn

253 Just (FFun "fileEOF" _ _) <- foreignFromTT fn

291 = do eofp <- execIO $ hIsEOF h

254 = do eofp <- execIO $ hIsEOF h

292 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))

255 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))

293− execApp' env ctxt res (tail rest)

256+ execApp env ctxt res (tail rest)

294

257

295−execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

258+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

296 | fp == mkfprim,

259 | fp == mkfprim,

297 Just (FFun "fileClose" _ _) <- foreignFromTT fn

260 Just (FFun "fileClose" _ _) <- foreignFromTT fn

298 = do execIO $ hClose h

261 = do execIO $ hClose h

299− execApp' env ctxt ioUnit (tail rest)

262+ execApp env ctxt ioUnit (tail rest)

300

263

301−execApp' env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)

264+execApp env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)

302 | fp == mkfprim,

265 | fp == mkfprim,

303 Just (FFun "isNull" _ _) <- foreignFromTT fn

266 Just (FFun "isNull" _ _) <- foreignFromTT fn

304 = let res = ioWrap . EConstant . I $

267 = let res = ioWrap . EConstant . I $

305 if p == nullPtr then 1 else 0

268 if p == nullPtr then 1 else 0

306− in execApp' env ctxt res (tail rest)

269+ in execApp env ctxt res (tail rest)

307

270

308-- Handles will be checked as null pointers sometimes - but if we got a

271-- Handles will be checked as null pointers sometimes - but if we got a

309-- real Handle, then it's valid, so just return 1.

272-- real Handle, then it's valid, so just return 1.

310−execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

273+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

311 | fp == mkfprim,

274 | fp == mkfprim,

312 Just (FFun "isNull" _ _) <- foreignFromTT fn

275 Just (FFun "isNull" _ _) <- foreignFromTT fn

313 = let res = ioWrap . EConstant . I $ 0

276 = let res = ioWrap . EConstant . I $ 0

314− in execApp' env ctxt res (tail rest)

277+ in execApp env ctxt res (tail rest)

315

278

316-- A foreign-returned char* has to be tested for NULL sometimes

279-- A foreign-returned char* has to be tested for NULL sometimes

317−execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str s):rest)

280+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str s):rest)

318 | fp == mkfprim,

281 | fp == mkfprim,

319 Just (FFun "isNull" _ _) <- foreignFromTT fn

282 Just (FFun "isNull" _ _) <- foreignFromTT fn

320 = let res = ioWrap . EConstant . I $ 0

283 = let res = ioWrap . EConstant . I $ 0

321− in execApp' env ctxt res (tail rest)

284+ in execApp env ctxt res (tail rest)

322

285

323-- Right now, there's no way to send command-line arguments to the executor,

286-- Right now, there's no way to send command-line arguments to the executor,

324-- so just return 0.

287-- so just return 0.

325−execApp' env ctxt (EP _ fp _) (_:fn:rest)

288+execApp env ctxt (EP _ fp _) (_:fn:rest)

326 | fp == mkfprim,

289 | fp == mkfprim,

327 Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn

290 Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn

328 = let res = ioWrap . EConstant . I $ 0

291 = let res = ioWrap . EConstant . I $ 0

329− in execApp' env ctxt res (tail rest)

292+ in execApp env ctxt res (tail rest)

330-- Throw away the 'World' argument to the foreign function

293-- Throw away the 'World' argument to the foreign function

331

294

332−execApp' env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

295+execApp env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

333 = case foreignFromTT fn of

296 = case foreignFromTT fn of

334 Just (FFun f argTs retT) | length xs >= length argTs ->

297 Just (FFun f argTs retT) | length xs >= length argTs ->

335 do let (args', xs') = (take (length argTs) xs, -- foreign args

298 do let (args', xs') = (take (length argTs) xs, -- foreign args

@@ -341,43 +304,41 @@ execApp' env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

341 Just r -> return (mkEApp r xs')

304 Just r -> return (mkEApp r xs')

342 Nothing -> return (mkEApp f args)

305 Nothing -> return (mkEApp f args)

343

306

344−execApp' env ctxt c@(EP (DCon _ arity) n _) args =

307+execApp env ctxt c@(EP (DCon _ arity) n _) args =

345− do args' <- mapM tryForce (take arity args)

308+ do let args' = take arity args

346 let restArgs = drop arity args

309 let restArgs = drop arity args

347− execApp' env ctxt (mkEApp c args') restArgs

310+ execApp env ctxt (mkEApp c args') restArgs

348

311

349−execApp' env ctxt c@(EP (TCon _ arity) n _) args =

312+execApp env ctxt c@(EP (TCon _ arity) n _) args =

350− do args' <- mapM tryForce (take arity args)

313+ do let args' = take arity args

351 let restArgs = drop arity args

314 let restArgs = drop arity args

352− execApp' env ctxt (mkEApp c args') restArgs

315+ execApp env ctxt (mkEApp c args') restArgs

353

316

354−execApp' env ctxt f@(EP _ n _) args =

317+execApp env ctxt f@(EP _ n _) args =

355 do let val = lookupDef n ctxt

318 do let val = lookupDef n ctxt

356 case val of

319 case val of

357 [Function _ tm] -> fail "should already have been eval'd"

320 [Function _ tm] -> fail "should already have been eval'd"

358 [TyDecl nt ty] -> return $ mkEApp f args

321 [TyDecl nt ty] -> return $ mkEApp f args

359 [Operator tp arity op] ->

322 [Operator tp arity op] ->

360 if length args >= arity

323 if length args >= arity

361− then do args' <- mapM tryForce $ take arity args

324+ then let args' = take arity args in

362− case getOp n args' of

325+ case getOp n args' of

363− Just res -> do r <- res

326+ Just res -> do r <- res

364− execApp' env ctxt r (drop arity args)

327+ execApp env ctxt r (drop arity args)

365− Nothing -> return (mkEApp f args)

328+ Nothing -> return (mkEApp f args)

366 else return (mkEApp f args)

329 else return (mkEApp f args)

367 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun

330 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun

368 do rhs <- doExec env ctxt tm

331 do rhs <- doExec env ctxt tm

369− execApp' env ctxt rhs args

332+ execApp env ctxt rhs args

370 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->

333 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->

371 do res <- execCase env ctxt ns sc args

334 do res <- execCase env ctxt ns sc args

372 return $ fromMaybe (mkEApp f args) res

335 return $ fromMaybe (mkEApp f args) res

373 thing -> return $ mkEApp f args

336 thing -> return $ mkEApp f args

374−execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg

337+execApp env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg

375− let (f', as) = unApplyV ret

338+ let (f', as) = unApplyV ret

376− execApp' env ctxt f' (as ++ args)

339+ execApp env ctxt f' (as ++ args)

377−execApp' env ctxt (EThunk i) args = do f <- force i

378− execApp' env ctxt f args

379−execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)

340+execApp env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp env ctxt f (args1 ++ args2)

380−execApp' env ctxt f args = return (mkEApp f args)

341+execApp env ctxt f args = return (mkEApp f args)

381

342

382prs = sUN "prim__readString"

343prs = sUN "prim__readString"

383pbm = sUN "prim__believe_me"

344pbm = sUN "prim__believe_me"

@@ -386,6 +347,8 @@ mkfprim = sUN "mkForeignPrim"

386pioret = sUN "prim_io_return"

347pioret = sUN "prim_io_return"

387piobind = sUN "prim_io_bind"

348piobind = sUN "prim_io_bind"

388upio = sUN "unsafePerformPrimIO"

349upio = sUN "unsafePerformPrimIO"

350+delay = sUN "Delay"

351+force = sUN "Force"

389

352

390-- | Look up primitive operations in the global table and transform them into ExecVal functions

353-- | Look up primitive operations in the global table and transform them into ExecVal functions

391getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)

354getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)

@@ -426,7 +389,7 @@ execCase env ctxt ns sc args =

426-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()

389-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()

427 caseRes <- execCase' env ctxt amap sc

390 caseRes <- execCase' env ctxt amap sc

428 case caseRes of

391 case caseRes of

429− Just res -> Just <$> execApp' (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)

392+ Just res -> Just <$> execApp (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)

430 Nothing -> return Nothing

393 Nothing -> return Nothing

431 else return Nothing

394 else return Nothing

432

395

@@ -436,8 +399,7 @@ execCase' env ctxt amap (UnmatchedCase _) = return Nothing

436execCase' env ctxt amap (STerm tm) =

399execCase' env ctxt amap (STerm tm) =

437 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm

400 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm

438execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =

401execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =

439− do tm' <- tryForce tm

440− case chooseAlt tm' alts of

402+ case chooseAlt tm alts of

441 Just (newCase, newBindings) ->

403 Just (newCase, newBindings) ->

442 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in

404 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in

443 execCase' env ctxt amap' newCase

405 execCase' env ctxt amap' newCase

test/reg039/expectednew file+2

@@ -0,0 +1,2 @@

1+Type checking ./reg039.idr

2+[3, 2, 1]

test/reg039/reg039.idrnew file+12

@@ -0,0 +1,12 @@

1+module LazyExec

3+-- The regression that this tests for is broken laziness in the executor.

5+covering

6+countdown : Int -> Lazy (List Int)

7+countdown n = if n > 0

8+ then (n :: countdown (n-1))

9+ else []

10+

11+go : IO ()

12+go = putStrLn $ show (Force (countdown 3))

test/reg039/runnew file+26

@@ -0,0 +1,26 @@

1+#!/usr/bin/env bash

3+# From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting

4+# Executes command with a timeout

5+# Params:

6+# $1 timeout in seconds

7+# $2 command

8+# Returns 1 if timed out 0 otherwise

9+timeout() {

10+

11+ time=$1

12+

13+ # start the command in a subshell to avoid problem with pipes

14+ # (spawn accepts one command)

15+ command="/bin/sh -c \"$2\""

16+

17+ expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"

18+

19+ if [ $? = 1 ] ; then

20+ echo "Timeout after ${time} seconds"

21+ fi

22+

23+}

24+

25+timeout 60 "idris $@ --nocolour reg039.idr --exec go"

26+rm -f reg039 *.ibc