@@ -22,6 +22,8 @@ import Foreign.LibFFI
2222import Foreign.C.String
2323import Foreign.Marshal.Alloc (free)
2424
25+import System.IO
26+
2527-- | Attempt to perform a side effect. Return either Just the next step in
2628-- evaluation (after performing the side effect through IO), or Nothing if no
2729-- IO was performed.
@@ -56,23 +58,21 @@ execute tm = do ctxt <- getContext
5658
5759doExec :: Env -> Context -> Term -> Idris Term
5860doExec env ctxt p@(P Ref n ty) =
59− do let val = trace ("looked up global ref "++show p) $ lookupDef Nothing n ctxt
61+ do let val = lookupDef Nothing n ctxt
6062 case val of
6163 [Function _ tm] ->
6264 do val <- doExec env ctxt tm
63− trace ("got value " ++ show val) $ return val
65+ return val
6466 [TyDecl nt ty] -> return p -- abstract def
6567 [Operator tp arity op] -> do ty' <- doExec env ctxt ty
6668 return (P Ref n ty')
6769 [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
70+ doExec env ctxt tm
71+ [CaseOp _ _ _ _ _ ns sc _ _] -> return p
7172 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
73+doExec env ctxt p@(P Bound n ty) = case (lookupDef Nothing n ctxt) of -- bound vars must be Function
74+ [Function ty tm] -> doExec env ctxt tm
75+ [] -> return p
7676 x -> fail ("Internal error lookup up bound var " ++ show n ++ " - found " ++ show x)
7777doExec env ctxt p@(P (DCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (DCon a b) n ty') }
7878doExec env ctxt p@(P (TCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (TCon a b) n ty') }
@@ -114,34 +114,30 @@ execApp' env ctxt (P _ (UN "prim__readString") _) [P _ (UN "prim__stdin") _] =
114114execApp' env ctxt (P _ (UN "prim__concat") _) [(Constant (Str s1)), (Constant (Str s2))] =
115115 return $ Constant (Str (s1 ++ s2))
116116
117−execApp' env ctxt f@(P _ n _) args = trace ("Applying " ++ show f ++ " to " ++ show args) $
117+execApp' env ctxt f@(P _ n _) args =
118118 do let val = lookupDef Nothing n ctxt
119119 case val of
120120 [Function _ tm] -> fail "should already have been eval'd"
121121 [TyDecl nt ty] -> return $ mkApp f args
122122 [Operator tp arity op] -> fail $ "Can't apply operator " ++ show n ++ " which needs special-casing"
123123 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
124− trace ("Nullary fun " ++ show f) $
125124 do rhs <- doExec env ctxt tm
126125 doExec env ctxt (mkApp tm args)
127− [CaseOp _ _ _ _ _ ns sc _ _] -> trace ("Applying case op " ++ show (zip ns args) ++ " ===> " ++ show sc) $
126+ [CaseOp _ _ _ _ _ ns sc _ _] ->
128127 do res <- execCase env ctxt ns sc args
129− trace ("Application result: " ++ show res) $ return ()
130128 return $ fromMaybe (mkApp f args) res
131− thing -> trace ("got to " ++ show thing) $ return $ mkApp f args
129+ thing -> return $ mkApp f args
132130
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
131+execApp' env ctxt bnd@(Bind n b body) (arg:args) = let ctxt' = addToCtxt n arg Erased ctxt in
135132 doExec ((n, b):env) ctxt' body
136133
137−execApp' env ctxt f args = trace ("Applying " ++ show f ++ " to " ++ show args) $ return (mkApp f args)
134+execApp' env ctxt f args = return (mkApp f args)
138135
139136execCase :: Env -> Context -> [Name] -> SC -> [Term] -> Idris (Maybe Term)
140137execCase env ctxt ns sc args =
141138 let arity = length ns in
142139 if arity <= length args
143140 then do let amap = (zip ns (take arity args))
144− trace ("Now we exec " ++ show sc ++ " in " ++ show amap) $ return ()
145141 caseRes <- execCase' env ctxt amap sc
146142 case caseRes of
147143 Just res-> Just <$> doExec env ctxt (mkApp res (drop arity args))
@@ -152,7 +148,6 @@ execCase' :: Env -> Context -> [(Name, Term)] -> SC -> Idris (Maybe Term)
152148execCase' env ctxt amap (STerm tm) =
153149 Just <$> doExec env (foldl (\c (n, t) -> addToCtxt n t Erased c) ctxt amap) tm
154150execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
155− trace ("Case split on " ++ show tm) $
156151 let (newCase, newBindings) = chooseAlt tm alts in
157152 execCase' env ctxt (amap ++ newBindings) newCase
158153
@@ -172,8 +167,8 @@ call :: Foreign -> [Term] -> Idris (Maybe Term)
172167call (FFun name argTypes retType) args = do fn <- findForeign name
173168 case fn of
174169 Nothing -> return Nothing
175− Just f -> call' f args retType >>=
176− return . Just . App (P Ref (UN "prim__IO") Erased)
170+ Just f -> do res <- call' f args retType
171+ return . Just $ App (P Ref (UN "prim__IO") Erased) res
177172 where call' :: ForeignFun -> [Term] -> FTy -> Idris Term
178173 call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
179174 return (Constant (I (fromIntegral res)))
@@ -204,11 +199,9 @@ foreignFromTT :: Term -> Maybe Foreign
204199foreignFromTT t = case (unApply t) of
205200 (_, [(Constant (Str name)), args, ret]) ->
206201 do argTy <- unList args
207− trace "fnord" $ return ()
208202 argFTy <- sequence $ map getFTy argTy
209− trace "argh" $ return ()
210203 retFTy <- getFTy ret
211− trace ("Returning ffun: " ++ show (FFun name argFTy retFTy)) $ return $ FFun name argFTy retFTy
204+ return $ FFun name argFTy retFTy
212205 _ -> trace "failed to construct ffun" Nothing
213206
214207getFTy :: Term -> Maybe FTy
@@ -223,7 +216,7 @@ getFTy (P _ (UN t) _) = case t of
223216getFTy _ = Nothing
224217
225218unList :: Term -> Maybe [Term]
226−unList tm = trace ("unApplying " ++ show tm) $ case unApply tm of
219+unList tm = case unApply tm of
227220 (nil, [_]) -> Just []
228221 (cons, ([_, x, xs])) ->
229222 do rest <- unList xs
@@ -236,7 +229,6 @@ toConst _ = Nothing
236229
237230stepForeign :: [Term] -> Idris (Maybe Term)
238231stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
239− trace ("Foreign fun call: (" ++ show ffun ++ ")(" ++ show args ++ ")") (return ())
240232 f' <- case (call <$> ffun) of
241233 Just f -> f args
242234 Nothing -> return Nothing