@@ -15,6 +15,8 @@ import Util.System
16import Control.Applicative hiding (Const)
16import Control.Applicative hiding (Const)
17import Control.Monad.Trans
17import Control.Monad.Trans
18+import Control.Monad.Trans.State.Strict
19+import Control.Monad.Trans.Error
18import Control.Monad
20import Control.Monad
19import Data.Maybe
21import Data.Maybe
20import qualified Data.Map as M
22import qualified Data.Map as M
@@ -53,14 +55,66 @@ import System.IO
53-- Nothing -> return tm
55-- Nothing -> return tm
54-- Just tm' -> execute' tm'
56-- Just tm' -> execute' tm'
58+data Lazy = Delayed Term | Forced Term
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
66+initState :: Idris ExecState
67+initState = do ist <- getIState
68+ return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)
70+type Exec = ErrorT String (StateT ExecState IO)
72+runExec :: Exec a -> ExecState -> IO (Either String a)
73+runExec ex st = fst <$> runStateT (runErrorT ex) st
75+getExecState :: Exec ExecState
76+getExecState = lift get
78+putExecState :: ExecState -> Exec ()
79+putExecState = lift . put
81+execFail :: String -> Exec a
84+execIO :: IO a -> Exec a
88+thunk = MN 0 "__execThunk"
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
96+ return $ App (P Ref thunk Erased) (Constant (I i))
98+force :: Int -> Exec Term
99+force i = do st <- getExecState
100+ let thunk = M.lookup i (exec_thunks st)
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!"
57execute :: Term -> Idris Term
106execute :: Term -> Idris Term
107+execute tm = do est <- initState
58−execute tm = do ctxt <- getContext
108+ ctxt <- getContext
59− doExec [] ctxt tm
109+ res <- lift $ runExec (doExec [] ctxt tm) est
111+ Left err -> fail err
112+ Right tm' -> return tm'
61−doExec :: Env -> Context -> Term -> Idris Term
115+doExec :: Env -> Context -> Term -> Exec Term
62doExec env ctxt p@(P Ref n ty) =
116doExec env ctxt p@(P Ref n ty) =
63− do let val = lookupDef Nothing n ctxt
117+ do let val = lookupDef n ctxt
64 case val of
118 case val of
65 [Function _ tm] ->
119 [Function _ tm] ->
66 do val <- doExec env ctxt tm
120 do val <- doExec env ctxt tm
@@ -72,7 +126,7 @@ doExec env ctxt p@(P Ref n ty) =
72 doExec env ctxt tm
126 doExec env ctxt tm
73 [CaseOp _ _ _ _ _ ns sc _ _] -> return p
127 [CaseOp _ _ _ _ _ ns sc _ _] -> return p
74 thing -> trace ("got to " ++ show thing) $ undefined
128 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
76 [Function ty tm] -> doExec env ctxt tm
130 [Function ty tm] -> doExec env ctxt tm
77 [] -> return p
131 [] -> return p
78 x -> fail ("Internal error lookup up bound var " ++ show n ++ " - found " ++ show x)
132 x -> fail ("Internal error lookup up bound var " ++ show n ++ " - found " ++ show x)
@@ -97,23 +151,23 @@ doExec env ctxt Erased = return Erased
97doExec env ctxt Impossible = fail "Tried to execute an impossible case"
151doExec env ctxt Impossible = fail "Tried to execute an impossible case"
98doExec env ctxt (TType u) = return (TType u)
152doExec env ctxt (TType u) = return (TType u)
100−execApp :: Env -> Context -> (Term, [Term]) -> Idris Term
154+execApp :: Env -> Context -> (Term, [Term]) -> Exec Term
101execApp env ctxt (f, args) = do newF <- doExec env ctxt f
155execApp env ctxt (f, args) = do newF <- doExec env ctxt f
102 laziness <- getLaziness newF
156 laziness <- getLaziness newF
103 newArgs <- mapM (doExec env ctxt) args
157 newArgs <- mapM (doExec env ctxt) args
104 trace (show newF ++ show (zip args laziness)) $ return ()
158 trace (show newF ++ show (zip args laziness)) $ return ()
105 execApp' env ctxt newF newArgs
159 execApp' env ctxt newF newArgs
106 where getLaziness (P _ (UN "lazy") _) = return [True]
160 where getLaziness (P _ (UN "lazy") _) = return [True]
107− getLaziness (P _ n _) = do ist <- getIState
161+ getLaziness (P _ n _) = do est <- getExecState
108− let argInfo = idris_implicits ist
162+ let argInfo = exec_implicits est
109− case lookupCtxtName Nothing n argInfo of
163+ case lookupCtxtName n argInfo of
110 [] -> return (repeat False)
164 [] -> return (repeat False)
111 [ps] -> return $ map lazyarg (snd ps)
165 [ps] -> return $ map lazyarg (snd ps)
112 many -> fail $ "Ambiguous " ++ show n ++ ", found " ++ show many
166 many -> fail $ "Ambiguous " ++ show n ++ ", found " ++ show many
113 getLaziness x = return (repeat False) -- ok due to zip above
167 getLaziness x = return (repeat False) -- ok due to zip above
116−execApp' :: Env -> Context -> Term -> [Term] -> Idris Term
170+execApp' :: Env -> Context -> Term -> [Term] -> Exec Term
117execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
171execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
118execApp' env ctxt (P _ (UN "unsafePerformIO") _) [ty, action] | (prim__IO, [ty', v]) <- unApply action = return v
172execApp' env ctxt (P _ (UN "unsafePerformIO") _) [ty, action] | (prim__IO, [ty', v]) <- unApply action = return v
119execApp' env ctxt (P _ (UN "mkForeign") _) args =
173execApp' env ctxt (P _ (UN "mkForeign") _) args =
@@ -122,7 +176,7 @@ execApp' env ctxt (P _ (UN "mkForeign") _) args =
122 Nothing -> fail "Could not call foreign function"
176 Nothing -> fail "Could not call foreign function"
123 Just r -> return r
177 Just r -> return r
124execApp' env ctxt (P _ (UN "prim__readString") _) [P _ (UN "prim__stdin") _] =
178execApp' env ctxt (P _ (UN "prim__readString") _) [P _ (UN "prim__stdin") _] =
125− do line <- lift getLine
179+ do line <- execIO getLine
126 return (Constant (Str line))
180 return (Constant (Str line))
128execApp' env ctxt (P _ (UN "prim__concat") _) [(Constant (Str s1)), (Constant (Str s2))] =
182execApp' 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 =
135 do fn <- findForeign "freadStr"
189 do fn <- findForeign "freadStr"
136 case fn of
190 case fn of
137 Just (Fun _ freadStr) -> do
191 Just (Fun _ freadStr) -> do
138− res <- lift $ callFFI freadStr retCString [argPtr p]
192+ res <- execIO $ callFFI freadStr retCString [argPtr p]
139− str <- lift $ peekCString res
193+ str <- execIO $ peekCString res
140 trace ("Found " ++ str) $ return ()
194 trace ("Found " ++ str) $ return ()
141 return $ Constant (Str str)
195 return $ Constant (Str str)
142 Nothing -> fail "Could not load freadStr"
196 Nothing -> fail "Could not load freadStr"
144execApp' env ctxt f@(P _ n _) args =
198execApp' env ctxt f@(P _ n _) args =
145− do let val = lookupDef Nothing n ctxt
199+ do let val = lookupDef n ctxt
146 case val of
200 case val of
147 [Function _ tm] -> fail "should already have been eval'd"
201 [Function _ tm] -> fail "should already have been eval'd"
148 [TyDecl nt ty] -> return $ mkApp f args
202 [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
161execApp' env ctxt f args = return (mkApp f args)
215execApp' env ctxt f args = return (mkApp f args)
163−execCase :: Env -> Context -> [Name] -> SC -> [Term] -> Idris (Maybe Term)
217+execCase :: Env -> Context -> [Name] -> SC -> [Term] -> Exec (Maybe Term)
164execCase env ctxt ns sc args =
218execCase env ctxt ns sc args =
165 let arity = length ns in
219 let arity = length ns in
166 if arity <= length args
220 if arity <= length args
@@ -171,7 +225,7 @@ execCase env ctxt ns sc args =
171 Nothing -> return Nothing
225 Nothing -> return Nothing
172 else return Nothing
226 else return Nothing
174−execCase' :: Env -> Context -> [(Name, Term)] -> SC -> Idris (Maybe Term)
228+execCase' :: Env -> Context -> [(Name, Term)] -> SC -> Exec (Maybe Term)
175execCase' env ctxt amap (STerm tm) =
229execCase' env ctxt amap (STerm tm) =
176 Just <$> doExec env (foldl (\c (n, t) -> addToCtxt n t Erased c) ctxt amap) tm
230 Just <$> doExec env (foldl (\c (n, t) -> addToCtxt n t Erased c) ctxt amap) tm
177execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap
231execCase' 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)
216unPtr _ = Nothing
270unPtr _ = Nothing
219−call :: Foreign -> [Term] -> Idris (Maybe Term)
273+call :: Foreign -> [Term] -> Exec (Maybe Term)
220call (FFun name argTypes retType) args =
274call (FFun name argTypes retType) args =
221 do fn <- findForeign name
275 do fn <- findForeign name
222 case fn of
276 case fn of
223 Nothing -> return Nothing
277 Nothing -> return Nothing
224 Just f -> do res <- call' f args retType
278 Just f -> do res <- call' f args retType
225 return . Just $ mkApp (P Ref (UN "prim__IO") Erased) [idrisType retType, res]
279 return . Just $ mkApp (P Ref (UN "prim__IO") Erased) [idrisType retType, res]
226− where call' :: ForeignFun -> [Term] -> FTy -> Idris Term
280+ where call' :: ForeignFun -> [Term] -> FTy -> Exec Term
227− call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
281+ call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)
228 return (Constant (I (fromIntegral res)))
282 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)
230 return (Constant (Fl (realToFrac res)))
284 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)
232 return (Constant (Ch (castCCharToChar res)))
286 return (Constant (Ch (castCCharToChar res)))
233− call' (Fun _ h) args FString = do res <- lift $ callFFI h retCString (prepArgs args)
287+ call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
234− hStr <- lift $ peekCString res
288+ hStr <- execIO $ peekCString res
235-- lift $ free res
289-- lift $ free res
236 return (Constant (Str hStr))
290 return (Constant (Str hStr))
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)
239 return (ptr res)
293 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)
241 return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level
295 return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level
242-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
296-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
@@ -284,7 +338,7 @@ toConst :: Term -> Maybe Const
284toConst (Constant c) = Just c
338toConst (Constant c) = Just c
285toConst _ = Nothing
339toConst _ = Nothing
287−stepForeign :: [Term] -> Idris (Maybe Term)
341+stepForeign :: [Term] -> Exec (Maybe Term)
288stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
342stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
289 f' <- case (call <$> ffun) of
343 f' <- case (call <$> ffun) of
290 Just f -> f args
344 Just f -> f args
@@ -300,17 +354,15 @@ mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
300 Just x'' -> return (x'':rest)
354 Just x'' -> return (x'':rest)
301 Nothing -> return rest
355 Nothing -> return rest
303−findForeign :: String -> Idris (Maybe ForeignFun)
357+findForeign :: String -> Exec (Maybe ForeignFun)
304−findForeign fn = do i <- getIState
358+findForeign fn = do est <- getExecState
305− let libs = idris_dynamic_libs i
359+ let libs = exec_dynamic_libs est
306 fns <- mapMaybeM getFn libs
360 fns <- mapMaybeM getFn libs
307 case fns of
361 case fns of
308 [f] -> return (Just f)
362 [f] -> return (Just f)
309− [] -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" not found"
363+ [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
310 return Nothing
364 return Nothing
311− fs -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
365+ fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
312− show (length fs) ++ " occurrences."
366+ show (length fs) ++ " occurrences."
313 return Nothing
367 return Nothing
314− where getFn lib = lift $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)
368+ where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)