@@ -1,3 +1,4 @@
1+{-# LANGUAGE PatternGuards #-}
12module Core.Execute (execute) where
23
34import Idris.AbsSyntax
@@ -5,6 +6,7 @@ import Idris.AbsSyntaxTree
56
67import Core.TT
78import Core.Evaluate
9+import Core.CaseTree
810
911import Debug.Trace
1012
@@ -14,6 +16,7 @@ import Control.Applicative hiding (Const)
1416import Control.Monad.Trans
1517import Control.Monad
1618import Data.Maybe
19+import qualified Data.Map as M
1720
1821import Foreign.LibFFI
1922import Foreign.C.String
@@ -25,39 +28,153 @@ import Foreign.Marshal.Alloc (free)
2528--
2629-- This function is exceedingly generous about what it will accept in order to
2730-- enable convenient testing at the REPL.
28−step :: TT Name -> Idris (Maybe (TT Name))
29−step tm = step' (unApply tm)
30− where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = step arg -- Only step if arg can be stepped
31− step' (P _ (UN "mkForeign") _, args) = stepForeign args
32− step' (P _ (UN "prim__IO") _, [_, arg]) = return (Just arg)
33− step' (P _ (UN "prim__readString") _, [(P _ (UN "prim__stdin") _)]) =
34− do line <- lift $ getLine
35− return . Just . Constant . Str $ line
36− step' _ = return Nothing
31+-- step :: TT Name -> Idris (Maybe (TT Name))
32+-- step tm = step' (unApply tm)
33+-- where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = step arg -- Only step if arg can be stepped
34+-- step' (P _ (UN "mkForeign") _, args) = stepForeign args
35+-- step' (P _ (UN "prim__IO") _, [_, arg]) = return (Just arg)
36+-- step' (P _ (UN "prim__readString") _, [(P _ (UN "prim__stdin") _)]) =
37+-- do line <- lift $ getLine
38+-- return . Just . Constant . Str $ line
39+-- step' _ = return Nothing
3740
3841-- | Perform side effects until no more can be performed, then return the
3942-- resulting term (possibly the argument).
40−execute :: TT Name -> Idris (TT Name)
41−execute tm = case unApply tm of
42− (P _ (UN "unsafePerformIO") _, [_, arg] ) -> execute' arg
43− _ -> return tm
44− where execute' tm = do stepped <- step tm
45− case stepped of
46− Nothing -> return tm
47− Just tm' -> execute' tm'
43+-- execute :: TT Name -> Idris (TT Name)
44+-- execute tm = case unApply tm of
45+-- (P _ (UN "unsafePerformIO") _, [_, arg] ) -> execute' arg
46+-- _ -> return tm
47+-- where execute' tm = do stepped <- step tm
48+-- case stepped of
49+-- Nothing -> return tm
50+-- Just tm' -> execute' tm'
4851
4952
53+execute :: Term -> Idris Term
54+execute tm = do ctxt <- getContext
55+ doExec [] ctxt tm
56+
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
60+ case val of
61+ [Function _ tm] ->
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
66+ return (P Ref n 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) $
70+ return p
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
80+ case binder of
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
93+ return ((x:xs) !! i)
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)
97+
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
102+
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
107+ case res of
108+ Nothing -> fail "Could not call foreign function"
109+ Just r -> return r
110+execApp' env ctxt (P _ (UN "prim__readString") _) [P _ (UN "prim__stdin") _] =
111+ do line <- lift getLine
112+ return (Constant (Str line))
113+
114+execApp' env ctxt (P _ (UN "prim__concat") _) [(Constant (Str s1)), (Constant (Str s2))] =
115+ return $ Constant (Str (s1 ++ s2))
116+
117+execApp' env ctxt f@(P _ n _) args = trace ("Applying " ++ show f ++ " to " ++ show args) $
118+ do let val = lookupDef Nothing n ctxt
119+ case val of
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
132+
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
136+
137+execApp' env ctxt f args = trace ("Applying " ++ show f ++ " to " ++ show args) $ return (mkApp f args)
138+
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
146+ case caseRes of
147+ Just res-> Just <$> doExec env ctxt (mkApp res (drop arity args))
148+ Nothing -> return Nothing
149+ else return Nothing
150+
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
158+
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
50166
51167data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
52168
53169data Foreign = FFun String [FTy] FTy deriving Show
54170
55−call :: Foreign -> [TT Name] -> Idris (Maybe (TT Name))
171+call :: Foreign -> [Term] -> Idris (Maybe Term)
56172call (FFun name argTypes retType) args = do fn <- findForeign name
57173 case fn of
58174 Nothing -> return Nothing
59− Just f -> return . Just =<< call' f args retType
60− where call' :: ForeignFun -> [TT Name] -> FTy -> Idris (TT Name)
175+ Just f -> call' f args retType >>=
176+ return . Just . App (P Ref (UN "prim__IO") Erased)
177+ where call' :: ForeignFun -> [Term] -> FTy -> Idris Term
61178 call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
62179 return (Constant (I (fromIntegral res)))
63180 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
79196 prepArg (Constant (Fl f)) = argCDouble (realToFrac f)
80197 prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
81198 prepArg (Constant (Str s)) = argString s
199+ prepArg other = trace ("Could not use " ++ show other ++ " as FFI arg.") undefined
82200
83201
84202
85−foreignFromTT :: TT Name -> Maybe Foreign
203+foreignFromTT :: Term -> Maybe Foreign
86204foreignFromTT t = case (unApply t) of
87205 (_, [(Constant (Str name)), args, ret]) ->
88206 do argTy <- unList args
207+ trace "fnord" $ return ()
89208 argFTy <- sequence $ map getFTy argTy
209+ trace "argh" $ return ()
90210 retFTy <- getFTy ret
91− return $ FFun name argFTy retFTy
92− _ -> Nothing
211+ trace ("Returning ffun: " ++ show (FFun name argFTy retFTy)) $ return $ FFun name argFTy retFTy
212+ _ -> trace "failed to construct ffun" Nothing
93213
94−getFTy :: TT Name -> Maybe FTy
214+getFTy :: Term -> Maybe FTy
95215getFTy (P _ (UN t) _) = case t of
96− "FInt" -> Just FInt
97− "FFloat" -> Just FFloat
98− "FChar" -> Just FChar
216+ "FInt" -> Just FInt
217+ "FFloat" -> Just FFloat
218+ "FChar" -> Just FChar
99219 "FString" -> Just FString
100− "FPtr" -> Just FPtr
101− "FUnit" -> Just FUnit
102− _ -> Nothing
220+ "FPtr" -> Just FPtr
221+ "FUnit" -> Just FUnit
222+ _ -> Nothing
103223getFTy _ = Nothing
104224
105−unList :: TT Name -> Maybe [TT Name]
106−unList tm = case unApply tm of
225+unList :: Term -> Maybe [Term]
226+unList tm = trace ("unApplying " ++ show tm) $ case unApply tm of
107227 (nil, [_]) -> Just []
108228 (cons, ([_, x, xs])) ->
109229 do rest <- unList xs
110230 return $ x:rest
111231 (f, args) -> Nothing
112232
113−toConst :: TT Name -> Maybe Const
233+toConst :: Term -> Maybe Const
114234toConst (Constant c) = Just c
115235toConst _ = Nothing
116236
117−stepForeign :: [TT Name] -> Idris (Maybe (TT Name))
237+stepForeign :: [Term] -> Idris (Maybe Term)
118238stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
239+ trace ("Foreign fun call: (" ++ show ffun ++ ")(" ++ show args ++ ")") (return ())
119240 f' <- case (call <$> ffun) of
120241 Just f -> f args
121242 Nothing -> return Nothing