Changeset 2951 for extracted/status.ml


Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (8 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/status.ml

    r2908 r2951  
    8989    serialBufferType -> 'a1 **)
    9090let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
    91 | Eight x_24810 -> h_Eight x_24810
    92 | Nine (x_24812, x_24811) -> h_Nine x_24812 x_24811
     91| Eight x_2622 -> h_Eight x_2622
     92| Nine (x_2624, x_2623) -> h_Nine x_2624 x_2623
    9393
    9494(** val serialBufferType_rect_Type5 :
     
    9696    serialBufferType -> 'a1 **)
    9797let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
    98 | Eight x_24816 -> h_Eight x_24816
    99 | Nine (x_24818, x_24817) -> h_Nine x_24818 x_24817
     98| Eight x_2628 -> h_Eight x_2628
     99| Nine (x_2630, x_2629) -> h_Nine x_2630 x_2629
    100100
    101101(** val serialBufferType_rect_Type3 :
     
    103103    serialBufferType -> 'a1 **)
    104104let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
    105 | Eight x_24822 -> h_Eight x_24822
    106 | Nine (x_24824, x_24823) -> h_Nine x_24824 x_24823
     105| Eight x_2634 -> h_Eight x_2634
     106| Nine (x_2636, x_2635) -> h_Nine x_2636 x_2635
    107107
    108108(** val serialBufferType_rect_Type2 :
     
    110110    serialBufferType -> 'a1 **)
    111111let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
    112 | Eight x_24828 -> h_Eight x_24828
    113 | Nine (x_24830, x_24829) -> h_Nine x_24830 x_24829
     112| Eight x_2640 -> h_Eight x_2640
     113| Nine (x_2642, x_2641) -> h_Nine x_2642 x_2641
    114114
    115115(** val serialBufferType_rect_Type1 :
     
    117117    serialBufferType -> 'a1 **)
    118118let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
    119 | Eight x_24834 -> h_Eight x_24834
    120 | Nine (x_24836, x_24835) -> h_Nine x_24836 x_24835
     119| Eight x_2646 -> h_Eight x_2646
     120| Nine (x_2648, x_2647) -> h_Nine x_2648 x_2647
    121121
    122122(** val serialBufferType_rect_Type0 :
     
    124124    serialBufferType -> 'a1 **)
    125125let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
    126 | Eight x_24840 -> h_Eight x_24840
    127 | Nine (x_24842, x_24841) -> h_Nine x_24842 x_24841
     126| Eight x_2652 -> h_Eight x_2652
     127| Nine (x_2654, x_2653) -> h_Nine x_2654 x_2653
    128128
    129129(** val serialBufferType_inv_rect_Type4 :
     
    182182    -> 'a1) -> lineType -> 'a1 **)
    183183let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
    184 | P1 x_24889 -> h_P1 x_24889
    185 | P3 x_24890 -> h_P3 x_24890
    186 | SerialBuffer x_24891 -> h_SerialBuffer x_24891
     184| P1 x_2701 -> h_P1 x_2701
     185| P3 x_2702 -> h_P3 x_2702
     186| SerialBuffer x_2703 -> h_SerialBuffer x_2703
    187187
    188188(** val lineType_rect_Type5 :
     
    190190    -> 'a1) -> lineType -> 'a1 **)
    191191let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
    192 | P1 x_24896 -> h_P1 x_24896
    193 | P3 x_24897 -> h_P3 x_24897
    194 | SerialBuffer x_24898 -> h_SerialBuffer x_24898
     192| P1 x_2708 -> h_P1 x_2708
     193| P3 x_2709 -> h_P3 x_2709
     194| SerialBuffer x_2710 -> h_SerialBuffer x_2710
    195195
    196196(** val lineType_rect_Type3 :
     
    198198    -> 'a1) -> lineType -> 'a1 **)
    199199let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
    200 | P1 x_24903 -> h_P1 x_24903
    201 | P3 x_24904 -> h_P3 x_24904
    202 | SerialBuffer x_24905 -> h_SerialBuffer x_24905
     200| P1 x_2715 -> h_P1 x_2715
     201| P3 x_2716 -> h_P3 x_2716
     202| SerialBuffer x_2717 -> h_SerialBuffer x_2717
    203203
    204204(** val lineType_rect_Type2 :
     
    206206    -> 'a1) -> lineType -> 'a1 **)
    207207let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
    208 | P1 x_24910 -> h_P1 x_24910
    209 | P3 x_24911 -> h_P3 x_24911
    210 | SerialBuffer x_24912 -> h_SerialBuffer x_24912
     208| P1 x_2722 -> h_P1 x_2722
     209| P3 x_2723 -> h_P3 x_2723
     210| SerialBuffer x_2724 -> h_SerialBuffer x_2724
    211211
    212212(** val lineType_rect_Type1 :
     
    214214    -> 'a1) -> lineType -> 'a1 **)
    215215let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
    216 | P1 x_24917 -> h_P1 x_24917
    217 | P3 x_24918 -> h_P3 x_24918
    218 | SerialBuffer x_24919 -> h_SerialBuffer x_24919
     216| P1 x_2729 -> h_P1 x_2729
     217| P3 x_2730 -> h_P3 x_2730
     218| SerialBuffer x_2731 -> h_SerialBuffer x_2731
    219219
    220220(** val lineType_rect_Type0 :
     
    222222    -> 'a1) -> lineType -> 'a1 **)
    223223let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
    224 | P1 x_24924 -> h_P1 x_24924
    225 | P3 x_24925 -> h_P3 x_24925
    226 | SerialBuffer x_24926 -> h_SerialBuffer x_24926
     224| P1 x_2736 -> h_P1 x_2736
     225| P3 x_2737 -> h_P3 x_2737
     226| SerialBuffer x_2738 -> h_SerialBuffer x_2738
    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_25312 =
     733let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_3124 =
    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_25312
     739    p3_latch0; clock = clock0 } = x_3124
    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_25314 =
     751let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_3126 =
    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_25314
     757    p3_latch0; clock = clock0 } = x_3126
    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_25316 =
     769let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_3128 =
    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_25316
     775    p3_latch0; clock = clock0 } = x_3128
    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_25318 =
     787let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_3130 =
    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_25318
     793    p3_latch0; clock = clock0 } = x_3130
    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_25320 =
     805let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_3132 =
    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_25320
     811    p3_latch0; clock = clock0 } = x_3132
    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_25322 =
     823let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_3134 =
    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_25322
     829    p3_latch0; clock = clock0 } = x_3134
    830830  in
    831831  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
Note: See TracChangeset for help on using the changeset viewer.