git.iko.soy/Idris-dev
on ace080c 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) = return (P (DCon 0 0) (MN i "THUNK") Erased) --(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, 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 tm -> return tm
183doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)
184doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)
185doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))
186 | otherwise = execFail "env too small"
187doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
188 doExec ((n, v'):env) ctxt body
189doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
190doExec env ctxt tm@(Bind n b body) = return $
191 EBind n (fmap (\_->EErased) b)
192 (\arg -> doExec ((n, arg):env) ctxt body)
193doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)
194doExec env ctxt (Constant c) = return (EConstant c)
195doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
196 doExec env ctxt ((x:xs) !! i)
197doExec env ctxt Erased = return EErased
198doExec env ctxt Impossible = fail "Tried to execute an impossible case"
199doExec env ctxt (TType u) = return (EType u)
201execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal
202execApp env ctxt (f, args) = do newF <- doExec env ctxt f
203 laziness <- (++ repeat False) <$> (getLaziness newF)
204 newArgs <- mapM argExec (zip args laziness)
205 execApp' env ctxt newF newArgs
206 where getLaziness (EP _ (UN "lazy") _) = return [False, True]
207 getLaziness (EP _ n _) = do est <- getExecState
208 let argInfo = exec_implicits est
209 case lookupCtxtName n argInfo of
210 [] -> return (repeat False)
211 [ps] -> return $ map lazyarg (snd ps)
212 many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)
213 getLaziness _ = return (repeat False) -- ok due to zip above
214 argExec :: (Term, Bool) -> Exec ExecVal
215 argExec (tm, False) = doExec env ctxt tm
216 argExec (tm, True) = delay env ctxt tm
219execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
220execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
221execApp' env ctxt (EP _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =
222 execApp' env ctxt v rest
224execApp' env ctxt (EP _ (UN "io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =
225 do v'' <- tryForce v'
226 res <- execApp' env ctxt k [v''] >>= tryForce
227 execApp' env ctxt res rest
228execApp' env ctxt con@(EP _ (UN "io_return") _) args@(tp:v:rest) =
229 do v' <- tryForce v
230 execApp' env ctxt (mkEApp con [tp, v']) rest
232-- Special cases arising from not having access to the C RTS in the interpreter
233execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)
234 | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)
235 execApp' env ctxt ioUnit rest
236execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
237 | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do m <- case mode of
238 "r" -> return ReadMode
239 "w" -> return WriteMode
240 "a" -> return AppendMode
241 "rw" -> return ReadWriteMode
242 "wr" -> return ReadWriteMode
243 "r+" -> return ReadWriteMode
244 _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
245 h <- execIO $ openFile f m
246 execApp' env ctxt (ioWrap (EHandle h)) rest
248execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
249 | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do eofp <- execIO $ hIsEOF h
250 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
251 execApp' env ctxt res rest
253execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
254 | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do execIO $ hClose h
255 execApp' env ctxt ioUnit rest
258execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun _ argTs retT) <- foreignFromTT fn
259 , length xs >= length argTs =
260 do res <- stepForeign (ty:fn:take (length argTs) xs)
261 case res of
262 Nothing -> fail "Could not call foreign function"
263 Just r -> return (mkEApp r (drop (length argTs) xs))
264 | otherwise = return (mkEApp f args)
266execApp' env ctxt f@(EP _ n _) args =
267 do let val = lookupDef n ctxt
268 case val of
269 [Function _ tm] -> fail "should already have been eval'd"
270 [TyDecl nt ty] -> return $ mkEApp f args
271 [Operator tp arity op] ->
272 if length args >= arity
273 then do args' <- mapM tryForce $ take arity args
274 case getOp n args' of
275 Just res -> do r <- res
276 execApp' env ctxt r (drop arity args)
277 Nothing -> return (mkEApp f args)
278 else return (mkEApp f args)
279 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
280 do rhs <- doExec env ctxt tm
281 execApp' env ctxt rhs args
282 [CaseOp _ _ _ _ _ ns sc _ _] ->
283 do res <- execCase env ctxt ns sc args
284 return $ fromMaybe (mkEApp f args) res
285 thing -> return $ mkEApp f args
286 where getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
287 getOp (UN "prim__addInt") [EConstant (I i1), EConstant (I i2)] =
288 primRes I (i1 + i2)
289 getOp (UN "prim__charToInt") [EConstant (Ch c)] =
290 primRes I (fromEnum c)
291 getOp (UN "prim__concat") [EConstant (Str s1), EConstant (Str s2)] =
292 primRes Str (s1 ++ s2)
293 getOp (UN "prim__eqChar") [EConstant (Ch c1), EConstant (Ch c2)] =
294 primResBool (c1 == c2)
295 getOp (UN "prim__eqInt") [EConstant (I i1), EConstant (I i2)] =
296 primResBool (i1 == i2)
297 getOp (UN "prim__eqString") [EConstant (Str s1), EConstant (Str s2)] =
298 primResBool (s1 == s2)
299 getOp (UN "prim__intToFloat") [EConstant (I i)] =
300 primRes Fl (fromRational (toRational i))
301 getOp (UN "prim__intToStr") [EConstant (I i)] =
302 primRes Str (show i)
303 getOp (UN "prim__ltInt") [EConstant (I i1), EConstant (I i2)] =
304 primResBool (i1 < i2)
305 getOp (UN "prim__mulBigInt") [EConstant (BI i1), EConstant (BI i2)] =
306 primRes BI (i1 * i2)
307 getOp (UN "prim__mulFloat") [EConstant (Fl i1), EConstant (Fl i2)] =
308 primRes Fl (i1 * i2)
309 getOp (UN "prim__mulInt") [EConstant (I i1), EConstant (I i2)] =
310 primRes I (i1 * i2)
311 getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
312 Just $ do line <- execIO getLine
313 return (EConstant (Str line))
314 getOp (UN "prim__readString") [EHandle h] =
315 Just $ do contents <- execIO $ hGetLine h
316 return (EConstant (Str contents))
317 getOp (UN "prim__strCons") [EConstant (Ch c), EConstant (Str s)] =
318 primRes Str (c:s)
319 getOp (UN "prim__strHead") [EConstant (Str (c:s))] =
320 primRes Ch c
321 getOp (UN "prim__strRev") [EConstant (Str s)] =
322 primRes Str (reverse s)
323 getOp (UN "prim__strTail") [EConstant (Str (c:s))] =
324 primRes Str s
325 getOp (UN "prim__subFloat") [EConstant (Fl i1), EConstant (Fl i2)] =
326 primRes Fl (i1 - i2)
327 getOp (UN "prim__subInt") [EConstant (I i1), EConstant (I i2)] =
328 primRes I (i1 - i2)
329 getOp n args = trace ("No prim " ++ show n ++ " for " ++ take 1000 (show args)) Nothing
331 primRes :: (a -> Const) -> a -> Maybe (Exec ExecVal)
332 primRes constr = Just . return . EConstant . constr
334 primResBool :: Bool -> Maybe (Exec ExecVal)
335 primResBool b = primRes I (if b then 1 else 0)
337execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
338 let (f', as) = unApplyV ret
339 execApp' env ctxt f' (as ++ args)
340execApp' env ctxt (EThunk i) args = do f <- force i
341 execApp' env ctxt f args
342execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)
343execApp' env ctxt f args = return (mkEApp f args)
349-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
350-- evaluates them, then begins the checks for matching cases.
351execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
352execCase env ctxt ns sc args =
353 let arity = length ns in
354 if arity <= length args
355 then do let amap = zip ns args
356 caseRes <- execCase' env ctxt amap sc
357 case caseRes of
358 Just res -> Just <$> execApp' (map (\(n, tm) -> (n, 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, 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)