--- a/src/HOL/Matrix/SparseMatrix.thy Wed Aug 01 21:10:36 2007 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy Thu Aug 02 12:06:27 2007 +0200
@@ -600,7 +600,7 @@
disj_matrices :: "('a::zero) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
"disj_matrices A B == (! j i. (Rep_matrix A j i \<noteq> 0) \<longrightarrow> (Rep_matrix B j i = 0)) & (! j i. (Rep_matrix B j i \<noteq> 0) \<longrightarrow> (Rep_matrix A j i = 0))"
-ML {* simp_depth_limit := 6 *}
+declare [[simp_depth_limit = 6]]
lemma disj_matrices_contr1: "disj_matrices A B \<Longrightarrow> Rep_matrix A j i \<noteq> 0 \<Longrightarrow> Rep_matrix B j i = 0"
by (simp add: disj_matrices_def)
@@ -777,7 +777,7 @@
apply (simp add: sorted_spvec_cons1 le_spvec_iff_sparse_row_le)
done
-ML {* simp_depth_limit := 999 *}
+declare [[simp_depth_limit = 999]]
consts
abs_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat"
--- a/src/HOL/Real/Float.thy Wed Aug 01 21:10:36 2007 +0200
+++ b/src/HOL/Real/Float.thy Thu Aug 02 12:06:27 2007 +0200
@@ -282,11 +282,11 @@
apply (auto)
done
-ML {* simp_depth_limit := 2 *}
+declare [[simp_depth_limit = 2]]
recdef norm_float "measure (% (a,b). nat (abs a))"
"norm_float (a,b) = (if (a \<noteq> 0) & (even a) then norm_float (a div 2, b+1) else (if a=0 then (0,0) else (a,b)))"
(hints simp: even_def terminating_norm_float)
-ML {* simp_depth_limit := 1000 *}
+declare [[simp_depth_limit = 100]]
lemma norm_float: "float x = float (norm_float x)"
proof -
--- a/src/HOL/ZF/HOLZF.thy Wed Aug 01 21:10:36 2007 +0200
+++ b/src/HOL/ZF/HOLZF.thy Thu Aug 02 12:06:27 2007 +0200
@@ -273,10 +273,9 @@
apply (auto simp add: PFun_def Sep)
done
-ML {* simp_depth_limit := 2 *}
lemma Fun_total: "\<lbrakk>Elem F (Fun U V); Elem a U\<rbrakk> \<Longrightarrow> \<exists>x. Elem (Opair a x) F"
+ using [[simp_depth_limit = 2]]
by (auto simp add: Fun_def Sep Domain)
-ML {* simp_depth_limit := 1000 *}
lemma unique_fun_value: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> ?! y. Elem (Opair x y) f"
--- a/src/Pure/meta_simplifier.ML Wed Aug 01 21:10:36 2007 +0200
+++ b/src/Pure/meta_simplifier.ML Thu Aug 02 12:06:27 2007 +0200
@@ -14,7 +14,6 @@
sig
val debug_simp: bool ref
val trace_simp: bool ref
- val simp_depth_limit: int ref
val trace_simp_depth_limit: int ref
type rrule
val eq_rrule: rrule * rrule -> bool
@@ -94,6 +93,8 @@
include BASIC_META_SIMPLIFIER
exception SIMPLIFIER of string * thm
val solver: simpset -> solver -> int -> tactic
+ val simp_depth_limit_value: Config.value Config.T
+ val simp_depth_limit: int Config.T
val clear_ss: simpset -> simpset
val simproc_i: theory -> string -> term list
-> (theory -> simpset -> term -> thm option) -> simproc
@@ -254,7 +255,9 @@
(* simp depth *)
-val simp_depth_limit = ref 100;
+val simp_depth_limit_value = Config.declare false "simp_depth_limit" (Config.Int 100);
+val simp_depth_limit = Config.int simp_depth_limit_value;
+
val trace_simp_depth_limit = ref 1;
fun trace_depth (Simpset ({depth = (depth, exceeded), ...}, _)) msg =
@@ -884,6 +887,7 @@
fun rewritec (prover, thyt, maxt) ss t =
let
+ val ctxt = the_context ss;
val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
val eta_thm = Thm.eta_conversion t;
val eta_t' = Thm.rhs_of eta_thm;
@@ -914,7 +918,7 @@
in SOME (thm'', uncond_skel (congs, lr)) end)
else
(trace_thm (fn () => "Trying to rewrite:") ss thm';
- if simp_depth ss > ! simp_depth_limit
+ if simp_depth ss > Config.get ctxt simp_depth_limit
then let val s = "simp_depth_limit exceeded - giving up"
in trace false (fn () => s) ss; warning s; NONE end
else
--- a/src/Pure/simplifier.ML Wed Aug 01 21:10:36 2007 +0200
+++ b/src/Pure/simplifier.ML Thu Aug 02 12:06:27 2007 +0200
@@ -346,7 +346,7 @@
>> (Library.apply o map Morphism.form))));
end;
-
+
(* conversions *)
@@ -389,11 +389,6 @@
Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
Scan.succeed asm_full_simp_tac);
-fun simp_flags x = (Scan.repeat
- (Args.parens (Args.$$$ "depth_limit" -- Args.colon |-- Args.nat)
- >> setmp MetaSimplifier.simp_depth_limit)
- >> (curry (Library.foldl op o) I o rev)) x;
-
val cong_modifiers =
[Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier),
Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add),
@@ -415,16 +410,16 @@
@ cong_modifiers;
fun simp_args more_mods =
- Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options -- Scan.lift simp_flags)
+ Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options)
(more_mods @ simp_modifiers');
-fun simp_method ((prems, tac), FLAGS) ctxt = Method.METHOD (fn facts =>
+fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
ALLGOALS (Method.insert_tac (prems @ facts)) THEN
- (FLAGS o CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
+ (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
-fun simp_method' ((prems, tac), FLAGS) ctxt = Method.METHOD (fn facts =>
+fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
HEADGOAL (Method.insert_tac (prems @ facts) THEN'
- ((FLAGS o CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
+ ((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));