tuned tracing markup;
authorwenzelm
Thu Dec 27 16:46:52 2001 +0100 (2001-12-27)
changeset 126037d2bca103101
parent 12602 6984018a98e3
child 12604 5292f393c64b
tuned tracing markup;
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu Dec 27 16:46:28 2001 +0100
     1.2 +++ b/src/Pure/meta_simplifier.ML	Thu Dec 27 16:46:52 2001 +0100
     1.3 @@ -17,20 +17,20 @@
     1.4    include BASIC_META_SIMPLIFIER
     1.5    exception SIMPLIFIER of string * thm
     1.6    type meta_simpset
     1.7 -  val dest_mss		: meta_simpset ->
     1.8 +  val dest_mss          : meta_simpset ->
     1.9      {simps: thm list, congs: thm list, procs: (string * cterm list) list}
    1.10    val empty_mss         : meta_simpset
    1.11 -  val clear_mss		: meta_simpset -> meta_simpset
    1.12 -  val merge_mss		: meta_simpset * meta_simpset -> meta_simpset
    1.13 +  val clear_mss         : meta_simpset -> meta_simpset
    1.14 +  val merge_mss         : meta_simpset * meta_simpset -> meta_simpset
    1.15    val add_simps         : meta_simpset * thm list -> meta_simpset
    1.16    val del_simps         : meta_simpset * thm list -> meta_simpset
    1.17    val mss_of            : thm list -> meta_simpset
    1.18    val add_congs         : meta_simpset * thm list -> meta_simpset
    1.19    val del_congs         : meta_simpset * thm list -> meta_simpset
    1.20 -  val add_simprocs	: meta_simpset *
    1.21 +  val add_simprocs      : meta_simpset *
    1.22      (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
    1.23        -> meta_simpset
    1.24 -  val del_simprocs	: meta_simpset *
    1.25 +  val del_simprocs      : meta_simpset *
    1.26      (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
    1.27        -> meta_simpset
    1.28    val add_prems         : meta_simpset * thm list -> meta_simpset
    1.29 @@ -64,19 +64,18 @@
    1.30  
    1.31  val simp_depth = ref 0;
    1.32  
    1.33 -fun println a = tracing (replicate_string (! simp_depth) " " ^ a);
    1.34 +local
    1.35 +
    1.36 +fun println a =
    1.37 +  tracing ((case ! simp_depth of 0 => "" | n => "[" ^ string_of_int n ^ "]") ^ a);
    1.38  
    1.39  fun prnt warn a = if warn then warning a else println a;
    1.40 -
    1.41 -fun prtm warn a sign t =
    1.42 -  (prnt warn a; prnt warn (Sign.string_of_term sign t));
    1.43 +fun prtm warn a sign t = prnt warn (a ^ "\n" ^ Sign.string_of_term sign t);
    1.44 +fun prctm warn a t = prnt warn (a ^ "\n" ^ Display.string_of_cterm t);
    1.45  
    1.46 -fun prctm warn a t =
    1.47 -  (prnt warn a; prnt warn (Display.string_of_cterm t));
    1.48 +in
    1.49  
    1.50 -fun prthm warn a thm =
    1.51 -  let val {sign, prop, ...} = rep_thm thm
    1.52 -  in prtm warn a sign prop end;
    1.53 +fun prthm warn a = prctm warn a o Thm.cprop_of;
    1.54  
    1.55  val trace_simp = ref false;
    1.56  val debug_simp = ref false;
    1.57 @@ -92,6 +91,7 @@
    1.58    let val {sign, prop, ...} = rep_thm thm
    1.59    in trace_term warn a sign prop end;
    1.60  
    1.61 +end;
    1.62  
    1.63  
    1.64  (** meta simp sets **)
    1.65 @@ -104,7 +104,7 @@
    1.66     elhs: the etac-contracted lhs.
    1.67     fo:  use first-order matching
    1.68     perm: the rewrite rule is permutative
    1.69 -Reamrks:
    1.70 +Remarks:
    1.71    - elhs is used for matching,
    1.72      lhs only for preservation of bound variable names.
    1.73    - fo is set iff
    1.74 @@ -120,7 +120,7 @@
    1.75  fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
    1.76    #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
    1.77  
    1.78 -fun eq_cong ({thm = thm1, ...}: cong, {thm = thm2, ...}: cong) = 
    1.79 +fun eq_cong ({thm = thm1, ...}: cong, {thm = thm2, ...}: cong) =
    1.80    #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
    1.81  
    1.82  fun eq_prem (thm1, thm2) =
    1.83 @@ -181,7 +181,7 @@
    1.84  
    1.85  fun incr_depth(Mss{rules,congs,procs,bounds,prems,mk_rews,termless,depth}) =
    1.86    mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless, depth+1)
    1.87 - 
    1.88 +
    1.89  
    1.90  
    1.91  (** simpset operations **)
    1.92 @@ -204,7 +204,7 @@
    1.93       |> Library.sort_wrt #1};
    1.94  
    1.95  
    1.96 -(* merge_mss *)	      (*NOTE: ignores mk_rews, termless and depth of 2nd mss*)
    1.97 +(* merge_mss *)       (*NOTE: ignores mk_rews, termless and depth of 2nd mss*)
    1.98  
    1.99  fun merge_mss
   1.100   (Mss {rules = rules1, congs = (congs1,weak1), procs = procs1,
   1.101 @@ -430,10 +430,10 @@
   1.102        sign t;
   1.103      mk_mss (rules, congs,
   1.104        Net.insert_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
   1.105 -        handle Net.INSERT => 
   1.106 -	    (warning ("Ignoring duplicate simplification procedure \"" 
   1.107 -	              ^ name ^ "\""); 
   1.108 -	     procs),
   1.109 +        handle Net.INSERT =>
   1.110 +            (warning ("Ignoring duplicate simplification procedure \""
   1.111 +                      ^ name ^ "\"");
   1.112 +             procs),
   1.113          bounds, prems, mk_rews, termless,depth))
   1.114    end;
   1.115  
   1.116 @@ -449,9 +449,9 @@
   1.117      (name, lhs, proc, id)) =
   1.118    mk_mss (rules, congs,
   1.119      Net.delete_term ((term_of lhs, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
   1.120 -      handle Net.DELETE => 
   1.121 -	  (warning ("Simplification procedure \"" ^ name ^
   1.122 -		       "\" not in simpset"); procs),
   1.123 +      handle Net.DELETE =>
   1.124 +          (warning ("Simplification procedure \"" ^ name ^
   1.125 +                       "\" not in simpset"); procs),
   1.126        bounds, prems, mk_rews, termless, depth);
   1.127  
   1.128  fun del_simproc (mss, (name, lhss, proc, id)) =
   1.129 @@ -630,11 +630,11 @@
   1.130            in case opt of None => rews rrules | some => some end;
   1.131  
   1.132      fun sort_rrules rrs = let
   1.133 -      fun is_simple({thm, ...}:rrule) = case #prop (rep_thm thm) of 
   1.134 +      fun is_simple({thm, ...}:rrule) = case #prop (rep_thm thm) of
   1.135                                        Const("==",_) $ _ $ _ => true
   1.136 -                                      | _                   => false 
   1.137 +                                      | _                   => false
   1.138        fun sort []        (re1,re2) = re1 @ re2
   1.139 -        | sort (rr::rrs) (re1,re2) = if is_simple rr 
   1.140 +        | sort (rr::rrs) (re1,re2) = if is_simple rr
   1.141                                       then sort rrs (rr::re1,re2)
   1.142                                       else sort rrs (re1,rr::re2)
   1.143      in sort rrs ([],[]) end
   1.144 @@ -823,7 +823,7 @@
   1.145          fun rebuild None = (case rewritec (prover, sign, maxidx) mss
   1.146              (mk_implies (prem1, conc)) of
   1.147                None => None
   1.148 -            | Some (thm, _) => 
   1.149 +            | Some (thm, _) =>
   1.150                  let val (prem, conc) = Drule.dest_implies (rhs_of thm)
   1.151                  in (case mut_impc (prems, prem, conc, mss) of
   1.152                      None => Some (None, thm)