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

    r2649 r2717  
    5151(** val universe_rect_Type4 :
    5252    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    53 let rec universe_rect_Type4 tag h_mk_universe x_1095 =
    54   let next_identifier = x_1095 in h_mk_universe next_identifier
     53let rec universe_rect_Type4 tag h_mk_universe x_3057 =
     54  let next_identifier = x_3057 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_1097 =
    59   let next_identifier = x_1097 in h_mk_universe next_identifier
     58let rec universe_rect_Type5 tag h_mk_universe x_3059 =
     59  let next_identifier = x_3059 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_1099 =
    64   let next_identifier = x_1099 in h_mk_universe next_identifier
     63let rec universe_rect_Type3 tag h_mk_universe x_3061 =
     64  let next_identifier = x_3061 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_1101 =
    69   let next_identifier = x_1101 in h_mk_universe next_identifier
     68let rec universe_rect_Type2 tag h_mk_universe x_3063 =
     69  let next_identifier = x_3063 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_1103 =
    74   let next_identifier = x_1103 in h_mk_universe next_identifier
     73let rec universe_rect_Type1 tag h_mk_universe x_3065 =
     74  let next_identifier = x_3065 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_1105 =
    79   let next_identifier = x_1105 in h_mk_universe next_identifier
     78let rec universe_rect_Type0 tag h_mk_universe x_3067 =
     79  let next_identifier = x_3067 in h_mk_universe next_identifier
    8080
    8181(** val next_identifier :
     
    221221    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    222222    'a1 identifier_map -> 'a2 **)
    223 let rec identifier_map_rect_Type4 tag h_an_id_map x_1122 =
    224   let x_1123 = x_1122 in h_an_id_map x_1123
     223let rec identifier_map_rect_Type4 tag h_an_id_map x_3229 =
     224  let x_3230 = x_3229 in h_an_id_map x_3230
    225225
    226226(** val identifier_map_rect_Type5 :
    227227    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    228228    'a1 identifier_map -> 'a2 **)
    229 let rec identifier_map_rect_Type5 tag h_an_id_map x_1125 =
    230   let x_1126 = x_1125 in h_an_id_map x_1126
     229let rec identifier_map_rect_Type5 tag h_an_id_map x_3232 =
     230  let x_3233 = x_3232 in h_an_id_map x_3233
    231231
    232232(** val identifier_map_rect_Type3 :
    233233    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    234234    'a1 identifier_map -> 'a2 **)
    235 let rec identifier_map_rect_Type3 tag h_an_id_map x_1128 =
    236   let x_1129 = x_1128 in h_an_id_map x_1129
     235let rec identifier_map_rect_Type3 tag h_an_id_map x_3235 =
     236  let x_3236 = x_3235 in h_an_id_map x_3236
    237237
    238238(** val identifier_map_rect_Type2 :
    239239    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    240240    'a1 identifier_map -> 'a2 **)
    241 let rec identifier_map_rect_Type2 tag h_an_id_map x_1131 =
    242   let x_1132 = x_1131 in h_an_id_map x_1132
     241let rec identifier_map_rect_Type2 tag h_an_id_map x_3238 =
     242  let x_3239 = x_3238 in h_an_id_map x_3239
    243243
    244244(** val identifier_map_rect_Type1 :
    245245    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    246246    'a1 identifier_map -> 'a2 **)
    247 let rec identifier_map_rect_Type1 tag h_an_id_map x_1134 =
    248   let x_1135 = x_1134 in h_an_id_map x_1135
     247let rec identifier_map_rect_Type1 tag h_an_id_map x_3241 =
     248  let x_3242 = x_3241 in h_an_id_map x_3242
    249249
    250250(** val identifier_map_rect_Type0 :
    251251    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    252252    'a1 identifier_map -> 'a2 **)
    253 let rec identifier_map_rect_Type0 tag h_an_id_map x_1137 =
    254   let x_1138 = x_1137 in h_an_id_map x_1138
     253let rec identifier_map_rect_Type0 tag h_an_id_map x_3244 =
     254  let x_3245 = x_3244 in h_an_id_map x_3245
    255255
    256256(** val identifier_map_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.