git.iko.soy/Idris-dev
on 63263f7 help sign in
Idris-dev/src/Core/Execute.hs
409 lines 19 kB history raw
1{-# LANGUAGE PatternGuards #-}
2module Core.Execute (execute) where
4import Idris.AbsSyntax
5import Idris.AbsSyntaxTree
7import Core.TT
8import Core.Evaluate
9import Core.CaseTree
11import Debug.Trace
13import Util.DynamicLinker
14import Util.System
16import Control.Applicative hiding (Const)
17import Control.Monad.Trans
18import Control.Monad.Trans.State.Strict
19import Control.Monad.Trans.Error
20import Control.Monad
21import Data.Maybe
22import qualified Data.Map as M
24import Foreign.LibFFI
25import Foreign.C.String
26import Foreign.Marshal.Alloc (free)
27import Foreign.Ptr
29import System.IO
31-- | Attempt to perform a side effect. Return either Just the next step in
32-- evaluation (after performing the side effect through IO), or Nothing if no
33-- IO was performed.
34--
35-- This function is exceedingly generous about what it will accept in order to
36-- enable convenient testing at the REPL.
37-- step :: TT Name -> Idris (Maybe (TT Name))
38-- step tm = step' (unApply tm)
39-- where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = step arg -- Only step if arg can be stepped
40-- step' (P _ (UN "mkForeign") _, args) = stepForeign args
41-- step' (P _ (UN "prim__IO") _, [_, arg]) = return (Just arg)
42-- step' (P _ (UN "prim__readString") _, [(P _ (UN "prim__stdin") _)]) =
43-- do line <- lift $ getLine
44-- return . Just . Constant . Str $ line
45-- step' _ = return Nothing
47-- | Perform side effects until no more can be performed, then return the
48-- resulting term (possibly the argument).
49-- execute :: TT Name -> Idris (TT Name)
50-- execute tm = case unApply tm of
51-- (P _ (UN "unsafePerformIO") _, [_, arg] ) -> execute' arg
52-- _ -> return tm
53-- where execute' tm = do stepped <- step tm
54-- case stepped of
55-- Nothing -> return tm
56-- Just tm' -> execute' tm'
58data Lazy = Delayed Term | Forced Term
60data 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 , exec_handles :: M.Map Int Handle -- ^ Opened files
65 , exec_next_handle :: Int -- ^ Ensure opened file key uniqueness
66 }
68initState :: Idris ExecState
69initState = do ist <- getIState
70 return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist) M.empty 0
72type Exec = ErrorT String (StateT ExecState IO)
74runExec :: Exec a -> ExecState -> IO (Either String a)
75runExec ex st = fst <$> runStateT (runErrorT ex) st
77getExecState :: Exec ExecState
78getExecState = lift get
80putExecState :: ExecState -> Exec ()
81putExecState = lift . put
83execFail :: String -> Exec a
84execFail = throwError
86execIO :: IO a -> Exec a
87execIO = lift . lift
89thunk :: Name
90thunk = MN 0 "__execThunk"
92delay :: Term -> Exec Term
93delay tm = do st <- getExecState
94 let i = exec_next_thunk st
95 putExecState $ st { exec_thunks = M.insert i (Delayed tm) (exec_thunks st)
96 , exec_next_thunk = exec_next_thunk st + 1
97 }
98 return $ App (P Ref thunk Erased) (Constant (I i))
100force :: Int -> Exec Term
101force i = do st <- getExecState
102 let thunk = M.lookup i (exec_thunks st)
103 case thunk of
104 Just (Delayed tm) -> return tm -- FIXME DO THE EXEC
105 Just (Forced tm) -> return tm
106 Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"
108execute :: Term -> Idris Term
109execute tm = do est <- initState
110 ctxt <- getContext
111 res <- lift $ runExec (doExec [] ctxt tm) est
112 case res of
113 Left err -> fail err
114 Right tm' -> return tm'
116ioWrap :: Term -> Term
117ioWrap = App (P Ref (UN "prim__IO") Erased)
119ioUnit :: Term
120ioUnit = ioWrap (P Ref unitCon Erased)
122doExec :: Env -> Context -> Term -> Exec Term
123doExec env ctxt p@(P Ref n ty) =
124 do let val = lookupDef n ctxt
125 case val of
126 [Function _ tm] ->
127 do val <- doExec env ctxt tm
128 return val
129 [TyDecl nt ty] -> return p -- abstract def
130 [Operator tp arity op] -> do ty' <- doExec env ctxt ty
131 return (P Ref n ty')
132 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
133 doExec env ctxt tm
134 [CaseOp _ _ _ _ _ ns sc _ _] -> return p
135 thing -> trace ("got to " ++ show thing) $ undefined
136doExec env ctxt p@(P Bound n ty) = case (lookupDef n ctxt) of -- bound vars must be Function
137 [Function ty tm] -> doExec env ctxt tm
138 [] -> return p
139 x -> fail ("Internal error lookup up bound var " ++ show n ++ " - found " ++ show x)
140doExec env ctxt p@(P (DCon _ _) n _) = return p
141doExec env ctxt p@(P (TCon _ _) n _) = return p
142doExec env ctxt v@(V i) | i < length env = do let binder = env !! i
143 case binder of
144 (_, (Let t v)) -> return v
145 (_, (NLet t v)) -> return v
146 (n, b) -> doExec env ctxt (P Bound n (binderTy b))
147 | otherwise = return $ V i
148doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
149 let ctxt' = addToCtxt n v' t ctxt
150 doExec ((n, Let t v'):env) ctxt' body
151doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
152doExec env ctxt tm@(Bind n b body) = return tm -- don't eval under lambda!
153doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)
154doExec env ctxt (Constant c) = return (Constant c)
155doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
156 return ((x:xs) !! i)
157doExec env ctxt Erased = return Erased
158doExec env ctxt Impossible = fail "Tried to execute an impossible case"
159doExec env ctxt (TType u) = return (TType u)
161execApp :: Env -> Context -> (Term, [Term]) -> Exec Term
162execApp env ctxt (f, args) = do newF <- doExec env ctxt f
163 laziness <- getLaziness newF
164 newArgs <- mapM (doExec env ctxt) args
165 -- trace (show newF ++ show (zip args laziness)) $ return ()
166 execApp' env ctxt newF newArgs
167 where getLaziness (P _ (UN "lazy") _) = return [True]
168 getLaziness (P _ n _) = do est <- getExecState
169 let argInfo = exec_implicits est
170 case lookupCtxtName n argInfo of
171 [] -> return (repeat False)
172 [ps] -> return $ map lazyarg (snd ps)
173 many -> fail $ "Ambiguous " ++ show n ++ ", found " ++ show many
174 getLaziness x = return (repeat False) -- ok due to zip above
177execApp' :: Env -> Context -> Term -> [Term] -> Exec Term
178execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
179execApp' env ctxt (P _ (UN "unsafePerformIO") _) [ty, action] | (prim__IO, [ty', v]) <- unApply action = return v
181-- Special cases arising from not having access to the C RTS in the interpreter
183execApp' env ctxt (P _ (UN "mkForeign") _) [_, fn, Constant (Str arg)]
184 | Just (FFun "putStr" _ _) <- foreignFromTT fn = execIO (putStr arg) >> return ioUnit
185execApp' 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')
200execApp' env ctxt (P _ (UN "mkForeign") _) args =
201 do res <- stepForeign args
202 case res of
203 Nothing -> fail "Could not call foreign function"
204 Just r -> return r
205execApp' env ctxt (P _ (UN "prim__readString") _) [P _ (UN "prim__stdin") _] =
206 do line <- execIO getLine
207 return (Constant (Str line))
209execApp' env ctxt (P _ (UN "prim__concat") _) [Constant (Str s1), Constant (Str s2)] =
210 return $ Constant (Str (s1 ++ s2))
212execApp' env ctxt (P _ (UN "prim__eqInt") _) [Constant (I i1), Constant (I i2)] =
213 return $ if i1 == i2 then Constant (I 1) else Constant (I 0)
215execApp' env ctxt (P _ (UN "prim__ltInt") _) [Constant (I i1), Constant (I i2)] =
216 return $ if i1 < i2 then Constant (I 1) else Constant (I 0)
218execApp' env ctxt (P _ (UN "prim__subInt") _) [Constant (I i1), Constant (I i2)] =
219 return . Constant . I $ i1 - i2
221execApp' env ctxt (P _ (UN "prim__readString") _) [ptr] = trace "readString" $ undefined
223execApp' env ctxt f@(P _ n _) args =
224 do let val = lookupDef n ctxt
225 case val of
226 [Function _ tm] -> fail "should already have been eval'd"
227 [TyDecl nt ty] -> return $ mkApp f args
228 [Operator tp arity op] -> fail $ "Can't apply operator " ++ show n ++ " which needs special-casing"
229 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
230 do rhs <- doExec env ctxt tm
231 doExec env ctxt (mkApp tm args)
232 [CaseOp _ _ _ _ _ ns sc _ _] ->
233 do res <- execCase env ctxt ns sc args
234 return $ fromMaybe (mkApp f args) res
235 thing -> return $ mkApp f args
237execApp' env ctxt bnd@(Bind n b body) (arg:args) = let ctxt' = addToCtxt n arg Erased ctxt in
238 doExec ((n, b):env) ctxt' body
240execApp' env ctxt f args = return (mkApp f args)
242execCase :: Env -> Context -> [Name] -> SC -> [Term] -> Exec (Maybe Term)
243execCase env ctxt ns sc args =
244 let arity = length ns in
245 if arity <= length args
246 then do let amap = (zip ns (take arity args))
247 caseRes <- execCase' env ctxt amap sc
248 case caseRes of
249 Just res-> Just <$> doExec env ctxt (mkApp res (drop arity args))
250 Nothing -> return Nothing
251 else return Nothing
253execCase' :: Env -> Context -> [(Name, Term)] -> SC -> Exec (Maybe Term)
254execCase' env ctxt amap (STerm tm) =
255 Just <$> doExec env (foldl (\c (n, t) -> addToCtxt n t Erased c) ctxt amap) tm
256execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap
257 , Just (newCase, newBindings) <- chooseAlt tm alts =
258 execCase' env ctxt (amap ++ newBindings) newCase
259 | otherwise = return Nothing
261chooseAlt :: Term -> [CaseAlt] -> Maybe (SC, [(Name, Term)])
262chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
263chooseAlt (Constant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
264chooseAlt tm (ConCase n i ns sc : alts) | ((P _ cn _), args) <- unApply tm, cn == n = Just (sc, zip ns args)
265 | otherwise = chooseAlt tm alts
266chooseAlt tm (_:alts) = chooseAlt tm alts
267chooseAlt _ [] = Nothing
269data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
271idrisType :: FTy -> Type
272idrisType FUnit = P Ref unitTy (TType (UVal 0))
273idrisType ft = Constant (idr ft)
274 where idr FInt = IType
275 idr FFloat = FlType
276 idr FChar = ChType
277 idr FString = StrType
278 idr FPtr = PtrType
280data Foreign = FFun String [FTy] FTy deriving Show
282-- | A representation of Ptr values, which otherwise don't work in TT
283ptrCon :: Name
284ptrCon = MN 0 "__Ptr"
286-- | Convert a Haskell pointer to a Ptr term in TT
287ptr :: Ptr a -> Term
288ptr p = App (P (DCon 1 0) ptrCon Erased) (Constant (I (addr p)))
289 where addr p = p `minusPtr` nullPtr
291-- | Convert a Ptr term in TT to a Haskell pointer
292unPtr :: Term -> Maybe (Ptr a)
293unPtr (App (P _ con _) (Constant (I addr))) | con == ptrCon = Just (unAddr addr)
294 where unAddr a = nullPtr `plusPtr` a
295unPtr _ = Nothing
297-- | Convert a Haskell file handle to a handle term in TT (an int)
298handle :: Handle -> Exec Term
299handle 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)
306unHandle :: Term -> Exec Handle
307unHandle (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"
312unHandle _ = execFail "Not a handle"
314call :: Foreign -> [Term] -> Exec (Maybe Term)
315call (FFun name argTypes retType) args =
316 do fn <- findForeign name
317 case fn of
318 Nothing -> return Nothing
319 Just f -> do res <- call' f args retType
320 return . Just $ mkApp (P Ref (UN "prim__IO") Erased) [idrisType retType, res]
321 where call' :: ForeignFun -> [Term] -> FTy -> Exec Term
322 call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)
323 return (Constant (I (fromIntegral res)))
324 call' (Fun _ h) args FFloat = do res <- execIO $ callFFI h retCDouble (prepArgs args)
325 return (Constant (Fl (realToFrac res)))
326 call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)
327 return (Constant (Ch (castCCharToChar res)))
328 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
329 hStr <- execIO $ peekCString res
330-- lift $ free res
331 return (Constant (Str hStr))
333 call' (Fun _ h) args FPtr = do res <- execIO $ callFFI h (retPtr retVoid) (prepArgs args)
334 return (ptr res)
335 call' (Fun _ h) args FUnit = do res <- execIO $ callFFI h retVoid (prepArgs args)
336 return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level
337-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
340 prepArgs = map prepArg
341 prepArg (Constant (I i)) = argCInt (fromIntegral i)
342 prepArg (Constant (Fl f)) = argCDouble (realToFrac f)
343 prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
344 prepArg (Constant (Str s)) = argString s
345 prepArg ptr | Just p <- unPtr ptr = argPtr p
346 prepArg other = trace ("Could not use " ++ show other ++ " as FFI arg.") undefined
350foreignFromTT :: Term -> Maybe Foreign
351foreignFromTT t = case (unApply t) of
352 (_, [(Constant (Str name)), args, ret]) ->
353 do argTy <- unList args
354 argFTy <- sequence $ map getFTy argTy
355 retFTy <- getFTy ret
356 return $ FFun name argFTy retFTy
357 _ -> trace "failed to construct ffun" Nothing
359getFTy :: Term -> Maybe FTy
360getFTy (P _ (UN t) _) = case t of
361 "FInt" -> Just FInt
362 "FFloat" -> Just FFloat
363 "FChar" -> Just FChar
364 "FString" -> Just FString
365 "FPtr" -> Just FPtr
366 "FUnit" -> Just FUnit
367 _ -> Nothing
368getFTy _ = Nothing
370unList :: Term -> Maybe [Term]
371unList tm = case unApply tm of
372 (nil, [_]) -> Just []
373 (cons, ([_, x, xs])) ->
374 do rest <- unList xs
375 return $ x:rest
376 (f, args) -> Nothing
378toConst :: Term -> Maybe Const
379toConst (Constant c) = Just c
380toConst _ = Nothing
382stepForeign :: [Term] -> Exec (Maybe Term)
383stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
384 f' <- case (call <$> ffun) of
385 Just f -> f args
386 Nothing -> return Nothing
387 return f'
388stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"
390mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
391mapMaybeM f [] = return []
392mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
393 x' <- f x
394 case x' of
395 Just x'' -> return (x'':rest)
396 Nothing -> return rest
398findForeign :: String -> Exec (Maybe ForeignFun)
399findForeign fn = do est <- getExecState
400 let libs = exec_dynamic_libs est
401 fns <- mapMaybeM getFn libs
402 case fns of
403 [f] -> return (Just f)
404 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
405 return Nothing
406 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
407 show (length fs) ++ " occurrences."
408 return Nothing
409 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)