Changeset 3069
 Timestamp:
 Apr 2, 2013, 2:09:34 PM (4 years ago)
 Location:
 extracted
 Files:

 6 edited
Legend:
 Unmodified
 Added
 Removed

extracted/assembly.ml
r3065 r3069 2644 2644  ASM.JMP arg > List.Cons ((ASM.RealInstruction (ASM.JMP arg)), List.Nil) 2645 2645 2646 (** val is_code : AST.region > Bool.bool **) 2647 let is_code = function 2648  AST.XData > Bool.False 2649  AST.Code > Bool.True 2650 2646 2651 (** val expand_pseudo_instruction : 2647 2652 (ASM.identifier > BitVector.word) > (BitVector.word > BitVector.word) 2648 2653 > (BitVector.word > Bool.bool) > BitVector.word > (ASM.identifier > 2649 BitVector.word) > ASM.pseudo_instruction > ASM.instruction List.list **) 2654 (AST.region, BitVector.word) Types.prod) > ASM.pseudo_instruction > 2655 ASM.instruction List.list **) 2650 2656 let expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels = function 2651 2657  ASM.Instruction instr > … … 2714 2720 List.Cons ((ASM.LCALL address), List.Nil)) 2715 2721  ASM.Mov (d, trgt, off) > 2716 let addr = 2717 (Arithmetic.add_16_with_carry (lookup_datalabels trgt) off Bool.False).Types.fst 2722 let { Types.fst = r; Types.snd = addr } = lookup_datalabels trgt in 2723 let addr0 = (Arithmetic.add_16_with_carry addr off Bool.False).Types.fst in 2724 let addr1 = 2725 match is_code r with 2726  Bool.True > sigma addr0 2727  Bool.False > addr0 2718 2728 in 2719 2729 (match d with 2720 2730  Types.Inl x > 2721 let address = ASM.DATA16 addr in2731 let address = ASM.DATA16 addr1 in 2722 2732 List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl 2723 2733 (Types.Inr { Types.fst = ASM.DPTR; Types.snd = address }))))), List.Nil) … … 2728 2738 (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 2729 2739 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 2730 (Nat.S (Nat.S Nat.O)))))))) addr ).Types.fst2740 (Nat.S (Nat.S Nat.O)))))))) addr1).Types.fst 2731 2741  ASM.LOW > 2732 2742 (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 2733 2743 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 2734 (Nat.S (Nat.S Nat.O)))))))) addr ).Types.snd)2744 (Nat.S (Nat.S Nat.O)))))))) addr1).Types.snd) 2735 2745 in 2736 2746 (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons … … 2744 2754  ASM.INDIRECT x > (fun _ > assert false (* absurd case *)) 2745 2755  ASM.EXT_INDIRECT x > (fun _ > assert false (* absurd case *)) 2746  ASM.REGISTER r >2756  ASM.REGISTER r0 > 2747 2757 (fun _ > List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl 2748 2758 (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = 2749 (ASM.REGISTER r ); Types.snd = v }))))))), List.Nil))2759 (ASM.REGISTER r0); Types.snd = v }))))))), List.Nil)) 2750 2760  ASM.ACC_A > 2751 2761 (fun _ > List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl … … 2770 2780 (ASM.identifier > BitVector.word) > (BitVector.word > BitVector.word) 2771 2781 > (BitVector.word > Bool.bool) > BitVector.word > (ASM.identifier > 2772 BitVector.word) > ASM.pseudo_instruction > (Nat.nat, Bool.bool2773 Vector.vector List.list) Types.prod **)2782 (AST.region, BitVector.word) Types.prod) > ASM.pseudo_instruction > 2783 (Nat.nat, Bool.bool Vector.vector List.list) Types.prod **) 2774 2784 let assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels i = 2775 2785 let pseudos = … … 2783 2793 2784 2794 (** val instruction_size : 2785 (ASM.identifier > BitVector.word) > (ASM.identifier > BitVector.word) 2786 > (BitVector.word > BitVector.word) > (BitVector.word > Bool.bool) > 2787 BitVector.word > ASM.pseudo_instruction > Nat.nat **) 2795 (ASM.identifier > BitVector.word) > (ASM.identifier > (AST.region, 2796 BitVector.word) Types.prod) > (BitVector.word > BitVector.word) > 2797 (BitVector.word > Bool.bool) > BitVector.word > ASM.pseudo_instruction 2798 > Nat.nat **) 2788 2799 let instruction_size lookup_labels lookup_datalabels sigma policy ppc i = 2789 2800 (assembly_1_pseudoinstruction lookup_labels sigma policy ppc … … 2808 2819 in 2809 2820 let lookup_datalabels = fun x > 2810 Identifiers.lookup_def PreIdentifiers.ASMTag datalabels x 2811 (sigma (lookup_labels x)) 2821 match Identifiers.lookup PreIdentifiers.ASMTag 2822 (Status.construct_datalabels preamble) x with 2823  Types.None > { Types.fst = AST.Code; Types.snd = (lookup_labels x) } 2824  Types.Some addr > { Types.fst = AST.XData; Types.snd = addr } 2812 2825 in 2813 2826 (let { Types.fst = next_pc; Types.snd = revcode } = 
extracted/assembly.mli
r3065 r3069 144 144 ASM.preinstruction > ASM.instruction List.list 145 145 146 val is_code : AST.region > Bool.bool 147 146 148 val expand_pseudo_instruction : 147 149 (ASM.identifier > BitVector.word) > (BitVector.word > BitVector.word) > 148 150 (BitVector.word > Bool.bool) > BitVector.word > (ASM.identifier > 149 BitVector.word) > ASM.pseudo_instruction > ASM.instruction List.list 151 (AST.region, BitVector.word) Types.prod) > ASM.pseudo_instruction > 152 ASM.instruction List.list 150 153 151 154 val assembly_1_pseudoinstruction : 152 155 (ASM.identifier > BitVector.word) > (BitVector.word > BitVector.word) > 153 156 (BitVector.word > Bool.bool) > BitVector.word > (ASM.identifier > 154 BitVector.word) > ASM.pseudo_instruction > (Nat.nat, Bool.bool155 Vector.vector List.list) Types.prod157 (AST.region, BitVector.word) Types.prod) > ASM.pseudo_instruction > 158 (Nat.nat, Bool.bool Vector.vector List.list) Types.prod 156 159 157 160 val instruction_size : 158 (ASM.identifier > BitVector.word) > (ASM.identifier > BitVector.word) > 159 (BitVector.word > BitVector.word) > (BitVector.word > Bool.bool) > 160 BitVector.word > ASM.pseudo_instruction > Nat.nat 161 (ASM.identifier > BitVector.word) > (ASM.identifier > (AST.region, 162 BitVector.word) Types.prod) > (BitVector.word > BitVector.word) > 163 (BitVector.word > Bool.bool) > BitVector.word > ASM.pseudo_instruction 164 > Nat.nat 161 165 162 166 val assembly : 
extracted/interpret.ml
r3064 r3069 1631 1631  Types.Inr r'' > 1632 1632 let { Types.fst = addr1; Types.snd = addr2 } = r'' in 1633 Status.set_arg_16 cm s0 (Status.get_arg_16 cm s0 addr2) addr1) 1633 Status.set_arg_16 cm s0 1634 (Status.get_arg_16 cm s0 1635 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O 1636 (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Data16, 1637 Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O), 1638 ASM.Data16, (Vector.VCons (Nat.O, ASM.Acc_dptr, 1639 Vector.VEmpty)))) addr2)) addr1) 1634 1640  Types.Inr r > 1635 1641 let { Types.fst = addr1; Types.snd = addr2 } = r in … … 1930 1936 Status.set_program_counter cm s2 new_pc) 1931 1937  ASM.NOP > (fun _ > let s0 = add_ticks1 s in s0) 1932  ASM.JMP x > 1933 (fun _ > 1934 let s0 = add_ticks1 s in 1935 let dptr = 1936 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1937 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1938 (Nat.S (Nat.S Nat.O)))))))) 1939 (Status.get_8051_sfr cm s0 Status.SFR_DPH) 1940 (Status.get_8051_sfr cm s0 Status.SFR_DPL) 1941 in 1942 let big_acc = 1943 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1944 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1945 (Nat.S (Nat.S Nat.O)))))))) 1946 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1947 (Nat.S Nat.O))))))))) 1948 (Status.get_8051_sfr cm s0 Status.SFR_ACC_A) 1949 in 1938  ASM.JMP acc_dptr > 1939 (fun _ > 1940 let s0 = add_ticks1 s in 1950 1941 let jmp_addr = 1951 Arithmetic.add 1952 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1953 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1954 (Nat.S Nat.O))))))))) big_acc dptr 1942 Status.get_arg_16 cm s0 1943 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S 1944 Nat.O) (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty)) 1945 (Vector.VCons ((Nat.S Nat.O), ASM.Data16, (Vector.VCons (Nat.O, 1946 ASM.Acc_dptr, Vector.VEmpty)))) acc_dptr) 1955 1947 in 1956 1948 Status.set_program_counter cm s0 jmp_addr)) __ … … 3501 3493  Types.Inr r'' > 3502 3494 let { Types.fst = addr1; Types.snd = addr2 } = r'' in 3503 Status.set_arg_16 cm s0 (Status.get_arg_16 cm s0 addr2) addr1) 3495 Status.set_arg_16 cm s0 3496 (Status.get_arg_16 cm s0 3497 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O 3498 (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Data16, 3499 Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O), 3500 ASM.Data16, (Vector.VCons (Nat.O, ASM.Acc_dptr, 3501 Vector.VEmpty)))) addr2)) addr1) 3504 3502  Types.Inr r > 3505 3503 let { Types.fst = addr1; Types.snd = addr2 } = r in … … 3816 3814 Status.set_program_counter cm s2 new_pc)) __)) __) 3817 3815  ASM.NOP > (fun _ > let s0 = add_ticks2 s in s0) 3818  ASM.JMP x > 3819 (fun _ > 3820 let s0 = add_ticks1 s in 3821 let dptr = 3822 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3823 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3824 (Nat.S (Nat.S Nat.O)))))))) 3825 (Status.get_8051_sfr cm s0 Status.SFR_DPH) 3826 (Status.get_8051_sfr cm s0 Status.SFR_DPL) 3827 in 3828 let big_acc = 3829 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3830 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3831 (Nat.S (Nat.S Nat.O)))))))) 3832 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3833 (Nat.S Nat.O))))))))) 3834 (Status.get_8051_sfr cm s0 Status.SFR_ACC_A) 3835 in 3816  ASM.JMP acc_dptr > 3817 (fun _ > 3818 let s0 = add_ticks1 s in 3836 3819 let jmp_addr = 3837 Arithmetic.add 3838 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3839 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3840 (Nat.S Nat.O))))))))) big_acc dptr 3841 in 3842 let new_pc = 3843 Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3844 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3845 Nat.O)))))))))))))))) s0.Status.program_counter jmp_addr 3846 in 3847 Status.set_program_counter cm s0 new_pc)) __ 3820 Status.get_arg_16 cm s0 3821 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S 3822 Nat.O) (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty)) 3823 (Vector.VCons ((Nat.S Nat.O), ASM.Data16, (Vector.VCons (Nat.O, 3824 ASM.Acc_dptr, Vector.VEmpty)))) acc_dptr) 3825 in 3826 Status.set_program_counter cm s0 jmp_addr)) __ 3848 3827 3849 3828 (** val compute_target_of_unconditional_jump : 
extracted/lINToASM.ml
r3059 r3069 140 140 Identifiers.identifier_map > ASM.identifier Identifiers.identifier_map 141 141 Identifiers.identifier_map > Positive.pos > 'a1) > aSM_universe > 'a1 **) 142 let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_ 21483=142 let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_588 = 143 143 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 144 144 ident_map0; label_map = label_map0; fresh_cost_label = 145 fresh_cost_label0 } = x_ 21483145 fresh_cost_label0 } = x_588 146 146 in 147 147 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 152 152 Identifiers.identifier_map > ASM.identifier Identifiers.identifier_map 153 153 Identifiers.identifier_map > Positive.pos > 'a1) > aSM_universe > 'a1 **) 154 let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_ 21485=154 let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_590 = 155 155 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 156 156 ident_map0; label_map = label_map0; fresh_cost_label = 157 fresh_cost_label0 } = x_ 21485157 fresh_cost_label0 } = x_590 158 158 in 159 159 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 164 164 Identifiers.identifier_map > ASM.identifier Identifiers.identifier_map 165 165 Identifiers.identifier_map > Positive.pos > 'a1) > aSM_universe > 'a1 **) 166 let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_ 21487=166 let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_592 = 167 167 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 168 168 ident_map0; label_map = label_map0; fresh_cost_label = 169 fresh_cost_label0 } = x_ 21487169 fresh_cost_label0 } = x_592 170 170 in 171 171 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 176 176 Identifiers.identifier_map > ASM.identifier Identifiers.identifier_map 177 177 Identifiers.identifier_map > Positive.pos > 'a1) > aSM_universe > 'a1 **) 178 let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_ 21489=178 let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_594 = 179 179 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 180 180 ident_map0; label_map = label_map0; fresh_cost_label = 181 fresh_cost_label0 } = x_ 21489181 fresh_cost_label0 } = x_594 182 182 in 183 183 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 188 188 Identifiers.identifier_map > ASM.identifier Identifiers.identifier_map 189 189 Identifiers.identifier_map > Positive.pos > 'a1) > aSM_universe > 'a1 **) 190 let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_ 21491=190 let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_596 = 191 191 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 192 192 ident_map0; label_map = label_map0; fresh_cost_label = 193 fresh_cost_label0 } = x_ 21491193 fresh_cost_label0 } = x_596 194 194 in 195 195 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 200 200 Identifiers.identifier_map > ASM.identifier Identifiers.identifier_map 201 201 Identifiers.identifier_map > Positive.pos > 'a1) > aSM_universe > 'a1 **) 202 let rec aSM_universe_rect_Type0 h_mk_ASM_universe x_ 21493=202 let rec aSM_universe_rect_Type0 h_mk_ASM_universe x_598 = 203 203 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 204 204 ident_map0; label_map = label_map0; fresh_cost_label = 205 fresh_cost_label0 } = x_ 21493205 fresh_cost_label0 } = x_598 206 206 in 207 207 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 303 303 (Identifiers.empty_map PreIdentifiers.LabelTag) 304 304 in 305 let { Types.fst = eta 28616; Types.snd = lmap0 } =305 let { Types.fst = eta154; Types.snd = lmap0 } = 306 306 match Identifiers.lookup PreIdentifiers.LabelTag lmap l with 307 307  Types.None > … … 315 315 lmap } 316 316 in 317 let { Types.fst = id; Types.snd = univ } = eta 28616in317 let { Types.fst = id; Types.snd = univ } = eta154 in 318 318 { Types.fst = { id_univ = univ; current_funct = current; ident_map = 319 319 u.ident_map; label_map = … … 1040 1040 Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil) 1041 1041 1042 type init_mutable = { virtual_dptr : Z.z; actual_dptr : Z.z; 1042 type init_mutable = { virtual_dptr : (ASM.identifier, Z.z) Types.prod; 1043 actual_dptr : (ASM.identifier, Z.z) Types.prod; 1043 1044 built_code : ASM.labelled_instruction List.list 1044 1045 List.list; … … 1047 1048 1048 1049 (** val init_mutable_rect_Type4 : 1049 ( Z.z > Z.z > ASM.labelled_instruction List.list List.list>1050 (ASM.identifier, BitVector.word) Types.prod List.list > 'a1) >1051 init_mutable > 'a1 **)1052 let rec init_mutable_rect_Type4 h_mk_init_mutable x_ 21509=1050 ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) Types.prod > 1051 ASM.labelled_instruction List.list List.list > (ASM.identifier, 1052 BitVector.word) Types.prod List.list > 'a1) > init_mutable > 'a1 **) 1053 let rec init_mutable_rect_Type4 h_mk_init_mutable x_614 = 1053 1054 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; 1054 built_code = built_code0; built_preamble = built_preamble0 } = x_ 215091055 built_code = built_code0; built_preamble = built_preamble0 } = x_614 1055 1056 in 1056 1057 h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 1057 1058 1058 1059 (** val init_mutable_rect_Type5 : 1059 ( Z.z > Z.z > ASM.labelled_instruction List.list List.list>1060 (ASM.identifier, BitVector.word) Types.prod List.list > 'a1) >1061 init_mutable > 'a1 **)1062 let rec init_mutable_rect_Type5 h_mk_init_mutable x_ 21511=1060 ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) Types.prod > 1061 ASM.labelled_instruction List.list List.list > (ASM.identifier, 1062 BitVector.word) Types.prod List.list > 'a1) > init_mutable > 'a1 **) 1063 let rec init_mutable_rect_Type5 h_mk_init_mutable x_616 = 1063 1064 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; 1064 built_code = built_code0; built_preamble = built_preamble0 } = x_ 215111065 built_code = built_code0; built_preamble = built_preamble0 } = x_616 1065 1066 in 1066 1067 h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 1067 1068 1068 1069 (** val init_mutable_rect_Type3 : 1069 ( Z.z > Z.z > ASM.labelled_instruction List.list List.list>1070 (ASM.identifier, BitVector.word) Types.prod List.list > 'a1) >1071 init_mutable > 'a1 **)1072 let rec init_mutable_rect_Type3 h_mk_init_mutable x_ 21513=1070 ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) Types.prod > 1071 ASM.labelled_instruction List.list List.list > (ASM.identifier, 1072 BitVector.word) Types.prod List.list > 'a1) > init_mutable > 'a1 **) 1073 let rec init_mutable_rect_Type3 h_mk_init_mutable x_618 = 1073 1074 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; 1074 built_code = built_code0; built_preamble = built_preamble0 } = x_ 215131075 built_code = built_code0; built_preamble = built_preamble0 } = x_618 1075 1076 in 1076 1077 h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 1077 1078 1078 1079 (** val init_mutable_rect_Type2 : 1079 ( Z.z > Z.z > ASM.labelled_instruction List.list List.list>1080 (ASM.identifier, BitVector.word) Types.prod List.list > 'a1) >1081 init_mutable > 'a1 **)1082 let rec init_mutable_rect_Type2 h_mk_init_mutable x_ 21515=1080 ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) Types.prod > 1081 ASM.labelled_instruction List.list List.list > (ASM.identifier, 1082 BitVector.word) Types.prod List.list > 'a1) > init_mutable > 'a1 **) 1083 let rec init_mutable_rect_Type2 h_mk_init_mutable x_620 = 1083 1084 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; 1084 built_code = built_code0; built_preamble = built_preamble0 } = x_ 215151085 built_code = built_code0; built_preamble = built_preamble0 } = x_620 1085 1086 in 1086 1087 h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 1087 1088 1088 1089 (** val init_mutable_rect_Type1 : 1089 ( Z.z > Z.z > ASM.labelled_instruction List.list List.list>1090 (ASM.identifier, BitVector.word) Types.prod List.list > 'a1) >1091 init_mutable > 'a1 **)1092 let rec init_mutable_rect_Type1 h_mk_init_mutable x_ 21517=1090 ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) Types.prod > 1091 ASM.labelled_instruction List.list List.list > (ASM.identifier, 1092 BitVector.word) Types.prod List.list > 'a1) > init_mutable > 'a1 **) 1093 let rec init_mutable_rect_Type1 h_mk_init_mutable x_622 = 1093 1094 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; 1094 built_code = built_code0; built_preamble = built_preamble0 } = x_ 215171095 built_code = built_code0; built_preamble = built_preamble0 } = x_622 1095 1096 in 1096 1097 h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 1097 1098 1098 1099 (** val init_mutable_rect_Type0 : 1099 ( Z.z > Z.z > ASM.labelled_instruction List.list List.list>1100 (ASM.identifier, BitVector.word) Types.prod List.list > 'a1) >1101 init_mutable > 'a1 **)1102 let rec init_mutable_rect_Type0 h_mk_init_mutable x_ 21519=1100 ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) Types.prod > 1101 ASM.labelled_instruction List.list List.list > (ASM.identifier, 1102 BitVector.word) Types.prod List.list > 'a1) > init_mutable > 'a1 **) 1103 let rec init_mutable_rect_Type0 h_mk_init_mutable x_624 = 1103 1104 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; 1104 built_code = built_code0; built_preamble = built_preamble0 } = x_ 215191105 built_code = built_code0; built_preamble = built_preamble0 } = x_624 1105 1106 in 1106 1107 h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 1107 1108 1108 (** val virtual_dptr : init_mutable > Z.z**)1109 (** val virtual_dptr : init_mutable > (ASM.identifier, Z.z) Types.prod **) 1109 1110 let rec virtual_dptr xxx = 1110 1111 xxx.virtual_dptr 1111 1112 1112 (** val actual_dptr : init_mutable > Z.z**)1113 (** val actual_dptr : init_mutable > (ASM.identifier, Z.z) Types.prod **) 1113 1114 let rec actual_dptr xxx = 1114 1115 xxx.actual_dptr … … 1125 1126 1126 1127 (** val init_mutable_inv_rect_Type4 : 1127 init_mutable > (Z.z > Z.z > ASM.labelled_instruction List.list 1128 List.list > (ASM.identifier, BitVector.word) Types.prod List.list > __ 1129 > 'a1) > 'a1 **) 1128 init_mutable > ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, 1129 Z.z) Types.prod > ASM.labelled_instruction List.list List.list > 1130 (ASM.identifier, BitVector.word) Types.prod List.list > __ > 'a1) > 1131 'a1 **) 1130 1132 let init_mutable_inv_rect_Type4 hterm h1 = 1131 1133 let hcut = init_mutable_rect_Type4 h1 hterm in hcut __ 1132 1134 1133 1135 (** val init_mutable_inv_rect_Type3 : 1134 init_mutable > (Z.z > Z.z > ASM.labelled_instruction List.list 1135 List.list > (ASM.identifier, BitVector.word) Types.prod List.list > __ 1136 > 'a1) > 'a1 **) 1136 init_mutable > ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, 1137 Z.z) Types.prod > ASM.labelled_instruction List.list List.list > 1138 (ASM.identifier, BitVector.word) Types.prod List.list > __ > 'a1) > 1139 'a1 **) 1137 1140 let init_mutable_inv_rect_Type3 hterm h1 = 1138 1141 let hcut = init_mutable_rect_Type3 h1 hterm in hcut __ 1139 1142 1140 1143 (** val init_mutable_inv_rect_Type2 : 1141 init_mutable > (Z.z > Z.z > ASM.labelled_instruction List.list 1142 List.list > (ASM.identifier, BitVector.word) Types.prod List.list > __ 1143 > 'a1) > 'a1 **) 1144 init_mutable > ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, 1145 Z.z) Types.prod > ASM.labelled_instruction List.list List.list > 1146 (ASM.identifier, BitVector.word) Types.prod List.list > __ > 'a1) > 1147 'a1 **) 1144 1148 let init_mutable_inv_rect_Type2 hterm h1 = 1145 1149 let hcut = init_mutable_rect_Type2 h1 hterm in hcut __ 1146 1150 1147 1151 (** val init_mutable_inv_rect_Type1 : 1148 init_mutable > (Z.z > Z.z > ASM.labelled_instruction List.list 1149 List.list > (ASM.identifier, BitVector.word) Types.prod List.list > __ 1150 > 'a1) > 'a1 **) 1152 init_mutable > ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, 1153 Z.z) Types.prod > ASM.labelled_instruction List.list List.list > 1154 (ASM.identifier, BitVector.word) Types.prod List.list > __ > 'a1) > 1155 'a1 **) 1151 1156 let init_mutable_inv_rect_Type1 hterm h1 = 1152 1157 let hcut = init_mutable_rect_Type1 h1 hterm in hcut __ 1153 1158 1154 1159 (** val init_mutable_inv_rect_Type0 : 1155 init_mutable > (Z.z > Z.z > ASM.labelled_instruction List.list 1156 List.list > (ASM.identifier, BitVector.word) Types.prod List.list > __ 1157 > 'a1) > 'a1 **) 1160 init_mutable > ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, 1161 Z.z) Types.prod > ASM.labelled_instruction List.list List.list > 1162 (ASM.identifier, BitVector.word) Types.prod List.list > __ > 'a1) > 1163 'a1 **) 1158 1164 let init_mutable_inv_rect_Type0 hterm h1 = 1159 1165 let hcut = init_mutable_rect_Type0 h1 hterm in hcut __ … … 1182 1188 built_preamble = acc2 } = mut 1183 1189 in 1184 let off = Z.zminus virt act in1185 1190 let pre = 1186 match Z.eqZb off Z.OZ with 1187  Bool.True > List.Nil 1191 match Identifiers.eq_identifier PreIdentifiers.ASMTag virt.Types.fst 1192 act.Types.fst with 1193  Bool.True > 1194 let off = Z.zminus virt.Types.snd act.Types.snd in 1195 (match Z.eqZb off Z.OZ with 1196  Bool.True > List.Nil 1197  Bool.False > 1198 (match Z.eqZb off (Z.z_of_nat (Nat.S Nat.O)) with 1199  Bool.True > 1200 List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction 1201 (ASM.INC ASM.DPTR)) }, List.Nil) 1202  Bool.False > 1203 List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Mov 1204 ((Types.Inl ASM.DPTR), virt.Types.fst, 1205 (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1206 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1207 (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) virt.Types.snd))) }, 1208 List.Nil))) 1188 1209  Bool.False > 1189 (match Z.eqZb off (Z.z_of_nat (Nat.S Nat.O)) with 1190  Bool.True > 1191 List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction 1192 (ASM.INC ASM.DPTR)) }, List.Nil) 1193  Bool.False > 1194 List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction 1195 (ASM.MOV (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR; 1196 Types.snd = (ASM.DATA16 1197 (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1198 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1199 (Nat.S (Nat.S Nat.O)))))))))))))))) virt)) }))))) }, List.Nil)) 1210 List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Mov ((Types.Inl 1211 ASM.DPTR), virt.Types.fst, 1212 (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1213 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1214 (Nat.S Nat.O)))))))))))))))) virt.Types.snd))) }, List.Nil) 1200 1215 in 1201 1216 let post = … … 1213 1228 Nat.O))))))))))))))))))) } 1214 1229 in 1215 { virtual_dptr = (Z.zsucc virt); actual_dptr = virt; built_code=1216 ( List.Cons1230 { virtual_dptr = { Types.fst = virt.Types.fst; Types.snd = 1231 (Z.zsucc virt.Types.snd) }; actual_dptr = virt; built_code = (List.Cons 1217 1232 ((List.append pre (List.Cons (post, (List.Cons ({ Types.fst = Types.None; 1218 1233 Types.snd = (ASM.Instruction (ASM.MOVX (Types.Inr { Types.fst = … … 1264 1279 (store_byte by2 (store_byte by1 (store_byte by0 mut)))) 1265 1280  AST.Init_space n > 1281 let { Types.fst = virt_id; Types.snd = virt_off } = mut.virtual_dptr 1282 in 1266 1283 Monad.m_return0 (Monad.smax_def State.state_monad) { virtual_dptr = 1267 (Z.zplus (Z.z_of_nat n) mut.virtual_dptr); actual_dptr=1268 mut.actual_dptr; built_code = mut.built_code; built_preamble =1269 mut.built_preamble }1284 { Types.fst = virt_id; Types.snd = 1285 (Z.zplus (Z.z_of_nat n) virt_off) }; actual_dptr = mut.actual_dptr; 1286 built_code = mut.built_code; built_preamble = mut.built_preamble } 1270 1287  AST.Init_null > 1271 1288 let z = … … 1287 1304 let do_store_global m_mut id_reg_data = 1288 1305 Monad.m_bind0 (Monad.smax_def State.state_monad) m_mut (fun mut > 1289 let { Types.fst = eta 28633; Types.snd = data } = id_reg_data in1290 let { Types.fst = id; Types.snd = reg } = eta 28633in1306 let { Types.fst = eta171; Types.snd = data } = id_reg_data in 1307 let { Types.fst = id; Types.snd = reg } = eta171 in 1291 1308 Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_ident id) 1292 1309 (fun id0 > 1293 let mut0 = { virtual_dptr = mut.virtual_dptr; actual_dptr =1294 mut.actual_dptr; built_code = mut.built_code; built_preamble =1295 (List.Cons ({ Types.fst = id0; Types.snd =1296 ( BitVectorZ.bitvector_of_Z (Nat.S(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S1310 let mut0 = { virtual_dptr = { Types.fst = id0; Types.snd = Z.OZ }; 1311 actual_dptr = mut.actual_dptr; built_code = mut.built_code; 1312 built_preamble = (List.Cons ({ Types.fst = id0; Types.snd = 1313 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1297 1314 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1298 (Nat.S Nat.O)))))))))))))))) mut.virtual_dptr) },1299 mut.built_preamble)) }1315 (Nat.S (Nat.S Nat.O)))))))))))))))) 1316 (Globalenvs.size_init_data_list data)) }, mut.built_preamble)) } 1300 1317 in 1301 1318 Util.foldl do_store_init_data … … 1317 1334 Monad.m_bind0 (Monad.smax_def State.state_monad) State.state_get 1318 1335 (fun u > 1319 let start_sp = 1320 Z.zopp 1321 (Z.z_of_nat (Nat.S 1322 (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p))) 1336 let dummy_dptr = { Types.fst = Positive.One; Types.snd = 1337 (Z.zopp (Z.z_of_nat (Nat.S Nat.O))) } 1323 1338 in 1324 let mut = { virtual_dptr = start_sp; actual_dptr = Z.OZ; built_code =1325 List.Nil; built_preamble = List.Nil }1339 let mut = { virtual_dptr = dummy_dptr; actual_dptr = dummy_dptr; 1340 built_code = List.Nil; built_preamble = List.Nil } 1326 1341 in 1327 1342 Monad.m_bind0 (Monad.smax_def State.state_monad) … … 1336 1351 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1337 1352 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1338 (Nat.S (Nat.S (Nat.S Nat.O))))))))) start_sp) 1353 (Nat.S (Nat.S (Nat.S Nat.O))))))))) 1354 (Z.zopp 1355 (Z.z_of_nat (Nat.S 1356 (Joint.globals_stacksize 1357 (Joint.lin_params_to_params LIN.lIN) p))))) 1339 1358 in 1340 1359 let init_isp = ASM.DATA 
extracted/lINToASM.mli
r3059 r3069 254 254 Joint.joint_function) Types.prod > __ 255 255 256 type init_mutable = { virtual_dptr : Z.z; actual_dptr : Z.z; 256 type init_mutable = { virtual_dptr : (ASM.identifier, Z.z) Types.prod; 257 actual_dptr : (ASM.identifier, Z.z) Types.prod; 257 258 built_code : ASM.labelled_instruction List.list 258 259 List.list; … … 261 262 262 263 val init_mutable_rect_Type4 : 263 ( Z.z > Z.z > ASM.labelled_instruction List.list List.list>264 (ASM.identifier, BitVector.word) Types.prod List.list > 'a1) >265 init_mutable > 'a1264 ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) Types.prod > 265 ASM.labelled_instruction List.list List.list > (ASM.identifier, 266 BitVector.word) Types.prod List.list > 'a1) > init_mutable > 'a1 266 267 267 268 val init_mutable_rect_Type5 : 268 ( Z.z > Z.z > ASM.labelled_instruction List.list List.list>269 (ASM.identifier, BitVector.word) Types.prod List.list > 'a1) >270 init_mutable > 'a1269 ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) Types.prod > 270 ASM.labelled_instruction List.list List.list > (ASM.identifier, 271 BitVector.word) Types.prod List.list > 'a1) > init_mutable > 'a1 271 272 272 273 val init_mutable_rect_Type3 : 273 ( Z.z > Z.z > ASM.labelled_instruction List.list List.list>274 (ASM.identifier, BitVector.word) Types.prod List.list > 'a1) >275 init_mutable > 'a1274 ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) Types.prod > 275 ASM.labelled_instruction List.list List.list > (ASM.identifier, 276 BitVector.word) Types.prod List.list > 'a1) > init_mutable > 'a1 276 277 277 278 val init_mutable_rect_Type2 : 278 ( Z.z > Z.z > ASM.labelled_instruction List.list List.list>279 (ASM.identifier, BitVector.word) Types.prod List.list > 'a1) >280 init_mutable > 'a1279 ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) Types.prod > 280 ASM.labelled_instruction List.list List.list > (ASM.identifier, 281 BitVector.word) Types.prod List.list > 'a1) > init_mutable > 'a1 281 282 282 283 val init_mutable_rect_Type1 : 283 ( Z.z > Z.z > ASM.labelled_instruction List.list List.list>284 (ASM.identifier, BitVector.word) Types.prod List.list > 'a1) >285 init_mutable > 'a1284 ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) Types.prod > 285 ASM.labelled_instruction List.list List.list > (ASM.identifier, 286 BitVector.word) Types.prod List.list > 'a1) > init_mutable > 'a1 286 287 287 288 val init_mutable_rect_Type0 : 288 ( Z.z > Z.z > ASM.labelled_instruction List.list List.list>289 (ASM.identifier, BitVector.word) Types.prod List.list > 'a1) >290 init_mutable > 'a1291 292 val virtual_dptr : init_mutable > Z.z293 294 val actual_dptr : init_mutable > Z.z289 ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) Types.prod > 290 ASM.labelled_instruction List.list List.list > (ASM.identifier, 291 BitVector.word) Types.prod List.list > 'a1) > init_mutable > 'a1 292 293 val virtual_dptr : init_mutable > (ASM.identifier, Z.z) Types.prod 294 295 val actual_dptr : init_mutable > (ASM.identifier, Z.z) Types.prod 295 296 296 297 val built_code : init_mutable > ASM.labelled_instruction List.list List.list … … 300 301 301 302 val init_mutable_inv_rect_Type4 : 302 init_mutable > ( Z.z > Z.z > ASM.labelled_instruction List.list List.list303 > (ASM.identifier, BitVector.word) Types.prod List.list > __ > 'a1)>304 'a1303 init_mutable > ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) 304 Types.prod > ASM.labelled_instruction List.list List.list > 305 (ASM.identifier, BitVector.word) Types.prod List.list > __ > 'a1) > 'a1 305 306 306 307 val init_mutable_inv_rect_Type3 : 307 init_mutable > ( Z.z > Z.z > ASM.labelled_instruction List.list List.list308 > (ASM.identifier, BitVector.word) Types.prod List.list > __ > 'a1)>309 'a1308 init_mutable > ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) 309 Types.prod > ASM.labelled_instruction List.list List.list > 310 (ASM.identifier, BitVector.word) Types.prod List.list > __ > 'a1) > 'a1 310 311 311 312 val init_mutable_inv_rect_Type2 : 312 init_mutable > ( Z.z > Z.z > ASM.labelled_instruction List.list List.list313 > (ASM.identifier, BitVector.word) Types.prod List.list > __ > 'a1)>314 'a1313 init_mutable > ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) 314 Types.prod > ASM.labelled_instruction List.list List.list > 315 (ASM.identifier, BitVector.word) Types.prod List.list > __ > 'a1) > 'a1 315 316 316 317 val init_mutable_inv_rect_Type1 : 317 init_mutable > ( Z.z > Z.z > ASM.labelled_instruction List.list List.list318 > (ASM.identifier, BitVector.word) Types.prod List.list > __ > 'a1)>319 'a1318 init_mutable > ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) 319 Types.prod > ASM.labelled_instruction List.list List.list > 320 (ASM.identifier, BitVector.word) Types.prod List.list > __ > 'a1) > 'a1 320 321 321 322 val init_mutable_inv_rect_Type0 : 322 init_mutable > ( Z.z > Z.z > ASM.labelled_instruction List.list List.list323 > (ASM.identifier, BitVector.word) Types.prod List.list > __ > 'a1)>324 'a1323 init_mutable > ((ASM.identifier, Z.z) Types.prod > (ASM.identifier, Z.z) 324 Types.prod > ASM.labelled_instruction List.list List.list > 325 (ASM.identifier, BitVector.word) Types.prod List.list > __ > 'a1) > 'a1 325 326 326 327 val init_mutable_discr : init_mutable > init_mutable > __ 
extracted/status.ml
r3059 r3069 89 89 serialBufferType > 'a1 **) 90 90 let rec serialBufferType_rect_Type4 h_Eight h_Nine = function 91  Eight x_ 21722 > h_Eight x_2172292  Nine (x_ 21724, x_21723) > h_Nine x_21724 x_2172391  Eight x_8 > h_Eight x_8 92  Nine (x_10, x_9) > h_Nine x_10 x_9 93 93 94 94 (** val serialBufferType_rect_Type5 : … … 96 96 serialBufferType > 'a1 **) 97 97 let rec serialBufferType_rect_Type5 h_Eight h_Nine = function 98  Eight x_ 21728 > h_Eight x_2172899  Nine (x_ 21730, x_21729) > h_Nine x_21730 x_2172998  Eight x_14 > h_Eight x_14 99  Nine (x_16, x_15) > h_Nine x_16 x_15 100 100 101 101 (** val serialBufferType_rect_Type3 : … … 103 103 serialBufferType > 'a1 **) 104 104 let rec serialBufferType_rect_Type3 h_Eight h_Nine = function 105  Eight x_2 1734 > h_Eight x_21734106  Nine (x_2 1736, x_21735) > h_Nine x_21736 x_21735105  Eight x_20 > h_Eight x_20 106  Nine (x_22, x_21) > h_Nine x_22 x_21 107 107 108 108 (** val serialBufferType_rect_Type2 : … … 110 110 serialBufferType > 'a1 **) 111 111 let rec serialBufferType_rect_Type2 h_Eight h_Nine = function 112  Eight x_2 1740 > h_Eight x_21740113  Nine (x_2 1742, x_21741) > h_Nine x_21742 x_21741112  Eight x_26 > h_Eight x_26 113  Nine (x_28, x_27) > h_Nine x_28 x_27 114 114 115 115 (** val serialBufferType_rect_Type1 : … … 117 117 serialBufferType > 'a1 **) 118 118 let rec serialBufferType_rect_Type1 h_Eight h_Nine = function 119  Eight x_ 21746 > h_Eight x_21746120  Nine (x_ 21748, x_21747) > h_Nine x_21748 x_21747119  Eight x_32 > h_Eight x_32 120  Nine (x_34, x_33) > h_Nine x_34 x_33 121 121 122 122 (** val serialBufferType_rect_Type0 : … … 124 124 serialBufferType > 'a1 **) 125 125 let rec serialBufferType_rect_Type0 h_Eight h_Nine = function 126  Eight x_ 21752 > h_Eight x_21752127  Nine (x_ 21754, x_21753) > h_Nine x_21754 x_21753126  Eight x_38 > h_Eight x_38 127  Nine (x_40, x_39) > h_Nine x_40 x_39 128 128 129 129 (** val serialBufferType_inv_rect_Type4 : … … 182 182 > 'a1) > lineType > 'a1 **) 183 183 let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function 184  P1 x_ 21801 > h_P1 x_21801185  P3 x_ 21802 > h_P3 x_21802186  SerialBuffer x_ 21803 > h_SerialBuffer x_21803184  P1 x_87 > h_P1 x_87 185  P3 x_88 > h_P3 x_88 186  SerialBuffer x_89 > h_SerialBuffer x_89 187 187 188 188 (** val lineType_rect_Type5 : … … 190 190 > 'a1) > lineType > 'a1 **) 191 191 let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function 192  P1 x_ 21808 > h_P1 x_21808193  P3 x_ 21809 > h_P3 x_21809194  SerialBuffer x_ 21810 > h_SerialBuffer x_21810192  P1 x_94 > h_P1 x_94 193  P3 x_95 > h_P3 x_95 194  SerialBuffer x_96 > h_SerialBuffer x_96 195 195 196 196 (** val lineType_rect_Type3 : … … 198 198 > 'a1) > lineType > 'a1 **) 199 199 let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function 200  P1 x_ 21815 > h_P1 x_21815201  P3 x_ 21816 > h_P3 x_21816202  SerialBuffer x_ 21817 > h_SerialBuffer x_21817200  P1 x_101 > h_P1 x_101 201  P3 x_102 > h_P3 x_102 202  SerialBuffer x_103 > h_SerialBuffer x_103 203 203 204 204 (** val lineType_rect_Type2 : … … 206 206 > 'a1) > lineType > 'a1 **) 207 207 let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function 208  P1 x_ 21822 > h_P1 x_21822209  P3 x_ 21823 > h_P3 x_21823210  SerialBuffer x_ 21824 > h_SerialBuffer x_21824208  P1 x_108 > h_P1 x_108 209  P3 x_109 > h_P3 x_109 210  SerialBuffer x_110 > h_SerialBuffer x_110 211 211 212 212 (** val lineType_rect_Type1 : … … 214 214 > 'a1) > lineType > 'a1 **) 215 215 let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function 216  P1 x_ 21829 > h_P1 x_21829217  P3 x_ 21830 > h_P3 x_21830218  SerialBuffer x_ 21831 > h_SerialBuffer x_21831216  P1 x_115 > h_P1 x_115 217  P3 x_116 > h_P3 x_116 218  SerialBuffer x_117 > h_SerialBuffer x_117 219 219 220 220 (** val lineType_rect_Type0 : … … 222 222 > 'a1) > lineType > 'a1 **) 223 223 let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function 224  P1 x_ 21836 > h_P1 x_21836225  P3 x_ 21837 > h_P3 x_21837226  SerialBuffer x_ 21838 > h_SerialBuffer x_21838224  P1 x_122 > h_P1 x_122 225  P3 x_123 > h_P3 x_123 226  SerialBuffer x_124 > h_SerialBuffer x_124 227 227 228 228 (** val lineType_inv_rect_Type4 : … … 731 731 Vector.vector > BitVector.byte > BitVector.byte > time > 'a2) > 'a1 732 732 preStatus > 'a2 **) 733 let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_ 22224=733 let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_510 = 734 734 let { low_internal_ram = low_internal_ram0; high_internal_ram = 735 735 high_internal_ram0; external_ram = external_ram0; program_counter = … … 737 737 special_function_registers_8053; special_function_registers_8052 = 738 738 special_function_registers_8054; p1_latch = p1_latch0; p3_latch = 739 p3_latch0; clock = clock0 } = x_ 22224739 p3_latch0; clock = clock0 } = x_510 740 740 in 741 741 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 … … 749 749 Vector.vector > BitVector.byte > BitVector.byte > time > 'a2) > 'a1 750 750 preStatus > 'a2 **) 751 let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_ 22226=751 let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_512 = 752 752 let { low_internal_ram = low_internal_ram0; high_internal_ram = 753 753 high_internal_ram0; external_ram = external_ram0; program_counter = … … 755 755 special_function_registers_8053; special_function_registers_8052 = 756 756 special_function_registers_8054; p1_latch = p1_latch0; p3_latch = 757 p3_latch0; clock = clock0 } = x_ 22226757 p3_latch0; clock = clock0 } = x_512 758 758 in 759 759 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 … … 767 767 Vector.vector > BitVector.byte > BitVector.byte > time > 'a2) > 'a1 768 768 preStatus > 'a2 **) 769 let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_ 22228=769 let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_514 = 770 770 let { low_internal_ram = low_internal_ram0; high_internal_ram = 771 771 high_internal_ram0; external_ram = external_ram0; program_counter = … … 773 773 special_function_registers_8053; special_function_registers_8052 = 774 774 special_function_registers_8054; p1_latch = p1_latch0; p3_latch = 775 p3_latch0; clock = clock0 } = x_ 22228775 p3_latch0; clock = clock0 } = x_514 776 776 in 777 777 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 … … 785 785 Vector.vector > BitVector.byte > BitVector.byte > time > 'a2) > 'a1 786 786 preStatus > 'a2 **) 787 let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_ 22230=787 let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_516 = 788 788 let { low_internal_ram = low_internal_ram0; high_internal_ram = 789 789 high_internal_ram0; external_ram = external_ram0; program_counter = … … 791 791 special_function_registers_8053; special_function_registers_8052 = 792 792 special_function_registers_8054; p1_latch = p1_latch0; p3_latch = 793 p3_latch0; clock = clock0 } = x_ 22230793 p3_latch0; clock = clock0 } = x_516 794 794 in 795 795 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 … … 803 803 Vector.vector > BitVector.byte > BitVector.byte > time > 'a2) > 'a1 804 804 preStatus > 'a2 **) 805 let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_ 22232=805 let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_518 = 806 806 let { low_internal_ram = low_internal_ram0; high_internal_ram = 807 807 high_internal_ram0; external_ram = external_ram0; program_counter = … … 809 809 special_function_registers_8053; special_function_registers_8052 = 810 810 special_function_registers_8054; p1_latch = p1_latch0; p3_latch = 811 p3_latch0; clock = clock0 } = x_ 22232811 p3_latch0; clock = clock0 } = x_518 812 812 in 813 813 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 … … 821 821 Vector.vector > BitVector.byte > BitVector.byte > time > 'a2) > 'a1 822 822 preStatus > 'a2 **) 823 let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_ 22234=823 let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_520 = 824 824 let { low_internal_ram = low_internal_ram0; high_internal_ram = 825 825 high_internal_ram0; external_ram = external_ram0; program_counter = … … 827 827 special_function_registers_8053; special_function_registers_8052 = 828 828 special_function_registers_8054; p1_latch = p1_latch0; p3_latch = 829 p3_latch0; clock = clock0 } = x_ 22234829 p3_latch0; clock = clock0 } = x_520 830 830 in 831 831 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 … … 3780 3780 'a1 > 'a1 preStatus > ASM.subaddressing_mode > BitVector.word **) 3781 3781 let get_arg_16 cm s a = 3782 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Data16, 3783 Vector.VEmpty)) a with 3782 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), 3783 ASM.Data16, (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty)))) 3784 a with 3784 3785  ASM.DIRECT x > (fun _ > assert false (* absurd case *)) 3785 3786  ASM.INDIRECT x > (fun _ > assert false (* absurd case *)) … … 3791 3792  ASM.DATA x > (fun _ > assert false (* absurd case *)) 3792 3793  ASM.DATA16 d > (fun _ > d) 3793  ASM.ACC_DPTR > (fun _ > assert false (* absurd case *)) 3794  ASM.ACC_DPTR > 3795 (fun _ > 3796 let dptr = 3797 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3798 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3799 (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH) 3800 (get_8051_sfr cm s SFR_DPL) 3801 in 3802 let big_acc = 3803 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3804 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3805 (Nat.S (Nat.S Nat.O)))))))) 3806 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3807 (Nat.S Nat.O))))))))) (get_8051_sfr cm s SFR_ACC_A) 3808 in 3809 Arithmetic.add 3810 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3811 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3812 (Nat.S Nat.O))))))))) big_acc dptr) 3794 3813  ASM.ACC_PC > (fun _ > assert false (* absurd case *)) 3795 3814  ASM.EXT_INDIRECT_DPTR > (fun _ > assert false (* absurd case *)) … … 4254 4273 (ASM.identifier, BitVector.word) Types.prod List.list > BitVector.word 4255 4274 Identifiers.identifier_map **) 4256 let construct_datalabels = 4257 Util.foldl (fun datalabels preamble > 4258 let { Types.fst = name; Types.snd = addr } = preamble in 4259 Identifiers.add PreIdentifiers.ASMTag datalabels name addr) 4260 (Identifiers.empty_map PreIdentifiers.ASMTag) 4261 4275 let construct_datalabels the_preamble = 4276 (Util.foldl (fun t preamble > 4277 let { Types.fst = datalabels; Types.snd = addr } = t in 4278 let { Types.fst = name; Types.snd = size } = preamble in 4279 let { Types.fst = addr0; Types.snd = carry } = 4280 Arithmetic.sub_16_with_carry addr size Bool.False 4281 in 4282 { Types.fst = 4283 (Identifiers.add PreIdentifiers.ASMTag datalabels name addr0); 4284 Types.snd = addr0 }) { Types.fst = 4285 (Identifiers.empty_map PreIdentifiers.ASMTag); Types.snd = 4286 (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 4287 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 4288 Nat.O))))))))))))))))) } the_preamble).Types.fst 4289
Note: See TracChangeset
for help on using the changeset viewer.