Changeset 2717 for extracted/status.ml
 Timestamp:
 Feb 23, 2013, 1:16:55 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/status.ml
r2649 r2717 5 5 open LabelledObjects 6 6 7 open BitVectorTrie 8 9 open Exp 10 7 11 open Arithmetic 8 12 … … 74 78 75 79 open ASM 76 77 open BitVectorTrie78 80 79 81 type time = Nat.nat … … 87 89 serialBufferType > 'a1 **) 88 90 let rec serialBufferType_rect_Type4 h_Eight h_Nine = function 89  Eight x_2 231 > h_Eight x_223190  Nine (x_2 233, x_2232) > h_Nine x_2233 x_223291  Eight x_21058 > h_Eight x_21058 92  Nine (x_21060, x_21059) > h_Nine x_21060 x_21059 91 93 92 94 (** val serialBufferType_rect_Type5 : … … 94 96 serialBufferType > 'a1 **) 95 97 let rec serialBufferType_rect_Type5 h_Eight h_Nine = function 96  Eight x_2 237 > h_Eight x_223797  Nine (x_2 239, x_2238) > h_Nine x_2239 x_223898  Eight x_21064 > h_Eight x_21064 99  Nine (x_21066, x_21065) > h_Nine x_21066 x_21065 98 100 99 101 (** val serialBufferType_rect_Type3 : … … 101 103 serialBufferType > 'a1 **) 102 104 let rec serialBufferType_rect_Type3 h_Eight h_Nine = function 103  Eight x_2 243 > h_Eight x_2243104  Nine (x_2 245, x_2244) > h_Nine x_2245 x_2244105  Eight x_21070 > h_Eight x_21070 106  Nine (x_21072, x_21071) > h_Nine x_21072 x_21071 105 107 106 108 (** val serialBufferType_rect_Type2 : … … 108 110 serialBufferType > 'a1 **) 109 111 let rec serialBufferType_rect_Type2 h_Eight h_Nine = function 110  Eight x_2 249 > h_Eight x_2249111  Nine (x_2 251, x_2250) > h_Nine x_2251 x_2250112  Eight x_21076 > h_Eight x_21076 113  Nine (x_21078, x_21077) > h_Nine x_21078 x_21077 112 114 113 115 (** val serialBufferType_rect_Type1 : … … 115 117 serialBufferType > 'a1 **) 116 118 let rec serialBufferType_rect_Type1 h_Eight h_Nine = function 117  Eight x_2 255 > h_Eight x_2255118  Nine (x_2 257, x_2256) > h_Nine x_2257 x_2256119  Eight x_21082 > h_Eight x_21082 120  Nine (x_21084, x_21083) > h_Nine x_21084 x_21083 119 121 120 122 (** val serialBufferType_rect_Type0 : … … 122 124 serialBufferType > 'a1 **) 123 125 let rec serialBufferType_rect_Type0 h_Eight h_Nine = function 124  Eight x_2 261 > h_Eight x_2261125  Nine (x_2 263, x_2262) > h_Nine x_2263 x_2262126  Eight x_21088 > h_Eight x_21088 127  Nine (x_21090, x_21089) > h_Nine x_21090 x_21089 126 128 127 129 (** val serialBufferType_inv_rect_Type4 : … … 180 182 > 'a1) > lineType > 'a1 **) 181 183 let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function 182  P2 x_2 310 > h_P1 x_2310183  P3 x_2 311 > h_P3 x_2311184  SerialBuffer x_2 312 > h_SerialBuffer x_2312184  P2 x_21137 > h_P1 x_21137 185  P3 x_21138 > h_P3 x_21138 186  SerialBuffer x_21139 > h_SerialBuffer x_21139 185 187 186 188 (** val lineType_rect_Type5 : … … 188 190 > 'a1) > lineType > 'a1 **) 189 191 let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function 190  P2 x_2 317 > h_P1 x_2317191  P3 x_2 318 > h_P3 x_2318192  SerialBuffer x_2 319 > h_SerialBuffer x_2319192  P2 x_21144 > h_P1 x_21144 193  P3 x_21145 > h_P3 x_21145 194  SerialBuffer x_21146 > h_SerialBuffer x_21146 193 195 194 196 (** val lineType_rect_Type3 : … … 196 198 > 'a1) > lineType > 'a1 **) 197 199 let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function 198  P2 x_2 324 > h_P1 x_2324199  P3 x_2 325 > h_P3 x_2325200  SerialBuffer x_2 326 > h_SerialBuffer x_2326200  P2 x_21151 > h_P1 x_21151 201  P3 x_21152 > h_P3 x_21152 202  SerialBuffer x_21153 > h_SerialBuffer x_21153 201 203 202 204 (** val lineType_rect_Type2 : … … 204 206 > 'a1) > lineType > 'a1 **) 205 207 let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function 206  P2 x_2 331 > h_P1 x_2331207  P3 x_2 332 > h_P3 x_2332208  SerialBuffer x_2 333 > h_SerialBuffer x_2333208  P2 x_21158 > h_P1 x_21158 209  P3 x_21159 > h_P3 x_21159 210  SerialBuffer x_21160 > h_SerialBuffer x_21160 209 211 210 212 (** val lineType_rect_Type1 : … … 212 214 > 'a1) > lineType > 'a1 **) 213 215 let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function 214  P2 x_2 338 > h_P1 x_2338215  P3 x_2 339 > h_P3 x_2339216  SerialBuffer x_2 340 > h_SerialBuffer x_2340216  P2 x_21165 > h_P1 x_21165 217  P3 x_21166 > h_P3 x_21166 218  SerialBuffer x_21167 > h_SerialBuffer x_21167 217 219 218 220 (** val lineType_rect_Type0 : … … 220 222 > 'a1) > lineType > 'a1 **) 221 223 let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function 222  P2 x_2 345 > h_P1 x_2345223  P3 x_2 346 > h_P3 x_2346224  SerialBuffer x_2 347 > h_SerialBuffer x_2347224  P2 x_21172 > h_P1 x_21172 225  P3 x_21173 > h_P3 x_21173 226  SerialBuffer x_21174 > h_SerialBuffer x_21174 225 227 226 228 (** val lineType_inv_rect_Type4 : … … 729 731 Vector.vector > BitVector.byte > BitVector.byte > time > 'a2) > 'a1 730 732 preStatus > 'a2 **) 731 let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_2 733=733 let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_21560 = 732 734 let { low_internal_ram = low_internal_ram0; high_internal_ram = 733 735 high_internal_ram0; external_ram = external_ram0; program_counter = … … 735 737 special_function_registers_8053; special_function_registers_8052 = 736 738 special_function_registers_8054; p1_latch = p1_latch0; p3_latch = 737 p3_latch0; clock = clock0 } = x_2 733739 p3_latch0; clock = clock0 } = x_21560 738 740 in 739 741 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 … … 747 749 Vector.vector > BitVector.byte > BitVector.byte > time > 'a2) > 'a1 748 750 preStatus > 'a2 **) 749 let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_2 735=751 let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_21562 = 750 752 let { low_internal_ram = low_internal_ram0; high_internal_ram = 751 753 high_internal_ram0; external_ram = external_ram0; program_counter = … … 753 755 special_function_registers_8053; special_function_registers_8052 = 754 756 special_function_registers_8054; p1_latch = p1_latch0; p3_latch = 755 p3_latch0; clock = clock0 } = x_2 735757 p3_latch0; clock = clock0 } = x_21562 756 758 in 757 759 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 … … 765 767 Vector.vector > BitVector.byte > BitVector.byte > time > 'a2) > 'a1 766 768 preStatus > 'a2 **) 767 let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_2 737=769 let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_21564 = 768 770 let { low_internal_ram = low_internal_ram0; high_internal_ram = 769 771 high_internal_ram0; external_ram = external_ram0; program_counter = … … 771 773 special_function_registers_8053; special_function_registers_8052 = 772 774 special_function_registers_8054; p1_latch = p1_latch0; p3_latch = 773 p3_latch0; clock = clock0 } = x_2 737775 p3_latch0; clock = clock0 } = x_21564 774 776 in 775 777 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 … … 783 785 Vector.vector > BitVector.byte > BitVector.byte > time > 'a2) > 'a1 784 786 preStatus > 'a2 **) 785 let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_2 739=787 let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_21566 = 786 788 let { low_internal_ram = low_internal_ram0; high_internal_ram = 787 789 high_internal_ram0; external_ram = external_ram0; program_counter = … … 789 791 special_function_registers_8053; special_function_registers_8052 = 790 792 special_function_registers_8054; p1_latch = p1_latch0; p3_latch = 791 p3_latch0; clock = clock0 } = x_2 739793 p3_latch0; clock = clock0 } = x_21566 792 794 in 793 795 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 … … 801 803 Vector.vector > BitVector.byte > BitVector.byte > time > 'a2) > 'a1 802 804 preStatus > 'a2 **) 803 let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_2 741=805 let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_21568 = 804 806 let { low_internal_ram = low_internal_ram0; high_internal_ram = 805 807 high_internal_ram0; external_ram = external_ram0; program_counter = … … 807 809 special_function_registers_8053; special_function_registers_8052 = 808 810 special_function_registers_8054; p1_latch = p1_latch0; p3_latch = 809 p3_latch0; clock = clock0 } = x_2 741811 p3_latch0; clock = clock0 } = x_21568 810 812 in 811 813 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 … … 819 821 Vector.vector > BitVector.byte > BitVector.byte > time > 'a2) > 'a1 820 822 preStatus > 'a2 **) 821 let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_2 743=823 let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_21570 = 822 824 let { low_internal_ram = low_internal_ram0; high_internal_ram = 823 825 high_internal_ram0; external_ram = external_ram0; program_counter = … … 825 827 special_function_registers_8053; special_function_registers_8052 = 826 828 special_function_registers_8054; p1_latch = p1_latch0; p3_latch = 827 p3_latch0; clock = clock0 } = x_2 743829 p3_latch0; clock = clock0 } = x_21570 828 830 in 829 831 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 … … 4286 4288 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 4287 4289 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 4288 Nat.O))))))))))))))))) } the_preamble .Types.snd).Types.fst4289 4290 Nat.O))))))))))))))))) } the_preamble).Types.fst 4291
Note: See TracChangeset
for help on using the changeset viewer.