Changeset 2649 for extracted/smallstep.ml
 Timestamp:
 Feb 7, 2013, 10:43:49 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/smallstep.ml
r2601 r2649 15 15 open Identifiers 16 16 17 open Floats18 19 17 open Integers 20 18 … … 39 37 open Pointers 40 38 39 open ErrorMessages 40 41 41 open Option 42 42 … … 46 46 47 47 open Positive 48 49 open Char50 51 open String52 48 53 49 open PreIdentifiers … … 161 157 'a1 **) 162 158 let 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_5846164  Diverges x_ 5848 > h_Diverges x_5848165  Reacts x_ 5849 > h_Reacts x_5849166  Goes_wrong x_ 5850 > h_Goes_wrong x_5850159  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 167 163 168 164 (** val program_behavior_rect_Type5 : … … 171 167 'a1 **) 172 168 let 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_5856174  Diverges x_ 5858 > h_Diverges x_5858175  Reacts x_ 5859 > h_Reacts x_5859176  Goes_wrong x_ 5860 > h_Goes_wrong x_5860169  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 177 173 178 174 (** val program_behavior_rect_Type3 : … … 181 177 'a1 **) 182 178 let 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_5866184  Diverges x_ 5868 > h_Diverges x_5868185  Reacts x_ 5869 > h_Reacts x_5869186  Goes_wrong x_ 5870 > h_Goes_wrong x_5870179  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 187 183 188 184 (** val program_behavior_rect_Type2 : … … 191 187 'a1 **) 192 188 let 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_5876194  Diverges x_ 5878 > h_Diverges x_5878195  Reacts x_ 5879 > h_Reacts x_5879196  Goes_wrong x_ 5880 > h_Goes_wrong x_5880189  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 197 193 198 194 (** val program_behavior_rect_Type1 : … … 201 197 'a1 **) 202 198 let 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_5886204  Diverges x_ 5888 > h_Diverges x_5888205  Reacts x_ 5889 > h_Reacts x_5889206  Goes_wrong x_ 5890 > h_Goes_wrong x_5890199  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 207 203 208 204 (** val program_behavior_rect_Type0 : … … 211 207 'a1 **) 212 208 let 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_5896214  Diverges x_ 5898 > h_Diverges x_5898215  Reacts x_ 5899 > h_Reacts x_5899216  Goes_wrong x_ 5900 > h_Goes_wrong x_5900209  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 217 213 218 214 (** val program_behavior_inv_rect_Type4 : … … 275 271 (** val semantics_rect_Type4 : 276 272 (transrel > __ > __ > __ > 'a1) > semantics > 'a1 **) 277 let rec semantics_rect_Type4 h_mk_semantics x_ 6227=278 let { trans = trans0; ge = ge0 } = x_ 6227in273 let rec semantics_rect_Type4 h_mk_semantics x_4420 = 274 let { trans = trans0; ge = ge0 } = x_4420 in 279 275 h_mk_semantics trans0 __ __ ge0 280 276 281 277 (** val semantics_rect_Type5 : 282 278 (transrel > __ > __ > __ > 'a1) > semantics > 'a1 **) 283 let rec semantics_rect_Type5 h_mk_semantics x_ 6229=284 let { trans = trans0; ge = ge0 } = x_ 6229in279 let rec semantics_rect_Type5 h_mk_semantics x_4422 = 280 let { trans = trans0; ge = ge0 } = x_4422 in 285 281 h_mk_semantics trans0 __ __ ge0 286 282 287 283 (** val semantics_rect_Type3 : 288 284 (transrel > __ > __ > __ > 'a1) > semantics > 'a1 **) 289 let rec semantics_rect_Type3 h_mk_semantics x_ 6231=290 let { trans = trans0; ge = ge0 } = x_ 6231in285 let rec semantics_rect_Type3 h_mk_semantics x_4424 = 286 let { trans = trans0; ge = ge0 } = x_4424 in 291 287 h_mk_semantics trans0 __ __ ge0 292 288 293 289 (** val semantics_rect_Type2 : 294 290 (transrel > __ > __ > __ > 'a1) > semantics > 'a1 **) 295 let rec semantics_rect_Type2 h_mk_semantics x_ 6233=296 let { trans = trans0; ge = ge0 } = x_ 6233in291 let rec semantics_rect_Type2 h_mk_semantics x_4426 = 292 let { trans = trans0; ge = ge0 } = x_4426 in 297 293 h_mk_semantics trans0 __ __ ge0 298 294 299 295 (** val semantics_rect_Type1 : 300 296 (transrel > __ > __ > __ > 'a1) > semantics > 'a1 **) 301 let rec semantics_rect_Type1 h_mk_semantics x_ 6235=302 let { trans = trans0; ge = ge0 } = x_ 6235in297 let rec semantics_rect_Type1 h_mk_semantics x_4428 = 298 let { trans = trans0; ge = ge0 } = x_4428 in 303 299 h_mk_semantics trans0 __ __ ge0 304 300 305 301 (** val semantics_rect_Type0 : 306 302 (transrel > __ > __ > __ > 'a1) > semantics > 'a1 **) 307 let rec semantics_rect_Type0 h_mk_semantics x_ 6237=308 let { trans = trans0; ge = ge0 } = x_ 6237in303 let rec semantics_rect_Type0 h_mk_semantics x_4430 = 304 let { trans = trans0; ge = ge0 } = x_4430 in 309 305 h_mk_semantics trans0 __ __ ge0 310 306 … … 357 353 (semantics > semantics > __ > __ > __ > 'a1) > related_semantics > 358 354 'a1 **) 359 let rec related_semantics_rect_Type4 h_mk_related_semantics x_ 6256=360 let { sem1 = sem3; sem2 = sem4 } = x_ 6256in355 let rec related_semantics_rect_Type4 h_mk_related_semantics x_4449 = 356 let { sem1 = sem3; sem2 = sem4 } = x_4449 in 361 357 h_mk_related_semantics sem3 sem4 __ __ __ 362 358 … … 364 360 (semantics > semantics > __ > __ > __ > 'a1) > related_semantics > 365 361 'a1 **) 366 let rec related_semantics_rect_Type5 h_mk_related_semantics x_ 6258=367 let { sem1 = sem3; sem2 = sem4 } = x_ 6258in362 let rec related_semantics_rect_Type5 h_mk_related_semantics x_4451 = 363 let { sem1 = sem3; sem2 = sem4 } = x_4451 in 368 364 h_mk_related_semantics sem3 sem4 __ __ __ 369 365 … … 371 367 (semantics > semantics > __ > __ > __ > 'a1) > related_semantics > 372 368 'a1 **) 373 let rec related_semantics_rect_Type3 h_mk_related_semantics x_ 6260=374 let { sem1 = sem3; sem2 = sem4 } = x_ 6260in369 let rec related_semantics_rect_Type3 h_mk_related_semantics x_4453 = 370 let { sem1 = sem3; sem2 = sem4 } = x_4453 in 375 371 h_mk_related_semantics sem3 sem4 __ __ __ 376 372 … … 378 374 (semantics > semantics > __ > __ > __ > 'a1) > related_semantics > 379 375 'a1 **) 380 let rec related_semantics_rect_Type2 h_mk_related_semantics x_ 6262=381 let { sem1 = sem3; sem2 = sem4 } = x_ 6262in376 let rec related_semantics_rect_Type2 h_mk_related_semantics x_4455 = 377 let { sem1 = sem3; sem2 = sem4 } = x_4455 in 382 378 h_mk_related_semantics sem3 sem4 __ __ __ 383 379 … … 385 381 (semantics > semantics > __ > __ > __ > 'a1) > related_semantics > 386 382 'a1 **) 387 let rec related_semantics_rect_Type1 h_mk_related_semantics x_ 6264=388 let { sem1 = sem3; sem2 = sem4 } = x_ 6264in383 let rec related_semantics_rect_Type1 h_mk_related_semantics x_4457 = 384 let { sem1 = sem3; sem2 = sem4 } = x_4457 in 389 385 h_mk_related_semantics sem3 sem4 __ __ __ 390 386 … … 392 388 (semantics > semantics > __ > __ > __ > 'a1) > related_semantics > 393 389 'a1 **) 394 let rec related_semantics_rect_Type0 h_mk_related_semantics x_ 6266=395 let { sem1 = sem3; sem2 = sem4 } = x_ 6266in390 let rec related_semantics_rect_Type0 h_mk_related_semantics x_4459 = 391 let { sem1 = sem3; sem2 = sem4 } = x_4459 in 396 392 h_mk_related_semantics sem3 sem4 __ __ __ 397 393 … … 449 445 (** val order_sim_rect_Type4 : 450 446 (related_semantics > __ > __ > 'a1) > order_sim > 'a1 **) 451 let rec order_sim_rect_Type4 h_mk_order_sim x_ 6287=452 let sem = x_ 6287in h_mk_order_sim sem __ __447 let rec order_sim_rect_Type4 h_mk_order_sim x_4480 = 448 let sem = x_4480 in h_mk_order_sim sem __ __ 453 449 454 450 (** val order_sim_rect_Type5 : 455 451 (related_semantics > __ > __ > 'a1) > order_sim > 'a1 **) 456 let rec order_sim_rect_Type5 h_mk_order_sim x_ 6289=457 let sem = x_ 6289in h_mk_order_sim sem __ __452 let rec order_sim_rect_Type5 h_mk_order_sim x_4482 = 453 let sem = x_4482 in h_mk_order_sim sem __ __ 458 454 459 455 (** val order_sim_rect_Type3 : 460 456 (related_semantics > __ > __ > 'a1) > order_sim > 'a1 **) 461 let rec order_sim_rect_Type3 h_mk_order_sim x_ 6291=462 let sem = x_ 6291in h_mk_order_sim sem __ __457 let rec order_sim_rect_Type3 h_mk_order_sim x_4484 = 458 let sem = x_4484 in h_mk_order_sim sem __ __ 463 459 464 460 (** val order_sim_rect_Type2 : 465 461 (related_semantics > __ > __ > 'a1) > order_sim > 'a1 **) 466 let rec order_sim_rect_Type2 h_mk_order_sim x_ 6293=467 let sem = x_ 6293in h_mk_order_sim sem __ __462 let rec order_sim_rect_Type2 h_mk_order_sim x_4486 = 463 let sem = x_4486 in h_mk_order_sim sem __ __ 468 464 469 465 (** val order_sim_rect_Type1 : 470 466 (related_semantics > __ > __ > 'a1) > order_sim > 'a1 **) 471 let rec order_sim_rect_Type1 h_mk_order_sim x_ 6295=472 let sem = x_ 6295in h_mk_order_sim sem __ __467 let rec order_sim_rect_Type1 h_mk_order_sim x_4488 = 468 let sem = x_4488 in h_mk_order_sim sem __ __ 473 469 474 470 (** val order_sim_rect_Type0 : 475 471 (related_semantics > __ > __ > 'a1) > order_sim > 'a1 **) 476 let rec order_sim_rect_Type0 h_mk_order_sim x_ 6297=477 let sem = x_ 6297in h_mk_order_sim sem __ __472 let rec order_sim_rect_Type0 h_mk_order_sim x_4490 = 473 let sem = x_4490 in h_mk_order_sim sem __ __ 478 474 479 475 (** val sem : order_sim > related_semantics **)
Note: See TracChangeset
for help on using the changeset viewer.