@@ -109,105 +109,107 @@ unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
109109-- such as we might have during construction of a proof)
110110
111111eval :: Context -> Ctxt [Bool] -> Env -> TT Name -> [EvalOpt] -> Eval Value
112−eval ctxt statics genv tm opts = ev True [] tm where
112+eval ctxt statics genv tm opts = ev [] True [] tm where
113113 spec = Spec `elem` opts
114114 simpl = Simplify `elem` opts
115115 atRepl = AtREPL `elem` opts
116116
117− ev top env (P _ n ty)
118− | Just (Let t v) <- lookup n genv = ev top env v
119− ev top env (P Ref n ty) = case lookupDefAcc Nothing n atRepl ctxt of
120− [(Function _ tm, Public)] -> ev True env tm
121− [(TyDecl nt ty, _)] -> do vty <- ev True env ty
117+ ev stk top env (P _ n ty)
118+ | Just (Let t v) <- lookup n genv = ev stk top env v
119+ ev stk top env (P Ref n ty) = case lookupDefAcc Nothing n atRepl ctxt of
120+ [(Function _ tm, Public)] ->
121+ ev (n:stk) True env tm
122+ [(TyDecl nt ty, _)] -> do vty <- ev stk True env ty
122123 return $ VP nt n vty
123124 [(CaseOp inl _ _ [] tree _ _, Public)] -> -- unoptimised version
124− if simpl && (not inl)
125− then liftM (VP Ref n) (ev top env ty)
126− else do c <- evCase top env [] [] tree
125+ if simpl && (not inl || elem n stk)
126+ then liftM (VP Ref n) (ev stk top env ty)
127+ else do c <- evCase (n:stk) top env [] [] tree
127128 case c of
128− (Nothing, _) -> liftM (VP Ref n) (ev top env ty)
129+ (Nothing, _) -> liftM (VP Ref n) (ev stk top env ty)
129130 (Just v, _) -> return v
130− _ -> liftM (VP Ref n) (ev top env ty)
131− ev top env (P nt n ty) = liftM (VP nt n) (ev top env ty)
132− ev top env (V i) | i < length env = return $ env !! i
131+ _ -> liftM (VP Ref n) (ev stk top env ty)
132+ ev stk top env (P nt n ty) = liftM (VP nt n) (ev stk top env ty)
133+ ev stk top env (V i) | i < length env = return $ env !! i
133134 | otherwise = return $ VV i
134− ev top env (Bind n (Let t v) sc)
135− = do v' <- ev top env v --(finalise v)
136− sc' <- ev top (v' : env) sc
135+ ev stk top env (Bind n (Let t v) sc)
136+ = do v' <- ev stk top env v --(finalise v)
137+ sc' <- ev stk top (v' : env) sc
137138 wknV (-1) sc'
138− ev top env (Bind n (NLet t v) sc)
139− = do t' <- ev top env (finalise t)
140− v' <- ev top env (finalise v)
141− sc' <- ev top (v' : env) sc
139+ ev stk top env (Bind n (NLet t v) sc)
140+ = do t' <- ev stk top env (finalise t)
141+ v' <- ev stk top env (finalise v)
142+ sc' <- ev stk top (v' : env) sc
142143 return $ VBind n (Let t' v') (\x -> return sc')
143− ev top env (Bind n b sc)
144+ ev stk top env (Bind n b sc)
144145 = do b' <- vbind env b
145− return $ VBind n b' (\x -> ev top (x:env) sc)
146− where vbind env t = fmapMB (\tm -> ev top env (finalise tm)) t
147− ev top env (App f a) = do f' <- ev top env f
148− a' <- ev False env a
149− evApply top env [a'] f'
150− ev top env (Constant c) = return $ VConstant c
151− ev top env Erased = return VErased
152− ev top env (Set i) = return $ VSet i
146+ return $ VBind n b' (\x -> ev stk top (x:env) sc)
147+ where vbind env t = fmapMB (\tm -> ev stk top env (finalise tm)) t
148+ ev stk top env (App f a) = do f' <- ev stk top env f
149+ a' <- ev stk False env a
150+ evApply stk top env [a'] f'
151+ ev stk top env (Constant c) = return $ VConstant c
152+ ev stk top env Erased = return VErased
153+ ev stk top env (Set i) = return $ VSet i
153154
154− evApply top env args (VApp f a) =
155− evApply top env (a:args) f
156− evApply top env args f = apply top env f args
155+ evApply stk top env args (VApp f a) =
156+ evApply stk top env (a:args) f
157+ evApply stk top env args f = apply stk top env f args
157158
158− apply top env (VBind n (Lam t) sc) (a:as)
159+ apply stk top env (VBind n (Lam t) sc) (a:as)
159160 = do a' <- sc a
160− app <- apply top env a' as
161+ app <- apply stk top env a' as
161162 wknV (-1) app
162− apply False env f args
163+ apply stk False env f args
163164 | spec = return $ unload env f args
164− apply top env (VP Ref n ty) args
165+ apply stk top env (VP Ref n ty) args
165166 | [(CaseOp inl _ _ ns tree _ _, Public)] <- lookupDefAcc Nothing n atRepl ctxt
166167 = -- traceWhen (n == UN ["interp"]) (show (n, args)) $
167− if simpl && (not inl) then return $ unload env (VP Ref n ty) args
168− else do c <- evCase top env ns args tree
168+ if simpl && (not inl || elem n stk)
169+ then return $ unload env (VP Ref n ty) args
170+ else do c <- evCase (n:stk) top env ns args tree
169171 case c of
170172 (Nothing, _) -> return $ unload env (VP Ref n ty) args
171− (Just v, rest) -> evApply top env rest v
173+ (Just v, rest) -> evApply stk top env rest v
172174 | [Operator _ i op] <- lookupDef Nothing n ctxt
173175 = if (i <= length args)
174176 then case op (take i args) of
175177 Nothing -> return $ unload env (VP Ref n ty) args
176− Just v -> evApply top env (drop i args) v
178+ Just v -> evApply stk top env (drop i args) v
177179 else return $ unload env (VP Ref n ty) args
178− apply top env f (a:as) = return $ unload env f (a:as)
179− apply top env f [] = return f
180+ apply stk top env f (a:as) = return $ unload env f (a:as)
181+ apply stk top env f [] = return f
180182
181183 unload env f [] = f
182184 unload env f (a:as) = unload env (VApp f a) as
183185
184− evCase top env ns args tree
186+ evCase stk top env ns args tree
185187 | length ns <= length args
186188 = do let args' = take (length ns) args
187189 let rest = drop (length ns) args
188− t <- evTree top env (zipWith (\n t -> (n, t)) ns args') tree
190+ t <- evTree stk top env (zipWith (\n t -> (n, t)) ns args') tree
189191 return (t, rest)
190192 | otherwise = return (Nothing, args)
191193
192− evTree :: Bool -> [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
193− evTree top env amap (UnmatchedCase str) = return Nothing
194− evTree top env amap (STerm tm)
194+ evTree :: [Name] -> Bool -> [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
195+ evTree stk top env amap (UnmatchedCase str) = return Nothing
196+ evTree stk top env amap (STerm tm)
195197 = do let etm = pToVs (map fst amap) tm
196− etm' <- ev top (map snd amap ++ env) etm
198+ etm' <- ev stk top (map snd amap ++ env) etm
197199 return $ Just etm'
198− evTree top env amap (Case n alts)
200+ evTree stk top env amap (Case n alts)
199201 = case lookup n amap of
200202 Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
201203 case c of
202− Just (altmap, sc) -> evTree top env altmap sc
203− _ -> do c' <- chooseAlt' env v (getValArgs v) alts amap
204+ Just (altmap, sc) -> evTree stk top env altmap sc
205+ _ -> do c' <- chooseAlt' stk env v (getValArgs v) alts amap
204206 case c' of
205− Just (altmap, sc) -> evTree top env altmap sc
207+ Just (altmap, sc) -> evTree stk top env altmap sc
206208 _ -> return Nothing
207209 _ -> return Nothing
208210
209− chooseAlt' env _ (f, args) alts amap
210− = do f' <- apply True env f args
211+ chooseAlt' stk env _ (f, args) alts amap
212+ = do f' <- apply stk True env f args
211213 chooseAlt env f' (getValArgs f') alts amap
212214
213215 chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->