Changeset 2743 for extracted/status.ml


Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (7 years ago)
Author:
sacerdot
Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/status.ml

    r2730 r2743  
    8989    serialBufferType -> 'a1 **)
    9090let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
    91 | Eight x_5042 -> h_Eight x_5042
    92 | Nine (x_5044, x_5043) -> h_Nine x_5044 x_5043
     91| Eight x_24138 -> h_Eight x_24138
     92| Nine (x_24140, x_24139) -> h_Nine x_24140 x_24139
    9393
    9494(** val serialBufferType_rect_Type5 :
     
    9696    serialBufferType -> 'a1 **)
    9797let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
    98 | Eight x_5048 -> h_Eight x_5048
    99 | Nine (x_5050, x_5049) -> h_Nine x_5050 x_5049
     98| Eight x_24144 -> h_Eight x_24144
     99| Nine (x_24146, x_24145) -> h_Nine x_24146 x_24145
    100100
    101101(** val serialBufferType_rect_Type3 :
     
    103103    serialBufferType -> 'a1 **)
    104104let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
    105 | Eight x_5054 -> h_Eight x_5054
    106 | Nine (x_5056, x_5055) -> h_Nine x_5056 x_5055
     105| Eight x_24150 -> h_Eight x_24150
     106| Nine (x_24152, x_24151) -> h_Nine x_24152 x_24151
    107107
    108108(** val serialBufferType_rect_Type2 :
     
    110110    serialBufferType -> 'a1 **)
    111111let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
    112 | Eight x_5060 -> h_Eight x_5060
    113 | Nine (x_5062, x_5061) -> h_Nine x_5062 x_5061
     112| Eight x_24156 -> h_Eight x_24156
     113| Nine (x_24158, x_24157) -> h_Nine x_24158 x_24157
    114114
    115115(** val serialBufferType_rect_Type1 :
     
    117117    serialBufferType -> 'a1 **)
    118118let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
    119 | Eight x_5066 -> h_Eight x_5066
    120 | Nine (x_5068, x_5067) -> h_Nine x_5068 x_5067
     119| Eight x_24162 -> h_Eight x_24162
     120| Nine (x_24164, x_24163) -> h_Nine x_24164 x_24163
    121121
    122122(** val serialBufferType_rect_Type0 :
     
    124124    serialBufferType -> 'a1 **)
    125125let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
    126 | Eight x_5072 -> h_Eight x_5072
    127 | Nine (x_5074, x_5073) -> h_Nine x_5074 x_5073
     126| Eight x_24168 -> h_Eight x_24168
     127| Nine (x_24170, x_24169) -> h_Nine x_24170 x_24169
    128128
    129129(** val serialBufferType_inv_rect_Type4 :
     
    182182    -> 'a1) -> lineType -> 'a1 **)
    183183let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
    184 | P2 x_5121 -> h_P1 x_5121
    185 | P3 x_5122 -> h_P3 x_5122
    186 | SerialBuffer x_5123 -> h_SerialBuffer x_5123
     184| P2 x_24217 -> h_P1 x_24217
     185| P3 x_24218 -> h_P3 x_24218
     186| SerialBuffer x_24219 -> h_SerialBuffer x_24219
    187187
    188188(** val lineType_rect_Type5 :
     
    190190    -> 'a1) -> lineType -> 'a1 **)
    191191let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
    192 | P2 x_5128 -> h_P1 x_5128
    193 | P3 x_5129 -> h_P3 x_5129
    194 | SerialBuffer x_5130 -> h_SerialBuffer x_5130
     192| P2 x_24224 -> h_P1 x_24224
     193| P3 x_24225 -> h_P3 x_24225
     194| SerialBuffer x_24226 -> h_SerialBuffer x_24226
    195195
    196196(** val lineType_rect_Type3 :
     
    198198    -> 'a1) -> lineType -> 'a1 **)
    199199let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
    200 | P2 x_5135 -> h_P1 x_5135
    201 | P3 x_5136 -> h_P3 x_5136
    202 | SerialBuffer x_5137 -> h_SerialBuffer x_5137
     200| P2 x_24231 -> h_P1 x_24231
     201| P3 x_24232 -> h_P3 x_24232
     202| SerialBuffer x_24233 -> h_SerialBuffer x_24233
    203203
    204204(** val lineType_rect_Type2 :
     
    206206    -> 'a1) -> lineType -> 'a1 **)
    207207let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
    208 | P2 x_5142 -> h_P1 x_5142
    209 | P3 x_5143 -> h_P3 x_5143
    210 | SerialBuffer x_5144 -> h_SerialBuffer x_5144
     208| P2 x_24238 -> h_P1 x_24238
     209| P3 x_24239 -> h_P3 x_24239
     210| SerialBuffer x_24240 -> h_SerialBuffer x_24240
    211211
    212212(** val lineType_rect_Type1 :
     
    214214    -> 'a1) -> lineType -> 'a1 **)
    215215let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
    216 | P2 x_5149 -> h_P1 x_5149
    217 | P3 x_5150 -> h_P3 x_5150
    218 | SerialBuffer x_5151 -> h_SerialBuffer x_5151
     216| P2 x_24245 -> h_P1 x_24245
     217| P3 x_24246 -> h_P3 x_24246
     218| SerialBuffer x_24247 -> h_SerialBuffer x_24247
    219219
    220220(** val lineType_rect_Type0 :
     
    222222    -> 'a1) -> lineType -> 'a1 **)
    223223let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
    224 | P2 x_5156 -> h_P1 x_5156
    225 | P3 x_5157 -> h_P3 x_5157
    226 | SerialBuffer x_5158 -> h_SerialBuffer x_5158
     224| P2 x_24252 -> h_P1 x_24252
     225| P3 x_24253 -> h_P3 x_24253
     226| SerialBuffer x_24254 -> h_SerialBuffer x_24254
    227227
    228228(** val lineType_inv_rect_Type4 :
     
    731731    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    732732    preStatus -> 'a2 **)
    733 let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_5544 =
     733let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_24640 =
    734734  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    735735    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    737737    special_function_registers_8053; special_function_registers_8052 =
    738738    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    739     p3_latch0; clock = clock0 } = x_5544
     739    p3_latch0; clock = clock0 } = x_24640
    740740  in
    741741  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    749749    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    750750    preStatus -> 'a2 **)
    751 let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_5546 =
     751let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_24642 =
    752752  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    753753    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    755755    special_function_registers_8053; special_function_registers_8052 =
    756756    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    757     p3_latch0; clock = clock0 } = x_5546
     757    p3_latch0; clock = clock0 } = x_24642
    758758  in
    759759  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    767767    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    768768    preStatus -> 'a2 **)
    769 let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_5548 =
     769let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_24644 =
    770770  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    771771    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    773773    special_function_registers_8053; special_function_registers_8052 =
    774774    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    775     p3_latch0; clock = clock0 } = x_5548
     775    p3_latch0; clock = clock0 } = x_24644
    776776  in
    777777  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    785785    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    786786    preStatus -> 'a2 **)
    787 let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_5550 =
     787let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_24646 =
    788788  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    789789    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    791791    special_function_registers_8053; special_function_registers_8052 =
    792792    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    793     p3_latch0; clock = clock0 } = x_5550
     793    p3_latch0; clock = clock0 } = x_24646
    794794  in
    795795  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    803803    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    804804    preStatus -> 'a2 **)
    805 let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_5552 =
     805let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_24648 =
    806806  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    807807    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    809809    special_function_registers_8053; special_function_registers_8052 =
    810810    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    811     p3_latch0; clock = clock0 } = x_5552
     811    p3_latch0; clock = clock0 } = x_24648
    812812  in
    813813  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    821821    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    822822    preStatus -> 'a2 **)
    823 let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_5554 =
     823let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_24650 =
    824824  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    825825    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    827827    special_function_registers_8053; special_function_registers_8052 =
    828828    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    829     p3_latch0; clock = clock0 } = x_5554
     829    p3_latch0; clock = clock0 } = x_24650
    830830  in
    831831  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
Note: See TracChangeset for help on using the changeset viewer.