replaced depth_limit ref by blast_depth_limit configuration option;
authorwenzelm
Tue Jul 31 21:19:21 2007 +0200 (2007-07-31)
changeset 240996534fd4c5d46
parent 24098 f1eb34ae33af
child 24100 a2f19514e156
replaced depth_limit ref by blast_depth_limit configuration option;
tuned method setup;
src/Provers/blast.ML
     1.1 --- a/src/Provers/blast.ML	Tue Jul 31 21:19:20 2007 +0200
     1.2 +++ b/src/Provers/blast.ML	Tue Jul 31 21:19:21 2007 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4      | $  of term*term;
     1.5    type branch
     1.6    val depth_tac         : claset -> int -> int -> tactic
     1.7 -  val depth_limit : int ref
     1.8 +  val depth_limit: int ConfigOption.T
     1.9    val blast_tac         : claset -> int -> tactic
    1.10    val Blast_tac         : int -> tactic
    1.11    val setup             : theory -> theory
    1.12 @@ -1274,10 +1274,11 @@
    1.13  (*Public version with fixed depth*)
    1.14  fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
    1.15  
    1.16 -val depth_limit = ref 20;
    1.17 +val (depth_limit, setup_depth_limit) = ConfigOption.global_int "blast_depth_limit" 20;
    1.18  
    1.19  fun blast_tac cs i st =
    1.20 -    ((DEEPEN (1, !depth_limit) (timing_depth_tac (start_timing ()) cs) 0) i
    1.21 +    ((DEEPEN (1, ConfigOption.get_thy (Thm.theory_of_thm st) depth_limit)
    1.22 +        (timing_depth_tac (start_timing ()) cs) 0) i
    1.23       THEN flexflex_tac) st
    1.24      handle TRANS s =>
    1.25        ((if !trace then warning ("blast: " ^ s) else ());
    1.26 @@ -1305,15 +1306,13 @@
    1.27  
    1.28  (** method setup **)
    1.29  
    1.30 -fun blast_args m =
    1.31 -  Method.bang_sectioned_args'
    1.32 -      Data.cla_modifiers (Scan.lift (Scan.option Args.nat)) m;
    1.33 -
    1.34 -fun blast_meth NONE = Data.cla_meth' blast_tac
    1.35 -  | blast_meth (SOME lim) = Data.cla_meth' (fn cs => depth_tac cs lim);
    1.36 +val blast_method =
    1.37 +  Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option Args.nat))
    1.38 +    (fn NONE => Data.cla_meth' blast_tac
    1.39 +      | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim));
    1.40  
    1.41  val setup =
    1.42 -  Method.add_methods [("blast", blast_args blast_meth, "tableau prover")];
    1.43 -
    1.44 +  setup_depth_limit #>
    1.45 +  Method.add_methods [("blast", blast_method, "tableau prover")];
    1.46  
    1.47  end;