turned Unify flags into configuration options (global only);
authorwenzelm
Tue Aug 07 20:19:55 2007 +0200 (2007-08-07)
changeset 241784ff1dc2aa18d
parent 24177 9229d09363c0
child 24179 c89d77d97f84
turned Unify flags into configuration options (global only);
src/HOL/Bali/Basis.thy
src/HOL/IMPP/Natural.thy
src/HOL/Induct/Com.thy
src/HOL/MicroJava/J/JTypeSafe.thy
src/Pure/Isar/attrib.ML
src/Pure/unify.ML
src/Sequents/LK/Hard_Quantifiers.thy
src/Sequents/ROOT.ML
src/Sequents/Sequents.thy
     1.1 --- a/src/HOL/Bali/Basis.thy	Tue Aug 07 20:19:54 2007 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Tue Aug 07 20:19:55 2007 +0200
     1.3 @@ -7,10 +7,8 @@
     1.4  
     1.5  theory Basis imports Main begin
     1.6  
     1.7 -ML {*
     1.8 -Unify.search_bound := 40;
     1.9 -Unify.trace_bound  := 40;
    1.10 -*}
    1.11 +declare [[unify_search_bound = 40, unify_trace_bound = 40]]
    1.12 +
    1.13  
    1.14  section "misc"
    1.15  
     2.1 --- a/src/HOL/IMPP/Natural.thy	Tue Aug 07 20:19:54 2007 +0200
     2.2 +++ b/src/HOL/IMPP/Natural.thy	Tue Aug 07 20:19:55 2007 +0200
     2.3 @@ -108,7 +108,7 @@
     2.4  lemma com_det [rule_format (no_asm)]: "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"
     2.5  apply (erule evalc.induct)
     2.6  apply (erule_tac [8] V = "<?c,s1> -c-> s2" in thin_rl)
     2.7 -(*blast_tac needs Unify.search_bound := 40*)
     2.8 +(*blast needs unify_search_bound = 40*)
     2.9  apply (best elim: evalc_WHILE_case)+
    2.10  done
    2.11  
     3.1 --- a/src/HOL/Induct/Com.thy	Tue Aug 07 20:19:54 2007 +0200
     3.2 +++ b/src/HOL/Induct/Com.thy	Tue Aug 07 20:19:55 2007 +0200
     3.3 @@ -93,10 +93,7 @@
     3.4    "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
     3.5    by (auto simp add: le_fun_def le_bool_def)
     3.6  
     3.7 -ML {*
     3.8 -Unify.trace_bound := 30;
     3.9 -Unify.search_bound := 60;
    3.10 -*}
    3.11 +declare [[unify_trace_bound = 30, unify_search_bound = 60]]
    3.12  
    3.13  text{*Command execution is functional (deterministic) provided evaluation is*}
    3.14  theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
     4.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Aug 07 20:19:54 2007 +0200
     4.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Aug 07 20:19:55 2007 +0200
     4.3 @@ -182,10 +182,8 @@
     4.4  val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
     4.5    (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
     4.6  *}
     4.7 -ML{*
     4.8 -Unify.search_bound := 40;
     4.9 -Unify.trace_bound  := 40
    4.10 -*}
    4.11 +
    4.12 +declare [[unify_search_bound = 40, unify_trace_bound = 40]]
    4.13  
    4.14  
    4.15  theorem eval_evals_exec_type_sound: 
    4.16 @@ -369,10 +367,8 @@
    4.17  apply (simp (no_asm_simp))+ 
    4.18  
    4.19  done
    4.20 -ML{*
    4.21 -Unify.search_bound := 20;
    4.22 -Unify.trace_bound  := 20
    4.23 -*}
    4.24 +
    4.25 +declare [[unify_search_bound = 20, unify_trace_bound = 20]]
    4.26  
    4.27  
    4.28  lemma eval_type_sound: "!!E s s'.  
     5.1 --- a/src/Pure/Isar/attrib.ML	Tue Aug 07 20:19:54 2007 +0200
     5.2 +++ b/src/Pure/Isar/attrib.ML	Tue Aug 07 20:19:55 2007 +0200
     5.3 @@ -349,7 +349,11 @@
     5.4  (* theory setup *)
     5.5  
     5.6  val _ = Context.add_setup
     5.7 - (register_config MetaSimplifier.simp_depth_limit_value #>
     5.8 + (register_config Unify.trace_bound_value #>
     5.9 +  register_config Unify.search_bound_value #>
    5.10 +  register_config Unify.trace_simp_value #>
    5.11 +  register_config Unify.trace_types_value #>
    5.12 +  register_config MetaSimplifier.simp_depth_limit_value #>
    5.13    add_attributes
    5.14     [("tagged", tagged, "tagged theorem"),
    5.15      ("untagged", untagged, "untagged theorem"),
     6.1 --- a/src/Pure/unify.ML	Tue Aug 07 20:19:54 2007 +0200
     6.2 +++ b/src/Pure/unify.ML	Tue Aug 07 20:19:55 2007 +0200
     6.3 @@ -12,10 +12,14 @@
     6.4  
     6.5  signature UNIFY =
     6.6  sig
     6.7 -  val trace_bound: int ref
     6.8 -  val trace_simp: bool ref
     6.9 -  val trace_types: bool ref
    6.10 -  val search_bound: int ref
    6.11 +  val trace_bound_value: Config.value Config.T
    6.12 +  val trace_bound: int Config.T
    6.13 +  val search_bound_value: Config.value Config.T
    6.14 +  val search_bound: int Config.T
    6.15 +  val trace_simp_value: Config.value Config.T
    6.16 +  val trace_simp: bool Config.T
    6.17 +  val trace_types_value: Config.value Config.T
    6.18 +  val trace_types: bool Config.T
    6.19    val unifiers: theory * Envir.env * ((term * term) list) ->
    6.20      (Envir.env * (term * term) list) Seq.seq
    6.21    val smash_unifiers: theory -> (term * term) list -> Envir.env -> Envir.env Seq.seq
    6.22 @@ -28,10 +32,22 @@
    6.23  
    6.24  (*Unification options*)
    6.25  
    6.26 -val trace_bound = ref 25  (*tracing starts above this depth, 0 for full*)
    6.27 -and search_bound = ref 30 (*unification quits above this depth*)
    6.28 -and trace_simp = ref false  (*print dpairs before calling SIMPL*)
    6.29 -and trace_types = ref false (*announce potential incompleteness of type unification*)
    6.30 +(*tracing starts above this depth, 0 for full*)
    6.31 +val trace_bound_value = Config.declare true "unify_trace_bound" (Config.Int 25);
    6.32 +val trace_bound = Config.int trace_bound_value;
    6.33 +
    6.34 +(*unification quits above this depth*)
    6.35 +val search_bound_value = Config.declare true "unify_search_bound" (Config.Int 30);
    6.36 +val search_bound = Config.int search_bound_value;
    6.37 +
    6.38 +(*print dpairs before calling SIMPL*)
    6.39 +val trace_simp_value = Config.declare true "unify_trace_simp" (Config.Bool false);
    6.40 +val trace_simp = Config.bool trace_simp_value;
    6.41 +
    6.42 +(*announce potential incompleteness of type unification*)
    6.43 +val trace_types_value = Config.declare true "unify_trace_types" (Config.Bool false);
    6.44 +val trace_types = Config.bool trace_types_value;
    6.45 +
    6.46  
    6.47  type binderlist = (string*typ) list;
    6.48  
    6.49 @@ -318,8 +334,10 @@
    6.50    NB "vname" is only used in the call to make_args!!   *)
    6.51  fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs))
    6.52    : (term * (Envir.env * dpair list))Seq.seq =
    6.53 -let (*Produce copies of uarg and cons them in front of uargs*)
    6.54 -    fun copycons uarg (uargs, (env, dpairs)) =
    6.55 +let
    6.56 +  val trace_tps = Config.get_thy thy trace_types;
    6.57 +  (*Produce copies of uarg and cons them in front of uargs*)
    6.58 +  fun copycons uarg (uargs, (env, dpairs)) =
    6.59    Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
    6.60        (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),
    6.61       (env, dpairs)));
    6.62 @@ -332,7 +350,7 @@
    6.63      (*attempt projection on argument with given typ*)
    6.64      val Ts = map (curry (fastype env) rbinder) targs;
    6.65      fun projenv (head, (Us,bary), targ, tail) =
    6.66 -  let val env = if !trace_types then test_unify_types thy (base,bary,env)
    6.67 +  let val env = if trace_tps then test_unify_types thy (base,bary,env)
    6.68            else unify_types thy (base,bary,env)
    6.69    in Seq.make (fn () =>
    6.70        let val (env',args) = make_args vname (Ts,env,Us);
    6.71 @@ -551,26 +569,30 @@
    6.72    SIMPL may raise exception CANTUNIFY. *)
    6.73  fun hounifiers (thy,env, tus : (term*term)list)
    6.74    : (Envir.env * (term*term)list)Seq.seq =
    6.75 -  let fun add_unify tdepth ((env,dpairs), reseq) =
    6.76 +  let
    6.77 +    val trace_bnd = Config.get_thy thy trace_bound;
    6.78 +    val search_bnd = Config.get_thy thy search_bound;
    6.79 +    val trace_smp = Config.get_thy thy trace_simp;
    6.80 +    fun add_unify tdepth ((env,dpairs), reseq) =
    6.81      Seq.make (fn()=>
    6.82      let val (env',flexflex,flexrigid) =
    6.83 -         (if tdepth> !trace_bound andalso !trace_simp
    6.84 +         (if tdepth> trace_bnd andalso trace_smp
    6.85      then print_dpairs thy "Enter SIMPL" (env,dpairs)  else ();
    6.86      SIMPL thy (env,dpairs))
    6.87      in case flexrigid of
    6.88          [] => SOME (List.foldr (add_ffpair thy) (env',[]) flexflex, reseq)
    6.89        | dp::frigid' =>
    6.90 -    if tdepth > !search_bound then
    6.91 +    if tdepth > search_bnd then
    6.92          (warning "Unification bound exceeded"; Seq.pull reseq)
    6.93      else
    6.94 -    (if tdepth > !trace_bound then
    6.95 +    (if tdepth > trace_bnd then
    6.96          print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
    6.97       else ();
    6.98       Seq.pull (Seq.it_right (add_unify (tdepth+1))
    6.99           (MATCH thy (env',dp, frigid'@flexflex), reseq)))
   6.100      end
   6.101      handle CANTUNIFY =>
   6.102 -      (if tdepth > !trace_bound then tracing"Failure node" else ();
   6.103 +      (if tdepth > trace_bnd then tracing"Failure node" else ();
   6.104         Seq.pull reseq));
   6.105       val dps = map (fn(t,u)=> ([],t,u)) tus
   6.106    in add_unify 1 ((env, dps), Seq.empty) end;
     7.1 --- a/src/Sequents/LK/Hard_Quantifiers.thy	Tue Aug 07 20:19:54 2007 +0200
     7.2 +++ b/src/Sequents/LK/Hard_Quantifiers.thy	Tue Aug 07 20:19:55 2007 +0200
     7.3 @@ -249,7 +249,7 @@
     7.4  text "Problem 59"
     7.5  (*Unification works poorly here -- the abstraction %sobj prevents efficient
     7.6    operation of the occurs check*)
     7.7 -ML {* Unify.trace_bound := !Unify.search_bound - 1 *}
     7.8 +
     7.9  lemma "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
    7.10    by best_dup
    7.11  
     8.1 --- a/src/Sequents/ROOT.ML	Tue Aug 07 20:19:54 2007 +0200
     8.2 +++ b/src/Sequents/ROOT.ML	Tue Aug 07 20:19:55 2007 +0200
     8.3 @@ -6,7 +6,4 @@
     8.4  Classical Sequent Calculus based on Pure Isabelle. 
     8.5  *)
     8.6  
     8.7 -Unify.trace_bound:= 20;
     8.8 -Unify.search_bound := 40;
     8.9 -
    8.10  use_thys ["LK", "ILL", "ILL_predlog", "Washing", "Modal0", "T", "S4", "S43"];
     9.1 --- a/src/Sequents/Sequents.thy	Tue Aug 07 20:19:54 2007 +0200
     9.2 +++ b/src/Sequents/Sequents.thy	Tue Aug 07 20:19:55 2007 +0200
     9.3 @@ -11,6 +11,8 @@
     9.4  uses ("prover.ML")
     9.5  begin
     9.6  
     9.7 +declare [[unify_trace_bound = 20, unify_search_bound = 40]]
     9.8 +
     9.9  global
    9.10  
    9.11  typedecl o