turned simp_depth_limit into configuration option;
authorwenzelm
Thu Aug 02 12:06:27 2007 +0200 (2007-08-02)
changeset 241244399175e3014
parent 24123 a0fc58900606
child 24125 454a0c895735
turned simp_depth_limit into configuration option;
src/HOL/Matrix/SparseMatrix.thy
src/HOL/Real/Float.thy
src/HOL/ZF/HOLZF.thy
src/Pure/meta_simplifier.ML
src/Pure/simplifier.ML
     1.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Wed Aug 01 21:10:36 2007 +0200
     1.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Thu Aug 02 12:06:27 2007 +0200
     1.3 @@ -600,7 +600,7 @@
     1.4    disj_matrices :: "('a::zero) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
     1.5    "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))"  
     1.6  
     1.7 -ML {* simp_depth_limit := 6 *}
     1.8 +declare [[simp_depth_limit = 6]]
     1.9  
    1.10  lemma disj_matrices_contr1: "disj_matrices A B \<Longrightarrow> Rep_matrix A j i \<noteq> 0 \<Longrightarrow> Rep_matrix B j i = 0"
    1.11     by (simp add: disj_matrices_def)
    1.12 @@ -777,7 +777,7 @@
    1.13    apply (simp add: sorted_spvec_cons1 le_spvec_iff_sparse_row_le)
    1.14    done
    1.15  
    1.16 -ML {* simp_depth_limit := 999 *}
    1.17 +declare [[simp_depth_limit = 999]]
    1.18  
    1.19  consts 
    1.20     abs_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat"
     2.1 --- a/src/HOL/Real/Float.thy	Wed Aug 01 21:10:36 2007 +0200
     2.2 +++ b/src/HOL/Real/Float.thy	Thu Aug 02 12:06:27 2007 +0200
     2.3 @@ -282,11 +282,11 @@
     2.4  apply (auto)
     2.5  done
     2.6  
     2.7 -ML {* simp_depth_limit := 2 *}
     2.8 +declare [[simp_depth_limit = 2]]
     2.9  recdef norm_float "measure (% (a,b). nat (abs a))"
    2.10    "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)))"
    2.11  (hints simp: even_def terminating_norm_float)
    2.12 -ML {* simp_depth_limit := 1000 *}
    2.13 +declare [[simp_depth_limit = 100]]
    2.14  
    2.15  lemma norm_float: "float x = float (norm_float x)"
    2.16  proof -
     3.1 --- a/src/HOL/ZF/HOLZF.thy	Wed Aug 01 21:10:36 2007 +0200
     3.2 +++ b/src/HOL/ZF/HOLZF.thy	Thu Aug 02 12:06:27 2007 +0200
     3.3 @@ -273,10 +273,9 @@
     3.4    apply (auto simp add: PFun_def Sep)
     3.5    done
     3.6  
     3.7 -ML {* simp_depth_limit := 2 *}
     3.8  lemma Fun_total: "\<lbrakk>Elem F (Fun U V); Elem a U\<rbrakk> \<Longrightarrow> \<exists>x. Elem (Opair a x) F"
     3.9 +  using [[simp_depth_limit = 2]]
    3.10    by (auto simp add: Fun_def Sep Domain)
    3.11 -ML {* simp_depth_limit := 1000 *}
    3.12  
    3.13  
    3.14  lemma unique_fun_value: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> ?! y. Elem (Opair x y) f"
     4.1 --- a/src/Pure/meta_simplifier.ML	Wed Aug 01 21:10:36 2007 +0200
     4.2 +++ b/src/Pure/meta_simplifier.ML	Thu Aug 02 12:06:27 2007 +0200
     4.3 @@ -14,7 +14,6 @@
     4.4  sig
     4.5    val debug_simp: bool ref
     4.6    val trace_simp: bool ref
     4.7 -  val simp_depth_limit: int ref
     4.8    val trace_simp_depth_limit: int ref
     4.9    type rrule
    4.10    val eq_rrule: rrule * rrule -> bool
    4.11 @@ -94,6 +93,8 @@
    4.12    include BASIC_META_SIMPLIFIER
    4.13    exception SIMPLIFIER of string * thm
    4.14    val solver: simpset -> solver -> int -> tactic
    4.15 +  val simp_depth_limit_value: Config.value Config.T
    4.16 +  val simp_depth_limit: int Config.T
    4.17    val clear_ss: simpset -> simpset
    4.18    val simproc_i: theory -> string -> term list
    4.19      -> (theory -> simpset -> term -> thm option) -> simproc
    4.20 @@ -254,7 +255,9 @@
    4.21  
    4.22  (* simp depth *)
    4.23  
    4.24 -val simp_depth_limit = ref 100;
    4.25 +val simp_depth_limit_value = Config.declare false "simp_depth_limit" (Config.Int 100);
    4.26 +val simp_depth_limit = Config.int simp_depth_limit_value;
    4.27 +
    4.28  val trace_simp_depth_limit = ref 1;
    4.29  
    4.30  fun trace_depth (Simpset ({depth = (depth, exceeded), ...}, _)) msg =
    4.31 @@ -884,6 +887,7 @@
    4.32  
    4.33  fun rewritec (prover, thyt, maxt) ss t =
    4.34    let
    4.35 +    val ctxt = the_context ss;
    4.36      val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
    4.37      val eta_thm = Thm.eta_conversion t;
    4.38      val eta_t' = Thm.rhs_of eta_thm;
    4.39 @@ -914,7 +918,7 @@
    4.40                in SOME (thm'', uncond_skel (congs, lr)) end)
    4.41             else
    4.42               (trace_thm (fn () => "Trying to rewrite:") ss thm';
    4.43 -              if simp_depth ss > ! simp_depth_limit
    4.44 +              if simp_depth ss > Config.get ctxt simp_depth_limit
    4.45                then let val s = "simp_depth_limit exceeded - giving up"
    4.46                     in trace false (fn () => s) ss; warning s; NONE end
    4.47                else
     5.1 --- a/src/Pure/simplifier.ML	Wed Aug 01 21:10:36 2007 +0200
     5.2 +++ b/src/Pure/simplifier.ML	Thu Aug 02 12:06:27 2007 +0200
     5.3 @@ -346,7 +346,7 @@
     5.4        >> (Library.apply o map Morphism.form))));
     5.5  
     5.6  end;
     5.7 -  
     5.8 +
     5.9  
    5.10  (* conversions *)
    5.11  
    5.12 @@ -389,11 +389,6 @@
    5.13    Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
    5.14    Scan.succeed asm_full_simp_tac);
    5.15  
    5.16 -fun simp_flags x = (Scan.repeat
    5.17 -  (Args.parens (Args.$$$ "depth_limit" -- Args.colon |-- Args.nat)
    5.18 -    >> setmp MetaSimplifier.simp_depth_limit)
    5.19 -  >> (curry (Library.foldl op o) I o rev)) x;
    5.20 -
    5.21  val cong_modifiers =
    5.22   [Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier),
    5.23    Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add),
    5.24 @@ -415,16 +410,16 @@
    5.25     @ cong_modifiers;
    5.26  
    5.27  fun simp_args more_mods =
    5.28 -  Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options -- Scan.lift simp_flags)
    5.29 +  Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options)
    5.30      (more_mods @ simp_modifiers');
    5.31  
    5.32 -fun simp_method ((prems, tac), FLAGS) ctxt = Method.METHOD (fn facts =>
    5.33 +fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
    5.34    ALLGOALS (Method.insert_tac (prems @ facts)) THEN
    5.35 -    (FLAGS o CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
    5.36 +    (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
    5.37  
    5.38 -fun simp_method' ((prems, tac), FLAGS) ctxt = Method.METHOD (fn facts =>
    5.39 +fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
    5.40    HEADGOAL (Method.insert_tac (prems @ facts) THEN'
    5.41 -      ((FLAGS o CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
    5.42 +      ((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
    5.43  
    5.44  
    5.45