@@ -15,6 +15,8 @@ import Util.System
1515
1616import Control.Applicative hiding (Const)
1717import Control.Monad.Trans
18+import Control.Monad.Trans.State.Strict
19+import Control.Monad.Trans.Error
1820import Control.Monad
1921import Data.Maybe
2022import qualified Data.Map as M
@@ -53,14 +55,66 @@ import System.IO
5355-- Nothing -> return tm
5456-- Just tm' -> execute' tm'
5557
58+data Lazy = Delayed Term | Forced Term
59+
60+data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs
61+ , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness
62+ , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad
63+ , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
64+ }
65+
66+initState :: Idris ExecState
67+initState = do ist <- getIState
68+ return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)
69+
70+type Exec = ErrorT String (StateT ExecState IO)
71+
72+runExec :: Exec a -> ExecState -> IO (Either String a)
73+runExec ex st = fst <$> runStateT (runErrorT ex) st
74+
75+getExecState :: Exec ExecState
76+getExecState = lift get
77+
78+putExecState :: ExecState -> Exec ()
79+putExecState = lift . put
80+
81+execFail :: String -> Exec a
82+execFail = throwError
83+
84+execIO :: IO a -> Exec a
85+execIO = lift . lift
86+
87+thunk :: Name
88+thunk = MN 0 "__execThunk"
89+
90+delay :: Term -> Exec Term
91+delay tm = do st <- getExecState
92+ let i = exec_next_thunk st
93+ putExecState $ st { exec_thunks = M.insert i (Delayed tm) (exec_thunks st)
94+ , exec_next_thunk = exec_next_thunk st + 1
95+ }
96+ return $ App (P Ref thunk Erased) (Constant (I i))
97+
98+force :: Int -> Exec Term
99+force i = do st <- getExecState
100+ let thunk = M.lookup i (exec_thunks st)
101+ case thunk of
102+ Just (Delayed tm) -> return tm -- FIXME DO THE EXEC
103+ Just (Forced tm) -> return tm
104+ Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"
56105
57106execute :: Term -> Idris Term
58−execute tm = do ctxt <- getContext
59− doExec [] ctxt tm
107+execute tm = do est <- initState
108+ ctxt <- getContext
109+ res <- lift $ runExec (doExec [] ctxt tm) est
110+ case res of
111+ Left err -> fail err
112+ Right tm' -> return tm'
60113
61−doExec :: Env -> Context -> Term -> Idris Term
114+
115+doExec :: Env -> Context -> Term -> Exec Term
62116doExec env ctxt p@(P Ref n ty) =
63− do let val = lookupDef Nothing n ctxt
117+ do let val = lookupDef n ctxt
64118 case val of
65119 [Function _ tm] ->
66120 do val <- doExec env ctxt tm
@@ -72,7 +126,7 @@ doExec env ctxt p@(P Ref n ty) =
72126 doExec env ctxt tm
73127 [CaseOp _ _ _ _ _ ns sc _ _] -> return p
74128 thing -> trace ("got to " ++ show thing) $ undefined
75−doExec env ctxt p@(P Bound n ty) = case (lookupDef Nothing n ctxt) of -- bound vars must be Function
129+doExec env ctxt p@(P Bound n ty) = case (lookupDef n ctxt) of -- bound vars must be Function
76130 [Function ty tm] -> doExec env ctxt tm
77131 [] -> return p
78132 x -> fail ("Internal error lookup up bound var " ++ show n ++ " - found " ++ show x)
@@ -97,23 +151,23 @@ doExec env ctxt Erased = return Erased
97151doExec env ctxt Impossible = fail "Tried to execute an impossible case"
98152doExec env ctxt (TType u) = return (TType u)
99153
100−execApp :: Env -> Context -> (Term, [Term]) -> Idris Term
154+execApp :: Env -> Context -> (Term, [Term]) -> Exec Term
101155execApp env ctxt (f, args) = do newF <- doExec env ctxt f
102156 laziness <- getLaziness newF
103157 newArgs <- mapM (doExec env ctxt) args
104158 trace (show newF ++ show (zip args laziness)) $ return ()
105159 execApp' env ctxt newF newArgs
106160 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
161+ getLaziness (P _ n _) = do est <- getExecState
162+ let argInfo = exec_implicits est
163+ case lookupCtxtName n argInfo of
110164 [] -> return (repeat False)
111165 [ps] -> return $ map lazyarg (snd ps)
112166 many -> fail $ "Ambiguous " ++ show n ++ ", found " ++ show many
113167 getLaziness x = return (repeat False) -- ok due to zip above
114168
115169
116−execApp' :: Env -> Context -> Term -> [Term] -> Idris Term
170+execApp' :: Env -> Context -> Term -> [Term] -> Exec Term
117171execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
118172execApp' env ctxt (P _ (UN "unsafePerformIO") _) [ty, action] | (prim__IO, [ty', v]) <- unApply action = return v
119173execApp' env ctxt (P _ (UN "mkForeign") _) args =
@@ -122,7 +176,7 @@ execApp' env ctxt (P _ (UN "mkForeign") _) args =
122176 Nothing -> fail "Could not call foreign function"
123177 Just r -> return r
124178execApp' env ctxt (P _ (UN "prim__readString") _) [P _ (UN "prim__stdin") _] =
125− do line <- lift getLine
179+ do line <- execIO getLine
126180 return (Constant (Str line))
127181
128182execApp' env ctxt (P _ (UN "prim__concat") _) [(Constant (Str s1)), (Constant (Str s2))] =
@@ -135,14 +189,14 @@ execApp' env ctxt (P _ (UN "prim__readString") _) [ptr] | Just p <- unPtr ptr =
135189 do fn <- findForeign "freadStr"
136190 case fn of
137191 Just (Fun _ freadStr) -> do
138− res <- lift $ callFFI freadStr retCString [argPtr p]
139− str <- lift $ peekCString res
192+ res <- execIO $ callFFI freadStr retCString [argPtr p]
193+ str <- execIO $ peekCString res
140194 trace ("Found " ++ str) $ return ()
141195 return $ Constant (Str str)
142196 Nothing -> fail "Could not load freadStr"
143197
144198execApp' env ctxt f@(P _ n _) args =
145− do let val = lookupDef Nothing n ctxt
199+ do let val = lookupDef n ctxt
146200 case val of
147201 [Function _ tm] -> fail "should already have been eval'd"
148202 [TyDecl nt ty] -> return $ mkApp f args
@@ -160,7 +214,7 @@ execApp' env ctxt bnd@(Bind n b body) (arg:args) = let ctxt' = addToCtxt n arg E
160214
161215execApp' env ctxt f args = return (mkApp f args)
162216
163−execCase :: Env -> Context -> [Name] -> SC -> [Term] -> Idris (Maybe Term)
217+execCase :: Env -> Context -> [Name] -> SC -> [Term] -> Exec (Maybe Term)
164218execCase env ctxt ns sc args =
165219 let arity = length ns in
166220 if arity <= length args
@@ -171,7 +225,7 @@ execCase env ctxt ns sc args =
171225 Nothing -> return Nothing
172226 else return Nothing
173227
174−execCase' :: Env -> Context -> [(Name, Term)] -> SC -> Idris (Maybe Term)
228+execCase' :: Env -> Context -> [(Name, Term)] -> SC -> Exec (Maybe Term)
175229execCase' env ctxt amap (STerm tm) =
176230 Just <$> doExec env (foldl (\c (n, t) -> addToCtxt n t Erased c) ctxt amap) tm
177231execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap
@@ -216,28 +270,28 @@ unPtr (App (P _ con _) (Constant (I addr))) | con == ptrCon = Just (unAddr addr)
216270unPtr _ = Nothing
217271
218272
219−call :: Foreign -> [Term] -> Idris (Maybe Term)
273+call :: Foreign -> [Term] -> Exec (Maybe Term)
220274call (FFun name argTypes retType) args =
221275 do fn <- findForeign name
222276 case fn of
223277 Nothing -> return Nothing
224278 Just f -> do res <- call' f args retType
225279 return . Just $ mkApp (P Ref (UN "prim__IO") Erased) [idrisType retType, res]
226− where call' :: ForeignFun -> [Term] -> FTy -> Idris Term
227− call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
280+ where call' :: ForeignFun -> [Term] -> FTy -> Exec Term
281+ call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)
228282 return (Constant (I (fromIntegral res)))
229− call' (Fun _ h) args FFloat = do res <- lift $ callFFI h retCDouble (prepArgs args)
283+ call' (Fun _ h) args FFloat = do res <- execIO $ callFFI h retCDouble (prepArgs args)
230284 return (Constant (Fl (realToFrac res)))
231− call' (Fun _ h) args FChar = do res <- lift $ callFFI h retCChar (prepArgs args)
285+ call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)
232286 return (Constant (Ch (castCCharToChar res)))
233− call' (Fun _ h) args FString = do res <- lift $ callFFI h retCString (prepArgs args)
234− hStr <- lift $ peekCString res
287+ call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
288+ hStr <- execIO $ peekCString res
235289-- lift $ free res
236290 return (Constant (Str hStr))
237291
238− call' (Fun _ h) args FPtr = do res <- lift $ callFFI h (retPtr retVoid) (prepArgs args)
292+ call' (Fun _ h) args FPtr = do res <- execIO $ callFFI h (retPtr retVoid) (prepArgs args)
239293 return (ptr res)
240− call' (Fun _ h) args FUnit = do res <- lift $ callFFI h retVoid (prepArgs args)
294+ call' (Fun _ h) args FUnit = do res <- execIO $ callFFI h retVoid (prepArgs args)
241295 return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level
242296-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
243297
@@ -284,7 +338,7 @@ toConst :: Term -> Maybe Const
284338toConst (Constant c) = Just c
285339toConst _ = Nothing
286340
287−stepForeign :: [Term] -> Idris (Maybe Term)
341+stepForeign :: [Term] -> Exec (Maybe Term)
288342stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
289343 f' <- case (call <$> ffun) of
290344 Just f -> f args
@@ -300,17 +354,15 @@ mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
300354 Just x'' -> return (x'':rest)
301355 Nothing -> return rest
302356
303−findForeign :: String -> Idris (Maybe ForeignFun)
304−findForeign fn = do i <- getIState
305− let libs = idris_dynamic_libs i
357+findForeign :: String -> Exec (Maybe ForeignFun)
358+findForeign fn = do est <- getExecState
359+ let libs = exec_dynamic_libs est
306360 fns <- mapMaybeM getFn libs
307361 case fns of
308362 [f] -> return (Just f)
309− [] -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" not found"
363+ [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
310364 return Nothing
311− fs -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
312− show (length fs) ++ " occurrences."
365+ fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
366+ show (length fs) ++ " occurrences."
313367 return Nothing
314− where getFn lib = lift $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)
315−
316−
368+ where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)