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