git.iko.soy/Idris-dev
on 02fa360 help sign in
Idris-dev/src/Core/Execute.hs
368 lines 17 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 }
66initState :: Idris ExecState
67initState = do ist <- getIState
68 return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)
70type Exec = ErrorT String (StateT ExecState IO)
72runExec :: Exec a -> ExecState -> IO (Either String a)
73runExec ex st = fst <$> runStateT (runErrorT ex) st
75getExecState :: Exec ExecState
76getExecState = lift get
78putExecState :: ExecState -> Exec ()
79putExecState = lift . put
81execFail :: String -> Exec a
82execFail = throwError
84execIO :: IO a -> Exec a
85execIO = lift . lift
87thunk :: Name
88thunk = MN 0 "__execThunk"
90delay :: Term -> Exec Term
91delay 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))
98force :: Int -> Exec Term
99force 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!"
106execute :: Term -> Idris Term
107execute 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'
115doExec :: Env -> Context -> Term -> Exec Term
116doExec env ctxt p@(P Ref n ty) =
117 do let val = lookupDef n ctxt
118 case val of
119 [Function _ tm] ->
120 do val <- doExec env ctxt tm
121 return val
122 [TyDecl nt ty] -> return p -- abstract def
123 [Operator tp arity op] -> do ty' <- doExec env ctxt ty
124 return (P Ref n ty')
125 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
126 doExec env ctxt tm
127 [CaseOp _ _ _ _ _ ns sc _ _] -> return p
128 thing -> trace ("got to " ++ show thing) $ undefined
129doExec env ctxt p@(P Bound n ty) = case (lookupDef n ctxt) of -- bound vars must be Function
130 [Function ty tm] -> doExec env ctxt tm
131 [] -> return p
132 x -> fail ("Internal error lookup up bound var " ++ show n ++ " - found " ++ show x)
133doExec env ctxt p@(P (DCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (DCon a b) n ty') }
134doExec env ctxt p@(P (TCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (TCon a b) n ty') }
135doExec env ctxt v@(V i) | i < length env = do let binder = env !! i
136 case binder of
137 (_, (Let t v)) -> return v
138 (_, (NLet t v)) -> return v
139 (n, b) -> doExec env ctxt (P Bound n (binderTy b))
140 | otherwise = return $ V i
141doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
142 let ctxt' = addToCtxt n v' t ctxt
143 doExec ((n, Let t v'):env) ctxt' body
144doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
145doExec env ctxt tm@(Bind n b body) = return tm -- don't eval under lambda!
146doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)
147doExec env ctxt (Constant c) = return (Constant c)
148doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
149 return ((x:xs) !! i)
150doExec env ctxt Erased = return Erased
151doExec env ctxt Impossible = fail "Tried to execute an impossible case"
152doExec env ctxt (TType u) = return (TType u)
154execApp :: Env -> Context -> (Term, [Term]) -> Exec Term
155execApp env ctxt (f, args) = do newF <- doExec env ctxt f
156 laziness <- getLaziness newF
157 newArgs <- mapM (doExec env ctxt) args
158 trace (show newF ++ show (zip args laziness)) $ return ()
159 execApp' env ctxt newF newArgs
160 where getLaziness (P _ (UN "lazy") _) = return [True]
161 getLaziness (P _ n _) = do est <- getExecState
162 let argInfo = exec_implicits est
163 case lookupCtxtName n argInfo of
164 [] -> return (repeat False)
165 [ps] -> return $ map lazyarg (snd ps)
166 many -> fail $ "Ambiguous " ++ show n ++ ", found " ++ show many
167 getLaziness x = return (repeat False) -- ok due to zip above
170execApp' :: Env -> Context -> Term -> [Term] -> Exec Term
171execApp' 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
173execApp' env ctxt (P _ (UN "mkForeign") _) args =
174 do res <- stepForeign args
175 case res of
176 Nothing -> fail "Could not call foreign function"
177 Just r -> return r
178execApp' env ctxt (P _ (UN "prim__readString") _) [P _ (UN "prim__stdin") _] =
179 do line <- execIO getLine
180 return (Constant (Str line))
182execApp' env ctxt (P _ (UN "prim__concat") _) [(Constant (Str s1)), (Constant (Str s2))] =
183 return $ Constant (Str (s1 ++ s2))
185execApp' env ctxt (P _ (UN "prim__eqInt") _) [(Constant (I i1)), (Constant (I i2))] =
186 return $ if i1 == i2 then Constant (I 1) else Constant (I 0)
188execApp' env ctxt (P _ (UN "prim__readString") _) [ptr] | Just p <- unPtr ptr =
189 do fn <- findForeign "freadStr"
190 case fn of
191 Just (Fun _ freadStr) -> do
192 res <- execIO $ callFFI freadStr retCString [argPtr p]
193 str <- execIO $ peekCString res
194 trace ("Found " ++ str) $ return ()
195 return $ Constant (Str str)
196 Nothing -> fail "Could not load freadStr"
198execApp' env ctxt f@(P _ n _) args =
199 do let val = lookupDef n ctxt
200 case val of
201 [Function _ tm] -> fail "should already have been eval'd"
202 [TyDecl nt ty] -> return $ mkApp f args
203 [Operator tp arity op] -> fail $ "Can't apply operator " ++ show n ++ " which needs special-casing"
204 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
205 do rhs <- doExec env ctxt tm
206 doExec env ctxt (mkApp tm args)
207 [CaseOp _ _ _ _ _ ns sc _ _] ->
208 do res <- execCase env ctxt ns sc args
209 return $ fromMaybe (mkApp f args) res
210 thing -> return $ mkApp f args
212execApp' env ctxt bnd@(Bind n b body) (arg:args) = let ctxt' = addToCtxt n arg Erased ctxt in
213 doExec ((n, b):env) ctxt' body
215execApp' env ctxt f args = return (mkApp f args)
217execCase :: Env -> Context -> [Name] -> SC -> [Term] -> Exec (Maybe Term)
218execCase env ctxt ns sc args =
219 let arity = length ns in
220 if arity <= length args
221 then do let amap = (zip ns (take arity args))
222 caseRes <- execCase' env ctxt amap sc
223 case caseRes of
224 Just res-> Just <$> doExec env ctxt (mkApp res (drop arity args))
225 Nothing -> return Nothing
226 else return Nothing
228execCase' :: Env -> Context -> [(Name, Term)] -> SC -> Exec (Maybe Term)
229execCase' env ctxt amap (STerm tm) =
230 Just <$> doExec env (foldl (\c (n, t) -> addToCtxt n t Erased c) ctxt amap) tm
231execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap
232 , Just (newCase, newBindings) <- chooseAlt tm alts =
233 execCase' env ctxt (amap ++ newBindings) newCase
234 | otherwise = return Nothing
236chooseAlt :: Term -> [CaseAlt] -> Maybe (SC, [(Name, Term)])
237chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
238chooseAlt (Constant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
239chooseAlt tm (ConCase n i ns sc : alts) | ((P _ cn _), args) <- unApply tm, cn == n = Just (sc, zip ns args)
240 | otherwise = chooseAlt tm alts
241chooseAlt tm (_:alts) = chooseAlt tm alts
242chooseAlt _ [] = Nothing
244data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
246idrisType :: FTy -> Type
247idrisType FUnit = P Ref unitTy (TType (UVal 0))
248idrisType ft = Constant (idr ft)
249 where idr FInt = IType
250 idr FFloat = FlType
251 idr FChar = ChType
252 idr FString = StrType
253 idr FPtr = PtrType
255data Foreign = FFun String [FTy] FTy deriving Show
257-- | A representation of Ptr values, which otherwise don't work in TT
258ptrCon :: Name
259ptrCon = MN 0 "__Ptr"
261-- | Convert a Haskell pointer to a Ptr term in TT
262ptr :: Ptr a -> Term
263ptr p = App (P (DCon 1 0) ptrCon Erased) (Constant (I (addr p)))
264 where addr p = p `minusPtr` nullPtr
266-- | Convert a Ptr term in TT to a Haskell pointer
267unPtr :: Term -> Maybe (Ptr a)
268unPtr (App (P _ con _) (Constant (I addr))) | con == ptrCon = Just (unAddr addr)
269 where unAddr a = nullPtr `plusPtr` a
270unPtr _ = Nothing
273call :: Foreign -> [Term] -> Exec (Maybe Term)
274call (FFun name argTypes retType) args =
275 do fn <- findForeign name
276 case fn of
277 Nothing -> return Nothing
278 Just f -> do res <- call' f args retType
279 return . Just $ mkApp (P Ref (UN "prim__IO") Erased) [idrisType retType, res]
280 where call' :: ForeignFun -> [Term] -> FTy -> Exec Term
281 call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)
282 return (Constant (I (fromIntegral res)))
283 call' (Fun _ h) args FFloat = do res <- execIO $ callFFI h retCDouble (prepArgs args)
284 return (Constant (Fl (realToFrac res)))
285 call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)
286 return (Constant (Ch (castCCharToChar res)))
287 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
288 hStr <- execIO $ peekCString res
289-- lift $ free res
290 return (Constant (Str hStr))
292 call' (Fun _ h) args FPtr = do res <- execIO $ callFFI h (retPtr retVoid) (prepArgs args)
293 return (ptr res)
294 call' (Fun _ h) args FUnit = do res <- execIO $ callFFI h retVoid (prepArgs args)
295 return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level
296-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
299 prepArgs = map prepArg
300 prepArg (Constant (I i)) = argCInt (fromIntegral i)
301 prepArg (Constant (Fl f)) = argCDouble (realToFrac f)
302 prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
303 prepArg (Constant (Str s)) = argString s
304 prepArg ptr | Just p <- unPtr ptr = argPtr p
305 prepArg other = trace ("Could not use " ++ show other ++ " as FFI arg.") undefined
309foreignFromTT :: Term -> Maybe Foreign
310foreignFromTT t = case (unApply t) of
311 (_, [(Constant (Str name)), args, ret]) ->
312 do argTy <- unList args
313 argFTy <- sequence $ map getFTy argTy
314 retFTy <- getFTy ret
315 return $ FFun name argFTy retFTy
316 _ -> trace "failed to construct ffun" Nothing
318getFTy :: Term -> Maybe FTy
319getFTy (P _ (UN t) _) = case t of
320 "FInt" -> Just FInt
321 "FFloat" -> Just FFloat
322 "FChar" -> Just FChar
323 "FString" -> Just FString
324 "FPtr" -> Just FPtr
325 "FUnit" -> Just FUnit
326 _ -> Nothing
327getFTy _ = Nothing
329unList :: Term -> Maybe [Term]
330unList tm = case unApply tm of
331 (nil, [_]) -> Just []
332 (cons, ([_, x, xs])) ->
333 do rest <- unList xs
334 return $ x:rest
335 (f, args) -> Nothing
337toConst :: Term -> Maybe Const
338toConst (Constant c) = Just c
339toConst _ = Nothing
341stepForeign :: [Term] -> Exec (Maybe Term)
342stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
343 f' <- case (call <$> ffun) of
344 Just f -> f args
345 Nothing -> return Nothing
346 return f'
347stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"
349mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
350mapMaybeM f [] = return []
351mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
352 x' <- f x
353 case x' of
354 Just x'' -> return (x'':rest)
355 Nothing -> return rest
357findForeign :: String -> Exec (Maybe ForeignFun)
358findForeign fn = do est <- getExecState
359 let libs = exec_dynamic_libs est
360 fns <- mapMaybeM getFn libs
361 case fns of
362 [f] -> return (Just f)
363 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
364 return Nothing
365 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
366 show (length fs) ++ " occurrences."
367 return Nothing
368 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)