Changeset 2773 for extracted/fetch.ml
 Timestamp:
 Mar 4, 2013, 10:03:33 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/fetch.ml
r2743 r2773 1 1 open Preamble 2 2 3 open Exp 4 5 open Setoids 6 7 open Monad 8 9 open Option 10 3 11 open Extranat 4 12 … … 11 19 open Russell 12 20 21 open Types 22 13 23 open List 14 24 … … 19 29 open Bool 20 30 31 open Hints_declaration 32 33 open Core_notation 34 35 open Pts 36 37 open Logic 38 21 39 open Relations 22 40 … … 25 43 open BitVector 26 44 27 open Hints_declaration 28 29 open Core_notation 30 31 open Pts 32 33 open Logic 34 35 open Types 45 open Arithmetic 36 46 37 47 open BitVectorTrie 38 48 39 open Exp40 41 open Arithmetic42 43 49 open String 44 50 51 open Integers 52 53 open AST 54 45 55 open LabelledObjects 46 56 47 open Integers 48 49 open AST 57 open Proper 58 59 open PositiveMap 60 61 open Deqsets 62 63 open ErrorMessages 64 65 open PreIdentifiers 66 67 open Errors 68 69 open Extralib 70 71 open Lists 72 73 open Positive 74 75 open Identifiers 50 76 51 77 open CostLabel 52 78 53 open Proper54 55 open PositiveMap56 57 open Deqsets58 59 open ErrorMessages60 61 open PreIdentifiers62 63 open Errors64 65 open Extralib66 67 open Setoids68 69 open Monad70 71 open Option72 73 open Lists74 75 open Positive76 77 open Identifiers78 79 79 open ASM 80 80 81 81 (** val inefficient_address_of_word_labels_code_mem : 82 ASM.labelled_instruction List.list > ASM.identifier 0>82 ASM.labelled_instruction List.list > ASM.identifier > 83 83 BitVector.bitVector **) 84 84 let inefficient_address_of_word_labels_code_mem code_mem id = … … 86 86 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 87 87 Nat.O)))))))))))))))) 88 (LabelledObjects.index_of 088 (LabelledObjects.index_of 89 89 (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag 90 90 id) code_mem) … … 95 95 ASM.labelled_instruction List.list > (label_map, CostLabel.costlabel 96 96 BitVectorTrie.bitVectorTrie) Types.prod Types.sig0 **) 97 let create_label_cost_map0 program 0=97 let create_label_cost_map0 program = 98 98 (Types.pi1 99 (FoldStuff.foldl_strong program 0 (fun prefix0x tl _ labels_costs_ppc >100 (let { Types.fst = eta2 9042; Types.snd = ppc } =99 (FoldStuff.foldl_strong program (fun prefix x tl _ labels_costs_ppc > 100 (let { Types.fst = eta27870; Types.snd = ppc } = 101 101 Types.pi1 labels_costs_ppc 102 102 in 103 103 (fun _ > 104 (let { Types.fst = labels; Types.snd = costs } = eta2 9042in104 (let { Types.fst = labels; Types.snd = costs } = eta27870 in 105 105 (fun _ > 106 106 (let { Types.fst = label; Types.snd = instr } = x in … … 138 138 ASM.labelled_instruction List.list > (label_map, CostLabel.costlabel 139 139 BitVectorTrie.bitVectorTrie) Types.prod **) 140 let create_label_cost_map program 0=141 Types.pi1 (create_label_cost_map0 program 0)140 let create_label_cost_map program = 141 Types.pi1 (create_label_cost_map0 program) 142 142 143 143 (** val address_of_word_labels : 144 ASM.labelled_instruction List.list > ASM.identifier 0> BitVector.word **)144 ASM.labelled_instruction List.list > ASM.identifier > BitVector.word **) 145 145 let address_of_word_labels code_mem id = 146 146 let labels = (create_label_cost_map code_mem).Types.fst in … … 151 151 152 152 (** val bitvector_max_nat : Nat.nat > Nat.nat **) 153 let bitvector_max_nat length 0=154 Exp.exp (Nat.S (Nat.S Nat.O)) length 0153 let bitvector_max_nat length = 154 Exp.exp (Nat.S (Nat.S Nat.O)) length 155 155 156 156 (** val code_memory_size : Nat.nat **) … … 178 178 179 179 (** val load_code_memory0 : 180 BitVector.byte List.list > BitVector.byte BitVectorTrie.bitVectorTrie 181 Types.sig0 **) 182 let load_code_memory0 program0 = 180 ASM.object_code > BitVector.byte BitVectorTrie.bitVectorTrie Types.sig0 **) 181 let load_code_memory0 program = 183 182 (Types.pi1 184 (FoldStuff.foldl_strong program 0 (fun prefix0v tl _ i_mem >185 (let { Types.fst = i; Types.snd = mem 1} = Types.pi1 i_mem in183 (FoldStuff.foldl_strong program (fun prefix v tl _ i_mem > 184 (let { Types.fst = i; Types.snd = mem } = Types.pi1 i_mem in 186 185 (fun _ > { Types.fst = (Nat.S i); Types.snd = 187 186 (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S … … 190 189 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 191 190 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 192 (Nat.S (Nat.S Nat.O)))))))))))))))) i) v mem 1) })) __)193 { Types.fst = Nat.O; Types.snd = (BitVectorTrie.Stub(Nat.S (Nat.S191 (Nat.S (Nat.S Nat.O)))))))))))))))) i) v mem) })) __) { Types.fst = 192 Nat.O; Types.snd = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S 194 193 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 195 (Nat.S (Nat.S (Nat.S (Nat.SNat.O))))))))))))))))) })).Types.snd194 (Nat.S (Nat.S Nat.O))))))))))))))))) })).Types.snd 196 195 197 196 (** val load_code_memory : 198 BitVector.byte List.list> BitVector.byte BitVectorTrie.bitVectorTrie **)199 let load_code_memory program 0=200 Types.pi1 (load_code_memory0 program 0)201 202 (** val prod_inv_rect_Type 5:197 ASM.object_code > BitVector.byte BitVectorTrie.bitVectorTrie **) 198 let load_code_memory program = 199 Types.pi1 (load_code_memory0 program) 200 201 (** val prod_inv_rect_Type0 : 203 202 ('a1, 'a2) Types.prod > ('a1 > 'a2 > __ > 'a3) > 'a3 **) 204 let prod_inv_rect_Type 5clearme =205 let { Types.fst = fst 0; Types.snd = snd0} = clearme in206 (fun auto > auto fst 0 snd0__)203 let prod_inv_rect_Type0 clearme = 204 let { Types.fst = fst; Types.snd = snd } = clearme in 205 (fun auto > auto fst snd __) 207 206 208 207 (** val fetch0 : … … 265 264 (match b6 with 266 265  Bool.True > 267 prod_inv_rect_Type 5(next pmem pc)266 prod_inv_rect_Type0 (next pmem pc) 268 267 (fun pc0 b10 _ > { Types.fst = { Types.fst = 269 268 (ASM.RealInstruction (ASM.MOV (Types.Inl … … 292 291 (match b6 with 293 292  Bool.True > 294 prod_inv_rect_Type 5(next pmem pc)293 prod_inv_rect_Type0 (next pmem pc) 295 294 (fun pc0 b10 _ > { Types.fst = { Types.fst = 296 295 (ASM.ACALL (ASM.ADDR11 297 (Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O)))296 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) 298 297 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 299 298 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons … … 342 341 (match b6 with 343 342  Bool.True > 344 prod_inv_rect_Type 5(next pmem pc)343 prod_inv_rect_Type0 (next pmem pc) 345 344 (fun pc0 b10 _ > { Types.fst = { Types.fst = 346 345 (ASM.RealInstruction (ASM.MOV (Types.Inl … … 370 369 (match b6 with 371 370  Bool.True > 372 prod_inv_rect_Type 5(next pmem pc)371 prod_inv_rect_Type0 (next pmem pc) 373 372 (fun pc0 b10 _ > { Types.fst = { Types.fst = 374 373 (ASM.AJMP (ASM.ADDR11 375 (Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O)))374 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) 376 375 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 377 376 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons … … 398 397 (match b3 with 399 398  Bool.True > 400 prod_inv_rect_Type 5(next pmem pc) (fun pc0 b10 _ >399 prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ > 401 400 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DJNZ 402 401 ((ASM.REGISTER v4), (ASM.RELATIVE b10)))); Types.snd = … … 423 422 (match b6 with 424 423  Bool.True > 425 prod_inv_rect_Type 5(next pmem pc)424 prod_inv_rect_Type0 (next pmem pc) 426 425 (fun pc0 b10 _ > 427 prod_inv_rect_Type 5(next pmem pc0)426 prod_inv_rect_Type0 (next pmem pc0) 428 427 (fun pc1 b20 _ > { Types.fst = { Types.fst = 429 428 (ASM.RealInstruction (ASM.DJNZ ((ASM.DIRECT … … 449 448 Types.snd = (Nat.S Nat.O) } 450 449  Bool.False > 451 prod_inv_rect_Type 5(next pmem pc)450 prod_inv_rect_Type0 (next pmem pc) 452 451 (fun pc0 b10 _ > { Types.fst = { Types.fst = 453 452 (ASM.RealInstruction (ASM.SETB (ASM.BIT_ADDR … … 460 459 (match b6 with 461 460  Bool.True > 462 prod_inv_rect_Type 5(next pmem pc)461 prod_inv_rect_Type0 (next pmem pc) 463 462 (fun pc0 b10 _ > { Types.fst = { Types.fst = 464 463 (ASM.ACALL (ASM.ADDR11 465 (Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O)))464 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) 466 465 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 467 466 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons … … 472 471 Types.snd = (Nat.S (Nat.S Nat.O)) }) 473 472  Bool.False > 474 prod_inv_rect_Type 5(next pmem pc)473 prod_inv_rect_Type0 (next pmem pc) 475 474 (fun pc0 b10 _ > { Types.fst = { Types.fst = 476 475 (ASM.RealInstruction (ASM.POP (ASM.DIRECT b10))); … … 507 506 (match b6 with 508 507  Bool.True > 509 prod_inv_rect_Type 5(next pmem pc)508 prod_inv_rect_Type0 (next pmem pc) 510 509 (fun pc0 b10 _ > { Types.fst = { Types.fst = 511 510 (ASM.RealInstruction (ASM.XCH (ASM.ACC_A, … … 531 530 Types.snd = (Nat.S Nat.O) } 532 531  Bool.False > 533 prod_inv_rect_Type 5(next pmem pc)532 prod_inv_rect_Type0 (next pmem pc) 534 533 (fun pc0 b10 _ > { Types.fst = { Types.fst = 535 534 (ASM.RealInstruction (ASM.CLR (ASM.BIT_ADDR … … 542 541 (match b6 with 543 542  Bool.True > 544 prod_inv_rect_Type 5(next pmem pc)543 prod_inv_rect_Type0 (next pmem pc) 545 544 (fun pc0 b10 _ > { Types.fst = { Types.fst = 546 545 (ASM.AJMP (ASM.ADDR11 547 (Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O)))546 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) 548 547 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 549 548 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons … … 554 553 Types.snd = (Nat.S (Nat.S Nat.O)) }) 555 554  Bool.False > 556 prod_inv_rect_Type 5(next pmem pc)555 prod_inv_rect_Type0 (next pmem pc) 557 556 (fun pc0 b10 _ > { Types.fst = { Types.fst = 558 557 (ASM.RealInstruction (ASM.PUSH (ASM.DIRECT … … 575 574 (match b3 with 576 575  Bool.True > 577 prod_inv_rect_Type 5(next pmem pc) (fun pc0 b10 _ >578 prod_inv_rect_Type 5(next pmem pc0) (fun pc1 b20 _ >576 prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ > 577 prod_inv_rect_Type0 (next pmem pc0) (fun pc1 b20 _ > 579 578 { Types.fst = { Types.fst = (ASM.RealInstruction 580 579 (ASM.CJNE ((Types.Inr { Types.fst = (ASM.REGISTER v4); … … 592 591 (match b5 with 593 592  Bool.True > 594 prod_inv_rect_Type 5(next pmem pc) (fun pc0 b10 _ >595 prod_inv_rect_Type 5(next pmem pc0)593 prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ > 594 prod_inv_rect_Type0 (next pmem pc0) 596 595 (fun pc1 b20 _ > { Types.fst = { Types.fst = 597 596 (ASM.RealInstruction (ASM.CJNE ((Types.Inr … … 606 605 (match b6 with 607 606  Bool.True > 608 prod_inv_rect_Type 5(next pmem pc)607 prod_inv_rect_Type0 (next pmem pc) 609 608 (fun pc0 b10 _ > 610 prod_inv_rect_Type 5(next pmem pc0)609 prod_inv_rect_Type0 (next pmem pc0) 611 610 (fun pc1 b20 _ > { Types.fst = { Types.fst = 612 611 (ASM.RealInstruction (ASM.CJNE ((Types.Inl … … 616 615 Nat.O)) })) 617 616  Bool.False > 618 prod_inv_rect_Type 5(next pmem pc)617 prod_inv_rect_Type0 (next pmem pc) 619 618 (fun pc0 b10 _ > 620 prod_inv_rect_Type 5(next pmem pc0)619 prod_inv_rect_Type0 (next pmem pc0) 621 620 (fun pc1 b20 _ > { Types.fst = { Types.fst = 622 621 (ASM.RealInstruction (ASM.CJNE ((Types.Inl … … 639 638 Types.snd = (Nat.S Nat.O) } 640 639  Bool.False > 641 prod_inv_rect_Type 5(next pmem pc)640 prod_inv_rect_Type0 (next pmem pc) 642 641 (fun pc0 b10 _ > { Types.fst = { Types.fst = 643 642 (ASM.RealInstruction (ASM.CPL (ASM.BIT_ADDR … … 650 649 (match b6 with 651 650  Bool.True > 652 prod_inv_rect_Type 5(next pmem pc)651 prod_inv_rect_Type0 (next pmem pc) 653 652 (fun pc0 b10 _ > { Types.fst = { Types.fst = 654 653 (ASM.ACALL (ASM.ADDR11 655 (Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O)))654 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) 656 655 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 657 656 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons … … 662 661 Types.snd = (Nat.S (Nat.S Nat.O)) }) 663 662  Bool.False > 664 prod_inv_rect_Type 5(next pmem pc)663 prod_inv_rect_Type0 (next pmem pc) 665 664 (fun pc0 b10 _ > { Types.fst = { Types.fst = 666 665 (ASM.RealInstruction (ASM.ANL (Types.Inr … … 674 673 (match b3 with 675 674  Bool.True > 676 prod_inv_rect_Type 5(next pmem pc) (fun pc0 b10 _ >675 prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ > 677 676 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV 678 677 (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr … … 691 690 (match b5 with 692 691  Bool.True > 693 prod_inv_rect_Type 5(next pmem pc) (fun pc0 b10 _ >692 prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ > 694 693 { Types.fst = { Types.fst = (ASM.RealInstruction 695 694 (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl … … 717 716 Types.snd = (Nat.S (Nat.S Nat.O)) } 718 717  Bool.False > 719 prod_inv_rect_Type 5(next pmem pc)718 prod_inv_rect_Type0 (next pmem pc) 720 719 (fun pc0 b10 _ > { Types.fst = { Types.fst = 721 720 (ASM.RealInstruction (ASM.MOV (Types.Inl … … 729 728 (match b6 with 730 729  Bool.True > 731 prod_inv_rect_Type 5(next pmem pc)730 prod_inv_rect_Type0 (next pmem pc) 732 731 (fun pc0 b10 _ > { Types.fst = { Types.fst = 733 732 (ASM.AJMP (ASM.ADDR11 734 (Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O)))733 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) 735 734 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 736 735 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons … … 741 740 Types.snd = (Nat.S (Nat.S Nat.O)) }) 742 741  Bool.False > 743 prod_inv_rect_Type 5(next pmem pc)742 prod_inv_rect_Type0 (next pmem pc) 744 743 (fun pc0 b10 _ > { Types.fst = { Types.fst = 745 744 (ASM.RealInstruction (ASM.ORL (Types.Inr … … 782 781 (match b6 with 783 782  Bool.True > 784 prod_inv_rect_Type 5(next pmem pc)783 prod_inv_rect_Type0 (next pmem pc) 785 784 (fun pc0 b10 _ > { Types.fst = { Types.fst = 786 785 (ASM.RealInstruction (ASM.SUBB (ASM.ACC_A, … … 788 787 Types.snd = (Nat.S Nat.O) }) 789 788  Bool.False > 790 prod_inv_rect_Type 5(next pmem pc)789 prod_inv_rect_Type0 (next pmem pc) 791 790 (fun pc0 b10 _ > { Types.fst = { Types.fst = 792 791 (ASM.RealInstruction (ASM.SUBB (ASM.ACC_A, … … 808 807 (Nat.S (Nat.S Nat.O)) } 809 808  Bool.False > 810 prod_inv_rect_Type 5(next pmem pc)809 prod_inv_rect_Type0 (next pmem pc) 811 810 (fun pc0 b10 _ > { Types.fst = { Types.fst = 812 811 (ASM.RealInstruction (ASM.MOV (Types.Inr … … 820 819 (match b6 with 821 820  Bool.True > 822 prod_inv_rect_Type 5(next pmem pc)821 prod_inv_rect_Type0 (next pmem pc) 823 822 (fun pc0 b10 _ > { Types.fst = { Types.fst = 824 823 (ASM.ACALL (ASM.ADDR11 825 (Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O)))824 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) 826 825 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 827 826 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons … … 832 831 Types.snd = (Nat.S (Nat.S Nat.O)) }) 833 832  Bool.False > 834 prod_inv_rect_Type 5(next pmem pc)833 prod_inv_rect_Type0 (next pmem pc) 835 834 (fun pc0 b10 _ > 836 prod_inv_rect_Type 5(next pmem pc0)835 prod_inv_rect_Type0 (next pmem pc0) 837 836 (fun pc1 b20 _ > { Types.fst = { Types.fst = 838 837 (ASM.RealInstruction (ASM.MOV (Types.Inl 839 838 (Types.Inl (Types.Inr { Types.fst = ASM.DPTR; 840 839 Types.snd = (ASM.DATA16 841 (Vector.append 0(Nat.S (Nat.S (Nat.S (Nat.S840 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S 842 841 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) 843 842 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S … … 851 850 (match b3 with 852 851  Bool.True > 853 prod_inv_rect_Type 5(next pmem pc) (fun pc0 b10 _ >852 prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ > 854 853 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV 855 854 (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = … … 867 866 (match b5 with 868 867  Bool.True > 869 prod_inv_rect_Type 5(next pmem pc) (fun pc0 b10 _ >868 prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ > 870 869 { Types.fst = { Types.fst = (ASM.RealInstruction 871 870 (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inr … … 880 879 (match b6 with 881 880  Bool.True > 882 prod_inv_rect_Type 5(next pmem pc)881 prod_inv_rect_Type0 (next pmem pc) 883 882 (fun pc0 b10 _ > 884 prod_inv_rect_Type 5(next pmem pc0)883 prod_inv_rect_Type0 (next pmem pc0) 885 884 (fun pc1 b20 _ > { Types.fst = { Types.fst = 886 885 (ASM.RealInstruction (ASM.MOV (Types.Inl … … 909 908 (Nat.S (Nat.S Nat.O)) } 910 909  Bool.False > 911 prod_inv_rect_Type 5(next pmem pc)910 prod_inv_rect_Type0 (next pmem pc) 912 911 (fun pc0 b10 _ > { Types.fst = { Types.fst = 913 912 (ASM.RealInstruction (ASM.ANL (Types.Inr … … 921 920 (match b6 with 922 921  Bool.True > 923 prod_inv_rect_Type 5(next pmem pc)922 prod_inv_rect_Type0 (next pmem pc) 924 923 (fun pc0 b10 _ > { Types.fst = { Types.fst = 925 924 (ASM.AJMP (ASM.ADDR11 926 (Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O)))925 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) 927 926 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 928 927 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons … … 933 932 Types.snd = (Nat.S (Nat.S Nat.O)) }) 934 933  Bool.False > 935 prod_inv_rect_Type 5(next pmem pc)934 prod_inv_rect_Type0 (next pmem pc) 936 935 (fun pc0 b10 _ > { Types.fst = { Types.fst = 937 936 (ASM.SJMP (ASM.RELATIVE b10)); Types.snd = pc0 }; … … 958 957 (match b3 with 959 958  Bool.True > 960 prod_inv_rect_Type 5(next pmem pc) (fun pc0 b10 _ >959 prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ > 961 960 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV 962 961 (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr … … 975 974 (match b5 with 976 975  Bool.True > 977 prod_inv_rect_Type 5(next pmem pc) (fun pc0 b10 _ >976 prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ > 978 977 { Types.fst = { Types.fst = (ASM.RealInstruction 979 978 (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl … … 988 987 (match b6 with 989 988  Bool.True > 990 prod_inv_rect_Type 5(next pmem pc)989 prod_inv_rect_Type0 (next pmem pc) 991 990 (fun pc0 b10 _ > 992 prod_inv_rect_Type 5(next pmem pc0)991 prod_inv_rect_Type0 (next pmem pc0) 993 992 (fun pc1 b20 _ > { Types.fst = { Types.fst = 994 993 (ASM.RealInstruction (ASM.MOV (Types.Inl … … 998 997 (Nat.S (Nat.S (Nat.S Nat.O))) })) 999 998  Bool.False > 1000 prod_inv_rect_Type 5(next pmem pc)999 prod_inv_rect_Type0 (next pmem pc) 1001 1000 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1002 1001 (ASM.RealInstruction (ASM.MOV (Types.Inl … … 1020 1019 Types.snd = (Nat.S (Nat.S Nat.O)) } 1021 1020  Bool.False > 1022 prod_inv_rect_Type 5(next pmem pc)1021 prod_inv_rect_Type0 (next pmem pc) 1023 1022 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1024 1023 (ASM.RealInstruction (ASM.ORL (Types.Inr … … 1032 1031 (match b6 with 1033 1032  Bool.True > 1034 prod_inv_rect_Type 5(next pmem pc)1033 prod_inv_rect_Type0 (next pmem pc) 1035 1034 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1036 1035 (ASM.ACALL (ASM.ADDR11 1037 (Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O)))1036 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) 1038 1037 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1039 1038 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons … … 1044 1043 Types.snd = (Nat.S (Nat.S Nat.O)) }) 1045 1044  Bool.False > 1046 prod_inv_rect_Type 5(next pmem pc)1045 prod_inv_rect_Type0 (next pmem pc) 1047 1046 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1048 1047 (ASM.RealInstruction (ASM.JNZ (ASM.RELATIVE … … 1081 1080 (match b6 with 1082 1081  Bool.True > 1083 prod_inv_rect_Type 5(next pmem pc)1082 prod_inv_rect_Type0 (next pmem pc) 1084 1083 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1085 1084 (ASM.RealInstruction (ASM.XRL (Types.Inl … … 1088 1087 Nat.O) }) 1089 1088  Bool.False > 1090 prod_inv_rect_Type 5(next pmem pc)1089 prod_inv_rect_Type0 (next pmem pc) 1091 1090 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1092 1091 (ASM.RealInstruction (ASM.XRL (Types.Inl … … 1105 1104 (match b6 with 1106 1105  Bool.True > 1107 prod_inv_rect_Type 5(next pmem pc)1106 prod_inv_rect_Type0 (next pmem pc) 1108 1107 (fun pc0 b10 _ > 1109 prod_inv_rect_Type 5(next pmem pc0)1108 prod_inv_rect_Type0 (next pmem pc0) 1110 1109 (fun pc1 b20 _ > { Types.fst = { Types.fst = 1111 1110 (ASM.RealInstruction (ASM.XRL (Types.Inr … … 1114 1113 Types.snd = (Nat.S (Nat.S Nat.O)) })) 1115 1114  Bool.False > 1116 prod_inv_rect_Type 5(next pmem pc)1115 prod_inv_rect_Type0 (next pmem pc) 1117 1116 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1118 1117 (ASM.RealInstruction (ASM.XRL (Types.Inr … … 1126 1125 (match b6 with 1127 1126  Bool.True > 1128 prod_inv_rect_Type 5(next pmem pc)1127 prod_inv_rect_Type0 (next pmem pc) 1129 1128 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1130 1129 (ASM.AJMP (ASM.ADDR11 1131 (Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O)))1130 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) 1132 1131 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1133 1132 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons … … 1138 1137 Types.snd = (Nat.S (Nat.S Nat.O)) }) 1139 1138  Bool.False > 1140 prod_inv_rect_Type 5(next pmem pc)1139 prod_inv_rect_Type0 (next pmem pc) 1141 1140 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1142 1141 (ASM.RealInstruction (ASM.JZ (ASM.RELATIVE … … 1180 1179 (match b6 with 1181 1180  Bool.True > 1182 prod_inv_rect_Type 5(next pmem pc)1181 prod_inv_rect_Type0 (next pmem pc) 1183 1182 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1184 1183 (ASM.RealInstruction (ASM.ANL (Types.Inl … … 1187 1186 Types.snd = (Nat.S Nat.O) }) 1188 1187  Bool.False > 1189 prod_inv_rect_Type 5(next pmem pc)1188 prod_inv_rect_Type0 (next pmem pc) 1190 1189 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1191 1190 (ASM.RealInstruction (ASM.ANL (Types.Inl … … 1204 1203 (match b6 with 1205 1204  Bool.True > 1206 prod_inv_rect_Type 5(next pmem pc)1205 prod_inv_rect_Type0 (next pmem pc) 1207 1206 (fun pc0 b10 _ > 1208 prod_inv_rect_Type 5(next pmem pc0)1207 prod_inv_rect_Type0 (next pmem pc0) 1209 1208 (fun pc1 b20 _ > { Types.fst = { Types.fst = 1210 1209 (ASM.RealInstruction (ASM.ANL (Types.Inl … … 1213 1212 pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) })) 1214 1213  Bool.False > 1215 prod_inv_rect_Type 5(next pmem pc)1214 prod_inv_rect_Type0 (next pmem pc) 1216 1215 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1217 1216 (ASM.RealInstruction (ASM.ANL (Types.Inl … … 1225 1224 (match b6 with 1226 1225  Bool.True > 1227 prod_inv_rect_Type 5(next pmem pc)1226 prod_inv_rect_Type0 (next pmem pc) 1228 1227 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1229 1228 (ASM.ACALL (ASM.ADDR11 1230 (Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O)))1229 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) 1231 1230 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1232 1231 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons … … 1237 1236 Types.snd = (Nat.S (Nat.S Nat.O)) }) 1238 1237  Bool.False > 1239 prod_inv_rect_Type 5(next pmem pc)1238 prod_inv_rect_Type0 (next pmem pc) 1240 1239 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1241 1240 (ASM.RealInstruction (ASM.JNC (ASM.RELATIVE … … 1274 1273 (match b6 with 1275 1274  Bool.True > 1276 prod_inv_rect_Type 5(next pmem pc)1275 prod_inv_rect_Type0 (next pmem pc) 1277 1276 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1278 1277 (ASM.RealInstruction (ASM.ORL (Types.Inl … … 1281 1280 Types.snd = (Nat.S Nat.O) }) 1282 1281  Bool.False > 1283 prod_inv_rect_Type 5(next pmem pc)1282 prod_inv_rect_Type0 (next pmem pc) 1284 1283 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1285 1284 (ASM.RealInstruction (ASM.ORL (Types.Inl … … 1298 1297 (match b6 with 1299 1298  Bool.True > 1300 prod_inv_rect_Type 5(next pmem pc)1299 prod_inv_rect_Type0 (next pmem pc) 1301 1300 (fun pc0 b10 _ > 1302 prod_inv_rect_Type 5(next pmem pc0)1301 prod_inv_rect_Type0 (next pmem pc0) 1303 1302 (fun pc1 b20 _ > { Types.fst = { Types.fst = 1304 1303 (ASM.RealInstruction (ASM.ORL (Types.Inl … … 1307 1306 pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) })) 1308 1307  Bool.False > 1309 prod_inv_rect_Type 5(next pmem pc)1308 prod_inv_rect_Type0 (next pmem pc) 1310 1309 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1311 1310 (ASM.RealInstruction (ASM.ORL (Types.Inl … … 1319 1318 (match b6 with 1320 1319  Bool.True > 1321 prod_inv_rect_Type 5(next pmem pc)1320 prod_inv_rect_Type0 (next pmem pc) 1322 1321 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1323 1322 (ASM.AJMP (ASM.ADDR11 1324 (Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O)))1323 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) 1325 1324 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1326 1325 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons … … 1331 1330 Types.snd = (Nat.S (Nat.S Nat.O)) }) 1332 1331  Bool.False > 1333 prod_inv_rect_Type 5(next pmem pc)1332 prod_inv_rect_Type0 (next pmem pc) 1334 1333 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1335 1334 (ASM.RealInstruction (ASM.JC (ASM.RELATIVE … … 1376 1375 (match b6 with 1377 1376  Bool.True > 1378 prod_inv_rect_Type 5(next pmem pc)1377 prod_inv_rect_Type0 (next pmem pc) 1379 1378 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1380 1379 (ASM.RealInstruction (ASM.ADDC (ASM.ACC_A, … … 1382 1381 Types.snd = (Nat.S Nat.O) }) 1383 1382  Bool.False > 1384 prod_inv_rect_Type 5(next pmem pc)1383 prod_inv_rect_Type0 (next pmem pc) 1385 1384 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1386 1385 (ASM.RealInstruction (ASM.ADDC (ASM.ACC_A, … … 1411 1410 (match b6 with 1412 1411  Bool.True > 1413 prod_inv_rect_Type 5(next pmem pc)1412 prod_inv_rect_Type0 (next pmem pc) 1414 1413 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1415 1414 (ASM.ACALL (ASM.ADDR11 1416 (Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O)))1415 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) 1417 1416 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1418 1417 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons … … 1423 1422 Types.snd = (Nat.S (Nat.S Nat.O)) }) 1424 1423  Bool.False > 1425 prod_inv_rect_Type 5(next pmem pc)1424 prod_inv_rect_Type0 (next pmem pc) 1426 1425 (fun pc0 b10 _ > 1427 prod_inv_rect_Type 5(next pmem pc0)1426 prod_inv_rect_Type0 (next pmem pc0) 1428 1427 (fun pc1 b20 _ > { Types.fst = { Types.fst = 1429 1428 (ASM.RealInstruction (ASM.JNB ((ASM.BIT_ADDR … … 1460 1459 (match b6 with 1461 1460  Bool.True > 1462 prod_inv_rect_Type 5(next pmem pc)1461 prod_inv_rect_Type0 (next pmem pc) 1463 1462 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1464 1463 (ASM.RealInstruction (ASM.ADD (ASM.ACC_A, … … 1466 1465 Types.snd = (Nat.S Nat.O) }) 1467 1466  Bool.False > 1468 prod_inv_rect_Type 5(next pmem pc)1467 prod_inv_rect_Type0 (next pmem pc) 1469 1468 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1470 1469 (ASM.RealInstruction (ASM.ADD (ASM.ACC_A, … … 1495 1494 (match b6 with 1496 1495  Bool.True > 1497 prod_inv_rect_Type 5(next pmem pc)1496 prod_inv_rect_Type0 (next pmem pc) 1498 1497 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1499 1498 (ASM.AJMP (ASM.ADDR11 1500 (Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O)))1499 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) 1501 1500 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1502 1501 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons … … 1507 1506 Types.snd = (Nat.S (Nat.S Nat.O)) }) 1508 1507  Bool.False > 1509 prod_inv_rect_Type 5(next pmem pc)1508 prod_inv_rect_Type0 (next pmem pc) 1510 1509 (fun pc0 b10 _ > 1511 prod_inv_rect_Type 5(next pmem pc0)1510 prod_inv_rect_Type0 (next pmem pc0) 1512 1511 (fun pc1 b20 _ > { Types.fst = { Types.fst = 1513 1512 (ASM.RealInstruction (ASM.JB ((ASM.BIT_ADDR … … 1548 1547 (match b6 with 1549 1548  Bool.True > 1550 prod_inv_rect_Type 5(next pmem pc)1549 prod_inv_rect_Type0 (next pmem pc) 1551 1550 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1552 1551 (ASM.RealInstruction (ASM.DEC (ASM.DIRECT b10))); … … 1571 1570 Types.snd = (Nat.S Nat.O) } 1572 1571  Bool.False > 1573 prod_inv_rect_Type 5(next pmem pc)1572 prod_inv_rect_Type0 (next pmem pc) 1574 1573 (fun pc0 b10 _ > 1575 prod_inv_rect_Type 5(next pmem pc0)1574 prod_inv_rect_Type0 (next pmem pc0) 1576 1575 (fun pc1 b20 _ > { Types.fst = { Types.fst = 1577 1576 (ASM.LCALL (ASM.ADDR16 1578 (Vector.append 0(Nat.S (Nat.S (Nat.S (Nat.S1577 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S 1579 1578 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) 1580 1579 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S … … 1588 1587 (match b6 with 1589 1588  Bool.True > 1590 prod_inv_rect_Type 5(next pmem pc)1589 prod_inv_rect_Type0 (next pmem pc) 1591 1590 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1592 1591 (ASM.ACALL (ASM.ADDR11 1593 (Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O)))1592 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) 1594 1593 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1595 1594 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons … … 1600 1599 Types.snd = (Nat.S (Nat.S Nat.O)) }) 1601 1600  Bool.False > 1602 prod_inv_rect_Type 5(next pmem pc)1601 prod_inv_rect_Type0 (next pmem pc) 1603 1602 (fun pc0 b10 _ > 1604 prod_inv_rect_Type 5(next pmem pc0)1603 prod_inv_rect_Type0 (next pmem pc0) 1605 1604 (fun pc1 b20 _ > { Types.fst = { Types.fst = 1606 1605 (ASM.RealInstruction (ASM.JBC ((ASM.BIT_ADDR … … 1636 1635 (match b6 with 1637 1636  Bool.True > 1638 prod_inv_rect_Type 5(next pmem pc)1637 prod_inv_rect_Type0 (next pmem pc) 1639 1638 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1640 1639 (ASM.RealInstruction (ASM.INC (ASM.DIRECT b10))); … … 1659 1658 Types.snd = (Nat.S Nat.O) } 1660 1659  Bool.False > 1661 prod_inv_rect_Type 5(next pmem pc)1660 prod_inv_rect_Type0 (next pmem pc) 1662 1661 (fun pc0 b10 _ > 1663 prod_inv_rect_Type 5(next pmem pc0)1662 prod_inv_rect_Type0 (next pmem pc0) 1664 1663 (fun pc1 b20 _ > { Types.fst = { Types.fst = 1665 1664 (ASM.LJMP (ASM.ADDR16 1666 (Vector.append 0(Nat.S (Nat.S (Nat.S (Nat.S1665 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S 1667 1666 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) 1668 1667 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S … … 1676 1675 (match b6 with 1677 1676  Bool.True > 1678 prod_inv_rect_Type 5(next pmem pc)1677 prod_inv_rect_Type0 (next pmem pc) 1679 1678 (fun pc0 b10 _ > { Types.fst = { Types.fst = 1680 1679 (ASM.AJMP (ASM.ADDR11 1681 (Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O)))1680 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) 1682 1681 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1683 1682 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons … … 1696 1695 ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod **) 1697 1696 let fetch pmem pc = 1698 let { Types.fst = word 0; Types.snd = byte0} = next pmem pc in1699 fetch0 pmem word 0 byte01700 1697 let { Types.fst = word; Types.snd = byte } = next pmem pc in 1698 fetch0 pmem word byte 1699
Note: See TracChangeset
for help on using the changeset viewer.