@@ -98,10 +98,20 @@ doExec env ctxt Impossible = fail "Tried to execute an impossible case"
98doExec env ctxt (TType u) = return (TType u)
98doExec env ctxt (TType u) = return (TType u)
100execApp :: Env -> Context -> (Term, [Term]) -> Idris Term
100execApp :: Env -> Context -> (Term, [Term]) -> Idris Term
101−execApp env ctxt (f, args) = trace ("Reducing " ++ show f) $
102− do newF <- doExec env ctxt f
101+execApp env ctxt (f, args) = do newF <- doExec env ctxt f
102+ laziness <- getLaziness newF
103 newArgs <- mapM (doExec env ctxt) args
103 newArgs <- mapM (doExec env ctxt) args
104+ trace (show newF ++ show (zip args laziness)) $ return ()
104 execApp' env ctxt newF newArgs
105 execApp' env ctxt newF newArgs
106+ where getLaziness (P _ (UN "lazy") _) = return [True]
107+ getLaziness (P _ n _) = do ist <- getIState
108+ let argInfo = idris_implicits ist
109+ case lookupCtxtName Nothing n argInfo of
110+ [] -> return (repeat False)
111+ [ps] -> return $ map lazyarg (snd ps)
112+ many -> fail $ "Ambiguous " ++ show n ++ ", found " ++ show many
113+ getLaziness x = return (repeat False) -- ok due to zip above
106execApp' :: Env -> Context -> Term -> [Term] -> Idris Term
116execApp' :: Env -> Context -> Term -> [Term] -> Idris Term
107execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
117execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls