git.iko.soy/Idris-dev
on 00ae7fe help sign in
Idris-dev/src/Core/Execute.hs
316 lines 15 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
19import Data.Maybe
20import qualified Data.Map as M
22import Foreign.LibFFI
23import Foreign.C.String
24import Foreign.Marshal.Alloc (free)
25import Foreign.Ptr
27import System.IO
29-- | Attempt to perform a side effect. Return either Just the next step in
30-- evaluation (after performing the side effect through IO), or Nothing if no
31-- IO was performed.
32--
33-- This function is exceedingly generous about what it will accept in order to
34-- enable convenient testing at the REPL.
35-- step :: TT Name -> Idris (Maybe (TT Name))
36-- step tm = step' (unApply tm)
37-- where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = step arg -- Only step if arg can be stepped
38-- step' (P _ (UN "mkForeign") _, args) = stepForeign args
39-- step' (P _ (UN "prim__IO") _, [_, arg]) = return (Just arg)
40-- step' (P _ (UN "prim__readString") _, [(P _ (UN "prim__stdin") _)]) =
41-- do line <- lift $ getLine
42-- return . Just . Constant . Str $ line
43-- step' _ = return Nothing
45-- | Perform side effects until no more can be performed, then return the
46-- resulting term (possibly the argument).
47-- execute :: TT Name -> Idris (TT Name)
48-- execute tm = case unApply tm of
49-- (P _ (UN "unsafePerformIO") _, [_, arg] ) -> execute' arg
50-- _ -> return tm
51-- where execute' tm = do stepped <- step tm
52-- case stepped of
53-- Nothing -> return tm
54-- Just tm' -> execute' tm'
57execute :: Term -> Idris Term
58execute tm = do ctxt <- getContext
59 doExec [] ctxt tm
61doExec :: Env -> Context -> Term -> Idris Term
62doExec env ctxt p@(P Ref n ty) =
63 do let val = lookupDef Nothing n ctxt
64 case val of
65 [Function _ tm] ->
66 do val <- doExec env ctxt tm
67 return val
68 [TyDecl nt ty] -> return p -- abstract def
69 [Operator tp arity op] -> do ty' <- doExec env ctxt ty
70 return (P Ref n ty')
71 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
72 doExec env ctxt tm
73 [CaseOp _ _ _ _ _ ns sc _ _] -> return p
74 thing -> trace ("got to " ++ show thing) $ undefined
75doExec env ctxt p@(P Bound n ty) = case (lookupDef Nothing n ctxt) of -- bound vars must be Function
76 [Function ty tm] -> doExec env ctxt tm
77 [] -> return p
78 x -> fail ("Internal error lookup up bound var " ++ show n ++ " - found " ++ show x)
79doExec env ctxt p@(P (DCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (DCon a b) n ty') }
80doExec env ctxt p@(P (TCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (TCon a b) n ty') }
81doExec env ctxt v@(V i) | i < length env = do let binder = env !! i
82 case binder of
83 (_, (Let t v)) -> return v
84 (_, (NLet t v)) -> return v
85 (n, b) -> doExec env ctxt (P Bound n (binderTy b))
86 | otherwise = return $ V i
87doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
88 let ctxt' = addToCtxt n v' t ctxt
89 doExec ((n, Let t v'):env) ctxt' body
90doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
91doExec env ctxt tm@(Bind n b body) = return tm -- don't eval under lambda!
92doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)
93doExec env ctxt (Constant c) = return (Constant c)
94doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
95 return ((x:xs) !! i)
96doExec env ctxt Erased = return Erased
97doExec env ctxt Impossible = fail "Tried to execute an impossible case"
98doExec env ctxt (TType u) = return (TType u)
100execApp :: Env -> Context -> (Term, [Term]) -> Idris Term
101execApp env ctxt (f, args) = do newF <- doExec env ctxt f
102 laziness <- getLaziness newF
103 newArgs <- mapM (doExec env ctxt) args
104 trace (show newF ++ show (zip args laziness)) $ return ()
105 execApp' env ctxt newF newArgs
106 where getLaziness (P _ (UN "lazy") _) = return [True]
107 getLaziness (P _ n _) = do ist <- getIState
108 let argInfo = idris_implicits ist
109 case lookupCtxtName Nothing n argInfo of
110 [] -> return (repeat False)
111 [ps] -> return $ map lazyarg (snd ps)
112 many -> fail $ "Ambiguous " ++ show n ++ ", found " ++ show many
113 getLaziness x = return (repeat False) -- ok due to zip above
116execApp' :: Env -> Context -> Term -> [Term] -> Idris Term
117execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
118execApp' env ctxt (P _ (UN "unsafePerformIO") _) [ty, action] | (prim__IO, [ty', v]) <- unApply action = return v
119execApp' env ctxt (P _ (UN "mkForeign") _) args =
120 do res <- stepForeign args
121 case res of
122 Nothing -> fail "Could not call foreign function"
123 Just r -> return r
124execApp' env ctxt (P _ (UN "prim__readString") _) [P _ (UN "prim__stdin") _] =
125 do line <- lift getLine
126 return (Constant (Str line))
128execApp' env ctxt (P _ (UN "prim__concat") _) [(Constant (Str s1)), (Constant (Str s2))] =
129 return $ Constant (Str (s1 ++ s2))
131execApp' env ctxt (P _ (UN "prim__eqInt") _) [(Constant (I i1)), (Constant (I i2))] =
132 return $ if i1 == i2 then Constant (I 1) else Constant (I 0)
134execApp' env ctxt (P _ (UN "prim__readString") _) [ptr] | Just p <- unPtr ptr =
135 do fn <- findForeign "freadStr"
136 case fn of
137 Just (Fun _ freadStr) -> do
138 res <- lift $ callFFI freadStr retCString [argPtr p]
139 str <- lift $ peekCString res
140 trace ("Found " ++ str) $ return ()
141 return $ Constant (Str str)
142 Nothing -> fail "Could not load freadStr"
144execApp' env ctxt f@(P _ n _) args =
145 do let val = lookupDef Nothing n ctxt
146 case val of
147 [Function _ tm] -> fail "should already have been eval'd"
148 [TyDecl nt ty] -> return $ mkApp f args
149 [Operator tp arity op] -> fail $ "Can't apply operator " ++ show n ++ " which needs special-casing"
150 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
151 do rhs <- doExec env ctxt tm
152 doExec env ctxt (mkApp tm args)
153 [CaseOp _ _ _ _ _ ns sc _ _] ->
154 do res <- execCase env ctxt ns sc args
155 return $ fromMaybe (mkApp f args) res
156 thing -> return $ mkApp f args
158execApp' env ctxt bnd@(Bind n b body) (arg:args) = let ctxt' = addToCtxt n arg Erased ctxt in
159 doExec ((n, b):env) ctxt' body
161execApp' env ctxt f args = return (mkApp f args)
163execCase :: Env -> Context -> [Name] -> SC -> [Term] -> Idris (Maybe Term)
164execCase env ctxt ns sc args =
165 let arity = length ns in
166 if arity <= length args
167 then do let amap = (zip ns (take arity args))
168 caseRes <- execCase' env ctxt amap sc
169 case caseRes of
170 Just res-> Just <$> doExec env ctxt (mkApp res (drop arity args))
171 Nothing -> return Nothing
172 else return Nothing
174execCase' :: Env -> Context -> [(Name, Term)] -> SC -> Idris (Maybe Term)
175execCase' env ctxt amap (STerm tm) =
176 Just <$> doExec env (foldl (\c (n, t) -> addToCtxt n t Erased c) ctxt amap) tm
177execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap
178 , Just (newCase, newBindings) <- chooseAlt tm alts =
179 execCase' env ctxt (amap ++ newBindings) newCase
180 | otherwise = return Nothing
182chooseAlt :: Term -> [CaseAlt] -> Maybe (SC, [(Name, Term)])
183chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
184chooseAlt (Constant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
185chooseAlt tm (ConCase n i ns sc : alts) | ((P _ cn _), args) <- unApply tm, cn == n = Just (sc, zip ns args)
186 | otherwise = chooseAlt tm alts
187chooseAlt tm (_:alts) = chooseAlt tm alts
188chooseAlt _ [] = Nothing
190data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
192idrisType :: FTy -> Type
193idrisType FUnit = P Ref unitTy (TType (UVal 0))
194idrisType ft = Constant (idr ft)
195 where idr FInt = IType
196 idr FFloat = FlType
197 idr FChar = ChType
198 idr FString = StrType
199 idr FPtr = PtrType
201data Foreign = FFun String [FTy] FTy deriving Show
203-- | A representation of Ptr values, which otherwise don't work in TT
204ptrCon :: Name
205ptrCon = MN 0 "__Ptr"
207-- | Convert a Haskell pointer to a Ptr term in TT
208ptr :: Ptr a -> Term
209ptr p = App (P (DCon 1 0) ptrCon Erased) (Constant (I (addr p)))
210 where addr p = p `minusPtr` nullPtr
212-- | Convert a Ptr term in TT to a Haskell pointer
213unPtr :: Term -> Maybe (Ptr a)
214unPtr (App (P _ con _) (Constant (I addr))) | con == ptrCon = Just (unAddr addr)
215 where unAddr a = nullPtr `plusPtr` a
216unPtr _ = Nothing
219call :: Foreign -> [Term] -> Idris (Maybe Term)
220call (FFun name argTypes retType) args =
221 do fn <- findForeign name
222 case fn of
223 Nothing -> return Nothing
224 Just f -> do res <- call' f args retType
225 return . Just $ mkApp (P Ref (UN "prim__IO") Erased) [idrisType retType, res]
226 where call' :: ForeignFun -> [Term] -> FTy -> Idris Term
227 call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
228 return (Constant (I (fromIntegral res)))
229 call' (Fun _ h) args FFloat = do res <- lift $ callFFI h retCDouble (prepArgs args)
230 return (Constant (Fl (realToFrac res)))
231 call' (Fun _ h) args FChar = do res <- lift $ callFFI h retCChar (prepArgs args)
232 return (Constant (Ch (castCCharToChar res)))
233 call' (Fun _ h) args FString = do res <- lift $ callFFI h retCString (prepArgs args)
234 hStr <- lift $ peekCString res
235-- lift $ free res
236 return (Constant (Str hStr))
238 call' (Fun _ h) args FPtr = do res <- lift $ callFFI h (retPtr retVoid) (prepArgs args)
239 return (ptr res)
240 call' (Fun _ h) args FUnit = do res <- lift $ callFFI h retVoid (prepArgs args)
241 return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level
242-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
245 prepArgs = map prepArg
246 prepArg (Constant (I i)) = argCInt (fromIntegral i)
247 prepArg (Constant (Fl f)) = argCDouble (realToFrac f)
248 prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
249 prepArg (Constant (Str s)) = argString s
250 prepArg ptr | Just p <- unPtr ptr = argPtr p
251 prepArg other = trace ("Could not use " ++ show other ++ " as FFI arg.") undefined
255foreignFromTT :: Term -> Maybe Foreign
256foreignFromTT t = case (unApply t) of
257 (_, [(Constant (Str name)), args, ret]) ->
258 do argTy <- unList args
259 argFTy <- sequence $ map getFTy argTy
260 retFTy <- getFTy ret
261 return $ FFun name argFTy retFTy
262 _ -> trace "failed to construct ffun" Nothing
264getFTy :: Term -> Maybe FTy
265getFTy (P _ (UN t) _) = case t of
266 "FInt" -> Just FInt
267 "FFloat" -> Just FFloat
268 "FChar" -> Just FChar
269 "FString" -> Just FString
270 "FPtr" -> Just FPtr
271 "FUnit" -> Just FUnit
272 _ -> Nothing
273getFTy _ = Nothing
275unList :: Term -> Maybe [Term]
276unList tm = case unApply tm of
277 (nil, [_]) -> Just []
278 (cons, ([_, x, xs])) ->
279 do rest <- unList xs
280 return $ x:rest
281 (f, args) -> Nothing
283toConst :: Term -> Maybe Const
284toConst (Constant c) = Just c
285toConst _ = Nothing
287stepForeign :: [Term] -> Idris (Maybe Term)
288stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
289 f' <- case (call <$> ffun) of
290 Just f -> f args
291 Nothing -> return Nothing
292 return f'
293stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"
295mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
296mapMaybeM f [] = return []
297mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
298 x' <- f x
299 case x' of
300 Just x'' -> return (x'':rest)
301 Nothing -> return rest
303findForeign :: String -> Idris (Maybe ForeignFun)
304findForeign fn = do i <- getIState
305 let libs = idris_dynamic_libs i
306 fns <- mapMaybeM getFn libs
307 case fns of
308 [f] -> return (Just f)
309 [] -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" not found"
310 return Nothing
311 fs -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
312 show (length fs) ++ " occurrences."
313 return Nothing
314 where getFn lib = lift $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)