Ignore:
Timestamp:
Mar 7, 2013, 12:55:34 PM (7 years ago)
Author:
sacerdot
Message:

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/smallstep.ml

    r2775 r2797  
    157157    'a1 **)
    158158let rec program_behavior_rect_Type4 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    159 | Terminates (x_6783, x_6782) -> h_Terminates x_6783 x_6782
    160 | Diverges x_6784 -> h_Diverges x_6784
    161 | Reacts x_6785 -> h_Reacts x_6785
    162 | Goes_wrong x_6786 -> h_Goes_wrong x_6786
     159| Terminates (x_6796, x_6795) -> h_Terminates x_6796 x_6795
     160| Diverges x_6797 -> h_Diverges x_6797
     161| Reacts x_6798 -> h_Reacts x_6798
     162| Goes_wrong x_6799 -> h_Goes_wrong x_6799
    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_6793, x_6792) -> h_Terminates x_6793 x_6792
    170 | Diverges x_6794 -> h_Diverges x_6794
    171 | Reacts x_6795 -> h_Reacts x_6795
    172 | Goes_wrong x_6796 -> h_Goes_wrong x_6796
     169| Terminates (x_6806, x_6805) -> h_Terminates x_6806 x_6805
     170| Diverges x_6807 -> h_Diverges x_6807
     171| Reacts x_6808 -> h_Reacts x_6808
     172| Goes_wrong x_6809 -> h_Goes_wrong x_6809
    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_6803, x_6802) -> h_Terminates x_6803 x_6802
    180 | Diverges x_6804 -> h_Diverges x_6804
    181 | Reacts x_6805 -> h_Reacts x_6805
    182 | Goes_wrong x_6806 -> h_Goes_wrong x_6806
     179| Terminates (x_6816, x_6815) -> h_Terminates x_6816 x_6815
     180| Diverges x_6817 -> h_Diverges x_6817
     181| Reacts x_6818 -> h_Reacts x_6818
     182| Goes_wrong x_6819 -> h_Goes_wrong x_6819
    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_6813, x_6812) -> h_Terminates x_6813 x_6812
    190 | Diverges x_6814 -> h_Diverges x_6814
    191 | Reacts x_6815 -> h_Reacts x_6815
    192 | Goes_wrong x_6816 -> h_Goes_wrong x_6816
     189| Terminates (x_6826, x_6825) -> h_Terminates x_6826 x_6825
     190| Diverges x_6827 -> h_Diverges x_6827
     191| Reacts x_6828 -> h_Reacts x_6828
     192| Goes_wrong x_6829 -> h_Goes_wrong x_6829
    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_6823, x_6822) -> h_Terminates x_6823 x_6822
    200 | Diverges x_6824 -> h_Diverges x_6824
    201 | Reacts x_6825 -> h_Reacts x_6825
    202 | Goes_wrong x_6826 -> h_Goes_wrong x_6826
     199| Terminates (x_6836, x_6835) -> h_Terminates x_6836 x_6835
     200| Diverges x_6837 -> h_Diverges x_6837
     201| Reacts x_6838 -> h_Reacts x_6838
     202| Goes_wrong x_6839 -> h_Goes_wrong x_6839
    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_6833, x_6832) -> h_Terminates x_6833 x_6832
    210 | Diverges x_6834 -> h_Diverges x_6834
    211 | Reacts x_6835 -> h_Reacts x_6835
    212 | Goes_wrong x_6836 -> h_Goes_wrong x_6836
     209| Terminates (x_6846, x_6845) -> h_Terminates x_6846 x_6845
     210| Diverges x_6847 -> h_Diverges x_6847
     211| Reacts x_6848 -> h_Reacts x_6848
     212| Goes_wrong x_6849 -> h_Goes_wrong x_6849
    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_7163 =
    274   let { trans = trans0; ge = ge0 } = x_7163 in
     273let rec semantics_rect_Type4 h_mk_semantics x_7176 =
     274  let { trans = trans0; ge = ge0 } = x_7176 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_7165 =
    280   let { trans = trans0; ge = ge0 } = x_7165 in
     279let rec semantics_rect_Type5 h_mk_semantics x_7178 =
     280  let { trans = trans0; ge = ge0 } = x_7178 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_7167 =
    286   let { trans = trans0; ge = ge0 } = x_7167 in
     285let rec semantics_rect_Type3 h_mk_semantics x_7180 =
     286  let { trans = trans0; ge = ge0 } = x_7180 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_7169 =
    292   let { trans = trans0; ge = ge0 } = x_7169 in
     291let rec semantics_rect_Type2 h_mk_semantics x_7182 =
     292  let { trans = trans0; ge = ge0 } = x_7182 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_7171 =
    298   let { trans = trans0; ge = ge0 } = x_7171 in
     297let rec semantics_rect_Type1 h_mk_semantics x_7184 =
     298  let { trans = trans0; ge = ge0 } = x_7184 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_7173 =
    304   let { trans = trans0; ge = ge0 } = x_7173 in
     303let rec semantics_rect_Type0 h_mk_semantics x_7186 =
     304  let { trans = trans0; ge = ge0 } = x_7186 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_7192 =
    352   let { sem1 = sem3; sem2 = sem4 } = x_7192 in
     351let rec related_semantics_rect_Type4 h_mk_related_semantics x_7205 =
     352  let { sem1 = sem3; sem2 = sem4 } = x_7205 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_7194 =
    359   let { sem1 = sem3; sem2 = sem4 } = x_7194 in
     358let rec related_semantics_rect_Type5 h_mk_related_semantics x_7207 =
     359  let { sem1 = sem3; sem2 = sem4 } = x_7207 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_7196 =
    366   let { sem1 = sem3; sem2 = sem4 } = x_7196 in
     365let rec related_semantics_rect_Type3 h_mk_related_semantics x_7209 =
     366  let { sem1 = sem3; sem2 = sem4 } = x_7209 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_7198 =
    373   let { sem1 = sem3; sem2 = sem4 } = x_7198 in
     372let rec related_semantics_rect_Type2 h_mk_related_semantics x_7211 =
     373  let { sem1 = sem3; sem2 = sem4 } = x_7211 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_7200 =
    380   let { sem1 = sem3; sem2 = sem4 } = x_7200 in
     379let rec related_semantics_rect_Type1 h_mk_related_semantics x_7213 =
     380  let { sem1 = sem3; sem2 = sem4 } = x_7213 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_7202 =
    387   let { sem1 = sem3; sem2 = sem4 } = x_7202 in
     386let rec related_semantics_rect_Type0 h_mk_related_semantics x_7215 =
     387  let { sem1 = sem3; sem2 = sem4 } = x_7215 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_7223 =
    442   let sem = x_7223 in h_mk_order_sim sem __ __
     441let rec order_sim_rect_Type4 h_mk_order_sim x_7236 =
     442  let sem = x_7236 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_7225 =
    447   let sem = x_7225 in h_mk_order_sim sem __ __
     446let rec order_sim_rect_Type5 h_mk_order_sim x_7238 =
     447  let sem = x_7238 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_7227 =
    452   let sem = x_7227 in h_mk_order_sim sem __ __
     451let rec order_sim_rect_Type3 h_mk_order_sim x_7240 =
     452  let sem = x_7240 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_7229 =
    457   let sem = x_7229 in h_mk_order_sim sem __ __
     456let rec order_sim_rect_Type2 h_mk_order_sim x_7242 =
     457  let sem = x_7242 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_7231 =
    462   let sem = x_7231 in h_mk_order_sim sem __ __
     461let rec order_sim_rect_Type1 h_mk_order_sim x_7244 =
     462  let sem = x_7244 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_7233 =
    467   let sem = x_7233 in h_mk_order_sim sem __ __
     466let rec order_sim_rect_Type0 h_mk_order_sim x_7246 =
     467  let sem = x_7246 in h_mk_order_sim sem __ __
    468468
    469469(** val sem : order_sim -> related_semantics **)
Note: See TracChangeset for help on using the changeset viewer.