# HG changeset patch
# User nipkow
# Date 1046195363 -3600
# Node ID fb6ec40dd291510d3ef057618cbbec26f7217bff
# Parent  c690cb885db4a2edfabd5ef110428bc81a09ca40
added simp_depth_limit

diff -r c690cb885db4 -r fb6ec40dd291 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Tue Feb 25 15:27:01 2003 +0100
+++ b/src/Pure/meta_simplifier.ML	Tue Feb 25 18:49:23 2003 +0100
@@ -10,6 +10,7 @@
 sig
   val trace_simp: bool ref
   val debug_simp: bool ref
+  val simp_depth_limit: int ref
 end;
 
 signature META_SIMPLIFIER =
@@ -67,6 +68,7 @@
 exception SIMPROC_FAIL of string * exn;
 
 val simp_depth = ref 0;
+val simp_depth_limit = ref 1000;
 
 local
 
@@ -188,8 +190,15 @@
   mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, termless,0);
 
 fun incr_depth(Mss{rules,congs,procs,bounds,prems,mk_rews,termless,depth}) =
-  mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless, depth+1)
-
+  let val depth1 = depth+1
+  in if depth1 > !simp_depth_limit
+     then (warning "simp_depth_limit exceeded - giving up"; None)
+     else (if depth1 mod 5 = 0
+           then warning("Simplification depth " ^ string_of_int depth1)
+           else ();
+           Some(mk_mss(rules,congs,procs,bounds,prems,mk_rews,termless,depth1))
+          )
+  end;
 
 
 (** simpset operations **)
@@ -622,7 +631,10 @@
               in Some (thm'', uncond_skel (congs, lr)) end)
            else
              (trace_thm "Trying to rewrite:" thm';
-              case prover (incr_depth mss) thm' of
+              case incr_depth mss of
+                None => (trace_thm "FAILED - reached depth limit" thm'; None)
+              | Some mss =>
+              (case prover mss thm' of
                 None       => (trace_thm "FAILED" thm'; None)
               | Some thm2 =>
                   (case check_conv true eta_thm thm2 of
@@ -630,7 +642,7 @@
                      Some thm2' =>
                        let val concl = Logic.strip_imp_concl prop
                            val lr = Logic.dest_equals concl
-                       in Some (thm2', cond_skel (congs, lr)) end)))
+                       in Some (thm2', cond_skel (congs, lr)) end))))
       end
 
     fun rews [] = None