--- a/src/HOL/Bali/Basis.thy Tue Aug 07 20:19:54 2007 +0200
+++ b/src/HOL/Bali/Basis.thy Tue Aug 07 20:19:55 2007 +0200
@@ -7,10 +7,8 @@
theory Basis imports Main begin
-ML {*
-Unify.search_bound := 40;
-Unify.trace_bound := 40;
-*}
+declare [[unify_search_bound = 40, unify_trace_bound = 40]]
+
section "misc"
--- a/src/HOL/IMPP/Natural.thy Tue Aug 07 20:19:54 2007 +0200
+++ b/src/HOL/IMPP/Natural.thy Tue Aug 07 20:19:55 2007 +0200
@@ -108,7 +108,7 @@
lemma com_det [rule_format (no_asm)]: "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"
apply (erule evalc.induct)
apply (erule_tac [8] V = "<?c,s1> -c-> s2" in thin_rl)
-(*blast_tac needs Unify.search_bound := 40*)
+(*blast needs unify_search_bound = 40*)
apply (best elim: evalc_WHILE_case)+
done
--- a/src/HOL/Induct/Com.thy Tue Aug 07 20:19:54 2007 +0200
+++ b/src/HOL/Induct/Com.thy Tue Aug 07 20:19:55 2007 +0200
@@ -93,10 +93,7 @@
"((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
by (auto simp add: le_fun_def le_bool_def)
-ML {*
-Unify.trace_bound := 30;
-Unify.search_bound := 60;
-*}
+declare [[unify_trace_bound = 30, unify_search_bound = 60]]
text{*Command execution is functional (deterministic) provided evaluation is*}
theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Tue Aug 07 20:19:54 2007 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Tue Aug 07 20:19:55 2007 +0200
@@ -182,10 +182,8 @@
val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
*}
-ML{*
-Unify.search_bound := 40;
-Unify.trace_bound := 40
-*}
+
+declare [[unify_search_bound = 40, unify_trace_bound = 40]]
theorem eval_evals_exec_type_sound:
@@ -369,10 +367,8 @@
apply (simp (no_asm_simp))+
done
-ML{*
-Unify.search_bound := 20;
-Unify.trace_bound := 20
-*}
+
+declare [[unify_search_bound = 20, unify_trace_bound = 20]]
lemma eval_type_sound: "!!E s s'.
--- a/src/Pure/Isar/attrib.ML Tue Aug 07 20:19:54 2007 +0200
+++ b/src/Pure/Isar/attrib.ML Tue Aug 07 20:19:55 2007 +0200
@@ -349,7 +349,11 @@
(* theory setup *)
val _ = Context.add_setup
- (register_config MetaSimplifier.simp_depth_limit_value #>
+ (register_config Unify.trace_bound_value #>
+ register_config Unify.search_bound_value #>
+ register_config Unify.trace_simp_value #>
+ register_config Unify.trace_types_value #>
+ register_config MetaSimplifier.simp_depth_limit_value #>
add_attributes
[("tagged", tagged, "tagged theorem"),
("untagged", untagged, "untagged theorem"),
--- a/src/Pure/unify.ML Tue Aug 07 20:19:54 2007 +0200
+++ b/src/Pure/unify.ML Tue Aug 07 20:19:55 2007 +0200
@@ -12,10 +12,14 @@
signature UNIFY =
sig
- val trace_bound: int ref
- val trace_simp: bool ref
- val trace_types: bool ref
- val search_bound: int ref
+ val trace_bound_value: Config.value Config.T
+ val trace_bound: int Config.T
+ val search_bound_value: Config.value Config.T
+ val search_bound: int Config.T
+ val trace_simp_value: Config.value Config.T
+ val trace_simp: bool Config.T
+ val trace_types_value: Config.value Config.T
+ val trace_types: bool Config.T
val unifiers: theory * Envir.env * ((term * term) list) ->
(Envir.env * (term * term) list) Seq.seq
val smash_unifiers: theory -> (term * term) list -> Envir.env -> Envir.env Seq.seq
@@ -28,10 +32,22 @@
(*Unification options*)
-val trace_bound = ref 25 (*tracing starts above this depth, 0 for full*)
-and search_bound = ref 30 (*unification quits above this depth*)
-and trace_simp = ref false (*print dpairs before calling SIMPL*)
-and trace_types = ref false (*announce potential incompleteness of type unification*)
+(*tracing starts above this depth, 0 for full*)
+val trace_bound_value = Config.declare true "unify_trace_bound" (Config.Int 25);
+val trace_bound = Config.int trace_bound_value;
+
+(*unification quits above this depth*)
+val search_bound_value = Config.declare true "unify_search_bound" (Config.Int 30);
+val search_bound = Config.int search_bound_value;
+
+(*print dpairs before calling SIMPL*)
+val trace_simp_value = Config.declare true "unify_trace_simp" (Config.Bool false);
+val trace_simp = Config.bool trace_simp_value;
+
+(*announce potential incompleteness of type unification*)
+val trace_types_value = Config.declare true "unify_trace_types" (Config.Bool false);
+val trace_types = Config.bool trace_types_value;
+
type binderlist = (string*typ) list;
@@ -318,8 +334,10 @@
NB "vname" is only used in the call to make_args!! *)
fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs))
: (term * (Envir.env * dpair list))Seq.seq =
-let (*Produce copies of uarg and cons them in front of uargs*)
- fun copycons uarg (uargs, (env, dpairs)) =
+let
+ val trace_tps = Config.get_thy thy trace_types;
+ (*Produce copies of uarg and cons them in front of uargs*)
+ fun copycons uarg (uargs, (env, dpairs)) =
Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
(mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),
(env, dpairs)));
@@ -332,7 +350,7 @@
(*attempt projection on argument with given typ*)
val Ts = map (curry (fastype env) rbinder) targs;
fun projenv (head, (Us,bary), targ, tail) =
- let val env = if !trace_types then test_unify_types thy (base,bary,env)
+ let val env = if trace_tps then test_unify_types thy (base,bary,env)
else unify_types thy (base,bary,env)
in Seq.make (fn () =>
let val (env',args) = make_args vname (Ts,env,Us);
@@ -551,26 +569,30 @@
SIMPL may raise exception CANTUNIFY. *)
fun hounifiers (thy,env, tus : (term*term)list)
: (Envir.env * (term*term)list)Seq.seq =
- let fun add_unify tdepth ((env,dpairs), reseq) =
+ let
+ val trace_bnd = Config.get_thy thy trace_bound;
+ val search_bnd = Config.get_thy thy search_bound;
+ val trace_smp = Config.get_thy thy trace_simp;
+ fun add_unify tdepth ((env,dpairs), reseq) =
Seq.make (fn()=>
let val (env',flexflex,flexrigid) =
- (if tdepth> !trace_bound andalso !trace_simp
+ (if tdepth> trace_bnd andalso trace_smp
then print_dpairs thy "Enter SIMPL" (env,dpairs) else ();
SIMPL thy (env,dpairs))
in case flexrigid of
[] => SOME (List.foldr (add_ffpair thy) (env',[]) flexflex, reseq)
| dp::frigid' =>
- if tdepth > !search_bound then
+ if tdepth > search_bnd then
(warning "Unification bound exceeded"; Seq.pull reseq)
else
- (if tdepth > !trace_bound then
+ (if tdepth > trace_bnd then
print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
else ();
Seq.pull (Seq.it_right (add_unify (tdepth+1))
(MATCH thy (env',dp, frigid'@flexflex), reseq)))
end
handle CANTUNIFY =>
- (if tdepth > !trace_bound then tracing"Failure node" else ();
+ (if tdepth > trace_bnd then tracing"Failure node" else ();
Seq.pull reseq));
val dps = map (fn(t,u)=> ([],t,u)) tus
in add_unify 1 ((env, dps), Seq.empty) end;
--- a/src/Sequents/LK/Hard_Quantifiers.thy Tue Aug 07 20:19:54 2007 +0200
+++ b/src/Sequents/LK/Hard_Quantifiers.thy Tue Aug 07 20:19:55 2007 +0200
@@ -249,7 +249,7 @@
text "Problem 59"
(*Unification works poorly here -- the abstraction %sobj prevents efficient
operation of the occurs check*)
-ML {* Unify.trace_bound := !Unify.search_bound - 1 *}
+
lemma "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
by best_dup
--- a/src/Sequents/ROOT.ML Tue Aug 07 20:19:54 2007 +0200
+++ b/src/Sequents/ROOT.ML Tue Aug 07 20:19:55 2007 +0200
@@ -6,7 +6,4 @@
Classical Sequent Calculus based on Pure Isabelle.
*)
-Unify.trace_bound:= 20;
-Unify.search_bound := 40;
-
use_thys ["LK", "ILL", "ILL_predlog", "Washing", "Modal0", "T", "S4", "S43"];
--- a/src/Sequents/Sequents.thy Tue Aug 07 20:19:54 2007 +0200
+++ b/src/Sequents/Sequents.thy Tue Aug 07 20:19:55 2007 +0200
@@ -11,6 +11,8 @@
uses ("prover.ML")
begin
+declare [[unify_trace_bound = 20, unify_search_bound = 40]]
+
global
typedecl o