src/Pure/meta_simplifier.ML
changeset 16042 8e15ff79851a
parent 15574 b1d1b5bfc464
child 16305 5e7b6731b004
     1.1 --- a/src/Pure/meta_simplifier.ML	Mon May 23 11:06:41 2005 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Mon May 23 11:14:58 2005 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    val debug_simp: bool ref
     1.5    val trace_simp: bool ref
     1.6    val simp_depth_limit: int ref
     1.7 +  val trace_simp_depth_limit: int ref
     1.8    type rrule
     1.9    type cong
    1.10    type solver
    1.11 @@ -24,8 +25,7 @@
    1.12    val rep_ss: simpset ->
    1.13     {rules: rrule Net.net,
    1.14      prems: thm list,
    1.15 -    bounds: int,
    1.16 -    depth: int} *
    1.17 +    bounds: int} *
    1.18     {congs: (string * cong) list * string list,
    1.19      procs: proc Net.net,
    1.20      mk_rews:
    1.21 @@ -107,11 +107,13 @@
    1.22  val trace_simp = ref false;
    1.23  val simp_depth = ref 0;
    1.24  val simp_depth_limit = ref 1000;
    1.25 +val trace_simp_depth_limit = ref 1000;
    1.26  
    1.27  local
    1.28  
    1.29  fun println a =
    1.30 -  tracing (case ! simp_depth of 0 => a | n => enclose "[" "]" (string_of_int n) ^ a);
    1.31 +  if !simp_depth > !trace_simp_depth_limit then ()
    1.32 +  else tracing (enclose "[" "]" (string_of_int(!simp_depth)) ^ a);
    1.33  
    1.34  fun prnt warn a = if warn then warning a else println a;
    1.35  fun prtm warn a sg t = prnt warn (a ^ "\n" ^ Sign.string_of_term sg t);
    1.36 @@ -195,7 +197,6 @@
    1.37      prems: current premises;
    1.38      bounds: maximal index of bound variables already used
    1.39        (for generating new names when rewriting under lambda abstractions);
    1.40 -    depth: depth of conditional rewriting;
    1.41      congs: association list of congruence rules and
    1.42             a list of `weak' congruence constants.
    1.43             A congruence is `weak' if it avoids normalization of some argument.
    1.44 @@ -218,8 +219,7 @@
    1.45    Simpset of
    1.46     {rules: rrule Net.net,
    1.47      prems: thm list,
    1.48 -    bounds: int,
    1.49 -    depth: int} *
    1.50 +    bounds: int} *
    1.51     {congs: (string * cong) list * string list,
    1.52      procs: proc Net.net,
    1.53      mk_rews: mk_rews,
    1.54 @@ -238,11 +238,11 @@
    1.55  
    1.56  fun rep_ss (Simpset args) = args;
    1.57  
    1.58 -fun make_ss1 (rules, prems, bounds, depth) =
    1.59 -  {rules = rules, prems = prems, bounds = bounds, depth = depth};
    1.60 +fun make_ss1 (rules, prems, bounds) =
    1.61 +  {rules = rules, prems = prems, bounds = bounds};
    1.62  
    1.63 -fun map_ss1 f {rules, prems, bounds, depth} =
    1.64 -  make_ss1 (f (rules, prems, bounds, depth));
    1.65 +fun map_ss1 f {rules, prems, bounds} =
    1.66 +  make_ss1 (f (rules, prems, bounds));
    1.67  
    1.68  fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =
    1.69    {congs = congs, procs = procs, mk_rews = mk_rews, termless = termless,
    1.70 @@ -253,9 +253,9 @@
    1.71  
    1.72  fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
    1.73  
    1.74 -fun map_simpset f (Simpset ({rules, prems, bounds, depth},
    1.75 +fun map_simpset f (Simpset ({rules, prems, bounds},
    1.76      {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers})) =
    1.77 -  make_simpset (f ((rules, prems, bounds, depth),
    1.78 +  make_simpset (f ((rules, prems, bounds),
    1.79      (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)));
    1.80  
    1.81  fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2);
    1.82 @@ -297,7 +297,7 @@
    1.83  local
    1.84  
    1.85  fun init_ss mk_rews termless subgoal_tac solvers =
    1.86 -  make_simpset ((Net.empty, [], 0, 0),
    1.87 +  make_simpset ((Net.empty, [], 0),
    1.88      (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
    1.89  
    1.90  val basic_mk_rews: mk_rews =
    1.91 @@ -320,10 +320,10 @@
    1.92  
    1.93  fun merge_ss (ss1, ss2) =
    1.94    let
    1.95 -    val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth},
    1.96 +    val Simpset ({rules = rules1, prems = prems1, bounds = bounds1},
    1.97       {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
    1.98        loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
    1.99 -    val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = _},
   1.100 +    val Simpset ({rules = rules2, prems = prems2, bounds = bounds2},
   1.101       {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
   1.102        loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
   1.103  
   1.104 @@ -337,7 +337,7 @@
   1.105      val unsafe_solvers' = merge_solvers unsafe_solvers1 unsafe_solvers2;
   1.106      val solvers' = merge_solvers solvers1 solvers2;
   1.107    in
   1.108 -    make_simpset ((rules', prems', bounds', depth), ((congs', weak'), procs',
   1.109 +    make_simpset ((rules', prems', bounds'), ((congs', weak'), procs',
   1.110        mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
   1.111    end;
   1.112  
   1.113 @@ -363,11 +363,11 @@
   1.114  
   1.115  (* bounds and prems *)
   1.116  
   1.117 -val incr_bounds = map_simpset1 (fn (rules, prems, bounds, depth) =>
   1.118 -  (rules, prems, bounds + 1, depth));
   1.119 +val incr_bounds = map_simpset1 (fn (rules, prems, bounds) =>
   1.120 +  (rules, prems, bounds + 1));
   1.121  
   1.122 -fun add_prems ths = map_simpset1 (fn (rules, prems, bounds, depth) =>
   1.123 -  (rules, ths @ prems, bounds, depth));
   1.124 +fun add_prems ths = map_simpset1 (fn (rules, prems, bounds) =>
   1.125 +  (rules, ths @ prems, bounds));
   1.126  
   1.127  fun prems_of_ss (Simpset ({prems, ...}, _)) = prems;
   1.128  
   1.129 @@ -381,11 +381,11 @@
   1.130  
   1.131  fun insert_rrule quiet (ss, rrule as {thm, name, lhs, elhs, perm}) =
   1.132   (trace_named_thm "Adding rewrite rule" (thm, name);
   1.133 -  ss |> map_simpset1 (fn (rules, prems, bounds, depth) =>
   1.134 +  ss |> map_simpset1 (fn (rules, prems, bounds) =>
   1.135      let
   1.136        val rrule2 as {elhs, ...} = mk_rrule2 rrule;
   1.137        val rules' = Net.insert_term ((term_of elhs, rrule2), rules, eq_rrule);
   1.138 -    in (rules', prems, bounds, depth) end)
   1.139 +    in (rules', prems, bounds) end)
   1.140    handle Net.INSERT =>
   1.141      (if quiet then () else warn_thm "Ignoring duplicate rewrite rule:" thm; ss));
   1.142  
   1.143 @@ -506,8 +506,8 @@
   1.144  (* delsimps *)
   1.145  
   1.146  fun del_rrule (ss, rrule as {thm, elhs, ...}) =
   1.147 -  ss |> map_simpset1 (fn (rules, prems, bounds, depth) =>
   1.148 -    (Net.delete_term ((term_of elhs, rrule), rules, eq_rrule), prems, bounds, depth))
   1.149 +  ss |> map_simpset1 (fn (rules, prems, bounds) =>
   1.150 +    (Net.delete_term ((term_of elhs, rrule), rules, eq_rrule), prems, bounds))
   1.151    handle Net.DELETE => (warn_thm "Rewrite rule not in simpset:" thm; ss);
   1.152  
   1.153  fun ss delsimps thms =
   1.154 @@ -757,21 +757,6 @@
   1.155    if term_varnames rhs subset term_varnames lhs then uncond_skel args
   1.156    else skel0;
   1.157  
   1.158 -fun incr_depth ss =
   1.159 -  let
   1.160 -    val ss' = ss |> map_simpset1 (fn (rules, prems, bounds, depth) =>
   1.161 -      (rules, prems, bounds, depth + 1));
   1.162 -    val Simpset ({depth = depth', ...}, _) = ss';
   1.163 -  in
   1.164 -    if depth' > ! simp_depth_limit
   1.165 -    then (warning "simp_depth_limit exceeded - giving up"; NONE)
   1.166 -    else
   1.167 -     (if depth' mod 10 = 0
   1.168 -      then warning ("Simplification depth " ^ string_of_int depth')
   1.169 -      else ();
   1.170 -      SOME ss')
   1.171 -  end;
   1.172 -
   1.173  (*
   1.174    Rewriting -- we try in order:
   1.175      (1) beta reduction
   1.176 @@ -813,10 +798,11 @@
   1.177                in SOME (thm'', uncond_skel (congs, lr)) end)
   1.178             else
   1.179               (trace_thm "Trying to rewrite:" thm';
   1.180 -              case incr_depth ss of
   1.181 -                NONE => (trace_thm "FAILED - reached depth limit" thm'; NONE)
   1.182 -              | SOME ss' =>
   1.183 -              (case prover ss' thm' of
   1.184 +              if !simp_depth > !simp_depth_limit
   1.185 +              then let val s = "simp_depth_limit exceeded - giving up"
   1.186 +                   in trace false s; warning s; NONE end
   1.187 +              else
   1.188 +              case prover ss thm' of
   1.189                  NONE => (trace_thm "FAILED" thm'; NONE)
   1.190                | SOME thm2 =>
   1.191                    (case check_conv true eta_thm thm2 of
   1.192 @@ -824,7 +810,7 @@
   1.193                       SOME thm2' =>
   1.194                         let val concl = Logic.strip_imp_concl prop
   1.195                             val lr = Logic.dest_equals concl
   1.196 -                       in SOME (thm2', cond_skel (congs, lr)) end))))
   1.197 +                       in SOME (thm2', cond_skel (congs, lr)) end)))
   1.198        end
   1.199  
   1.200      fun rews [] = NONE
   1.201 @@ -1099,16 +1085,18 @@
   1.202  *)
   1.203  
   1.204  fun rewrite_cterm mode prover ss ct =
   1.205 -  let
   1.206 -    val Simpset ({depth, ...}, _) = ss;
   1.207 -    val {sign, t, maxidx, ...} = Thm.rep_cterm ct;
   1.208 -  in
   1.209 -    trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ct;
   1.210 -    simp_depth := depth;
   1.211 -    bottomc (mode, prover, sign, maxidx) ss ct
   1.212 -  end handle THM (s, _, thms) =>
   1.213 -    error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
   1.214 -      Pretty.string_of (Display.pretty_thms thms));
   1.215 +  (simp_depth := !simp_depth + 1;
   1.216 +   if !simp_depth mod 10 = 0
   1.217 +   then warning ("Simplification depth " ^ string_of_int (!simp_depth))
   1.218 +   else ();
   1.219 +   trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ct;
   1.220 +   let val {sign, t, maxidx, ...} = Thm.rep_cterm ct
   1.221 +       val res = bottomc (mode, prover, sign, maxidx) ss ct
   1.222 +         handle THM (s, _, thms) =>
   1.223 +         error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
   1.224 +           Pretty.string_of (Display.pretty_thms thms))
   1.225 +   in simp_depth := !simp_depth - 1; res end
   1.226 +  ) handle exn => (simp_depth := 0; raise exn);
   1.227  
   1.228  (*Rewrite a cterm*)
   1.229  fun rewrite_aux _ _ [] = (fn ct => Thm.reflexive ct)