src/Provers/blast.ML
changeset 58826 2ed2eaabe3df
parent 56245 84fc7dfa3cd4
child 58838 59203adfc33f
equal deleted inserted replaced
58825:2065f49da190 58826:2ed2eaabe3df
    60   val depth_tac: Proof.context -> int -> int -> tactic
    60   val depth_tac: Proof.context -> int -> int -> tactic
    61   val depth_limit: int Config.T
    61   val depth_limit: int Config.T
    62   val trace: bool Config.T
    62   val trace: bool Config.T
    63   val stats: bool Config.T
    63   val stats: bool Config.T
    64   val blast_tac: Proof.context -> int -> tactic
    64   val blast_tac: Proof.context -> int -> tactic
    65   val setup: theory -> theory
       
    66   (*debugging tools*)
    65   (*debugging tools*)
    67   type branch
    66   type branch
    68   val tryIt: Proof.context -> int -> string ->
    67   val tryIt: Proof.context -> int -> string ->
    69     {fullTrace: branch list list,
    68     {fullTrace: branch list list,
    70       result: ((int -> tactic) list * branch list list * (int * int * exn) list)}
    69       result: ((int -> tactic) list * branch list list * (int * int * exn) list)}
    75 
    74 
    76 structure Classical = Data.Classical;
    75 structure Classical = Data.Classical;
    77 
    76 
    78 (* options *)
    77 (* options *)
    79 
    78 
    80 val (depth_limit, setup_depth_limit) = Attrib.config_int @{binding blast_depth_limit} (K 20);
    79 val depth_limit = Attrib.setup_config_int @{binding blast_depth_limit} (K 20);
    81 val (trace, _) = Attrib.config_bool @{binding blast_trace} (K false);
    80 val (trace, _) = Attrib.config_bool @{binding blast_trace} (K false);
    82 val (stats, _) = Attrib.config_bool @{binding blast_stats} (K false);
    81 val (stats, _) = Attrib.config_bool @{binding blast_stats} (K false);
    83 
    82 
    84 
    83 
    85 datatype term =
    84 datatype term =
  1292     val state as State {fullTrace, ...} = initialize ctxt;
  1291     val state as State {fullTrace, ...} = initialize ctxt;
  1293     val res = timeap prove (state, Timing.start (), [initBranch ([readGoal ctxt s], lim)], I);
  1292     val res = timeap prove (state, Timing.start (), [initBranch ([readGoal ctxt s], lim)], I);
  1294   in {fullTrace = !fullTrace, result = res} end;
  1293   in {fullTrace = !fullTrace, result = res} end;
  1295 
  1294 
  1296 
  1295 
       
  1296 
  1297 (** method setup **)
  1297 (** method setup **)
  1298 
  1298 
  1299 val setup =
  1299 val _ =
  1300   setup_depth_limit #>
  1300   Theory.setup
  1301   Method.setup @{binding blast}
  1301     (Method.setup @{binding blast}
  1302     (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
  1302       (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
  1303       (fn NONE => SIMPLE_METHOD' o blast_tac
  1303         (fn NONE => SIMPLE_METHOD' o blast_tac
  1304         | SOME lim => (fn ctxt => SIMPLE_METHOD' (depth_tac ctxt lim))))
  1304           | SOME lim => (fn ctxt => SIMPLE_METHOD' (depth_tac ctxt lim))))
  1305     "classical tableau prover";
  1305       "classical tableau prover");
  1306 
  1306 
  1307 end;
  1307 end;