@@ -1,3 +1,4 @@
1+{-# LANGUAGE PatternGuards #-}
1module Core.Execute (execute) where
2module Core.Execute (execute) where
3import Idris.AbsSyntax
4import Idris.AbsSyntax
@@ -5,6 +6,7 @@ import Idris.AbsSyntaxTree
6import Core.TT
7import Core.TT
7import Core.Evaluate
8import Core.Evaluate
9import Debug.Trace
11import Debug.Trace
@@ -14,6 +16,7 @@ import Control.Applicative hiding (Const)
14import Control.Monad.Trans
16import Control.Monad.Trans
15import Control.Monad
17import Control.Monad
16import Data.Maybe
18import Data.Maybe
19+import qualified Data.Map as M
18import Foreign.LibFFI
21import Foreign.LibFFI
19import Foreign.C.String
22import Foreign.C.String
@@ -25,39 +28,153 @@ import Foreign.Marshal.Alloc (free)
26-- This function is exceedingly generous about what it will accept in order to
29-- This function is exceedingly generous about what it will accept in order to
27-- enable convenient testing at the REPL.
30-- enable convenient testing at the REPL.
28−step :: TT Name -> Idris (Maybe (TT Name))
31+-- step :: TT Name -> Idris (Maybe (TT Name))
29−step tm = step' (unApply tm)
32+-- step tm = step' (unApply tm)
30− where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = step arg -- Only step if arg can be stepped
33+-- where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = step arg -- Only step if arg can be stepped
31− step' (P _ (UN "mkForeign") _, args) = stepForeign args
34+-- step' (P _ (UN "mkForeign") _, args) = stepForeign args
32− step' (P _ (UN "prim__IO") _, [_, arg]) = return (Just arg)
35+-- step' (P _ (UN "prim__IO") _, [_, arg]) = return (Just arg)
33− step' (P _ (UN "prim__readString") _, [(P _ (UN "prim__stdin") _)]) =
36+-- step' (P _ (UN "prim__readString") _, [(P _ (UN "prim__stdin") _)]) =
34− do line <- lift $ getLine
37+-- do line <- lift $ getLine
35− return . Just . Constant . Str $ line
38+-- return . Just . Constant . Str $ line
36− step' _ = return Nothing
39+-- step' _ = return Nothing
38-- | Perform side effects until no more can be performed, then return the
41-- | Perform side effects until no more can be performed, then return the
39-- resulting term (possibly the argument).
42-- resulting term (possibly the argument).
40−execute :: TT Name -> Idris (TT Name)
43+-- execute :: TT Name -> Idris (TT Name)
41−execute tm = case unApply tm of
44+-- execute tm = case unApply tm of
42− (P _ (UN "unsafePerformIO") _, [_, arg] ) -> execute' arg
45+-- (P _ (UN "unsafePerformIO") _, [_, arg] ) -> execute' arg
43− _ -> return tm
46+-- _ -> return tm
44− where execute' tm = do stepped <- step tm
47+-- where execute' tm = do stepped <- step tm
45− case stepped of
48+-- case stepped of
46− Nothing -> return tm
49+-- Nothing -> return tm
47− Just tm' -> execute' tm'
50+-- Just tm' -> execute' tm'
53+execute :: Term -> Idris Term
54+execute tm = do ctxt <- getContext
57+doExec :: Env -> Context -> Term -> Idris Term
58+doExec env ctxt p@(P Ref n ty) =
59+ do let val = trace ("looked up global ref "++show p) $ lookupDef Nothing n ctxt
62+ do val <- doExec env ctxt tm
63+ trace ("got value " ++ show val) $ return val
64+ [TyDecl nt ty] -> return p -- abstract def
65+ [Operator tp arity op] -> do ty' <- doExec env ctxt ty
67+ [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
68+ trace (show n ++ " is " ++ show tm ) $ doExec env ctxt tm
69+ [CaseOp _ _ _ _ _ ns sc _ _] -> trace ("non-app case op " ++ show ns ++ " =-=> " ++ show sc) $
71+ thing -> trace ("got to " ++ show thing) $ undefined
72+doExec env ctxt p@(P Bound n ty) = trace ("bound " ++ show p ++ " : " ++ show ty) $
73+ case (lookupDef Nothing n ctxt) of -- bound vars must be Function
74+ [Function ty tm] -> trace (show n ++ " = " ++ show tm ++ " : " ++ show ty) $ doExec env ctxt tm
75+ [] -> trace ("didn't find " ++ show p) $ return p
76+ x -> fail ("Internal error lookup up bound var " ++ show n ++ " - found " ++ show x)
77+doExec env ctxt p@(P (DCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (DCon a b) n ty') }
78+doExec env ctxt p@(P (TCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (TCon a b) n ty') }
79+doExec env ctxt v@(V i) | i < length env = do let binder = env !! i
81+ (_, (Let t v)) -> return v
82+ (_, (NLet t v)) -> return v
83+ (n, b) -> doExec env ctxt (P Bound n (binderTy b))
84+ | otherwise = return $ V i
85+doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
86+ let ctxt' = addToCtxt n v' t ctxt
87+ doExec ((n, Let t v'):env) ctxt' body
88+doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
89+doExec env ctxt tm@(Bind n b body) = return tm -- don't eval under lambda!
90+doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)
91+doExec env ctxt (Constant c) = return (Constant c)
92+doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
94+doExec env ctxt Erased = return Erased
95+doExec env ctxt Impossible = fail "Tried to execute an impossible case"
96+doExec env ctxt (TType u) = return (TType u)
98+execApp :: Env -> Context -> (Term, [Term]) -> Idris Term
99+execApp env ctxt (f, args) = do newF <- doExec env ctxt f
100+ newArgs <- mapM (doExec env ctxt) args
101+ execApp' env ctxt newF newArgs
103+execApp' :: Env -> Context -> Term -> [Term] -> Idris Term
104+execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
105+execApp' env ctxt (P _ (UN "mkForeign") _) args =
106+ do res <- stepForeign args
108+ Nothing -> fail "Could not call foreign function"
110+execApp' env ctxt (P _ (UN "prim__readString") _) [P _ (UN "prim__stdin") _] =
111+ do line <- lift getLine
112+ return (Constant (Str line))
114+execApp' env ctxt (P _ (UN "prim__concat") _) [(Constant (Str s1)), (Constant (Str s2))] =
115+ return $ Constant (Str (s1 ++ s2))
117+execApp' env ctxt f@(P _ n _) args = trace ("Applying " ++ show f ++ " to " ++ show args) $
118+ do let val = lookupDef Nothing n ctxt
120+ [Function _ tm] -> fail "should already have been eval'd"
121+ [TyDecl nt ty] -> return $ mkApp f args
122+ [Operator tp arity op] -> fail $ "Can't apply operator " ++ show n ++ " which needs special-casing"
123+ [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
124+ trace ("Nullary fun " ++ show f) $
125+ do rhs <- doExec env ctxt tm
126+ doExec env ctxt (mkApp tm args)
127+ [CaseOp _ _ _ _ _ ns sc _ _] -> trace ("Applying case op " ++ show (zip ns args) ++ " ===> " ++ show sc) $
128+ do res <- execCase env ctxt ns sc args
129+ trace ("Application result: " ++ show res) $ return ()
130+ return $ fromMaybe (mkApp f args) res
131+ thing -> trace ("got to " ++ show thing) $ return $ mkApp f args
133+execApp' env ctxt bnd@(Bind n b body) (arg:args) = trace ("Applying binder " ++ show bnd ++ " to " ++ show arg) $
134+ let ctxt' = addToCtxt n arg Erased ctxt in
135+ doExec ((n, b):env) ctxt' body
137+execApp' env ctxt f args = trace ("Applying " ++ show f ++ " to " ++ show args) $ return (mkApp f args)
139+execCase :: Env -> Context -> [Name] -> SC -> [Term] -> Idris (Maybe Term)
140+execCase env ctxt ns sc args =
141+ let arity = length ns in
142+ if arity <= length args
143+ then do let amap = (zip ns (take arity args))
144+ trace ("Now we exec " ++ show sc ++ " in " ++ show amap) $ return ()
145+ caseRes <- execCase' env ctxt amap sc
147+ Just res-> Just <$> doExec env ctxt (mkApp res (drop arity args))
148+ Nothing -> return Nothing
151+execCase' :: Env -> Context -> [(Name, Term)] -> SC -> Idris (Maybe Term)
152+execCase' env ctxt amap (STerm tm) =
153+ Just <$> doExec env (foldl (\c (n, t) -> addToCtxt n t Erased c) ctxt amap) tm
154+execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
155+ trace ("Case split on " ++ show tm) $
156+ let (newCase, newBindings) = chooseAlt tm alts in
157+ execCase' env ctxt (amap ++ newBindings) newCase
159+chooseAlt :: Term -> [CaseAlt] -> (SC, [(Name, Term)])
160+chooseAlt _ (DefaultCase sc : alts) = (sc, [])
161+chooseAlt (Constant c) (ConstCase c' sc : alts) | c == c' = (sc, [])
162+chooseAlt tm (ConCase n i ns sc : alts) | ((P _ cn _), args) <- unApply tm, cn == n = (sc, zip ns args)
163+ | otherwise = chooseAlt tm alts
164+chooseAlt tm (_:alts) = chooseAlt tm alts
165+chooseAlt _ [] = trace "bad pattern match" undefined
51data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
167data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
53data Foreign = FFun String [FTy] FTy deriving Show
169data Foreign = FFun String [FTy] FTy deriving Show
55−call :: Foreign -> [TT Name] -> Idris (Maybe (TT Name))
171+call :: Foreign -> [Term] -> Idris (Maybe Term)
56call (FFun name argTypes retType) args = do fn <- findForeign name
172call (FFun name argTypes retType) args = do fn <- findForeign name
57 case fn of
173 case fn of
58 Nothing -> return Nothing
174 Nothing -> return Nothing
59− Just f -> return . Just =<< call' f args retType
175+ Just f -> call' f args retType >>=
176+ return . Just . App (P Ref (UN "prim__IO") Erased)
60− where call' :: ForeignFun -> [TT Name] -> FTy -> Idris (TT Name)
177+ where call' :: ForeignFun -> [Term] -> FTy -> Idris Term
61 call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
178 call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
62 return (Constant (I (fromIntegral res)))
179 return (Constant (I (fromIntegral res)))
63 call' (Fun _ h) args FFloat = do res <- lift $ callFFI h retCDouble (prepArgs args)
180 call' (Fun _ h) args FFloat = do res <- lift $ callFFI h retCDouble (prepArgs args)
@@ -79,43 +196,47 @@ call (FFun name argTypes retType) args = do fn <- findForeign name
79 prepArg (Constant (Fl f)) = argCDouble (realToFrac f)
196 prepArg (Constant (Fl f)) = argCDouble (realToFrac f)
80 prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
197 prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
81 prepArg (Constant (Str s)) = argString s
198 prepArg (Constant (Str s)) = argString s
199+ prepArg other = trace ("Could not use " ++ show other ++ " as FFI arg.") undefined
85−foreignFromTT :: TT Name -> Maybe Foreign
203+foreignFromTT :: Term -> Maybe Foreign
86foreignFromTT t = case (unApply t) of
204foreignFromTT t = case (unApply t) of
87 (_, [(Constant (Str name)), args, ret]) ->
205 (_, [(Constant (Str name)), args, ret]) ->
88 do argTy <- unList args
206 do argTy <- unList args
207+ trace "fnord" $ return ()
89 argFTy <- sequence $ map getFTy argTy
208 argFTy <- sequence $ map getFTy argTy
209+ trace "argh" $ return ()
90 retFTy <- getFTy ret
210 retFTy <- getFTy ret
91− return $ FFun name argFTy retFTy
211+ trace ("Returning ffun: " ++ show (FFun name argFTy retFTy)) $ return $ FFun name argFTy retFTy
92− _ -> Nothing
212+ _ -> trace "failed to construct ffun" Nothing
94−getFTy :: TT Name -> Maybe FTy
214+getFTy :: Term -> Maybe FTy
95getFTy (P _ (UN t) _) = case t of
215getFTy (P _ (UN t) _) = case t of
96− "FInt" -> Just FInt
216+ "FInt" -> Just FInt
97− "FFloat" -> Just FFloat
217+ "FFloat" -> Just FFloat
98− "FChar" -> Just FChar
218+ "FChar" -> Just FChar
99 "FString" -> Just FString
219 "FString" -> Just FString
100− "FPtr" -> Just FPtr
220+ "FPtr" -> Just FPtr
101− "FUnit" -> Just FUnit
221+ "FUnit" -> Just FUnit
102− _ -> Nothing
222+ _ -> Nothing
103getFTy _ = Nothing
223getFTy _ = Nothing
105−unList :: TT Name -> Maybe [TT Name]
225+unList :: Term -> Maybe [Term]
106−unList tm = case unApply tm of
226+unList tm = trace ("unApplying " ++ show tm) $ case unApply tm of
107 (nil, [_]) -> Just []
227 (nil, [_]) -> Just []
108 (cons, ([_, x, xs])) ->
228 (cons, ([_, x, xs])) ->
109 do rest <- unList xs
229 do rest <- unList xs
110 return $ x:rest
230 return $ x:rest
111 (f, args) -> Nothing
231 (f, args) -> Nothing
113−toConst :: TT Name -> Maybe Const
233+toConst :: Term -> Maybe Const
114toConst (Constant c) = Just c
234toConst (Constant c) = Just c
115toConst _ = Nothing
235toConst _ = Nothing
117−stepForeign :: [TT Name] -> Idris (Maybe (TT Name))
237+stepForeign :: [Term] -> Idris (Maybe Term)
118stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
238stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
239+ trace ("Foreign fun call: (" ++ show ffun ++ ")(" ++ show args ++ ")") (return ())
119 f' <- case (call <$> ffun) of
240 f' <- case (call <$> ffun) of
120 Just f -> f args
241 Just f -> f args
121 Nothing -> return Nothing
242 Nothing -> return Nothing