added simp_depth_limit
authornipkow
Tue Feb 25 18:49:23 2003 +0100 (2003-02-25)
changeset 13828fb6ec40dd291
parent 13827 c690cb885db4
child 13829 af0218406395
added simp_depth_limit
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Tue Feb 25 15:27:01 2003 +0100
     1.2 +++ b/src/Pure/meta_simplifier.ML	Tue Feb 25 18:49:23 2003 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4  sig
     1.5    val trace_simp: bool ref
     1.6    val debug_simp: bool ref
     1.7 +  val simp_depth_limit: int ref
     1.8  end;
     1.9  
    1.10  signature META_SIMPLIFIER =
    1.11 @@ -67,6 +68,7 @@
    1.12  exception SIMPROC_FAIL of string * exn;
    1.13  
    1.14  val simp_depth = ref 0;
    1.15 +val simp_depth_limit = ref 1000;
    1.16  
    1.17  local
    1.18  
    1.19 @@ -188,8 +190,15 @@
    1.20    mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, termless,0);
    1.21  
    1.22  fun incr_depth(Mss{rules,congs,procs,bounds,prems,mk_rews,termless,depth}) =
    1.23 -  mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless, depth+1)
    1.24 -
    1.25 +  let val depth1 = depth+1
    1.26 +  in if depth1 > !simp_depth_limit
    1.27 +     then (warning "simp_depth_limit exceeded - giving up"; None)
    1.28 +     else (if depth1 mod 5 = 0
    1.29 +           then warning("Simplification depth " ^ string_of_int depth1)
    1.30 +           else ();
    1.31 +           Some(mk_mss(rules,congs,procs,bounds,prems,mk_rews,termless,depth1))
    1.32 +          )
    1.33 +  end;
    1.34  
    1.35  
    1.36  (** simpset operations **)
    1.37 @@ -622,7 +631,10 @@
    1.38                in Some (thm'', uncond_skel (congs, lr)) end)
    1.39             else
    1.40               (trace_thm "Trying to rewrite:" thm';
    1.41 -              case prover (incr_depth mss) thm' of
    1.42 +              case incr_depth mss of
    1.43 +                None => (trace_thm "FAILED - reached depth limit" thm'; None)
    1.44 +              | Some mss =>
    1.45 +              (case prover mss thm' of
    1.46                  None       => (trace_thm "FAILED" thm'; None)
    1.47                | Some thm2 =>
    1.48                    (case check_conv true eta_thm thm2 of
    1.49 @@ -630,7 +642,7 @@
    1.50                       Some thm2' =>
    1.51                         let val concl = Logic.strip_imp_concl prop
    1.52                             val lr = Logic.dest_equals concl
    1.53 -                       in Some (thm2', cond_skel (congs, lr)) end)))
    1.54 +                       in Some (thm2', cond_skel (congs, lr)) end))))
    1.55        end
    1.56  
    1.57      fun rews [] = None