Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/smallstep.ml

    r2827 r2951  
    157157    'a1 **)
    158158let rec program_behavior_rect_Type4 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    159 | Terminates (x_6913, x_6912) -> h_Terminates x_6913 x_6912
    160 | Diverges x_6914 -> h_Diverges x_6914
    161 | Reacts x_6915 -> h_Reacts x_6915
    162 | Goes_wrong x_6916 -> h_Goes_wrong x_6916
     159| Terminates (x_6952, x_6951) -> h_Terminates x_6952 x_6951
     160| Diverges x_6953 -> h_Diverges x_6953
     161| Reacts x_6954 -> h_Reacts x_6954
     162| Goes_wrong x_6955 -> h_Goes_wrong x_6955
    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_6923, x_6922) -> h_Terminates x_6923 x_6922
    170 | Diverges x_6924 -> h_Diverges x_6924
    171 | Reacts x_6925 -> h_Reacts x_6925
    172 | Goes_wrong x_6926 -> h_Goes_wrong x_6926
     169| Terminates (x_6962, x_6961) -> h_Terminates x_6962 x_6961
     170| Diverges x_6963 -> h_Diverges x_6963
     171| Reacts x_6964 -> h_Reacts x_6964
     172| Goes_wrong x_6965 -> h_Goes_wrong x_6965
    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_6933, x_6932) -> h_Terminates x_6933 x_6932
    180 | Diverges x_6934 -> h_Diverges x_6934
    181 | Reacts x_6935 -> h_Reacts x_6935
    182 | Goes_wrong x_6936 -> h_Goes_wrong x_6936
     179| Terminates (x_6972, x_6971) -> h_Terminates x_6972 x_6971
     180| Diverges x_6973 -> h_Diverges x_6973
     181| Reacts x_6974 -> h_Reacts x_6974
     182| Goes_wrong x_6975 -> h_Goes_wrong x_6975
    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_6943, x_6942) -> h_Terminates x_6943 x_6942
    190 | Diverges x_6944 -> h_Diverges x_6944
    191 | Reacts x_6945 -> h_Reacts x_6945
    192 | Goes_wrong x_6946 -> h_Goes_wrong x_6946
     189| Terminates (x_6982, x_6981) -> h_Terminates x_6982 x_6981
     190| Diverges x_6983 -> h_Diverges x_6983
     191| Reacts x_6984 -> h_Reacts x_6984
     192| Goes_wrong x_6985 -> h_Goes_wrong x_6985
    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_6953, x_6952) -> h_Terminates x_6953 x_6952
    200 | Diverges x_6954 -> h_Diverges x_6954
    201 | Reacts x_6955 -> h_Reacts x_6955
    202 | Goes_wrong x_6956 -> h_Goes_wrong x_6956
     199| Terminates (x_6992, x_6991) -> h_Terminates x_6992 x_6991
     200| Diverges x_6993 -> h_Diverges x_6993
     201| Reacts x_6994 -> h_Reacts x_6994
     202| Goes_wrong x_6995 -> h_Goes_wrong x_6995
    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_6963, x_6962) -> h_Terminates x_6963 x_6962
    210 | Diverges x_6964 -> h_Diverges x_6964
    211 | Reacts x_6965 -> h_Reacts x_6965
    212 | Goes_wrong x_6966 -> h_Goes_wrong x_6966
     209| Terminates (x_7002, x_7001) -> h_Terminates x_7002 x_7001
     210| Diverges x_7003 -> h_Diverges x_7003
     211| Reacts x_7004 -> h_Reacts x_7004
     212| Goes_wrong x_7005 -> h_Goes_wrong x_7005
    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_7293 =
    274   let { trans = trans0; ge = ge0 } = x_7293 in
     273let rec semantics_rect_Type4 h_mk_semantics x_7332 =
     274  let { trans = trans0; ge = ge0 } = x_7332 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_7295 =
    280   let { trans = trans0; ge = ge0 } = x_7295 in
     279let rec semantics_rect_Type5 h_mk_semantics x_7334 =
     280  let { trans = trans0; ge = ge0 } = x_7334 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_7297 =
    286   let { trans = trans0; ge = ge0 } = x_7297 in
     285let rec semantics_rect_Type3 h_mk_semantics x_7336 =
     286  let { trans = trans0; ge = ge0 } = x_7336 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_7299 =
    292   let { trans = trans0; ge = ge0 } = x_7299 in
     291let rec semantics_rect_Type2 h_mk_semantics x_7338 =
     292  let { trans = trans0; ge = ge0 } = x_7338 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_7301 =
    298   let { trans = trans0; ge = ge0 } = x_7301 in
     297let rec semantics_rect_Type1 h_mk_semantics x_7340 =
     298  let { trans = trans0; ge = ge0 } = x_7340 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_7303 =
    304   let { trans = trans0; ge = ge0 } = x_7303 in
     303let rec semantics_rect_Type0 h_mk_semantics x_7342 =
     304  let { trans = trans0; ge = ge0 } = x_7342 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_7322 =
    352   let { sem1 = sem3; sem2 = sem4 } = x_7322 in
     351let rec related_semantics_rect_Type4 h_mk_related_semantics x_7361 =
     352  let { sem1 = sem3; sem2 = sem4 } = x_7361 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_7324 =
    359   let { sem1 = sem3; sem2 = sem4 } = x_7324 in
     358let rec related_semantics_rect_Type5 h_mk_related_semantics x_7363 =
     359  let { sem1 = sem3; sem2 = sem4 } = x_7363 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_7326 =
    366   let { sem1 = sem3; sem2 = sem4 } = x_7326 in
     365let rec related_semantics_rect_Type3 h_mk_related_semantics x_7365 =
     366  let { sem1 = sem3; sem2 = sem4 } = x_7365 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_7328 =
    373   let { sem1 = sem3; sem2 = sem4 } = x_7328 in
     372let rec related_semantics_rect_Type2 h_mk_related_semantics x_7367 =
     373  let { sem1 = sem3; sem2 = sem4 } = x_7367 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_7330 =
    380   let { sem1 = sem3; sem2 = sem4 } = x_7330 in
     379let rec related_semantics_rect_Type1 h_mk_related_semantics x_7369 =
     380  let { sem1 = sem3; sem2 = sem4 } = x_7369 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_7332 =
    387   let { sem1 = sem3; sem2 = sem4 } = x_7332 in
     386let rec related_semantics_rect_Type0 h_mk_related_semantics x_7371 =
     387  let { sem1 = sem3; sem2 = sem4 } = x_7371 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_7353 =
    442   let sem = x_7353 in h_mk_order_sim sem __ __
     441let rec order_sim_rect_Type4 h_mk_order_sim x_7392 =
     442  let sem = x_7392 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_7355 =
    447   let sem = x_7355 in h_mk_order_sim sem __ __
     446let rec order_sim_rect_Type5 h_mk_order_sim x_7394 =
     447  let sem = x_7394 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_7357 =
    452   let sem = x_7357 in h_mk_order_sim sem __ __
     451let rec order_sim_rect_Type3 h_mk_order_sim x_7396 =
     452  let sem = x_7396 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_7359 =
    457   let sem = x_7359 in h_mk_order_sim sem __ __
     456let rec order_sim_rect_Type2 h_mk_order_sim x_7398 =
     457  let sem = x_7398 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_7361 =
    462   let sem = x_7361 in h_mk_order_sim sem __ __
     461let rec order_sim_rect_Type1 h_mk_order_sim x_7400 =
     462  let sem = x_7400 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_7363 =
    467   let sem = x_7363 in h_mk_order_sim sem __ __
     466let rec order_sim_rect_Type0 h_mk_order_sim x_7402 =
     467  let sem = x_7402 in h_mk_order_sim sem __ __
    468468
    469469(** val sem : order_sim -> related_semantics **)
Note: See TracChangeset for help on using the changeset viewer.