1structure bitstringLib :> bitstringLib = 2struct 3 4open HolKernel Parse boolLib bossLib; 5open listLib wordsLib bitstringSyntax 6 7structure Parse = struct 8 open Parse 9 val (Type, Term) = parse_from_grammars bitstringTheory.bitstring_grammars 10end 11open Parse 12 13val _ = Lib.with_flag (Feedback.emit_MESG, false) bossLib.srw_ss () 14 15val ERR = Feedback.mk_HOL_ERR "bitstringLib" 16 17(* ------------------------------------------------------------------------- *) 18 19fun Cases_on_v2w t = 20 Q.ISPEC_THEN t Tactic.FULL_STRUCT_CASES_TAC 21 bitstringTheory.ranged_bitstring_nchotomy 22 23(* ------------------------------------------------------------------------- *) 24 25fun qm l = Feedback.trace ("metis", 0) (metisLib.METIS_TAC l) 26 27fun new_def s x = Definition.new_definition (s ^ "_def", boolSyntax.mk_eq x) 28 29val list_length = List.length o fst o listSyntax.dest_list 30 31val get_const = 32 fst o Term.dest_comb o boolSyntax.lhs o Thm.concl o Drule.SPEC_ALL 33 34fun change_compset_conv c e = Conv.CHANGED_CONV (computeLib.compset_conv c e) 35 36local 37 fun bit n = 38 if Arbnum.mod2 n = Arbnum.one then boolSyntax.T else boolSyntax.F 39 fun btfy (a, n) = 40 if n = Arbnum.zero then a else btfy (bit n :: a, Arbnum.div2 n) 41in 42 fun bitify_num w n = 43 let 44 val l = btfy ([], n) 45 val s = w - List.length l 46 val () = ignore (0 <= s orelse raise ERR "bitify_num" "too big") 47 in 48 List.tabulate (s, K boolSyntax.F) @ l 49 end 50end 51 52fun check P err thm = 53 (P (boolSyntax.rhs (Thm.concl thm)) orelse raise err; thm) 54 55(* ------------------------------------------------------------------------- *) 56 57(* Evaluate ``fixwidth n [...]`` *) 58 59local 60 open bitstringTheory 61 val cnv = 62 Conv.REWR_CONV (REWRITE_RULE [zero_extend_def] fixwidth_def) 63 THENC change_compset_conv (listSimps.list_compset()) 64 [computeLib.Defs [combinTheory.K_THM], 65 computeLib.Convs 66 [(``fcp$dimindex:'a itself -> num``, 1, wordsLib.SIZES_CONV)]] 67in 68 fun FIX_CONV tm = Lib.with_exn cnv tm (ERR "FIX_CONV" "") 69end 70 71(* ------------------------------------------------------------------------- *) 72 73(* Canonicalize ``v2w [...]``. 74 75 For example: 76 77 FIX_v2w_CONV ``v2w [T;T] : word4`` 78 val it = |- v2w [T; T] = v2w [F; F; T; T]: thm 79*) 80 81local 82 val cnv = Conv.REWR_CONV (GSYM bitstringTheory.v2w_fixwidth) 83 THENC Conv.RAND_CONV FIX_CONV 84in 85 fun FIX_v2w_CONV tm = 86 let 87 val (l, n) = bitstringSyntax.dest_v2w tm 88 val sz = Arbnum.toInt (fcpSyntax.dest_numeric_type n) 89 in 90 if sz = list_length l 91 then raise Conv.UNCHANGED 92 else Lib.with_exn cnv tm (ERR "FIX_v2w_CONV" "") 93 end 94end 95 96(* ------------------------------------------------------------------------- *) 97 98(* Evaluate ``v2n [...]`` *) 99 100local 101 open arithmeticTheory numeralTheory 102 103 val l2n_2_compute = prove( 104 ���(l2n 2 [] = 0) /\ 105 (!l. l2n 2 (0::l) = 2 * l2n 2 l) /\ 106 (!l. l2n 2 (1::l) = 2 * l2n 2 l + 1)���, 107 simp [numposrepTheory.l2n_def]) 108 109 val l2n_2_numeric = prove( 110 ���(l2n 2 [] = ZERO) /\ 111 (!l. l2n 2 (0::l) = numeral$iDUB (l2n 2 l)) /\ 112 (!l. l2n 2 (1::l) = BIT1 (l2n 2 l))���, 113 qm 114 [l2n_2_compute, ALT_ZERO, ONE, ADD_ASSOC, BIT1, TIMES2, MULT_COMM, iDUB]) 115 116 val num_from_bin_list_compute = prove( 117 ���(num_from_bin_list [] = 0) /\ 118 (!l. num_from_bin_list (0::l) = NUMERAL (l2n 2 (0::l))) /\ 119 (!l. num_from_bin_list (1::l) = NUMERAL (l2n 2 (1::l)))���, 120 simp [numposrepTheory.num_from_bin_list_def] >> qm [NUMERAL_DEF]) 121 122 val cnv = 123 Conv.REWR_CONV bitstringTheory.v2n_def 124 THENC Conv.RAND_CONV (PURE_REWRITE_CONV [bitstringTheory.bitify_def]) 125 THENC PURE_ONCE_REWRITE_CONV [num_from_bin_list_compute] 126 THENC Conv.TRY_CONV 127 (Conv.RAND_CONV (PURE_REWRITE_CONV [l2n_2_numeric, iDUB_removal]) 128 THENC Conv.TRY_CONV (Conv.REWR_CONV NORM_0)) 129in 130 fun v2n_CONV tm = 131 check numLib.is_numeral (ERR "v2n_CONV" "not ground") 132 (Lib.with_exn cnv tm (ERR "v2n_CONV" "")) 133end 134 135(* ------------------------------------------------------------------------- *) 136 137(* Convert ``v2w [...]`` to ``n2w n`` *) 138 139local 140 val v2w_n2w_thm = prove( 141 ���!l n. (v2n l = n) ==> (v2w l = n2w n : 'a word)���, 142 qm [bitstringTheory.ops_to_n2w]) 143in 144 fun v2w_n2w_CONV tm = 145 let 146 val (l, ty) = bitstringSyntax.dest_v2w tm 147 val thm = v2n_CONV (bitstringSyntax.mk_v2n l) 148 in 149 Drule.MATCH_MP (Thm.INST_TYPE [Type.alpha |-> ty] v2w_n2w_thm) thm 150 end 151 handle HOL_ERR {message = m, ...} => raise ERR "v2w_n2w_CONV" m 152end 153 154val v2w_n2w_ss = 155 simpLib.std_conv_ss 156 {name = "v2w_n2w", pats = [``v2w x: 'a word``], conv = v2w_n2w_CONV} 157 158(* ------------------------------------------------------------------------- *) 159 160(* Convert ``n2w n`` to ``v2w [...]`` *) 161 162fun n2w_v2w_CONV tm = 163 let 164 val (n, ty) = wordsSyntax.dest_n2w tm 165 val b = 166 bitify_num (fcpSyntax.dest_int_numeric_type ty) (numLib.dest_numeral n) 167 val l = listSyntax.mk_list (b, Type.bool) 168 in 169 Thm.SYM (v2w_n2w_CONV (bitstringSyntax.mk_v2w (l, ty))) 170 end 171 handle HOL_ERR {message = m, ...} => raise ERR "n2w_v2w_CONV" m 172 173(* ------------------------------------------------------------------------- *) 174 175(* Bitify expressions of the form: 176 ``v2w [...] = n2w n`` 177 ``n2w n = v2w [...]`` 178 ``v2w [...] = v2w [...]`` 179 for ground n. 180 181 For example: 182 183 v2w_eq_CONV ``v2w [T;b] = 3w : word4`` 184 val it = |- (v2w [T; b] = 3w) <=> b: thm 185 186 v2w_eq_CONV ``v2w [T;b] = v2w [c;d] : word4`` 187 val it = (v2w [T; b] = v2w [c; d]) <=> c /\ (b <=> d): thm 188*) 189 190fun v2w_eq_CONV tm = 191 let 192 val (l, r) = boolSyntax.dest_eq tm 193 val c = Conv.RHS_CONV (Conv.REWR_CONV (n2w_v2w_CONV r)) 194 handle HOL_ERR _ => 195 Conv.LHS_CONV (Conv.REWR_CONV (n2w_v2w_CONV l)) 196 handle HOL_ERR _ => 197 Conv.ALL_CONV 198 in 199 (c THENC Conv.REWR_CONV bitstringTheory.v2w_11 200 THENC Conv.BINOP_CONV 201 (Conv.RATOR_CONV (Conv.RAND_CONV wordsLib.SIZES_CONV) 202 THENC FIX_CONV) 203 THENC listLib.LIST_EQ_SIMP_CONV) tm 204 end 205 handle HOL_ERR {message = m, ...} => raise ERR "v2w_eq_n2w_CONV" m 206 207(* ------------------------------------------------------------------------- *) 208 209(* Equality check for any ground term combinations of ``v2w [..]`` and 210 ``n2w n``. Should be faster than using the above. 211*) 212 213local 214 fun is_bool tm = Teq tm orelse Feq tm 215 val cnv = 216 Conv.REWR_CONV bitstringTheory.v2w_11 217 THENC change_compset_conv (listSimps.list_compset()) 218 [computeLib.Defs 219 [bitstringTheory.v2w_fixwidth, 220 bitstringTheory.fixwidth, 221 bitstringTheory.extend_def], 222 computeLib.Convs 223 [(``fcp$dimindex:'a itself -> num``, 1, wordsLib.SIZES_CONV)]] 224in 225 fun word_eq_CONV tm = 226 let 227 val (l, r) = boolSyntax.dest_eq tm 228 in 229 if bitstringSyntax.is_v2w l 230 then if bitstringSyntax.is_v2w r 231 then check is_bool (ERR "word_eq_CONV" "not ground") 232 (cnv tm) 233 else (Conv.LHS_CONV v2w_n2w_CONV 234 THENC wordsLib.word_EQ_CONV) tm 235 else if bitstringSyntax.is_v2w r 236 then (Conv.RHS_CONV v2w_n2w_CONV THENC wordsLib.word_EQ_CONV) tm 237 else wordsLib.word_EQ_CONV tm 238 end 239 handle HOL_ERR {message = m, ...} => raise ERR "word_eq_CONV" m 240end 241 242(* ------------------------------------------------------------------------- *) 243 244(* Simplify expressions of the form ``(h >< l) (v2w [...])``. 245 246 For example: 247 248 extract_v2w_CONV ``(3 >< 1) (v2w [a;b;c;d;e] : word5) : word3`` 249 |- (3 >< 1) (v2w [a; b; c; d; e]) = v2w [b; c; d]: thm 250*) 251 252local 253 val extract_v2w_cor = prove( 254 ���!h l v. 255 (LENGTH v <= dimindex(:'a)) /\ (dimindex(:'b) = SUC h - l) /\ 256 dimindex(:'b) <= dimindex(:'a) ==> 257 ((h >< l) (v2w v : 'a word) : 'b word = 258 v2w (fixwidth (dimindex(:'b)) (shiftr v l)))���, 259 qm [bitstringTheory.extract_v2w, bitstringTheory.field_def]) 260 val shiftr_CONV = 261 Conv.REWR_CONV bitstringTheory.shiftr_def 262 THENC Conv.CHANGED_CONV (computeLib.CBV_CONV (listSimps.list_compset())) 263in 264 fun extract_v2w_CONV tm = 265 let 266 val (h, l, w, ty1) = wordsSyntax.dest_word_extract tm 267 val (v, ty2) = bitstringSyntax.dest_v2w w 268 val dim_a = fcpSyntax.mk_dimindex ty2 269 val dim_a_thm = wordsLib.SIZES_CONV dim_a 270 val dim_b = fcpSyntax.mk_dimindex ty1 271 val dim_b_thm = wordsLib.SIZES_CONV dim_b 272 val len_thm = 273 numSyntax.mk_leq (listSyntax.mk_length v, dim_a) 274 |> (Conv.FORK_CONV (listLib.LENGTH_CONV, Conv.REWR_CONV dim_a_thm) 275 THENC numLib.REDUCE_CONV) 276 |> Drule.EQT_ELIM 277 val width_thm = 278 boolSyntax.mk_eq (dim_b, numSyntax.mk_minus (numSyntax.mk_suc h, l)) 279 |> (Conv.LHS_CONV (Conv.REWR_CONV dim_b_thm) 280 THENC numLib.REDUCE_CONV) 281 |> Drule.EQT_ELIM 282 val le_thm = 283 numSyntax.mk_leq (dim_b, dim_a) 284 |> (Conv.FORK_CONV (Conv.REWR_CONV dim_b_thm, 285 Conv.REWR_CONV dim_a_thm) 286 THENC numLib.REDUCE_CONV) 287 |> Drule.EQT_ELIM 288 val thm = Drule.MATCH_MP extract_v2w_cor 289 (Drule.LIST_CONJ [len_thm, width_thm, le_thm]) 290 in 291 (Conv.REWR_CONV thm 292 THENC Conv.RAND_CONV (Conv.RAND_CONV shiftr_CONV) 293 THENC Conv.RAND_CONV FIX_CONV) tm 294 end 295 handle HOL_ERR {message = m, ...} => raise ERR "extract_v2w_CONV" m 296end 297 298(* ------------------------------------------------------------------------- *) 299 300(* Simplify expressions of the form 301 302 ``word_bit i (v2w [...])`` and ``v2w [...] ' i``. 303 304 For example: 305 306 word_bit_CONV ``word_bit 1 (v2w [a;b;c;d;e] : word5)`` 307 |- word_bit 1 (v2w [a; b; c; d; e]) <=> d: thm 308*) 309 310local 311 open numeralTheory listTheory 312 val word_bit_last_shiftr = 313 REWRITE_RULE [bitstringTheory.shiftr_def] 314 bitstringTheory.word_bit_last_shiftr 315 val cnv = change_compset_conv (computeLib.bool_compset()) 316 [computeLib.Defs 317 [numeral_distrib, numeral_suc, numeral_iisuc, numeral_sub, 318 numeral_lt, iSUB_THM, iDUB_removal, 319 LENGTH, TAKE_compute, NULL_DEF, LAST_compute]] 320in 321 fun word_bit_CONV tm = 322 let 323 val ((i, t), c) = 324 case Lib.total wordsSyntax.dest_word_bit tm of 325 SOME x => (x, ALL_CONV) 326 | NONE => (Lib.swap (fcpSyntax.dest_fcp_index tm), 327 wordsLib.WORD_BIT_INDEX_CONV false) 328 val ty = wordsSyntax.dim_of t 329 val lt_thm = 330 numSyntax.mk_less (i, fcpSyntax.mk_dimindex ty) 331 |> (Conv.RAND_CONV wordsLib.SIZES_CONV 332 THENC numLib.REDUCE_CONV) 333 |> Drule.EQT_ELIM 334 val thm = Drule.MATCH_MP word_bit_last_shiftr lt_thm 335 in 336 (c THENC Conv.REWR_CONV thm THENC cnv) tm 337 end 338 handle HOL_ERR {message = m, ...} => raise ERR "word_bit_CONV" m 339end 340 341(* ------------------------------------------------------------------------- *) 342 343local 344 fun mk_boolify i = 345 let 346 fun mk_n j = 347 Term.mk_var ("n" ^ (if j + 1 = i then "" else Int.toString (i-1-j)), 348 numSyntax.num) 349 val ns = List.tabulate (i, mk_n) 350 val t = pairSyntax.list_mk_pair (List.map numSyntax.mk_odd ns) 351 fun mk_p j = (List.nth (ns, j), List.nth (ns, j + 1)) 352 val ps = List.tabulate (i - 1, mk_p) 353 in 354 (List.last ns, 355 List.foldl (fn ((a, b), t) => 356 boolSyntax.mk_let (Term.mk_abs (a, t), numSyntax.mk_div2 b)) 357 t ps) 358 end 359 360 fun BOOLIFY_v2w_CONV thm = RAND_CONV FIX_v2w_CONV THENC REWR_CONV thm 361 362 fun add_boolify_v2w thm = 363 let 364 val c = thm |> Drule.SPEC_ALL |> Thm.concl 365 |> boolSyntax.lhs |> Term.dest_comb |> fst 366 in 367 computeLib.add_conv (c, 1, BOOLIFY_v2w_CONV thm) 368 end 369 370 val rw = SRW_TAC [boolSimps.LET_ss] 371 372 fun Cases_on_v2w q = 373 Q.ISPEC_THEN q STRUCT_CASES_TAC bitstringTheory.ranged_bitstring_nchotomy 374 375 fun boolify_n2w_tac thm = 376 Tactic.STRIP_TAC 377 THEN Rewrite.PURE_REWRITE_TAC 378 (thm :: [wordsTheory.word_bit_n2w, bitTheory.BIT_def, 379 bitTheory.BITS_def]) 380 THEN Tactic.CONV_TAC (Conv.LHS_CONV (Conv.DEPTH_CONV wordsLib.SIZES_CONV)) 381 THEN Tactic.CONV_TAC (Conv.RHS_CONV (Conv.DEPTH_CONV pairLib.let_CONV)) 382 THEN Rewrite.PURE_REWRITE_TAC [pairTheory.CLOSED_PAIR_EQ] 383 THEN Tactical.REPEAT Tactic.CONJ_TAC 384 THEN Rewrite.PURE_REWRITE_TAC 385 [bitTheory.MOD_2EXP_def, bitTheory.ODD_MOD2_LEM, 386 numeral_bitTheory.DIV_2EXP] 387 THEN computeLib.EVAL_TAC 388 389 fun boolify_v2w_tac thm = 390 Tactical.REPEAT Tactic.STRIP_TAC 391 THEN Rewrite.PURE_REWRITE_TAC [thm, bitstringTheory.bit_v2w] 392 THEN computeLib.EVAL_TAC 393 394 fun boolify_bitify_tac x l = 395 Tactic.STRIP_TAC THEN pairLib.PairCases_on [HOLPP.ANTIQUOTE x] 396 THEN rw l 397 398 fun bitify_boolify_tac l = 399 SRW_TAC [fcpLib.FCP_ss, boolSimps.LET_ss] (l @ 400 [wordsTheory.word_bit, bitstringTheory.bit_v2w, 401 bitstringTheory.testbit]) 402 THEN Tactical.POP_ASSUM (fn th => Tactic.STRIP_ASSUME_TAC 403 (Conv.CONV_RULE wordsLib.LESS_CONV th)) 404 THEN Tactical.POP_ASSUM Tactic.SUBST1_TAC 405 THEN computeLib.EVAL_TAC 406in 407 fun define_bit_bool_maps (bitify_lhs, boolify_lhs) i = 408 let 409 val ty = wordsSyntax.mk_int_word_type i 410 val tyi = wordsSyntax.dest_word_type ty 411 val w = Term.mk_var ("w", ty) 412 fun mk_bit j = wordsSyntax.mk_word_bit (numSyntax.term_of_int (i-1-j), w) 413 val boolify_rhs = pairSyntax.list_mk_pair (List.tabulate (i, mk_bit)) 414 val f = Term.mk_var (boolify_lhs, Type.--> (ty, Term.type_of boolify_rhs)) 415 val boolify_def = new_def boolify_lhs (Term.mk_comb (f, w), boolify_rhs) 416 val boolify_c = get_const boolify_def 417 fun mk_b j = Term.mk_var ("b" ^ Int.toString (i-1-j), Type.bool) 418 val bs = List.tabulate (i, mk_b) 419 val btuple = pairSyntax.list_mk_pair bs 420 val blist = listSyntax.mk_list (bs, Type.bool) 421 val bitify_rhs = bitstringSyntax.mk_v2w (blist, tyi) 422 val f = Term.mk_var (bitify_lhs, 423 Type.--> (Term.type_of btuple, Term.type_of bitify_rhs)) 424 val bitify_def = new_def bitify_lhs (Term.mk_comb (f, btuple), bitify_rhs) 425 val bitify_c = get_const bitify_def 426 val (n, boolify_n2w_rhs) = mk_boolify i 427 val boolify_n2w_lhs = 428 Term.mk_comb (boolify_c, wordsSyntax.mk_n2w (n, tyi)) 429 val boolify_n2w_goal = 430 boolSyntax.mk_forall (n, 431 boolSyntax.mk_eq (boolify_n2w_lhs, boolify_n2w_rhs)) 432 val boolify_n2w_thm = 433 Tactical.store_thm(boolify_lhs ^ "_n2w", boolify_n2w_goal, 434 boolify_n2w_tac boolify_def) 435 val boolify_v2w_goal = 436 boolSyntax.list_mk_forall (bs, 437 boolSyntax.mk_eq (Term.mk_comb (boolify_c, bitify_rhs), btuple)) 438 val boolify_v2w_thm = 439 Tactical.store_thm(boolify_lhs ^ "_v2w", boolify_v2w_goal, 440 boolify_v2w_tac boolify_def) 441 val x = Term.mk_var ("x", Term.type_of btuple) 442 val boolify_bitify_goal = 443 boolSyntax.mk_forall (x, 444 boolSyntax.mk_eq 445 (Term.mk_comb (boolify_c, Term.mk_comb (bitify_c, x)), x)) 446 val boolify_bitify_thm = 447 Tactical.store_thm(boolify_lhs ^ bitify_lhs, boolify_bitify_goal, 448 boolify_bitify_tac x [bitify_def, boolify_v2w_thm]) 449 val bitify_boolify_goal = 450 boolSyntax.mk_forall (w, 451 boolSyntax.mk_eq 452 (Term.mk_comb (bitify_c, Term.mk_comb (boolify_c, w)), w)) 453 val bitify_boolify_thm = 454 Tactical.store_thm(bitify_lhs ^ boolify_lhs, bitify_boolify_goal, 455 bitify_boolify_tac [bitify_def, boolify_def]) 456 val () = computeLib.add_funs [boolify_n2w_thm, bitify_def] 457 val () = computeLib.add_convs 458 [(boolify_c, 1, BOOLIFY_v2w_CONV boolify_v2w_thm)] 459 in 460 (bitify_def, boolify_def) 461 end 462end 463 464type bitify_boolify = 465 { bitify_def : thm, 466 bitify_tm : term, 467 mk_bitify : term -> term, 468 dest_bitify : term -> term, 469 is_bitify : term -> bool, 470 boolify_def : thm, 471 boolify_tm : term, 472 mk_boolify : term -> term, 473 dest_boolify : term -> term, 474 is_boolify : term -> bool } 475 476local 477 fun findDef s = 478 case s |> DB.find 479 |> List.partition (fn ((_, s2), (_, DB.Def)) => s2 = s 480 | _ => false) 481 |> fst of 482 [((thy, _), (thm, _))] => SOME (thy, thm) 483 | _ => NONE 484in 485 fun bitify_boolify i = 486 let 487 val n = Int.toString i 488 val bitify = "bitify" ^ n 489 val boolify = "boolify" ^ n 490 fun f s = findDef (s ^ "_def") 491 val ((thy1, bitify_def), (thy2, boolify_def)) = 492 case (f bitify, f boolify) of 493 (SOME x, SOME y) => (x, y) 494 | _ => 495 let 496 val () = Feedback.HOL_MESG 497 ("Defining " ^ n ^ "-bit bitify/boolify maps") 498 val thy = Theory.current_theory () 499 val (thm1, thm2) = define_bit_bool_maps (bitify, boolify) i 500 in 501 ((thy, thm1), (thy, thm2)) 502 end 503 val (bitify_tm, mk_bitify, dest_bitify, is_bitify) = 504 HolKernel.syntax_fns1 thy1 bitify 505 val (boolify_tm, mk_boolify, dest_boolify, is_boolify) = 506 HolKernel.syntax_fns1 thy2 boolify 507 in 508 { bitify_def = bitify_def, 509 bitify_tm = bitify_tm, 510 mk_bitify = mk_bitify, 511 dest_bitify = dest_bitify, 512 is_bitify = is_bitify, 513 boolify_def = boolify_def, 514 boolify_tm = boolify_tm, 515 mk_boolify = mk_boolify, 516 dest_boolify = dest_boolify, 517 is_boolify = is_boolify } : bitify_boolify 518 end 519end 520 521(* ------------------------------------------------------------------------- *) 522 523local 524 open bitstringTheory 525 val thms = 526 [ 527 numLib.SUC_RULE extend_def, boolify_def, bitify_def, n2v_def, v2n_def, 528 s2v_def, v2s_def, shiftl_def, shiftr_def, field_def, rotate_def, w2v_def, 529 rev_count_list_def, modify_def, field_insert_def, add_def, bitwise_def, 530 bnot_def, bor_def, band_def, bxor_def, bnor_def, bxnor_def, bnand_def, 531 replicate_def, testbit, ops_to_v2w, ops_to_n2w, fixwidth, extend, v2w_11, 532 bit_v2w, w2n_v2w, w2v_v2w, w2w_v2w, sw2sw_v2w, word_index_v2w, 533 word_lsl_v2w, word_lsr_v2w, word_asr_v2w, word_ror_v2w, word_1comp_v2w, 534 word_and_v2w, word_or_v2w, word_xor_v2w, word_nand_v2w, word_nor_v2w, 535 word_xnor_v2w, word_lsb_v2w, word_msb_v2w, word_reverse_v2w, 536 word_modify_v2w, word_bits_v2w, word_extract_v2w, word_slice_v2w, 537 word_join_v2w_rwt, word_concat_v2w_rwt, word_reduce_v2w, reduce_and_v2w, 538 reduce_or_v2w 539 ] 540 fun name_ty tm = 541 let 542 val {Thy = thy, Name = name, ...} = 543 Term.dest_thy_const tm 544 handle e as HOL_ERR _ => (print_term tm; raise e) 545 in 546 (thy ^ "$" ^ name, 547 List.length (fst (boolSyntax.strip_fun (Term.type_of tm)))) 548 end 549 val get_function = 550 name_ty o fst o boolSyntax.strip_comb o boolSyntax.lhs o 551 snd o boolSyntax.strip_forall o List.hd o boolSyntax.strip_conj o 552 snd o boolSyntax.strip_forall o Thm.concl 553 val s = 554 thms |> List.map get_function 555 |> List.filter 556 (fn (s, _) => 557 not (Lib.mem s ["bitstring$modify", "bitstring$bitwise", 558 "words$word_modify", "words$word_reduce"])) 559 |> Redblackmap.fromList String.compare 560 fun is_ground_arg tm = 561 Lib.can bitstringSyntax.bitlist_of_term tm orelse 562 Lib.can (bitstringSyntax.bitlist_of_term o fst o 563 bitstringSyntax.dest_v2w) tm orelse 564 listSyntax.is_nil tm orelse 565 wordsSyntax.is_word_literal tm andalso Lib.can wordsSyntax.size_of tm orelse 566 numSyntax.is_numeral tm orelse 567 Term.same_const boolSyntax.T tm orelse 568 Term.same_const boolSyntax.F tm orelse 569 stringSyntax.is_string_literal tm 570 fun is_ground tm = 571 case Lib.total boolSyntax.dest_strip_comb tm of 572 SOME (name, l) => 573 (case Redblackmap.peek (s, name) of 574 SOME i => List.length l = i andalso List.all is_ground_arg l 575 | NONE => false) 576 | NONE => false 577in 578 val add_bitstring_compset = computeLib.add_thms thms 579 val cnv = change_compset_conv (wordsLib.words_compset()) 580 [computeLib.Extenders [add_bitstring_compset]] 581 fun BITSTRING_GROUND_CONV tm = 582 if is_ground tm then cnv tm 583 else raise ERR "BITSTRING_GROUND_CONV" "Term not ground" 584 val BITSTRING_GROUND_ss = 585 simpLib.std_conv_ss 586 {name = "BITSTRING_GROUND", pats = [], conv = BITSTRING_GROUND_CONV} 587end 588 589(* ------------------------------------------------------------------------- *) 590 591end 592