git.iko.soy/Idris-dev
on b82cec2 help sign in
Idris-dev/src/Core/Execute.hs
501 lines 23 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
32data Lazy = Delayed ExecEnv Context Term | Forced ExecVal
34data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs
35 , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness
36 , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad
37 , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
38 , exec_handles :: M.Map Int Handle -- ^ Opened files
39 , exec_next_handle :: Int -- ^ Ensure opened file key uniqueness
40 }
42data ExecVal = EP NameType Name ExecVal
43 | EV Int
44 | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)
45 | EApp ExecVal ExecVal
46 | EType UExp
47 | EErased
48 | EConstant Const
49-- | ETmp Int
50 | EThunk Int
51 | EHandle Int
53instance Show ExecVal where
54 show (EP _ n _) = show n
55 show (EV i) = "!!V" ++ show i ++ "!!"
56 show (EBind n b body) = "EBind " ++ show b ++ " <<fn>> "
57 show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
58 show (EType _) = "Type"
59 show EErased = "[__]"
60 show (EConstant c) = show c
61 show (EThunk i) = "<<thunk " ++ show i ++ ">>"
62 show (EHandle i) = "<<handle " ++ show i ++ ">>"
64toTT :: ExecVal -> Exec Term
65toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
66toTT (EV i) = return $ V i
67toTT (EBind n b body) = do body' <- body $ EP Bound n EErased
68 b' <- fixBinder b
69 Bind n b' <$> toTT body'
70 where fixBinder (Lam t) = Lam <$> toTT t
71 fixBinder (Pi t) = Pi <$> toTT t
72 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
73 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
74 fixBinder (Hole t) = Hole <$> toTT t
75 fixBinder (GHole t) = GHole <$> toTT t
76 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
77 fixBinder (PVar t) = PVar <$> toTT t
78 fixBinder (PVTy t) = PVTy <$> toTT t
79toTT (EApp e1 e2) = do e1' <- toTT e1
80 e2' <- toTT e2
81 return $ App e1' e2'
82toTT (EType u) = return $ TType u
83toTT EErased = return Erased
84toTT (EConstant c) = return (Constant c)
85toTT (EThunk _) = return Erased
86toTT (EHandle _) = return Erased
88unApplyV :: ExecVal -> (ExecVal, [ExecVal])
89unApplyV tm = ua [] tm
90 where ua args (EApp f a) = ua (a:args) f
91 ua args t = (t, args)
93mkEApp :: ExecVal -> [ExecVal] -> ExecVal
94mkEApp f [] = f
95mkEApp f (a:args) = mkEApp (EApp f a) args
97initState :: Idris ExecState
98initState = do ist <- getIState
99 return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist) M.empty 0
101type Exec = ErrorT String (StateT ExecState IO)
103runExec :: Exec a -> ExecState -> IO (Either String a)
104runExec ex st = fst <$> runStateT (runErrorT ex) st
106getExecState :: Exec ExecState
107getExecState = lift get
109putExecState :: ExecState -> Exec ()
110putExecState = lift . put
112execFail :: String -> Exec a
113execFail = throwError
115execIO :: IO a -> Exec a
116execIO = lift . lift
118delay :: ExecEnv -> Context -> Term -> Exec ExecVal
119delay env ctxt tm =
120 do st <- getExecState
121 let i = exec_next_thunk st
122 putExecState $ st { exec_thunks = M.insert i (Delayed env ctxt tm) (exec_thunks st)
123 , exec_next_thunk = exec_next_thunk st + 1
124 }
125 return $ EThunk i
127force :: Int -> Exec ExecVal
128force i = do st <- getExecState
129 case M.lookup i (exec_thunks st) of
130 Just (Delayed env ctxt tm) -> do tm' <- doExec env ctxt tm
131 case tm' of
132 EThunk i ->
133 do res <- force i
134 update res i
135 return res
136 _ -> do update tm' i
137 return tm'
138 Just (Forced tm) -> return tm
139 Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"
140 where update :: ExecVal -> Int -> Exec ()
141 update tm i = do est <- getExecState
142 putExecState $ est { exec_thunks = M.insert i (Forced tm) (exec_thunks est) }
144tryForce :: ExecVal -> Exec ExecVal
145tryForce (EThunk i) = force i
146tryForce tm = return tm
148execute :: Term -> Idris Term
149execute tm = do est <- initState
150 ctxt <- getContext
151 res <- lift $ flip runExec est $ do res <- doExec [] ctxt tm
152 trace ("Result: " ++ show res) $ return ()
153 toTT res
154 case res of
155 Left err -> fail err
156 Right tm' -> return tm'
158ioWrap :: ExecVal -> ExecVal
159ioWrap tm = mkEApp (EP (DCon 0 2) (UN "prim__IO") EErased) [EErased, tm]
161ioUnit :: ExecVal
162ioUnit = ioWrap (EP Ref unitCon EErased)
164type ExecEnv = [(Name, Binder ExecVal)]
166doExec :: ExecEnv -> Context -> Term -> Exec ExecVal
167doExec env ctxt p@(P Ref n ty) =
168 do let val = lookupDef n ctxt
169 case val of
170 [Function _ tm] -> doExec env ctxt tm
171 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def
172 [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later
173 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
174 doExec env ctxt tm
175 [CaseOp _ _ _ _ _ ns sc _ _] -> return (EP Ref n EErased)
176 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined
177doExec env ctxt p@(P Bound n ty) =
178 case lookup n env of
179 Nothing -> execFail "not found"
180 Just (Let _ tm) -> return tm
181 Just b -> execFail $ "Unknown binder " ++ show b
182doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)
183doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)
184doExec env ctxt v@(V i) | i < length env = do let binder = env !! i
185 case binder of
186 (_, (Let t v)) -> return v
187 (_, (NLet t v)) -> return v
188 (n, b) -> doExec env ctxt (P Bound n Erased)
189 | otherwise = execFail "env too small"
190doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
191 doExec ((n, Let EErased v'):env) ctxt body
192doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
193doExec env ctxt tm@(Bind n b body) = return $
194 EBind n (fmap (\_->EErased) b)
195 (\arg -> doExec ((n, Let EErased arg):env) ctxt body)
196doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)
197doExec env ctxt (Constant c) = return (EConstant c)
198doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
199 doExec env ctxt ((x:xs) !! i)
200doExec env ctxt Erased = return EErased
201doExec env ctxt Impossible = fail "Tried to execute an impossible case"
202doExec env ctxt (TType u) = return (EType u)
204execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal
205execApp env ctxt (f, args) = do newF <- doExec env ctxt f
206 laziness <- (getLaziness newF) >>= return . (++ repeat False)
207 newArgs <- mapM argExec (zip args laziness)
208 execApp' env ctxt newF newArgs
209 where getLaziness (EP _ (UN "lazy") _) = return [True]
210 getLaziness (EP _ n _) = do est <- getExecState
211 let argInfo = exec_implicits est
212 case lookupCtxtName n argInfo of
213 [] -> return (repeat False)
214 [ps] -> return $ map lazyarg (snd ps)
215 many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)
216 getLaziness _ = return (repeat False) -- ok due to zip above
217 argExec :: (Term, Bool) -> Exec ExecVal
218 argExec (tm, False) = doExec env ctxt tm
219 argExec (tm, True) = delay env ctxt tm
222execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
223execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
224execApp' env ctxt (EP _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =
225 execApp' env ctxt v rest
227execApp' env ctxt (EP _ (UN "io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =
228 trace ("io_bind " ++ take 1000 (show args)) $
229 do res <- execApp' env ctxt k [v'] >>= tryForce
230 trace ("io_bind result was " ++ take 1000 (show res)) $ return ()
231 execApp' env ctxt res rest
233-- Special cases arising from not having access to the C RTS in the interpreter
234execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)
235 | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)
236 execApp' env ctxt ioUnit rest
237execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
238 | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do m <- case mode of
239 "r" -> return ReadMode
240 "w" -> return WriteMode
241 "a" -> return AppendMode
242 "rw" -> return ReadWriteMode
243 "wr" -> return ReadWriteMode
244 "r+" -> return ReadWriteMode
245 _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
246 h <- execIO $ openFile f m
247 h' <- handle h
248 execApp' env ctxt (ioWrap h') rest
250execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:fh:rest)
251 | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do h <- unHandle fh
252 eofp <- execIO $ hIsEOF h
253 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
254 execApp' env ctxt res rest
256execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:fh:rest)
257 | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do h <- unHandle fh
258 execIO $ hClose h
259 execApp' env ctxt ioUnit rest
262execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun _ argTs retT) <- foreignFromTT fn
263 , length xs >= length argTs =
264 do res <- stepForeign (ty:fn:take (length argTs) xs)
265 case res of
266 Nothing -> fail "Could not call foreign function"
267 Just r -> return (mkEApp r (drop (length argTs) xs))
268 | otherwise = return (mkEApp f args)
270execApp' env ctxt f@(EP _ n _) args =
271 do let val = lookupDef n ctxt
272 case val of
273 [Function _ tm] -> fail "should already have been eval'd"
274 [TyDecl nt ty] -> return $ mkEApp f args
275 [Operator tp arity op] ->
276 case getOp n (take arity args) of
277 Just res -> do r <- res
278 execApp' env ctxt r (drop arity args)
279 Nothing -> return (mkEApp f args)
280 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
281 do rhs <- doExec env ctxt tm
282 execApp' env ctxt rhs args
283 [CaseOp _ _ _ _ _ ns sc _ _] ->
284 do res <- execCase env ctxt ns sc args
285 return $ fromMaybe (mkEApp f args) res
286 thing -> return $ mkEApp f args
287 where getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
288 getOp (UN "prim__concat") [EConstant (Str s1), EConstant (Str s2)] =
289 Just . return . EConstant . Str $ s1 ++ s2
290 getOp (UN "prim__eqInt") [EConstant (I i1), EConstant (I i2)] =
291 Just . return . EConstant . I $ if i1 == i2 then 1 else 0
292 getOp (UN "prim__ltInt") [EConstant (I i1), EConstant (I i2)] =
293 Just . return . EConstant . I $ if i1 < i2 then 1 else 0
294 getOp (UN "prim__subInt") [EConstant (I i1), EConstant (I i2)] =
295 Just . return . EConstant . I $ i1 - i2
296 getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
297 Just $ do line <- execIO getLine
298 return (EConstant (Str line))
299 getOp (UN "prim__readString") [ptr] =
300 Just $ do h <- unHandle ptr
301 contents <- execIO $ hGetLine h
302 return $ ioWrap (EConstant (Str contents))
303 getOp _ _ = Nothing
304execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
305 let (f', as) = unApplyV ret
306 execApp' env ctxt f' (as ++ args)
307execApp' env ctxt (EThunk i) args = do f <- force i
308 execApp' env ctxt f args
309execApp' env ctxt f args = return (mkEApp f args)
312-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
313-- evaluates them, then begins the checks for matching cases.
314execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
315execCase env ctxt ns sc args =
316 let arity = length ns in
317 if arity <= length args
318 then do -- args' <- mapM tryForce (take arity args)
319 let amap = zip ns args
320 caseRes <- execCase' env ctxt amap sc
321 case caseRes of
322 Just res -> Just <$> execApp' (map (\(n, tm) -> (n, Let EErased tm)) amap ++ env) ctxt res (drop arity args)
323 Nothing -> return Nothing
324 else return Nothing
326-- | Take bindings and a case tree and examines them, executing the matching case if possible.
327execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
328execCase' env ctxt amap (UnmatchedCase _) = return Nothing
329execCase' env ctxt amap (STerm tm) =
330 Just <$> doExec (map (\(n, v) -> (n, Let EErased v)) amap ++ env) ctxt tm
331execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
332 do tm' <- tryForce tm
333 case chooseAlt tm alts of
334 Just (newCase, newBindings) ->
335 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
336 execCase' env ctxt amap' newCase
337 Nothing -> return Nothing
339chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
340chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
341chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
342chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
343 , cn == n = Just (sc, zip ns args)
344 | otherwise = chooseAlt tm alts
345chooseAlt tm (_:alts) = chooseAlt tm alts
346chooseAlt _ [] = Nothing
348data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
350idrisType :: FTy -> ExecVal
351idrisType FUnit = EP Ref unitTy EErased
352idrisType ft = EConstant (idr ft)
353 where idr FInt = IType
354 idr FFloat = FlType
355 idr FChar = ChType
356 idr FString = StrType
357 idr FPtr = PtrType
359data Foreign = FFun String [FTy] FTy deriving Show
361-- | A representation of Ptr values, which otherwise don't work in TT
362ptrCon :: Name
363ptrCon = MN 0 "__Ptr"
365-- | Convert a Haskell pointer to a Ptr term in TT
366ptr :: Ptr a -> ExecVal
367ptr p = EApp (EP (DCon 0 1) ptrCon EErased) (EConstant (I (addr p)))
368 where addr p = p `minusPtr` nullPtr
370-- | Convert a Ptr term in TT to a Haskell pointer
371unPtr :: ExecVal -> Maybe (Ptr a)
372unPtr (EApp (EP _ con _) (EConstant (I addr))) | con == ptrCon = Just (unAddr addr)
373 where unAddr a = nullPtr `plusPtr` a
374unPtr _ = Nothing
376handleCon :: Name
377handleCon = MN 0 "__Handle"
379-- | Convert a Haskell file handle to a handle term in TT (an int)
380handle :: Handle -> Exec ExecVal
381handle h = do est <- getExecState
382 let i = exec_next_handle est
383 putExecState $ est { exec_next_handle = exec_next_handle est + 1
384 , exec_handles = M.insert i h (exec_handles est)
385 }
386 return $ EHandle i
388unHandle :: ExecVal -> Exec Handle
389unHandle (EHandle i) =
390 do est <- getExecState
391 case M.lookup i (exec_handles est) of
392 Just h -> return h
393 Nothing -> execFail "Bad handle ID"
394unHandle _ = execFail "Not a handle"
396call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
397call (FFun name argTypes retType) args =
398 do fn <- findForeign name
399 case fn of
400 Nothing -> return Nothing
401 Just f -> do res <- call' f args retType
402 return . Just . ioWrap $ res
403 where call' :: ForeignFun -> [ExecVal] -> FTy -> Exec ExecVal
404 call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)
405 return (EConstant (I (fromIntegral res)))
406 call' (Fun _ h) args FFloat = do res <- execIO $ callFFI h retCDouble (prepArgs args)
407 return (EConstant (Fl (realToFrac res)))
408 call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)
409 return (EConstant (Ch (castCCharToChar res)))
410 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
411 hStr <- execIO $ peekCString res
412-- lift $ free res
413 return (EConstant (Str hStr))
415 call' (Fun _ h) args FPtr = do res <- execIO $ callFFI h (retPtr retVoid) (prepArgs args)
416 return (ptr res)
417 call' (Fun _ h) args FUnit = do res <- execIO $ callFFI h retVoid (prepArgs args)
418 return (EP Ref unitCon EErased)
419-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
422 prepArgs = map prepArg
423 prepArg (EConstant (I i)) = argCInt (fromIntegral i)
424 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
425 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
426 prepArg (EConstant (Str s)) = argString s
427 prepArg ptr | Just p <- unPtr ptr = argPtr p
428 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
432foreignFromTT :: ExecVal -> Maybe Foreign
433foreignFromTT t = case (unApplyV t) of
434 (_, [(EConstant (Str name)), args, ret]) ->
435 do argTy <- unEList args
436 argFTy <- sequence $ map getFTy argTy
437 retFTy <- getFTy ret
438 return $ FFun name argFTy retFTy
439 _ -> trace "failed to construct ffun" Nothing
441getFTy :: ExecVal -> Maybe FTy
442getFTy (EP _ (UN t) _) =
443 case t of
444 "FInt" -> Just FInt
445 "FFloat" -> Just FFloat
446 "FChar" -> Just FChar
447 "FString" -> Just FString
448 "FPtr" -> Just FPtr
449 "FUnit" -> Just FUnit
450 _ -> Nothing
451getFTy _ = Nothing
453unList :: Term -> Maybe [Term]
454unList tm = case unApply tm of
455 (nil, [_]) -> Just []
456 (cons, ([_, x, xs])) ->
457 do rest <- unList xs
458 return $ x:rest
459 (f, args) -> Nothing
461unEList :: ExecVal -> Maybe [ExecVal]
462unEList tm = case unApplyV tm of
463 (nil, [_]) -> Just []
464 (cons, ([_, x, xs])) ->
465 do rest <- unEList xs
466 return $ x:rest
467 (f, args) -> Nothing
470toConst :: Term -> Maybe Const
471toConst (Constant c) = Just c
472toConst _ = Nothing
474stepForeign :: [ExecVal] -> Exec (Maybe ExecVal)
475stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
476 f' <- case (call <$> ffun) of
477 Just f -> f args
478 Nothing -> return Nothing
479 return f'
480stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"
482mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
483mapMaybeM f [] = return []
484mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
485 x' <- f x
486 case x' of
487 Just x'' -> return (x'':rest)
488 Nothing -> return rest
490findForeign :: String -> Exec (Maybe ForeignFun)
491findForeign fn = do est <- getExecState
492 let libs = exec_dynamic_libs est
493 fns <- mapMaybeM getFn libs
494 case fns of
495 [f] -> return (Just f)
496 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
497 return Nothing
498 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
499 show (length fs) ++ " occurrences."
500 return Nothing
501 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)