# HG changeset patch # User paulson # Date 862561130 -7200 # Node ID b92a1b50b16ba6744159906aa30e03b6a9a6807c # Parent 9366415b93ad54626d3d5d109eefe62107caabfa More tracing. hyp_subst_tac allowed to fail diff -r 9366415b93ad -r b92a1b50b16b src/Provers/blast.ML --- a/src/Provers/blast.ML Fri May 02 10:17:44 1997 +0200 +++ b/src/Provers/blast.ML Fri May 02 10:18:50 1997 +0200 @@ -20,9 +20,10 @@ * its proof strategy is more general but can actually be slower Known problems: - "Recursive" rules such as transitivity can exclude other unsafe formulae + "Recursive" chains of rules can sometimes exclude other unsafe formulae from expansion. This happens because newly-created formulae always - have priority over existing ones. + have priority over existing ones. But obviously recursive rules + such as transitivity are treated specially to prevent this. With overloading: Overloading can't follow all chains of type dependencies. Cannot @@ -34,9 +35,7 @@ type ... set) 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 substitution affects a haz formula or literal, it is moved + 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. @@ -106,7 +105,7 @@ end; -functor BlastFun(Data: BLAST_DATA)(**********: BLAST*******) = +functor BlastFun(Data: BLAST_DATA) : BLAST = struct type claset = Data.claset; @@ -124,13 +123,6 @@ | op $ of term*term; -exception DEST_EQ; - - (*Take apart an equality (plain or overloaded). NO constant Trueprop*) - fun dest_eq (Const "op =" $ t $ u) = (t,u) - | dest_eq (OConst("op =",_) $ t $ u) = (t,u) - | dest_eq _ = raise DEST_EQ; - (** Basic syntactic operations **) fun is_Var (Var _) = true @@ -308,7 +300,7 @@ in subst (t,0) end; -(*Normalize...but not the bodies of ABSTRACTIONS*) +(*Normalize, INCLUDING bodies of abstractions--this might be slow?*) fun norm t = case t of Skolem (a,args) => Skolem(a, vars_in_vars args) | (Var (ref None)) => t @@ -316,6 +308,7 @@ | (f $ u) => (case norm f of Abs(_,body) => norm (subst_bound (u, body)) | nf => nf $ norm u) + | Abs (a,body) => Abs (a, norm body) | _ => t; @@ -333,7 +326,7 @@ if (0 mem_int loose_bnos f) orelse wkNorm t <> Bound 0 then Abs(a,nb) else wkNorm (incr_boundvars ~1 f) - | nb => Abs (a,nb)) + | nb => Abs (a,nb)) | _ => t and wkNorm t = case head_of t of Const _ => t @@ -553,6 +546,77 @@ end; **) + +(*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*) + +val fullTrace = ref[] : branch list list ref; + +(*Normalize a branch--for tracing*) +fun norm2 (G,md) = (norm G, md); + +fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs); + +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 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 _) = 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); + + +fun traceTerm sign t = Sign.string_of_term sign (showTerm 8 (norm t)); + + +(*Print tracing information at each iteration of prover*) +fun tracing sign brs = + 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) = + (fullTrace := brs0 :: !fullTrace; + seq (fn _ => prs "+") brs; + prs (" [" ^ Int.toString lim ^ "] "); + printPairs pairs; + writeln"") + in if !trace then printBrs (map normBr brs) else () + end; + +(*Tracing: variables updated in the last branch operation?*) +fun traceVars ntrl = + if !trace then + (case !ntrail-ntrl of + 0 => writeln"" + | 1 => writeln"\t1 variable updated" + | n => writeln("\t" ^ Int.toString n ^ " variables updated")) + else (); + +(*Tracing: how many new branches are created?*) +fun traceNew prems = + if !trace then + case length prems of + 0 => prs"branch closed by rule" + | 1 => prs"branch extended (1 new subgoal)" + | n => prs("branch split: "^ Int.toString n ^ " new subgoals") + else (); + + + (*** Code for handling equality: naive substitution, like hyp_subst_tac ***) (*Replace the ATOMIC term "old" by "new" in t*) @@ -593,26 +657,32 @@ | occ (_) = false; in occEq end; +exception DEST_EQ; + +(*Take apart an equality (plain or overloaded). NO constant Trueprop*) +fun dest_eq (Const "op =" $ t $ u) = + (eta_contract_atom t, eta_contract_atom u) + | dest_eq (OConst("op =",_) $ t $ u) = + (eta_contract_atom t, eta_contract_atom u) + | dest_eq _ = raise DEST_EQ; + fun check (t,u,v) = if substOccur t u then raise DEST_EQ else v; (*IF the goal is an equality with a substitutable variable THEN orient that equality ELSE raise exception DEST_EQ*) -fun orientGoal (t,u) = - case (eta_contract_atom t, eta_contract_atom u) of +fun orientGoal (t,u) = case (t,u) of (Skolem _, _) => check(t,u,(t,u)) (*eliminates t*) | (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*) | (Free _, _) => check(t,u,(t,u)) (*eliminates t*) | (_, Free _) => check(u,t,(u,t)) (*eliminates u*) | _ => 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 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) (*substitute throughout Haz list; move affected ones to Safe part*) fun subHazs ([], Gs, nHs) = (Gs,nHs) @@ -630,72 +700,15 @@ in if nlit aconv lit then subLits (lits, Gs, nlit::nlits) else subLits (lits, (nlit,true)::Gs, nlits) end - in if !trace then writeln "substitution in branch" else (); + in if !trace then writeln ("Substituting " ^ traceTerm sign u ^ + " for " ^ traceTerm sign t ^ " in branch" ) + else (); subLits (rev lits, [], []) end; exception NEWBRANCHES and CLOSEF; -(*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*) - -val fullTrace = ref[] : branch list list ref; - -(*Normalize a branch--for tracing*) -fun norm2 (G,md) = (norm G, md); - -fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs); - -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 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 _) = 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 8 t)) - fun printPairs (((G,_)::_,_)::_) = pr G - | printPairs (([],(H,_)::_)::_) = (pr H; prs"\t (Unsafe)") - | printPairs _ = () - fun printBrs (brs0 as (pairs, lits, _, lim) :: brs) = - (fullTrace := brs0 :: !fullTrace; - seq (fn _ => prs "+") brs; - prs (" [" ^ Int.toString lim ^ "] "); - printPairs pairs; - writeln"") - in if !trace then printBrs (map normBr brs) else () - 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; val eq_contr_tac = eresolve_tac [Data.notE] THEN' eq_assume_tac; @@ -873,7 +886,7 @@ val tacs' = (DETERM o (tac false)) :: tacs (*no duplication*) in - traceNew prems; + traceNew prems; traceVars ntrl; (if null prems then (*closed the branch: prune!*) prv(tacs', brs0::trs, prune (nbrs, nxtVars, choices'), @@ -901,7 +914,8 @@ None => closeF Ls | Some tac => let val choices' = - (if !trace then writeln"branch closed" + (if !trace then (prs"branch closed"; + traceVars ntrl) else (); prune (nbrs, nxtVars, (ntrl, nbrs, PRV) :: choices)) @@ -919,9 +933,12 @@ in tracing sign brs0; if lim<0 then backtrack choices else - prv (Data.vars_gen_hyp_subst_tac false :: tacs, + prv ((TRY o Data.vars_gen_hyp_subst_tac false) :: tacs, + (*The TRY above allows the substitution to fail, e.g. if + the real version is z = f(?x z). Rest of proof might + still succeed!*) brs0::trs, choices, - equalSubst (G, (br,haz)::pairs, lits, vars, lim) :: brs) + equalSubst sign (G, (br,haz)::pairs, lits, vars, lim) :: brs) handle DEST_EQ => closeF lits handle CLOSEF => closeFl ((br,haz)::pairs) handle CLOSEF => @@ -989,7 +1006,7 @@ then (*it's faster to kill ALL the alternatives*) raise NEWBRANCHES else - traceNew prems; + traceNew prems; traceVars ntrl; prv(tac dup :: tacs, brs0::trs, (ntrl, length brs0, PRV) :: choices, @@ -1073,7 +1090,7 @@ fun skoSubgoal i t = if i