# HG changeset patch # User paulson # Date 860582212 -7200 # Node ID af506c35b4edb2e5b4a69157b3c4df44e7f54c2b # Parent f675fb52727ba22e95ab52ef572fb2bcf6952ad2 Control over excessive branching by applying a log2 penalty Incorporation of debugging features Allows backtracking over haz rules if alternatives exist Subsitution for equality may more a rule from the haz to the safe part diff -r f675fb52727b -r af506c35b4ed src/Provers/blast.ML --- a/src/Provers/blast.ML Wed Apr 09 12:34:28 1997 +0200 +++ b/src/Provers/blast.ML Wed Apr 09 12:36:52 1997 +0200 @@ -9,21 +9,24 @@ Needs explicit instantiation of assumptions? -Limitations compared with fast_tac: +Blast_tac is often more powerful than fast_tac, but has some limitations. +Blast_tac... * ignores addss, addbefore, addafter; this restriction is intrinsic - * seems to loop given transitivity and similar rules * ignores elimination rules that don't have the correct format (conclusion must be a formula variable) * ignores types, which can make HOL proofs fail + * rules must not require higher-order unification, e.g. apply_type in ZF + + message "Function Var's argument not a bound variable" relates to this + * its proof strategy is more general but can actually be slower Known problems: - With hyp_subst_tac: + With substition for equalities (hyp_subst_tac): 1. Sometimes hyp_subst_tac will fail due to occurrence of the parameter as the argument of a function variable - 2. When a literal is affected, it is moved back to the active formulae. - But there's no way of putting it in the right place. - 3. Affected haz formulae should also be moved, but they are not. - + 2. When substitution affects a haz formula or literal, it is moved + back to the list of safe formulae. + But there's no way of putting it in the right place. A "moved" or + "no DETERM" flag would prevent proofs failing here. *) @@ -58,15 +61,39 @@ signature BLAST = sig - type claset + type claset + datatype term = + Const of string + | OConst of string * int + | Skolem of string * term option ref list + | Free of string + | Var of term option ref + | Bound of int + | Abs of string*term + | op $ of term*term; + type branch val depth_tac : claset -> int -> int -> tactic val blast_tac : claset -> int -> tactic val Blast_tac : int -> tactic val declConsts : string list * thm list -> unit + (*debugging tools*) + val trace : bool ref + val fullTrace : branch list list ref + val fromTerm : Type.type_sig -> Term.term -> term + val fromSubgoal : Type.type_sig -> Term.term -> term + 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 + 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 + val normBr : branch -> branch end; -functor BlastFun(Data: BLAST_DATA) = +functor BlastFun(Data: BLAST_DATA): BLAST = struct type claset = Data.claset; @@ -433,11 +460,15 @@ val trl = rl |> rep_thm |> #prop |> fromTerm tsig |> convertRule vars fun tac dup i = TRACE rl - (DETERM (etac (if dup then rev_dup_elim rl else rl) i)) + (etac (if dup then rev_dup_elim rl else rl) i) THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i in General.SOME (trl, tac) end - handle Bind => General.NONE (*reject: conclusion is not just a variable*); + handle Bind => (*reject: conclusion is not just a variable*) + (if !trace then (writeln"Warning: ignoring ill-formed elimination rule"; + print_thm rl) + else (); + General.NONE); (*** Conversion of Introduction Rules (needed for efficiency in @@ -465,28 +496,28 @@ val dummyVar = Term.Var (("Doom",666), dummyT); (*Convert from prototerms to ordinary terms with dummy types - Ignore abstractions; identify all Vars*) -fun dummyTerm 0 _ = dummyVar - | dummyTerm d (Const a) = Term.Const (a,dummyT) - | dummyTerm d (OConst(a,_)) = Term.Const (a,dummyT) - | dummyTerm d (Skolem(a,_)) = Term.Const (a,dummyT) - | dummyTerm d (Free a) = Term.Free (a,dummyT) - | dummyTerm d (Bound i) = Term.Bound i - | dummyTerm d (Var _) = dummyVar - | dummyTerm d (Abs(a,_)) = dummyVar - | dummyTerm d (f $ u) = Term.$ (dummyTerm d f, dummyTerm (d-1) u); + Ignore abstractions; identify all Vars; STOP at given depth*) +fun toTerm 0 _ = dummyVar + | toTerm d (Const a) = Term.Const (a,dummyT) + | toTerm d (OConst(a,_)) = Term.Const (a,dummyT) + | toTerm d (Skolem(a,_)) = Term.Const (a,dummyT) + | toTerm d (Free a) = Term.Free (a,dummyT) + | toTerm d (Bound i) = Term.Bound i + | toTerm d (Var _) = dummyVar + | toTerm d (Abs(a,_)) = dummyVar + | toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d-1) u); fun netMkRules P vars (nps: netpair list) = case P of (Const "*Goal*" $ G) => - let val pG = mk_tprop (dummyTerm 2 G) + let val pG = mk_tprop (toTerm 2 G) val intrs = List.concat (map (fn (inet,_) => Net.unify_term inet pG) nps) in map (fromIntrRule vars o #2) (orderlist intrs) end | _ => - let val pP = mk_tprop (dummyTerm 3 P) + let val pP = mk_tprop (toTerm 3 P) val elims = List.concat (map (fn (_,enet) => Net.unify_term enet pP) nps) @@ -549,14 +580,23 @@ | _ => raise DEST_EQ; + + (*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 (G, pairs, lits, vars, lim) = let val subst = subst_atomic (orientGoal(dest_eq G)) fun subst2(G,md) = (subst G, md) - val pairs' = map (fn(Gs,Hs) => (map subst2 Gs, map subst2 Hs)) pairs - (*substitute throughout literals and note those affected*) + (*substitute throughout Haz list; move affected ones to Safe part*) + fun subHazs ([], Gs, nHs) = (Gs,nHs) + | subHazs ((H,md)::Hs, Gs, nHs) = + let val nH = subst H + in if nH aconv H then subHazs (Hs, Gs, (H,md)::nHs) + else subHazs (Hs, (nH,md)::Gs, nHs) + end + val pairs' = map (fn(Gs,Hs) => subHazs(rev Hs, map subst2 Gs, [])) pairs + (*substitute throughout literals; move affected ones to Safe part*) fun subLits ([], [], nlits) = (pairs', nlits, vars, lim) | subLits ([], Gs, nlits) = ((Gs,[])::pairs', nlits, vars, lim) | subLits (lit::lits, Gs, nlits) = @@ -579,6 +619,21 @@ val fullTrace = ref[] : branch list list ref; +(*Normalize a branch--for tracing*) +local + fun norm2 (G,md) = (norm G, md); + + 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); + +fun tracing brs = if !trace then fullTrace := map normBr brs :: !fullTrace + else () +end; + + exception PROVE; val eq_contr_tac = eresolve_tac [Data.notE] THEN' eq_assume_tac; @@ -685,6 +740,11 @@ | addLit (G,lits) = ins_term(G, lits) +(*For calculating the "penalty" to assess on a branching factor of n*) +fun log2 1 = 0 + | log2 n = 1 + log2(n div 2); + + (*Tableau prover based on leanTaP. Argument is a list of branches. Each branch contains a list of unexpanded formulae, a list of literals, and a bound on unsafe expansions.*) @@ -700,6 +760,7 @@ val nbrs = length brs0 val nxtVars = nextVars brs val G = norm G + val rules = netMkRules G vars safeList (*Make a new branch, decrementing "lim" if instantiations occur*) fun newBr (vars',lim') prems = map (fn prem => @@ -719,22 +780,25 @@ let val dummy = unify(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-3 else lim + val lim' = if ntrl < !ntrail + then lim - (1+log2(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(tac false :: tacs, (*no duplication*) - brs0::trs, + prv(tacs', brs0::trs, prune (nbrs, nxtVars, choices'), brs) - handle PRV => - (*reset Vars and try another rule*) + handle PRV => (*reset Vars and try another rule*) (clearTo ntrl; deeper grls) - else - prv(tac false :: tacs, (*no duplication*) - brs0::trs, choices', + else (*can we kill all the alternatives??*) + if lim'<0 then raise NEWBRANCHES + else + prv(tacs', brs0::trs, choices', newBr (vars',lim') prems) handle PRV => if ntrl < ntrl' then @@ -764,7 +828,7 @@ closeF (map fst br) handle CLOSEF => closeF (map fst haz) handle CLOSEF => closeFl pairs - in if !trace then fullTrace := brs0 :: !fullTrace else (); + in tracing brs0; if lim<0 then backtrack choices else prv (Data.vars_gen_hyp_subst_tac false :: tacs, @@ -773,7 +837,7 @@ handle DEST_EQ => closeF lits handle CLOSEF => closeFl ((br,haz)::pairs) handle CLOSEF => - deeper (netMkRules G vars safeList) + deeper rules handle NEWBRANCHES => (case netMkRules G vars hazList of [] => (*no plausible rules: move G to literals*) @@ -787,26 +851,22 @@ ((br, haz@[(negOfGoal G, md)])::pairs, lits, vars, lim) :: brs)) end - | prv (tacs, trs, choices, (([],haz)::(Gs,haz')::pairs, - lits, vars, lim) :: brs) = + | prv (tacs, trs, choices, + (([],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) + prv (tacs, trs, choices, + ((Gs,haz@haz')::pairs, lits, vars, lim) :: brs) | prv (tacs, trs, choices, brs0 as ([([], (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 val ntrl = !ntrail - fun newPrem (vars,dup) prem = + val rules = netMkRules H vars hazList + fun newPrem (vars,dup,lim') prem = ([(map (fn P => (P,false)) prem, []), (*may NOT duplicate*) ([], if dup then Hs @ [(negOfGoal H, md)] else Hs)], - lits, - vars, - (*Decrement "lim" if instantiations occur or the - formula is duplicated*) - if ntrl < !ntrail then lim-3 - else if dup then lim-1 else lim) + lits, vars, lim') fun newBr x prems = map (newPrem x) prems @ brs (*Seek a matching rule. If unifiable then add new premises to branch.*) @@ -818,24 +878,37 @@ val vars' = foldr add_terms_vars (prems, vars) val dup = md andalso vars' <> vars (*duplicate H only if md and the premise has new vars*) - in - prv(tac dup :: tacs, - brs0::trs, - (ntrl, length brs0, PRV) :: choices, - newBr (vars', dup) prems) - handle PRV => - if ntrl < ntrl' (*variables updated?*) - orelse vars=vars' (*pseudo-unsafe: no new Vars?*) - then (*reset Vars and try another rule*) - (clearTo ntrl; deeper grls) - else (*backtrack to previous level*) - backtrack choices + val lim' = (*Decrement "lim" extra if updates occur*) + if ntrl < !ntrail then lim - (1+log2(length rules)) + else lim-1 + (*NB: if the formula is duplicated, + then it seems plausible to leave lim alone. + But then transitivity laws loop.*) + 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 + (*can we kill all the alternatives??*) + if lim'<0 andalso not (null prems) + then raise NEWBRANCHES + else + prv(tac dup :: tacs, + brs0::trs, + (ntrl, length brs0, PRV) :: choices, + newBr (vars', 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 if !trace then fullTrace := brs0 :: !fullTrace else (); + in tracing brs0; if lim<1 then backtrack choices - else - deeper (netMkRules H vars hazList) + else deeper rules handle NEWBRANCHES => (*cannot close branch: move H to literals*) prv (tacs, brs0::trs, choices, @@ -934,5 +1007,36 @@ fun Blast_tac i = blast_tac (!Data.claset) i; + +(*** For debugging: these apply the prover to a subgoal and return + the resulting tactics, trace, etc. ***) + +(*Translate subgoal i from a proof state*) +fun trygl cs lim i = + (fullTrace:=[]; trail := []; ntrail := 0; + let val st = topthm() + val {tsig,...} = Sign.rep_sg (#sign (rep_thm st)) + val skoprem = fromSubgoal tsig (List.nth(prems_of st, i-1)) + val hyps = strip_imp_prems skoprem + and concl = strip_imp_concl skoprem + in timeap prove + (cs, [initBranch (mkGoal concl :: hyps, lim)], I) + end + handle Subscript => error("There is no subgoal " ^ Int.toString i)); + +fun Trygl lim i = trygl (!Data.claset) lim i; + +(*Read a string to make an initial, singleton branch*) +fun readGoal sign s = read_cterm sign (s,propT) |> + term_of |> fromTerm (#tsig(Sign.rep_sg sign)) |> + rand |> mkGoal; + +fun tryInThy thy lim s = + (fullTrace:=[]; trail := []; ntrail := 0; + timeap prove (!Data.claset, + [initBranch ([readGoal (sign_of thy) s], lim)], + I)); + + end;