Ignore:
Timestamp:
Mar 28, 2013, 1:02:48 PM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/smallstep.ml

    r2997 r3001  
    157157    'a1 **)
    158158let rec program_behavior_rect_Type4 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    159 | Terminates (x_13237, x_13236) -> h_Terminates x_13237 x_13236
    160 | Diverges x_13238 -> h_Diverges x_13238
    161 | Reacts x_13239 -> h_Reacts x_13239
    162 | Goes_wrong x_13240 -> h_Goes_wrong x_13240
     159| Terminates (x_10164, x_10163) -> h_Terminates x_10164 x_10163
     160| Diverges x_10165 -> h_Diverges x_10165
     161| Reacts x_10166 -> h_Reacts x_10166
     162| Goes_wrong x_10167 -> h_Goes_wrong x_10167
    163163
    164164(** val program_behavior_rect_Type5 :
     
    167167    'a1 **)
    168168let rec program_behavior_rect_Type5 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    169 | Terminates (x_13247, x_13246) -> h_Terminates x_13247 x_13246
    170 | Diverges x_13248 -> h_Diverges x_13248
    171 | Reacts x_13249 -> h_Reacts x_13249
    172 | Goes_wrong x_13250 -> h_Goes_wrong x_13250
     169| Terminates (x_10174, x_10173) -> h_Terminates x_10174 x_10173
     170| Diverges x_10175 -> h_Diverges x_10175
     171| Reacts x_10176 -> h_Reacts x_10176
     172| Goes_wrong x_10177 -> h_Goes_wrong x_10177
    173173
    174174(** val program_behavior_rect_Type3 :
     
    177177    'a1 **)
    178178let rec program_behavior_rect_Type3 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    179 | Terminates (x_13257, x_13256) -> h_Terminates x_13257 x_13256
    180 | Diverges x_13258 -> h_Diverges x_13258
    181 | Reacts x_13259 -> h_Reacts x_13259
    182 | Goes_wrong x_13260 -> h_Goes_wrong x_13260
     179| Terminates (x_10184, x_10183) -> h_Terminates x_10184 x_10183
     180| Diverges x_10185 -> h_Diverges x_10185
     181| Reacts x_10186 -> h_Reacts x_10186
     182| Goes_wrong x_10187 -> h_Goes_wrong x_10187
    183183
    184184(** val program_behavior_rect_Type2 :
     
    187187    'a1 **)
    188188let rec program_behavior_rect_Type2 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    189 | Terminates (x_13267, x_13266) -> h_Terminates x_13267 x_13266
    190 | Diverges x_13268 -> h_Diverges x_13268
    191 | Reacts x_13269 -> h_Reacts x_13269
    192 | Goes_wrong x_13270 -> h_Goes_wrong x_13270
     189| Terminates (x_10194, x_10193) -> h_Terminates x_10194 x_10193
     190| Diverges x_10195 -> h_Diverges x_10195
     191| Reacts x_10196 -> h_Reacts x_10196
     192| Goes_wrong x_10197 -> h_Goes_wrong x_10197
    193193
    194194(** val program_behavior_rect_Type1 :
     
    197197    'a1 **)
    198198let rec program_behavior_rect_Type1 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    199 | Terminates (x_13277, x_13276) -> h_Terminates x_13277 x_13276
    200 | Diverges x_13278 -> h_Diverges x_13278
    201 | Reacts x_13279 -> h_Reacts x_13279
    202 | Goes_wrong x_13280 -> h_Goes_wrong x_13280
     199| Terminates (x_10204, x_10203) -> h_Terminates x_10204 x_10203
     200| Diverges x_10205 -> h_Diverges x_10205
     201| Reacts x_10206 -> h_Reacts x_10206
     202| Goes_wrong x_10207 -> h_Goes_wrong x_10207
    203203
    204204(** val program_behavior_rect_Type0 :
     
    207207    'a1 **)
    208208let rec program_behavior_rect_Type0 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    209 | Terminates (x_13287, x_13286) -> h_Terminates x_13287 x_13286
    210 | Diverges x_13288 -> h_Diverges x_13288
    211 | Reacts x_13289 -> h_Reacts x_13289
    212 | Goes_wrong x_13290 -> h_Goes_wrong x_13290
     209| Terminates (x_10214, x_10213) -> h_Terminates x_10214 x_10213
     210| Diverges x_10215 -> h_Diverges x_10215
     211| Reacts x_10216 -> h_Reacts x_10216
     212| Goes_wrong x_10217 -> h_Goes_wrong x_10217
    213213
    214214(** val program_behavior_inv_rect_Type4 :
     
    271271(** val semantics_rect_Type4 :
    272272    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    273 let rec semantics_rect_Type4 h_mk_semantics x_13617 =
    274   let { trans = trans0; ge = ge0 } = x_13617 in
     273let rec semantics_rect_Type4 h_mk_semantics x_10544 =
     274  let { trans = trans0; ge = ge0 } = x_10544 in
    275275  h_mk_semantics trans0 __ __ ge0
    276276
    277277(** val semantics_rect_Type5 :
    278278    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    279 let rec semantics_rect_Type5 h_mk_semantics x_13619 =
    280   let { trans = trans0; ge = ge0 } = x_13619 in
     279let rec semantics_rect_Type5 h_mk_semantics x_10546 =
     280  let { trans = trans0; ge = ge0 } = x_10546 in
    281281  h_mk_semantics trans0 __ __ ge0
    282282
    283283(** val semantics_rect_Type3 :
    284284    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    285 let rec semantics_rect_Type3 h_mk_semantics x_13621 =
    286   let { trans = trans0; ge = ge0 } = x_13621 in
     285let rec semantics_rect_Type3 h_mk_semantics x_10548 =
     286  let { trans = trans0; ge = ge0 } = x_10548 in
    287287  h_mk_semantics trans0 __ __ ge0
    288288
    289289(** val semantics_rect_Type2 :
    290290    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    291 let rec semantics_rect_Type2 h_mk_semantics x_13623 =
    292   let { trans = trans0; ge = ge0 } = x_13623 in
     291let rec semantics_rect_Type2 h_mk_semantics x_10550 =
     292  let { trans = trans0; ge = ge0 } = x_10550 in
    293293  h_mk_semantics trans0 __ __ ge0
    294294
    295295(** val semantics_rect_Type1 :
    296296    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    297 let rec semantics_rect_Type1 h_mk_semantics x_13625 =
    298   let { trans = trans0; ge = ge0 } = x_13625 in
     297let rec semantics_rect_Type1 h_mk_semantics x_10552 =
     298  let { trans = trans0; ge = ge0 } = x_10552 in
    299299  h_mk_semantics trans0 __ __ ge0
    300300
    301301(** val semantics_rect_Type0 :
    302302    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    303 let rec semantics_rect_Type0 h_mk_semantics x_13627 =
    304   let { trans = trans0; ge = ge0 } = x_13627 in
     303let rec semantics_rect_Type0 h_mk_semantics x_10554 =
     304  let { trans = trans0; ge = ge0 } = x_10554 in
    305305  h_mk_semantics trans0 __ __ ge0
    306306
     
    349349    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    350350    'a1 **)
    351 let rec related_semantics_rect_Type4 h_mk_related_semantics x_13646 =
    352   let { sem1 = sem3; sem2 = sem4 } = x_13646 in
     351let rec related_semantics_rect_Type4 h_mk_related_semantics x_10573 =
     352  let { sem1 = sem3; sem2 = sem4 } = x_10573 in
    353353  h_mk_related_semantics sem3 sem4 __ __ __
    354354
     
    356356    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    357357    'a1 **)
    358 let rec related_semantics_rect_Type5 h_mk_related_semantics x_13648 =
    359   let { sem1 = sem3; sem2 = sem4 } = x_13648 in
     358let rec related_semantics_rect_Type5 h_mk_related_semantics x_10575 =
     359  let { sem1 = sem3; sem2 = sem4 } = x_10575 in
    360360  h_mk_related_semantics sem3 sem4 __ __ __
    361361
     
    363363    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    364364    'a1 **)
    365 let rec related_semantics_rect_Type3 h_mk_related_semantics x_13650 =
    366   let { sem1 = sem3; sem2 = sem4 } = x_13650 in
     365let rec related_semantics_rect_Type3 h_mk_related_semantics x_10577 =
     366  let { sem1 = sem3; sem2 = sem4 } = x_10577 in
    367367  h_mk_related_semantics sem3 sem4 __ __ __
    368368
     
    370370    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    371371    'a1 **)
    372 let rec related_semantics_rect_Type2 h_mk_related_semantics x_13652 =
    373   let { sem1 = sem3; sem2 = sem4 } = x_13652 in
     372let rec related_semantics_rect_Type2 h_mk_related_semantics x_10579 =
     373  let { sem1 = sem3; sem2 = sem4 } = x_10579 in
    374374  h_mk_related_semantics sem3 sem4 __ __ __
    375375
     
    377377    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    378378    'a1 **)
    379 let rec related_semantics_rect_Type1 h_mk_related_semantics x_13654 =
    380   let { sem1 = sem3; sem2 = sem4 } = x_13654 in
     379let rec related_semantics_rect_Type1 h_mk_related_semantics x_10581 =
     380  let { sem1 = sem3; sem2 = sem4 } = x_10581 in
    381381  h_mk_related_semantics sem3 sem4 __ __ __
    382382
     
    384384    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    385385    'a1 **)
    386 let rec related_semantics_rect_Type0 h_mk_related_semantics x_13656 =
    387   let { sem1 = sem3; sem2 = sem4 } = x_13656 in
     386let rec related_semantics_rect_Type0 h_mk_related_semantics x_10583 =
     387  let { sem1 = sem3; sem2 = sem4 } = x_10583 in
    388388  h_mk_related_semantics sem3 sem4 __ __ __
    389389
     
    439439(** val order_sim_rect_Type4 :
    440440    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    441 let rec order_sim_rect_Type4 h_mk_order_sim x_13677 =
    442   let sem = x_13677 in h_mk_order_sim sem __ __
     441let rec order_sim_rect_Type4 h_mk_order_sim x_10604 =
     442  let sem = x_10604 in h_mk_order_sim sem __ __
    443443
    444444(** val order_sim_rect_Type5 :
    445445    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    446 let rec order_sim_rect_Type5 h_mk_order_sim x_13679 =
    447   let sem = x_13679 in h_mk_order_sim sem __ __
     446let rec order_sim_rect_Type5 h_mk_order_sim x_10606 =
     447  let sem = x_10606 in h_mk_order_sim sem __ __
    448448
    449449(** val order_sim_rect_Type3 :
    450450    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    451 let rec order_sim_rect_Type3 h_mk_order_sim x_13681 =
    452   let sem = x_13681 in h_mk_order_sim sem __ __
     451let rec order_sim_rect_Type3 h_mk_order_sim x_10608 =
     452  let sem = x_10608 in h_mk_order_sim sem __ __
    453453
    454454(** val order_sim_rect_Type2 :
    455455    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    456 let rec order_sim_rect_Type2 h_mk_order_sim x_13683 =
    457   let sem = x_13683 in h_mk_order_sim sem __ __
     456let rec order_sim_rect_Type2 h_mk_order_sim x_10610 =
     457  let sem = x_10610 in h_mk_order_sim sem __ __
    458458
    459459(** val order_sim_rect_Type1 :
    460460    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    461 let rec order_sim_rect_Type1 h_mk_order_sim x_13685 =
    462   let sem = x_13685 in h_mk_order_sim sem __ __
     461let rec order_sim_rect_Type1 h_mk_order_sim x_10612 =
     462  let sem = x_10612 in h_mk_order_sim sem __ __
    463463
    464464(** val order_sim_rect_Type0 :
    465465    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    466 let rec order_sim_rect_Type0 h_mk_order_sim x_13687 =
    467   let sem = x_13687 in h_mk_order_sim sem __ __
     466let rec order_sim_rect_Type0 h_mk_order_sim x_10614 =
     467  let sem = x_10614 in h_mk_order_sim sem __ __
    468468
    469469(** val sem : order_sim -> related_semantics **)
Note: See TracChangeset for help on using the changeset viewer.