@@ -22,6 +22,8 @@ import Foreign.LibFFI
22import Foreign.C.String
22import Foreign.C.String
23import Foreign.Marshal.Alloc (free)
23import Foreign.Marshal.Alloc (free)
25-- | Attempt to perform a side effect. Return either Just the next step in
27-- | Attempt to perform a side effect. Return either Just the next step in
26-- evaluation (after performing the side effect through IO), or Nothing if no
28-- evaluation (after performing the side effect through IO), or Nothing if no
27-- IO was performed.
29-- IO was performed.
@@ -56,23 +58,21 @@ execute tm = do ctxt <- getContext
57doExec :: Env -> Context -> Term -> Idris Term
59doExec :: Env -> Context -> Term -> Idris Term
58doExec env ctxt p@(P Ref n ty) =
60doExec 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
60 case val of
62 case val of
61 [Function _ tm] ->
63 [Function _ tm] ->
62 do val <- doExec env ctxt tm
64 do val <- doExec env ctxt tm
63− trace ("got value " ++ show val) $ return val
65+ return val
64 [TyDecl nt ty] -> return p -- abstract def
66 [TyDecl nt ty] -> return p -- abstract def
65 [Operator tp arity op] -> do ty' <- doExec env ctxt ty
67 [Operator tp arity op] -> do ty' <- doExec env ctxt ty
66 return (P Ref n ty')
68 return (P Ref n ty')
67 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
69 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
68− trace (show n ++ " is " ++ show tm ) $ doExec env ctxt tm
70+ doExec env ctxt tm
69− [CaseOp _ _ _ _ _ ns sc _ _] -> trace ("non-app case op " ++ show ns ++ " =-=> " ++ show sc) $
71+ [CaseOp _ _ _ _ _ ns sc _ _] -> return p
71 thing -> trace ("got to " ++ show thing) $ undefined
72 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
73+doExec env ctxt p@(P Bound n ty) = 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
74+ [Function ty tm] -> doExec env ctxt tm
75− [] -> trace ("didn't find " ++ show p) $ return p
75+ [] -> return p
76 x -> fail ("Internal error lookup up bound var " ++ show n ++ " - found " ++ show x)
76 x -> fail ("Internal error lookup up bound var " ++ show n ++ " - found " ++ show x)
77doExec env ctxt p@(P (DCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (DCon a b) n ty') }
77doExec env ctxt p@(P (DCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (DCon a b) n ty') }
78doExec env ctxt p@(P (TCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (TCon a b) n ty') }
78doExec 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") _] =
114execApp' env ctxt (P _ (UN "prim__concat") _) [(Constant (Str s1)), (Constant (Str s2))] =
114execApp' env ctxt (P _ (UN "prim__concat") _) [(Constant (Str s1)), (Constant (Str s2))] =
115 return $ Constant (Str (s1 ++ s2))
115 return $ Constant (Str (s1 ++ s2))
117−execApp' env ctxt f@(P _ n _) args = trace ("Applying " ++ show f ++ " to " ++ show args) $
117+execApp' env ctxt f@(P _ n _) args =
118 do let val = lookupDef Nothing n ctxt
118 do let val = lookupDef Nothing n ctxt
119 case val of
119 case val of
120 [Function _ tm] -> fail "should already have been eval'd"
120 [Function _ tm] -> fail "should already have been eval'd"
121 [TyDecl nt ty] -> return $ mkApp f args
121 [TyDecl nt ty] -> return $ mkApp f args
122 [Operator tp arity op] -> fail $ "Can't apply operator " ++ show n ++ " which needs special-casing"
122 [Operator tp arity op] -> fail $ "Can't apply operator " ++ show n ++ " which needs special-casing"
123 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
123 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
124− trace ("Nullary fun " ++ show f) $
125 do rhs <- doExec env ctxt tm
124 do rhs <- doExec env ctxt tm
126 doExec env ctxt (mkApp tm args)
125 doExec env ctxt (mkApp tm args)
127− [CaseOp _ _ _ _ _ ns sc _ _] -> trace ("Applying case op " ++ show (zip ns args) ++ " ===> " ++ show sc) $
126+ [CaseOp _ _ _ _ _ ns sc _ _] ->
128 do res <- execCase env ctxt ns sc args
127 do res <- execCase env ctxt ns sc args
129− trace ("Application result: " ++ show res) $ return ()
130 return $ fromMaybe (mkApp f args) res
128 return $ fromMaybe (mkApp f args) res
131− thing -> trace ("got to " ++ show thing) $ return $ mkApp f args
129+ 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
131+execApp' env ctxt bnd@(Bind n b body) (arg:args) = let ctxt' = addToCtxt n arg Erased ctxt in
135 doExec ((n, b):env) ctxt' body
132 doExec ((n, b):env) ctxt' body
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)
139execCase :: Env -> Context -> [Name] -> SC -> [Term] -> Idris (Maybe Term)
136execCase :: Env -> Context -> [Name] -> SC -> [Term] -> Idris (Maybe Term)
140execCase env ctxt ns sc args =
137execCase env ctxt ns sc args =
141 let arity = length ns in
138 let arity = length ns in
142 if arity <= length args
139 if arity <= length args
143 then do let amap = (zip ns (take arity args))
140 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
141 caseRes <- execCase' env ctxt amap sc
146 case caseRes of
142 case caseRes of
147 Just res-> Just <$> doExec env ctxt (mkApp res (drop arity args))
143 Just res-> Just <$> doExec env ctxt (mkApp res (drop arity args))
@@ -152,7 +148,6 @@ execCase' :: Env -> Context -> [(Name, Term)] -> SC -> Idris (Maybe Term)
152execCase' env ctxt amap (STerm tm) =
148execCase' env ctxt amap (STerm tm) =
153 Just <$> doExec env (foldl (\c (n, t) -> addToCtxt n t Erased c) ctxt amap) tm
149 Just <$> doExec env (foldl (\c (n, t) -> addToCtxt n t Erased c) ctxt amap) tm
154execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
150execCase' 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
151 let (newCase, newBindings) = chooseAlt tm alts in
157 execCase' env ctxt (amap ++ newBindings) newCase
152 execCase' env ctxt (amap ++ newBindings) newCase
@@ -172,8 +167,8 @@ call :: Foreign -> [Term] -> Idris (Maybe Term)
172call (FFun name argTypes retType) args = do fn <- findForeign name
167call (FFun name argTypes retType) args = do fn <- findForeign name
173 case fn of
168 case fn of
174 Nothing -> return Nothing
169 Nothing -> return Nothing
175− Just f -> call' f args retType >>=
170+ Just f -> do res <- call' f args retType
176− return . Just . App (P Ref (UN "prim__IO") Erased)
171+ return . Just $ App (P Ref (UN "prim__IO") Erased) res
177 where call' :: ForeignFun -> [Term] -> FTy -> Idris Term
172 where call' :: ForeignFun -> [Term] -> FTy -> Idris Term
178 call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
173 call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
179 return (Constant (I (fromIntegral res)))
174 return (Constant (I (fromIntegral res)))
@@ -204,11 +199,9 @@ foreignFromTT :: Term -> Maybe Foreign
204foreignFromTT t = case (unApply t) of
199foreignFromTT t = case (unApply t) of
205 (_, [(Constant (Str name)), args, ret]) ->
200 (_, [(Constant (Str name)), args, ret]) ->
206 do argTy <- unList args
201 do argTy <- unList args
207− trace "fnord" $ return ()
208 argFTy <- sequence $ map getFTy argTy
202 argFTy <- sequence $ map getFTy argTy
209− trace "argh" $ return ()
210 retFTy <- getFTy ret
203 retFTy <- getFTy ret
211− trace ("Returning ffun: " ++ show (FFun name argFTy retFTy)) $ return $ FFun name argFTy retFTy
204+ return $ FFun name argFTy retFTy
212 _ -> trace "failed to construct ffun" Nothing
205 _ -> trace "failed to construct ffun" Nothing
214getFTy :: Term -> Maybe FTy
207getFTy :: Term -> Maybe FTy
@@ -223,7 +216,7 @@ getFTy (P _ (UN t) _) = case t of
223getFTy _ = Nothing
216getFTy _ = Nothing
225unList :: Term -> Maybe [Term]
218unList :: Term -> Maybe [Term]
226−unList tm = trace ("unApplying " ++ show tm) $ case unApply tm of
219+unList tm = case unApply tm of
227 (nil, [_]) -> Just []
220 (nil, [_]) -> Just []
228 (cons, ([_, x, xs])) ->
221 (cons, ([_, x, xs])) ->
229 do rest <- unList xs
222 do rest <- unList xs
@@ -236,7 +229,6 @@ toConst _ = Nothing
237stepForeign :: [Term] -> Idris (Maybe Term)
230stepForeign :: [Term] -> Idris (Maybe Term)
238stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
231stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
239− trace ("Foreign fun call: (" ++ show ffun ++ ")(" ++ show args ++ ")") (return ())
240 f' <- case (call <$> ffun) of
232 f' <- case (call <$> ffun) of
241 Just f -> f args
233 Just f -> f args
242 Nothing -> return Nothing
234 Nothing -> return Nothing