Changeset 3024
 Timestamp:
 Mar 28, 2013, 10:53:54 PM (4 years ago)
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

extracted/status.ml
r2999 r3024 89 89 serialBufferType > 'a1 **) 90 90 let rec serialBufferType_rect_Type4 h_Eight h_Nine = function 91  Eight x_ 2400 > h_Eight x_240092  Nine (x_ 2402, x_2401) > h_Nine x_2402 x_240191  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_ 2406 > h_Eight x_240699  Nine (x_ 2408, x_2407) > h_Nine x_2408 x_240798  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 412 > h_Eight x_2412106  Nine (x_2 414, x_2413) > h_Nine x_2414 x_2413105  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 418 > h_Eight x_2418113  Nine (x_2 420, x_2419) > h_Nine x_2420 x_2419112  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_ 2424 > h_Eight x_2424120  Nine (x_ 2426, x_2425) > h_Nine x_2426 x_2425119  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_ 2430 > h_Eight x_2430127  Nine (x_ 2432, x_2431) > h_Nine x_2432 x_2431126  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_ 2479 > h_P1 x_2479185  P3 x_ 2480 > h_P3 x_2480186  SerialBuffer x_ 2481 > h_SerialBuffer x_2481184  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_ 2486 > h_P1 x_2486193  P3 x_ 2487 > h_P3 x_2487194  SerialBuffer x_ 2488 > h_SerialBuffer x_2488192  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_ 2493 > h_P1 x_2493201  P3 x_ 2494 > h_P3 x_2494202  SerialBuffer x_ 2495 > h_SerialBuffer x_2495200  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_ 2500 > h_P1 x_2500209  P3 x_ 2501 > h_P3 x_2501210  SerialBuffer x_ 2502 > h_SerialBuffer x_2502208  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_ 2507 > h_P1 x_2507217  P3 x_ 2508 > h_P3 x_2508218  SerialBuffer x_ 2509 > h_SerialBuffer x_2509216  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_ 2514 > h_P1 x_2514225  P3 x_ 2515 > h_P3 x_2515226  SerialBuffer x_ 2516 > h_SerialBuffer x_2516224  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_ 2902=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_ 2902739 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_ 2904=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_ 2904757 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_ 2906=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_ 2906775 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_ 2908=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_ 2908793 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_ 2910=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_ 2910811 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_ 2912=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_ 2912829 p3_latch0; clock = clock0 } = x_520 830 830 in 831 831 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 … … 1296 1296 in 1297 1297 set_8051_sfr code_memory s SFR_PSW (Vector.VCons ((Nat.S (Nat.S (Nat.S 1298 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), old_cy, (Vector.VCons ((Nat.S1298 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), cy, (Vector.VCons ((Nat.S 1299 1299 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), new_ac, (Vector.VCons 1300 1300 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), old_fo, (Vector.VCons 1301 1301 ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), old_rs1, (Vector.VCons ((Nat.S 1302 1302 (Nat.S (Nat.S Nat.O))), old_rs0, (Vector.VCons ((Nat.S (Nat.S Nat.O)), 1303 o ld_ov, (Vector.VCons ((Nat.S Nat.O), old_ud, (Vector.VCons (Nat.O,1304 old_p,Vector.VEmpty))))))))))))))))1303 ov, (Vector.VCons ((Nat.S Nat.O), old_ud, (Vector.VCons (Nat.O, old_p, 1304 Vector.VEmpty)))))))))))))))) 1305 1305 1306 1306 (** val initialise_status : 'a1 > 'a1 preStatus **) 
src/ASM/Status.ma
r2907 r3024 521 521 let new_ac ≝ match ac with [ None ⇒ old_ac  Some j ⇒ j ] in 522 522 set_8051_sfr ?? s SFR_PSW 523 [[ old_cy ; new_ac ; old_fo ; old_rs1 ;524 old_rs0 ; o ld_ov ; old_ud ; old_p ]].523 [[ cy ; new_ac ; old_fo ; old_rs1 ; 524 old_rs0 ; ov ; old_ud ; old_p ]]. 525 525 [1,2,3,4,5,6,7,8: 526 526 normalize
Note: See TracChangeset
for help on using the changeset viewer.