Ignore:
Timestamp:
Mar 5, 2013, 9:52:39 PM (8 years ago)
Author:
sacerdot
Message:

The compiler now computes also the stack cost model.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/identifiers.ml

    r2773 r2775  
    5151(** val universe_rect_Type4 :
    5252    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    53 let rec universe_rect_Type4 tag h_mk_universe x_3343 =
    54   let next_identifier = x_3343 in h_mk_universe next_identifier
     53let rec universe_rect_Type4 tag h_mk_universe x_3096 =
     54  let next_identifier = x_3096 in h_mk_universe next_identifier
    5555
    5656(** val universe_rect_Type5 :
    5757    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    58 let rec universe_rect_Type5 tag h_mk_universe x_3345 =
    59   let next_identifier = x_3345 in h_mk_universe next_identifier
     58let rec universe_rect_Type5 tag h_mk_universe x_3098 =
     59  let next_identifier = x_3098 in h_mk_universe next_identifier
    6060
    6161(** val universe_rect_Type3 :
    6262    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    63 let rec universe_rect_Type3 tag h_mk_universe x_3347 =
    64   let next_identifier = x_3347 in h_mk_universe next_identifier
     63let rec universe_rect_Type3 tag h_mk_universe x_3100 =
     64  let next_identifier = x_3100 in h_mk_universe next_identifier
    6565
    6666(** val universe_rect_Type2 :
    6767    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    68 let rec universe_rect_Type2 tag h_mk_universe x_3349 =
    69   let next_identifier = x_3349 in h_mk_universe next_identifier
     68let rec universe_rect_Type2 tag h_mk_universe x_3102 =
     69  let next_identifier = x_3102 in h_mk_universe next_identifier
    7070
    7171(** val universe_rect_Type1 :
    7272    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    73 let rec universe_rect_Type1 tag h_mk_universe x_3351 =
    74   let next_identifier = x_3351 in h_mk_universe next_identifier
     73let rec universe_rect_Type1 tag h_mk_universe x_3104 =
     74  let next_identifier = x_3104 in h_mk_universe next_identifier
    7575
    7676(** val universe_rect_Type0 :
    7777    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    78 let rec universe_rect_Type0 tag h_mk_universe x_3353 =
    79   let next_identifier = x_3353 in h_mk_universe next_identifier
     78let rec universe_rect_Type0 tag h_mk_universe x_3106 =
     79  let next_identifier = x_3106 in h_mk_universe next_identifier
    8080
    8181(** val next_identifier :
     
    215215    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    216216    'a1 identifier_map -> 'a2 **)
    217 let rec identifier_map_rect_Type4 tag h_an_id_map x_3515 =
    218   let x_3516 = x_3515 in h_an_id_map x_3516
     217let rec identifier_map_rect_Type4 tag h_an_id_map x_3268 =
     218  let x_3269 = x_3268 in h_an_id_map x_3269
    219219
    220220(** val identifier_map_rect_Type5 :
    221221    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    222222    'a1 identifier_map -> 'a2 **)
    223 let rec identifier_map_rect_Type5 tag h_an_id_map x_3518 =
    224   let x_3519 = x_3518 in h_an_id_map x_3519
     223let rec identifier_map_rect_Type5 tag h_an_id_map x_3271 =
     224  let x_3272 = x_3271 in h_an_id_map x_3272
    225225
    226226(** val identifier_map_rect_Type3 :
    227227    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    228228    'a1 identifier_map -> 'a2 **)
    229 let rec identifier_map_rect_Type3 tag h_an_id_map x_3521 =
    230   let x_3522 = x_3521 in h_an_id_map x_3522
     229let rec identifier_map_rect_Type3 tag h_an_id_map x_3274 =
     230  let x_3275 = x_3274 in h_an_id_map x_3275
    231231
    232232(** val identifier_map_rect_Type2 :
    233233    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    234234    'a1 identifier_map -> 'a2 **)
    235 let rec identifier_map_rect_Type2 tag h_an_id_map x_3524 =
    236   let x_3525 = x_3524 in h_an_id_map x_3525
     235let rec identifier_map_rect_Type2 tag h_an_id_map x_3277 =
     236  let x_3278 = x_3277 in h_an_id_map x_3278
    237237
    238238(** val identifier_map_rect_Type1 :
    239239    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    240240    'a1 identifier_map -> 'a2 **)
    241 let rec identifier_map_rect_Type1 tag h_an_id_map x_3527 =
    242   let x_3528 = x_3527 in h_an_id_map x_3528
     241let rec identifier_map_rect_Type1 tag h_an_id_map x_3280 =
     242  let x_3281 = x_3280 in h_an_id_map x_3281
    243243
    244244(** val identifier_map_rect_Type0 :
    245245    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    246246    'a1 identifier_map -> 'a2 **)
    247 let rec identifier_map_rect_Type0 tag h_an_id_map x_3530 =
    248   let x_3531 = x_3530 in h_an_id_map x_3531
     247let rec identifier_map_rect_Type0 tag h_an_id_map x_3283 =
     248  let x_3284 = x_3283 in h_an_id_map x_3284
    249249
    250250(** val identifier_map_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.