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