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

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/status.ml
r2743 r2773 1 1 open Preamble 2 2 3 open BitVectorTrie 4 3 5 open String 4 6 7 open Exp 8 9 open Arithmetic 10 11 open Vector 12 13 open FoldStuff 14 15 open BitVector 16 17 open Extranat 18 19 open Integers 20 21 open AST 22 5 23 open LabelledObjects 6 24 7 open BitVectorTrie 8 9 open Exp 10 11 open Arithmetic 12 13 open Integers 14 15 open AST 25 open Proper 26 27 open PositiveMap 28 29 open Deqsets 30 31 open ErrorMessages 32 33 open PreIdentifiers 34 35 open Errors 36 37 open Extralib 38 39 open Setoids 40 41 open Monad 42 43 open Option 44 45 open Div_and_mod 46 47 open Jmeq 48 49 open Russell 50 51 open Util 52 53 open List 54 55 open Lists 56 57 open Bool 58 59 open Relations 60 61 open Nat 62 63 open Positive 64 65 open Hints_declaration 66 67 open Core_notation 68 69 open Pts 70 71 open Logic 72 73 open Types 74 75 open Identifiers 16 76 17 77 open CostLabel 18 19 open Proper20 21 open PositiveMap22 23 open Deqsets24 25 open ErrorMessages26 27 open PreIdentifiers28 29 open Errors30 31 open Extralib32 33 open Setoids34 35 open Monad36 37 open Option38 39 open Lists40 41 open Positive42 43 open Identifiers44 45 open Extranat46 47 open Vector48 49 open Div_and_mod50 51 open Jmeq52 53 open Russell54 55 open Types56 57 open List58 59 open Util60 61 open FoldStuff62 63 open Bool64 65 open Hints_declaration66 67 open Core_notation68 69 open Pts70 71 open Logic72 73 open Relations74 75 open Nat76 77 open BitVector78 78 79 79 open ASM … … 89 89 serialBufferType > 'a1 **) 90 90 let rec serialBufferType_rect_Type4 h_Eight h_Nine = function 91  Eight x_ 24138 > h_Eight x_2413892  Nine (x_ 24140, x_24139) > h_Nine x_24140 x_2413991  Eight x_19500 > h_Eight x_19500 92  Nine (x_19502, x_19501) > h_Nine x_19502 x_19501 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_ 24144 > h_Eight x_2414499  Nine (x_ 24146, x_24145) > h_Nine x_24146 x_2414598  Eight x_19506 > h_Eight x_19506 99  Nine (x_19508, x_19507) > h_Nine x_19508 x_19507 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_ 24150 > h_Eight x_24150106  Nine (x_ 24152, x_24151) > h_Nine x_24152 x_24151105  Eight x_19512 > h_Eight x_19512 106  Nine (x_19514, x_19513) > h_Nine x_19514 x_19513 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_ 24156 > h_Eight x_24156113  Nine (x_ 24158, x_24157) > h_Nine x_24158 x_24157112  Eight x_19518 > h_Eight x_19518 113  Nine (x_19520, x_19519) > h_Nine x_19520 x_19519 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_ 24162 > h_Eight x_24162120  Nine (x_ 24164, x_24163) > h_Nine x_24164 x_24163119  Eight x_19524 > h_Eight x_19524 120  Nine (x_19526, x_19525) > h_Nine x_19526 x_19525 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_ 24168 > h_Eight x_24168127  Nine (x_ 24170, x_24169) > h_Nine x_24170 x_24169126  Eight x_19530 > h_Eight x_19530 127  Nine (x_19532, x_19531) > h_Nine x_19532 x_19531 128 128 129 129 (** val serialBufferType_inv_rect_Type4 : … … 174 174 175 175 type lineType = 176  P 2of BitVector.byte176  P1 of BitVector.byte 177 177  P3 of BitVector.byte 178 178  SerialBuffer of serialBufferType … … 182 182 > 'a1) > lineType > 'a1 **) 183 183 let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function 184  P 2 x_24217 > h_P1 x_24217185  P3 x_ 24218 > h_P3 x_24218186  SerialBuffer x_ 24219 > h_SerialBuffer x_24219184  P1 x_19579 > h_P1 x_19579 185  P3 x_19580 > h_P3 x_19580 186  SerialBuffer x_19581 > h_SerialBuffer x_19581 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  P 2 x_24224 > h_P1 x_24224193  P3 x_ 24225 > h_P3 x_24225194  SerialBuffer x_ 24226 > h_SerialBuffer x_24226192  P1 x_19586 > h_P1 x_19586 193  P3 x_19587 > h_P3 x_19587 194  SerialBuffer x_19588 > h_SerialBuffer x_19588 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  P 2 x_24231 > h_P1 x_24231201  P3 x_ 24232 > h_P3 x_24232202  SerialBuffer x_ 24233 > h_SerialBuffer x_24233200  P1 x_19593 > h_P1 x_19593 201  P3 x_19594 > h_P3 x_19594 202  SerialBuffer x_19595 > h_SerialBuffer x_19595 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  P 2 x_24238 > h_P1 x_24238209  P3 x_ 24239 > h_P3 x_24239210  SerialBuffer x_ 24240 > h_SerialBuffer x_24240208  P1 x_19600 > h_P1 x_19600 209  P3 x_19601 > h_P3 x_19601 210  SerialBuffer x_19602 > h_SerialBuffer x_19602 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  P 2 x_24245 > h_P1 x_24245217  P3 x_ 24246 > h_P3 x_24246218  SerialBuffer x_ 24247 > h_SerialBuffer x_24247216  P1 x_19607 > h_P1 x_19607 217  P3 x_19608 > h_P3 x_19608 218  SerialBuffer x_19609 > h_SerialBuffer x_19609 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  P 2 x_24252 > h_P1 x_24252225  P3 x_ 24253 > h_P3 x_24253226  SerialBuffer x_ 24254 > h_SerialBuffer x_24254224  P1 x_19614 > h_P1 x_19614 225  P3 x_19615 > h_P3 x_19615 226  SerialBuffer x_19616 > h_SerialBuffer x_19616 227 227 228 228 (** val lineType_inv_rect_Type4 : … … 260 260 Logic.eq_rect_Type2 x 261 261 (match x with 262  P 2a0 > Obj.magic (fun _ dH > dH __)262  P1 a0 > Obj.magic (fun _ dH > dH __) 263 263  P3 a0 > Obj.magic (fun _ dH > dH __) 264 264  SerialBuffer a0 > Obj.magic (fun _ dH > dH __)) y … … 268 268 Logic.eq_rect_Type2 x 269 269 (match x with 270  P 2a0 > Obj.magic (fun _ dH > dH __)270  P1 a0 > Obj.magic (fun _ dH > dH __) 271 271  P3 a0 > Obj.magic (fun _ dH > dH __) 272 272  SerialBuffer a0 > Obj.magic (fun _ dH > dH __)) y … … 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_2 4640=733 let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_20002 = 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_2 4640739 p3_latch0; clock = clock0 } = x_20002 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_2 4642=751 let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_20004 = 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_2 4642757 p3_latch0; clock = clock0 } = x_20004 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_2 4644=769 let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_20006 = 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_2 4644775 p3_latch0; clock = clock0 } = x_20006 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_2 4646=787 let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_20008 = 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_2 4646793 p3_latch0; clock = clock0 } = x_20008 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_2 4648=805 let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_20010 = 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_2 4648811 p3_latch0; clock = clock0 } = x_20010 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_2 4650=823 let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_20012 = 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_2 4650829 p3_latch0; clock = clock0 } = x_20012 830 830 in 831 831 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 … … 3639 3639 (Nat.S Nat.O)))) (get_8051_sfr code_memory s SFR_PSW) 3640 3640 in 3641 let { Types.fst = r 5; Types.snd = r6} = { Types.fst =3641 let { Types.fst = r1; Types.snd = r0 } = { Types.fst = 3642 3642 (Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) un (Nat.S 3643 3643 (Nat.S Nat.O))); Types.snd = … … 3646 3646 in 3647 3647 let offset = 3648 match Bool.andb (Bool.notb r 5) (Bool.notb r6) with3648 match Bool.andb (Bool.notb r1) (Bool.notb r0) with 3649 3649  Bool.True > Nat.O 3650 3650  Bool.False > 3651 (match Bool.andb (Bool.notb r 5) r6with3651 (match Bool.andb (Bool.notb r1) r0 with 3652 3652  Bool.True > 3653 3653 Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) 3654 3654  Bool.False > 3655 (match Bool.andb r 5 r6with3655 (match Bool.andb r1 r0 with 3656 3656  Bool.True > 3657 3657 Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S … … 3822 3822  ASM.DIRECT d > 3823 3823 (fun _ > 3824 let { Types.fst = hd 0; Types.snd = seven_bits } =3824 let { Types.fst = hd; Types.snd = seven_bits } = 3825 3825 Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3826 3826 (Nat.S (Nat.S Nat.O))))))) d 3827 3827 in 3828 (match Vector.head' Nat.O hd 0with3828 (match Vector.head' Nat.O hd with 3829 3829  Bool.True > 3830 3830 get_bit_addressable_sfr cm s (Vector.VCons ((Nat.S (Nat.S (Nat.S … … 3838 3838  ASM.INDIRECT i > 3839 3839 (fun _ > 3840 let { Types.fst = hd 0; Types.snd = seven_bits } =3840 let { Types.fst = hd; Types.snd = seven_bits } = 3841 3841 Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3842 3842 (Nat.S (Nat.S Nat.O))))))) … … 3845 3845 (Vector.VCons (Nat.O, i, Vector.VEmpty))))))) 3846 3846 in 3847 (match Vector.head' Nat.O hd 0with3847 (match Vector.head' Nat.O hd with 3848 3848  Bool.True > 3849 3849 BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S … … 3856 3856 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3857 3857 (Nat.S Nat.O))))))))))) 3858  ASM.EXT_INDIRECT e 0>3858  ASM.EXT_INDIRECT e > 3859 3859 (fun _ > 3860 3860 let address = 3861 3861 get_register cm s (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, 3862 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, 3863 e0,Vector.VEmpty))))))3862 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, e, 3863 Vector.VEmpty)))))) 3864 3864 in 3865 3865 let padded_address = … … 3882 3882 (fun _ > 3883 3883 let dptr = 3884 Vector.append 0(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S3884 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3885 3885 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3886 3886 (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH) … … 3922 3922 (fun _ > 3923 3923 let address = 3924 Vector.append 0(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S3924 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3925 3925 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 3926 3926 (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH) … … 3994 3994 in 3995 3995 set_low_internal_ram cm s memory)) 3996  ASM.EXT_INDIRECT e 0>3996  ASM.EXT_INDIRECT e > 3997 3997 (fun _ > 3998 3998 let address = 3999 3999 get_register cm s (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, 4000 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, 4001 e0,Vector.VEmpty))))))4000 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, e, 4001 Vector.VEmpty)))))) 4002 4002 in 4003 4003 let padded_address = … … 4023 4023 (fun _ > 4024 4024 let address = 4025 Vector.append 0(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S4025 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 4026 4026 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 4027 4027 (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH) … … 4076 4076 in 4077 4077 let trans = 4078 Vector.append 0(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))4078 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) 4079 4079 (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S 4080 4080 (Nat.S (Nat.S Nat.O)))), Bool.True, four_bits)) (Vector.VCons … … 4094 4094 in 4095 4095 let address' = 4096 Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S4096 Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S 4097 4097 (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)), 4098 4098 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False, … … 4122 4122 in 4123 4123 let trans = 4124 Vector.append 0(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))4124 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) 4125 4125 (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S 4126 4126 (Nat.S (Nat.S Nat.O)))), Bool.True, four_bits)) (Vector.VCons … … 4141 4141 in 4142 4142 let address' = 4143 Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S4143 Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S 4144 4144 (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)), 4145 4145 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False, … … 4203 4203 in 4204 4204 let trans = 4205 Vector.append 0(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))4205 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) 4206 4206 (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S 4207 4207 (Nat.S (Nat.S Nat.O)))), Bool.True, four_bits)) (Vector.VCons … … 4224 4224 in 4225 4225 let address' = 4226 Vector.append 0(Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S4226 Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S 4227 4227 (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)), 4228 4228 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False, … … 4251 4251  ASM.ADDR16 x > (fun _ > assert false (* absurd case *))) __ 4252 4252 4253 (** val fetch_pseudo_instruction :4254 ASM.labelled_instruction List.list > BitVector.word >4255 (ASM.pseudo_instruction, BitVector.word) Types.prod **)4256 let fetch_pseudo_instruction code_mem pc =4257 let { Types.fst = lbl; Types.snd = instr } =4258 Util.nth_safe4259 (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S4260 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S4261 Nat.O)))))))))))))))) pc) code_mem4262 in4263 let new_pc =4264 Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S4265 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S4266 Nat.O)))))))))))))))) pc4267 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S4268 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S4269 Nat.O)))))))))))))))) (Nat.S Nat.O))4270 in4271 { Types.fst = instr; Types.snd = new_pc }4272 4273 4253 (** val construct_datalabels : 4274 ASM.preamble > BitVector.word Identifiers.identifier_map **) 4254 (ASM.identifier, BitVector.word) Types.prod List.list > BitVector.word 4255 Identifiers.identifier_map **) 4275 4256 let construct_datalabels the_preamble = 4276 (Util.foldl (fun t preamble 0>4257 (Util.foldl (fun t preamble > 4277 4258 let { Types.fst = datalabels; Types.snd = addr } = t in 4278 let { Types.fst = name; Types.snd = size } = preamble 0in4279 let { Types.fst = carry; Types.snd = sum 0} =4259 let { Types.fst = name; Types.snd = size } = preamble in 4260 let { Types.fst = carry; Types.snd = sum } = 4280 4261 Arithmetic.half_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 4281 4262 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S … … 4284 4265 { Types.fst = 4285 4266 (Identifiers.add PreIdentifiers.ASMTag datalabels name addr); Types.snd = 4286 sum 0}) { Types.fst = (Identifiers.empty_map PreIdentifiers.ASMTag);4267 sum }) { Types.fst = (Identifiers.empty_map PreIdentifiers.ASMTag); 4287 4268 Types.snd = 4288 4269 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
Note: See TracChangeset
for help on using the changeset viewer.