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

    r2730 r2743  
    161161    'a1 **)
    162162let rec program_behavior_rect_Type4 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    163 | Terminates (x_5329, x_5328) -> h_Terminates x_5329 x_5328
    164 | Diverges x_5330 -> h_Diverges x_5330
    165 | Reacts x_5331 -> h_Reacts x_5331
    166 | Goes_wrong x_5332 -> h_Goes_wrong x_5332
     163| Terminates (x_6874, x_6873) -> h_Terminates x_6874 x_6873
     164| Diverges x_6875 -> h_Diverges x_6875
     165| Reacts x_6876 -> h_Reacts x_6876
     166| Goes_wrong x_6877 -> h_Goes_wrong x_6877
    167167
    168168(** val program_behavior_rect_Type5 :
     
    171171    'a1 **)
    172172let rec program_behavior_rect_Type5 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    173 | Terminates (x_5339, x_5338) -> h_Terminates x_5339 x_5338
    174 | Diverges x_5340 -> h_Diverges x_5340
    175 | Reacts x_5341 -> h_Reacts x_5341
    176 | Goes_wrong x_5342 -> h_Goes_wrong x_5342
     173| Terminates (x_6884, x_6883) -> h_Terminates x_6884 x_6883
     174| Diverges x_6885 -> h_Diverges x_6885
     175| Reacts x_6886 -> h_Reacts x_6886
     176| Goes_wrong x_6887 -> h_Goes_wrong x_6887
    177177
    178178(** val program_behavior_rect_Type3 :
     
    181181    'a1 **)
    182182let rec program_behavior_rect_Type3 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    183 | Terminates (x_5349, x_5348) -> h_Terminates x_5349 x_5348
    184 | Diverges x_5350 -> h_Diverges x_5350
    185 | Reacts x_5351 -> h_Reacts x_5351
    186 | Goes_wrong x_5352 -> h_Goes_wrong x_5352
     183| Terminates (x_6894, x_6893) -> h_Terminates x_6894 x_6893
     184| Diverges x_6895 -> h_Diverges x_6895
     185| Reacts x_6896 -> h_Reacts x_6896
     186| Goes_wrong x_6897 -> h_Goes_wrong x_6897
    187187
    188188(** val program_behavior_rect_Type2 :
     
    191191    'a1 **)
    192192let rec program_behavior_rect_Type2 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    193 | Terminates (x_5359, x_5358) -> h_Terminates x_5359 x_5358
    194 | Diverges x_5360 -> h_Diverges x_5360
    195 | Reacts x_5361 -> h_Reacts x_5361
    196 | Goes_wrong x_5362 -> h_Goes_wrong x_5362
     193| Terminates (x_6904, x_6903) -> h_Terminates x_6904 x_6903
     194| Diverges x_6905 -> h_Diverges x_6905
     195| Reacts x_6906 -> h_Reacts x_6906
     196| Goes_wrong x_6907 -> h_Goes_wrong x_6907
    197197
    198198(** val program_behavior_rect_Type1 :
     
    201201    'a1 **)
    202202let rec program_behavior_rect_Type1 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    203 | Terminates (x_5369, x_5368) -> h_Terminates x_5369 x_5368
    204 | Diverges x_5370 -> h_Diverges x_5370
    205 | Reacts x_5371 -> h_Reacts x_5371
    206 | Goes_wrong x_5372 -> h_Goes_wrong x_5372
     203| Terminates (x_6914, x_6913) -> h_Terminates x_6914 x_6913
     204| Diverges x_6915 -> h_Diverges x_6915
     205| Reacts x_6916 -> h_Reacts x_6916
     206| Goes_wrong x_6917 -> h_Goes_wrong x_6917
    207207
    208208(** val program_behavior_rect_Type0 :
     
    211211    'a1 **)
    212212let rec program_behavior_rect_Type0 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    213 | Terminates (x_5379, x_5378) -> h_Terminates x_5379 x_5378
    214 | Diverges x_5380 -> h_Diverges x_5380
    215 | Reacts x_5381 -> h_Reacts x_5381
    216 | Goes_wrong x_5382 -> h_Goes_wrong x_5382
     213| Terminates (x_6924, x_6923) -> h_Terminates x_6924 x_6923
     214| Diverges x_6925 -> h_Diverges x_6925
     215| Reacts x_6926 -> h_Reacts x_6926
     216| Goes_wrong x_6927 -> h_Goes_wrong x_6927
    217217
    218218(** val program_behavior_inv_rect_Type4 :
     
    275275(** val semantics_rect_Type4 :
    276276    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    277 let rec semantics_rect_Type4 h_mk_semantics x_5709 =
    278   let { trans = trans0; ge = ge0 } = x_5709 in
     277let rec semantics_rect_Type4 h_mk_semantics x_7254 =
     278  let { trans = trans0; ge = ge0 } = x_7254 in
    279279  h_mk_semantics trans0 __ __ ge0
    280280
    281281(** val semantics_rect_Type5 :
    282282    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    283 let rec semantics_rect_Type5 h_mk_semantics x_5711 =
    284   let { trans = trans0; ge = ge0 } = x_5711 in
     283let rec semantics_rect_Type5 h_mk_semantics x_7256 =
     284  let { trans = trans0; ge = ge0 } = x_7256 in
    285285  h_mk_semantics trans0 __ __ ge0
    286286
    287287(** val semantics_rect_Type3 :
    288288    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    289 let rec semantics_rect_Type3 h_mk_semantics x_5713 =
    290   let { trans = trans0; ge = ge0 } = x_5713 in
     289let rec semantics_rect_Type3 h_mk_semantics x_7258 =
     290  let { trans = trans0; ge = ge0 } = x_7258 in
    291291  h_mk_semantics trans0 __ __ ge0
    292292
    293293(** val semantics_rect_Type2 :
    294294    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    295 let rec semantics_rect_Type2 h_mk_semantics x_5715 =
    296   let { trans = trans0; ge = ge0 } = x_5715 in
     295let rec semantics_rect_Type2 h_mk_semantics x_7260 =
     296  let { trans = trans0; ge = ge0 } = x_7260 in
    297297  h_mk_semantics trans0 __ __ ge0
    298298
    299299(** val semantics_rect_Type1 :
    300300    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    301 let rec semantics_rect_Type1 h_mk_semantics x_5717 =
    302   let { trans = trans0; ge = ge0 } = x_5717 in
     301let rec semantics_rect_Type1 h_mk_semantics x_7262 =
     302  let { trans = trans0; ge = ge0 } = x_7262 in
    303303  h_mk_semantics trans0 __ __ ge0
    304304
    305305(** val semantics_rect_Type0 :
    306306    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    307 let rec semantics_rect_Type0 h_mk_semantics x_5719 =
    308   let { trans = trans0; ge = ge0 } = x_5719 in
     307let rec semantics_rect_Type0 h_mk_semantics x_7264 =
     308  let { trans = trans0; ge = ge0 } = x_7264 in
    309309  h_mk_semantics trans0 __ __ ge0
    310310
     
    357357    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    358358    'a1 **)
    359 let rec related_semantics_rect_Type4 h_mk_related_semantics x_5738 =
    360   let { sem1 = sem3; sem2 = sem4 } = x_5738 in
     359let rec related_semantics_rect_Type4 h_mk_related_semantics x_7283 =
     360  let { sem1 = sem3; sem2 = sem4 } = x_7283 in
    361361  h_mk_related_semantics sem3 sem4 __ __ __
    362362
     
    364364    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    365365    'a1 **)
    366 let rec related_semantics_rect_Type5 h_mk_related_semantics x_5740 =
    367   let { sem1 = sem3; sem2 = sem4 } = x_5740 in
     366let rec related_semantics_rect_Type5 h_mk_related_semantics x_7285 =
     367  let { sem1 = sem3; sem2 = sem4 } = x_7285 in
    368368  h_mk_related_semantics sem3 sem4 __ __ __
    369369
     
    371371    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    372372    'a1 **)
    373 let rec related_semantics_rect_Type3 h_mk_related_semantics x_5742 =
    374   let { sem1 = sem3; sem2 = sem4 } = x_5742 in
     373let rec related_semantics_rect_Type3 h_mk_related_semantics x_7287 =
     374  let { sem1 = sem3; sem2 = sem4 } = x_7287 in
    375375  h_mk_related_semantics sem3 sem4 __ __ __
    376376
     
    378378    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    379379    'a1 **)
    380 let rec related_semantics_rect_Type2 h_mk_related_semantics x_5744 =
    381   let { sem1 = sem3; sem2 = sem4 } = x_5744 in
     380let rec related_semantics_rect_Type2 h_mk_related_semantics x_7289 =
     381  let { sem1 = sem3; sem2 = sem4 } = x_7289 in
    382382  h_mk_related_semantics sem3 sem4 __ __ __
    383383
     
    385385    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    386386    'a1 **)
    387 let rec related_semantics_rect_Type1 h_mk_related_semantics x_5746 =
    388   let { sem1 = sem3; sem2 = sem4 } = x_5746 in
     387let rec related_semantics_rect_Type1 h_mk_related_semantics x_7291 =
     388  let { sem1 = sem3; sem2 = sem4 } = x_7291 in
    389389  h_mk_related_semantics sem3 sem4 __ __ __
    390390
     
    392392    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    393393    'a1 **)
    394 let rec related_semantics_rect_Type0 h_mk_related_semantics x_5748 =
    395   let { sem1 = sem3; sem2 = sem4 } = x_5748 in
     394let rec related_semantics_rect_Type0 h_mk_related_semantics x_7293 =
     395  let { sem1 = sem3; sem2 = sem4 } = x_7293 in
    396396  h_mk_related_semantics sem3 sem4 __ __ __
    397397
     
    449449(** val order_sim_rect_Type4 :
    450450    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    451 let rec order_sim_rect_Type4 h_mk_order_sim x_5769 =
    452   let sem = x_5769 in h_mk_order_sim sem __ __
     451let rec order_sim_rect_Type4 h_mk_order_sim x_7314 =
     452  let sem = x_7314 in h_mk_order_sim sem __ __
    453453
    454454(** val order_sim_rect_Type5 :
    455455    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    456 let rec order_sim_rect_Type5 h_mk_order_sim x_5771 =
    457   let sem = x_5771 in h_mk_order_sim sem __ __
     456let rec order_sim_rect_Type5 h_mk_order_sim x_7316 =
     457  let sem = x_7316 in h_mk_order_sim sem __ __
    458458
    459459(** val order_sim_rect_Type3 :
    460460    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    461 let rec order_sim_rect_Type3 h_mk_order_sim x_5773 =
    462   let sem = x_5773 in h_mk_order_sim sem __ __
     461let rec order_sim_rect_Type3 h_mk_order_sim x_7318 =
     462  let sem = x_7318 in h_mk_order_sim sem __ __
    463463
    464464(** val order_sim_rect_Type2 :
    465465    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    466 let rec order_sim_rect_Type2 h_mk_order_sim x_5775 =
    467   let sem = x_5775 in h_mk_order_sim sem __ __
     466let rec order_sim_rect_Type2 h_mk_order_sim x_7320 =
     467  let sem = x_7320 in h_mk_order_sim sem __ __
    468468
    469469(** val order_sim_rect_Type1 :
    470470    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    471 let rec order_sim_rect_Type1 h_mk_order_sim x_5777 =
    472   let sem = x_5777 in h_mk_order_sim sem __ __
     471let rec order_sim_rect_Type1 h_mk_order_sim x_7322 =
     472  let sem = x_7322 in h_mk_order_sim sem __ __
    473473
    474474(** val order_sim_rect_Type0 :
    475475    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    476 let rec order_sim_rect_Type0 h_mk_order_sim x_5779 =
    477   let sem = x_5779 in h_mk_order_sim sem __ __
     476let rec order_sim_rect_Type0 h_mk_order_sim x_7324 =
     477  let sem = x_7324 in h_mk_order_sim sem __ __
    478478
    479479(** val sem : order_sim -> related_semantics **)
Note: See TracChangeset for help on using the changeset viewer.