@@ -516,9 +516,9 @@ try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
516516try' t1 t2 proofSearch
517517 = do s <- get
518518 ps <- get_probs
519− case prunStateT ps t1 s of
520− OK (v, s') -> do put s'
521− return v
519+ case prunStateT 999999 False ps t1 s of
520+ OK ((v, _), s') -> do put s'
521+ return v
522522 Error e1 -> if recoverableErr e1 then
523523 do case runStateT t2 s of
524524 OK (v, s') -> do put s'; return v
@@ -539,42 +539,51 @@ tryWhen False a b = a
539539
540540-- Try a selection of tactics. Exactly one must work, all others must fail
541541tryAll :: [(Elab' aux a, String)] -> Elab' aux a
542−tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)
542+tryAll xs = tryAll' [] 999999 (cantResolve, 0) (map fst xs)
543543 where
544544 cantResolve :: Elab' aux a
545545 cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)
546546
547547 tryAll' :: [Elab' aux a] -> -- successes
548+ Int -> -- most problems
548549 (Elab' aux a, Int) -> -- smallest failure
549550 [Elab' aux a] -> -- still to try
550551 Elab' aux a
551− tryAll' [res] _ [] = res
552− tryAll' (_:_) _ [] = cantResolve
553− tryAll' [] (f, _) [] = f
554− tryAll' cs f (x:xs)
552+ tryAll' [res] pmax _ [] = res
553+ tryAll' (_:_) pmax _ [] = cantResolve
554+ tryAll' [] pmax (f, _) [] = f
555+ tryAll' cs pmax f (x:xs)
555556 = do s <- get
556557 ps <- get_probs
557− case prunStateT ps x s of
558− OK (v, s') -> tryAll' ((do put s'
559− return v):cs) f xs
558+ case prunStateT pmax True ps x s of
559+ OK ((v, newps), s') ->
560+ do let cs' = if (newps < pmax)
561+ then [do put s'; return v]
562+ else (do put s'; return v) : cs
563+ tryAll' cs' newps f xs
560564 Error err -> do put s
561565 if (score err) < 100
562− then tryAll' cs (better err f) xs
563− else tryAll' [] (better err f) xs -- give up
566+ then tryAll' cs pmax (better err f) xs
567+ else tryAll' [] pmax (better err f) xs -- give up
564568
565569
566570 better err (f, i) = let s = score err in
567571 if (s >= i) then (lift (tfail err), s)
568572 else (f, i)
569573
570−prunStateT ps x s
574+prunStateT pmax zok ps x s
571575 = case runStateT x s of
572576 OK (v, s'@(ES (p, _) _ _)) ->
573− if (length (problems p) > length ps)
577+ let newps = length (problems p) - length ps
578+ newpmax = if newps < 0 then 0 else newps in
579+ if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))
574580 then case reverse (problems p) of
575581 ((_,_,_,e):_) -> Error e
576− else OK (v, s')
582+ else OK ((v, newpmax), s')
577583 Error e -> Error e
578584
585+qshow :: Fails -> String
586+qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)
587+
579588dumpprobs [] = ""
580589dumpprobs ((_,_,_,e):es) = show e ++ "\n" ++ dumpprobs es