Changeset 2649 for extracted/byteValues.ml
 Timestamp:
 Feb 7, 2013, 10:43:49 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/byteValues.ml
r2601 r2649 7 7 open Deqsets 8 8 9 open ErrorMessages 10 9 11 open PreIdentifiers 10 12 … … 23 25 open Identifiers 24 26 25 open Coqlib26 27 open Floats28 29 27 open Integers 30 28 … … 34 32 35 33 open Arithmetic 36 37 open Char38 39 open String40 34 41 35 open Extranat … … 93 87 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 94 88 'a1 **) 95 let rec program_counter_rect_Type4 h_mk_program_counter x_ 5073=96 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 5073in89 let rec program_counter_rect_Type4 h_mk_program_counter x_4510 = 90 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4510 in 97 91 h_mk_program_counter pc_block0 pc_offset0 98 92 … … 100 94 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 101 95 'a1 **) 102 let rec program_counter_rect_Type5 h_mk_program_counter x_ 5075=103 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 5075in96 let rec program_counter_rect_Type5 h_mk_program_counter x_4512 = 97 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4512 in 104 98 h_mk_program_counter pc_block0 pc_offset0 105 99 … … 107 101 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 108 102 'a1 **) 109 let rec program_counter_rect_Type3 h_mk_program_counter x_ 5077=110 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 5077in103 let rec program_counter_rect_Type3 h_mk_program_counter x_4514 = 104 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4514 in 111 105 h_mk_program_counter pc_block0 pc_offset0 112 106 … … 114 108 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 115 109 'a1 **) 116 let rec program_counter_rect_Type2 h_mk_program_counter x_ 5079=117 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 5079in110 let rec program_counter_rect_Type2 h_mk_program_counter x_4516 = 111 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4516 in 118 112 h_mk_program_counter pc_block0 pc_offset0 119 113 … … 121 115 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 122 116 'a1 **) 123 let rec program_counter_rect_Type1 h_mk_program_counter x_ 5081=124 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 5081in117 let rec program_counter_rect_Type1 h_mk_program_counter x_4518 = 118 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4518 in 125 119 h_mk_program_counter pc_block0 pc_offset0 126 120 … … 128 122 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 129 123 'a1 **) 130 let rec program_counter_rect_Type0 h_mk_program_counter x_ 5083=131 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 5083in124 let rec program_counter_rect_Type0 h_mk_program_counter x_4520 = 125 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4520 in 132 126 h_mk_program_counter pc_block0 pc_offset0 133 127 … … 219 213 220 214 (** val part_rect_Type4 : (Nat.nat > __ > 'a1) > part > 'a1 **) 221 let rec part_rect_Type4 h_mk_part x_ 5099=222 let part_no = x_ 5099in h_mk_part part_no __215 let rec part_rect_Type4 h_mk_part x_4536 = 216 let part_no = x_4536 in h_mk_part part_no __ 223 217 224 218 (** val part_rect_Type5 : (Nat.nat > __ > 'a1) > part > 'a1 **) 225 let rec part_rect_Type5 h_mk_part x_ 5101=226 let part_no = x_ 5101in h_mk_part part_no __219 let rec part_rect_Type5 h_mk_part x_4538 = 220 let part_no = x_4538 in h_mk_part part_no __ 227 221 228 222 (** val part_rect_Type3 : (Nat.nat > __ > 'a1) > part > 'a1 **) 229 let rec part_rect_Type3 h_mk_part x_ 5103=230 let part_no = x_ 5103in h_mk_part part_no __223 let rec part_rect_Type3 h_mk_part x_4540 = 224 let part_no = x_4540 in h_mk_part part_no __ 231 225 232 226 (** val part_rect_Type2 : (Nat.nat > __ > 'a1) > part > 'a1 **) 233 let rec part_rect_Type2 h_mk_part x_ 5105=234 let part_no = x_ 5105in h_mk_part part_no __227 let rec part_rect_Type2 h_mk_part x_4542 = 228 let part_no = x_4542 in h_mk_part part_no __ 235 229 236 230 (** val part_rect_Type1 : (Nat.nat > __ > 'a1) > part > 'a1 **) 237 let rec part_rect_Type1 h_mk_part x_ 5107=238 let part_no = x_ 5107in h_mk_part part_no __231 let rec part_rect_Type1 h_mk_part x_4544 = 232 let part_no = x_4544 in h_mk_part part_no __ 239 233 240 234 (** val part_rect_Type0 : (Nat.nat > __ > 'a1) > part > 'a1 **) 241 let rec part_rect_Type0 h_mk_part x_ 5109=242 let part_no = x_ 5109in h_mk_part part_no __235 let rec part_rect_Type0 h_mk_part x_4546 = 236 let part_no = x_4546 in h_mk_part part_no __ 243 237 244 238 (** val part_no : part > Nat.nat **) … … 330 324  BVundef > h_BVundef 331 325  BVnonzero > h_BVnonzero 332  BVXor (x_ 5143, x_5142, x_5141) > h_BVXor x_5143 x_5142 x_5141333  BVByte x_ 5144 > h_BVByte x_5144334  BVnull x_ 5145 > h_BVnull x_5145335  BVptr (x_ 5147, x_5146) > h_BVptr x_5147 x_5146336  BVpc (x_ 5149, x_5148) > h_BVpc x_5149 x_5148326  BVXor (x_4580, x_4579, x_4578) > h_BVXor x_4580 x_4579 x_4578 327  BVByte x_4581 > h_BVByte x_4581 328  BVnull x_4582 > h_BVnull x_4582 329  BVptr (x_4584, x_4583) > h_BVptr x_4584 x_4583 330  BVpc (x_4586, x_4585) > h_BVpc x_4586 x_4585 337 331 338 332 (** val beval_rect_Type5 : … … 344 338  BVundef > h_BVundef 345 339  BVnonzero > h_BVnonzero 346  BVXor (x_ 5160, x_5159, x_5158) > h_BVXor x_5160 x_5159 x_5158347  BVByte x_ 5161 > h_BVByte x_5161348  BVnull x_ 5162 > h_BVnull x_5162349  BVptr (x_ 5164, x_5163) > h_BVptr x_5164 x_5163350  BVpc (x_ 5166, x_5165) > h_BVpc x_5166 x_5165340  BVXor (x_4597, x_4596, x_4595) > h_BVXor x_4597 x_4596 x_4595 341  BVByte x_4598 > h_BVByte x_4598 342  BVnull x_4599 > h_BVnull x_4599 343  BVptr (x_4601, x_4600) > h_BVptr x_4601 x_4600 344  BVpc (x_4603, x_4602) > h_BVpc x_4603 x_4602 351 345 352 346 (** val beval_rect_Type3 : … … 358 352  BVundef > h_BVundef 359 353  BVnonzero > h_BVnonzero 360  BVXor (x_ 5177, x_5176, x_5175) > h_BVXor x_5177 x_5176 x_5175361  BVByte x_ 5178 > h_BVByte x_5178362  BVnull x_ 5179 > h_BVnull x_5179363  BVptr (x_ 5181, x_5180) > h_BVptr x_5181 x_5180364  BVpc (x_ 5183, x_5182) > h_BVpc x_5183 x_5182354  BVXor (x_4614, x_4613, x_4612) > h_BVXor x_4614 x_4613 x_4612 355  BVByte x_4615 > h_BVByte x_4615 356  BVnull x_4616 > h_BVnull x_4616 357  BVptr (x_4618, x_4617) > h_BVptr x_4618 x_4617 358  BVpc (x_4620, x_4619) > h_BVpc x_4620 x_4619 365 359 366 360 (** val beval_rect_Type2 : … … 372 366  BVundef > h_BVundef 373 367  BVnonzero > h_BVnonzero 374  BVXor (x_ 5194, x_5193, x_5192) > h_BVXor x_5194 x_5193 x_5192375  BVByte x_ 5195 > h_BVByte x_5195376  BVnull x_ 5196 > h_BVnull x_5196377  BVptr (x_ 5198, x_5197) > h_BVptr x_5198 x_5197378  BVpc (x_ 5200, x_5199) > h_BVpc x_5200 x_5199368  BVXor (x_4631, x_4630, x_4629) > h_BVXor x_4631 x_4630 x_4629 369  BVByte x_4632 > h_BVByte x_4632 370  BVnull x_4633 > h_BVnull x_4633 371  BVptr (x_4635, x_4634) > h_BVptr x_4635 x_4634 372  BVpc (x_4637, x_4636) > h_BVpc x_4637 x_4636 379 373 380 374 (** val beval_rect_Type1 : … … 386 380  BVundef > h_BVundef 387 381  BVnonzero > h_BVnonzero 388  BVXor (x_ 5211, x_5210, x_5209) > h_BVXor x_5211 x_5210 x_5209389  BVByte x_ 5212 > h_BVByte x_5212390  BVnull x_ 5213 > h_BVnull x_5213391  BVptr (x_ 5215, x_5214) > h_BVptr x_5215 x_5214392  BVpc (x_ 5217, x_5216) > h_BVpc x_5217 x_5216382  BVXor (x_4648, x_4647, x_4646) > h_BVXor x_4648 x_4647 x_4646 383  BVByte x_4649 > h_BVByte x_4649 384  BVnull x_4650 > h_BVnull x_4650 385  BVptr (x_4652, x_4651) > h_BVptr x_4652 x_4651 386  BVpc (x_4654, x_4653) > h_BVpc x_4654 x_4653 393 387 394 388 (** val beval_rect_Type0 : … … 400 394  BVundef > h_BVundef 401 395  BVnonzero > h_BVnonzero 402  BVXor (x_ 5228, x_5227, x_5226) > h_BVXor x_5228 x_5227 x_5226403  BVByte x_ 5229 > h_BVByte x_5229404  BVnull x_ 5230 > h_BVnull x_5230405  BVptr (x_ 5232, x_5231) > h_BVptr x_5232 x_5231406  BVpc (x_ 5234, x_5233) > h_BVpc x_5234 x_5233396  BVXor (x_4665, x_4664, x_4663) > h_BVXor x_4665 x_4664 x_4663 397  BVByte x_4666 > h_BVByte x_4666 398  BVnull x_4667 > h_BVnull x_4667 399  BVptr (x_4669, x_4668) > h_BVptr x_4669 x_4668 400  BVpc (x_4671, x_4670) > h_BVpc x_4671 x_4670 407 401 408 402 (** val beval_inv_rect_Type4 : … … 477 471 let b2 = (Vector.vsplit m p v2).Types.snd in BitVector.eq_bv p b1 b2 478 472 479 (** val corruptedPointer : String.string **)480 let corruptedPointer = "corrupted pointer"481 (* failwith "AXIOM TO BE REALIZED" *)482 483 473 (** val pointer_of_bevals : 484 474 beval List.list > Pointers.pointer Errors.res **) 485 475 let pointer_of_bevals = function 486 476  List.Nil > 487 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)) 477 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer), 478 List.Nil)) 488 479  List.Cons (bv1, tl) > 489 480 (match tl with 490 481  List.Nil > 491 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)) 482 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer), 483 List.Nil)) 492 484  List.Cons (bv2, tl') > 493 485 (match tl' with … … 495 487 (match bv1 with 496 488  BVundef > 497 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)) 489 Errors.Error (List.Cons ((Errors.MSG 490 ErrorMessages.CorruptedPointer), List.Nil)) 498 491  BVnonzero > 499 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)) 492 Errors.Error (List.Cons ((Errors.MSG 493 ErrorMessages.CorruptedPointer), List.Nil)) 500 494  BVXor (x, x0, x1) > 501 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)) 495 Errors.Error (List.Cons ((Errors.MSG 496 ErrorMessages.CorruptedPointer), List.Nil)) 502 497  BVByte x > 503 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)) 498 Errors.Error (List.Cons ((Errors.MSG 499 ErrorMessages.CorruptedPointer), List.Nil)) 504 500  BVnull x > 505 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)) 501 Errors.Error (List.Cons ((Errors.MSG 502 ErrorMessages.CorruptedPointer), List.Nil)) 506 503  BVptr (ptr1, p3) > 507 504 (match bv2 with 508 505  BVundef > 509 Errors.Error (List.Cons ((Errors.MSG corruptedPointer),510 List.Nil))506 Errors.Error (List.Cons ((Errors.MSG 507 ErrorMessages.CorruptedPointer), List.Nil)) 511 508  BVnonzero > 512 Errors.Error (List.Cons ((Errors.MSG corruptedPointer),513 List.Nil))509 Errors.Error (List.Cons ((Errors.MSG 510 ErrorMessages.CorruptedPointer), List.Nil)) 514 511  BVXor (x, x0, x1) > 515 Errors.Error (List.Cons ((Errors.MSG corruptedPointer),516 List.Nil))512 Errors.Error (List.Cons ((Errors.MSG 513 ErrorMessages.CorruptedPointer), List.Nil)) 517 514  BVByte x > 518 Errors.Error (List.Cons ((Errors.MSG corruptedPointer),519 List.Nil))515 Errors.Error (List.Cons ((Errors.MSG 516 ErrorMessages.CorruptedPointer), List.Nil)) 520 517  BVnull x > 521 Errors.Error (List.Cons ((Errors.MSG corruptedPointer),522 List.Nil))518 Errors.Error (List.Cons ((Errors.MSG 519 ErrorMessages.CorruptedPointer), List.Nil)) 523 520  BVptr (ptr2, p4) > 524 521 (match Bool.andb … … 538 535 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2) 539 536  Bool.False > 540 Errors.Error (List.Cons ((Errors.MSG corruptedPointer),541 List.Nil)))537 Errors.Error (List.Cons ((Errors.MSG 538 ErrorMessages.CorruptedPointer), List.Nil))) 542 539  BVpc (x, x0) > 543 Errors.Error (List.Cons ((Errors.MSG corruptedPointer),544 List.Nil)))540 Errors.Error (List.Cons ((Errors.MSG 541 ErrorMessages.CorruptedPointer), List.Nil))) 545 542  BVpc (x, x0) > 546 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))) 543 Errors.Error (List.Cons ((Errors.MSG 544 ErrorMessages.CorruptedPointer), List.Nil))) 547 545  List.Cons (x, x0) > 548 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)))) 546 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer), 547 List.Nil)))) 549 548 550 549 (** val pc_of_bevals : beval List.list > program_counter Errors.res **) 551 550 let pc_of_bevals = function 552 551  List.Nil > 553 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)) 552 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer), 553 List.Nil)) 554 554  List.Cons (bv1, tl) > 555 555 (match tl with 556 556  List.Nil > 557 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)) 557 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer), 558 List.Nil)) 558 559  List.Cons (bv2, tl') > 559 560 (match tl' with … … 561 562 (match bv1 with 562 563  BVundef > 563 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)) 564 Errors.Error (List.Cons ((Errors.MSG 565 ErrorMessages.CorruptedPointer), List.Nil)) 564 566  BVnonzero > 565 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)) 567 Errors.Error (List.Cons ((Errors.MSG 568 ErrorMessages.CorruptedPointer), List.Nil)) 566 569  BVXor (x, x0, x1) > 567 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)) 570 Errors.Error (List.Cons ((Errors.MSG 571 ErrorMessages.CorruptedPointer), List.Nil)) 568 572  BVByte x > 569 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)) 573 Errors.Error (List.Cons ((Errors.MSG 574 ErrorMessages.CorruptedPointer), List.Nil)) 570 575  BVnull x > 571 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)) 576 Errors.Error (List.Cons ((Errors.MSG 577 ErrorMessages.CorruptedPointer), List.Nil)) 572 578  BVptr (x, x0) > 573 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)) 579 Errors.Error (List.Cons ((Errors.MSG 580 ErrorMessages.CorruptedPointer), List.Nil)) 574 581  BVpc (ptr1, p3) > 575 582 (match bv2 with 576 583  BVundef > 577 Errors.Error (List.Cons ((Errors.MSG corruptedPointer),578 List.Nil))584 Errors.Error (List.Cons ((Errors.MSG 585 ErrorMessages.CorruptedPointer), List.Nil)) 579 586  BVnonzero > 580 Errors.Error (List.Cons ((Errors.MSG corruptedPointer),581 List.Nil))587 Errors.Error (List.Cons ((Errors.MSG 588 ErrorMessages.CorruptedPointer), List.Nil)) 582 589  BVXor (x, x0, x1) > 583 Errors.Error (List.Cons ((Errors.MSG corruptedPointer),584 List.Nil))590 Errors.Error (List.Cons ((Errors.MSG 591 ErrorMessages.CorruptedPointer), List.Nil)) 585 592  BVByte x > 586 Errors.Error (List.Cons ((Errors.MSG corruptedPointer),587 List.Nil))593 Errors.Error (List.Cons ((Errors.MSG 594 ErrorMessages.CorruptedPointer), List.Nil)) 588 595  BVnull x > 589 Errors.Error (List.Cons ((Errors.MSG corruptedPointer),590 List.Nil))596 Errors.Error (List.Cons ((Errors.MSG 597 ErrorMessages.CorruptedPointer), List.Nil)) 591 598  BVptr (x, x0) > 592 Errors.Error (List.Cons ((Errors.MSG corruptedPointer),593 List.Nil))599 Errors.Error (List.Cons ((Errors.MSG 600 ErrorMessages.CorruptedPointer), List.Nil)) 594 601  BVpc (ptr2, p4) > 595 602 (match Bool.andb … … 600 607 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2) 601 608  Bool.False > 602 Errors.Error (List.Cons ((Errors.MSG corruptedPointer),603 List.Nil)))))609 Errors.Error (List.Cons ((Errors.MSG 610 ErrorMessages.CorruptedPointer), List.Nil))))) 604 611  List.Cons (x, x0) > 605 Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)))) 612 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer), 613 List.Nil)))) 606 614 607 615 (** val bevals_of_pointer : Pointers.pointer > beval List.list **) … … 638 646 __ 639 647 640 (** val notATwoBytesPointer : String.string **)641 let notATwoBytesPointer = "not a two bytes pointer"642 (* failwith "AXIOM TO BE REALIZED" *)643 644 648 (** val beval_pair_of_pointer : 645 649 Pointers.pointer > (beval, beval) Types.prod **) … … 651 655 list_to_pair (bevals_of_pc p) 652 656 653 (** val valueNotABoolean : String.string **)654 let valueNotABoolean = "value not a boolean"655 (* failwith "AXIOM TO BE REALIZED" *)656 657 657 (** val bool_of_beval : beval > Bool.bool Errors.res **) 658 658 let bool_of_beval = function 659 659  BVundef > 660 Errors.Error (List.Cons ((Errors.MSG valueNotABoolean), List.Nil)) 660 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean), 661 List.Nil)) 661 662  BVnonzero > Errors.OK Bool.True 662 663  BVXor (x, x0, x1) > 663 Errors.Error (List.Cons ((Errors.MSG valueNotABoolean), List.Nil)) 664 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean), 665 List.Nil)) 664 666  BVByte b > 665 667 Errors.OK … … 671 673  BVptr (x, x0) > Errors.OK Bool.True 672 674  BVpc (x, x0) > 673 Errors.Error (List.Cons ((Errors.MSG valueNotABoolean), List.Nil)) 674 675 (** val byte_of_val : String.string > beval > BitVector.byte Errors.res **) 675 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean), 676 List.Nil)) 677 678 (** val byte_of_val : 679 ErrorMessages.errorMessage > beval > BitVector.byte Errors.res **) 676 680 let byte_of_val err = function 677 681  BVundef > Errors.Error (List.Cons ((Errors.MSG err), List.Nil)) … … 683 687  BVpc (x, x0) > Errors.Error (List.Cons ((Errors.MSG err), List.Nil)) 684 688 685 (** val notAnInt32Val : String.string **)686 let notAnInt32Val = "not an int32 val"687 (* failwith "AXIOM TO BE REALIZED" *)688 689 689 (** val word_of_list_beval : beval List.list > Integers.int Errors.res **) 690 690 let word_of_list_beval l = … … 692 692 match l0 with 693 693  List.Nil > 694 Obj.magic (Errors.Error (List.Cons ((Errors.MSG notAnInt32Val),695 List.Nil)))694 Obj.magic (Errors.Error (List.Cons ((Errors.MSG 695 ErrorMessages.NotAnInt32Val), List.Nil))) 696 696  List.Cons (hd0, tl) > 697 697 Monad.m_bind0 (Monad.max_def Errors.res0) 698 (Obj.magic (byte_of_val notAnInt32Val hd0)) (fun b >698 (Obj.magic (byte_of_val ErrorMessages.NotAnInt32Val hd0)) (fun b > 699 699 Obj.magic (Errors.OK { Types.fst = b; Types.snd = tl })) 700 700 in … … 725 725 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) b2 b1)))) 726 726  List.Cons (x, x0) > 727 Obj.magic (Errors.Error (List.Cons ((Errors.MSG notAnInt32Val),728 List.Nil))))))))727 Obj.magic (Errors.Error (List.Cons ((Errors.MSG 728 ErrorMessages.NotAnInt32Val), List.Nil)))))))) 729 729 730 730 type bebit = … … 737 737 BitVector.bitVector > 'a1) > bebit > 'a1 **) 738 738 let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function 739  BBbit x_ 5353 > h_BBbit x_5353739  BBbit x_4790 > h_BBbit x_4790 740 740  BBundef > h_BBundef 741  BBptrcarry (x_ 5356, x_5355, p, x_5354) >742 h_BBptrcarry x_ 5356 x_5355 p x_5354741  BBptrcarry (x_4793, x_4792, p, x_4791) > 742 h_BBptrcarry x_4793 x_4792 p x_4791 743 743 744 744 (** val bebit_rect_Type5 : … … 746 746 BitVector.bitVector > 'a1) > bebit > 'a1 **) 747 747 let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function 748  BBbit x_ 5361 > h_BBbit x_5361748  BBbit x_4798 > h_BBbit x_4798 749 749  BBundef > h_BBundef 750  BBptrcarry (x_ 5364, x_5363, p, x_5362) >751 h_BBptrcarry x_ 5364 x_5363 p x_5362750  BBptrcarry (x_4801, x_4800, p, x_4799) > 751 h_BBptrcarry x_4801 x_4800 p x_4799 752 752 753 753 (** val bebit_rect_Type3 : … … 755 755 BitVector.bitVector > 'a1) > bebit > 'a1 **) 756 756 let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function 757  BBbit x_ 5369 > h_BBbit x_5369757  BBbit x_4806 > h_BBbit x_4806 758 758  BBundef > h_BBundef 759  BBptrcarry (x_ 5372, x_5371, p, x_5370) >760 h_BBptrcarry x_ 5372 x_5371 p x_5370759  BBptrcarry (x_4809, x_4808, p, x_4807) > 760 h_BBptrcarry x_4809 x_4808 p x_4807 761 761 762 762 (** val bebit_rect_Type2 : … … 764 764 BitVector.bitVector > 'a1) > bebit > 'a1 **) 765 765 let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function 766  BBbit x_ 5377 > h_BBbit x_5377766  BBbit x_4814 > h_BBbit x_4814 767 767  BBundef > h_BBundef 768  BBptrcarry (x_ 5380, x_5379, p, x_5378) >769 h_BBptrcarry x_ 5380 x_5379 p x_5378768  BBptrcarry (x_4817, x_4816, p, x_4815) > 769 h_BBptrcarry x_4817 x_4816 p x_4815 770 770 771 771 (** val bebit_rect_Type1 : … … 773 773 BitVector.bitVector > 'a1) > bebit > 'a1 **) 774 774 let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function 775  BBbit x_ 5385 > h_BBbit x_5385775  BBbit x_4822 > h_BBbit x_4822 776 776  BBundef > h_BBundef 777  BBptrcarry (x_ 5388, x_5387, p, x_5386) >778 h_BBptrcarry x_ 5388 x_5387 p x_5386777  BBptrcarry (x_4825, x_4824, p, x_4823) > 778 h_BBptrcarry x_4825 x_4824 p x_4823 779 779 780 780 (** val bebit_rect_Type0 : … … 782 782 BitVector.bitVector > 'a1) > bebit > 'a1 **) 783 783 let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function 784  BBbit x_ 5393 > h_BBbit x_5393784  BBbit x_4830 > h_BBbit x_4830 785 785  BBundef > h_BBundef 786  BBptrcarry (x_ 5396, x_5395, p, x_5394) >787 h_BBptrcarry x_ 5396 x_5395 p x_5394786  BBptrcarry (x_4833, x_4832, p, x_4831) > 787 h_BBptrcarry x_4833 x_4832 p x_4831 788 788 789 789 (** val bebit_inv_rect_Type4 : … … 835 835 y 836 836 837 (** val bit_of_val : String.string > bebit > BitVector.bit Errors.res **) 837 (** val bit_of_val : 838 ErrorMessages.errorMessage > bebit > BitVector.bit Errors.res **) 838 839 let bit_of_val err = function 839 840  BBbit b0 > Errors.OK b0
Note: See TracChangeset
for help on using the changeset viewer.