# HG changeset patch # User paulson # Date 905441589 -7200 # Node ID a5479f5cd4827bc48fa63689c4a765519d8dc98f # Parent 7c5b2a8adbf0683598d3ada279314af722b1e662 Allows more backtracking in proof reconstruction, making it slower but more robust (avoiding PROOF FAILED) Record type of branches, better tracing, etc. diff -r 7c5b2a8adbf0 -r a5479f5cd482 src/Provers/blast.ML --- a/src/Provers/blast.ML Thu Sep 10 17:32:07 1998 +0200 +++ b/src/Provers/blast.ML Thu Sep 10 17:33:09 1998 +0200 @@ -469,7 +469,7 @@ | nNewHyps (Const "*Goal*" $ _ :: Ps) = nNewHyps Ps | nNewHyps (P::Ps) = 1 + nNewHyps Ps; - fun rot_tac [] i st = Seq.single (Seq.hd (flexflex_rule st)) + fun rot_tac [] i st = Seq.single st | rot_tac (0::ks) i st = rot_tac ks (i+1) st | rot_tac (k::ks) i st = rot_tac ks (i+1) (rotate_rule (~k) i st); in @@ -562,11 +562,12 @@ (*Pending formulae carry md (may duplicate) flags*) -type branch = ((term*bool) list * (*safe formulae on this level*) - (term*bool) list) list * (*haz formulae on this level*) - term list * (*literals: irreducible formulae*) - term option ref list * (*variables occurring in branch*) - int; (*resource limit*) +type branch = + {pairs: ((term*bool) list * (*safe formulae on this level*) + (term*bool) list) list, (*haz formulae on this level*) + lits: term list, (*literals: irreducible formulae*) + vars: term option ref list, (*variables occurring in branch*) + lim: int}; (*resource limit*) val fullTrace = ref[] : branch list list ref; @@ -575,8 +576,11 @@ fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs); -fun normBr (br, lits, vars, lim) = - (map normLev br, map norm lits, vars, lim); +fun normBr {pairs, lits, vars, lim} = + {pairs = map normLev pairs, + lits = map norm lits, + vars = vars, + lim = lim}; val dummyTVar = Term.TVar(("a",0), []); @@ -629,7 +633,7 @@ let fun printPairs (((G,_)::_,_)::_) = prs(traceTerm sign G) | printPairs (([],(H,_)::_)::_) = prs(traceTerm sign H ^ "\t (Unsafe)") | printPairs _ = () - fun printBrs (brs0 as (pairs, lits, _, lim) :: brs) = + fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) = (fullTrace := brs0 :: !fullTrace; seq (fn _ => prs "+") brs; prs (" [" ^ Int.toString lim ^ "] "); @@ -735,7 +739,7 @@ (*Substitute through the branch if an equality goal (else raise DEST_EQ). Moves affected literals back into the branch, but it is not clear where they should go: this could make proofs fail.*) -fun equalSubst sign (G, pairs, lits, vars, lim) = +fun equalSubst sign (G, {pairs, lits, vars, lim}) = let val (t,u) = orientGoal(dest_eq G) val subst = subst_atomic (t,u) fun subst2(G,md) = (subst G, md) @@ -761,9 +765,10 @@ in if !trace then writeln ("Substituting " ^ traceTerm sign u ^ " for " ^ traceTerm sign t ^ " in branch" ) else (); - ((changed',[])::pairs', (*affected formulas, and others*) - lits', (*unaffected literals*) - vars, lim) + {pairs = (changed',[])::pairs', (*affected formulas, and others*) + lits = lits', (*unaffected literals*) + vars = vars, + lim = lim} end; @@ -856,8 +861,8 @@ choices) in traceIt (pruneAux (choices, !ntrail, !trail, choices)) end; -fun nextVars ((br, lits, vars, lim) :: _) = map Var vars - | nextVars [] = []; +fun nextVars ({pairs, lits, vars, lim} :: _) = map Var vars + | nextVars [] = []; fun backtrack (choices as (ntrl, nbrs, exn)::_) = (if !trace then (writeln ("Backtracking; now there are " ^ @@ -932,7 +937,8 @@ (printStats (!trace orelse !stats, start, tacs); cont (tacs, trs, choices)) (*all branches closed!*) | prv (tacs, trs, choices, - brs0 as (((G,md)::br, haz)::pairs, lits, vars, lim) :: brs) = + brs0 as {pairs = ((G,md)::br, haz)::pairs, + lits, vars, lim} :: brs) = (*apply a safe rule only (possibly allowing instantiation); defer any haz formulae*) let exception PRV (*backtrack to precisely this recursion!*) @@ -945,12 +951,16 @@ fun newBr (vars',lim') prems = map (fn prem => if (exists isGoal prem) - then (((joinMd md prem, []) :: - negOfGoals ((br, haz)::pairs)), - map negOfGoal lits, - vars', lim') - else (((joinMd md prem, []) :: (br, haz) :: pairs), - lits, vars', lim')) + then {pairs = ((joinMd md prem, []) :: + negOfGoals ((br, haz)::pairs)), + lits = map negOfGoal lits, + vars = vars', + lim = lim'} + else {pairs = ((joinMd md prem, []) :: + (br, haz) :: pairs), + lits = lits, + vars = vars', + lim = lim'}) prems @ brs (*Seek a matching rule. If unifiable then add new premises @@ -966,7 +976,7 @@ val vars = vars_in_vars vars val vars' = foldr add_terms_vars (prems, vars) val choices' = (ntrl, nbrs, PRV) :: choices - val tacs' = (DETERM o tac(updated,false,true)) + val tacs' = (tac(updated,false,true)) :: tacs (*no duplication; rotate*) in traceNew prems; traceVars sign ntrl; @@ -1021,32 +1031,44 @@ else prv (Data.hyp_subst_tac trace :: tacs, brs0::trs, choices, - equalSubst sign (G, (br,haz)::pairs, lits, vars, lim) :: brs) + equalSubst sign + (G, {pairs = (br,haz)::pairs, + lits = lits, vars = vars, lim = lim}) + :: brs) handle DEST_EQ => closeF lits handle CLOSEF => closeFl ((br,haz)::pairs) handle CLOSEF => deeper rules handle NEWBRANCHES => (case netMkRules G vars hazList of [] => (*there are no plausible haz rules*) - (traceMsg "moving goal to literals"; - prv (tacs, brs0::trs, choices, - ((br,haz)::pairs, addLit(G,lits), vars, lim) - ::brs)) + (traceMsg "moving formula to literals"; + prv (tacs, brs0::trs, choices, + {pairs = (br,haz)::pairs, + lits = addLit(G,lits), + vars = vars, + lim = lim} :: brs)) | _ => (*G admits some haz rules: try later*) - (traceMsg "moving goal to haz list"; + (traceMsg "moving formula to haz list"; prv (if isGoal G then negOfGoal_tac :: tacs - else tacs, - brs0::trs, choices, - ((br, haz@[(negOfGoal G, md)])::pairs, - lits, vars, lim) :: brs))) + else tacs, + brs0::trs, + choices, + {pairs = (br, haz@[(negOfGoal G, md)])::pairs, + lits = lits, + vars = vars, + lim = lim} :: brs))) end | prv (tacs, trs, choices, - (([],haz)::(Gs,haz')::pairs, lits, vars, lim) :: brs) = + {pairs = ([],haz)::(Gs,haz')::pairs, lits, vars, lim} :: brs) = (*no more "safe" formulae: transfer haz down a level*) prv (tacs, trs, choices, - ((Gs,haz@haz')::pairs, lits, vars, lim) :: brs) + {pairs = (Gs,haz@haz')::pairs, + lits = lits, + vars = vars, + lim = lim} :: brs) | prv (tacs, trs, choices, - brs0 as ([([], (H,md)::Hs)], lits, vars, lim) :: brs) = + brs0 as {pairs = [([], (H,md)::Hs)], + lits, vars, lim} :: brs) = (*no safe steps possible at any level: apply a haz rule*) let exception PRV (*backtrack to precisely this recursion!*) val H = norm H @@ -1059,14 +1081,15 @@ and lits' = if (exists isGoal prem) then map negOfGoal lits else lits - in (if exists (match P) prem - then (*Recursive in this premise. - Don't make new "stack frame". - New haz premises will end up at the BACK of the - queue, preventing exclusion of others*) - [(Gs',Hs')] - else [(Gs',[]), ([],Hs')], - lits', vars, lim') + in {pairs = if exists (match P) prem then [(Gs',Hs')] + (*Recursive in this premise. Don't make new + "stack frame". New haz premises will end up + at the BACK of the queue, preventing + exclusion of others*) + else [(Gs',[]), ([],Hs')], + lits = lits', + vars = vars, + lim = lim'} end fun newBr x prems = map (newPrem x) prems @ brs (*Seek a matching rule. If unifiable then add new premises @@ -1080,7 +1103,8 @@ val vars' = foldr add_terms_vars (prems, vars) (*duplicate H if md and the subgoal has new vars*) val dup = md andalso vars' <> vars - (*any instances of P in the subgoals?*) + (*any instances of P in the subgoals? + NB: this boolean affects tracing only!*) and recur = exists (exists (match P)) prems val lim' = (*Decrement "lim" extra if updates occur*) if updated then lim - (1+log(length rules)) @@ -1103,10 +1127,11 @@ orelse vars=vars' (*no new Vars?*) val tac' = if mayUndo then tac(updated, dup, true) else DETERM o tac(updated, dup, true) - (*if recur then doesn't call rotate_tac: - new formulae should be last; WRONG - if the new formulae are Goals, since - they remain in the first position*) + (*if recur then perhaps shouldn't call rotate_tac: new + formulae should be last, but that's WRONG if the new + formulae are Goals, since they remain in the first + position*) + in if lim'<0 andalso not (null prems) then (*it's faster to kill ALL the alternatives*) @@ -1137,7 +1162,10 @@ handle NEWBRANCHES => (*cannot close branch: move H to literals*) prv (tacs, brs0::trs, choices, - ([([], Hs)], H::lits, vars, lim)::brs) + {pairs = [([], Hs)], + lits = H::lits, + vars = vars, + lim = lim} :: brs) end | prv (tacs, trs, choices, _ :: brs) = backtrack choices in init_gensym(); @@ -1147,8 +1175,10 @@ (*Construct an initial branch.*) fun initBranch (ts,lim) = - ([(map (fn t => (t,true)) ts, [])], - [], add_terms_vars (ts,[]), lim); + {pairs = [(map (fn t => (t,true)) ts, [])], + lits = [], + vars = add_terms_vars (ts,[]), + lim = lim}; (*** Conversion & Skolemization of the Isabelle proof state ***) @@ -1237,6 +1267,8 @@ case Seq.pull(EVERY' (rev tacs) i st) of None => (writeln ("PROOF FAILED for depth " ^ Int.toString lim); + if !trace then writeln "************************\n" + else (); backtrack choices) | cell => (if (!trace orelse !stats) then writeln (endTiming start ^ " for reconstruction") @@ -1251,7 +1283,8 @@ fun depth_tac cs lim i st = timing_depth_tac (startTiming()) cs lim i st; fun blast_tac cs i st = - (DEEPEN (1,20) (timing_depth_tac (startTiming()) cs) 0) i st + ((DEEPEN (1,20) (timing_depth_tac (startTiming()) cs) 0) i + THEN flexflex_tac) st handle TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty); fun Blast_tac i = blast_tac (Data.claset()) i;