Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/smallstep.ml

    r2743 r2773  
    11open Preamble
    2 
    3 open BitVectorTrie
    42
    53open CostLabel
     
    117115
    118116type state = __
    119 
    120 type step = __
    121117
    122118(** val transrel_inv_rect_Type4 :
     
    161157    'a1 **)
    162158let rec program_behavior_rect_Type4 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    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
     159| Terminates (x_1952, x_1951) -> h_Terminates x_1952 x_1951
     160| Diverges x_1953 -> h_Diverges x_1953
     161| Reacts x_1954 -> h_Reacts x_1954
     162| Goes_wrong x_1955 -> h_Goes_wrong x_1955
    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_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
     169| Terminates (x_1962, x_1961) -> h_Terminates x_1962 x_1961
     170| Diverges x_1963 -> h_Diverges x_1963
     171| Reacts x_1964 -> h_Reacts x_1964
     172| Goes_wrong x_1965 -> h_Goes_wrong x_1965
    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_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
     179| Terminates (x_1972, x_1971) -> h_Terminates x_1972 x_1971
     180| Diverges x_1973 -> h_Diverges x_1973
     181| Reacts x_1974 -> h_Reacts x_1974
     182| Goes_wrong x_1975 -> h_Goes_wrong x_1975
    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_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
     189| Terminates (x_1982, x_1981) -> h_Terminates x_1982 x_1981
     190| Diverges x_1983 -> h_Diverges x_1983
     191| Reacts x_1984 -> h_Reacts x_1984
     192| Goes_wrong x_1985 -> h_Goes_wrong x_1985
    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_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
     199| Terminates (x_1992, x_1991) -> h_Terminates x_1992 x_1991
     200| Diverges x_1993 -> h_Diverges x_1993
     201| Reacts x_1994 -> h_Reacts x_1994
     202| Goes_wrong x_1995 -> h_Goes_wrong x_1995
    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_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
     209| Terminates (x_2002, x_2001) -> h_Terminates x_2002 x_2001
     210| Diverges x_2003 -> h_Diverges x_2003
     211| Reacts x_2004 -> h_Reacts x_2004
     212| Goes_wrong x_2005 -> h_Goes_wrong x_2005
    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_7254 =
    278   let { trans = trans0; ge = ge0 } = x_7254 in
     273let rec semantics_rect_Type4 h_mk_semantics x_2332 =
     274  let { trans = trans0; ge = ge0 } = x_2332 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_7256 =
    284   let { trans = trans0; ge = ge0 } = x_7256 in
     279let rec semantics_rect_Type5 h_mk_semantics x_2334 =
     280  let { trans = trans0; ge = ge0 } = x_2334 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_7258 =
    290   let { trans = trans0; ge = ge0 } = x_7258 in
     285let rec semantics_rect_Type3 h_mk_semantics x_2336 =
     286  let { trans = trans0; ge = ge0 } = x_2336 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_7260 =
    296   let { trans = trans0; ge = ge0 } = x_7260 in
     291let rec semantics_rect_Type2 h_mk_semantics x_2338 =
     292  let { trans = trans0; ge = ge0 } = x_2338 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_7262 =
    302   let { trans = trans0; ge = ge0 } = x_7262 in
     297let rec semantics_rect_Type1 h_mk_semantics x_2340 =
     298  let { trans = trans0; ge = ge0 } = x_2340 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_7264 =
    308   let { trans = trans0; ge = ge0 } = x_7264 in
     303let rec semantics_rect_Type0 h_mk_semantics x_2342 =
     304  let { trans = trans0; ge = ge0 } = x_2342 in
    309305  h_mk_semantics trans0 __ __ ge0
    310306
     
    312308let rec trans xxx =
    313309  xxx.trans
    314 
    315 type initial = __
    316 
    317 type final = __
    318310
    319311(** val ge : semantics -> __ **)
     
    357349    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    358350    'a1 **)
    359 let rec related_semantics_rect_Type4 h_mk_related_semantics x_7283 =
    360   let { sem1 = sem3; sem2 = sem4 } = x_7283 in
     351let rec related_semantics_rect_Type4 h_mk_related_semantics x_2361 =
     352  let { sem1 = sem3; sem2 = sem4 } = x_2361 in
    361353  h_mk_related_semantics sem3 sem4 __ __ __
    362354
     
    364356    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    365357    'a1 **)
    366 let rec related_semantics_rect_Type5 h_mk_related_semantics x_7285 =
    367   let { sem1 = sem3; sem2 = sem4 } = x_7285 in
     358let rec related_semantics_rect_Type5 h_mk_related_semantics x_2363 =
     359  let { sem1 = sem3; sem2 = sem4 } = x_2363 in
    368360  h_mk_related_semantics sem3 sem4 __ __ __
    369361
     
    371363    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    372364    'a1 **)
    373 let rec related_semantics_rect_Type3 h_mk_related_semantics x_7287 =
    374   let { sem1 = sem3; sem2 = sem4 } = x_7287 in
     365let rec related_semantics_rect_Type3 h_mk_related_semantics x_2365 =
     366  let { sem1 = sem3; sem2 = sem4 } = x_2365 in
    375367  h_mk_related_semantics sem3 sem4 __ __ __
    376368
     
    378370    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    379371    'a1 **)
    380 let rec related_semantics_rect_Type2 h_mk_related_semantics x_7289 =
    381   let { sem1 = sem3; sem2 = sem4 } = x_7289 in
     372let rec related_semantics_rect_Type2 h_mk_related_semantics x_2367 =
     373  let { sem1 = sem3; sem2 = sem4 } = x_2367 in
    382374  h_mk_related_semantics sem3 sem4 __ __ __
    383375
     
    385377    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    386378    'a1 **)
    387 let rec related_semantics_rect_Type1 h_mk_related_semantics x_7291 =
    388   let { sem1 = sem3; sem2 = sem4 } = x_7291 in
     379let rec related_semantics_rect_Type1 h_mk_related_semantics x_2369 =
     380  let { sem1 = sem3; sem2 = sem4 } = x_2369 in
    389381  h_mk_related_semantics sem3 sem4 __ __ __
    390382
     
    392384    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    393385    'a1 **)
    394 let rec related_semantics_rect_Type0 h_mk_related_semantics x_7293 =
    395   let { sem1 = sem3; sem2 = sem4 } = x_7293 in
     386let rec related_semantics_rect_Type0 h_mk_related_semantics x_2371 =
     387  let { sem1 = sem3; sem2 = sem4 } = x_2371 in
    396388  h_mk_related_semantics sem3 sem4 __ __ __
    397389
     
    403395let rec sem2 xxx =
    404396  xxx.sem2
    405 
    406 type match_states = __
    407397
    408398(** val related_semantics_inv_rect_Type4 :
     
    449439(** val order_sim_rect_Type4 :
    450440    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    451 let rec order_sim_rect_Type4 h_mk_order_sim x_7314 =
    452   let sem = x_7314 in h_mk_order_sim sem __ __
     441let rec order_sim_rect_Type4 h_mk_order_sim x_2392 =
     442  let sem = x_2392 in h_mk_order_sim sem __ __
    453443
    454444(** val order_sim_rect_Type5 :
    455445    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    456 let rec order_sim_rect_Type5 h_mk_order_sim x_7316 =
    457   let sem = x_7316 in h_mk_order_sim sem __ __
     446let rec order_sim_rect_Type5 h_mk_order_sim x_2394 =
     447  let sem = x_2394 in h_mk_order_sim sem __ __
    458448
    459449(** val order_sim_rect_Type3 :
    460450    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    461 let rec order_sim_rect_Type3 h_mk_order_sim x_7318 =
    462   let sem = x_7318 in h_mk_order_sim sem __ __
     451let rec order_sim_rect_Type3 h_mk_order_sim x_2396 =
     452  let sem = x_2396 in h_mk_order_sim sem __ __
    463453
    464454(** val order_sim_rect_Type2 :
    465455    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    466 let rec order_sim_rect_Type2 h_mk_order_sim x_7320 =
    467   let sem = x_7320 in h_mk_order_sim sem __ __
     456let rec order_sim_rect_Type2 h_mk_order_sim x_2398 =
     457  let sem = x_2398 in h_mk_order_sim sem __ __
    468458
    469459(** val order_sim_rect_Type1 :
    470460    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    471 let rec order_sim_rect_Type1 h_mk_order_sim x_7322 =
    472   let sem = x_7322 in h_mk_order_sim sem __ __
     461let rec order_sim_rect_Type1 h_mk_order_sim x_2400 =
     462  let sem = x_2400 in h_mk_order_sim sem __ __
    473463
    474464(** val order_sim_rect_Type0 :
    475465    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    476 let rec order_sim_rect_Type0 h_mk_order_sim x_7324 =
    477   let sem = x_7324 in h_mk_order_sim sem __ __
     466let rec order_sim_rect_Type0 h_mk_order_sim x_2402 =
     467  let sem = x_2402 in h_mk_order_sim sem __ __
    478468
    479469(** val sem : order_sim -> related_semantics **)
    480470let rec sem xxx =
    481471  let yyy = xxx in yyy
    482 
    483 type order = __
    484472
    485473(** val order_sim_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.