Traced depth of conditional rewriting
authornipkow
Thu Aug 23 14:32:48 2001 +0200 (2001-08-23)
changeset 11504935f9e8de0d0
parent 11503 4c25eef6f325
child 11505 a410fa8acfca
Traced depth of conditional rewriting
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Tue Aug 21 20:09:09 2001 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Thu Aug 23 14:32:48 2001 +0200
     1.3 @@ -137,6 +137,7 @@
     1.4               mk_sym: turns == around; (needs Drule!)
     1.5               mk_eq_True: turns P into P == True - logic specific;
     1.6      termless: relation for ordered rewriting;
     1.7 +    depth: depth of conditional rewriting;
     1.8  *)
     1.9  
    1.10  datatype meta_simpset =
    1.11 @@ -149,22 +150,26 @@
    1.12      mk_rews: {mk: thm -> thm list,
    1.13                mk_sym: thm -> thm option,
    1.14                mk_eq_True: thm -> thm option},
    1.15 -    termless: term * term -> bool};
    1.16 +    termless: term * term -> bool,
    1.17 +    depth: int};
    1.18  
    1.19 -fun mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless) =
    1.20 +fun mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless, depth) =
    1.21    Mss {rules = rules, congs = congs, procs = procs, bounds = bounds,
    1.22 -       prems=prems, mk_rews=mk_rews, termless=termless};
    1.23 +       prems=prems, mk_rews=mk_rews, termless=termless, depth=depth};
    1.24  
    1.25 -fun upd_rules(Mss{rules,congs,procs,bounds,prems,mk_rews,termless}, rules') =
    1.26 -  mk_mss(rules',congs,procs,bounds,prems,mk_rews,termless);
    1.27 +fun upd_rules(Mss{rules,congs,procs,bounds,prems,mk_rews,termless,depth}, rules') =
    1.28 +  mk_mss(rules',congs,procs,bounds,prems,mk_rews,termless,depth);
    1.29  
    1.30  val empty_mss =
    1.31    let val mk_rews = {mk = K [], mk_sym = K None, mk_eq_True = K None}
    1.32 -  in mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, Term.termless) end;
    1.33 +  in mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, Term.termless, 0) end;
    1.34  
    1.35  fun clear_mss (Mss {mk_rews, termless, ...}) =
    1.36 -  mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, termless);
    1.37 +  mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, termless,0);
    1.38  
    1.39 +fun incr_depth(Mss{rules,congs,procs,bounds,prems,mk_rews,termless,depth}) =
    1.40 +  mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless, depth+1)
    1.41 + 
    1.42  
    1.43  
    1.44  (** simpset operations **)
    1.45 @@ -187,11 +192,11 @@
    1.46       |> Library.sort_wrt #1};
    1.47  
    1.48  
    1.49 -(* merge_mss *)		(*NOTE: ignores mk_rews and termless of 2nd mss*)
    1.50 +(* merge_mss *)	      (*NOTE: ignores mk_rews, termless and depth of 2nd mss*)
    1.51  
    1.52  fun merge_mss
    1.53   (Mss {rules = rules1, congs = (congs1,weak1), procs = procs1,
    1.54 -       bounds = bounds1, prems = prems1, mk_rews, termless},
    1.55 +       bounds = bounds1, prems = prems1, mk_rews, termless, depth},
    1.56    Mss {rules = rules2, congs = (congs2,weak2), procs = procs2,
    1.57         bounds = bounds2, prems = prems2, ...}) =
    1.58        mk_mss
    1.59 @@ -201,7 +206,7 @@
    1.60          Net.merge (procs1, procs2, eq_simproc),
    1.61          merge_lists bounds1 bounds2,
    1.62          generic_merge eq_prem I I prems1 prems2,
    1.63 -        mk_rews, termless);
    1.64 +        mk_rews, termless, depth);
    1.65  
    1.66  
    1.67  (* add_simps *)
    1.68 @@ -365,7 +370,7 @@
    1.69    is_full_cong_prems prems (xs ~~ ys)
    1.70  end
    1.71  
    1.72 -fun add_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thm) =
    1.73 +fun add_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, thm) =
    1.74    let
    1.75      val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (cprop_of thm)) handle TERM _ =>
    1.76        raise SIMPLIFIER ("Congruence not a meta-equality", thm);
    1.77 @@ -377,7 +382,7 @@
    1.78             ("Overwriting congruence rule for " ^ quote a);
    1.79      val weak2 = if is_full_cong thm then weak else a::weak
    1.80    in
    1.81 -    mk_mss (rules, (alist2,weak2), procs, bounds, prems, mk_rews, termless)
    1.82 +    mk_mss (rules,(alist2,weak2),procs,bounds,prems,mk_rews,termless,depth)
    1.83    end;
    1.84  
    1.85  val (op add_congs) = foldl add_cong;
    1.86 @@ -385,7 +390,7 @@
    1.87  
    1.88  (* del_congs *)
    1.89  
    1.90 -fun del_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thm) =
    1.91 +fun del_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, thm) =
    1.92    let
    1.93      val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ =>
    1.94        raise SIMPLIFIER ("Congruence not a meta-equality", thm);
    1.95 @@ -398,7 +403,7 @@
    1.96                                                else Some a)
    1.97                     alist2
    1.98    in
    1.99 -    mk_mss (rules, (alist2,weak2), procs, bounds, prems, mk_rews, termless)
   1.100 +    mk_mss (rules,(alist2,weak2),procs,bounds,prems,mk_rews,termless,depth)
   1.101    end;
   1.102  
   1.103  val (op del_congs) = foldl del_cong;
   1.104 @@ -406,7 +411,7 @@
   1.105  
   1.106  (* add_simprocs *)
   1.107  
   1.108 -fun add_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
   1.109 +fun add_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth},
   1.110      (name, lhs, proc, id)) =
   1.111    let val {sign, t, ...} = rep_cterm lhs
   1.112    in (trace_term false ("Adding simplification procedure " ^ quote name ^ " for")
   1.113 @@ -417,7 +422,7 @@
   1.114  	    (warning ("Ignoring duplicate simplification procedure \"" 
   1.115  	              ^ name ^ "\""); 
   1.116  	     procs),
   1.117 -        bounds, prems, mk_rews, termless))
   1.118 +        bounds, prems, mk_rews, termless,depth))
   1.119    end;
   1.120  
   1.121  fun add_simproc (mss, (name, lhss, proc, id)) =
   1.122 @@ -428,14 +433,14 @@
   1.123  
   1.124  (* del_simprocs *)
   1.125  
   1.126 -fun del_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
   1.127 +fun del_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth},
   1.128      (name, lhs, proc, id)) =
   1.129    mk_mss (rules, congs,
   1.130      Net.delete_term ((term_of lhs, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
   1.131        handle Net.DELETE => 
   1.132  	  (warning ("Simplification procedure \"" ^ name ^
   1.133  		       "\" not in simpset"); procs),
   1.134 -      bounds, prems, mk_rews, termless);
   1.135 +      bounds, prems, mk_rews, termless, depth);
   1.136  
   1.137  fun del_simproc (mss, (name, lhss, proc, id)) =
   1.138    foldl del_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
   1.139 @@ -445,8 +450,8 @@
   1.140  
   1.141  (* prems *)
   1.142  
   1.143 -fun add_prems (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thms) =
   1.144 -  mk_mss (rules, congs, procs, bounds, thms @ prems, mk_rews, termless);
   1.145 +fun add_prems (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, thms) =
   1.146 +  mk_mss (rules, congs, procs, bounds, thms @ prems, mk_rews, termless, depth);
   1.147  
   1.148  fun prems_of_mss (Mss {prems, ...}) = prems;
   1.149  
   1.150 @@ -454,28 +459,28 @@
   1.151  (* mk_rews *)
   1.152  
   1.153  fun set_mk_rews
   1.154 -  (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk) =
   1.155 +  (Mss {rules, congs, procs, bounds, prems, mk_rews, termless, depth}, mk) =
   1.156      mk_mss (rules, congs, procs, bounds, prems,
   1.157              {mk=mk, mk_sym= #mk_sym mk_rews, mk_eq_True= #mk_eq_True mk_rews},
   1.158 -            termless);
   1.159 +            termless, depth);
   1.160  
   1.161  fun set_mk_sym
   1.162 -  (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk_sym) =
   1.163 +  (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, mk_sym) =
   1.164      mk_mss (rules, congs, procs, bounds, prems,
   1.165              {mk= #mk mk_rews, mk_sym= mk_sym, mk_eq_True= #mk_eq_True mk_rews},
   1.166 -            termless);
   1.167 +            termless,depth);
   1.168  
   1.169  fun set_mk_eq_True
   1.170 -  (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk_eq_True) =
   1.171 +  (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, mk_eq_True) =
   1.172      mk_mss (rules, congs, procs, bounds, prems,
   1.173              {mk= #mk mk_rews, mk_sym= #mk_sym mk_rews, mk_eq_True= mk_eq_True},
   1.174 -            termless);
   1.175 +            termless,depth);
   1.176  
   1.177  (* termless *)
   1.178  
   1.179  fun set_termless
   1.180 -  (Mss {rules, congs, procs, bounds, prems, mk_rews, termless = _}, termless) =
   1.181 -    mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless);
   1.182 +  (Mss {rules, congs, procs, bounds, prems, mk_rews, depth, ...}, termless) =
   1.183 +    mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless, depth);
   1.184  
   1.185  
   1.186  
   1.187 @@ -563,7 +568,7 @@
   1.188  *)
   1.189  
   1.190  fun rewritec (prover, signt, maxt)
   1.191 -             (mss as Mss{rules, procs, termless, prems, congs, ...}) t =
   1.192 +             (mss as Mss{rules, procs, termless, prems, congs, depth,...}) t =
   1.193    let
   1.194      val eta_thm = Thm.eta_conversion t;
   1.195      val eta_t' = rhs_of eta_thm;
   1.196 @@ -588,24 +593,26 @@
   1.197          then (trace_thm false "Cannot apply permutative rewrite rule:" thm;
   1.198                trace_thm false "Term does not become smaller:" thm'; None)
   1.199          else
   1.200 -          (trace_thm false "Applying instance of rewrite rule:" thm;
   1.201 +          let val ds = "[" ^ string_of_int depth ^ "]"
   1.202 +          in trace_thm false "Applying instance of rewrite rule:" thm;
   1.203             if unconditional
   1.204             then
   1.205 -             (trace_thm false "Rewriting:" thm';
   1.206 +             (trace_thm false (ds ^ "Rewriting:") thm';
   1.207                let val lr = Logic.dest_equals prop;
   1.208                    val Some thm'' = check_conv false eta_thm thm'
   1.209                in Some (thm'', uncond_skel (congs, lr)) end)
   1.210             else
   1.211 -             (trace_thm false "Trying to rewrite:" thm';
   1.212 -              case prover mss thm' of
   1.213 -                None       => (trace_thm false "FAILED" thm'; None)
   1.214 +             (trace_thm false (ds ^ "Trying to rewrite:") thm';
   1.215 +              case prover (incr_depth mss) thm' of
   1.216 +                None       => (trace_thm false (ds ^ "FAILED") thm'; None)
   1.217                | Some thm2 =>
   1.218                    (case check_conv true eta_thm thm2 of
   1.219                       None => None |
   1.220                       Some thm2' =>
   1.221                         let val concl = Logic.strip_imp_concl prop
   1.222                             val lr = Logic.dest_equals concl
   1.223 -                       in Some (thm2', cond_skel (congs, lr)) end)))
   1.224 +                       in Some (thm2', cond_skel (congs, lr)) end))
   1.225 +          end
   1.226        end
   1.227  
   1.228      fun rews [] = None
   1.229 @@ -694,12 +701,12 @@
   1.230               Some trec1 => trec1 | None => (reflexive t))
   1.231  
   1.232      and subc skel
   1.233 -          (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless}) t0 =
   1.234 +          (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless,depth}) t0 =
   1.235         (case term_of t0 of
   1.236             Abs (a, T, t) =>
   1.237               let val b = variant bounds a
   1.238                   val (v, t') = Thm.dest_abs (Some ("." ^ b)) t0
   1.239 -                 val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless)
   1.240 +                 val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless,depth)
   1.241                   val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0
   1.242               in case botc skel' mss' t' of
   1.243                    Some thm => Some (abstract_rule a v thm)