git.iko.soy/Idris-dev
on master help sign in
More primitives
63263f7David Christiansen
src/Core/Execute.hs+48−13
compare with master
unifiedsplit
@@ -61,11 +61,13 @@ data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the res
61 , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness
61 , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness
62 , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad
62 , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad
63 , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
63 , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
64+ , exec_handles :: M.Map Int Handle -- ^ Opened files
65+ , exec_next_handle :: Int -- ^ Ensure opened file key uniqueness
64 }
66 }
65
67
66initState :: Idris ExecState
68initState :: Idris ExecState
67initState = do ist <- getIState
69initState = do ist <- getIState
68− return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)
70+ return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist) M.empty 0
69
71
70type Exec = ErrorT String (StateT ExecState IO)
72type Exec = ErrorT String (StateT ExecState IO)
71
73
@@ -111,6 +113,11 @@ execute tm = do est <- initState
111 Left err -> fail err
113 Left err -> fail err
112 Right tm' -> return tm'
114 Right tm' -> return tm'
113
115
116+ioWrap :: Term -> Term
117+ioWrap = App (P Ref (UN "prim__IO") Erased)
118+
119+ioUnit :: Term
120+ioUnit = ioWrap (P Ref unitCon Erased)
114
121
115doExec :: Env -> Context -> Term -> Exec Term
122doExec :: Env -> Context -> Term -> Exec Term
116doExec env ctxt p@(P Ref n ty) =
123doExec env ctxt p@(P Ref n ty) =
@@ -130,8 +137,8 @@ doExec env ctxt p@(P Bound n ty) = case (lookupDef n ctxt) of -- bound vars must
130 [Function ty tm] -> doExec env ctxt tm
137 [Function ty tm] -> doExec env ctxt tm
131 [] -> return p
138 [] -> return p
132 x -> fail ("Internal error lookup up bound var " ++ show n ++ " - found " ++ show x)
139 x -> fail ("Internal error lookup up bound var " ++ show n ++ " - found " ++ show x)
133−doExec env ctxt p@(P (DCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (DCon a b) n ty') }
140+doExec env ctxt p@(P (DCon _ _) n _) = return p
134−doExec env ctxt p@(P (TCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (TCon a b) n ty') }
141+doExec env ctxt p@(P (TCon _ _) n _) = return p
135doExec env ctxt v@(V i) | i < length env = do let binder = env !! i
142doExec env ctxt v@(V i) | i < length env = do let binder = env !! i
136 case binder of
143 case binder of
137 (_, (Let t v)) -> return v
144 (_, (Let t v)) -> return v
@@ -155,7 +162,7 @@ execApp :: Env -> Context -> (Term, [Term]) -> Exec Term
155execApp env ctxt (f, args) = do newF <- doExec env ctxt f
162execApp env ctxt (f, args) = do newF <- doExec env ctxt f
156 laziness <- getLaziness newF
163 laziness <- getLaziness newF
157 newArgs <- mapM (doExec env ctxt) args
164 newArgs <- mapM (doExec env ctxt) args
158− trace (show newF ++ show (zip args laziness)) $ return ()
165+ -- trace (show newF ++ show (zip args laziness)) $ return ()
159 execApp' env ctxt newF newArgs
166 execApp' env ctxt newF newArgs
160 where getLaziness (P _ (UN "lazy") _) = return [True]
167 where getLaziness (P _ (UN "lazy") _) = return [True]
161 getLaziness (P _ n _) = do est <- getExecState
168 getLaziness (P _ n _) = do est <- getExecState
@@ -170,6 +177,26 @@ execApp env ctxt (f, args) = do newF <- doExec env ctxt f
170execApp' :: Env -> Context -> Term -> [Term] -> Exec Term
177execApp' :: Env -> Context -> Term -> [Term] -> Exec Term
171execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
178execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
172execApp' env ctxt (P _ (UN "unsafePerformIO") _) [ty, action] | (prim__IO, [ty', v]) <- unApply action = return v
179execApp' env ctxt (P _ (UN "unsafePerformIO") _) [ty, action] | (prim__IO, [ty', v]) <- unApply action = return v
180+
181+-- Special cases arising from not having access to the C RTS in the interpreter
182+
183+execApp' env ctxt (P _ (UN "mkForeign") _) [_, fn, Constant (Str arg)]
184+ | Just (FFun "putStr" _ _) <- foreignFromTT fn = execIO (putStr arg) >> return ioUnit
185+execApp' env ctxt (P _ (UN "mkForeign") _) [_, fn, Constant (Str f), Constant (Str mode)]
186+ | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do trace ("Opening " ++ f ++ " with " ++ mode) $ return ()
187+ m <- case mode of
188+ "r" -> return ReadMode
189+ "w" -> return WriteMode
190+ "a" -> return AppendMode
191+ "rw" -> return ReadWriteMode
192+ "wr" -> return ReadWriteMode
193+ "r+" -> return ReadWriteMode
194+ _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
195+ h <- execIO $ openFile f m
196+ h' <- handle h
197+ return (ioWrap h')
198+
199+
173execApp' env ctxt (P _ (UN "mkForeign") _) args =
200execApp' env ctxt (P _ (UN "mkForeign") _) args =
174 do res <- stepForeign args
201 do res <- stepForeign args
175 case res of
202 case res of
@@ -191,15 +218,7 @@ execApp' env ctxt (P _ (UN "prim__ltInt") _) [Constant (I i1), Constant (I i2)]
191execApp' env ctxt (P _ (UN "prim__subInt") _) [Constant (I i1), Constant (I i2)] =
218execApp' env ctxt (P _ (UN "prim__subInt") _) [Constant (I i1), Constant (I i2)] =
192 return . Constant . I $ i1 - i2
219 return . Constant . I $ i1 - i2
193
220
194−execApp' env ctxt (P _ (UN "prim__readString") _) [ptr] | Just p <- unPtr ptr =
221+execApp' env ctxt (P _ (UN "prim__readString") _) [ptr] = trace "readString" $ undefined
195− do fn <- findForeign "freadStr"
196− case fn of
197− Just (Fun _ freadStr) -> do
198− res <- execIO $ callFFI freadStr retCString [argPtr p]
199− str <- execIO $ peekCString res
200− trace ("Found " ++ str) $ return ()
201− return $ Constant (Str str)
202− Nothing -> fail "Could not load freadStr"
203
222
204execApp' env ctxt f@(P _ n _) args =
223execApp' env ctxt f@(P _ n _) args =
205 do let val = lookupDef n ctxt
224 do let val = lookupDef n ctxt
@@ -275,6 +294,22 @@ unPtr (App (P _ con _) (Constant (I addr))) | con == ptrCon = Just (unAddr addr)
275 where unAddr a = nullPtr `plusPtr` a
294 where unAddr a = nullPtr `plusPtr` a
276unPtr _ = Nothing
295unPtr _ = Nothing
277
296
297+-- | Convert a Haskell file handle to a handle term in TT (an int)
298+handle :: Handle -> Exec Term
299+handle h = do est <- getExecState
300+ let i = exec_next_handle est
301+ putExecState $ est { exec_next_handle = exec_next_handle est + 1
302+ , exec_handles = M.insert i h (exec_handles est)
303+ }
304+ return $ Constant (I i)
305+
306+unHandle :: Term -> Exec Handle
307+unHandle (Constant (I i)) =
308+ do est <- getExecState
309+ case M.lookup i (exec_handles est) of
310+ Just h -> return h
311+ Nothing -> execFail "Bad handle ID"
312+unHandle _ = execFail "Not a handle"
278
313
279call :: Foreign -> [Term] -> Exec (Maybe Term)
314call :: Foreign -> [Term] -> Exec (Maybe Term)
280call (FFun name argTypes retType) args =
315call (FFun name argTypes retType) args =