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 +fun prtm warn a sign t = prnt warn (a ^ "\n" ^ Sign.string_of_term sign t);
1.41 +fun prctm warn a t = prnt warn (a ^ "\n" ^ Display.string_of_cterm t);
1.42
1.43 -fun prtm warn a sign t =
1.44 - (prnt warn a; prnt warn (Sign.string_of_term sign t));
1.45 +in
1.46
1.47 -fun prctm warn a t =
1.48 - (prnt warn a; prnt warn (Display.string_of_cterm t));
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)