git.iko.soy/Idris-dev
on 9792d64 help sign in
Idris-dev/src/Core/Execute.hs
506 lines 23 kB history raw
1{-# LANGUAGE PatternGuards, ExistentialQuantification #-}
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 deriving Show
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 }
40data ExecVal = EP NameType Name ExecVal
41 | EV Int
42 | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)
43 | EApp ExecVal ExecVal
44 | EType UExp
45 | EErased
46 | EConstant Const
47 | forall a. EPtr (Ptr a)
48 | EThunk Int
49 | EHandle Handle
51instance Show ExecVal where
52 show (EP _ n _) = show n
53 show (EV i) = "!!V" ++ show i ++ "!!"
54 show (EBind n b body) = "EBind " ++ show b ++ " <<fn>> "
55 show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
56 show (EType _) = "Type"
57 show EErased = "[__]"
58 show (EConstant c) = show c
59 show (EPtr p) = "<<ptr " ++ show p ++ ">>"
60 show (EThunk i) = "<<thunk " ++ show i ++ ">>"
61 show (EHandle h) = "<<handle " ++ show h ++ ">>"
63toTT :: ExecVal -> Exec Term
64toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
65toTT (EV i) = return $ V i
66toTT (EBind n b body) = do body' <- body $ EP Bound n EErased
67 b' <- fixBinder b
68 Bind n b' <$> toTT body'
69 where fixBinder (Lam t) = Lam <$> toTT t
70 fixBinder (Pi t) = Pi <$> toTT t
71 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
72 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
73 fixBinder (Hole t) = Hole <$> toTT t
74 fixBinder (GHole t) = GHole <$> toTT t
75 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
76 fixBinder (PVar t) = PVar <$> toTT t
77 fixBinder (PVTy t) = PVTy <$> toTT t
78toTT (EApp e1 e2) = do e1' <- toTT e1
79 e2' <- toTT e2
80 return $ App e1' e2'
81toTT (EType u) = return $ TType u
82toTT EErased = return Erased
83toTT (EConstant c) = return (Constant c)
84toTT (EThunk i) = (force i) >>= toTT
85toTT (EHandle _) = return Erased
87unApplyV :: ExecVal -> (ExecVal, [ExecVal])
88unApplyV tm = ua [] tm
89 where ua args (EApp f a) = ua (a:args) f
90 ua args t = (t, args)
92mkEApp :: ExecVal -> [ExecVal] -> ExecVal
93mkEApp f [] = f
94mkEApp f (a:args) = mkEApp (EApp f a) args
96initState :: Idris ExecState
97initState = do ist <- getIState
98 return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)
100type Exec = ErrorT String (StateT ExecState IO)
102runExec :: Exec a -> ExecState -> IO (Either String a)
103runExec ex st = fst <$> runStateT (runErrorT ex) st
105getExecState :: Exec ExecState
106getExecState = lift get
108putExecState :: ExecState -> Exec ()
109putExecState = lift . put
111execFail :: String -> Exec a
112execFail = throwError
114execIO :: IO a -> Exec a
115execIO = lift . lift
117delay :: ExecEnv -> Context -> Term -> Exec ExecVal
118delay env ctxt tm =
119 do st <- getExecState
120 let i = exec_next_thunk st
121 putExecState $ st { exec_thunks = M.insert i (Delayed env ctxt tm) (exec_thunks st)
122 , exec_next_thunk = exec_next_thunk st + 1
123 }
124 return $ EThunk i
126force :: Int -> Exec ExecVal
127force i = do st <- getExecState
128 case M.lookup i (exec_thunks st) of
129 Just (Delayed env ctxt tm) -> do tm' <- doExec env ctxt tm
130 case tm' of
131 EThunk i ->
132 do res <- force i
133 update res i
134 return res
135 _ -> do update tm' i
136 return tm'
137 Just (Forced tm) -> return tm
138 Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"
139 where update :: ExecVal -> Int -> Exec ()
140 update tm i = do est <- getExecState
141 putExecState $ est { exec_thunks = M.insert i (Forced tm) (exec_thunks est) }
143tryForce :: ExecVal -> Exec ExecVal
144tryForce (EThunk i) = force i
145tryForce tm = return tm
147debugThunks :: Exec ()
148debugThunks = do st <- getExecState
149 execIO $ putStrLn (take 4000 (show (exec_thunks st)))
151execute :: Term -> Idris Term
152execute tm = do est <- initState
153 ctxt <- getContext
154 res <- lift $ flip runExec est $ do res <- doExec [] ctxt tm
155 toTT res
156 case res of
157 Left err -> fail err
158 Right tm' -> return tm'
160ioWrap :: ExecVal -> ExecVal
161ioWrap tm = mkEApp (EP (DCon 0 2) (UN "prim__IO") EErased) [EErased, tm]
163ioUnit :: ExecVal
164ioUnit = ioWrap (EP Ref unitCon EErased)
166type ExecEnv = [(Name, Binder ExecVal)]
168doExec :: ExecEnv -> Context -> Term -> Exec ExecVal
169doExec env ctxt p@(P Ref n ty) =
170 do let val = lookupDef n ctxt
171 case val of
172 [Function _ tm] -> doExec env ctxt tm
173 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def
174 [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later
175 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
176 doExec env ctxt tm
177 [CaseOp _ _ _ _ _ ns sc _ _] -> return (EP Ref n EErased)
178 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined
179doExec env ctxt p@(P Bound n ty) =
180 case lookup n env of
181 Nothing -> execFail "not found"
182 Just (Let _ tm) -> return tm
183 Just b -> execFail $ "Unknown binder " ++ show b
184doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)
185doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)
186doExec env ctxt v@(V i) | i < length env = do let binder = env !! i
187 case binder of
188 (_, (Let t v)) -> return v
189 (_, (NLet t v)) -> return v
190 (n, b) -> doExec env ctxt (P Bound n Erased)
191 | otherwise = execFail "env too small"
192doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
193 doExec ((n, Let EErased v'):env) ctxt body
194doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
195doExec env ctxt tm@(Bind n b body) = return $
196 EBind n (fmap (\_->EErased) b)
197 (\arg -> doExec ((n, Let EErased arg):env) ctxt body)
198doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)
199doExec env ctxt (Constant c) = return (EConstant c)
200doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
201 doExec env ctxt ((x:xs) !! i)
202doExec env ctxt Erased = return EErased
203doExec env ctxt Impossible = fail "Tried to execute an impossible case"
204doExec env ctxt (TType u) = return (EType u)
206execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal
207execApp env ctxt (f, args) = do newF <- doExec env ctxt f
208 laziness <- (++ repeat False) <$> (getLaziness newF)
209 newArgs <- mapM argExec (zip args laziness)
210 execApp' env ctxt newF newArgs
211 where getLaziness (EP _ (UN "lazy") _) = return [True]
212 getLaziness (EP _ n _) = do est <- getExecState
213 let argInfo = exec_implicits est
214 case lookupCtxtName n argInfo of
215 [] -> return (repeat False)
216 [ps] -> return $ map lazyarg (snd ps)
217 many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)
218 getLaziness _ = return (repeat False) -- ok due to zip above
219 argExec :: (Term, Bool) -> Exec ExecVal
220 argExec (tm, False) = doExec env ctxt tm
221 argExec (tm, True) = delay env ctxt tm
224execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
225execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
226execApp' env ctxt (EP _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =
227 execApp' env ctxt v rest
229execApp' env ctxt (EP _ (UN "io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =
230 do res <- execApp' env ctxt k [v'] >>= tryForce
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 execApp' env ctxt (ioWrap (EHandle h)) rest
249execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
250 | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do eofp <- execIO $ hIsEOF h
251 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
252 execApp' env ctxt res rest
254execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
255 | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do execIO $ hClose h
256 execApp' env ctxt ioUnit rest
259execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun _ argTs retT) <- foreignFromTT fn
260 , length xs >= length argTs =
261 do res <- stepForeign (ty:fn:take (length argTs) xs)
262 case res of
263 Nothing -> fail "Could not call foreign function"
264 Just r -> return (mkEApp r (drop (length argTs) xs))
265 | otherwise = return (mkEApp f args)
267execApp' env ctxt f@(EP _ n _) args =
268 do let val = lookupDef n ctxt
269 case val of
270 [Function _ tm] -> fail "should already have been eval'd"
271 [TyDecl nt ty] -> return $ mkEApp f args
272 [Operator tp arity op] ->
273 if length args >= arity
274 then do args' <- mapM tryForce $ take arity args
275 case getOp n args' of
276 Just res -> do r <- res
277 execApp' env ctxt r (drop arity args)
278 Nothing -> return (mkEApp f args)
279 else 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__addInt") [EConstant (I i1), EConstant (I i2)] =
289 primRes I (i1 + i2)
290 getOp (UN "prim__charToInt") [EConstant (Ch c)] =
291 primRes I (fromEnum c)
292 getOp (UN "prim__concat") [EConstant (Str s1), EConstant (Str s2)] =
293 primRes Str (s1 ++ s2)
294 getOp (UN "prim__eqChar") [EConstant (Ch c1), EConstant (Ch c2)] =
295 primResBool (c1 == c2)
296 getOp (UN "prim__eqInt") [EConstant (I i1), EConstant (I i2)] =
297 primResBool (i1 == i2)
298 getOp (UN "prim__eqString") [EConstant (Str s1), EConstant (Str s2)] =
299 primResBool (s1 == s2)
300 getOp (UN "prim__intToFloat") [EConstant (I i)] =
301 primRes Fl (fromRational (toRational i))
302 getOp (UN "prim__ltInt") [EConstant (I i1), EConstant (I i2)] =
303 primResBool (i1 < i2)
304 getOp (UN "prim__mulBigInt") [EConstant (BI i1), EConstant (BI i2)] =
305 primRes BI (i1 * i2)
306 getOp (UN "prim__mulFloat") [EConstant (Fl i1), EConstant (Fl i2)] =
307 primRes Fl (i1 * i2)
308 getOp (UN "prim__mulInt") [EConstant (I i1), EConstant (I i2)] =
309 primRes I (i1 * i2)
310 getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
311 Just $ do line <- execIO getLine
312 return (EConstant (Str line))
313 getOp (UN "prim__readString") [EHandle h] =
314 Just $ do contents <- execIO $ hGetLine h
315 return (EConstant (Str contents))
316 getOp (UN "prim__strCons") [EConstant (Ch c), EConstant (Str s)] =
317 primRes Str (c:s)
318 getOp (UN "prim__strHead") [EConstant (Str (c:s))] =
319 primRes Ch c
320 getOp (UN "prim__strRev") [EConstant (Str s)] =
321 primRes Str (reverse s)
322 getOp (UN "prim__strTail") [EConstant (Str (c:s))] =
323 primRes Str s
324 getOp (UN "prim__subFloat") [EConstant (Fl i1), EConstant (Fl i2)] =
325 primRes Fl (i1 - i2)
326 getOp (UN "prim__subInt") [EConstant (I i1), EConstant (I i2)] =
327 primRes I (i1 - i2)
328 getOp n args = trace ("No prim " ++ show n ++ " for " ++ take 1000 (show args)) Nothing
330 primRes :: (a -> Const) -> a -> Maybe (Exec ExecVal)
331 primRes constr = Just . return . EConstant . constr
333 primResBool :: Bool -> Maybe (Exec ExecVal)
334 primResBool b = primRes I (if b then 1 else 0)
336execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
337 let (f', as) = unApplyV ret
338 execApp' env ctxt f' (as ++ args)
339execApp' env ctxt (EThunk i) args = do f <- force i
340 execApp' env ctxt f args
341execApp' env ctxt f args = return (mkEApp f args)
347-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
348-- evaluates them, then begins the checks for matching cases.
349execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
350execCase env ctxt ns sc args =
351 let arity = length ns in
352 if arity <= length args
353 then do let amap = zip ns args
354-- debugThunks
355-- trace ("Case exec in " ++ take 1000 (show amap) ++ "\nwith " ++ show sc++"\n") $ return ()
356 caseRes <- execCase' env ctxt amap sc
357 case caseRes of
358 Just res -> Just <$> execApp' (map (\(n, tm) -> (n, Let EErased tm)) amap ++ env) ctxt res (drop arity args)
359 Nothing -> return Nothing
360 else return Nothing
362-- | Take bindings and a case tree and examines them, executing the matching case if possible.
363execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
364execCase' env ctxt amap (UnmatchedCase _) = return Nothing
365execCase' env ctxt amap (STerm tm) =
366 Just <$> doExec (map (\(n, v) -> (n, Let EErased v)) amap ++ env) ctxt tm
367execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
368 do tm' <- tryForce tm
369 case chooseAlt tm alts of
370 Just (newCase, newBindings) ->
371 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
372 execCase' env ctxt amap' newCase
373 Nothing -> return Nothing
375chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
376chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
377chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
378chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
379 , cn == n = Just (sc, zip ns args)
380 | otherwise = chooseAlt tm alts
381chooseAlt tm (_:alts) = chooseAlt tm alts
382chooseAlt _ [] = Nothing
387data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
389idrisType :: FTy -> ExecVal
390idrisType FUnit = EP Ref unitTy EErased
391idrisType ft = EConstant (idr ft)
392 where idr FInt = IType
393 idr FFloat = FlType
394 idr FChar = ChType
395 idr FString = StrType
396 idr FPtr = PtrType
398data Foreign = FFun String [FTy] FTy deriving Show
401call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
402call (FFun name argTypes retType) args =
403 do fn <- findForeign name
404 case fn of
405 Nothing -> return Nothing
406 Just f -> do res <- call' f args retType
407 return . Just . ioWrap $ res
408 where call' :: ForeignFun -> [ExecVal] -> FTy -> Exec ExecVal
409 call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)
410 return (EConstant (I (fromIntegral res)))
411 call' (Fun _ h) args FFloat = do res <- execIO $ callFFI h retCDouble (prepArgs args)
412 return (EConstant (Fl (realToFrac res)))
413 call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)
414 return (EConstant (Ch (castCCharToChar res)))
415 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
416 hStr <- execIO $ peekCString res
417-- lift $ free res
418 return (EConstant (Str hStr))
420 call' (Fun _ h) args FPtr = do res <- execIO $ callFFI h (retPtr retVoid) (prepArgs args)
421 return (EPtr res)
422 call' (Fun _ h) args FUnit = do res <- execIO $ callFFI h retVoid (prepArgs args)
423 return (EP Ref unitCon EErased)
424-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
427 prepArgs = map prepArg
428 prepArg (EConstant (I i)) = argCInt (fromIntegral i)
429 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
430 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
431 prepArg (EConstant (Str s)) = argString s
432 prepArg (EPtr p) = argPtr p
433 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
437foreignFromTT :: ExecVal -> Maybe Foreign
438foreignFromTT t = case (unApplyV t) of
439 (_, [(EConstant (Str name)), args, ret]) ->
440 do argTy <- unEList args
441 argFTy <- sequence $ map getFTy argTy
442 retFTy <- getFTy ret
443 return $ FFun name argFTy retFTy
444 _ -> trace "failed to construct ffun" Nothing
446getFTy :: ExecVal -> Maybe FTy
447getFTy (EP _ (UN t) _) =
448 case t of
449 "FInt" -> Just FInt
450 "FFloat" -> Just FFloat
451 "FChar" -> Just FChar
452 "FString" -> Just FString
453 "FPtr" -> Just FPtr
454 "FUnit" -> Just FUnit
455 _ -> Nothing
456getFTy _ = Nothing
458unList :: Term -> Maybe [Term]
459unList tm = case unApply tm of
460 (nil, [_]) -> Just []
461 (cons, ([_, x, xs])) ->
462 do rest <- unList xs
463 return $ x:rest
464 (f, args) -> Nothing
466unEList :: ExecVal -> Maybe [ExecVal]
467unEList tm = case unApplyV tm of
468 (nil, [_]) -> Just []
469 (cons, ([_, x, xs])) ->
470 do rest <- unEList xs
471 return $ x:rest
472 (f, args) -> Nothing
475toConst :: Term -> Maybe Const
476toConst (Constant c) = Just c
477toConst _ = Nothing
479stepForeign :: [ExecVal] -> Exec (Maybe ExecVal)
480stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
481 f' <- case (call <$> ffun) of
482 Just f -> f args
483 Nothing -> return Nothing
484 return f'
485stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"
487mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
488mapMaybeM f [] = return []
489mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
490 x' <- f x
491 case x' of
492 Just x'' -> return (x'':rest)
493 Nothing -> return rest
495findForeign :: String -> Exec (Maybe ForeignFun)
496findForeign fn = do est <- getExecState
497 let libs = exec_dynamic_libs est
498 fns <- mapMaybeM getFn libs
499 case fns of
500 [f] -> return (Just f)
501 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
502 return Nothing
503 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
504 show (length fs) ++ " occurrences."
505 return Nothing
506 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)