src/Provers/blast.ML

   val depth_limit: int 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 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

 functor Blast(Data: BLAST_DATA): BLAST =
 struct
 
 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!*)
   | Skolem of string * term option Unsynchronized.ref list
   | Free   of string

           let val start = Timing.start ()
           in
           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")
                        else ();
                        Seq.make(fn()=> cell))

   SELECT_GOAL
     (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 ();
     val lim = Config.get ctxt depth_limit;
   in

 
 (** method setup **)
 
 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
         | SOME lim => (fn ctxt => SIMPLE_METHOD' (depth_tac ctxt lim))))
     "classical tableau prover";