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/globalenvs.ml

    r2649 r2717  
    4848
    4949open Identifiers
     50
     51open Exp
    5052
    5153open Arithmetic
     
    9698    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    9799    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    98 let rec genv_t_rect_Type4 h_mk_genv_t x_4940 =
     100let rec genv_t_rect_Type4 h_mk_genv_t x_6504 =
    99101  let { functions = functions0; nextfunction = nextfunction0; symbols =
    100     symbols0 } = x_4940
     102    symbols0 } = x_6504
    101103  in
    102104  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    105107    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    106108    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    107 let rec genv_t_rect_Type5 h_mk_genv_t x_4942 =
     109let rec genv_t_rect_Type5 h_mk_genv_t x_6506 =
    108110  let { functions = functions0; nextfunction = nextfunction0; symbols =
    109     symbols0 } = x_4942
     111    symbols0 } = x_6506
    110112  in
    111113  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    114116    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    115117    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    116 let rec genv_t_rect_Type3 h_mk_genv_t x_4944 =
     118let rec genv_t_rect_Type3 h_mk_genv_t x_6508 =
    117119  let { functions = functions0; nextfunction = nextfunction0; symbols =
    118     symbols0 } = x_4944
     120    symbols0 } = x_6508
    119121  in
    120122  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    123125    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    124126    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    125 let rec genv_t_rect_Type2 h_mk_genv_t x_4946 =
     127let rec genv_t_rect_Type2 h_mk_genv_t x_6510 =
    126128  let { functions = functions0; nextfunction = nextfunction0; symbols =
    127     symbols0 } = x_4946
     129    symbols0 } = x_6510
    128130  in
    129131  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    132134    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    133135    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    134 let rec genv_t_rect_Type1 h_mk_genv_t x_4948 =
     136let rec genv_t_rect_Type1 h_mk_genv_t x_6512 =
    135137  let { functions = functions0; nextfunction = nextfunction0; symbols =
    136     symbols0 } = x_4948
     138    symbols0 } = x_6512
    137139  in
    138140  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    141143    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    142144    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    143 let rec genv_t_rect_Type0 h_mk_genv_t x_4950 =
     145let rec genv_t_rect_Type0 h_mk_genv_t x_6514 =
    144146  let { functions = functions0; nextfunction = nextfunction0; symbols =
    145     symbols0 } = x_4950
     147    symbols0 } = x_6514
    146148  in
    147149  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    312314let add_globals extract_init init_env vars =
    313315  Util.foldl (fun g_st id_init ->
    314     let { Types.fst = eta295; Types.snd = init_info } = id_init in
    315     let { Types.fst = id; Types.snd = r } = eta295 in
     316    let { Types.fst = eta1792; Types.snd = init_info } = id_init in
     317    let { Types.fst = id; Types.snd = r } = eta1792 in
    316318    let init = extract_init init_info in
    317319    let { Types.fst = g0; Types.snd = st } = g_st in
     
    328330let init_globals extract_init g0 m vars =
    329331  Util.foldl (fun st id_init ->
    330     let { Types.fst = eta296; Types.snd = init_info } = id_init in
    331     let { Types.fst = id; Types.snd = r } = eta296 in
     332    let { Types.fst = eta1793; Types.snd = init_info } = id_init in
     333    let { Types.fst = id; Types.snd = r } = eta1793 in
    332334    let init = extract_init init_info in
    333335    Obj.magic
Note: See TracChangeset for help on using the changeset viewer.