Changeset 2730 for extracted/smallstepExec.ml
 Timestamp:
 Feb 25, 2013, 9:54:49 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/smallstepExec.ml
r2717 r2730 99 99 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 100 100 'a2) trans_system > 'a3 **) 101 let rec trans_system_rect_Type4 h_mk_trans_system x_ 5847=102 let { is_final = is_final0; step = step0 } = x_ 5847in101 let rec trans_system_rect_Type4 h_mk_trans_system x_8529 = 102 let { is_final = is_final0; step = step0 } = x_8529 in 103 103 h_mk_trans_system __ __ is_final0 step0 104 104 … … 107 107 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 108 108 'a2) trans_system > 'a3 **) 109 let rec trans_system_rect_Type5 h_mk_trans_system x_ 5849=110 let { is_final = is_final0; step = step0 } = x_ 5849in109 let rec trans_system_rect_Type5 h_mk_trans_system x_8531 = 110 let { is_final = is_final0; step = step0 } = x_8531 in 111 111 h_mk_trans_system __ __ is_final0 step0 112 112 … … 115 115 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 116 116 'a2) trans_system > 'a3 **) 117 let rec trans_system_rect_Type3 h_mk_trans_system x_ 5851=118 let { is_final = is_final0; step = step0 } = x_ 5851in117 let rec trans_system_rect_Type3 h_mk_trans_system x_8533 = 118 let { is_final = is_final0; step = step0 } = x_8533 in 119 119 h_mk_trans_system __ __ is_final0 step0 120 120 … … 123 123 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 124 124 'a2) trans_system > 'a3 **) 125 let rec trans_system_rect_Type2 h_mk_trans_system x_ 5853=126 let { is_final = is_final0; step = step0 } = x_ 5853in125 let rec trans_system_rect_Type2 h_mk_trans_system x_8535 = 126 let { is_final = is_final0; step = step0 } = x_8535 in 127 127 h_mk_trans_system __ __ is_final0 step0 128 128 … … 131 131 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 132 132 'a2) trans_system > 'a3 **) 133 let rec trans_system_rect_Type1 h_mk_trans_system x_ 5855=134 let { is_final = is_final0; step = step0 } = x_ 5855in133 let rec trans_system_rect_Type1 h_mk_trans_system x_8537 = 134 let { is_final = is_final0; step = step0 } = x_8537 in 135 135 h_mk_trans_system __ __ is_final0 step0 136 136 … … 139 139 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 140 140 'a2) trans_system > 'a3 **) 141 let rec trans_system_rect_Type0 h_mk_trans_system x_ 5857=142 let { is_final = is_final0; step = step0 } = x_ 5857in141 let rec trans_system_rect_Type0 h_mk_trans_system x_8539 = 142 let { is_final = is_final0; step = step0 } = x_8539 in 143 143 h_mk_trans_system __ __ is_final0 step0 144 144 … … 227 227 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 228 228 await_value_stuff > 'a1 **) 229 let rec await_value_stuff_rect_Type4 h_mk_await_value_stuff x_ 6019=230 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 6019229 let rec await_value_stuff_rect_Type4 h_mk_await_value_stuff x_8701 = 230 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8701 231 231 in 232 232 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 235 235 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 236 236 await_value_stuff > 'a1 **) 237 let rec await_value_stuff_rect_Type5 h_mk_await_value_stuff x_ 6021=238 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 6021237 let rec await_value_stuff_rect_Type5 h_mk_await_value_stuff x_8703 = 238 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8703 239 239 in 240 240 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 243 243 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 244 244 await_value_stuff > 'a1 **) 245 let rec await_value_stuff_rect_Type3 h_mk_await_value_stuff x_ 6023=246 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 6023245 let rec await_value_stuff_rect_Type3 h_mk_await_value_stuff x_8705 = 246 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8705 247 247 in 248 248 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 251 251 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 252 252 await_value_stuff > 'a1 **) 253 let rec await_value_stuff_rect_Type2 h_mk_await_value_stuff x_ 6025=254 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 6025253 let rec await_value_stuff_rect_Type2 h_mk_await_value_stuff x_8707 = 254 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8707 255 255 in 256 256 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 259 259 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 260 260 await_value_stuff > 'a1 **) 261 let rec await_value_stuff_rect_Type1 h_mk_await_value_stuff x_ 6027=262 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 6027261 let rec await_value_stuff_rect_Type1 h_mk_await_value_stuff x_8709 = 262 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8709 263 263 in 264 264 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 267 267 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 268 268 await_value_stuff > 'a1 **) 269 let rec await_value_stuff_rect_Type0 h_mk_await_value_stuff x_ 6029=270 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 6029269 let rec await_value_stuff_rect_Type0 h_mk_await_value_stuff x_8711 = 270 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8711 271 271 in 272 272 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 456 456 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 457 457 'a3) > ('a1, 'a2) fullexec > 'a3 **) 458 let rec fullexec_rect_Type4 h_mk_fullexec x_ 6047=458 let rec fullexec_rect_Type4 h_mk_fullexec x_8729 = 459 459 let { es1 = es2; make_global = make_global0; make_initial_state = 460 make_initial_state0 } = x_ 6047460 make_initial_state0 } = x_8729 461 461 in 462 462 h_mk_fullexec __ es2 make_global0 make_initial_state0 … … 465 465 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 466 466 'a3) > ('a1, 'a2) fullexec > 'a3 **) 467 let rec fullexec_rect_Type5 h_mk_fullexec x_ 6049=467 let rec fullexec_rect_Type5 h_mk_fullexec x_8731 = 468 468 let { es1 = es2; make_global = make_global0; make_initial_state = 469 make_initial_state0 } = x_ 6049469 make_initial_state0 } = x_8731 470 470 in 471 471 h_mk_fullexec __ es2 make_global0 make_initial_state0 … … 474 474 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 475 475 'a3) > ('a1, 'a2) fullexec > 'a3 **) 476 let rec fullexec_rect_Type3 h_mk_fullexec x_ 6051=476 let rec fullexec_rect_Type3 h_mk_fullexec x_8733 = 477 477 let { es1 = es2; make_global = make_global0; make_initial_state = 478 make_initial_state0 } = x_ 6051478 make_initial_state0 } = x_8733 479 479 in 480 480 h_mk_fullexec __ es2 make_global0 make_initial_state0 … … 483 483 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 484 484 'a3) > ('a1, 'a2) fullexec > 'a3 **) 485 let rec fullexec_rect_Type2 h_mk_fullexec x_ 6053=485 let rec fullexec_rect_Type2 h_mk_fullexec x_8735 = 486 486 let { es1 = es2; make_global = make_global0; make_initial_state = 487 make_initial_state0 } = x_ 6053487 make_initial_state0 } = x_8735 488 488 in 489 489 h_mk_fullexec __ es2 make_global0 make_initial_state0 … … 492 492 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 493 493 'a3) > ('a1, 'a2) fullexec > 'a3 **) 494 let rec fullexec_rect_Type1 h_mk_fullexec x_ 6055=494 let rec fullexec_rect_Type1 h_mk_fullexec x_8737 = 495 495 let { es1 = es2; make_global = make_global0; make_initial_state = 496 make_initial_state0 } = x_ 6055496 make_initial_state0 } = x_8737 497 497 in 498 498 h_mk_fullexec __ es2 make_global0 make_initial_state0 … … 501 501 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 502 502 'a3) > ('a1, 'a2) fullexec > 'a3 **) 503 let rec fullexec_rect_Type0 h_mk_fullexec x_ 6057=503 let rec fullexec_rect_Type0 h_mk_fullexec x_8739 = 504 504 let { es1 = es2; make_global = make_global0; make_initial_state = 505 make_initial_state0 } = x_ 6057505 make_initial_state0 } = x_8739 506 506 in 507 507 h_mk_fullexec __ es2 make_global0 make_initial_state0
Note: See TracChangeset
for help on using the changeset viewer.