Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/smallstep.ml

    r2601 r2649  
    1515open Identifiers
    1616
    17 open Floats
    18 
    1917open Integers
    2018
     
    3937open Pointers
    4038
     39open ErrorMessages
     40
    4141open Option
    4242
     
    4646
    4747open Positive
    48 
    49 open Char
    50 
    51 open String
    5248
    5349open PreIdentifiers
     
    161157    'a1 **)
    162158let rec program_behavior_rect_Type4 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    163 | Terminates (x_5847, x_5846) -> h_Terminates x_5847 x_5846
    164 | Diverges x_5848 -> h_Diverges x_5848
    165 | Reacts x_5849 -> h_Reacts x_5849
    166 | Goes_wrong x_5850 -> h_Goes_wrong x_5850
     159| Terminates (x_4040, x_4039) -> h_Terminates x_4040 x_4039
     160| Diverges x_4041 -> h_Diverges x_4041
     161| Reacts x_4042 -> h_Reacts x_4042
     162| Goes_wrong x_4043 -> h_Goes_wrong x_4043
    167163
    168164(** val program_behavior_rect_Type5 :
     
    171167    'a1 **)
    172168let rec program_behavior_rect_Type5 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    173 | Terminates (x_5857, x_5856) -> h_Terminates x_5857 x_5856
    174 | Diverges x_5858 -> h_Diverges x_5858
    175 | Reacts x_5859 -> h_Reacts x_5859
    176 | Goes_wrong x_5860 -> h_Goes_wrong x_5860
     169| Terminates (x_4050, x_4049) -> h_Terminates x_4050 x_4049
     170| Diverges x_4051 -> h_Diverges x_4051
     171| Reacts x_4052 -> h_Reacts x_4052
     172| Goes_wrong x_4053 -> h_Goes_wrong x_4053
    177173
    178174(** val program_behavior_rect_Type3 :
     
    181177    'a1 **)
    182178let rec program_behavior_rect_Type3 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    183 | Terminates (x_5867, x_5866) -> h_Terminates x_5867 x_5866
    184 | Diverges x_5868 -> h_Diverges x_5868
    185 | Reacts x_5869 -> h_Reacts x_5869
    186 | Goes_wrong x_5870 -> h_Goes_wrong x_5870
     179| Terminates (x_4060, x_4059) -> h_Terminates x_4060 x_4059
     180| Diverges x_4061 -> h_Diverges x_4061
     181| Reacts x_4062 -> h_Reacts x_4062
     182| Goes_wrong x_4063 -> h_Goes_wrong x_4063
    187183
    188184(** val program_behavior_rect_Type2 :
     
    191187    'a1 **)
    192188let rec program_behavior_rect_Type2 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    193 | Terminates (x_5877, x_5876) -> h_Terminates x_5877 x_5876
    194 | Diverges x_5878 -> h_Diverges x_5878
    195 | Reacts x_5879 -> h_Reacts x_5879
    196 | Goes_wrong x_5880 -> h_Goes_wrong x_5880
     189| Terminates (x_4070, x_4069) -> h_Terminates x_4070 x_4069
     190| Diverges x_4071 -> h_Diverges x_4071
     191| Reacts x_4072 -> h_Reacts x_4072
     192| Goes_wrong x_4073 -> h_Goes_wrong x_4073
    197193
    198194(** val program_behavior_rect_Type1 :
     
    201197    'a1 **)
    202198let rec program_behavior_rect_Type1 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    203 | Terminates (x_5887, x_5886) -> h_Terminates x_5887 x_5886
    204 | Diverges x_5888 -> h_Diverges x_5888
    205 | Reacts x_5889 -> h_Reacts x_5889
    206 | Goes_wrong x_5890 -> h_Goes_wrong x_5890
     199| Terminates (x_4080, x_4079) -> h_Terminates x_4080 x_4079
     200| Diverges x_4081 -> h_Diverges x_4081
     201| Reacts x_4082 -> h_Reacts x_4082
     202| Goes_wrong x_4083 -> h_Goes_wrong x_4083
    207203
    208204(** val program_behavior_rect_Type0 :
     
    211207    'a1 **)
    212208let rec program_behavior_rect_Type0 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    213 | Terminates (x_5897, x_5896) -> h_Terminates x_5897 x_5896
    214 | Diverges x_5898 -> h_Diverges x_5898
    215 | Reacts x_5899 -> h_Reacts x_5899
    216 | Goes_wrong x_5900 -> h_Goes_wrong x_5900
     209| Terminates (x_4090, x_4089) -> h_Terminates x_4090 x_4089
     210| Diverges x_4091 -> h_Diverges x_4091
     211| Reacts x_4092 -> h_Reacts x_4092
     212| Goes_wrong x_4093 -> h_Goes_wrong x_4093
    217213
    218214(** val program_behavior_inv_rect_Type4 :
     
    275271(** val semantics_rect_Type4 :
    276272    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    277 let rec semantics_rect_Type4 h_mk_semantics x_6227 =
    278   let { trans = trans0; ge = ge0 } = x_6227 in
     273let rec semantics_rect_Type4 h_mk_semantics x_4420 =
     274  let { trans = trans0; ge = ge0 } = x_4420 in
    279275  h_mk_semantics trans0 __ __ ge0
    280276
    281277(** val semantics_rect_Type5 :
    282278    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    283 let rec semantics_rect_Type5 h_mk_semantics x_6229 =
    284   let { trans = trans0; ge = ge0 } = x_6229 in
     279let rec semantics_rect_Type5 h_mk_semantics x_4422 =
     280  let { trans = trans0; ge = ge0 } = x_4422 in
    285281  h_mk_semantics trans0 __ __ ge0
    286282
    287283(** val semantics_rect_Type3 :
    288284    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    289 let rec semantics_rect_Type3 h_mk_semantics x_6231 =
    290   let { trans = trans0; ge = ge0 } = x_6231 in
     285let rec semantics_rect_Type3 h_mk_semantics x_4424 =
     286  let { trans = trans0; ge = ge0 } = x_4424 in
    291287  h_mk_semantics trans0 __ __ ge0
    292288
    293289(** val semantics_rect_Type2 :
    294290    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    295 let rec semantics_rect_Type2 h_mk_semantics x_6233 =
    296   let { trans = trans0; ge = ge0 } = x_6233 in
     291let rec semantics_rect_Type2 h_mk_semantics x_4426 =
     292  let { trans = trans0; ge = ge0 } = x_4426 in
    297293  h_mk_semantics trans0 __ __ ge0
    298294
    299295(** val semantics_rect_Type1 :
    300296    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    301 let rec semantics_rect_Type1 h_mk_semantics x_6235 =
    302   let { trans = trans0; ge = ge0 } = x_6235 in
     297let rec semantics_rect_Type1 h_mk_semantics x_4428 =
     298  let { trans = trans0; ge = ge0 } = x_4428 in
    303299  h_mk_semantics trans0 __ __ ge0
    304300
    305301(** val semantics_rect_Type0 :
    306302    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    307 let rec semantics_rect_Type0 h_mk_semantics x_6237 =
    308   let { trans = trans0; ge = ge0 } = x_6237 in
     303let rec semantics_rect_Type0 h_mk_semantics x_4430 =
     304  let { trans = trans0; ge = ge0 } = x_4430 in
    309305  h_mk_semantics trans0 __ __ ge0
    310306
     
    357353    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    358354    'a1 **)
    359 let rec related_semantics_rect_Type4 h_mk_related_semantics x_6256 =
    360   let { sem1 = sem3; sem2 = sem4 } = x_6256 in
     355let rec related_semantics_rect_Type4 h_mk_related_semantics x_4449 =
     356  let { sem1 = sem3; sem2 = sem4 } = x_4449 in
    361357  h_mk_related_semantics sem3 sem4 __ __ __
    362358
     
    364360    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    365361    'a1 **)
    366 let rec related_semantics_rect_Type5 h_mk_related_semantics x_6258 =
    367   let { sem1 = sem3; sem2 = sem4 } = x_6258 in
     362let rec related_semantics_rect_Type5 h_mk_related_semantics x_4451 =
     363  let { sem1 = sem3; sem2 = sem4 } = x_4451 in
    368364  h_mk_related_semantics sem3 sem4 __ __ __
    369365
     
    371367    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    372368    'a1 **)
    373 let rec related_semantics_rect_Type3 h_mk_related_semantics x_6260 =
    374   let { sem1 = sem3; sem2 = sem4 } = x_6260 in
     369let rec related_semantics_rect_Type3 h_mk_related_semantics x_4453 =
     370  let { sem1 = sem3; sem2 = sem4 } = x_4453 in
    375371  h_mk_related_semantics sem3 sem4 __ __ __
    376372
     
    378374    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    379375    'a1 **)
    380 let rec related_semantics_rect_Type2 h_mk_related_semantics x_6262 =
    381   let { sem1 = sem3; sem2 = sem4 } = x_6262 in
     376let rec related_semantics_rect_Type2 h_mk_related_semantics x_4455 =
     377  let { sem1 = sem3; sem2 = sem4 } = x_4455 in
    382378  h_mk_related_semantics sem3 sem4 __ __ __
    383379
     
    385381    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    386382    'a1 **)
    387 let rec related_semantics_rect_Type1 h_mk_related_semantics x_6264 =
    388   let { sem1 = sem3; sem2 = sem4 } = x_6264 in
     383let rec related_semantics_rect_Type1 h_mk_related_semantics x_4457 =
     384  let { sem1 = sem3; sem2 = sem4 } = x_4457 in
    389385  h_mk_related_semantics sem3 sem4 __ __ __
    390386
     
    392388    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    393389    'a1 **)
    394 let rec related_semantics_rect_Type0 h_mk_related_semantics x_6266 =
    395   let { sem1 = sem3; sem2 = sem4 } = x_6266 in
     390let rec related_semantics_rect_Type0 h_mk_related_semantics x_4459 =
     391  let { sem1 = sem3; sem2 = sem4 } = x_4459 in
    396392  h_mk_related_semantics sem3 sem4 __ __ __
    397393
     
    449445(** val order_sim_rect_Type4 :
    450446    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    451 let rec order_sim_rect_Type4 h_mk_order_sim x_6287 =
    452   let sem = x_6287 in h_mk_order_sim sem __ __
     447let rec order_sim_rect_Type4 h_mk_order_sim x_4480 =
     448  let sem = x_4480 in h_mk_order_sim sem __ __
    453449
    454450(** val order_sim_rect_Type5 :
    455451    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    456 let rec order_sim_rect_Type5 h_mk_order_sim x_6289 =
    457   let sem = x_6289 in h_mk_order_sim sem __ __
     452let rec order_sim_rect_Type5 h_mk_order_sim x_4482 =
     453  let sem = x_4482 in h_mk_order_sim sem __ __
    458454
    459455(** val order_sim_rect_Type3 :
    460456    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    461 let rec order_sim_rect_Type3 h_mk_order_sim x_6291 =
    462   let sem = x_6291 in h_mk_order_sim sem __ __
     457let rec order_sim_rect_Type3 h_mk_order_sim x_4484 =
     458  let sem = x_4484 in h_mk_order_sim sem __ __
    463459
    464460(** val order_sim_rect_Type2 :
    465461    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    466 let rec order_sim_rect_Type2 h_mk_order_sim x_6293 =
    467   let sem = x_6293 in h_mk_order_sim sem __ __
     462let rec order_sim_rect_Type2 h_mk_order_sim x_4486 =
     463  let sem = x_4486 in h_mk_order_sim sem __ __
    468464
    469465(** val order_sim_rect_Type1 :
    470466    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    471 let rec order_sim_rect_Type1 h_mk_order_sim x_6295 =
    472   let sem = x_6295 in h_mk_order_sim sem __ __
     467let rec order_sim_rect_Type1 h_mk_order_sim x_4488 =
     468  let sem = x_4488 in h_mk_order_sim sem __ __
    473469
    474470(** val order_sim_rect_Type0 :
    475471    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    476 let rec order_sim_rect_Type0 h_mk_order_sim x_6297 =
    477   let sem = x_6297 in h_mk_order_sim sem __ __
     472let rec order_sim_rect_Type0 h_mk_order_sim x_4490 =
     473  let sem = x_4490 in h_mk_order_sim sem __ __
    478474
    479475(** val sem : order_sim -> related_semantics **)
Note: See TracChangeset for help on using the changeset viewer.