# HG changeset patch # User wenzelm # Date 1307705571 -7200 # Node ID 46b4f57fb034beddc2a186b4dc7309aa451eba24 # Parent 3e153e7190397362c51c7815508b4c42175c99a0 local gensym based on Name.variant; do not export internals by default; diff -r 3e153e719039 -r 46b4f57fb034 src/Provers/blast.ML --- a/src/Provers/blast.ML Fri Jun 10 12:51:29 2011 +0200 +++ b/src/Provers/blast.ML Fri Jun 10 13:32:51 2011 +0200 @@ -59,22 +59,15 @@ | $ of term*term; val depth_tac: Proof.context -> int -> int -> tactic val depth_limit: int Config.T + val trace: bool Config.T + val stats: bool Config.T val blast_tac: Proof.context -> int -> tactic val setup: theory -> theory (*debugging tools*) type branch - val trace: bool Config.T - val stats: bool Config.T - val fromType: (indexname * term) list Unsynchronized.ref -> Term.typ -> term - val fromTerm: theory -> Term.term -> term - val fromSubgoal: theory -> Term.term -> term - val instVars: term -> (unit -> unit) - val toTerm: int -> term -> Term.term - val readGoal: Proof.context -> string -> term val tryIt: Proof.context -> int -> string -> {fullTrace: branch list list, result: ((int -> tactic) list * branch list list * (int * int * exn) list)} - val normBr: branch -> branch end; functor Blast(Data: BLAST_DATA): BLAST = @@ -111,6 +104,7 @@ datatype state = State of {ctxt: Proof.context, + names: Name.context Unsynchronized.ref, fullTrace: branch list list Unsynchronized.ref, trail: term option Unsynchronized.ref list Unsynchronized.ref, ntrail: int Unsynchronized.ref, @@ -129,6 +123,7 @@ in State {ctxt = ctxt, + names = Unsynchronized.ref (Variable.names_of ctxt), fullTrace = Unsynchronized.ref [], trail = Unsynchronized.ref [], ntrail = Unsynchronized.ref 0, @@ -136,6 +131,8 @@ ntried = Unsynchronized.ref 1} (*number of branches created by splitting (counting from 1)*) end; +fun gensym (State {names, ...}) x = + Unsynchronized.change_result names (Name.variant x); (** Basic syntactic operations **) @@ -446,19 +443,19 @@ else P :: delete_concl Ps | _ => P :: delete_concl Ps); -fun skoPrem vars (Const ("all", _) $ Abs (_, P)) = - skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P)) - | skoPrem vars P = P; +fun skoPrem state vars (Const ("all", _) $ Abs (_, P)) = + skoPrem state vars (subst_bound (Skolem (gensym state "S", vars), P)) + | skoPrem _ _ P = P; fun convertPrem t = delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t); (*Expects elimination rules to have a formula variable as conclusion*) -fun convertRule vars t = +fun convertRule state vars t = let val (P::Ps) = strip_imp_prems t val Var v = strip_imp_concl t in v := SOME (Const ("*False*", [])); - (P, map (convertPrem o skoPrem vars) Ps) + (P, map (convertPrem o skoPrem state vars) Ps) end handle Bind => raise ElimBadConcl; @@ -495,9 +492,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 ctxt vars rl = +fun fromRule (state as State {ctxt, ...}) vars rl = let val thy = Proof_Context.theory_of ctxt - val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule vars + val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule state vars fun tac (upd, dup,rot) i = emtac ctxt upd (if dup then rev_dup_elim rl else rl) i THEN @@ -519,10 +516,10 @@ fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t; -fun convertIntrRule vars t = +fun convertIntrRule state vars t = let val Ps = strip_imp_prems t val P = strip_imp_concl t - in (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps) + in (mkGoal P, map (convertIntrPrem o skoPrem state vars) Ps) end; (*Tableau rule from introduction rule. @@ -530,9 +527,9 @@ Flag "dup" requests duplication of the affected formula. Since haz rules are now delayed, "dup" is always FALSE for introduction rules.*) -fun fromIntrRule ctxt vars rl = +fun fromIntrRule (state as State {ctxt, ...}) vars rl = let val thy = Proof_Context.theory_of ctxt - val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars + val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule state vars fun tac (upd,dup,rot) i = rmtac ctxt upd (if dup then Classical.dup_intr rl else rl) i THEN @@ -554,16 +551,16 @@ | toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d-1) u); -fun netMkRules ctxt P vars (nps: Classical.netpair list) = +fun netMkRules state P vars (nps: Classical.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 ctxt vars o #2) (order_list intrs) end + in map (fromIntrRule state 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 ctxt vars o #2) (order_list elims) end; + in map_filter (fromRule state vars o #2) (order_list elims) end; (*Normalize a branch--for tracing*) @@ -939,7 +936,7 @@ val nbrs = length brs0 val nxtVars = nextVars brs val G = norm G - val rules = netMkRules ctxt G vars safeList + val rules = netMkRules state G vars safeList (*Make a new branch, decrementing "lim" if instantiations occur*) fun newBr (vars',lim') prems = map (fn prem => @@ -1033,7 +1030,7 @@ handle CLOSEF => closeFl ((br,haz)::pairs) handle CLOSEF => deeper rules handle NEWBRANCHES => - (case netMkRules ctxt G vars hazList of + (case netMkRules state G vars hazList of [] => (*there are no plausible haz rules*) (traceMsg trace "moving formula to literals"; prv (tacs, brs0::trs, choices, @@ -1067,7 +1064,7 @@ let exception PRV (*backtrack to precisely this recursion!*) val H = norm H val ntrl = !ntrail - val rules = netMkRules ctxt H vars hazList + val rules = netMkRules state 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 @@ -1191,8 +1188,9 @@ exception TRANS of string; (*Translation of a subgoal: Skolemize all parameters*) -fun fromSubgoal thy t = - let val alistVar = Unsynchronized.ref [] +fun fromSubgoal (state as State {ctxt, ...}) t = + let val thy = Proof_Context.theory_of ctxt + val alistVar = Unsynchronized.ref [] and alistTVar = Unsynchronized.ref [] fun hdvar ((ix,(v,is))::_) = v fun from lev t = @@ -1230,8 +1228,7 @@ fun skoSubgoal i t = if i