Changeset 2827 for extracted/smallstepExec.ml
 Timestamp:
 Mar 8, 2013, 9:07:28 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/smallstepExec.ml
r2797 r2827 97 97 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 98 98 'a2) trans_system > 'a3 **) 99 let rec trans_system_rect_Type4 h_mk_trans_system x_5 795=100 let { is_final = is_final0; step = step0 } = x_5 795in99 let rec trans_system_rect_Type4 h_mk_trans_system x_5912 = 100 let { is_final = is_final0; step = step0 } = x_5912 in 101 101 h_mk_trans_system __ __ is_final0 step0 102 102 … … 105 105 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 106 106 'a2) trans_system > 'a3 **) 107 let rec trans_system_rect_Type5 h_mk_trans_system x_5 797=108 let { is_final = is_final0; step = step0 } = x_5 797in107 let rec trans_system_rect_Type5 h_mk_trans_system x_5914 = 108 let { is_final = is_final0; step = step0 } = x_5914 in 109 109 h_mk_trans_system __ __ is_final0 step0 110 110 … … 113 113 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 114 114 'a2) trans_system > 'a3 **) 115 let rec trans_system_rect_Type3 h_mk_trans_system x_5 799=116 let { is_final = is_final0; step = step0 } = x_5 799in115 let rec trans_system_rect_Type3 h_mk_trans_system x_5916 = 116 let { is_final = is_final0; step = step0 } = x_5916 in 117 117 h_mk_trans_system __ __ is_final0 step0 118 118 … … 121 121 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 122 122 'a2) trans_system > 'a3 **) 123 let rec trans_system_rect_Type2 h_mk_trans_system x_5 801=124 let { is_final = is_final0; step = step0 } = x_5 801in123 let rec trans_system_rect_Type2 h_mk_trans_system x_5918 = 124 let { is_final = is_final0; step = step0 } = x_5918 in 125 125 h_mk_trans_system __ __ is_final0 step0 126 126 … … 129 129 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 130 130 'a2) trans_system > 'a3 **) 131 let rec trans_system_rect_Type1 h_mk_trans_system x_5 803=132 let { is_final = is_final0; step = step0 } = x_5 803in131 let rec trans_system_rect_Type1 h_mk_trans_system x_5920 = 132 let { is_final = is_final0; step = step0 } = x_5920 in 133 133 h_mk_trans_system __ __ is_final0 step0 134 134 … … 137 137 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 138 138 'a2) trans_system > 'a3 **) 139 let rec trans_system_rect_Type0 h_mk_trans_system x_5 805=140 let { is_final = is_final0; step = step0 } = x_5 805in139 let rec trans_system_rect_Type0 h_mk_trans_system x_5922 = 140 let { is_final = is_final0; step = step0 } = x_5922 in 141 141 h_mk_trans_system __ __ is_final0 step0 142 142 … … 225 225 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 226 226 await_value_stuff > 'a1 **) 227 let rec await_value_stuff_rect_Type4 h_mk_await_value_stuff x_ 5967=228 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 5967227 let rec await_value_stuff_rect_Type4 h_mk_await_value_stuff x_6084 = 228 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6084 229 229 in 230 230 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 233 233 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 234 234 await_value_stuff > 'a1 **) 235 let rec await_value_stuff_rect_Type5 h_mk_await_value_stuff x_ 5969=236 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 5969235 let rec await_value_stuff_rect_Type5 h_mk_await_value_stuff x_6086 = 236 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6086 237 237 in 238 238 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 241 241 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 242 242 await_value_stuff > 'a1 **) 243 let rec await_value_stuff_rect_Type3 h_mk_await_value_stuff x_ 5971=244 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 5971243 let rec await_value_stuff_rect_Type3 h_mk_await_value_stuff x_6088 = 244 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6088 245 245 in 246 246 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 249 249 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 250 250 await_value_stuff > 'a1 **) 251 let rec await_value_stuff_rect_Type2 h_mk_await_value_stuff x_ 5973=252 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 5973251 let rec await_value_stuff_rect_Type2 h_mk_await_value_stuff x_6090 = 252 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6090 253 253 in 254 254 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 257 257 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 258 258 await_value_stuff > 'a1 **) 259 let rec await_value_stuff_rect_Type1 h_mk_await_value_stuff x_ 5975=260 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 5975259 let rec await_value_stuff_rect_Type1 h_mk_await_value_stuff x_6092 = 260 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6092 261 261 in 262 262 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 265 265 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 266 266 await_value_stuff > 'a1 **) 267 let rec await_value_stuff_rect_Type0 h_mk_await_value_stuff x_ 5977=268 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 5977267 let rec await_value_stuff_rect_Type0 h_mk_await_value_stuff x_6094 = 268 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6094 269 269 in 270 270 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 446 446 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 447 447 'a3) > ('a1, 'a2) fullexec > 'a3 **) 448 let rec fullexec_rect_Type4 h_mk_fullexec x_ 5995=448 let rec fullexec_rect_Type4 h_mk_fullexec x_6112 = 449 449 let { es1 = es2; make_global = make_global0; make_initial_state = 450 make_initial_state0 } = x_ 5995450 make_initial_state0 } = x_6112 451 451 in 452 452 h_mk_fullexec __ es2 make_global0 make_initial_state0 … … 455 455 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 456 456 'a3) > ('a1, 'a2) fullexec > 'a3 **) 457 let rec fullexec_rect_Type5 h_mk_fullexec x_ 5997=457 let rec fullexec_rect_Type5 h_mk_fullexec x_6114 = 458 458 let { es1 = es2; make_global = make_global0; make_initial_state = 459 make_initial_state0 } = x_ 5997459 make_initial_state0 } = x_6114 460 460 in 461 461 h_mk_fullexec __ es2 make_global0 make_initial_state0 … … 464 464 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 465 465 'a3) > ('a1, 'a2) fullexec > 'a3 **) 466 let rec fullexec_rect_Type3 h_mk_fullexec x_ 5999=466 let rec fullexec_rect_Type3 h_mk_fullexec x_6116 = 467 467 let { es1 = es2; make_global = make_global0; make_initial_state = 468 make_initial_state0 } = x_ 5999468 make_initial_state0 } = x_6116 469 469 in 470 470 h_mk_fullexec __ es2 make_global0 make_initial_state0 … … 473 473 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 474 474 'a3) > ('a1, 'a2) fullexec > 'a3 **) 475 let rec fullexec_rect_Type2 h_mk_fullexec x_6 001=475 let rec fullexec_rect_Type2 h_mk_fullexec x_6118 = 476 476 let { es1 = es2; make_global = make_global0; make_initial_state = 477 make_initial_state0 } = x_6 001477 make_initial_state0 } = x_6118 478 478 in 479 479 h_mk_fullexec __ es2 make_global0 make_initial_state0 … … 482 482 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 483 483 'a3) > ('a1, 'a2) fullexec > 'a3 **) 484 let rec fullexec_rect_Type1 h_mk_fullexec x_6 003=484 let rec fullexec_rect_Type1 h_mk_fullexec x_6120 = 485 485 let { es1 = es2; make_global = make_global0; make_initial_state = 486 make_initial_state0 } = x_6 003486 make_initial_state0 } = x_6120 487 487 in 488 488 h_mk_fullexec __ es2 make_global0 make_initial_state0 … … 491 491 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 492 492 'a3) > ('a1, 'a2) fullexec > 'a3 **) 493 let rec fullexec_rect_Type0 h_mk_fullexec x_6 005=493 let rec fullexec_rect_Type0 h_mk_fullexec x_6122 = 494 494 let { es1 = es2; make_global = make_global0; make_initial_state = 495 make_initial_state0 } = x_6 005495 make_initial_state0 } = x_6122 496 496 in 497 497 h_mk_fullexec __ es2 make_global0 make_initial_state0
Note: See TracChangeset
for help on using the changeset viewer.