# HG changeset patch # User paulson # Date 862397964 -7200 # Node ID 1a7edbd7f55afff2382a8367cef65bea0322c3d5 # Parent 9b68848654bf73083d12573c22919fdd33746f61 More tracing; less exception handling diff -r 9b68848654bf -r 1a7edbd7f55a src/Provers/blast.ML --- a/src/Provers/blast.ML Wed Apr 30 12:13:17 1997 +0200 +++ b/src/Provers/blast.ML Wed Apr 30 12:59:24 1997 +0200 @@ -1,7 +1,7 @@ (* Title: Provers/blast ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge + Copyright 1997 University of Cambridge Generic tableau prover with proof reconstruction @@ -97,11 +97,11 @@ val toTerm : int -> term -> Term.term val readGoal : Sign.sg -> string -> term val tryInThy : theory -> int -> string -> - branch list list * (int*int*exn) list * (int -> tactic) list + (int->tactic) list * branch list list * (int*int*exn) list val trygl : claset -> int -> int -> - branch list list * (int*int*exn) list * (int -> tactic) list - val Trygl : int -> int -> - branch list list * (int*int*exn) list * (int -> tactic) list + (int->tactic) list * branch list list * (int*int*exn) list + val Trygl : int -> int -> + (int->tactic) list * branch list list * (int*int*exn) list val normBr : branch -> branch end; @@ -365,7 +365,7 @@ (*Restore the trail to some previous state: for backtracking*) fun clearTo n = - while !ntrail>n do + while !ntrail<>n do (hd(!trail) := None; trail := tl (!trail); ntrail := !ntrail - 1); @@ -398,7 +398,7 @@ (*NB: can yield unifiers having dangling Bound vars!*) | (f$t', g$u') => (unifyAux(f,g); unifyAux(t',u')) | (nt, nu) => if nt aconv nu then () else raise UNIFY - in unifyAux(t,u) handle UNIFY => (clearTo n; raise UNIFY) + in (unifyAux(t,u); true) handle UNIFY => (clearTo n; false) end; @@ -477,6 +477,8 @@ fun TRACE rl tac st i = if !trace then (prth rl; tac st i) else tac st i; +local open General in (*make available the Basis type "option"*) + (*Tableau rule from elimination rule. Flag "dup" requests duplication of the affected formula.*) fun fromRule vars rl = @@ -492,6 +494,7 @@ print_thm rl) else (); NONE); +end; (*** Conversion of Introduction Rules (needed for efficiency in @@ -627,7 +630,8 @@ in if nlit aconv lit then subLits (lits, Gs, nlit::nlits) else subLits (lits, (nlit,true)::Gs, nlits) end - in subLits (rev lits, [], []) + in if !trace then writeln "substitution in branch" else (); + subLits (rev lits, [], []) end; @@ -643,32 +647,34 @@ val fullTrace = ref[] : branch list list ref; (*Normalize a branch--for tracing*) -local - fun norm2 (G,md) = (norm G, md); +fun norm2 (G,md) = (norm G, md); - fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs); +fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs); -in fun normBr (br, lits, vars, lim) = (map normLev br, map norm lits, vars, lim); +val dummyVar2 = Term.Var(("var",0), dummyT); + (*Convert from prototerms to ordinary terms with dummy types for tracing*) -fun showTerm 0 _ = dummyVar - | showTerm d (Const a) = Term.Const (a,dummyT) +fun showTerm d (Const a) = Term.Const (a,dummyT) | showTerm d (OConst(a,_)) = Term.Const (a,dummyT) | showTerm d (Skolem(a,_)) = Term.Const (a,dummyT) | showTerm d (Free a) = Term.Free (a,dummyT) | showTerm d (Bound i) = Term.Bound i - | showTerm d (Var _) = dummyVar - | showTerm d (Abs(a,t)) = Term.Abs(a, dummyT, showTerm (d-1) t) - | showTerm d (f $ u) = Term.$ (showTerm d f, showTerm (d-1) u); + | showTerm d (Var _) = dummyVar2 + | showTerm d (Abs(a,t)) = if d=0 then dummyVar + else Term.Abs(a, dummyT, showTerm (d-1) t) + | showTerm d (f $ u) = if d=0 then dummyVar + else Term.$ (showTerm d f, showTerm (d-1) u); +(*Print tracing information at each iteration of prover*) fun tracing sign brs = - let fun pr t = prs (Sign.string_of_term sign (showTerm 5 t)) + let fun pr t = prs (Sign.string_of_term sign (showTerm 8 t)) fun printPairs (((G,_)::_,_)::_) = pr G - | printPairs (([],(H,_)::_)::_) = (prs"Haz: "; pr H) + | printPairs (([],(H,_)::_)::_) = (pr H; prs"\t (Unsafe)") | printPairs _ = () fun printBrs (brs0 as (pairs, lits, _, lim) :: brs) = (fullTrace := brs0 :: !fullTrace; @@ -679,7 +685,15 @@ in if !trace then printBrs (map normBr brs) else () end; -end; +fun traceNew prems = + if !trace then + case length prems of + 0 => writeln"branch closed by rule" + | 1 => writeln"branch extended (1 new subgoal)" + | n => writeln("branch split: "^ Int.toString n ^ + " new subgoals") + else (); + exception PROVE; @@ -690,11 +704,15 @@ val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac); (*Try to unify complementary literals and return the corresponding tactic. *) -fun tryClose (Const"*Goal*" $ G, L) = (unify(true,[],G,L); eAssume_tac) - | tryClose (G, Const"*Goal*" $ L) = (unify(true,[],G,L); eAssume_tac) - | tryClose (Const"Not" $ G, L) = (unify(true,[],G,L); eContr_tac) - | tryClose (G, Const"Not" $ L) = (unify(true,[],G,L); eContr_tac) - | tryClose _ = raise UNIFY; +fun tryClose (Const"*Goal*" $ G, L) = + if unify(true,[],G,L) then Some eAssume_tac else None + | tryClose (G, Const"*Goal*" $ L) = + if unify(true,[],G,L) then Some eAssume_tac else None + | tryClose (Const"Not" $ G, L) = + if unify(true,[],G,L) then Some eContr_tac else None + | tryClose (G, Const"Not" $ L) = + if unify(true,[],G,L) then Some eContr_tac else None + | tryClose _ = None; (*Were there Skolem terms in the premise? Must NOT chase Vars*) @@ -746,12 +764,12 @@ let val ll = length last and lc = length choices in if !trace andalso ll nbrs then pruneAux (last, ntrl, trl, choices) @@ -763,10 +781,14 @@ in traceIt (pruneAux (choices, !ntrail, !trail, choices)) end; fun nextVars ((br, lits, vars, lim) :: _) = map Var vars - | nextVars [] = []; + | nextVars [] = []; -fun backtrack ((_, _, exn)::_) = raise exn - | backtrack _ = raise PROVE; +fun backtrack (choices as (ntrl, nbrs, exn)::_) = + (if !trace then (writeln ("Backtracking; now there are " ^ + Int.toString nbrs ^ " branches")) + else (); + raise exn) + | backtrack _ = raise PROVE; (*Add the literal G, handling *Goal* and detecting duplicates.*) fun addLit (Const "*Goal*" $ G, lits) = @@ -790,7 +812,7 @@ (*For calculating the "penalty" to assess on a branching factor of n log2 seems a little too severe*) -fun log4 n = if n<4 then 0 else 1 + log4(n div 4); +fun log n = if n<4 then 0 else 1 + log(n div 4); (*match(t,u) says whether the term u might be an instance of the pattern t @@ -814,7 +836,7 @@ let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_claset cs val safeList = [safe0_netpair, safep_netpair] and hazList = [haz_netpair] - fun prv (tacs, trs, choices, []) = (cont (trs,choices,tacs)) + fun prv (tacs, trs, choices, []) = cont (tacs, trs, choices) | prv (tacs, trs, choices, brs0 as (((G,md)::br, haz)::pairs, lits, vars, lim) :: brs) = let exception PRV (*backtrack to precisely this recursion!*) @@ -839,59 +861,62 @@ to branch.*) fun deeper [] = raise NEWBRANCHES | deeper (((P,prems),tac)::grls) = - let val dummy = unify(false, add_term_vars(P,[]), P, G) - (*P comes from the rule; G comes from the branch.*) - val ntrl' = !ntrail - val lim' = if ntrl < !ntrail - then lim - (1+log4(length rules)) - else lim (*discourage branching updates*) - 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 false)) :: tacs - (*no duplication*) - in - if null prems then (*closed the branch: prune!*) - prv(tacs', brs0::trs, - prune (nbrs, nxtVars, choices'), - brs) - handle PRV => (*reset Vars and try another rule*) - (clearTo ntrl; deeper grls) - else - if lim'<0 (*it's faster to kill ALL the alternatives*) - then raise NEWBRANCHES - else - prv(tacs', brs0::trs, choices', - newBr (vars',lim') prems) - handle PRV => - if ntrl < ntrl' (*Vars have been updated*) - then - (*Backtrack at this level. - Reset Vars and try another rule*) - (clearTo ntrl; deeper grls) - else (*backtrack to previous level*) - backtrack choices - end - handle UNIFY => deeper grls + if unify(false, add_term_vars(P,[]), P, G) + then (*P comes from the rule; G comes from the branch.*) + let val ntrl' = !ntrail + val lim' = if ntrl < !ntrail + then lim - (1+log(length rules)) + else lim (*discourage branching updates*) + 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 false)) :: tacs + (*no duplication*) + in + traceNew prems; + (if null prems then (*closed the branch: prune!*) + prv(tacs', brs0::trs, + prune (nbrs, nxtVars, choices'), + brs) + else + if lim'<0 (*faster to kill ALL the alternatives*) + then raise NEWBRANCHES + else + prv(tacs', brs0::trs, choices', + newBr (vars',lim') prems)) + handle PRV => + if ntrl < ntrl' (*Vars have been updated*) + then + (*Backtrack at this level. + Reset Vars and try another rule*) + (clearTo ntrl; deeper grls) + else (*backtrack to previous level*) + backtrack choices + end + else deeper grls (*Try to close branch by unifying with head goal*) fun closeF [] = raise CLOSEF | closeF (L::Ls) = - let val tacs' = tryClose(G,L)::tacs - val choices' = prune (nbrs, nxtVars, - (ntrl, nbrs, PRV) :: choices) - in prv (tacs', brs0::trs, choices', brs) - handle PRV => - (*reset Vars and try another literal - [this handler is pruned if possible!]*) - (clearTo ntrl; closeF Ls) - end - handle UNIFY => closeF Ls + case tryClose(G,L) of + None => closeF Ls + | Some tac => + let val choices' = + (if !trace then writeln"branch closed" + else (); + prune (nbrs, nxtVars, + (ntrl, nbrs, PRV) :: choices)) + in prv (tac::tacs, brs0::trs, choices', brs) + handle PRV => + (*reset Vars and try another literal + [this handler is pruned if possible!]*) + (clearTo ntrl; closeF Ls) + end fun closeFl [] = raise CLOSEF | closeFl ((br, haz)::pairs) = closeF (map fst br) handle CLOSEF => closeF (map fst haz) handle CLOSEF => closeFl pairs - in tracing sign brs0; + in tracing sign brs0; if lim<0 then backtrack choices else prv (Data.vars_gen_hyp_subst_tac false :: tacs, @@ -938,44 +963,46 @@ to branch.*) fun deeper [] = raise NEWBRANCHES | deeper (((P,prems),tac)::grls) = - let val dummy = unify(false, add_term_vars(P,[]), P, H) - val ntrl' = !ntrail - val vars = vars_in_vars vars - 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?*) - and recur = exists (exists (match P)) prems - val lim' = (*Decrement "lim" extra if updates occur*) - if ntrl < !ntrail then lim - (1+log4(length rules)) - else lim-1 - (*It is tempting to leave "lim" UNCHANGED if - both dup and recur are false. Proofs are - found at shallower depths, but looping - occurs too often...*) - val mayUndo = not (null grls) (*other rules to try?*) - orelse ntrl < ntrl' (*variables updated?*) - orelse vars=vars' (*no new Vars?*) - val tac' = if mayUndo then tac dup - else DETERM o (tac dup) - in - if lim'<0 andalso not (null prems) - then (*it's faster to kill ALL the alternatives*) - raise NEWBRANCHES - else - prv(tac dup :: tacs, - brs0::trs, - (ntrl, length brs0, PRV) :: choices, - newBr (vars', recur, dup, lim') prems) - handle PRV => - if mayUndo - then (*reset Vars and try another rule*) - (clearTo ntrl; deeper grls) - else (*backtrack to previous level*) - backtrack choices - end - handle UNIFY => deeper grls - in tracing sign brs0; + if unify(false, add_term_vars(P,[]), P, H) + then + let val ntrl' = !ntrail + val vars = vars_in_vars vars + 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?*) + and recur = exists (exists (match P)) prems + val lim' = (*Decrement "lim" extra if updates occur*) + if ntrl < !ntrail then lim - (1+log(length rules)) + else lim-1 + (*It is tempting to leave "lim" UNCHANGED if + both dup and recur are false. Proofs are + found at shallower depths, but looping + occurs too often...*) + val mayUndo = not(null grls) (*other rules to try?*) + orelse ntrl < ntrl' (*variables updated?*) + orelse vars=vars' (*no new Vars?*) + val tac' = if mayUndo then tac dup + else DETERM o (tac dup) + in + if lim'<0 andalso not (null prems) + then (*it's faster to kill ALL the alternatives*) + raise NEWBRANCHES + else + traceNew prems; + prv(tac dup :: tacs, + brs0::trs, + (ntrl, length brs0, PRV) :: choices, + newBr (vars', recur, dup, lim') prems) + handle PRV => + if mayUndo + then (*reset Vars and try another rule*) + (clearTo ntrl; deeper grls) + else (*backtrack to previous level*) + backtrack choices + end + else deeper grls + in tracing sign brs0; if lim<1 then backtrack choices else deeper rules handle NEWBRANCHES => @@ -1062,7 +1089,7 @@ val skoprem = fromSubgoal tsig (List.nth(prems_of st, i-1)) val hyps = strip_imp_prems skoprem and concl = strip_imp_concl skoprem - fun cont (_,choices,tacs) = + fun cont (tacs,_,choices) = (case Sequence.pull(EVERY' (rev tacs) i st) of None => (writeln ("PROOF FAILED for depth " ^ Int.toString lim);