--- a/src/Provers/blast.ML Fri Jun 10 12:01:15 2011 +0200
+++ b/src/Provers/blast.ML Fri Jun 10 15:03:29 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 stats: bool Config.T
- val trace: 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 =
@@ -82,9 +75,12 @@
structure Classical = Data.Classical;
-val trace = Config.bool (Config.declare "Blast.trace" (K (Config.Bool false)));
-val stats = Config.bool (Config.declare "Blast.stats" (K (Config.Bool false)));
-(*for runtime and search statistics*)
+(* options *)
+
+val (depth_limit, setup_depth_limit) = Attrib.config_int @{binding blast_depth_limit} (K 20);
+val (trace, setup_trace) = Attrib.config_bool @{binding blast_trace} (K false);
+val (stats, setup_stats) = Attrib.config_bool @{binding blast_stats} (K false);
+
datatype term =
Const of string * term list (*typargs constant--as a terms!*)
@@ -108,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,
@@ -126,6 +123,7 @@
in
State
{ctxt = ctxt,
+ names = Unsynchronized.ref (Variable.names_of ctxt),
fullTrace = Unsynchronized.ref [],
trail = Unsynchronized.ref [],
ntrail = Unsynchronized.ref 0,
@@ -133,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 **)
@@ -443,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;
@@ -492,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
@@ -516,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.
@@ -527,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
@@ -551,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*)
@@ -936,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 =>
@@ -1030,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,
@@ -1064,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
@@ -1188,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 =
@@ -1227,8 +1228,7 @@
fun skoSubgoal i t =
if i<npars then
skoSubgoal (i+1)
- (subst_bound (Skolem (gensym "T_", getVars (!alistVar) i),
- t))
+ (subst_bound (Skolem (gensym state "T", getVars (!alistVar) i), t))
else t
in skoSubgoal 0 (from 0 (discard_foralls t)) end;
@@ -1238,11 +1238,10 @@
"start" is CPU time at start, for printing SEARCH time (also prints reconstruction time)
"lim" is depth limit.*)
fun raw_blast start ctxt lim st =
- let val thy = Proof_Context.theory_of ctxt
- val state = initialize ctxt
+ let val state = initialize ctxt
val trace = Config.get ctxt trace;
val stats = Config.get ctxt stats;
- val skoprem = fromSubgoal thy (#1 (Logic.dest_implies (Thm.prop_of st)))
+ val skoprem = fromSubgoal state (#1 (Logic.dest_implies (Thm.prop_of st)))
val hyps = strip_imp_prems skoprem
and concl = strip_imp_concl skoprem
fun cont (tacs,_,choices) =
@@ -1251,8 +1250,6 @@
case Seq.pull(EVERY' (rev tacs) 1 st) of
NONE => (writeln ("PROOF FAILED for depth " ^
string_of_int lim);
- if trace then error "************************\n"
- else ();
backtrack trace choices)
| cell => (if (trace orelse stats)
then writeln (Timing.message (Timing.result start) ^ " for reconstruction")
@@ -1261,6 +1258,7 @@
end
in
prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont)
+ |> Seq.maps Thm.flexflex_rule
end
handle PROVE => Seq.empty
| TRANS s => (if Config.get ctxt trace then warning ("Blast: " ^ s) else (); Seq.empty);
@@ -1270,10 +1268,6 @@
(Object_Logic.atomize_prems_tac 1 THEN
raw_blast (Timing.start ()) ctxt lim) i st;
-
-val (depth_limit, setup_depth_limit) =
- Attrib.config_int @{binding blast_depth_limit} (K 20);
-
fun blast_tac ctxt i st =
let
val start = Timing.start ();
@@ -1281,8 +1275,7 @@
in
SELECT_GOAL
(Object_Logic.atomize_prems_tac 1 THEN
- DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1 THEN
- flexflex_tac) i st
+ DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1) i st
end;
@@ -1305,6 +1298,8 @@
val setup =
setup_depth_limit #>
+ setup_trace #>
+ setup_stats #>
Method.setup @{binding blast}
(Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
(fn NONE => SIMPLE_METHOD' o blast_tac