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