Changeset 2649 for extracted/status.ml


Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/status.ml

    r2601 r2649  
    11open Preamble
    22
     3open String
     4
    35open LabelledObjects
    46
    5 open Coqlib
    6 
    7 open Floats
    8 
    97open Arithmetic
    108
     
    2119open Deqsets
    2220
     21open ErrorMessages
     22
    2323open PreIdentifiers
    2424
     
    3838
    3939open Identifiers
    40 
    41 open Char
    42 
    43 open String
    4440
    4541open Extranat
     
    9187    serialBufferType -> 'a1 **)
    9288let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
    93 | Eight x_16874 -> h_Eight x_16874
    94 | Nine (x_16876, x_16875) -> h_Nine x_16876 x_16875
     89| Eight x_2231 -> h_Eight x_2231
     90| Nine (x_2233, x_2232) -> h_Nine x_2233 x_2232
    9591
    9692(** val serialBufferType_rect_Type5 :
     
    9894    serialBufferType -> 'a1 **)
    9995let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
    100 | Eight x_16880 -> h_Eight x_16880
    101 | Nine (x_16882, x_16881) -> h_Nine x_16882 x_16881
     96| Eight x_2237 -> h_Eight x_2237
     97| Nine (x_2239, x_2238) -> h_Nine x_2239 x_2238
    10298
    10399(** val serialBufferType_rect_Type3 :
     
    105101    serialBufferType -> 'a1 **)
    106102let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
    107 | Eight x_16886 -> h_Eight x_16886
    108 | Nine (x_16888, x_16887) -> h_Nine x_16888 x_16887
     103| Eight x_2243 -> h_Eight x_2243
     104| Nine (x_2245, x_2244) -> h_Nine x_2245 x_2244
    109105
    110106(** val serialBufferType_rect_Type2 :
     
    112108    serialBufferType -> 'a1 **)
    113109let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
    114 | Eight x_16892 -> h_Eight x_16892
    115 | Nine (x_16894, x_16893) -> h_Nine x_16894 x_16893
     110| Eight x_2249 -> h_Eight x_2249
     111| Nine (x_2251, x_2250) -> h_Nine x_2251 x_2250
    116112
    117113(** val serialBufferType_rect_Type1 :
     
    119115    serialBufferType -> 'a1 **)
    120116let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
    121 | Eight x_16898 -> h_Eight x_16898
    122 | Nine (x_16900, x_16899) -> h_Nine x_16900 x_16899
     117| Eight x_2255 -> h_Eight x_2255
     118| Nine (x_2257, x_2256) -> h_Nine x_2257 x_2256
    123119
    124120(** val serialBufferType_rect_Type0 :
     
    126122    serialBufferType -> 'a1 **)
    127123let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
    128 | Eight x_16904 -> h_Eight x_16904
    129 | Nine (x_16906, x_16905) -> h_Nine x_16906 x_16905
     124| Eight x_2261 -> h_Eight x_2261
     125| Nine (x_2263, x_2262) -> h_Nine x_2263 x_2262
    130126
    131127(** val serialBufferType_inv_rect_Type4 :
     
    184180    -> 'a1) -> lineType -> 'a1 **)
    185181let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
    186 | P2 x_16953 -> h_P1 x_16953
    187 | P3 x_16954 -> h_P3 x_16954
    188 | SerialBuffer x_16955 -> h_SerialBuffer x_16955
     182| P2 x_2310 -> h_P1 x_2310
     183| P3 x_2311 -> h_P3 x_2311
     184| SerialBuffer x_2312 -> h_SerialBuffer x_2312
    189185
    190186(** val lineType_rect_Type5 :
     
    192188    -> 'a1) -> lineType -> 'a1 **)
    193189let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
    194 | P2 x_16960 -> h_P1 x_16960
    195 | P3 x_16961 -> h_P3 x_16961
    196 | SerialBuffer x_16962 -> h_SerialBuffer x_16962
     190| P2 x_2317 -> h_P1 x_2317
     191| P3 x_2318 -> h_P3 x_2318
     192| SerialBuffer x_2319 -> h_SerialBuffer x_2319
    197193
    198194(** val lineType_rect_Type3 :
     
    200196    -> 'a1) -> lineType -> 'a1 **)
    201197let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
    202 | P2 x_16967 -> h_P1 x_16967
    203 | P3 x_16968 -> h_P3 x_16968
    204 | SerialBuffer x_16969 -> h_SerialBuffer x_16969
     198| P2 x_2324 -> h_P1 x_2324
     199| P3 x_2325 -> h_P3 x_2325
     200| SerialBuffer x_2326 -> h_SerialBuffer x_2326
    205201
    206202(** val lineType_rect_Type2 :
     
    208204    -> 'a1) -> lineType -> 'a1 **)
    209205let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
    210 | P2 x_16974 -> h_P1 x_16974
    211 | P3 x_16975 -> h_P3 x_16975
    212 | SerialBuffer x_16976 -> h_SerialBuffer x_16976
     206| P2 x_2331 -> h_P1 x_2331
     207| P3 x_2332 -> h_P3 x_2332
     208| SerialBuffer x_2333 -> h_SerialBuffer x_2333
    213209
    214210(** val lineType_rect_Type1 :
     
    216212    -> 'a1) -> lineType -> 'a1 **)
    217213let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
    218 | P2 x_16981 -> h_P1 x_16981
    219 | P3 x_16982 -> h_P3 x_16982
    220 | SerialBuffer x_16983 -> h_SerialBuffer x_16983
     214| P2 x_2338 -> h_P1 x_2338
     215| P3 x_2339 -> h_P3 x_2339
     216| SerialBuffer x_2340 -> h_SerialBuffer x_2340
    221217
    222218(** val lineType_rect_Type0 :
     
    224220    -> 'a1) -> lineType -> 'a1 **)
    225221let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
    226 | P2 x_16988 -> h_P1 x_16988
    227 | P3 x_16989 -> h_P3 x_16989
    228 | SerialBuffer x_16990 -> h_SerialBuffer x_16990
     222| P2 x_2345 -> h_P1 x_2345
     223| P3 x_2346 -> h_P3 x_2346
     224| SerialBuffer x_2347 -> h_SerialBuffer x_2347
    229225
    230226(** val lineType_inv_rect_Type4 :
     
    733729    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    734730    preStatus -> 'a2 **)
    735 let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_17376 =
     731let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_2733 =
    736732  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    737733    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    739735    special_function_registers_8053; special_function_registers_8052 =
    740736    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    741     p3_latch0; clock = clock0 } = x_17376
     737    p3_latch0; clock = clock0 } = x_2733
    742738  in
    743739  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    751747    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    752748    preStatus -> 'a2 **)
    753 let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_17378 =
     749let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_2735 =
    754750  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    755751    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    757753    special_function_registers_8053; special_function_registers_8052 =
    758754    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    759     p3_latch0; clock = clock0 } = x_17378
     755    p3_latch0; clock = clock0 } = x_2735
    760756  in
    761757  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    769765    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    770766    preStatus -> 'a2 **)
    771 let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_17380 =
     767let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_2737 =
    772768  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    773769    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    775771    special_function_registers_8053; special_function_registers_8052 =
    776772    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    777     p3_latch0; clock = clock0 } = x_17380
     773    p3_latch0; clock = clock0 } = x_2737
    778774  in
    779775  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    787783    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    788784    preStatus -> 'a2 **)
    789 let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_17382 =
     785let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_2739 =
    790786  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    791787    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    793789    special_function_registers_8053; special_function_registers_8052 =
    794790    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    795     p3_latch0; clock = clock0 } = x_17382
     791    p3_latch0; clock = clock0 } = x_2739
    796792  in
    797793  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    805801    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    806802    preStatus -> 'a2 **)
    807 let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_17384 =
     803let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_2741 =
    808804  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    809805    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    811807    special_function_registers_8053; special_function_registers_8052 =
    812808    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    813     p3_latch0; clock = clock0 } = x_17384
     809    p3_latch0; clock = clock0 } = x_2741
    814810  in
    815811  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    823819    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    824820    preStatus -> 'a2 **)
    825 let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_17386 =
     821let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_2743 =
    826822  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    827823    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    829825    special_function_registers_8053; special_function_registers_8052 =
    830826    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    831     p3_latch0; clock = clock0 } = x_17386
     827    p3_latch0; clock = clock0 } = x_2743
    832828  in
    833829  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    42844280        Nat.O)))))))))))))))) addr size
    42854281    in
    4286     { Types.fst = (Identifiers.add ASM.aSMTag datalabels name addr);
    4287     Types.snd = sum0 }) { Types.fst = (Identifiers.empty_map ASM.aSMTag);
     4282    { Types.fst =
     4283    (Identifiers.add PreIdentifiers.ASMTag datalabels name addr); Types.snd =
     4284    sum0 }) { Types.fst = (Identifiers.empty_map PreIdentifiers.ASMTag);
    42884285    Types.snd =
    42894286    (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.