# HG changeset patch
# User wenzelm
# Date 1186049187 -7200
# Node ID 4399175e3014505aacfa06eedd4b03d70280773f
# Parent  a0fc58900606f202dbdf4fa4460f7815521d8462
turned simp_depth_limit into configuration option;

diff -r a0fc58900606 -r 4399175e3014 src/HOL/Matrix/SparseMatrix.thy
--- 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"
diff -r a0fc58900606 -r 4399175e3014 src/HOL/Real/Float.thy
--- 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 -
diff -r a0fc58900606 -r 4399175e3014 src/HOL/ZF/HOLZF.thy
--- 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"
diff -r a0fc58900606 -r 4399175e3014 src/Pure/meta_simplifier.ML
--- 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
diff -r a0fc58900606 -r 4399175e3014 src/Pure/simplifier.ML
--- 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)));