@@ -22,6 +22,7 @@ import Core.CaseTree
2222
2323data EvalState = ES { limited :: [(Name, Int)],
2424 nexthole :: Int }
25+ deriving Show
2526
2627type Eval a = State EvalState a
2728
@@ -185,7 +186,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
185186 -- normal evaluation should return false
186187 blockSimplify (CaseInfo inl dict) n stk
187188 | RunTT `elem` opts
188− = not inl || elem n stk
189+ = not (inl || dict) || elem n stk
189190 | Simplify `elem` opts
190191 = (not (inl || dict) || elem n stk)
191192 || (n == UN "prim__syntactic_eq")
@@ -260,7 +261,9 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
260261 a' <- ev ntimes stk False env a
261262 evApply ntimes stk top env [a'] f'
262263 ev ntimes stk top env (Proj t i)
263− = do t' <- ev ntimes stk top env t
264+ = do -- evaluate dictionaries if it means the projection works
265+ t' <- ev ntimes stk top env t
266+-- tfull' <- reapply ntimes stk top env t' []
264267 return (doProj t' (getValArgs t'))
265268 where doProj t' (VP (DCon _ _) _ _, args) | i < length args = args!!i
266269 doProj t' _ = VProj t' i
@@ -275,6 +278,22 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
275278 evApply ntimes stk top env args f
276279 = apply ntimes stk top env f args
277280
281+ reapply ntimes stk top env f@(VP Ref n ty) args
282+ = let val = lookupDefAcc n atRepl ctxt in
283+ case val of
284+ [(CaseOp ci _ _ _ cd, acc)] ->
285+ let (ns, tree) = getCases cd in
286+ do c <- evCase ntimes n (n:stk) top env ns args tree
287+ case c of
288+ (Nothing, _) -> return $ unload env (VP Ref n ty) args
289+ (Just v, rest) -> evApply ntimes stk top env rest v
290+ _ -> case args of
291+ (a : as) -> return $ unload env f (a : as)
292+ [] -> return f
293+ reapply ntimes stk top env (VApp f a) args
294+ = reapply ntimes stk top env f (a : args)
295+ reapply ntimes stk top env v args = return v
296+
278297 apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)
279298 = do a' <- sc a
280299 app <- apply ntimes stk top env a' as
@@ -344,18 +363,24 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
344363 etm' <- ev ntimes stk (not (conHeaded tm))
345364 (map snd amap ++ env) etm
346365 return $ Just etm'
366+ evTree ntimes stk top env amap (ProjCase t alts)
367+ = do t' <- ev ntimes stk top env t
368+ doCase ntimes stk top env amap t' alts
347369 evTree ntimes stk top env amap (Case n alts)
348370 = case lookup n amap of
349− Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
350− case c of
351− Just (altmap, sc) -> evTree ntimes stk top env altmap sc
352− _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap
353− case c' of
354− Just (altmap, sc) -> evTree ntimes stk top env altmap sc
355− _ -> return Nothing
371+ Just v -> doCase ntimes stk top env amap v alts
356372 _ -> return Nothing
357373 evTree ntimes stk top env amap ImpossibleCase = return Nothing
358374
375+ doCase ntimes stk top env amap v alts =
376+ do c <- chooseAlt env v (getValArgs v) alts amap
377+ case c of
378+ Just (altmap, sc) -> evTree ntimes stk top env altmap sc
379+ _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap
380+ case c' of
381+ Just (altmap, sc) -> evTree ntimes stk top env altmap sc
382+ _ -> return Nothing
383+
359384 conHeaded tm@(App _ _)
360385 | (P (DCon _ _) _ _, args) <- unApply tm = True
361386 conHeaded t = False