Changeset 2717 for extracted/status.ml


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/status.ml

    r2649 r2717  
    55open LabelledObjects
    66
     7open BitVectorTrie
     8
     9open Exp
     10
    711open Arithmetic
    812
     
    7478
    7579open ASM
    76 
    77 open BitVectorTrie
    7880
    7981type time = Nat.nat
     
    8789    serialBufferType -> 'a1 **)
    8890let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
    89 | Eight x_2231 -> h_Eight x_2231
    90 | Nine (x_2233, x_2232) -> h_Nine x_2233 x_2232
     91| Eight x_21058 -> h_Eight x_21058
     92| Nine (x_21060, x_21059) -> h_Nine x_21060 x_21059
    9193
    9294(** val serialBufferType_rect_Type5 :
     
    9496    serialBufferType -> 'a1 **)
    9597let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
    96 | Eight x_2237 -> h_Eight x_2237
    97 | Nine (x_2239, x_2238) -> h_Nine x_2239 x_2238
     98| Eight x_21064 -> h_Eight x_21064
     99| Nine (x_21066, x_21065) -> h_Nine x_21066 x_21065
    98100
    99101(** val serialBufferType_rect_Type3 :
     
    101103    serialBufferType -> 'a1 **)
    102104let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
    103 | Eight x_2243 -> h_Eight x_2243
    104 | Nine (x_2245, x_2244) -> h_Nine x_2245 x_2244
     105| Eight x_21070 -> h_Eight x_21070
     106| Nine (x_21072, x_21071) -> h_Nine x_21072 x_21071
    105107
    106108(** val serialBufferType_rect_Type2 :
     
    108110    serialBufferType -> 'a1 **)
    109111let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
    110 | Eight x_2249 -> h_Eight x_2249
    111 | Nine (x_2251, x_2250) -> h_Nine x_2251 x_2250
     112| Eight x_21076 -> h_Eight x_21076
     113| Nine (x_21078, x_21077) -> h_Nine x_21078 x_21077
    112114
    113115(** val serialBufferType_rect_Type1 :
     
    115117    serialBufferType -> 'a1 **)
    116118let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
    117 | Eight x_2255 -> h_Eight x_2255
    118 | Nine (x_2257, x_2256) -> h_Nine x_2257 x_2256
     119| Eight x_21082 -> h_Eight x_21082
     120| Nine (x_21084, x_21083) -> h_Nine x_21084 x_21083
    119121
    120122(** val serialBufferType_rect_Type0 :
     
    122124    serialBufferType -> 'a1 **)
    123125let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
    124 | Eight x_2261 -> h_Eight x_2261
    125 | Nine (x_2263, x_2262) -> h_Nine x_2263 x_2262
     126| Eight x_21088 -> h_Eight x_21088
     127| Nine (x_21090, x_21089) -> h_Nine x_21090 x_21089
    126128
    127129(** val serialBufferType_inv_rect_Type4 :
     
    180182    -> 'a1) -> lineType -> 'a1 **)
    181183let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
    182 | P2 x_2310 -> h_P1 x_2310
    183 | P3 x_2311 -> h_P3 x_2311
    184 | SerialBuffer x_2312 -> h_SerialBuffer x_2312
     184| P2 x_21137 -> h_P1 x_21137
     185| P3 x_21138 -> h_P3 x_21138
     186| SerialBuffer x_21139 -> h_SerialBuffer x_21139
    185187
    186188(** val lineType_rect_Type5 :
     
    188190    -> 'a1) -> lineType -> 'a1 **)
    189191let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
    190 | P2 x_2317 -> h_P1 x_2317
    191 | P3 x_2318 -> h_P3 x_2318
    192 | SerialBuffer x_2319 -> h_SerialBuffer x_2319
     192| P2 x_21144 -> h_P1 x_21144
     193| P3 x_21145 -> h_P3 x_21145
     194| SerialBuffer x_21146 -> h_SerialBuffer x_21146
    193195
    194196(** val lineType_rect_Type3 :
     
    196198    -> 'a1) -> lineType -> 'a1 **)
    197199let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
    198 | P2 x_2324 -> h_P1 x_2324
    199 | P3 x_2325 -> h_P3 x_2325
    200 | SerialBuffer x_2326 -> h_SerialBuffer x_2326
     200| P2 x_21151 -> h_P1 x_21151
     201| P3 x_21152 -> h_P3 x_21152
     202| SerialBuffer x_21153 -> h_SerialBuffer x_21153
    201203
    202204(** val lineType_rect_Type2 :
     
    204206    -> 'a1) -> lineType -> 'a1 **)
    205207let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
    206 | P2 x_2331 -> h_P1 x_2331
    207 | P3 x_2332 -> h_P3 x_2332
    208 | SerialBuffer x_2333 -> h_SerialBuffer x_2333
     208| P2 x_21158 -> h_P1 x_21158
     209| P3 x_21159 -> h_P3 x_21159
     210| SerialBuffer x_21160 -> h_SerialBuffer x_21160
    209211
    210212(** val lineType_rect_Type1 :
     
    212214    -> 'a1) -> lineType -> 'a1 **)
    213215let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
    214 | P2 x_2338 -> h_P1 x_2338
    215 | P3 x_2339 -> h_P3 x_2339
    216 | SerialBuffer x_2340 -> h_SerialBuffer x_2340
     216| P2 x_21165 -> h_P1 x_21165
     217| P3 x_21166 -> h_P3 x_21166
     218| SerialBuffer x_21167 -> h_SerialBuffer x_21167
    217219
    218220(** val lineType_rect_Type0 :
     
    220222    -> 'a1) -> lineType -> 'a1 **)
    221223let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
    222 | P2 x_2345 -> h_P1 x_2345
    223 | P3 x_2346 -> h_P3 x_2346
    224 | SerialBuffer x_2347 -> h_SerialBuffer x_2347
     224| P2 x_21172 -> h_P1 x_21172
     225| P3 x_21173 -> h_P3 x_21173
     226| SerialBuffer x_21174 -> h_SerialBuffer x_21174
    225227
    226228(** val lineType_inv_rect_Type4 :
     
    729731    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    730732    preStatus -> 'a2 **)
    731 let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_2733 =
     733let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_21560 =
    732734  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    733735    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    735737    special_function_registers_8053; special_function_registers_8052 =
    736738    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    737     p3_latch0; clock = clock0 } = x_2733
     739    p3_latch0; clock = clock0 } = x_21560
    738740  in
    739741  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    747749    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    748750    preStatus -> 'a2 **)
    749 let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_2735 =
     751let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_21562 =
    750752  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    751753    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    753755    special_function_registers_8053; special_function_registers_8052 =
    754756    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    755     p3_latch0; clock = clock0 } = x_2735
     757    p3_latch0; clock = clock0 } = x_21562
    756758  in
    757759  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    765767    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    766768    preStatus -> 'a2 **)
    767 let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_2737 =
     769let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_21564 =
    768770  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    769771    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    771773    special_function_registers_8053; special_function_registers_8052 =
    772774    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    773     p3_latch0; clock = clock0 } = x_2737
     775    p3_latch0; clock = clock0 } = x_21564
    774776  in
    775777  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    783785    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    784786    preStatus -> 'a2 **)
    785 let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_2739 =
     787let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_21566 =
    786788  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    787789    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    789791    special_function_registers_8053; special_function_registers_8052 =
    790792    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    791     p3_latch0; clock = clock0 } = x_2739
     793    p3_latch0; clock = clock0 } = x_21566
    792794  in
    793795  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    801803    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    802804    preStatus -> 'a2 **)
    803 let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_2741 =
     805let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_21568 =
    804806  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    805807    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    807809    special_function_registers_8053; special_function_registers_8052 =
    808810    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    809     p3_latch0; clock = clock0 } = x_2741
     811    p3_latch0; clock = clock0 } = x_21568
    810812  in
    811813  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    819821    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    820822    preStatus -> 'a2 **)
    821 let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_2743 =
     823let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_21570 =
    822824  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    823825    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    825827    special_function_registers_8053; special_function_registers_8052 =
    826828    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    827     p3_latch0; clock = clock0 } = x_2743
     829    p3_latch0; clock = clock0 } = x_21570
    828830  in
    829831  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    42864288    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    42874289      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4288       Nat.O))))))))))))))))) } the_preamble.Types.snd).Types.fst
    4289 
     4290      Nat.O))))))))))))))))) } the_preamble).Types.fst
     4291
Note: See TracChangeset for help on using the changeset viewer.