tuned trace info (depth)
authornipkow
Mon May 23 11:14:58 2005 +0200 (2005-05-23)
changeset 160428e15ff79851a
parent 16041 5a8736668ced
child 16043 e38b2ec79a2e
tuned trace info (depth)
NEWS
src/Pure/meta_simplifier.ML
     1.1 --- a/NEWS	Mon May 23 11:06:41 2005 +0200
     1.2 +++ b/NEWS	Mon May 23 11:14:58 2005 +0200
     1.3 @@ -113,6 +113,9 @@
     1.4    etc.) may depend on the signature of the theory context being
     1.5    presently used for parsing/printing, see also isar-ref manual.
     1.6  
     1.7 +* Pure/Simplifier: you can control the depth to which conditional rewriting
     1.8 +  is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth Limit.
     1.9 +
    1.10  * Pure/Simplifier: simplification procedures may now take the current
    1.11    simpset into account (cf. Simplifier.simproc(_i) / mk_simproc
    1.12    interface), which is very useful for calling the Simplifier
     2.1 --- a/src/Pure/meta_simplifier.ML	Mon May 23 11:06:41 2005 +0200
     2.2 +++ b/src/Pure/meta_simplifier.ML	Mon May 23 11:14:58 2005 +0200
     2.3 @@ -15,6 +15,7 @@
     2.4    val debug_simp: bool ref
     2.5    val trace_simp: bool ref
     2.6    val simp_depth_limit: int ref
     2.7 +  val trace_simp_depth_limit: int ref
     2.8    type rrule
     2.9    type cong
    2.10    type solver
    2.11 @@ -24,8 +25,7 @@
    2.12    val rep_ss: simpset ->
    2.13     {rules: rrule Net.net,
    2.14      prems: thm list,
    2.15 -    bounds: int,
    2.16 -    depth: int} *
    2.17 +    bounds: int} *
    2.18     {congs: (string * cong) list * string list,
    2.19      procs: proc Net.net,
    2.20      mk_rews:
    2.21 @@ -107,11 +107,13 @@
    2.22  val trace_simp = ref false;
    2.23  val simp_depth = ref 0;
    2.24  val simp_depth_limit = ref 1000;
    2.25 +val trace_simp_depth_limit = ref 1000;
    2.26  
    2.27  local
    2.28  
    2.29  fun println a =
    2.30 -  tracing (case ! simp_depth of 0 => a | n => enclose "[" "]" (string_of_int n) ^ a);
    2.31 +  if !simp_depth > !trace_simp_depth_limit then ()
    2.32 +  else tracing (enclose "[" "]" (string_of_int(!simp_depth)) ^ a);
    2.33  
    2.34  fun prnt warn a = if warn then warning a else println a;
    2.35  fun prtm warn a sg t = prnt warn (a ^ "\n" ^ Sign.string_of_term sg t);
    2.36 @@ -195,7 +197,6 @@
    2.37      prems: current premises;
    2.38      bounds: maximal index of bound variables already used
    2.39        (for generating new names when rewriting under lambda abstractions);
    2.40 -    depth: depth of conditional rewriting;
    2.41      congs: association list of congruence rules and
    2.42             a list of `weak' congruence constants.
    2.43             A congruence is `weak' if it avoids normalization of some argument.
    2.44 @@ -218,8 +219,7 @@
    2.45    Simpset of
    2.46     {rules: rrule Net.net,
    2.47      prems: thm list,
    2.48 -    bounds: int,
    2.49 -    depth: int} *
    2.50 +    bounds: int} *
    2.51     {congs: (string * cong) list * string list,
    2.52      procs: proc Net.net,
    2.53      mk_rews: mk_rews,
    2.54 @@ -238,11 +238,11 @@
    2.55  
    2.56  fun rep_ss (Simpset args) = args;
    2.57  
    2.58 -fun make_ss1 (rules, prems, bounds, depth) =
    2.59 -  {rules = rules, prems = prems, bounds = bounds, depth = depth};
    2.60 +fun make_ss1 (rules, prems, bounds) =
    2.61 +  {rules = rules, prems = prems, bounds = bounds};
    2.62  
    2.63 -fun map_ss1 f {rules, prems, bounds, depth} =
    2.64 -  make_ss1 (f (rules, prems, bounds, depth));
    2.65 +fun map_ss1 f {rules, prems, bounds} =
    2.66 +  make_ss1 (f (rules, prems, bounds));
    2.67  
    2.68  fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =
    2.69    {congs = congs, procs = procs, mk_rews = mk_rews, termless = termless,
    2.70 @@ -253,9 +253,9 @@
    2.71  
    2.72  fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
    2.73  
    2.74 -fun map_simpset f (Simpset ({rules, prems, bounds, depth},
    2.75 +fun map_simpset f (Simpset ({rules, prems, bounds},
    2.76      {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers})) =
    2.77 -  make_simpset (f ((rules, prems, bounds, depth),
    2.78 +  make_simpset (f ((rules, prems, bounds),
    2.79      (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)));
    2.80  
    2.81  fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2);
    2.82 @@ -297,7 +297,7 @@
    2.83  local
    2.84  
    2.85  fun init_ss mk_rews termless subgoal_tac solvers =
    2.86 -  make_simpset ((Net.empty, [], 0, 0),
    2.87 +  make_simpset ((Net.empty, [], 0),
    2.88      (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
    2.89  
    2.90  val basic_mk_rews: mk_rews =
    2.91 @@ -320,10 +320,10 @@
    2.92  
    2.93  fun merge_ss (ss1, ss2) =
    2.94    let
    2.95 -    val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth},
    2.96 +    val Simpset ({rules = rules1, prems = prems1, bounds = bounds1},
    2.97       {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
    2.98        loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
    2.99 -    val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = _},
   2.100 +    val Simpset ({rules = rules2, prems = prems2, bounds = bounds2},
   2.101       {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
   2.102        loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
   2.103  
   2.104 @@ -337,7 +337,7 @@
   2.105      val unsafe_solvers' = merge_solvers unsafe_solvers1 unsafe_solvers2;
   2.106      val solvers' = merge_solvers solvers1 solvers2;
   2.107    in
   2.108 -    make_simpset ((rules', prems', bounds', depth), ((congs', weak'), procs',
   2.109 +    make_simpset ((rules', prems', bounds'), ((congs', weak'), procs',
   2.110        mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
   2.111    end;
   2.112  
   2.113 @@ -363,11 +363,11 @@
   2.114  
   2.115  (* bounds and prems *)
   2.116  
   2.117 -val incr_bounds = map_simpset1 (fn (rules, prems, bounds, depth) =>
   2.118 -  (rules, prems, bounds + 1, depth));
   2.119 +val incr_bounds = map_simpset1 (fn (rules, prems, bounds) =>
   2.120 +  (rules, prems, bounds + 1));
   2.121  
   2.122 -fun add_prems ths = map_simpset1 (fn (rules, prems, bounds, depth) =>
   2.123 -  (rules, ths @ prems, bounds, depth));
   2.124 +fun add_prems ths = map_simpset1 (fn (rules, prems, bounds) =>
   2.125 +  (rules, ths @ prems, bounds));
   2.126  
   2.127  fun prems_of_ss (Simpset ({prems, ...}, _)) = prems;
   2.128  
   2.129 @@ -381,11 +381,11 @@
   2.130  
   2.131  fun insert_rrule quiet (ss, rrule as {thm, name, lhs, elhs, perm}) =
   2.132   (trace_named_thm "Adding rewrite rule" (thm, name);
   2.133 -  ss |> map_simpset1 (fn (rules, prems, bounds, depth) =>
   2.134 +  ss |> map_simpset1 (fn (rules, prems, bounds) =>
   2.135      let
   2.136        val rrule2 as {elhs, ...} = mk_rrule2 rrule;
   2.137        val rules' = Net.insert_term ((term_of elhs, rrule2), rules, eq_rrule);
   2.138 -    in (rules', prems, bounds, depth) end)
   2.139 +    in (rules', prems, bounds) end)
   2.140    handle Net.INSERT =>
   2.141      (if quiet then () else warn_thm "Ignoring duplicate rewrite rule:" thm; ss));
   2.142  
   2.143 @@ -506,8 +506,8 @@
   2.144  (* delsimps *)
   2.145  
   2.146  fun del_rrule (ss, rrule as {thm, elhs, ...}) =
   2.147 -  ss |> map_simpset1 (fn (rules, prems, bounds, depth) =>
   2.148 -    (Net.delete_term ((term_of elhs, rrule), rules, eq_rrule), prems, bounds, depth))
   2.149 +  ss |> map_simpset1 (fn (rules, prems, bounds) =>
   2.150 +    (Net.delete_term ((term_of elhs, rrule), rules, eq_rrule), prems, bounds))
   2.151    handle Net.DELETE => (warn_thm "Rewrite rule not in simpset:" thm; ss);
   2.152  
   2.153  fun ss delsimps thms =
   2.154 @@ -757,21 +757,6 @@
   2.155    if term_varnames rhs subset term_varnames lhs then uncond_skel args
   2.156    else skel0;
   2.157  
   2.158 -fun incr_depth ss =
   2.159 -  let
   2.160 -    val ss' = ss |> map_simpset1 (fn (rules, prems, bounds, depth) =>
   2.161 -      (rules, prems, bounds, depth + 1));
   2.162 -    val Simpset ({depth = depth', ...}, _) = ss';
   2.163 -  in
   2.164 -    if depth' > ! simp_depth_limit
   2.165 -    then (warning "simp_depth_limit exceeded - giving up"; NONE)
   2.166 -    else
   2.167 -     (if depth' mod 10 = 0
   2.168 -      then warning ("Simplification depth " ^ string_of_int depth')
   2.169 -      else ();
   2.170 -      SOME ss')
   2.171 -  end;
   2.172 -
   2.173  (*
   2.174    Rewriting -- we try in order:
   2.175      (1) beta reduction
   2.176 @@ -813,10 +798,11 @@
   2.177                in SOME (thm'', uncond_skel (congs, lr)) end)
   2.178             else
   2.179               (trace_thm "Trying to rewrite:" thm';
   2.180 -              case incr_depth ss of
   2.181 -                NONE => (trace_thm "FAILED - reached depth limit" thm'; NONE)
   2.182 -              | SOME ss' =>
   2.183 -              (case prover ss' thm' of
   2.184 +              if !simp_depth > !simp_depth_limit
   2.185 +              then let val s = "simp_depth_limit exceeded - giving up"
   2.186 +                   in trace false s; warning s; NONE end
   2.187 +              else
   2.188 +              case prover ss thm' of
   2.189                  NONE => (trace_thm "FAILED" thm'; NONE)
   2.190                | SOME thm2 =>
   2.191                    (case check_conv true eta_thm thm2 of
   2.192 @@ -824,7 +810,7 @@
   2.193                       SOME thm2' =>
   2.194                         let val concl = Logic.strip_imp_concl prop
   2.195                             val lr = Logic.dest_equals concl
   2.196 -                       in SOME (thm2', cond_skel (congs, lr)) end))))
   2.197 +                       in SOME (thm2', cond_skel (congs, lr)) end)))
   2.198        end
   2.199  
   2.200      fun rews [] = NONE
   2.201 @@ -1099,16 +1085,18 @@
   2.202  *)
   2.203  
   2.204  fun rewrite_cterm mode prover ss ct =
   2.205 -  let
   2.206 -    val Simpset ({depth, ...}, _) = ss;
   2.207 -    val {sign, t, maxidx, ...} = Thm.rep_cterm ct;
   2.208 -  in
   2.209 -    trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ct;
   2.210 -    simp_depth := depth;
   2.211 -    bottomc (mode, prover, sign, maxidx) ss ct
   2.212 -  end handle THM (s, _, thms) =>
   2.213 -    error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
   2.214 -      Pretty.string_of (Display.pretty_thms thms));
   2.215 +  (simp_depth := !simp_depth + 1;
   2.216 +   if !simp_depth mod 10 = 0
   2.217 +   then warning ("Simplification depth " ^ string_of_int (!simp_depth))
   2.218 +   else ();
   2.219 +   trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ct;
   2.220 +   let val {sign, t, maxidx, ...} = Thm.rep_cterm ct
   2.221 +       val res = bottomc (mode, prover, sign, maxidx) ss ct
   2.222 +         handle THM (s, _, thms) =>
   2.223 +         error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
   2.224 +           Pretty.string_of (Display.pretty_thms thms))
   2.225 +   in simp_depth := !simp_depth - 1; res end
   2.226 +  ) handle exn => (simp_depth := 0; raise exn);
   2.227  
   2.228  (*Rewrite a cterm*)
   2.229  fun rewrite_aux _ _ [] = (fn ct => Thm.reflexive ct)