@@ -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,20 +58,20 @@ data ExecVal = EP NameType Name ExecVal
6158 | EErased
6259 | EConstant Const
6360 | forall a. EPtr (Ptr a)
64− | EThunk Int
61+ | EThunk Context ExecEnv Term
6562 | EHandle Handle
6663
6764instance Show ExecVal where
68− show (EP _ n _) = show n
69− show (EV i) = "!!V" ++ show i ++ "!!"
70− show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
71− show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
72− show (EType _) = "Type"
73− show EErased = "[__]"
74− show (EConstant c) = show c
75− show (EPtr p) = "<<ptr " ++ show p ++ ">>"
76− show (EThunk i) = "<<thunk " ++ show i ++ ">>"
77− show (EHandle h) = "<<handle " ++ show h ++ ">>"
65+ show (EP _ n _) = show n
66+ show (EV i) = "!!V" ++ show i ++ "!!"
67+ show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
68+ show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
69+ show (EType _) = "Type"
70+ show EErased = "[__]"
71+ show (EConstant c) = show c
72+ show (EPtr p) = "<<ptr " ++ show p ++ ">>"
73+ show (EThunk _ env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"
74+ show (EHandle h) = "<<handle " ++ show h ++ ">>"
7875
7976toTT :: ExecVal -> Exec Term
8077toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
@@ -82,22 +79,25 @@ toTT (EV i) = return $ V i
8279toTT (EBind n b body) = do body' <- body $ EP Bound n EErased
8380 b' <- fixBinder b
8481 Bind n b' <$> toTT body'
85− where fixBinder (Lam t) = Lam <$> toTT t
86− fixBinder (Pi t) = Pi <$> toTT t
87− fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
88− fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
89− fixBinder (Hole t) = Hole <$> toTT t
82+ where fixBinder (Lam t) = Lam <$> toTT t
83+ fixBinder (Pi t) = Pi <$> toTT t
84+ fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
85+ fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
86+ fixBinder (Hole t) = Hole <$> toTT t
9087 fixBinder (GHole i t) = GHole i <$> toTT t
91− fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
92− fixBinder (PVar t) = PVar <$> toTT t
93− fixBinder (PVTy t) = PVTy <$> toTT t
88+ fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
89+ fixBinder (PVar t) = PVar <$> toTT t
90+ fixBinder (PVTy t) = PVTy <$> toTT t
9491toTT (EApp e1 e2) = do e1' <- toTT e1
9592 e2' <- toTT e2
9693 return $ App e1' e2'
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 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')
101101toTT (EHandle _) = return Erased
102102
103103unApplyV :: ExecVal -> (ExecVal, [ExecVal])
@@ -111,7 +111,7 @@ mkEApp f (a:args) = mkEApp (EApp f a) args
111111
112112initState :: Idris ExecState
113113initState = do ist <- getIState
114− return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)
114+ return $ ExecState (idris_dynamic_libs ist)
115115
116116type Exec = ErrorT String (StateT ExecState IO)
117117
@@ -130,45 +130,13 @@ execFail = throwError
130130execIO :: IO a -> Exec a
131131execIO = lift . lift
132132
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)))
166133
167134execute :: Term -> Idris Term
168135execute tm = do est <- initState
169136 ctxt <- getContext
170− res <- lift . lift $ flip runExec est $ do res <- doExec [] ctxt tm
171− toTT res
137+ res <- lift . lift . flip runExec est $
138+ do res <- doExec [] ctxt tm
139+ toTT res
172140 case res of
173141 Left err -> fail err
174142 Right tm' -> return tm'
@@ -208,7 +176,18 @@ doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
208176doExec env ctxt tm@(Bind n b body) = return $
209177 EBind n (fmap (\_->EErased) b)
210178 (\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'
212191doExec env ctxt (Constant c) = return (EConstant c)
213192doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
214193 doExec env ctxt ((x:xs) !! i)
@@ -216,55 +195,39 @@ doExec env ctxt Erased = return EErased
216195doExec env ctxt Impossible = fail "Tried to execute an impossible case"
217196doExec env ctxt (TType u) = return (EType u)
218197
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)
198+
199+execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
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
206+execApp env ctxt (EP _ fp _) (ty:action:rest)
241207 | fp == upio,
242208 (prim__IO, [_, v]) <- unApplyV action
243− = execApp' env ctxt v rest
209+ = execApp env ctxt v rest
244210
245−execApp' env ctxt (EP _ fp _) args@(_:_:v:k:rest)
211+execApp env ctxt (EP _ fp _) args@(_:_:v:k:rest)
246212 | fp == piobind,
247213 (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
214+ do res <- execApp env ctxt k [v']
215+ execApp env ctxt res rest
216+execApp env ctxt con@(EP _ fp _) args@(tp:v:rest)
217+ | fp == pioret = execApp env ctxt (mkEApp con [tp, v]) rest
255218
256219-- 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)
258221 | fp == mkfprim,
259222 Just (FFun "putStr" _ _) <- foreignFromTT fn
260223 = do execIO (putStr arg)
261− execApp' env ctxt ioUnit rest
262−execApp' env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)
224+ execApp env ctxt ioUnit rest
225+execApp env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)
263226 | fp == mkfprim,
264227 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn
265228 = 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)
229+ execApp env ctxt (EConstant (Str (contents ++ "\n"))) rest
230+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
268231 | fp == mkfprim,
269232 Just (FFun "fileOpen" _ _) <- foreignFromTT fn
270233 = do f <- execIO $
@@ -283,53 +246,53 @@ execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
283246 in return $ Right (ioWrap (EPtr nullPtr), tail rest))
284247 case f of
285248 Left err -> execFail err
286− Right (res, rest) -> execApp' env ctxt res rest
249+ Right (res, rest) -> execApp env ctxt res rest
287250
288−execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
251+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
289252 | fp == mkfprim,
290253 Just (FFun "fileEOF" _ _) <- foreignFromTT fn
291254 = do eofp <- execIO $ hIsEOF h
292255 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)
294257
295−execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
258+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
296259 | fp == mkfprim,
297260 Just (FFun "fileClose" _ _) <- foreignFromTT fn
298261 = do execIO $ hClose h
299− execApp' env ctxt ioUnit (tail rest)
262+ execApp env ctxt ioUnit (tail rest)
300263
301−execApp' env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)
264+execApp env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)
302265 | fp == mkfprim,
303266 Just (FFun "isNull" _ _) <- foreignFromTT fn
304267 = let res = ioWrap . EConstant . I $
305268 if p == nullPtr then 1 else 0
306− in execApp' env ctxt res (tail rest)
269+ in execApp env ctxt res (tail rest)
307270
308271-- Handles will be checked as null pointers sometimes - but if we got a
309272-- 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)
311274 | fp == mkfprim,
312275 Just (FFun "isNull" _ _) <- foreignFromTT fn
313276 = let res = ioWrap . EConstant . I $ 0
314− in execApp' env ctxt res (tail rest)
277+ in execApp env ctxt res (tail rest)
315278
316279-- 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)
318281 | fp == mkfprim,
319282 Just (FFun "isNull" _ _) <- foreignFromTT fn
320283 = let res = ioWrap . EConstant . I $ 0
321− in execApp' env ctxt res (tail rest)
284+ in execApp env ctxt res (tail rest)
322285
323286-- Right now, there's no way to send command-line arguments to the executor,
324287-- so just return 0.
325−execApp' env ctxt (EP _ fp _) (_:fn:rest)
288+execApp env ctxt (EP _ fp _) (_:fn:rest)
326289 | fp == mkfprim,
327290 Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn
328291 = let res = ioWrap . EConstant . I $ 0
329− in execApp' env ctxt res (tail rest)
292+ in execApp env ctxt res (tail rest)
330293-- Throw away the 'World' argument to the foreign function
331294
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
333296 = case foreignFromTT fn of
334297 Just (FFun f argTs retT) | length xs >= length argTs ->
335298 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
341304 Just r -> return (mkEApp r xs')
342305 Nothing -> return (mkEApp f args)
343306
344−execApp' env ctxt c@(EP (DCon _ arity) n _) args =
345− do args' <- mapM tryForce (take arity args)
307+execApp env ctxt c@(EP (DCon _ arity) n _) args =
308+ do let args' = take arity args
346309 let restArgs = drop arity args
347− execApp' env ctxt (mkEApp c args') restArgs
310+ execApp env ctxt (mkEApp c args') restArgs
348311
349−execApp' env ctxt c@(EP (TCon _ arity) n _) args =
350− do args' <- mapM tryForce (take arity args)
312+execApp env ctxt c@(EP (TCon _ arity) n _) args =
313+ do let args' = take arity args
351314 let restArgs = drop arity args
352− execApp' env ctxt (mkEApp c args') restArgs
315+ execApp env ctxt (mkEApp c args') restArgs
353316
354−execApp' env ctxt f@(EP _ n _) args =
317+execApp env ctxt f@(EP _ n _) args =
355318 do let val = lookupDef n ctxt
356319 case val of
357320 [Function _ tm] -> fail "should already have been eval'd"
358321 [TyDecl nt ty] -> return $ mkEApp f args
359322 [Operator tp arity op] ->
360323 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)
324+ then let args' = take arity args in
325+ case getOp n args' of
326+ Just res -> do r <- res
327+ execApp env ctxt r (drop arity args)
328+ Nothing -> return (mkEApp f args)
366329 else return (mkEApp f args)
367330 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
368331 do rhs <- doExec env ctxt tm
369− execApp' env ctxt rhs args
332+ execApp env ctxt rhs args
370333 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->
371334 do res <- execCase env ctxt ns sc args
372335 return $ fromMaybe (mkEApp f args) res
373336 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)
337+execApp env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
338+ let (f', as) = unApplyV ret
339+ execApp env ctxt f' (as ++ args)
340+execApp env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp env ctxt f (args1 ++ args2)
341+execApp env ctxt f args = return (mkEApp f args)
381342
382343prs = sUN "prim__readString"
383344pbm = sUN "prim__believe_me"
@@ -386,6 +347,8 @@ mkfprim = sUN "mkForeignPrim"
386347pioret = sUN "prim_io_return"
387348piobind = sUN "prim_io_bind"
388349upio = sUN "unsafePerformPrimIO"
350+delay = sUN "Delay"
351+force = sUN "Force"
389352
390353-- | Look up primitive operations in the global table and transform them into ExecVal functions
391354getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
@@ -426,7 +389,7 @@ execCase env ctxt ns sc args =
426389-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()
427390 caseRes <- execCase' env ctxt amap sc
428391 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)
430393 Nothing -> return Nothing
431394 else return Nothing
432395
@@ -436,8 +399,7 @@ execCase' env ctxt amap (UnmatchedCase _) = return Nothing
436399execCase' env ctxt amap (STerm tm) =
437400 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm
438401execCase' 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
441403 Just (newCase, newBindings) ->
442404 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
443405 execCase' env ctxt amap' newCase