git.iko.soy/Idris-dev
on cf9d50f help sign in
Idris-dev/src/Core/Execute.hs
306 lines 14 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) = trace ("Reducing " ++ show f) $
102 do newF <- doExec env ctxt f
103 newArgs <- mapM (doExec env ctxt) args
104 execApp' env ctxt newF newArgs
106execApp' :: Env -> Context -> Term -> [Term] -> Idris Term
107execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
108execApp' env ctxt (P _ (UN "unsafePerformIO") _) [ty, action] | (prim__IO, [ty', v]) <- unApply action = return v
109execApp' env ctxt (P _ (UN "mkForeign") _) args =
110 do res <- stepForeign args
111 case res of
112 Nothing -> fail "Could not call foreign function"
113 Just r -> return r
114execApp' env ctxt (P _ (UN "prim__readString") _) [P _ (UN "prim__stdin") _] =
115 do line <- lift getLine
116 return (Constant (Str line))
118execApp' env ctxt (P _ (UN "prim__concat") _) [(Constant (Str s1)), (Constant (Str s2))] =
119 return $ Constant (Str (s1 ++ s2))
121execApp' env ctxt (P _ (UN "prim__eqInt") _) [(Constant (I i1)), (Constant (I i2))] =
122 return $ if i1 == i2 then Constant (I 1) else Constant (I 0)
124execApp' env ctxt (P _ (UN "prim__readString") _) [ptr] | Just p <- unPtr ptr =
125 do fn <- findForeign "freadStr"
126 case fn of
127 Just (Fun _ freadStr) -> do
128 res <- lift $ callFFI freadStr retCString [argPtr p]
129 str <- lift $ peekCString res
130 trace ("Found " ++ str) $ return ()
131 return $ Constant (Str str)
132 Nothing -> fail "Could not load freadStr"
134execApp' env ctxt f@(P _ n _) args =
135 do let val = lookupDef Nothing n ctxt
136 case val of
137 [Function _ tm] -> fail "should already have been eval'd"
138 [TyDecl nt ty] -> return $ mkApp f args
139 [Operator tp arity op] -> fail $ "Can't apply operator " ++ show n ++ " which needs special-casing"
140 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
141 do rhs <- doExec env ctxt tm
142 doExec env ctxt (mkApp tm args)
143 [CaseOp _ _ _ _ _ ns sc _ _] ->
144 do res <- execCase env ctxt ns sc args
145 return $ fromMaybe (mkApp f args) res
146 thing -> return $ mkApp f args
148execApp' env ctxt bnd@(Bind n b body) (arg:args) = let ctxt' = addToCtxt n arg Erased ctxt in
149 doExec ((n, b):env) ctxt' body
151execApp' env ctxt f args = return (mkApp f args)
153execCase :: Env -> Context -> [Name] -> SC -> [Term] -> Idris (Maybe Term)
154execCase env ctxt ns sc args =
155 let arity = length ns in
156 if arity <= length args
157 then do let amap = (zip ns (take arity args))
158 caseRes <- execCase' env ctxt amap sc
159 case caseRes of
160 Just res-> Just <$> doExec env ctxt (mkApp res (drop arity args))
161 Nothing -> return Nothing
162 else return Nothing
164execCase' :: Env -> Context -> [(Name, Term)] -> SC -> Idris (Maybe Term)
165execCase' env ctxt amap (STerm tm) =
166 Just <$> doExec env (foldl (\c (n, t) -> addToCtxt n t Erased c) ctxt amap) tm
167execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap
168 , Just (newCase, newBindings) <- chooseAlt tm alts =
169 execCase' env ctxt (amap ++ newBindings) newCase
170 | otherwise = return Nothing
172chooseAlt :: Term -> [CaseAlt] -> Maybe (SC, [(Name, Term)])
173chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
174chooseAlt (Constant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
175chooseAlt tm (ConCase n i ns sc : alts) | ((P _ cn _), args) <- unApply tm, cn == n = Just (sc, zip ns args)
176 | otherwise = chooseAlt tm alts
177chooseAlt tm (_:alts) = chooseAlt tm alts
178chooseAlt _ [] = Nothing
180data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
182idrisType :: FTy -> Type
183idrisType FUnit = P Ref unitTy (TType (UVal 0))
184idrisType ft = Constant (idr ft)
185 where idr FInt = IType
186 idr FFloat = FlType
187 idr FChar = ChType
188 idr FString = StrType
189 idr FPtr = PtrType
191data Foreign = FFun String [FTy] FTy deriving Show
193-- | A representation of Ptr values, which otherwise don't work in TT
194ptrCon :: Name
195ptrCon = MN 0 "__Ptr"
197-- | Convert a Haskell pointer to a Ptr term in TT
198ptr :: Ptr a -> Term
199ptr p = App (P (DCon 1 0) ptrCon Erased) (Constant (I (addr p)))
200 where addr p = p `minusPtr` nullPtr
202-- | Convert a Ptr term in TT to a Haskell pointer
203unPtr :: Term -> Maybe (Ptr a)
204unPtr (App (P _ con _) (Constant (I addr))) | con == ptrCon = Just (unAddr addr)
205 where unAddr a = nullPtr `plusPtr` a
206unPtr _ = Nothing
209call :: Foreign -> [Term] -> Idris (Maybe Term)
210call (FFun name argTypes retType) args =
211 do fn <- findForeign name
212 case fn of
213 Nothing -> return Nothing
214 Just f -> do res <- call' f args retType
215 return . Just $ mkApp (P Ref (UN "prim__IO") Erased) [idrisType retType, res]
216 where call' :: ForeignFun -> [Term] -> FTy -> Idris Term
217 call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
218 return (Constant (I (fromIntegral res)))
219 call' (Fun _ h) args FFloat = do res <- lift $ callFFI h retCDouble (prepArgs args)
220 return (Constant (Fl (realToFrac res)))
221 call' (Fun _ h) args FChar = do res <- lift $ callFFI h retCChar (prepArgs args)
222 return (Constant (Ch (castCCharToChar res)))
223 call' (Fun _ h) args FString = do res <- lift $ callFFI h retCString (prepArgs args)
224 hStr <- lift $ peekCString res
225-- lift $ free res
226 return (Constant (Str hStr))
228 call' (Fun _ h) args FPtr = do res <- lift $ callFFI h (retPtr retVoid) (prepArgs args)
229 return (ptr res)
230 call' (Fun _ h) args FUnit = do res <- lift $ callFFI h retVoid (prepArgs args)
231 return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level
232-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
235 prepArgs = map prepArg
236 prepArg (Constant (I i)) = argCInt (fromIntegral i)
237 prepArg (Constant (Fl f)) = argCDouble (realToFrac f)
238 prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
239 prepArg (Constant (Str s)) = argString s
240 prepArg ptr | Just p <- unPtr ptr = argPtr p
241 prepArg other = trace ("Could not use " ++ show other ++ " as FFI arg.") undefined
245foreignFromTT :: Term -> Maybe Foreign
246foreignFromTT t = case (unApply t) of
247 (_, [(Constant (Str name)), args, ret]) ->
248 do argTy <- unList args
249 argFTy <- sequence $ map getFTy argTy
250 retFTy <- getFTy ret
251 return $ FFun name argFTy retFTy
252 _ -> trace "failed to construct ffun" Nothing
254getFTy :: Term -> Maybe FTy
255getFTy (P _ (UN t) _) = case t of
256 "FInt" -> Just FInt
257 "FFloat" -> Just FFloat
258 "FChar" -> Just FChar
259 "FString" -> Just FString
260 "FPtr" -> Just FPtr
261 "FUnit" -> Just FUnit
262 _ -> Nothing
263getFTy _ = Nothing
265unList :: Term -> Maybe [Term]
266unList tm = case unApply tm of
267 (nil, [_]) -> Just []
268 (cons, ([_, x, xs])) ->
269 do rest <- unList xs
270 return $ x:rest
271 (f, args) -> Nothing
273toConst :: Term -> Maybe Const
274toConst (Constant c) = Just c
275toConst _ = Nothing
277stepForeign :: [Term] -> Idris (Maybe Term)
278stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
279 f' <- case (call <$> ffun) of
280 Just f -> f args
281 Nothing -> return Nothing
282 return f'
283stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"
285mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
286mapMaybeM f [] = return []
287mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
288 x' <- f x
289 case x' of
290 Just x'' -> return (x'':rest)
291 Nothing -> return rest
293findForeign :: String -> Idris (Maybe ForeignFun)
294findForeign fn = do i <- getIState
295 let libs = idris_dynamic_libs i
296 fns <- mapMaybeM getFn libs
297 case fns of
298 [f] -> return (Just f)
299 [] -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" not found"
300 return Nothing
301 fs -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
302 show (length fs) ++ " occurrences."
303 return Nothing
304 where getFn lib = lift $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)