git.iko.soy/Idris-dev
on 0752bed help sign in
Idris-dev/src/Core/Execute.hs
272 lines 13 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)
26import System.IO
28-- | Attempt to perform a side effect. Return either Just the next step in
29-- evaluation (after performing the side effect through IO), or Nothing if no
30-- IO was performed.
31--
32-- This function is exceedingly generous about what it will accept in order to
33-- enable convenient testing at the REPL.
34-- step :: TT Name -> Idris (Maybe (TT Name))
35-- step tm = step' (unApply tm)
36-- where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = step arg -- Only step if arg can be stepped
37-- step' (P _ (UN "mkForeign") _, args) = stepForeign args
38-- step' (P _ (UN "prim__IO") _, [_, arg]) = return (Just arg)
39-- step' (P _ (UN "prim__readString") _, [(P _ (UN "prim__stdin") _)]) =
40-- do line <- lift $ getLine
41-- return . Just . Constant . Str $ line
42-- step' _ = return Nothing
44-- | Perform side effects until no more can be performed, then return the
45-- resulting term (possibly the argument).
46-- execute :: TT Name -> Idris (TT Name)
47-- execute tm = case unApply tm of
48-- (P _ (UN "unsafePerformIO") _, [_, arg] ) -> execute' arg
49-- _ -> return tm
50-- where execute' tm = do stepped <- step tm
51-- case stepped of
52-- Nothing -> return tm
53-- Just tm' -> execute' tm'
56execute :: Term -> Idris Term
57execute tm = do ctxt <- getContext
58 doExec [] ctxt tm
60doExec :: Env -> Context -> Term -> Idris Term
61doExec env ctxt p@(P Ref n ty) =
62 do let val = lookupDef Nothing n ctxt
63 case val of
64 [Function _ tm] ->
65 do val <- doExec env ctxt tm
66 return val
67 [TyDecl nt ty] -> return p -- abstract def
68 [Operator tp arity op] -> do ty' <- doExec env ctxt ty
69 return (P Ref n ty')
70 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
71 doExec env ctxt tm
72 [CaseOp _ _ _ _ _ ns sc _ _] -> return p
73 thing -> trace ("got to " ++ show thing) $ undefined
74doExec env ctxt p@(P Bound n ty) = case (lookupDef Nothing n ctxt) of -- bound vars must be Function
75 [Function ty tm] -> doExec env ctxt tm
76 [] -> return p
77 x -> fail ("Internal error lookup up bound var " ++ show n ++ " - found " ++ show x)
78doExec env ctxt p@(P (DCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (DCon a b) n ty') }
79doExec env ctxt p@(P (TCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (TCon a b) n ty') }
80doExec env ctxt v@(V i) | i < length env = do let binder = env !! i
81 case binder of
82 (_, (Let t v)) -> return v
83 (_, (NLet t v)) -> return v
84 (n, b) -> doExec env ctxt (P Bound n (binderTy b))
85 | otherwise = return $ V i
86doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
87 let ctxt' = addToCtxt n v' t ctxt
88 doExec ((n, Let t v'):env) ctxt' body
89doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
90doExec env ctxt tm@(Bind n b body) = return tm -- don't eval under lambda!
91doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)
92doExec env ctxt (Constant c) = return (Constant c)
93doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
94 return ((x:xs) !! i)
95doExec env ctxt Erased = return Erased
96doExec env ctxt Impossible = fail "Tried to execute an impossible case"
97doExec env ctxt (TType u) = return (TType u)
99execApp :: Env -> Context -> (Term, [Term]) -> Idris Term
100execApp env ctxt (f, args) = do newF <- doExec env ctxt f
101 newArgs <- mapM (doExec env ctxt) args
102 execApp' env ctxt newF newArgs
104execApp' :: Env -> Context -> Term -> [Term] -> Idris Term
105execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
106execApp' env ctxt (P _ (UN "unsafePerformIO") _) [ty, action] | (prim__IO, [ty', v]) <- unApply action = return v
107execApp' env ctxt (P _ (UN "mkForeign") _) args =
108 do res <- stepForeign args
109 case res of
110 Nothing -> fail "Could not call foreign function"
111 Just r -> return r
112execApp' env ctxt (P _ (UN "prim__readString") _) [P _ (UN "prim__stdin") _] =
113 do line <- lift getLine
114 return (Constant (Str line))
116execApp' env ctxt (P _ (UN "prim__concat") _) [(Constant (Str s1)), (Constant (Str s2))] =
117 return $ Constant (Str (s1 ++ s2))
119execApp' env ctxt f@(P _ n _) args =
120 do let val = lookupDef Nothing n ctxt
121 case val of
122 [Function _ tm] -> fail "should already have been eval'd"
123 [TyDecl nt ty] -> return $ mkApp f args
124 [Operator tp arity op] -> fail $ "Can't apply operator " ++ show n ++ " which needs special-casing"
125 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
126 do rhs <- doExec env ctxt tm
127 doExec env ctxt (mkApp tm args)
128 [CaseOp _ _ _ _ _ ns sc _ _] ->
129 do res <- execCase env ctxt ns sc args
130 return $ fromMaybe (mkApp f args) res
131 thing -> return $ mkApp f args
133execApp' env ctxt bnd@(Bind n b body) (arg:args) = let ctxt' = addToCtxt n arg Erased ctxt in
134 doExec ((n, b):env) ctxt' body
136execApp' env ctxt f args = return (mkApp f args)
138execCase :: Env -> Context -> [Name] -> SC -> [Term] -> Idris (Maybe Term)
139execCase env ctxt ns sc args =
140 let arity = length ns in
141 if arity <= length args
142 then do let amap = (zip ns (take arity args))
143 caseRes <- execCase' env ctxt amap sc
144 case caseRes of
145 Just res-> Just <$> doExec env ctxt (mkApp res (drop arity args))
146 Nothing -> return Nothing
147 else return Nothing
149execCase' :: Env -> Context -> [(Name, Term)] -> SC -> Idris (Maybe Term)
150execCase' env ctxt amap (STerm tm) =
151 Just <$> doExec env (foldl (\c (n, t) -> addToCtxt n t Erased c) ctxt amap) tm
152execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap
153 , Just (newCase, newBindings) <- chooseAlt tm alts =
154 execCase' env ctxt (amap ++ newBindings) newCase
155 | otherwise = return Nothing
157chooseAlt :: Term -> [CaseAlt] -> Maybe (SC, [(Name, Term)])
158chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
159chooseAlt (Constant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
160chooseAlt tm (ConCase n i ns sc : alts) | ((P _ cn _), args) <- unApply tm, cn == n = Just (sc, zip ns args)
161 | otherwise = chooseAlt tm alts
162chooseAlt tm (_:alts) = chooseAlt tm alts
163chooseAlt _ [] = Nothing
165data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
167idrisType :: FTy -> Type
168idrisType FUnit = P Ref unitTy (TType (UVal 0))
169idrisType ft = Constant (idr ft)
170 where idr FInt = IType
171 idr FFloat = FlType
172 idr FChar = ChType
173 idr FString = StrType
174 idr FPtr = PtrType
176data Foreign = FFun String [FTy] FTy deriving Show
178call :: Foreign -> [Term] -> Idris (Maybe Term)
179call (FFun name argTypes retType) args =
180 do fn <- findForeign name
181 case fn of
182 Nothing -> return Nothing
183 Just f -> do res <- call' f args retType
184 return . Just $ mkApp (P Ref (UN "prim__IO") Erased) [idrisType retType, res]
185 where call' :: ForeignFun -> [Term] -> FTy -> Idris Term
186 call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
187 return (Constant (I (fromIntegral res)))
188 call' (Fun _ h) args FFloat = do res <- lift $ callFFI h retCDouble (prepArgs args)
189 return (Constant (Fl (realToFrac res)))
190 call' (Fun _ h) args FChar = do res <- lift $ callFFI h retCChar (prepArgs args)
191 return (Constant (Ch (castCCharToChar res)))
192 call' (Fun _ h) args FString = do res <- lift $ callFFI h retCString (prepArgs args)
193 hStr <- lift $ peekCString res
194-- lift $ free res
195 return (Constant (Str hStr))
196-- awaiting Const constructor for pointers
197-- call' (Fun _ h) args FPtr = do res <- lift $ callFFI h retPtr (prepArgs args)
198-- return (Constant (Ch (castCCharToChar res)))
199 call' (Fun _ h) args FUnit = do res <- lift $ callFFI h retVoid (prepArgs args)
200 return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level
202 prepArgs = map prepArg
203 prepArg (Constant (I i)) = argCInt (fromIntegral i)
204 prepArg (Constant (Fl f)) = argCDouble (realToFrac f)
205 prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
206 prepArg (Constant (Str s)) = argString s
207 prepArg other = trace ("Could not use " ++ show other ++ " as FFI arg.") undefined
211foreignFromTT :: Term -> Maybe Foreign
212foreignFromTT t = case (unApply t) of
213 (_, [(Constant (Str name)), args, ret]) ->
214 do argTy <- unList args
215 argFTy <- sequence $ map getFTy argTy
216 retFTy <- getFTy ret
217 return $ FFun name argFTy retFTy
218 _ -> trace "failed to construct ffun" Nothing
220getFTy :: Term -> Maybe FTy
221getFTy (P _ (UN t) _) = case t of
222 "FInt" -> Just FInt
223 "FFloat" -> Just FFloat
224 "FChar" -> Just FChar
225 "FString" -> Just FString
226 "FPtr" -> Just FPtr
227 "FUnit" -> Just FUnit
228 _ -> Nothing
229getFTy _ = Nothing
231unList :: Term -> Maybe [Term]
232unList tm = case unApply tm of
233 (nil, [_]) -> Just []
234 (cons, ([_, x, xs])) ->
235 do rest <- unList xs
236 return $ x:rest
237 (f, args) -> Nothing
239toConst :: Term -> Maybe Const
240toConst (Constant c) = Just c
241toConst _ = Nothing
243stepForeign :: [Term] -> Idris (Maybe Term)
244stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
245 f' <- case (call <$> ffun) of
246 Just f -> f args
247 Nothing -> return Nothing
248 return f'
249stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"
251mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
252mapMaybeM f [] = return []
253mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
254 x' <- f x
255 case x' of
256 Just x'' -> return (x'':rest)
257 Nothing -> return rest
259findForeign :: String -> Idris (Maybe ForeignFun)
260findForeign fn = do i <- getIState
261 let libs = idris_dynamic_libs i
262 fns <- mapMaybeM getFn libs
263 case fns of
264 [f] -> return (Just f)
265 [] -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" not found"
266 return Nothing
267 fs -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
268 show (length fs) ++ " occurrences."
269 return Nothing
270 where getFn lib = lift $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)