Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 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/globalenvs.ml

    r2827 r2951  
    9898    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    9999    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    100 let rec genv_t_rect_Type4 h_mk_genv_t x_6569 =
     100let rec genv_t_rect_Type4 h_mk_genv_t x_6608 =
    101101  let { functions = functions0; nextfunction = nextfunction0; symbols =
    102     symbols0 } = x_6569
     102    symbols0 } = x_6608
    103103  in
    104104  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    107107    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    108108    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    109 let rec genv_t_rect_Type5 h_mk_genv_t x_6571 =
     109let rec genv_t_rect_Type5 h_mk_genv_t x_6610 =
    110110  let { functions = functions0; nextfunction = nextfunction0; symbols =
    111     symbols0 } = x_6571
     111    symbols0 } = x_6610
    112112  in
    113113  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    116116    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    117117    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    118 let rec genv_t_rect_Type3 h_mk_genv_t x_6573 =
     118let rec genv_t_rect_Type3 h_mk_genv_t x_6612 =
    119119  let { functions = functions0; nextfunction = nextfunction0; symbols =
    120     symbols0 } = x_6573
     120    symbols0 } = x_6612
    121121  in
    122122  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    125125    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    126126    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    127 let rec genv_t_rect_Type2 h_mk_genv_t x_6575 =
     127let rec genv_t_rect_Type2 h_mk_genv_t x_6614 =
    128128  let { functions = functions0; nextfunction = nextfunction0; symbols =
    129     symbols0 } = x_6575
     129    symbols0 } = x_6614
    130130  in
    131131  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    134134    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    135135    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    136 let rec genv_t_rect_Type1 h_mk_genv_t x_6577 =
     136let rec genv_t_rect_Type1 h_mk_genv_t x_6616 =
    137137  let { functions = functions0; nextfunction = nextfunction0; symbols =
    138     symbols0 } = x_6577
     138    symbols0 } = x_6616
    139139  in
    140140  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    143143    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    144144    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    145 let rec genv_t_rect_Type0 h_mk_genv_t x_6579 =
     145let rec genv_t_rect_Type0 h_mk_genv_t x_6618 =
    146146  let { functions = functions0; nextfunction = nextfunction0; symbols =
    147     symbols0 } = x_6579
     147    symbols0 } = x_6618
    148148  in
    149149  h_mk_genv_t functions0 nextfunction0 symbols0 __
Note: See TracChangeset for help on using the changeset viewer.