Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (7 years ago)
Author:
sacerdot
Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/globalenvs.ml

    r2730 r2743  
    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_2466 =
     100let rec genv_t_rect_Type4 h_mk_genv_t x_6530 =
    101101  let { functions = functions0; nextfunction = nextfunction0; symbols =
    102     symbols0 } = x_2466
     102    symbols0 } = x_6530
    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_2468 =
     109let rec genv_t_rect_Type5 h_mk_genv_t x_6532 =
    110110  let { functions = functions0; nextfunction = nextfunction0; symbols =
    111     symbols0 } = x_2468
     111    symbols0 } = x_6532
    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_2470 =
     118let rec genv_t_rect_Type3 h_mk_genv_t x_6534 =
    119119  let { functions = functions0; nextfunction = nextfunction0; symbols =
    120     symbols0 } = x_2470
     120    symbols0 } = x_6534
    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_2472 =
     127let rec genv_t_rect_Type2 h_mk_genv_t x_6536 =
    128128  let { functions = functions0; nextfunction = nextfunction0; symbols =
    129     symbols0 } = x_2472
     129    symbols0 } = x_6536
    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_2474 =
     136let rec genv_t_rect_Type1 h_mk_genv_t x_6538 =
    137137  let { functions = functions0; nextfunction = nextfunction0; symbols =
    138     symbols0 } = x_2474
     138    symbols0 } = x_6538
    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_2476 =
     145let rec genv_t_rect_Type0 h_mk_genv_t x_6540 =
    146146  let { functions = functions0; nextfunction = nextfunction0; symbols =
    147     symbols0 } = x_2476
     147    symbols0 } = x_6540
    148148  in
    149149  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    314314let add_globals extract_init init_env vars =
    315315  Util.foldl (fun g_st id_init ->
    316     let { Types.fst = eta860; Types.snd = init_info } = id_init in
    317     let { Types.fst = id; Types.snd = r } = eta860 in
     316    let { Types.fst = eta1792; Types.snd = init_info } = id_init in
     317    let { Types.fst = id; Types.snd = r } = eta1792 in
    318318    let init = extract_init init_info in
    319319    let { Types.fst = g0; Types.snd = st } = g_st in
     
    330330let init_globals extract_init g0 m vars =
    331331  Util.foldl (fun st id_init ->
    332     let { Types.fst = eta861; Types.snd = init_info } = id_init in
    333     let { Types.fst = id; Types.snd = r } = eta861 in
     332    let { Types.fst = eta1793; Types.snd = init_info } = id_init in
     333    let { Types.fst = id; Types.snd = r } = eta1793 in
    334334    let init = extract_init init_info in
    335335    Obj.magic
     
    420420       (symbol_of_function_block' ge b f) })) __
    421421
     422(** val opt_eq_from_res__o__ffpi_drop__o__inject :
     423    Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
     424    Types.sig0 **)
     425let opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 =
     426  __
     427
     428(** val dpi1__o__opt_eq_from_res__o__ffpi_drop__o__inject :
     429    Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__,
     430    'a2) Types.dPair -> __ Types.sig0 **)
     431let dpi1__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 x8 =
     432  __
     433
     434(** val eject__o__opt_eq_from_res__o__ffpi_drop__o__inject :
     435    Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
     436    Types.sig0 -> __ Types.sig0 **)
     437let eject__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 x8 =
     438  __
     439
     440(** val jmeq_to_eq__o__ffpi_drop__o__inject :
     441    Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
     442let jmeq_to_eq__o__ffpi_drop__o__inject x1 x2 x3 x4 =
     443  __
     444
     445(** val jmeq_to_eq__o__opt_eq_from_res__o__ffpi_drop__o__inject :
     446    Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
     447    Types.sig0 **)
     448let jmeq_to_eq__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 =
     449  __
     450
     451(** val dpi1__o__ffpi_drop__o__inject :
     452    Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair
     453    -> __ Types.sig0 **)
     454let dpi1__o__ffpi_drop__o__inject x1 x2 x3 x4 x7 =
     455  __
     456
     457(** val eject__o__ffpi_drop__o__inject :
     458    Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
     459    Types.sig0 **)
     460let eject__o__ffpi_drop__o__inject x1 x2 x3 x4 x7 =
     461  __
     462
     463(** val ffpi_drop__o__inject :
     464    Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
     465let ffpi_drop__o__inject x1 x2 x3 x4 =
     466  __
     467
    422468(** val symbol_of_function_val : 'a1 genv_t -> Values.val0 -> AST.ident **)
    423469let symbol_of_function_val ge v =
     
    442488     (fun _ -> Types.Some { Types.fst = f; Types.snd =
    443489       (symbol_of_function_val' ge v f) })) __
     490
     491(** val opt_eq_from_res__o__ffi_drop__o__inject :
     492    Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
     493    Types.sig0 **)
     494let opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 =
     495  __
     496
     497(** val dpi1__o__opt_eq_from_res__o__ffi_drop__o__inject :
     498    Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__,
     499    'a2) Types.dPair -> __ Types.sig0 **)
     500let dpi1__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 x8 =
     501  __
     502
     503(** val eject__o__opt_eq_from_res__o__ffi_drop__o__inject :
     504    Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
     505    Types.sig0 -> __ Types.sig0 **)
     506let eject__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 x8 =
     507  __
     508
     509(** val jmeq_to_eq__o__ffi_drop__o__inject :
     510    Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
     511let jmeq_to_eq__o__ffi_drop__o__inject x1 x2 x3 x4 =
     512  __
     513
     514(** val jmeq_to_eq__o__opt_eq_from_res__o__ffi_drop__o__inject :
     515    Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
     516    Types.sig0 **)
     517let jmeq_to_eq__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 =
     518  __
     519
     520(** val dpi1__o__ffi_drop__o__inject :
     521    Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair ->
     522    __ Types.sig0 **)
     523let dpi1__o__ffi_drop__o__inject x1 x2 x3 x4 x7 =
     524  __
     525
     526(** val eject__o__ffi_drop__o__inject :
     527    Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
     528    Types.sig0 **)
     529let eject__o__ffi_drop__o__inject x1 x2 x3 x4 x7 =
     530  __
     531
     532(** val ffi_drop__o__inject :
     533    Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
     534let ffi_drop__o__inject x1 x2 x3 x4 =
     535  __
    444536
    445537(** val nat_plus_pos : Nat.nat -> Positive.pos -> Positive.pos **)
Note: See TracChangeset for help on using the changeset viewer.