1structure updateLib :> updateLib = 2struct 3 4open HolKernel Parse boolLib bossLib 5open wordsLib updateSyntax; 6 7structure Parse = struct 8 open Parse 9 val (Type,Term) = parse_from_grammars updateTheory.update_grammars 10end 11open Parse 12 13val ERR = Feedback.mk_HOL_ERR "updateLib" 14 15(* ----------------------------------------------------------------------- 16 COND_CONV 17 Simpler version of Conv.COND_CONV (doesn't do alpha-conversion) 18 ----------------------------------------------------------------------- *) 19 20local 21 val thm = Drule.SPEC_ALL boolTheory.COND_CLAUSES 22 val cond_cnv1 = Conv.REWR_CONV (Thm.CONJUNCT1 thm) 23 val cond_cnv2 = Conv.REWR_CONV (Thm.CONJUNCT2 thm) 24 val cond_cnv3 = Conv.REWR_CONV boolTheory.COND_ID 25in 26 val COND_CONV = cond_cnv1 ORELSEC cond_cnv2 ORELSEC cond_cnv3 27end 28 29(* ----------------------------------------------------------------------- 30 NOT_CONV 31 Simpler version of Boolconv.NOT_CONV (doesn't do double negation) 32 ----------------------------------------------------------------------- *) 33 34local 35 val (_, thm1, thm2) = 36 Lib.triple_of_list (Drule.CONJUNCTS boolTheory.NOT_CLAUSES) 37in 38 fun NOT_CONV tm = 39 let 40 val b = Lib.with_exn boolSyntax.dest_neg tm (ERR "NOT_CONV" "") 41 in 42 if b = boolSyntax.T 43 then thm1 44 else if b = boolSyntax.F 45 then thm2 46 else raise ERR "NOT_CONV" "" 47 end 48end 49 50(* ------------------------------------------------------------------------ 51 UPDATE_APPLY_CONV cnv 52 53 Evaluate terms of the from ``((a =+ b) f) c`` using "cnv" to decide 54 whether or not ``a = c``. 55 56 Example: 57 58 UPDATE_APPLY_CONV numLib.REDUCE_CONV ``(1 =+ "a") ((2 =+ "b") f) 2`` 59 |- (1 =+ "a") ((2 =+ "b") f) 2 = "b" 60 ------------------------------------------------------------------------- *) 61 62local 63 val cnv1 = Conv.REWR_CONV (Thm.CONJUNCT1 combinTheory.UPDATE_APPLY) 64 val cnv2 = Conv.REWR_CONV combinTheory.APPLY_UPDATE_THM 65in 66 fun UPDATE_APPLY_CONV eqconv = 67 let 68 fun eqconv' tm = 69 eqconv tm 70 handle Conv.UNCHANGED => (Conv.SYM_CONV THENC eqconv) tm 71 val cnv3 = 72 cnv2 73 THENC Conv.RATOR_CONV (Conv.RATOR_CONV (Conv.RAND_CONV eqconv')) 74 THENC COND_CONV 75 fun APPLY_CONV tm = 76 let 77 val (u, v) = Term.dest_comb tm 78 val ((a, _), _) = 79 Lib.with_exn combinSyntax.dest_update_comb u Conv.UNCHANGED 80 in 81 if a = v 82 then cnv1 tm 83 else (cnv3 THENC Conv.TRY_CONV APPLY_CONV) tm 84 end 85 in 86 APPLY_CONV 87 end 88end 89 90(* ------------------------------------------------------------------------ 91 LIST_UPDATE_INTRO_CONV 92 93 Convert repeated applications of =+ into an application of LIST_UPDATE. 94 95 Examples: 96 97 LIST_UPDATE_INTRO_CONV ``(1 =+ "a") ((2 =+ "b") f)`` 98 |- (1 =+ "a") ((2 =+ "b") f) = LIST_UPDATE [(1,"a"); (2,"b")] f 99 100 LIST_UPDATE_INTRO_CONV ``(1 =+ "a") o (2 =+ "b")`` 101 |- |- (1 =+ "a") o (2 =+ "b") = LIST_UPDATE [(1,"a"); (2,"b")] 102 ------------------------------------------------------------------------ *) 103 104val LIST_UPDATE_INTRO_CONV = 105 PURE_REWRITE_CONV 106 [updateTheory.LIST_UPDATE_THMS, listTheory.APPEND, listTheory.SNOC] 107 108(* ------------------------------------------------------------------------ 109 LIST_UPDATE_ELIM_CONV 110 111 Convert applications of LIST_UPDATE into repeated applications of =+. 112 113 Examples: 114 115 LIST_UPDATE_ELIM_CONV ``LIST_UPDATE [(1,"a"); (2,"b")] f`` 116 |- LIST_UPDATE [(1,"a"); (2,"b")] f = (1 =+ "a") ((2 =+ "b") f) 117 118 LIST_UPDATE_ELIM_CONV ``LIST_UPDATE [(1,"a"); (2,"b")]`` 119 |- LIST_UPDATE [(1,"a"); (2,"b")] = (1 =+ "a") o (2 =+ "b") 120 ------------------------------------------------------------------------ *) 121 122local 123 val (thm1, thm2) = Drule.CONJ_PAIR updateTheory.LIST_UPDATE_def 124 val thm3 = 125 PURE_REWRITE_RULE [pairTheory.FST, pairTheory.SND] (Q.SPEC `(a, b)` thm2) 126 val thm4 = Thm.CONJUNCT2 (Drule.SPEC_ALL combinTheory.I_o_ID) 127 val cnv1 = Conv.REWR_CONV thm3 128 val cnv2 = Conv.REWR_CONV thm1 129 val cnv3 = Conv.REWR_CONV thm2 130 val cnv4 = Conv.ONCE_DEPTH_CONV (Conv.REWR_CONV thm4) 131 val cnv5 = Conv.TOP_DEPTH_CONV (Conv.REWR_CONV combinTheory.o_THM) 132 fun expand_conv0 tm = 133 ((cnv1 THENC (Conv.RAND_CONV expand_conv0)) 134 ORELSEC cnv2 135 ORELSEC (cnv3 THENC (Conv.RAND_CONV expand_conv0))) tm 136 val expand_conv = expand_conv0 THENC cnv4 137in 138 fun LIST_UPDATE_ELIM_CONV tm = 139 let 140 val (f, x) = Term.dest_comb tm 141 val is_upd = Term.same_const updateSyntax.list_update_tm f 142 val _ = is_upd orelse updateSyntax.is_list_update f orelse 143 raise ERR "LIST_UPDATE_ELIM_CONV" "" 144 in 145 if is_upd 146 then expand_conv tm 147 else (Conv.RATOR_CONV expand_conv THENC cnv5) tm 148 end 149end 150 151(* ----------------------------------------------------------------------- 152 Some syntax functions 153 ----------------------------------------------------------------------- *) 154 155local 156 val is_ground = List.null o Term.free_vars 157in 158 fun is_ground_update tm = 159 case Lib.total combinSyntax.dest_update tm of 160 SOME (l, _) => is_ground l 161 | NONE => false 162 fun is_ground_list_update tm = 163 case Lib.total updateSyntax.strip_list_update tm of 164 SOME l => Lib.all (is_ground o fst) l 165 | NONE => false 166end 167 168local 169 fun is_ground_upd tm = is_ground_update tm orelse is_ground_list_update tm 170in 171 fun is_o_expr tm = 172 is_ground_upd tm orelse 173 case Lib.total combinSyntax.dest_o tm of 174 SOME (l, r) => 175 is_ground_upd l andalso is_o_expr r orelse 176 is_o_expr l andalso is_ground_upd r 177 | NONE => false 178 fun is_base tm = 179 case Lib.total Term.dest_comb tm of 180 SOME (l, _) => not (is_ground_upd l) 181 | NONE => true 182end 183 184fun is_c_expr tm = 185 case Lib.total Term.dest_comb tm of 186 SOME (l, r) => is_o_expr l andalso (is_base r orelse is_c_expr r) 187 | NONE => false 188 189fun is_update_expr tm = is_o_expr tm orelse is_c_expr tm 190 191(* ----------------------------------------------------------------------- 192 UNCHANGED_CONV cnv 193 194 Raise Conv.UNCHANGED if conversion "cnv" produces result |- t = t' where 195 t and t' are alpha-equivalent, or if an exception is raised. 196 ----------------------------------------------------------------------- *) 197 198fun UNCHANGED_CONV (conv: conv) tm = 199 let 200 val th = Lib.with_exn conv tm Conv.UNCHANGED 201 val (l, r) = boolSyntax.dest_eq (Thm.concl th) 202 in 203 if Term.aconv l r then raise Conv.UNCHANGED else th 204 end 205 206(* ----------------------------------------------------------------------- 207 FILTER_CONV cnv 208 209 Evaluation for ``FILTER P l``. Faster than version in listLib. 210 ----------------------------------------------------------------------- *) 211 212local 213 val cnv1 = Conv.REWR_CONV (Thm.CONJUNCT1 listTheory.FILTER) 214 val cnv2 = Conv.REWR_CONV (Thm.CONJUNCT2 listTheory.FILTER) 215in 216 fun FILTER_CONV cnv = 217 let 218 fun filter_conv tm = 219 ((cnv2 220 THENC Conv.RATOR_CONV (Conv.RATOR_CONV (Conv.RAND_CONV cnv)) 221 THENC COND_CONV 222 THENC (fn tm => if listSyntax.is_cons tm 223 then Conv.RAND_CONV filter_conv tm 224 else filter_conv tm)) ORELSEC cnv1) tm 225 in 226 filter_conv 227 end 228end 229 230(* ----------------------------------------------------------------------- 231 OVERRIDE_CONV cnv 232 233 Evaluation for ``OVERRIDE l``. 234 ----------------------------------------------------------------------- *) 235 236local 237 val cnv1 = Conv.REWR_CONV (Thm.CONJUNCT1 updateTheory.OVERRIDE_def) 238 val cnv2 = Conv.REWR_CONV (Thm.CONJUNCT2 updateTheory.OVERRIDE_def) 239 val cnv3 = Conv.REWR_CONV pairTheory.FST 240in 241 fun OVERRIDE_CONV cnv = 242 let 243 val cnv' = PairRules.PBETA_CONV 244 THENC Conv.RAND_CONV (Conv.RHS_CONV cnv3 THENC cnv) 245 THENC NOT_CONV 246 val fcnv = FILTER_CONV cnv' 247 fun override_conv tm = 248 ((cnv2 249 THENC Conv.RAND_CONV 250 (Conv.RAND_CONV 251 (Conv.RATOR_CONV 252 (Conv.RAND_CONV 253 (Conv.ABS_CONV 254 (Conv.RAND_CONV (Conv.LHS_CONV cnv3)))) 255 THENC fcnv) 256 THENC override_conv)) ORELSEC cnv1) tm 257 in 258 override_conv 259 end 260end 261 262(* ----------------------------------------------------------------------- 263 OVERRIDE_UPDATES_CONV ty cnv 264 265 Eliminate redundant (overwritten) updates for functions of type "ty" using 266 conversion "cnv" to evaluate equality. 267 268 Examples: 269 270 OVERRIDE_UPDATES_CONV ``:word32 -> string`` wordsLib.word_EQ_CONV 271 ``(1w:word32 =+ "a") ((3w =+ "b") ((2w =+ "c") ((3w =+ "c") f)))`` 272 |- (1w =+ "a") ((3w =+ "b") ((2w =+ "c") ((3w =+ "c") f))) = 273 (1w =+ "a") ((3w =+ "b") ((2w =+ "c") f)) 274 275 OVERRIDE_UPDATES_CONV ``:word32 -> string`` wordsLib.word_EQ_CONV 276 ``(1w:word32 =+ "a") o (3w =+ "b") o (2w =+ "c") o (3w =+ "c")`` 277 |- (1w =+ "a") o (3w =+ "b") o (2w =+ "c") o (3w =+ "c") = 278 (1w =+ "a") o (3w =+ "b") o (2w =+ "c") 279 ----------------------------------------------------------------------- *) 280 281local 282 val cnv1 = Conv.REWR_CONV updateTheory.LIST_UPDATE_OVERRIDE 283in 284 fun OVERRIDE_UPDATES_CONV ty cnv = 285 let 286 val ocnv = cnv1 THENC Conv.RAND_CONV (OVERRIDE_CONV cnv) 287 val ok1 = Lib.can (Type.match_type ty) 288 val ok2 = Lib.can (Type.match_type (ty --> ty)) 289 in 290 fn tm => 291 let 292 val tm_ty = Term.type_of tm 293 val c_form = ok1 tm_ty andalso is_c_expr tm 294 val _ = c_form orelse ok2 tm_ty andalso is_o_expr tm 295 orelse raise ERR "OVERRIDE_UPDATES_CONV" 296 "Not expected type/form" 297 in 298 UNCHANGED_CONV 299 (LIST_UPDATE_INTRO_CONV 300 THENC (if c_form then Conv.RATOR_CONV else Lib.I) ocnv 301 THENC LIST_UPDATE_ELIM_CONV) tm 302 end 303 end 304end 305 306(* ----------------------------------------------------------------------- 307 SORT_UPDATES_CONV ord cmp cnv 308 309 Sort repeated applications of =+ using an ordering function "ord". 310 The ordering can be based on the function's range as well as its domain, 311 i.e. (2 =+ 1) can be "less-than" (1 =+ 2). The ordering is evaluated 312 using the compset "cmp" and conversion "cnv" is used to test equality. 313 314 Examples: 315 316 SORT_UPDATES_CONV ``\(a, x:'a) (b, y:'a). a <+ b`` 317 (wordsLib.words_compset()) wordsLib.word_EQ_CONV 318 ``(1w:word32 =+ "a") ((3w =+ "b") ((2w =+ "c") ((3w =+ "c") f)))`` 319 |- (1w =+ "a") ((3w =+ "b") ((2w =+ "c") ((3w =+ "c") f))) = 320 (1w =+ "a") ((2w =+ "c") ((3w =+ "b") f)) 321 322 SORT_UPDATES_CONV ``\(a, x:'a) (b, y:'a). a <+ b`` 323 (wordsLib.words_compset()) wordsLib.word_EQ_CONV 324 ``(1w:word32 =+ "a") o (3w =+ "b") o (2w =+ "c") o (3w =+ "c")`` 325 |- (1w =+ "a") o (3w =+ "b") o (2w =+ "c") o (3w =+ "c") = 326 (1w =+ "a") o (2w =+ "c") o (3w =+ "b") 327 ----------------------------------------------------------------------- *) 328 329fun SORT_UPDATES_CONV ord cmp cnv = 330 let 331 val () = computeLib.add_thms 332 [pairTheory.CURRY_DEF, pairTheory.UNCURRY_DEF, 333 pairTheory.PAIR_EQ, pairTheory.FST, pairTheory.SND, 334 listTheory.APPEND, combinTheory.o_THM, sortingTheory.PART_DEF, 335 REWRITE_RULE [sortingTheory.PARTITION_DEF] 336 sortingTheory.QSORT_DEF] cmp 337 val SORT_CONV = computeLib.CBV_CONV cmp 338 val thm = Drule.ISPEC ord updateTheory.LIST_UPDATE_SORT_OVERRIDE 339 val cnv1 = Conv.REWR_CONV thm 340 val cnv2 = OVERRIDE_CONV cnv 341 val cnv3 = cnv1 THENC Conv.RAND_CONV (Conv.RAND_CONV cnv2 THENC SORT_CONV) 342 val (ty1, ty2) = 343 ord |> Term.type_of |> Type.dom_rng |> fst |> pairSyntax.dest_prod 344 val ty3 = ty1 --> ty2 345 in 346 fn tm => 347 let 348 val ty = Term.type_of tm 349 val c_form = Lib.can (Type.match_type ty3) ty andalso is_c_expr tm 350 val _ = 351 c_form orelse 352 Lib.can (Type.match_type (ty3 --> ty3)) ty andalso is_o_expr tm 353 orelse raise ERR "SORT_UPDATES_CONV" "Not expected type/form" 354 in 355 UNCHANGED_CONV 356 (LIST_UPDATE_INTRO_CONV 357 THENC (if c_form then Conv.RATOR_CONV else Lib.I) cnv3 358 THENC LIST_UPDATE_ELIM_CONV) tm 359 end 360 end 361 362(* ----------------------------------------------------------------------- 363 SORT_UPDATES_MAPTO_CONV f ord cnv 364 365 An alternative interface to SORT_UPDATES_CONV. The ordering is 366 ``\x y. ord (f x) (f y)``. 367 368 Examples: 369 370 SORT_UPDATES_MAPTO_CONV ``FST : 'a word # 'b -> 'a word`` 371 (wordsLib.words_compset()) wordsLib.WORD_EVAL_CONV 372 ``(1w:word32 =+ "a") ((3w =+ "b") ((2w =+ "c") ((3w =+ "c") f)))`` 373 |- (1w =+ "a") ((3w =+ "b") ((2w =+ "c") ((3w =+ "c") f))) = 374 (1w =+ "a") ((2w =+ "c") ((3w =+ "b") f)) 375 376 SORT_UPDATES_MAPTO_CONV ``FST : 'a word # 'b -> 'a word`` 377 wordsSyntax.word_lo_tm wordsLib.WORD_EVAL_CONV 378 ``(1w:word32 =+ "a") o (3w =+ "b") o (2w =+ "c") o (3w =+ "c")`` 379 |- (1w =+ "a") o (3w =+ "b") o (2w =+ "c") o (3w =+ "c") = 380 (1w =+ "a") o (2w =+ "c") o (3w =+ "b") 381 ----------------------------------------------------------------------- *) 382 383fun SORT_UPDATES_MAPTO_CONV f ord = 384 let 385 val (uty, oty) = Type.dom_rng (Term.type_of f) 386 val _ = Type.match_type (Term.type_of ord) (oty --> oty --> Type.bool) 387 val x = Term.mk_var ("x", uty) 388 val y = Term.mk_var ("y", uty) 389 val f_x = Term.mk_comb (f, x) 390 val f_y = Term.mk_comb (f, y) 391 val f_ord = Term.list_mk_abs 392 ([x,y], boolSyntax.list_mk_icomb (ord, [f_x, f_y])) 393 in 394 SORT_UPDATES_CONV f_ord 395 end 396 397(* ----------------------------------------------------------------------- 398 SORT_NUM_UPDATES_CONV 399 400 Sort sequences of updates for maps of type ``:num -> 'a``. 401 402 Example: 403 404 SORT_NUM_UPDATES_CONV 405 ``(1 =+ "a") ((3 =+ "b") ((2 =+ "c") ((3 =+ "c") f)))`` 406 |- (1 =+ "a") ((3 =+ "b") ((2 =+ "c") ((3 =+ "c") f))) = 407 (1 =+ "a") ((2 =+ "c") ((3 =+ "b") f)) 408 ----------------------------------------------------------------------- *) 409 410val SORT_NUM_UPDATES_CONV = 411 let 412 val fty = pairSyntax.mk_prod (numSyntax.num, Type.alpha) --> numSyntax.num 413 val f = Term.mk_thy_const {Ty = fty, Thy = "pair", Name = "FST"} 414 in 415 SORT_UPDATES_MAPTO_CONV 416 f numSyntax.less_tm (reduceLib.num_compset()) numLib.REDUCE_CONV 417 end 418 419(* ----------------------------------------------------------------------- 420 SORT_WORD_UPDATES_CONV ty 421 422 Sort sequences of updates for maps of type ``:ty word -> 'a``. 423 424 Example: 425 426 SORT_WORD_UPDATES_CONV ``:32`` 427 ``(1w:word32 =+ "a") ((3w =+ "b") ((2w =+ "c") ((3w =+ "c") f)))`` 428 |- (1 =+ "a") ((3 =+ "b") ((2 =+ "c") ((3 =+ "c") f))) = 429 (1 =+ "a") ((2 =+ "c") ((3 =+ "b") f)) 430 ----------------------------------------------------------------------- *) 431 432fun SORT_WORD_UPDATES_CONV ty = 433 let 434 val dimword = 435 Lib.with_exn wordsLib.SIZES_CONV (wordsSyntax.mk_dimword ty) 436 (ERR "SORT_WORD_UPDATES_CONV" 437 "Cannot compute size or word type") 438 val word_lo = 439 PURE_REWRITE_RULE [dimword] 440 (Thm.INST_TYPE [Type.alpha |-> ty] wordsTheory.word_lo_n2w) 441 val cmp = reduceLib.num_compset() 442 val () = computeLib.add_thms 443 [numLib.SUC_RULE numeral_bitTheory.MOD_2EXP_EQ, word_lo, 444 numLib.SUC_RULE numeral_bitTheory.MOD_2EXP_MAX] cmp 445 val wty = wordsSyntax.mk_word_type ty 446 val fty = pairSyntax.mk_prod (wty, Type.alpha) --> wty 447 val f = Term.mk_thy_const {Ty = fty, Thy = "pair", Name = "FST"} 448 in 449 SORT_UPDATES_MAPTO_CONV f wordsSyntax.word_lo_tm cmp wordsLib.word_EQ_CONV 450 end 451 452(* ----------------------------------------------------------------------- 453 SORT_ENUM_UPDATES_CONV ty 454 455 Sort sequences of updates for maps of type ``:ty -> 'a`` where ``:ty`` 456 if an enumerated type. 457 458 Example: 459 460 val () = Hol_datatype `enum = One | Two | Three` 461 SORT_ENUM_UPDATES_CONV ``:enum`` 462 ``(One =+ "a") ((Three =+ "b") ((Two =+ "c") ((Three =+ "c") f)))`` 463 |- (One =+ "a") ((Three =+ "b") ((Two =+ "c") ((Three =+ "c") f))) = 464 (One =+ "a") ((Two =+ "c") ((Three =+ "b") f)) 465 ----------------------------------------------------------------------- *) 466 467fun SORT_ENUM_UPDATES_CONV ty = 468 let 469 val {Thy, Args, Tyop} = Type.dest_thy_type ty 470 val _ = List.null Args orelse 471 raise ERR "SORT_ENUM_UPDATES_CONV" "Not an enumerated type" 472 val ty2num = Tyop ^ "2num" 473 val ty2num_tm = Term.prim_mk_const {Thy = Thy, Name = ty2num} 474 val ty2num_11 = DB.fetch Thy (ty2num ^ "_11") 475 val ty2num_thm = DB.fetch Thy (ty2num ^ "_thm") 476 val cmp = reduceLib.num_compset() 477 val () = computeLib.add_thms [GSYM ty2num_11, ty2num_thm] cmp 478 val cnv = computeLib.CBV_CONV cmp 479 in 480 SORT_UPDATES_MAPTO_CONV 481 ``(^ty2num_tm o FST) : ^(ty_antiq ty) # 'a -> num`` numSyntax.less_tm 482 cmp cnv 483 end 484 485end 486