1(* ===================================================================== *)
2(* FILE          : Rewrite.sml                                           *)
3(* DESCRIPTION   : Basic rewriting routines. Translated from hol88.      *)
4(*                                                                       *)
5(* AUTHOR        : (c) Larry Paulson, University of Cambridge, for hol88 *)
6(* TRANSLATOR    : Konrad Slind, University of Calgary                   *)
7(* DATE          : September 11, 1991                                    *)
8(* REVISED       : November 1994, to encapsulate the type of rewrite     *)
9(*                 rules. (KLS)                                          *)
10(* ===================================================================== *)
11
12
13structure Rewrite :> Rewrite =
14struct
15
16open HolKernel boolTheory boolSyntax Drule BoundedRewrites Abbrev;
17
18val ERR = mk_HOL_ERR "Rewrite";
19
20type pred = term -> bool
21
22infix 3 ##
23
24(*---------------------------------------------------------------------------*)
25(* Datatype for controlling the application of individual rewrite rules      *)
26(*---------------------------------------------------------------------------*)
27
28datatype control = UNBOUNDED | BOUNDED of int ref
29
30
31(*---------------------------------------------------------------------------*
32 * Split a theorem into a list of theorems suitable for rewriting:           *
33 *                                                                           *
34 *   1. Specialize all variables (SPEC_ALL).                                 *
35 *                                                                           *
36 *   2. Then do the following:                                               *
37 *                                                                           *
38 *         |- t1 /\ t2 -->    [|- t1 ; |- t2]                                *
39 *                                                                           *
40 *   3. Then     |- t  --> |- t = T                                          *
41 *       and     |- ~t --> |- t = F                                          *
42 *                                                                           *
43 *---------------------------------------------------------------------------*)
44
45
46fun decompose tag th =
47 let val th = SPEC_ALL th
48     val t = concl th
49 in
50   if aconv t T then [] else
51   if is_eq t   then [(th,tag)] else
52   if is_conj t then (op@ o (decompose tag##decompose tag) o CONJ_PAIR) th else
53   if is_neg t  then [(EQF_INTRO th,tag)]
54                else [(EQT_INTRO th,tag)]
55  end
56  handle e => raise wrap_exn "Rewrite" "mk_rewrites.decompose" e;
57
58fun local_mk_rewrites th =
59 case total DEST_BOUNDED th
60  of NONE => decompose UNBOUNDED th
61   | SOME(th',n) => decompose (BOUNDED (ref n)) th';
62
63val mk_rewrites = map fst o local_mk_rewrites;
64
65(*---------------------------------------------------------------------------*)
66(* Support for examining some aspects of the work of the rewriter            *)
67(*---------------------------------------------------------------------------*)
68
69val monitoring = ref false;
70
71val _ = register_btrace ("Rewrite", monitoring) ;
72
73(*---------------------------------------------------------------------------*)
74(* Abstract datatype of rewrite rule sets.                                   *)
75(*---------------------------------------------------------------------------*)
76
77abstype rewrites = RW of {thms : thm list, net : conv Net.net}
78with
79 fun dest_rewrites(RW{thms, ...}) = thms
80 fun net_of(RW{net,...})          = net
81 val empty_rewrites = RW{thms = [], net= Net.empty}
82 val implicit = ref empty_rewrites;
83 fun implicit_rewrites() = !implicit
84 fun set_implicit_rewrites rws = (implicit := rws);
85
86fun add_rewrites (RW{thms,net}) thl =
87 let val rewrites = itlist (append o local_mk_rewrites) thl []
88     fun appconv (c,UNBOUNDED) tm     = c tm
89       | appconv (c,BOUNDED r) tm     = if !r = 0 then failwith "exceeded bound" else c tm before Portable.dec r
90 in
91   RW{thms = thms@thl,
92       net = itlist Net.insert
93                (map (fn (th,tag) =>
94                        (boolSyntax.lhs(concl th),
95                         (appconv (Conv.REWR_CONV th,tag)))) rewrites)
96                net}
97 end
98
99end (* abstype *)
100
101(*---------------------------------------------------------------------------
102     Create a conversion from some rewrites
103 ---------------------------------------------------------------------------*)
104
105fun REWRITES_CONV rws tm =
106 let val net = net_of rws
107 in if !monitoring
108    then case mapfilter (fn f => f tm) (Net.match tm net)
109          of []   => Conv.NO_CONV tm
110           | [x]  => (HOL_MESG (String.concat
111                       ["Rewrite:\n", Parse.thm_to_string x]) ; x)
112           | h::t => (HOL_MESG (String.concat
113                    ["Multiple rewrites possible (first taken):\n",
114                  String.concatWith ",\n" (map Parse.thm_to_string (h::t))]); h)
115    else Conv.FIRST_CONV (Net.match tm net) tm
116 end;
117
118
119(* Derived manipulations *)
120
121fun add_implicit_rewrites thl =
122    set_implicit_rewrites (add_rewrites (implicit_rewrites()) thl);
123
124val bool_rewrites =
125  add_rewrites empty_rewrites
126     [REFL_CLAUSE,  EQ_CLAUSES,  NOT_CLAUSES,  AND_CLAUSES,
127      OR_CLAUSES,   IMP_CLAUSES, COND_CLAUSES, FORALL_SIMP,
128      EXISTS_SIMP,  ABS_SIMP];
129
130val _ = set_implicit_rewrites bool_rewrites;
131
132(* =====================================================================*)
133(* Main rewriting conversion                                            *)
134(* =====================================================================*)
135
136fun GEN_REWRITE_CONV (rw_func:conv->conv) rws thl =
137   rw_func (REWRITES_CONV (add_rewrites rws thl));
138
139(* ---------------------------------------------------------------------*)
140(* Rewriting conversions.                                               *)
141(* ---------------------------------------------------------------------*)
142
143val PURE_REWRITE_CONV = GEN_REWRITE_CONV Conv.TOP_DEPTH_CONV empty_rewrites
144and
145PURE_ONCE_REWRITE_CONV = GEN_REWRITE_CONV Conv.ONCE_DEPTH_CONV empty_rewrites;
146
147fun REWRITE_CONV thl = GEN_REWRITE_CONV Conv.TOP_DEPTH_CONV
148                                        (implicit_rewrites()) thl
149and ONCE_REWRITE_CONV thl = GEN_REWRITE_CONV Conv.ONCE_DEPTH_CONV
150                                        (implicit_rewrites()) thl;
151
152(* Main rewriting rule *)
153fun GEN_REWRITE_RULE f rws = Conv.CONV_RULE o GEN_REWRITE_CONV f rws;
154
155val PURE_REWRITE_RULE = GEN_REWRITE_RULE Conv.TOP_DEPTH_CONV empty_rewrites
156and
157PURE_ONCE_REWRITE_RULE = GEN_REWRITE_RULE Conv.ONCE_DEPTH_CONV empty_rewrites;
158
159fun REWRITE_RULE thl = GEN_REWRITE_RULE Conv.TOP_DEPTH_CONV
160                                        (implicit_rewrites()) thl
161and ONCE_REWRITE_RULE thl = GEN_REWRITE_RULE Conv.ONCE_DEPTH_CONV
162                                             (implicit_rewrites()) thl;
163
164(* Rewrite a theorem with the help of its assumptions *)
165
166fun PURE_ASM_REWRITE_RULE thl th =
167   PURE_REWRITE_RULE ((map ASSUME (hyp th)) @ thl) th
168and
169PURE_ONCE_ASM_REWRITE_RULE thl th =
170   PURE_ONCE_REWRITE_RULE ((map ASSUME (hyp th)) @ thl) th
171and
172ASM_REWRITE_RULE thl th =
173   REWRITE_RULE ((map ASSUME (hyp th)) @ thl) th
174and
175ONCE_ASM_REWRITE_RULE thl th =
176   ONCE_REWRITE_RULE ((map ASSUME (hyp th)) @ thl) th;
177
178
179(* Main rewriting tactic *)
180
181fun GEN_REWRITE_TAC f rws = Tactic.CONV_TAC o GEN_REWRITE_CONV f rws;
182
183val PURE_REWRITE_TAC = GEN_REWRITE_TAC Conv.TOP_DEPTH_CONV empty_rewrites
184and
185PURE_ONCE_REWRITE_TAC = GEN_REWRITE_TAC Conv.ONCE_DEPTH_CONV empty_rewrites;
186
187fun REWRITE_TAC thl = GEN_REWRITE_TAC Conv.TOP_DEPTH_CONV (implicit_rewrites())
188                                      thl
189and ONCE_REWRITE_TAC thl =
190    GEN_REWRITE_TAC Conv.ONCE_DEPTH_CONV (implicit_rewrites()) thl;
191
192val rewrite_tac = REWRITE_TAC and once_rewrite_tac = ONCE_REWRITE_TAC
193
194
195(* Rewrite a goal with the help of its assumptions *)
196
197fun PURE_ASM_REWRITE_TAC thl :tactic =
198   Tactical.ASSUM_LIST (fn asl => PURE_REWRITE_TAC (asl @ thl))
199and ASM_REWRITE_TAC thl :tactic      =
200   Tactical.ASSUM_LIST (fn asl => REWRITE_TAC (asl @ thl))
201and PURE_ONCE_ASM_REWRITE_TAC thl :tactic =
202   Tactical.ASSUM_LIST (fn asl => PURE_ONCE_REWRITE_TAC (asl @ thl))
203and ONCE_ASM_REWRITE_TAC thl :tactic      =
204   Tactical.ASSUM_LIST (fn asl => ONCE_REWRITE_TAC (asl @ thl));
205
206val asm_rewrite_tac = ASM_REWRITE_TAC
207val once_asm_rewrite_tac = ONCE_ASM_REWRITE_TAC
208
209(* Rewriting using equations that satisfy a predicate  *)
210fun FILTER_PURE_ASM_REWRITE_RULE f thl th =
211    PURE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th
212and FILTER_ASM_REWRITE_RULE f thl th =
213    REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th
214and FILTER_PURE_ONCE_ASM_REWRITE_RULE f thl th =
215    PURE_ONCE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th
216and FILTER_ONCE_ASM_REWRITE_RULE f thl th =
217    ONCE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th;;
218
219fun FILTER_PURE_ASM_REWRITE_TAC f thl =
220    Tactical.ASSUM_LIST
221          (fn asl => PURE_REWRITE_TAC ((filter (f o concl) asl)@thl))
222and FILTER_ASM_REWRITE_TAC f thl =
223    Tactical.ASSUM_LIST
224          (fn asl => REWRITE_TAC ((filter (f o concl) asl) @ thl))
225and FILTER_PURE_ONCE_ASM_REWRITE_TAC f thl =
226    Tactical.ASSUM_LIST
227         (fn asl => PURE_ONCE_REWRITE_TAC ((filter (f o concl) asl) @ thl))
228and FILTER_ONCE_ASM_REWRITE_TAC f thl =
229    Tactical.ASSUM_LIST
230          (fn asl => ONCE_REWRITE_TAC ((filter (f o concl) asl) @ thl));
231
232
233(*---------------------------------------------------------------------------*
234 * SUBST_MATCH (|-u=v) th   searches for an instance of u in                 *
235 * (the conclusion of) th and then substitutes the corresponding             *
236 * instance of v.                                                            *
237 *---------------------------------------------------------------------------*)
238
239fun SUBST_MATCH eqth th =
240  let val matchr = match_term (lhs(concl eqth))
241      fun find_match t =
242             matchr t              handle HOL_ERR _ =>
243             find_match(rator t)   handle HOL_ERR _ =>
244             find_match(rand t)    handle HOL_ERR _ =>
245             find_match(body t)
246      val (tm_inst,ty_inst) = find_match (concl th)
247  in
248     SUBS [INST tm_inst (INST_TYPE ty_inst eqth)] th
249  end
250  handle HOL_ERR _ => raise ERR "SUBST_MATCH" "";
251
252
253
254fun pp_rewrites rws =
255    let
256      open Portable smpp
257      val pp_thm = lift Parse.pp_thm
258      val thms = dest_rewrites rws
259      val thms' = flatten (map mk_rewrites thms)
260      val how_many = length thms'
261      val m =
262           block CONSISTENT 0 (
263             (if (how_many = 0) then add_string "<empty rule set>"
264              else
265                block INCONSISTENT 0 (
266                  pr_list pp_thm (add_string";" >> add_break(2,0)) thms'
267                )
268             ) >>
269             add_newline >>
270             add_string("Number of rewrite rules = "^Lib.int_to_string how_many) >>
271             add_newline
272           )
273    in
274      Parse.mlower m
275    end;
276
277end (* Rewrite *)
278