Changeset 3001 for extracted/smallstep.ml
 Timestamp:
 Mar 28, 2013, 1:02:48 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/smallstep.ml
r2997 r3001 157 157 'a1 **) 158 158 let rec program_behavior_rect_Type4 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function 159  Terminates (x_1 3237, x_13236) > h_Terminates x_13237 x_13236160  Diverges x_1 3238 > h_Diverges x_13238161  Reacts x_1 3239 > h_Reacts x_13239162  Goes_wrong x_1 3240 > h_Goes_wrong x_13240159  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 163 163 164 164 (** val program_behavior_rect_Type5 : … … 167 167 'a1 **) 168 168 let rec program_behavior_rect_Type5 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function 169  Terminates (x_1 3247, x_13246) > h_Terminates x_13247 x_13246170  Diverges x_1 3248 > h_Diverges x_13248171  Reacts x_1 3249 > h_Reacts x_13249172  Goes_wrong x_1 3250 > h_Goes_wrong x_13250169  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 173 173 174 174 (** val program_behavior_rect_Type3 : … … 177 177 'a1 **) 178 178 let rec program_behavior_rect_Type3 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function 179  Terminates (x_1 3257, x_13256) > h_Terminates x_13257 x_13256180  Diverges x_1 3258 > h_Diverges x_13258181  Reacts x_1 3259 > h_Reacts x_13259182  Goes_wrong x_1 3260 > h_Goes_wrong x_13260179  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 183 183 184 184 (** val program_behavior_rect_Type2 : … … 187 187 'a1 **) 188 188 let rec program_behavior_rect_Type2 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function 189  Terminates (x_1 3267, x_13266) > h_Terminates x_13267 x_13266190  Diverges x_1 3268 > h_Diverges x_13268191  Reacts x_1 3269 > h_Reacts x_13269192  Goes_wrong x_1 3270 > h_Goes_wrong x_13270189  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 193 193 194 194 (** val program_behavior_rect_Type1 : … … 197 197 'a1 **) 198 198 let rec program_behavior_rect_Type1 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function 199  Terminates (x_1 3277, x_13276) > h_Terminates x_13277 x_13276200  Diverges x_1 3278 > h_Diverges x_13278201  Reacts x_1 3279 > h_Reacts x_13279202  Goes_wrong x_1 3280 > h_Goes_wrong x_13280199  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 203 203 204 204 (** val program_behavior_rect_Type0 : … … 207 207 'a1 **) 208 208 let rec program_behavior_rect_Type0 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function 209  Terminates (x_1 3287, x_13286) > h_Terminates x_13287 x_13286210  Diverges x_1 3288 > h_Diverges x_13288211  Reacts x_1 3289 > h_Reacts x_13289212  Goes_wrong x_1 3290 > h_Goes_wrong x_13290209  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 213 213 214 214 (** val program_behavior_inv_rect_Type4 : … … 271 271 (** val semantics_rect_Type4 : 272 272 (transrel > __ > __ > __ > 'a1) > semantics > 'a1 **) 273 let rec semantics_rect_Type4 h_mk_semantics x_1 3617=274 let { trans = trans0; ge = ge0 } = x_1 3617in273 let rec semantics_rect_Type4 h_mk_semantics x_10544 = 274 let { trans = trans0; ge = ge0 } = x_10544 in 275 275 h_mk_semantics trans0 __ __ ge0 276 276 277 277 (** val semantics_rect_Type5 : 278 278 (transrel > __ > __ > __ > 'a1) > semantics > 'a1 **) 279 let rec semantics_rect_Type5 h_mk_semantics x_1 3619=280 let { trans = trans0; ge = ge0 } = x_1 3619in279 let rec semantics_rect_Type5 h_mk_semantics x_10546 = 280 let { trans = trans0; ge = ge0 } = x_10546 in 281 281 h_mk_semantics trans0 __ __ ge0 282 282 283 283 (** val semantics_rect_Type3 : 284 284 (transrel > __ > __ > __ > 'a1) > semantics > 'a1 **) 285 let rec semantics_rect_Type3 h_mk_semantics x_1 3621=286 let { trans = trans0; ge = ge0 } = x_1 3621in285 let rec semantics_rect_Type3 h_mk_semantics x_10548 = 286 let { trans = trans0; ge = ge0 } = x_10548 in 287 287 h_mk_semantics trans0 __ __ ge0 288 288 289 289 (** val semantics_rect_Type2 : 290 290 (transrel > __ > __ > __ > 'a1) > semantics > 'a1 **) 291 let rec semantics_rect_Type2 h_mk_semantics x_1 3623=292 let { trans = trans0; ge = ge0 } = x_1 3623in291 let rec semantics_rect_Type2 h_mk_semantics x_10550 = 292 let { trans = trans0; ge = ge0 } = x_10550 in 293 293 h_mk_semantics trans0 __ __ ge0 294 294 295 295 (** val semantics_rect_Type1 : 296 296 (transrel > __ > __ > __ > 'a1) > semantics > 'a1 **) 297 let rec semantics_rect_Type1 h_mk_semantics x_1 3625=298 let { trans = trans0; ge = ge0 } = x_1 3625in297 let rec semantics_rect_Type1 h_mk_semantics x_10552 = 298 let { trans = trans0; ge = ge0 } = x_10552 in 299 299 h_mk_semantics trans0 __ __ ge0 300 300 301 301 (** val semantics_rect_Type0 : 302 302 (transrel > __ > __ > __ > 'a1) > semantics > 'a1 **) 303 let rec semantics_rect_Type0 h_mk_semantics x_1 3627=304 let { trans = trans0; ge = ge0 } = x_1 3627in303 let rec semantics_rect_Type0 h_mk_semantics x_10554 = 304 let { trans = trans0; ge = ge0 } = x_10554 in 305 305 h_mk_semantics trans0 __ __ ge0 306 306 … … 349 349 (semantics > semantics > __ > __ > __ > 'a1) > related_semantics > 350 350 'a1 **) 351 let rec related_semantics_rect_Type4 h_mk_related_semantics x_1 3646=352 let { sem1 = sem3; sem2 = sem4 } = x_1 3646in351 let rec related_semantics_rect_Type4 h_mk_related_semantics x_10573 = 352 let { sem1 = sem3; sem2 = sem4 } = x_10573 in 353 353 h_mk_related_semantics sem3 sem4 __ __ __ 354 354 … … 356 356 (semantics > semantics > __ > __ > __ > 'a1) > related_semantics > 357 357 'a1 **) 358 let rec related_semantics_rect_Type5 h_mk_related_semantics x_1 3648=359 let { sem1 = sem3; sem2 = sem4 } = x_1 3648in358 let rec related_semantics_rect_Type5 h_mk_related_semantics x_10575 = 359 let { sem1 = sem3; sem2 = sem4 } = x_10575 in 360 360 h_mk_related_semantics sem3 sem4 __ __ __ 361 361 … … 363 363 (semantics > semantics > __ > __ > __ > 'a1) > related_semantics > 364 364 'a1 **) 365 let rec related_semantics_rect_Type3 h_mk_related_semantics x_1 3650=366 let { sem1 = sem3; sem2 = sem4 } = x_1 3650in365 let rec related_semantics_rect_Type3 h_mk_related_semantics x_10577 = 366 let { sem1 = sem3; sem2 = sem4 } = x_10577 in 367 367 h_mk_related_semantics sem3 sem4 __ __ __ 368 368 … … 370 370 (semantics > semantics > __ > __ > __ > 'a1) > related_semantics > 371 371 'a1 **) 372 let rec related_semantics_rect_Type2 h_mk_related_semantics x_1 3652=373 let { sem1 = sem3; sem2 = sem4 } = x_1 3652in372 let rec related_semantics_rect_Type2 h_mk_related_semantics x_10579 = 373 let { sem1 = sem3; sem2 = sem4 } = x_10579 in 374 374 h_mk_related_semantics sem3 sem4 __ __ __ 375 375 … … 377 377 (semantics > semantics > __ > __ > __ > 'a1) > related_semantics > 378 378 'a1 **) 379 let rec related_semantics_rect_Type1 h_mk_related_semantics x_1 3654=380 let { sem1 = sem3; sem2 = sem4 } = x_1 3654in379 let rec related_semantics_rect_Type1 h_mk_related_semantics x_10581 = 380 let { sem1 = sem3; sem2 = sem4 } = x_10581 in 381 381 h_mk_related_semantics sem3 sem4 __ __ __ 382 382 … … 384 384 (semantics > semantics > __ > __ > __ > 'a1) > related_semantics > 385 385 'a1 **) 386 let rec related_semantics_rect_Type0 h_mk_related_semantics x_1 3656=387 let { sem1 = sem3; sem2 = sem4 } = x_1 3656in386 let rec related_semantics_rect_Type0 h_mk_related_semantics x_10583 = 387 let { sem1 = sem3; sem2 = sem4 } = x_10583 in 388 388 h_mk_related_semantics sem3 sem4 __ __ __ 389 389 … … 439 439 (** val order_sim_rect_Type4 : 440 440 (related_semantics > __ > __ > 'a1) > order_sim > 'a1 **) 441 let rec order_sim_rect_Type4 h_mk_order_sim x_1 3677=442 let sem = x_1 3677in h_mk_order_sim sem __ __441 let rec order_sim_rect_Type4 h_mk_order_sim x_10604 = 442 let sem = x_10604 in h_mk_order_sim sem __ __ 443 443 444 444 (** val order_sim_rect_Type5 : 445 445 (related_semantics > __ > __ > 'a1) > order_sim > 'a1 **) 446 let rec order_sim_rect_Type5 h_mk_order_sim x_1 3679=447 let sem = x_1 3679in h_mk_order_sim sem __ __446 let rec order_sim_rect_Type5 h_mk_order_sim x_10606 = 447 let sem = x_10606 in h_mk_order_sim sem __ __ 448 448 449 449 (** val order_sim_rect_Type3 : 450 450 (related_semantics > __ > __ > 'a1) > order_sim > 'a1 **) 451 let rec order_sim_rect_Type3 h_mk_order_sim x_1 3681=452 let sem = x_1 3681in h_mk_order_sim sem __ __451 let rec order_sim_rect_Type3 h_mk_order_sim x_10608 = 452 let sem = x_10608 in h_mk_order_sim sem __ __ 453 453 454 454 (** val order_sim_rect_Type2 : 455 455 (related_semantics > __ > __ > 'a1) > order_sim > 'a1 **) 456 let rec order_sim_rect_Type2 h_mk_order_sim x_1 3683=457 let sem = x_1 3683in h_mk_order_sim sem __ __456 let rec order_sim_rect_Type2 h_mk_order_sim x_10610 = 457 let sem = x_10610 in h_mk_order_sim sem __ __ 458 458 459 459 (** val order_sim_rect_Type1 : 460 460 (related_semantics > __ > __ > 'a1) > order_sim > 'a1 **) 461 let rec order_sim_rect_Type1 h_mk_order_sim x_1 3685=462 let sem = x_1 3685in h_mk_order_sim sem __ __461 let rec order_sim_rect_Type1 h_mk_order_sim x_10612 = 462 let sem = x_10612 in h_mk_order_sim sem __ __ 463 463 464 464 (** val order_sim_rect_Type0 : 465 465 (related_semantics > __ > __ > 'a1) > order_sim > 'a1 **) 466 let rec order_sim_rect_Type0 h_mk_order_sim x_1 3687=467 let sem = x_1 3687in h_mk_order_sim sem __ __466 let rec order_sim_rect_Type0 h_mk_order_sim x_10614 = 467 let sem = x_10614 in h_mk_order_sim sem __ __ 468 468 469 469 (** val sem : order_sim > related_semantics **)
Note: See TracChangeset
for help on using the changeset viewer.