1structure Import :> Import = 2struct 3 4open HolKernel boolLib bossLib 5open state_transformerTheory bitstringLib stringLib binary_ieeeSyntax 6 fp32Syntax fp64Syntax machine_ieeeSyntax intSyntax integer_wordSyntax 7 bitstringSyntax state_transformerSyntax 8 9val ERR = mk_HOL_ERR "Import" 10 11(* ------------------------------------------------------------------------ *) 12 13local 14 val boolify_vals = ref (Redblackset.empty Int.compare) 15 val type_names = ref [] 16 val const_names = ref [] 17 fun decl s = "val " ^ s 18 val typ = "{Thy: string, T: string list, C: string list, N: int list}" 19 val B = PP.block PP.CONSISTENT 0 20in 21 fun log_boolify n = boolify_vals := Redblackset.add (!boolify_vals, n) 22 fun log_type s = type_names := s :: !type_names 23 fun log_constant s = const_names := (s ^ "_def") :: !const_names 24 fun start thy = 25 (type_names := [] 26 ; const_names := [] 27 ; new_theory thy) 28 fun finish i = 29 (Theory.adjoin_to_theory { 30 sig_ps = 31 SOME (fn _ => B[PP.add_string (decl "inventory:"), 32 PP.add_break (1, 2), 33 PP.add_string typ]), 34 struct_ps = 35 SOME (fn _ => 36 let 37 val name = Lib.quote (Theory.current_theory ()) 38 fun bl f s l = B [ 39 PP.add_break (1, 0), 40 PP.add_string (s ^ " ["), 41 PP.block PP.INCONSISTENT 0 ( 42 PP.pr_list (PP.add_string o f) 43 [PP.add_string ",", PP.add_break (1, 0)] 44 l 45 ), 46 PP.add_string "]" 47 ] 48 in 49 B [ 50 PP.add_string (decl "inventory = {"), 51 PP.add_break (0, 2), 52 B [ 53 PP.add_string ("Thy = " ^ name ^ ","), 54 bl Lib.quote "T =" (!type_names), 55 PP.add_string (","), 56 bl Lib.quote "C =" (!const_names), 57 PP.add_string (","), 58 bl Int.toString "N =" 59 (Redblackset.listItems (!boolify_vals)), 60 PP.add_string "}" 61 ], 62 PP.add_newline 63 ] 64 end)} 65 ; Feedback.set_trace "TheoryPP.include_docs" i 66 ; export_theory () 67 ; type_names := [] 68 ; const_names := []) 69end 70 71(* ------------------------------------------------------------------------ *) 72 73val Ty = ParseDatatype.pretypeToType 74fun typeName ty = String.extract (Parse.type_to_string ty, 1, NONE) 75 76(* Constant type *) 77local 78 fun mkTy (t, n) = ParseDatatype.dTyop {Thy = t, Tyop = n, Args = []} 79 fun mkListTy a = 80 ParseDatatype.dTyop {Thy = SOME "list", Tyop = "list", Args = [a]} 81in 82 val uTy = mkTy (SOME "one", "one") 83 val iTy = mkTy (SOME "integer", "int") 84 val nTy = mkTy (SOME "num", "num") 85 val bTy = mkTy (SOME "min", "bool") 86 val rTy = mkTy (SOME "binary_ieee", "rounding") 87 val oTy = mkTy (SOME "binary_ieee", "float_compare") 88 val fTy = mkTy (SOME "binary_ieee", "flags") 89 val cTy = mkTy (SOME "string", "char") 90 val sTy = mkListTy cTy 91 val vTy = mkListTy bTy 92 fun CTy n = mkTy (NONE, n) 93end 94 95(* Variable type *) 96fun VTy s = ParseDatatype.dVartype ("'" ^ s) 97 98(* Fixed-width bit-vector type *) 99val FTy = ParseDatatype.dAQ o wordsSyntax.mk_int_word_type 100 101val F1 = FTy 1 102val F4 = FTy 4 103val F8 = FTy 8 104val F16 = FTy 16 105val F32 = FTy 32 106val F64 = FTy 64 107 108(* N-bit type *) 109fun typevar s = Type.mk_vartype ("'" ^ s) 110fun BTy s = ParseDatatype.dAQ (wordsSyntax.mk_word_type (typevar s)) 111 112(* Arrow type *) 113fun ATy (t1, t2) = 114 ParseDatatype.dTyop {Thy = SOME "min", Tyop = "fun", Args = [t1, t2]} 115 116(* Product type *) 117fun PTy (t1, t2) = 118 ParseDatatype.dTyop {Thy = SOME "pair", Tyop = "prod", Args = [t1, t2]} 119 120(* Set type *) 121fun STy t = ATy (t, bTy) 122 123(* List type *) 124fun LTy t = 125 ParseDatatype.dTyop {Thy = SOME "list", Tyop = "list", Args = [t]} 126 127(* Option type *) 128fun OTy t = 129 ParseDatatype.dTyop {Thy = SOME "option", Tyop = "option", Args = [t]} 130 131(* ------------------------------------------------------------------------ *) 132 133val myDatatype = 134 let 135 val w = String.size "Defined type: \"" 136 in 137 (Lib.with_flag 138 (Feedback.MESG_to_string, 139 fn s => (log_type 140 (String.extract (s, w, SOME (String.size s - w - 1))) 141 ; s ^ "\n")) o 142 Feedback.trace ("Theory.save_thm_reporting", 0)) 143 Datatype.astHol_datatype 144 end 145 146val l3_big_record_size = 28 147 148(* Record type *) 149fun Record (n, l) = 150 ( if l3_big_record_size < List.length l 151 then Feedback.HOL_WARNING "Import" "Record" 152 ("Defining big record type; size " ^ Int.toString (List.length l)) 153 else () 154 ; myDatatype [(n, ParseDatatype.Record l)] 155 ) 156 157fun NoBigRecord (n, l) = 158 myDatatype [(n, ParseDatatype.Record l)] 159 160(* Algebraic type *) 161val Construct = myDatatype o List.map (I ## ParseDatatype.Constructors) 162 163(* ------------------------------------------------------------------------ *) 164 165fun mk_local_const (n, ty) = 166 Term.mk_thy_const {Ty = ty, Thy = Theory.current_theory (), Name = n} 167 168fun mk_ieee_const n = Term.prim_mk_const {Name = n, Thy = "binary_ieee"} 169 170(* Literals *) 171 172(* Unit *) 173val LU = oneSyntax.one_tm 174(* Bool *) 175val LT = boolSyntax.T 176val LF = boolSyntax.F 177(* Integer *) 178fun LI i = intSyntax.term_of_int (Arbint.fromLargeInt i) 179(* Natural *) 180fun LN n = numSyntax.mk_numeral (Arbnum.fromLargeInt n) 181(* Char *) 182fun LSC c = stringSyntax.fromMLchar c 183(* String *) 184fun LS s = stringSyntax.fromMLstring s 185(* Bitstring *) 186fun LV v = bitstringSyntax.bitstring_of_binstring v 187(* Fixed-width *) 188fun LW (i, w) = wordsSyntax.mk_wordi (Arbnum.fromLargeInt i, w) 189(* N-bit *) 190fun LY (i, n) = wordsSyntax.mk_n2w (LN i, typevar n) 191(* Enumerated *) 192fun LC (c, ty) = mk_local_const (c, Ty ty) 193(* NONE *) 194fun LO ty = optionSyntax.mk_none (Ty ty) 195(* Empty set *) 196fun LE ty = pred_setSyntax.mk_empty (Ty ty) 197(* Empty list (Nil) *) 198fun LNL ty = listSyntax.mk_nil (Ty ty) 199(* UNKNOWN *) 200fun LX ty = boolSyntax.mk_arb (Ty ty) 201 202val NEGINF32 = fp32Syntax.fp_neginf_tm 203val POSINF32 = fp32Syntax.fp_posinf_tm 204val NEGINF64 = fp64Syntax.fp_neginf_tm 205val POSINF64 = fp64Syntax.fp_posinf_tm 206 207val NEGZERO32 = fp32Syntax.fp_negzero_tm 208val POSZERO32 = fp32Syntax.fp_poszero_tm 209val NEGZERO64 = fp64Syntax.fp_negzero_tm 210val POSZERO64 = fp64Syntax.fp_poszero_tm 211 212val NEGMIN32 = fp32Syntax.fp_negmin_tm 213val POSMIN32 = fp32Syntax.fp_posmin_tm 214val NEGMIN64 = fp64Syntax.fp_negmin_tm 215val POSMIN64 = fp64Syntax.fp_posmin_tm 216 217val NEGMAX32 = fp32Syntax.fp_bottom_tm 218val POSMAX32 = fp32Syntax.fp_top_tm 219val NEGMAX64 = fp64Syntax.fp_bottom_tm 220val POSMAX64 = fp64Syntax.fp_top_tm 221 222val QUIETNAN32 = LW (0x7FC00000, 32) 223val SIGNALNAN32 = LW (0x7F800001, 32) 224val QUIETNAN64 = LW (0x7FF8000000000000, 64) 225val SIGNALNAN64 = LW (0x7FF0000000000001, 64) 226 227(* ------------------------------------------------------------------------ *) 228 229(* Function call *) 230 231fun Call (f, ty, tm) = 232 let 233 val typ = Type.--> (Term.type_of tm, Ty ty) 234 val vc = mk_local_const (f, typ) 235 handle HOL_ERR {origin_function = "mk_thy_const", ...} => 236 Term.mk_var (f, typ) (* for recursion *) 237 in 238 Term.mk_comb (vc, tm) 239 end 240 241(* Constants *) 242 243fun Const (c, ty) = 244 let 245 val typ = Ty ty 246 in 247 mk_local_const (c, typ) 248 handle HOL_ERR {origin_function = "mk_thy_const", ...} => 249 Term.mk_var (c, typ) (* for recursion *) 250 end 251 252(* Variables *) 253 254local 255 val anon = ref 0 256 fun anonSuffix () = (if !anon = 0 then "" else Int.toString (!anon)) 257 before anon := !anon + 1 258in 259 fun resetAnon () = anon := 0 260 fun AVar ty = Term.mk_var ("_" ^ anonSuffix(), Ty ty) 261end 262 263fun Var (v, ty) = Term.mk_var (v, Ty ty) 264 265fun uVar v = Term.mk_var (v, oneSyntax.one_ty) 266fun bVar v = Term.mk_var (v, Type.bool) 267fun nVar v = Term.mk_var (v, numSyntax.num) 268fun iVar v = Term.mk_var (v, intSyntax.int_ty) 269fun sVar v = Term.mk_var (v, stringSyntax.string_ty) 270fun vVar v = Term.mk_var (v, bitstringSyntax.bitstring_ty) 271 272(* Closure *) 273 274val Close = pairSyntax.mk_pabs 275 276(* Application *) 277 278val Apply = Term.mk_comb 279 280(* Tuple *) 281 282fun TP l = 283 let 284 val (f, lst) = Lib.front_last l 285 in 286 List.foldr pairSyntax.mk_pair lst f 287 end 288 289(* Map update *) 290 291fun Fupd (m, i, e) = Term.mk_comb (combinSyntax.mk_update (i, e), m) 292 293(* Cases *) 294 295(* val CS = TypeBase.mk_case *) 296 297fun CS (x, cs) = 298 Term.beta_conv (Term.mk_comb 299 (Lib.with_flag (Feedback.emit_MESG, false) 300 (TypeBase.mk_pattern_fn) cs, x)) 301 before resetAnon () 302 303(* Let-expression *) 304 305fun Let (v,e,b) = 306 boolSyntax.mk_let (Close (v, b), e) 307 handle HOL_ERR {origin_function = "mk_pabs", ...} => CS (e, [(v, b)]) 308 309(* Set of list *) 310 311val SL = 312 fn [] => raise ERR "SL" "empty" 313 | l as (h::_) => pred_setSyntax.prim_mk_set (l, Term.type_of h) 314 315(* List of list *) 316 317val LL = 318 fn [] => raise ERR "LL" "empty" 319 | l as (h::_) => listSyntax.mk_list (l, Term.type_of h) 320 321local 322 fun gen_mk_list (l, tm) = List.foldr listSyntax.mk_cons tm l 323in 324 val LLC = 325 fn ([], tm) => 326 let 327 val ty = fst (pairSyntax.dest_prod (Term.type_of tm)) 328 val cons = Term.inst [Type.alpha |-> ty] listSyntax.cons_tm 329 in 330 pairSyntax.mk_uncurry (cons, tm) 331 end 332 | ltm => gen_mk_list ltm 333end 334 335(* Record constructor (may not work for really big records) *) 336 337local 338 fun strip_fun_type ty = 339 let 340 fun strip (a, ty) = 341 case Lib.total Type.dom_rng ty of 342 SOME (ty1, ty2) => strip (ty1::a, ty2) 343 | NONE => (List.rev a, ty) 344 in 345 strip ([], ty) 346 end 347 fun get_cons ty = 348 let 349 val tm = Lib.singleton_of_list (TypeBase.constructors_of ty) 350 in 351 (fst (strip_fun_type (Term.type_of tm)), tm) 352 end 353 fun split l = Lib.split_after (List.length l) 354in 355 fun Rec (ty, l) = 356 let 357 val (tys, tm) = get_cons (Ty ty) 358 in 359 if List.length l = List.length tys 360 then Term.list_mk_comb (tm, l) 361 else let 362 val cs = List.map get_cons tys 363 val (tms, rst) = 364 List.foldl 365 (fn ((tys, f), (a, r)) => 366 let 367 val (args, rst) = split tys r 368 in 369 (Term.list_mk_comb (f, args) :: a, rst) 370 end) ([], l) cs 371 in 372 List.null rst orelse raise ERR "Rec" "too many arguments"; 373 Term.list_mk_comb (tm, List.rev tms) 374 end 375 end 376end 377 378(* Record destructor *) 379 380fun flag s tm = Term.mk_comb (mk_ieee_const ("flags_" ^ s), tm) 381val ieee_underflow_before = ref false 382fun underflow () = 383 "Underflow_" ^ (if !ieee_underflow_before then "Before" else "After") ^ 384 "Rounding" 385 386fun Dest (f, ty, tm) = 387 case f of 388 "DivideByZero" => flag "DivideByZero" tm 389 | "InvalidOp" => flag "InvalidOp" tm 390 | "Overflow" => flag "Overflow" tm 391 | "Precision" => flag "Precision" tm 392 | "Underflow" => flag (underflow()) tm 393 | _ => Call (typeName (Term.type_of tm) ^ "_" ^ f, ty, tm) 394 395(* Record update *) 396 397fun smart_dest_pair tm = 398 case Lib.total pairSyntax.dest_pair tm of 399 SOME p => p 400 | NONE => (pairSyntax.mk_fst tm, pairSyntax.mk_snd tm) 401 402fun Rupd (f, tm) = 403 let 404 val (rty, fty) = pairSyntax.dest_prod (Term.type_of tm) 405 val typ = Type.--> (Type.--> (fty, fty), Type.--> (rty, rty)) 406 val name = typeName rty ^ "_" ^ f ^ "_fupd" 407 val fupd = case f of 408 "DivideByZero" => mk_ieee_const name 409 | "InvalidOp" => mk_ieee_const name 410 | "Overflow" => mk_ieee_const name 411 | "Precision" => mk_ieee_const name 412 | "Underflow" => 413 mk_ieee_const ("flags_" ^ underflow() ^ "_fupd") 414 | _ => mk_local_const (name, typ) 415 val (x, d) = smart_dest_pair tm 416 in 417 Term.list_mk_comb (fupd, [combinSyntax.mk_K_1 (d, Term.type_of d), x]) 418 end 419 420(* Boolify constructor *) 421 422val bit_bool = 423 Feedback.trace ("Theory.save_thm_reporting", 0) bitstringLib.bitify_boolify 424 425fun BL (i, tm) = 426 let 427 val () = log_boolify i 428 val { mk_boolify, ... } = bit_bool i 429 in 430 mk_boolify tm 431 end 432 433(* If-then-else *) 434 435fun ITE (i, t, e) = boolSyntax.mk_cond (i, t, e) 436 437fun ITB (l, e) = List.foldr (fn ((b, t), e) => ITE (b, t, e)) e l 438 439(* Sub-word extract *) 440 441fun EX (x, h, l, ty) = 442 let 443 val typ = Ty ty 444 in 445 if typ = bitstringSyntax.bitstring_ty 446 then bitstringSyntax.mk_field (h, l, x) 447 else wordsSyntax.mk_word_extract (h, l, x, wordsSyntax.dest_word_type typ) 448 end 449 450(* Bit-field insert *) 451 452fun BFI (t as (_, _, x, _)) = 453 if Term.type_of x = bitstringSyntax.bitstring_ty 454 then bitstringSyntax.mk_field_insert t 455 else wordsSyntax.mk_bit_field_insert t 456 457(* Concatenation *) 458 459fun CC [] = raise ERR "CC" "empty" 460 | CC l = 461 let 462 val (f, lst) = Lib.front_last l 463 val mk = if listSyntax.is_list_type (Term.type_of lst) 464 then listSyntax.mk_append 465 else wordsSyntax.mk_word_concat 466 in 467 List.foldr mk lst f 468 end 469 470(* Word Replicate *) 471 472fun REP (w, n, ty) = 473 wordsSyntax.mk_word_replicate_ty (n, w, wordsSyntax.dest_word_type (Ty ty)) 474 475(* Equality *) 476 477fun EQ (x, y) = boolSyntax.mk_eq (x, y) 478 479(* Monad operations *) 480 481(* Return/Unit *) 482 483val MU = state_transformerSyntax.mk_unit o (I ## Ty) 484 485(* Bind *) 486 487val MB = state_transformerSyntax.mk_bind 488 489(* Read *) 490 491val MR = state_transformerSyntax.mk_read 492 493(* Write *) 494 495val MW = state_transformerSyntax.mk_write 496 497(* Narrow *) 498 499val MN = state_transformerSyntax.mk_narrow 500 501(* Widen *) 502 503val MD = state_transformerSyntax.mk_widen o (I ## Ty) 504 505(* For-loop *) 506 507val For = HolKernel.mk_monop state_transformerSyntax.for_tm 508 509val Foreach = HolKernel.mk_monop state_transformerSyntax.foreach_tm 510 511(* ------------------------------------------------------------------------ *) 512 513(* Primitive binary and unary operations *) 514 515datatype monop = 516 Abs 517 | BNot 518 | Bin 519 | Cardinality 520 | Cast of ParseDatatype.pretype 521 | Dec 522 | Difference 523 | Drop 524 | Element 525 | FP32To64 526 | FP64To32 527 | FP64To32_ 528 | FPAbs of int 529 | FPAdd of int 530 | FPAdd_ of int 531 | FPCmp of int 532 | FPDiv of int 533 | FPDiv_ of int 534 | FPEq of int 535 | FPFromInt of int 536 | FPGe of int 537 | FPGt of int 538 | FPIsIntegral of int 539 | FPIsFinite of int 540 | FPIsNan of int 541 | FPIsNormal of int 542 | FPIsSignallingNan of int 543 | FPIsSubnormal of int 544 | FPIsZero of int 545 | FPLe of int 546 | FPLt of int 547 | FPMul of int 548 | FPMul_ of int 549 | FPMulAdd of int 550 | FPMulAdd_ of int 551 | FPMulSub of int 552 | FPMulSub_ of int 553 | FPNeg of int 554 | FPRoundToIntegral of int 555 | FPSqrt of int 556 | FPSqrt_ of int 557 | FPSub of int 558 | FPSub_ of int 559 | FPToInt of int 560 | Flat 561 | Fst 562 | Head 563 | Hex 564 | IndexOf 565 | Intersect 566 | IsAlpha 567 | IsAlphaNum 568 | IsDigit 569 | IsHexDigit 570 | IsLower 571 | IsMember 572 | IsSome 573 | IsSpace 574 | IsSubset 575 | IsUpper 576 | K1 of ParseDatatype.pretype 577 | Length 578 | Log 579 | Max 580 | Min 581 | Msb 582 | Neg 583 | Not 584 | PadLeft 585 | PadRight 586 | QuotRem 587 | Remove 588 | RemoveExcept 589 | RemoveDuplicates 590 | Rev 591 | SE of ParseDatatype.pretype 592 | Size 593 | Smax 594 | Smin 595 | Snd 596 | SofL 597 | Some 598 | Tail 599 | Take 600 | ToLower 601 | ToUpper 602 | Union 603 | Update 604 | ValOf 605 606datatype binop = 607 Add 608 | And 609 | Asr 610 | BAnd 611 | BOr 612 | BXor 613 | Bit 614 | Div 615 | Exp 616 | Fld 617 | Ge 618 | Gt 619 | In 620 | Insert 621 | Le 622 | Lsl 623 | Lsr 624 | Lt 625 | Mod 626 | Mul 627 | Or 628 | Quot 629 | Rem 630 | Rep 631 | Rol 632 | Ror 633 | SDiv 634 | SMod 635 | Splitl 636 | Splitr 637 | Sub 638 | Tok 639 | Uge 640 | Ugt 641 | Ule 642 | Ult 643 644local 645 val m = 646 ref (Redblackmap.mkDict String.compare : (string, term) Redblackmap.dict) 647in 648 fun string2enum ty = 649 let 650 val name = fst (Type.dest_type ty) 651 in 652 case Redblackmap.peek (!m, name) of 653 SOME tm => tm 654 | NONE => 655 let 656 val tm = ty 657 |> stringLib.Define_string2enum 658 |> Thm.concl 659 |> boolSyntax.dest_forall 660 |> snd 661 |> boolSyntax.lhs 662 |> boolSyntax.rator 663 in 664 m := Redblackmap.insert (!m, name, tm) 665 ; tm 666 end 667 end 668end 669 670local 671 val m = 672 ref (Redblackmap.mkDict String.compare : (string, term) Redblackmap.dict) 673in 674 fun enum2string ty = 675 let 676 val name = fst (Type.dest_type ty) 677 in 678 case Redblackmap.peek (!m, name) of 679 SOME tm => tm 680 | NONE => 681 let 682 val tm = ty 683 |> stringLib.Define_enum2string 684 |> Thm.concl 685 |> boolSyntax.strip_conj 686 |> hd 687 |> boolSyntax.lhs 688 |> boolSyntax.rator 689 in 690 m := Redblackmap.insert (!m, name, tm) 691 ; tm 692 end 693 end 694end 695 696local 697 local 698 val try_pbeta = 699 Lib.total (boolSyntax.rhs o Thm.concl o PairedLambda.PAIRED_BETA_CONV) 700 in 701 fun pbeta t = Option.getOpt (try_pbeta t, t) 702 fun mk_uncurry f_tm tm = pbeta (boolSyntax.mk_icomb (f_tm, tm)) 703 end 704 705 val one_tm = numSyntax.mk_numeral Arbnum.one 706 val t_tm = ``#"t"`` 707 val f_tm = ``#"f"`` 708 709 local 710 fun mk_w tm ty = wordsSyntax.mk_n2w (tm, wordsSyntax.dest_word_type ty) 711 in 712 val mk_word0 = mk_w numSyntax.zero_tm 713 val mk_word1 = mk_w one_tm 714 end 715 716 fun mk_sign_extend ty tm = 717 wordsSyntax.mk_sw2sw (tm, wordsSyntax.dest_word_type (Ty ty)) 718 719 local 720 val mk_map = Lib.curry boolSyntax.mk_icomb listSyntax.map_tm 721 val lower_tm = mk_map stringSyntax.tolower_tm 722 val upper_tm = mk_map stringSyntax.toupper_tm 723 in 724 fun mk_lower tm = Term.mk_comb (lower_tm, tm) 725 fun mk_upper tm = Term.mk_comb (upper_tm, tm) 726 end 727 728 val mk_pad_left = mk_uncurry ``\(a:'a, b, c). list$PAD_LEFT a b c`` 729 val mk_pad_right = mk_uncurry ``\(a:'a, b, c). list$PAD_RIGHT a b c`` 730 val mk_ismember = mk_uncurry ``\(x:'a, l). x IN list$LIST_TO_SET l`` 731 val mk_take = mk_uncurry ``\(x, l:'a list). list$TAKE x l`` 732 val mk_drop = mk_uncurry ``\(x, l:'a list). list$DROP x l`` 733 val mk_update = mk_uncurry ``\(e, x, l:'a list). list$LUPDATE e x l`` 734 val mk_element = mk_uncurry ``\(x, l:'a list). list$EL x l`` 735 val mk_indexof = mk_uncurry ``\(x:'a, l). list$INDEX_OF x l`` 736 val mk_remove = mk_uncurry ``\(l1:'a list, l2). 737 list$FILTER (\x. ~MEM x l1) l2`` 738 val mk_remove_e = mk_uncurry ``\(l1:'a list, l2). 739 list$FILTER (\x. MEM x l1) l2`` 740 741 val mk_word_min = mk_uncurry ``\(m:'a word, n). words$word_min m n`` 742 val mk_word_max = mk_uncurry ``\(m:'a word, n). words$word_max m n`` 743 val mk_word_smin = mk_uncurry ``\(m:'a word, n). words$word_smin m n`` 744 val mk_word_smax = mk_uncurry ``\(m:'a word, n). words$word_smax m n`` 745 746 val mk_num_min = mk_uncurry ``\(m, n). arithmetic$MIN m n`` 747 val mk_num_max = mk_uncurry ``\(m, n). arithmetic$MAX m n`` 748 val mk_int_min = mk_uncurry ``\(m, n). integer$int_min m n`` 749 val mk_int_max = mk_uncurry ``\(m, n). integer$int_max m n`` 750 751 val mk_union = mk_uncurry ``\(s1:'a set, s2). pred_set$UNION s1 s2`` 752 val mk_intersect = mk_uncurry ``\(s1:'a set, s2). pred_set$INTER s1 s2`` 753 val mk_difference = mk_uncurry ``\(s1:'a set, s2). pred_set$DIFF s1 s2`` 754 val mk_issubset = mk_uncurry ``\(s1:'a set, s2). pred_set$SUBSET s1 s2`` 755 756 val mk_quot_rem = 757 mk_uncurry ``\(m, n). (integer$int_quot m n, integer$int_rem m n)`` 758 759 fun enum2num ty = 760 Lib.with_exn mk_local_const 761 (typeName ty ^ "2num", Type.--> (ty, numLib.num)) 762 (ERR "pickCast" "enum2num not found") 763 764 fun num2enum ty = 765 Lib.with_exn mk_local_const 766 ("num2" ^ typeName ty, Type.--> (numLib.num, ty)) 767 (ERR "pickCast" "num2enum not found") 768 769 fun mk_from_enum ty = 770 SOME (Lib.curry Term.mk_comb (enum2num ty)) handle HOL_ERR _ => NONE 771 772 local 773 val mk_vars = 774 List.rev o snd o 775 List.foldl 776 (fn (ty, (c, l)) => 777 (Char.succ c, Term.mk_var (String.str c, ty) :: l)) (#"a", []) 778 in 779 fun mk_fp_op f = 780 let 781 val ftm = 782 case f of 783 FPCmp 32 => fp32Syntax.fp_compare_tm 784 | FPCmp 64 => fp64Syntax.fp_compare_tm 785 | FPEq 32 => fp32Syntax.fp_equal_tm 786 | FPEq 64 => fp64Syntax.fp_equal_tm 787 | FPLt 32 => fp32Syntax.fp_lessThan_tm 788 | FPLt 64 => fp64Syntax.fp_lessThan_tm 789 | FPLe 32 => fp32Syntax.fp_lessEqual_tm 790 | FPLe 64 => fp64Syntax.fp_lessEqual_tm 791 | FPGt 32 => fp32Syntax.fp_greaterThan_tm 792 | FPGt 64 => fp64Syntax.fp_greaterThan_tm 793 | FPGe 32 => fp32Syntax.fp_greaterEqual_tm 794 | FPGe 64 => fp64Syntax.fp_greaterEqual_tm 795 | FPRoundToIntegral 32 => fp32Syntax.fp_roundToIntegral_tm 796 | FPRoundToIntegral 64 => fp64Syntax.fp_roundToIntegral_tm 797 | FPSqrt 32 => fp32Syntax.fp_sqrt_tm 798 | FPSqrt 64 => fp64Syntax.fp_sqrt_tm 799 | FPSqrt_ 32 => fp32Syntax.fp_sqrt_with_flags_tm 800 | FPSqrt_ 64 => fp64Syntax.fp_sqrt_with_flags_tm 801 | FPToInt 32 => fp32Syntax.fp_to_int_tm 802 | FPToInt 64 => fp64Syntax.fp_to_int_tm 803 | FPFromInt 32 => fp32Syntax.int_to_fp_tm 804 | FPFromInt 64 => fp64Syntax.int_to_fp_tm 805 | FP64To32 => machine_ieeeSyntax.fp64_to_fp32_tm 806 | FP64To32_ => machine_ieeeSyntax.fp64_to_fp32_with_flags_tm 807 | FPAdd 32 => fp32Syntax.fp_add_tm 808 | FPAdd 64 => fp64Syntax.fp_add_tm 809 | FPAdd_ 32 => fp32Syntax.fp_add_with_flags_tm 810 | FPAdd_ 64 => fp64Syntax.fp_add_with_flags_tm 811 | FPDiv 32 => fp32Syntax.fp_div_tm 812 | FPDiv 64 => fp64Syntax.fp_div_tm 813 | FPDiv_ 32 => fp32Syntax.fp_div_with_flags_tm 814 | FPDiv_ 64 => fp64Syntax.fp_div_with_flags_tm 815 | FPMul 32 => fp32Syntax.fp_mul_tm 816 | FPMul 64 => fp64Syntax.fp_mul_tm 817 | FPMul_ 32 => fp32Syntax.fp_mul_with_flags_tm 818 | FPMul_ 64 => fp64Syntax.fp_mul_with_flags_tm 819 | FPSub 32 => fp32Syntax.fp_sub_tm 820 | FPSub 64 => fp64Syntax.fp_sub_tm 821 | FPSub_ 32 => fp32Syntax.fp_sub_with_flags_tm 822 | FPSub_ 64 => fp64Syntax.fp_sub_with_flags_tm 823 | FPMulAdd 32 => fp32Syntax.fp_mul_add_tm 824 | FPMulAdd 64 => fp64Syntax.fp_mul_add_tm 825 | FPMulAdd_ 32 => fp32Syntax.fp_mul_add_with_flags_tm 826 | FPMulAdd_ 64 => fp64Syntax.fp_mul_add_with_flags_tm 827 | FPMulSub 32 => fp32Syntax.fp_mul_sub_tm 828 | FPMulSub 64 => fp64Syntax.fp_mul_sub_tm 829 | FPMulSub_ 32 => fp32Syntax.fp_mul_sub_with_flags_tm 830 | FPMulSub_ 64 => fp64Syntax.fp_mul_sub_with_flags_tm 831 | _ => raise ERR "mk_fp_op" "" 832 val l = mk_vars (fst (HolKernel.strip_fun (Term.type_of ftm))) 833 val p = pairSyntax.list_mk_pair l 834 val ptm = pairSyntax.mk_pabs (p, Term.list_mk_comb (ftm, l)) 835 in 836 fn tm => pbeta (Term.mk_comb (ptm, tm)) 837 end 838 end 839 840 local 841 fun mk_test a b c d = boolSyntax.mk_cond (boolSyntax.mk_eq (a, b), c, d) 842 in 843 val string2bool = 844 let 845 val v = Term.mk_var ("s", stringSyntax.string_ty) 846 in 847 Term.mk_abs (v, 848 mk_test v (stringSyntax.fromMLstring "true") boolSyntax.T 849 (mk_test v (stringSyntax.fromMLstring "false") boolSyntax.F 850 (boolSyntax.mk_arb Type.bool))) 851 end 852 end 853 854 fun mk_from_bool (x as (tm, a, b)) = 855 if Teq tm then a 856 else if Feq tm then b 857 else boolSyntax.mk_cond x 858 859 fun mk_word_from_bool (tm, ty) = 860 if Teq tm then mk_word1 ty 861 else if Feq tm then mk_word0 ty 862 else bitstringSyntax.mk_v2w 863 (listSyntax.mk_list ([tm], Type.bool), 864 wordsSyntax.dest_word_type ty) 865 866 fun pickCast ty2 tm = 867 let 868 val ty1 = Term.type_of tm 869 val dw = wordsSyntax.dest_word_type 870 in 871 if wordsSyntax.is_word_type ty1 872 then if wordsSyntax.is_word_type ty2 873 then wordsSyntax.mk_w2w (tm, dw ty2) 874 else if ty2 = bitstringSyntax.bitstring_ty 875 then bitstringSyntax.mk_w2v tm 876 else if ty2 = numSyntax.num 877 then wordsSyntax.mk_w2n tm 878 else if ty2 = intSyntax.int_ty 879 then integer_wordSyntax.mk_w2i tm 880 else if ty2 = stringSyntax.string_ty 881 then wordsSyntax.mk_word_to_hex_string tm 882 else if ty2 = Type.bool 883 then boolSyntax.mk_neg (boolSyntax.mk_eq (tm, mk_word0 ty1)) 884 else if ty2 = stringSyntax.char_ty 885 then stringSyntax.mk_chr (wordsSyntax.mk_w2n tm) 886 else Term.mk_comb (num2enum ty2, wordsSyntax.mk_w2n tm) 887 else if ty1 = bitstringSyntax.bitstring_ty 888 then if wordsSyntax.is_word_type ty2 889 then bitstringSyntax.mk_v2w (tm, dw ty2) 890 else if ty2 = bitstringSyntax.bitstring_ty 891 then tm 892 else if ty2 = numSyntax.num 893 then bitstringSyntax.mk_v2n tm 894 else if ty2 = intSyntax.int_ty 895 then intSyntax.mk_injected (bitstringSyntax.mk_v2n tm) 896 else if ty2 = stringSyntax.string_ty 897 then bitstringSyntax.mk_v2s tm 898 else if ty2 = Type.bool 899 then boolSyntax.mk_neg (boolSyntax.mk_eq 900 (bitstringSyntax.mk_v2n tm, numSyntax.zero_tm)) 901 else if ty2 = stringSyntax.char_ty 902 then stringSyntax.mk_chr (bitstringSyntax.mk_v2n tm) 903 else Term.mk_comb (num2enum ty2, bitstringSyntax.mk_v2n tm) 904 else if ty1 = numSyntax.num 905 then if wordsSyntax.is_word_type ty2 906 then wordsSyntax.mk_n2w (tm, dw ty2) 907 else if ty2 = bitstringSyntax.bitstring_ty 908 then bitstringSyntax.mk_n2v tm 909 else if ty2 = numSyntax.num 910 then tm 911 else if ty2 = intSyntax.int_ty 912 then intSyntax.mk_injected tm 913 else if ty2 = stringSyntax.string_ty 914 then ASCIInumbersSyntax.mk_num_to_dec_string tm 915 else if ty2 = Type.bool 916 then boolSyntax.mk_neg (boolSyntax.mk_eq 917 (tm, numSyntax.zero_tm)) 918 else if ty2 = stringSyntax.char_ty 919 then stringSyntax.mk_chr tm 920 else Term.mk_comb (num2enum ty2, tm) 921 else if ty1 = intSyntax.int_ty 922 then if wordsSyntax.is_word_type ty2 923 then integer_wordSyntax.mk_i2w (tm, dw ty2) 924 else if ty2 = bitstringSyntax.bitstring_ty 925 then bitstringSyntax.mk_n2v (intSyntax.mk_Num tm) 926 else if ty2 = numSyntax.num 927 then intSyntax.mk_Num tm 928 else if ty2 = intSyntax.int_ty 929 then tm 930 else if ty2 = stringSyntax.string_ty 931 then integer_wordSyntax.mk_toString tm 932 else if ty2 = Type.bool 933 then boolSyntax.mk_neg (boolSyntax.mk_eq 934 (tm, intSyntax.zero_tm)) 935 else if ty2 = stringSyntax.char_ty 936 then stringSyntax.mk_chr (intSyntax.mk_Num tm) 937 else Term.mk_comb (num2enum ty2, intSyntax.mk_Num tm) 938 else if ty1 = stringSyntax.string_ty 939 then if wordsSyntax.is_word_type ty2 940 then wordsSyntax.mk_word_from_hex_string (tm, dw ty2) 941 else if ty2 = bitstringSyntax.bitstring_ty 942 then bitstringSyntax.mk_s2v tm 943 else if ty2 = numSyntax.num 944 then ASCIInumbersSyntax.mk_num_from_dec_string tm 945 else if ty2 = intSyntax.int_ty 946 then integer_wordSyntax.mk_fromString tm 947 else if ty2 = stringSyntax.string_ty 948 then tm 949 else if ty2 = Type.bool 950 then Term.mk_comb (string2bool, tm) 951 else if ty2 = stringSyntax.char_ty 952 then stringSyntax.mk_tochar tm 953 else Term.mk_comb (string2enum ty2, tm) 954 else if ty1 = Type.bool 955 then if wordsSyntax.is_word_type ty2 956 then mk_word_from_bool (tm, ty2) 957 else if ty2 = bitstringSyntax.bitstring_ty 958 then listSyntax.mk_list ([tm], Type.bool) 959 else if ty2 = numSyntax.num 960 then mk_from_bool (tm, one_tm, numSyntax.zero_tm) 961 else if ty2 = intSyntax.int_ty 962 then mk_from_bool (tm, intSyntax.one_tm, intSyntax.zero_tm) 963 else if ty2 = stringSyntax.string_ty 964 then mk_from_bool (tm, 965 stringSyntax.fromMLstring "true", 966 stringSyntax.fromMLstring "false") 967 else if ty2 = Type.bool 968 then tm 969 else if ty2 = stringSyntax.char_ty 970 then mk_from_bool (tm, t_tm, f_tm) 971 else raise ERR "pickCast" "bool -> ?" 972 else if ty1 = stringSyntax.char_ty 973 then if wordsSyntax.is_word_type ty2 974 then wordsSyntax.mk_n2w (stringSyntax.mk_ord tm, dw ty2) 975 else if ty2 = bitstringSyntax.bitstring_ty 976 then bitstringSyntax.mk_n2v (stringSyntax.mk_ord tm) 977 else if ty2 = numSyntax.num 978 then stringSyntax.mk_ord tm 979 else if ty2 = intSyntax.int_ty 980 then intSyntax.mk_injected (stringSyntax.mk_ord tm) 981 else if ty2 = stringSyntax.string_ty 982 then stringSyntax.mk_str tm 983 else if ty2 = Type.bool 984 then boolSyntax.mk_eq (tm, t_tm) 985 else if ty2 = stringSyntax.char_ty 986 then tm 987 else Term.mk_comb (num2enum ty2, stringSyntax.mk_ord tm) 988 else case mk_from_enum ty1 of 989 SOME e2n => 990 if wordsSyntax.is_word_type ty2 991 then wordsSyntax.mk_n2w (e2n tm, dw ty2) 992 else if ty2 = bitstringSyntax.bitstring_ty 993 then bitstringSyntax.mk_n2v (e2n tm) 994 else if ty2 = numSyntax.num 995 then e2n tm 996 else if ty2 = intSyntax.int_ty 997 then intSyntax.mk_injected (e2n tm) 998 else if ty2 = stringSyntax.string_ty 999 then Term.mk_comb (enum2string ty1, tm) 1000 else if ty2 = Type.bool 1001 then boolSyntax.mk_neg (boolSyntax.mk_eq 1002 (tm, hd (TypeBase.constructors_of ty1))) 1003 else if ty2 = stringSyntax.char_ty 1004 then stringSyntax.mk_chr (e2n tm) 1005 else Term.mk_comb (num2enum ty2, e2n tm) 1006 | _ => raise ERR "pickCast" 1007 ("bad domain: " ^ typeName ty1 ^ " -> " ^ typeName ty2) 1008 end 1009 1010 fun pick (a, b) tm = (if Lib.can wordsSyntax.dim_of tm then a else b) tm 1011 1012 fun pickMinMax (a, b, c) tm = 1013 let 1014 val ty = (fst o pairSyntax.dest_prod o Term.type_of) tm 1015 in 1016 (if wordsSyntax.is_word_type ty 1017 then a 1018 else if ty = numSyntax.num 1019 then b 1020 else if ty = intSyntax.int_ty 1021 then c 1022 else raise ERR "Mop" "pickMinMax") tm 1023 end 1024in 1025 fun Mop (m : monop, x) = 1026 (case m of 1027 Abs => pick (wordsSyntax.mk_word_abs, intSyntax.mk_absval) 1028 | BNot => wordsSyntax.mk_word_1comp 1029 | Bin => ASCIInumbersSyntax.mk_fromBinString 1030 | Cardinality => pred_setSyntax.mk_card 1031 | Cast ty => pickCast (Ty ty) 1032 | Dec => ASCIInumbersSyntax.mk_fromDecString 1033 | Difference => mk_difference 1034 | Drop => mk_drop 1035 | Element => mk_element 1036 | FPAbs 32 => fp32Syntax.mk_fp_abs 1037 | FPAbs 64 => fp64Syntax.mk_fp_abs 1038 | FPAbs i => raise ERR "Mop" ("FPAbs " ^ Int.toString i) 1039 | FPIsIntegral 32 => fp32Syntax.mk_fp_isIntegral 1040 | FPIsIntegral 64 => fp64Syntax.mk_fp_isIntegral 1041 | FPIsIntegral i => raise ERR "Mop" ("FPIsIntegral " ^ Int.toString i) 1042 | FPIsFinite 32 => fp32Syntax.mk_fp_isFinite 1043 | FPIsFinite 64 => fp64Syntax.mk_fp_isFinite 1044 | FPIsFinite i => raise ERR "Mop" ("FPIsFinite " ^ Int.toString i) 1045 | FPIsNan 32 => fp32Syntax.mk_fp_isNan 1046 | FPIsNan 64 => fp64Syntax.mk_fp_isNan 1047 | FPIsNan i => raise ERR "Mop" ("FPIsNaN " ^ Int.toString i) 1048 | FPIsNormal 32 => fp32Syntax.mk_fp_isNormal 1049 | FPIsNormal 64 => fp64Syntax.mk_fp_isNormal 1050 | FPIsNormal i => raise ERR "Mop" ("FPIsNormal " ^ Int.toString i) 1051 | FPIsSubnormal 32 => fp32Syntax.mk_fp_isSubnormal 1052 | FPIsSubnormal 64 => fp64Syntax.mk_fp_isSubnormal 1053 | FPIsSubnormal i => raise ERR "Mop" ("FPIsSubnormal " ^ Int.toString i) 1054 | FPIsZero 32 => fp32Syntax.mk_fp_isZero 1055 | FPIsZero 64 => fp64Syntax.mk_fp_isZero 1056 | FPIsZero i => raise ERR "Mop" ("FPIsZero " ^ Int.toString i) 1057 | FPIsSignallingNan 32 => fp32Syntax.mk_fp_isSignallingNan 1058 | FPIsSignallingNan 64 => fp64Syntax.mk_fp_isSignallingNan 1059 | FPIsSignallingNan i => 1060 raise ERR "Mop" ("FPIsSignallingNaN " ^ Int.toString i) 1061 | FPNeg 32 => fp32Syntax.mk_fp_negate 1062 | FPNeg 64 => fp64Syntax.mk_fp_negate 1063 | FPNeg i => raise ERR "Mop" ("FPNeg " ^ Int.toString i) 1064 | FP32To64 => machine_ieeeSyntax.mk_fp32_to_fp64 1065 | Flat => listSyntax.mk_flat 1066 | Fst => pairSyntax.mk_fst 1067 | Head => listSyntax.mk_hd 1068 | Hex => ASCIInumbersSyntax.mk_fromHexString 1069 | IndexOf => mk_indexof 1070 | Intersect => mk_intersect 1071 | IsAlpha => stringSyntax.mk_isalpha 1072 | IsAlphaNum => stringSyntax.mk_isalphanum 1073 | IsDigit => stringSyntax.mk_isdigit 1074 | IsHexDigit => stringSyntax.mk_ishexdigit 1075 | IsLower => stringSyntax.mk_islower 1076 | IsMember => mk_ismember 1077 | IsSome => optionSyntax.mk_is_some 1078 | IsSpace => stringSyntax.mk_isspace 1079 | IsSubset => mk_issubset 1080 | IsUpper => stringSyntax.mk_isupper 1081 | K1 ty => (fn tm => combinSyntax.mk_K_1 (tm, Ty ty)) 1082 | Length => listSyntax.mk_length 1083 | Log => pick (wordsSyntax.mk_word_log2, bitSyntax.mk_log2) 1084 | Max => pickMinMax (mk_word_max, mk_num_max, mk_int_max) 1085 | Min => pickMinMax (mk_word_min, mk_num_min, mk_int_min) 1086 | Msb => wordsSyntax.mk_word_msb 1087 | Neg => pick (wordsSyntax.mk_word_2comp, intSyntax.mk_negated) 1088 | Not => boolSyntax.mk_neg 1089 | PadLeft => mk_pad_left 1090 | PadRight => mk_pad_right 1091 | QuotRem => mk_quot_rem 1092 | Remove => mk_remove 1093 | RemoveExcept => mk_remove_e 1094 | RemoveDuplicates => listSyntax.mk_nub 1095 | Rev => pick (wordsSyntax.mk_word_reverse, listSyntax.mk_reverse) 1096 | SE ty => mk_sign_extend ty 1097 | Size => wordsSyntax.mk_word_len 1098 | Smax => mk_word_smax 1099 | Smin => mk_word_smin 1100 | Snd => pairSyntax.mk_snd 1101 | SofL => listSyntax.mk_list_to_set 1102 | Some => optionSyntax.mk_some 1103 | Tail => listSyntax.mk_tl 1104 | Take => mk_take 1105 | ToLower => mk_lower 1106 | ToUpper => mk_upper 1107 | Union => mk_union 1108 | Update => mk_update 1109 | ValOf => optionSyntax.mk_the 1110 | _ => mk_fp_op m 1111 ) x 1112end 1113 1114local 1115 fun pick (a, b, c, d) (tm1, tm2: term) : term = 1116 let 1117 val ty = Term.type_of tm1 1118 in 1119 Option.valOf 1120 (if Option.isSome a andalso wordsSyntax.is_word_type ty 1121 then a 1122 else if Option.isSome b andalso ty = bitstringSyntax.bitstring_ty 1123 then b 1124 else if Option.isSome c andalso ty = numSyntax.num 1125 then c 1126 else if Option.isSome d andalso ty = intSyntax.int_ty 1127 then d 1128 else raise ERR "Bop" "pick") (tm1, tm2) 1129 end 1130 fun pickWordShift (a, b) (tm1 : term, tm2) : term = 1131 (if wordsSyntax.is_word_type (Term.type_of tm2) then a else b) (tm1, tm2) 1132 fun pickShift (a, b, c) = 1133 pick (SOME (pickWordShift (a, b)), SOME c, NONE, NONE) 1134 fun COMM f (x, y) = f (y, x) 1135 fun icurry tm = 1136 Term.mk_comb 1137 (Term.inst [Type.alpha |-> numSyntax.num, Type.beta |-> Type.bool, 1138 Type.gamma |-> Type.bool] pairSyntax.curry_tm, tm) 1139in 1140 fun Bop (b : binop, x, y) = (x, y) |> 1141 (case b of 1142 And => boolSyntax.mk_conj 1143 | BAnd => pick (SOME wordsSyntax.mk_word_and, 1144 SOME bitstringSyntax.mk_band, NONE, NONE) 1145 | BOr => pick (SOME wordsSyntax.mk_word_or, 1146 SOME bitstringSyntax.mk_bor, NONE, NONE) 1147 | BXor => pick (SOME wordsSyntax.mk_word_xor, 1148 SOME bitstringSyntax.mk_bxor, NONE, NONE) 1149 | In => pred_setSyntax.mk_in 1150 | Insert => pred_setSyntax.mk_insert 1151 | Or => boolSyntax.mk_disj 1152 | Uge => wordsSyntax.mk_word_hs 1153 | Ugt => wordsSyntax.mk_word_hi 1154 | Ule => wordsSyntax.mk_word_ls 1155 | Ult => wordsSyntax.mk_word_lo 1156 | Splitl => rich_listSyntax.mk_splitl 1157 | Splitr => rich_listSyntax.mk_splitr 1158 | Fld => stringSyntax.mk_fields 1159 | Tok => stringSyntax.mk_tokens 1160 | Rep => bitstringSyntax.mk_replicate 1161 | Lt => pick (SOME wordsSyntax.mk_word_lt, NONE, 1162 SOME numSyntax.mk_less, SOME intSyntax.mk_less) 1163 | Gt => pick (SOME wordsSyntax.mk_word_gt, NONE, 1164 SOME numSyntax.mk_greater, SOME intSyntax.mk_greater) 1165 | Le => pick (SOME wordsSyntax.mk_word_le, NONE, 1166 SOME numSyntax.mk_leq, SOME intSyntax.mk_leq) 1167 | Ge => pick (SOME wordsSyntax.mk_word_ge, NONE, 1168 SOME numSyntax.mk_geq, SOME intSyntax.mk_geq) 1169 | Bit => pick (SOME (COMM wordsSyntax.mk_word_bit), 1170 SOME (COMM bitstringSyntax.mk_testbit), NONE, NONE) 1171 | Add => pick (SOME wordsSyntax.mk_word_add, 1172 SOME bitstringSyntax.mk_add, SOME numSyntax.mk_plus, 1173 SOME intSyntax.mk_plus) 1174 | Sub => pick (SOME wordsSyntax.mk_word_sub, NONE, 1175 SOME numSyntax.mk_minus, SOME intSyntax.mk_minus) 1176 | Mul => pick (SOME wordsSyntax.mk_word_mul, NONE, 1177 SOME numSyntax.mk_mult, SOME intSyntax.mk_mult) 1178 | Div => pick (SOME wordsSyntax.mk_word_div, NONE, 1179 SOME numSyntax.mk_div, SOME intSyntax.mk_div) 1180 | Mod => pick (SOME wordsSyntax.mk_word_mod, NONE, 1181 SOME numSyntax.mk_mod, SOME intSyntax.mk_mod) 1182 | Quot => pick (SOME wordsSyntax.mk_word_quot, NONE, NONE, 1183 SOME intSyntax.mk_quot) 1184 | Rem => pick (SOME wordsSyntax.mk_word_rem, NONE, NONE, 1185 SOME intSyntax.mk_rem) 1186 | SDiv => integer_wordSyntax.mk_word_sdiv 1187 | SMod => integer_wordSyntax.mk_word_smod 1188 | Exp => pick (NONE, NONE, SOME numSyntax.mk_exp, SOME intSyntax.mk_exp) 1189 | Lsl => pickShift (wordsSyntax.mk_word_lsl_bv, wordsSyntax.mk_word_lsl, 1190 bitstringSyntax.mk_shiftl) 1191 | Lsr => pickShift (wordsSyntax.mk_word_lsr_bv, wordsSyntax.mk_word_lsr, 1192 bitstringSyntax.mk_shiftr) 1193 | Ror => pickShift (wordsSyntax.mk_word_ror_bv, wordsSyntax.mk_word_ror, 1194 bitstringSyntax.mk_rotate) 1195 | Asr => pickWordShift 1196 (wordsSyntax.mk_word_asr_bv, wordsSyntax.mk_word_asr) 1197 | Rol => pickWordShift 1198 (wordsSyntax.mk_word_rol_bv, wordsSyntax.mk_word_rol)) 1199end 1200 1201(* ------------------------------------------------------------------------ *) 1202 1203(* Definitions *) 1204 1205local 1206 val tac = SRW_TAC [listSimps.LIST_ss, numSimps.ARITH_ss] [] 1207in 1208 fun MEASURE_TAC tm = 1209 TotalDefn.WF_REL_TAC `^(boolSyntax.mk_icomb (numSyntax.measure_tm, tm))` 1210 THEN tac 1211end 1212 1213fun new_def s x = Definition.new_definition (s ^ "_def", boolSyntax.mk_eq x) 1214 1215fun z_def def = 1216 Feedback.trace ("Define.storage_message", 0) 1217 bossLib.zDefine [HOLPP.ANTIQUOTE (boolSyntax.mk_eq def)] 1218 1219fun t_def s def m tac = 1220 Feedback.trace ("Define.storage_message", 0) 1221 (bossLib.tDefine s [HOLPP.ANTIQUOTE (boolSyntax.mk_eq def)]) 1222 (MEASURE_TAC m THEN tac) 1223 1224val mesg = 1225 Lib.with_flag 1226 (Feedback.MESG_to_string, 1227 fn s => (log_constant s; "Defined: " ^ s ^ "\n")) 1228 Feedback.HOL_MESG 1229 1230fun Def (s, a, b) = 1231 let 1232 val ty = Type.--> (Term.type_of a, Term.type_of b) 1233 val c = Term.mk_var (s, ty) 1234 val isrec = (HolKernel.find_term (aconv c) b; true) 1235 handle HOL_ERR _ => false 1236 val def = if isrec andalso Term.is_abs b 1237 then let 1238 val (vs, b1) = Term.strip_abs b 1239 in 1240 (Term.list_mk_comb (c, a :: vs), b1) 1241 end 1242 else (Term.mk_comb (c, a), b) 1243 val () = resetAnon () 1244 in 1245 (if isrec then z_def else new_def s) def before mesg s 1246 end 1247 1248fun tDef (s, a, b, m, t) = 1249 let 1250 val ty = Type.--> (Term.type_of a, Term.type_of b) 1251 val c = Term.mk_var (s, ty) 1252 val def = if Term.is_abs b 1253 then let 1254 val (vs, b1) = Term.strip_abs b 1255 in 1256 (Term.list_mk_comb (c, a :: vs), b1) 1257 end 1258 else (Term.mk_comb (c, a), b) 1259 val () = resetAnon () 1260 in 1261 t_def s def m t before mesg s 1262 end 1263 1264fun Def0 (s, b) = new_def s (Term.mk_var (s, Term.type_of b), b) before mesg s 1265 1266end (* Import *) 1267