# HG changeset patch # User wenzelm # Date 1305372415 -7200 # Node ID da4ad5f989532907cee9f325195be5dabc74ec8f # Parent df2dc94062870494814418a546556962a3eeb64b proper Proof.context -- eliminated global operations; diff -r df2dc9406287 -r da4ad5f98953 src/Provers/blast.ML --- a/src/Provers/blast.ML Sat May 14 12:40:11 2011 +0200 +++ b/src/Provers/blast.ML Sat May 14 13:26:55 2011 +0200 @@ -109,7 +109,7 @@ (* global state information *) datatype state = State of - {thy: theory, + {ctxt: Proof.context, fullTrace: branch list list Unsynchronized.ref, trail: term option Unsynchronized.ref list Unsynchronized.ref, ntrail: int Unsynchronized.ref, @@ -120,16 +120,20 @@ is_some (Sign.const_type thy c) andalso error ("blast: theory contains illegal constant " ^ quote c); -fun initialize thy = - (reject_const thy "*Goal*"; - reject_const thy "*False*"; - State - {thy = thy, - fullTrace = Unsynchronized.ref [], - trail = Unsynchronized.ref [], - ntrail = Unsynchronized.ref 0, - nclosed = Unsynchronized.ref 0, (*branches closed: number of branches closed during the search*) - ntried = Unsynchronized.ref 1}); (*branches tried: number of branches created by splitting (counting from 1)*) +fun initialize ctxt = + let + val thy = Proof_Context.theory_of ctxt; + val _ = reject_const thy "*Goal*"; + val _ = reject_const thy "*False*"; + in + State + {ctxt = ctxt, + fullTrace = Unsynchronized.ref [], + trail = Unsynchronized.ref [], + ntrail = Unsynchronized.ref 0, + nclosed = Unsynchronized.ref 0, (*number of branches closed during the search*) + ntried = Unsynchronized.ref 1} (*number of branches created by splitting (counting from 1)*) + end; @@ -168,7 +172,7 @@ fun isGoal (Const ("*Goal*", _) $ _) = true | isGoal _ = false; -val TruepropC = Object_Logic.judgment_name Data.thy; +val TruepropC = Object_Logic.judgment_name Data.thy; (* FIXME *) val TruepropT = Sign.the_const_type Data.thy TruepropC; fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t); @@ -491,8 +495,9 @@ (*Tableau rule from elimination rule. Flag "upd" says that the inference updated the branch. Flag "dup" requests duplication of the affected formula.*) -fun fromRule thy vars rl = - let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule vars +fun fromRule ctxt vars rl = + let val thy = Proof_Context.theory_of ctxt + val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule vars fun tac (upd, dup,rot) i = emtac upd (if dup then rev_dup_elim rl else rl) i THEN @@ -500,12 +505,12 @@ in Option.SOME (trl, tac) end handle ElimBadPrem => (*reject: prems don't preserve conclusion*) - (warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm_global thy rl); + (warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm ctxt rl); Option.NONE) | ElimBadConcl => (*ignore: conclusion is not just a variable*) (if !trace then (warning ("Ignoring ill-formed elimination rule:\n" ^ - "conclusion should be a variable\n" ^ Display.string_of_thm_global thy rl)) + "conclusion should be a variable\n" ^ Display.string_of_thm ctxt rl)) else (); Option.NONE); @@ -525,8 +530,9 @@ Flag "dup" requests duplication of the affected formula. Since haz rules are now delayed, "dup" is always FALSE for introduction rules.*) -fun fromIntrRule thy vars rl = - let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars +fun fromIntrRule ctxt vars rl = + let val thy = Proof_Context.theory_of ctxt + val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars fun tac (upd,dup,rot) i = rmtac upd (if dup then Classical.dup_intr rl else rl) i THEN @@ -548,16 +554,16 @@ | toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d-1) u); -fun netMkRules thy P vars (nps: netpair list) = +fun netMkRules ctxt P vars (nps: netpair list) = case P of (Const ("*Goal*", _) $ G) => let val pG = mk_Trueprop (toTerm 2 G) val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps - in map (fromIntrRule thy vars o #2) (order_list intrs) end + in map (fromIntrRule ctxt vars o #2) (order_list intrs) end | _ => let val pP = mk_Trueprop (toTerm 3 P) val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps - in map_filter (fromRule thy vars o #2) (order_list elims) end; + in map_filter (fromRule ctxt vars o #2) (order_list elims) end; (*Normalize a branch--for tracing*) @@ -602,7 +608,7 @@ | showTerm d (f $ u) = if d=0 then dummyVar else Term.$ (showTerm d f, showTerm (d-1) u); -fun string_of thy d t = Syntax.string_of_term_global thy (showTerm d t); +fun string_of ctxt d t = Syntax.string_of_term ctxt (showTerm d t); (*Convert a Goal to an ordinary Not. Used also in dup_intr, where a goal like Ex(P) is duplicated as the assumption ~Ex(P). *) @@ -620,20 +626,21 @@ fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN rotate_tac ~1 i; -fun traceTerm thy t = - let val t' = norm (negOfGoal t) - val stm = string_of thy 8 t' +fun traceTerm ctxt t = + let val thy = Proof_Context.theory_of ctxt + val t' = norm (negOfGoal t) + val stm = string_of ctxt 8 t' in case topType thy t' of NONE => stm (*no type to attach*) - | SOME T => stm ^ "\t:: " ^ Syntax.string_of_typ_global thy T + | SOME T => stm ^ "\t:: " ^ Syntax.string_of_typ ctxt T end; (*Print tracing information at each iteration of prover*) -fun tracing (State {thy, fullTrace, ...}) brs = - let fun printPairs (((G,_)::_,_)::_) = Output.tracing (traceTerm thy G) - | printPairs (([],(H,_)::_)::_) = Output.tracing (traceTerm thy H ^ "\t (Unsafe)") +fun tracing (State {ctxt, fullTrace, ...}) brs = + let fun printPairs (((G,_)::_,_)::_) = Output.tracing (traceTerm ctxt G) + | printPairs (([],(H,_)::_)::_) = Output.tracing (traceTerm ctxt H ^ "\t (Unsafe)") | printPairs _ = () fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) = (fullTrace := brs0 :: !fullTrace; @@ -647,16 +654,16 @@ fun traceMsg s = if !trace then writeln s else (); (*Tracing: variables updated in the last branch operation?*) -fun traceVars (State {thy, ntrail, trail, ...}) ntrl = +fun traceVars (State {ctxt, ntrail, trail, ...}) ntrl = if !trace then (case !ntrail-ntrl of 0 => () | 1 => Output.tracing "\t1 variable UPDATED:" | n => Output.tracing ("\t" ^ string_of_int n ^ " variables UPDATED:"); (*display the instantiations themselves, though no variable names*) - List.app (fn v => Output.tracing (" " ^ string_of thy 4 (the (!v)))) + List.app (fn v => Output.tracing (" " ^ string_of ctxt 4 (the (!v)))) (List.take(!trail, !ntrail-ntrl)); - writeln"") + writeln "") else (); (*Tracing: how many new branches are created?*) @@ -740,7 +747,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 thy (G, {pairs, lits, vars, lim}) = +fun equalSubst ctxt (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) @@ -763,8 +770,8 @@ end val (changed, lits') = List.foldr subLit ([], []) lits val (changed', pairs') = List.foldr subFrame (changed, []) pairs - in if !trace then writeln ("Substituting " ^ traceTerm thy u ^ - " for " ^ traceTerm thy t ^ " in branch" ) + in if !trace then writeln ("Substituting " ^ traceTerm ctxt u ^ + " for " ^ traceTerm ctxt t ^ " in branch" ) else (); {pairs = (changed',[])::pairs', (*affected formulas, and others*) lits = lits', (*unaffected literals*) @@ -800,7 +807,7 @@ (*Were there Skolem terms in the premise? Must NOT chase Vars*) fun hasSkolem (Skolem _) = true | hasSkolem (Abs (_,body)) = hasSkolem body - | hasSkolem (f$t) = hasSkolem f orelse hasSkolem t + | hasSkolem (f$t) = hasSkolem f orelse hasSkolem t | hasSkolem _ = false; (*Attach the right "may duplicate" flag to new formulae: if they contain @@ -913,8 +920,8 @@ bound on unsafe expansions. "start" is CPU time at start, for printing search time *) -fun prove (state, start, ctxt, brs, cont) = - let val State {thy, ntrail, nclosed, ntried, ...} = state; +fun prove (state, start, brs, cont) = + let val State {ctxt, ntrail, nclosed, ntried, ...} = state; val {safe0_netpair, safep_netpair, haz_netpair, ...} = Classical.rep_cs (Classical.claset_of ctxt); val safeList = [safe0_netpair, safep_netpair] @@ -932,7 +939,7 @@ val nbrs = length brs0 val nxtVars = nextVars brs val G = norm G - val rules = netMkRules thy G vars safeList + val rules = netMkRules ctxt G vars safeList (*Make a new branch, decrementing "lim" if instantiations occur*) fun newBr (vars',lim') prems = map (fn prem => @@ -1018,7 +1025,7 @@ else prv (Data.hyp_subst_tac (!trace) :: tacs, brs0::trs, choices, - equalSubst thy + equalSubst ctxt (G, {pairs = (br,haz)::pairs, lits = lits, vars = vars, lim = lim}) :: brs) @@ -1026,7 +1033,7 @@ handle CLOSEF => closeFl ((br,haz)::pairs) handle CLOSEF => deeper rules handle NEWBRANCHES => - (case netMkRules thy G vars hazList of + (case netMkRules ctxt G vars hazList of [] => (*there are no plausible haz rules*) (traceMsg "moving formula to literals"; prv (tacs, brs0::trs, choices, @@ -1060,7 +1067,7 @@ let exception PRV (*backtrack to precisely this recursion!*) val H = norm H val ntrl = !ntrail - val rules = netMkRules thy H vars hazList + val rules = netMkRules ctxt H vars hazList (*new premises of haz rules may NOT be duplicated*) fun newPrem (vars,P,dup,lim') prem = let val Gs' = map (fn Q => (Q,false)) prem @@ -1237,8 +1244,8 @@ (also prints reconstruction time) "lim" is depth limit.*) fun timing_depth_tac start ctxt lim i st0 = - let val thy = Thm.theory_of_thm st0 - val state = initialize thy + let val thy = Proof_Context.theory_of ctxt + val state = initialize ctxt val st = st0 |> rotate_prems (i - 1) |> Conv.gconv_rule Object_Logic.atomize_prems 1 @@ -1260,7 +1267,7 @@ Seq.make(fn()=> cell)) end in - prove (state, start, ctxt, [initBranch (mkGoal concl :: hyps, lim)], cont) + prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont) |> Seq.map (rotate_prems (1 - i)) end handle PROVE => Seq.empty; @@ -1269,15 +1276,12 @@ fun depth_tac ctxt lim i st = timing_depth_tac (Timing.start ()) ctxt lim i st; val (depth_limit, setup_depth_limit) = - Attrib.config_int_global @{binding blast_depth_limit} (K 20); + Attrib.config_int @{binding blast_depth_limit} (K 20); fun blast_tac ctxt i st = - ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit) - (timing_depth_tac (Timing.start ()) ctxt) 0) i - THEN flexflex_tac) st - handle TRANS s => - ((if !trace then warning ("blast: " ^ s) else ()); - Seq.empty); + ((DEEPEN (1, Config.get ctxt depth_limit) (timing_depth_tac (Timing.start ()) ctxt) 0) i + THEN flexflex_tac) st + handle TRANS s => (if !trace then warning ("blast: " ^ s) else (); Seq.empty); @@ -1292,10 +1296,8 @@ fun tryIt ctxt lim s = let - val thy = Proof_Context.theory_of ctxt; - val state as State {fullTrace = ft, ...} = initialize thy; - val res = timeap prove - (state, Timing.start (), ctxt, [initBranch ([readGoal ctxt s], lim)], I); + val state as State {fullTrace = ft, ...} = initialize ctxt; + val res = timeap prove (state, Timing.start (), [initBranch ([readGoal ctxt s], lim)], I); val _ = fullTrace := !ft; in res end;