@@ -47,11 +47,8 @@ readMay s = case reads s of
4747
4848data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
4949
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
54− }
50+newtype ExecState = ExecState { exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
51+ }
5552
5653data ExecVal = EP NameType Name ExecVal
5754 | EV Int
@@ -61,7 +58,7 @@ data ExecVal = EP NameType Name ExecVal
6158 | EErased
6259 | EConstant Const
6360 | forall a. EPtr (Ptr a)
64− | EThunk Int
61+ | EThunk ExecEnv Term
6562 | EHandle Handle
6663
6764instance Show ExecVal where
@@ -73,7 +70,7 @@ instance Show ExecVal where
7370 show EErased = "[__]"
7471 show (EConstant c) = show c
7572 show (EPtr p) = "<<ptr " ++ show p ++ ">>"
76− show (EThunk i) = "<<thunk " ++ show i ++ ">>"
73+ show (EThunk env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"
7774 show (EHandle h) = "<<handle " ++ show h ++ ">>"
7875
7976toTT :: ExecVal -> Exec Term
@@ -97,7 +94,7 @@ toTT (EApp e1 e2) = do e1' <- toTT e1
9794toTT (EType u) = return $ TType u
9895toTT EErased = return Erased
9996toTT (EConstant c) = return (Constant c)
100−toTT (EThunk i) = return (P (DCon 0 0) (sMN i "THUNK") Erased) --(force i) >>= toTT
97+toTT (EThunk env tm) = return tm
10198toTT (EHandle _) = return Erased
10299
103100unApplyV :: ExecVal -> (ExecVal, [ExecVal])
@@ -111,7 +108,7 @@ mkEApp f (a:args) = mkEApp (EApp f a) args
111108
112109initState :: Idris ExecState
113110initState = do ist <- getIState
114− return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)
111+ return $ ExecState (idris_dynamic_libs ist)
115112
116113type Exec = ErrorT String (StateT ExecState IO)
117114
@@ -130,45 +127,13 @@ execFail = throwError
130127execIO :: IO a -> Exec a
131128execIO = lift . lift
132129
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)))
166130
167131execute :: Term -> Idris Term
168132execute tm = do est <- initState
169133 ctxt <- getContext
170− res <- lift . lift $ flip runExec est $ do res <- doExec [] ctxt tm
171− toTT res
134+ res <- lift . lift . flip runExec est $
135+ do res <- doExec [] ctxt tm
136+ toTT res
172137 case res of
173138 Left err -> fail err
174139 Right tm' -> return tm'
@@ -208,7 +173,18 @@ doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
208173doExec env ctxt tm@(Bind n b body) = return $
209174 EBind n (fmap (\_->EErased) b)
210175 (\arg -> doExec ((n, arg):env) ctxt body)
211−doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)
176+doExec env ctxt a@(App _ _) =
177+ do let (f, args) = unApply a
178+ f' <- doExec env ctxt f
179+ args' <- case f' of
180+ (EP _ d _) | d == delay ->
181+ case args of
182+ [t,a,tm] -> do t' <- doExec env ctxt t
183+ a' <- doExec env ctxt a
184+ return [t', a', EThunk env tm]
185+ _ -> mapM (doExec env ctxt) args -- partial applications are fine to evaluate
186+ fun' -> do mapM (doExec env ctxt) args
187+ execApp env ctxt f' args'
212188doExec env ctxt (Constant c) = return (EConstant c)
213189doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
214190 doExec env ctxt ((x:xs) !! i)
@@ -216,55 +192,39 @@ doExec env ctxt Erased = return EErased
216192doExec env ctxt Impossible = fail "Tried to execute an impossible case"
217193doExec env ctxt (TType u) = return (EType u)
218194
219−execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal
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
239−execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
240−execApp' env ctxt (EP _ fp _) (ty:action:rest)
195+
196+execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
197+execApp env ctxt v [] = return v -- no args is just a constant! can result from function calls
198+execApp env ctxt (EP _ f _) (t:a:delayed:rest)
199+ | f == force
200+ , (_, [_, _, EThunk tmEnv tm]) <- unApplyV delayed =
201+ do tm' <- doExec tmEnv ctxt tm
202+ execApp env ctxt tm' rest
203+execApp env ctxt (EP _ fp _) (ty:action:rest)
241204 | fp == upio,
242205 (prim__IO, [_, v]) <- unApplyV action
243− = execApp' env ctxt v rest
206+ = execApp env ctxt v rest
244207
245−execApp' env ctxt (EP _ fp _) args@(_:_:v:k:rest)
208+execApp env ctxt (EP _ fp _) args@(_:_:v:k:rest)
246209 | fp == piobind,
247210 (prim__IO, [_, v']) <- unApplyV v =
248− do v'' <- tryForce v'
249− res <- execApp' env ctxt k [v''] >>= tryForce
250− execApp' env ctxt res rest
251−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
211+ do res <- execApp env ctxt k [v']
212+ execApp env ctxt res rest
213+execApp env ctxt con@(EP _ fp _) args@(tp:v:rest)
214+ | fp == pioret = execApp env ctxt (mkEApp con [tp, v]) rest
255215
256216-- 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)
217+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str arg):_:rest)
258218 | fp == mkfprim,
259219 Just (FFun "putStr" _ _) <- foreignFromTT fn
260220 = do execIO (putStr arg)
261− execApp' env ctxt ioUnit rest
262−execApp' env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)
221+ execApp env ctxt ioUnit rest
222+execApp env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)
263223 | fp == mkfprim,
264224 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn
265225 = do contents <- execIO $ hGetLine h
266− execApp' env ctxt (EConstant (Str (contents ++ "\n"))) rest
267−execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
226+ execApp env ctxt (EConstant (Str (contents ++ "\n"))) rest
227+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
268228 | fp == mkfprim,
269229 Just (FFun "fileOpen" _ _) <- foreignFromTT fn
270230 = do f <- execIO $
@@ -283,53 +243,53 @@ execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
283243 in return $ Right (ioWrap (EPtr nullPtr), tail rest))
284244 case f of
285245 Left err -> execFail err
286− Right (res, rest) -> execApp' env ctxt res rest
246+ Right (res, rest) -> execApp env ctxt res rest
287247
288−execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
248+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
289249 | fp == mkfprim,
290250 Just (FFun "fileEOF" _ _) <- foreignFromTT fn
291251 = do eofp <- execIO $ hIsEOF h
292252 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
293− execApp' env ctxt res (tail rest)
253+ execApp env ctxt res (tail rest)
294254
295−execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
255+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
296256 | fp == mkfprim,
297257 Just (FFun "fileClose" _ _) <- foreignFromTT fn
298258 = do execIO $ hClose h
299− execApp' env ctxt ioUnit (tail rest)
259+ execApp env ctxt ioUnit (tail rest)
300260
301−execApp' env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)
261+execApp env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)
302262 | fp == mkfprim,
303263 Just (FFun "isNull" _ _) <- foreignFromTT fn
304264 = let res = ioWrap . EConstant . I $
305265 if p == nullPtr then 1 else 0
306− in execApp' env ctxt res (tail rest)
266+ in execApp env ctxt res (tail rest)
307267
308268-- Handles will be checked as null pointers sometimes - but if we got a
309269-- real Handle, then it's valid, so just return 1.
310−execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
270+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
311271 | fp == mkfprim,
312272 Just (FFun "isNull" _ _) <- foreignFromTT fn
313273 = let res = ioWrap . EConstant . I $ 0
314− in execApp' env ctxt res (tail rest)
274+ in execApp env ctxt res (tail rest)
315275
316276-- A foreign-returned char* has to be tested for NULL sometimes
317−execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str s):rest)
277+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str s):rest)
318278 | fp == mkfprim,
319279 Just (FFun "isNull" _ _) <- foreignFromTT fn
320280 = let res = ioWrap . EConstant . I $ 0
321− in execApp' env ctxt res (tail rest)
281+ in execApp env ctxt res (tail rest)
322282
323283-- Right now, there's no way to send command-line arguments to the executor,
324284-- so just return 0.
325−execApp' env ctxt (EP _ fp _) (_:fn:rest)
285+execApp env ctxt (EP _ fp _) (_:fn:rest)
326286 | fp == mkfprim,
327287 Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn
328288 = let res = ioWrap . EConstant . I $ 0
329− in execApp' env ctxt res (tail rest)
289+ in execApp env ctxt res (tail rest)
330290-- Throw away the 'World' argument to the foreign function
331291
332−execApp' env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim
292+execApp env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim
333293 = case foreignFromTT fn of
334294 Just (FFun f argTs retT) | length xs >= length argTs ->
335295 do let (args', xs') = (take (length argTs) xs, -- foreign args
@@ -341,43 +301,41 @@ execApp' env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim
341301 Just r -> return (mkEApp r xs')
342302 Nothing -> return (mkEApp f args)
343303
344−execApp' env ctxt c@(EP (DCon _ arity) n _) args =
345− do args' <- mapM tryForce (take arity args)
304+execApp env ctxt c@(EP (DCon _ arity) n _) args =
305+ do let args' = take arity args
346306 let restArgs = drop arity args
347− execApp' env ctxt (mkEApp c args') restArgs
307+ execApp env ctxt (mkEApp c args') restArgs
348308
349−execApp' env ctxt c@(EP (TCon _ arity) n _) args =
350− do args' <- mapM tryForce (take arity args)
309+execApp env ctxt c@(EP (TCon _ arity) n _) args =
310+ do let args' = take arity args
351311 let restArgs = drop arity args
352− execApp' env ctxt (mkEApp c args') restArgs
312+ execApp env ctxt (mkEApp c args') restArgs
353313
354−execApp' env ctxt f@(EP _ n _) args =
314+execApp env ctxt f@(EP _ n _) args =
355315 do let val = lookupDef n ctxt
356316 case val of
357317 [Function _ tm] -> fail "should already have been eval'd"
358318 [TyDecl nt ty] -> return $ mkEApp f args
359319 [Operator tp arity op] ->
360320 if length args >= arity
361− then do args' <- mapM tryForce $ take arity args
362− case getOp n args' of
363− Just res -> do r <- res
364− execApp' env ctxt r (drop arity args)
365− Nothing -> return (mkEApp f args)
321+ then let args' = take arity args in
322+ case getOp n args' of
323+ Just res -> do r <- res
324+ execApp env ctxt r (drop arity args)
325+ Nothing -> return (mkEApp f args)
366326 else return (mkEApp f args)
367327 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
368328 do rhs <- doExec env ctxt tm
369− execApp' env ctxt rhs args
329+ execApp env ctxt rhs args
370330 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->
371331 do res <- execCase env ctxt ns sc args
372332 return $ fromMaybe (mkEApp f args) res
373333 thing -> return $ mkEApp f args
374−execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
375− let (f', as) = unApplyV ret
376− 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)
380−execApp' env ctxt f args = return (mkEApp f args)
334+execApp env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
335+ let (f', as) = unApplyV ret
336+ execApp env ctxt f' (as ++ args)
337+execApp env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp env ctxt f (args1 ++ args2)
338+execApp env ctxt f args = return (mkEApp f args)
381339
382340prs = sUN "prim__readString"
383341pbm = sUN "prim__believe_me"
@@ -386,6 +344,8 @@ mkfprim = sUN "mkForeignPrim"
386344pioret = sUN "prim_io_return"
387345piobind = sUN "prim_io_bind"
388346upio = sUN "unsafePerformPrimIO"
347+delay = sUN "Delay"
348+force = sUN "Force"
389349
390350-- | Look up primitive operations in the global table and transform them into ExecVal functions
391351getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
@@ -426,7 +386,7 @@ execCase env ctxt ns sc args =
426386-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()
427387 caseRes <- execCase' env ctxt amap sc
428388 case caseRes of
429− Just res -> Just <$> execApp' (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)
389+ Just res -> Just <$> execApp (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)
430390 Nothing -> return Nothing
431391 else return Nothing
432392
@@ -436,8 +396,7 @@ execCase' env ctxt amap (UnmatchedCase _) = return Nothing
436396execCase' env ctxt amap (STerm tm) =
437397 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm
438398execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
439− do tm' <- tryForce tm
440− case chooseAlt tm' alts of
399+ case chooseAlt tm alts of
441400 Just (newCase, newBindings) ->
442401 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
443402 execCase' env ctxt amap' newCase