Changeset 2717 for extracted/smallstepExec.ml
 Timestamp:
 Feb 23, 2013, 1:16:55 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/smallstepExec.ml
r2649 r2717 47 47 open IOMonad 48 48 49 open Exp 50 49 51 open Arithmetic 50 52 … … 58 60 59 61 open Integers 62 63 open BitVectorTrie 60 64 61 65 open CostLabel … … 95 99 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 96 100 'a2) trans_system > 'a3 **) 97 let rec trans_system_rect_Type4 h_mk_trans_system x_ 7818=98 let { is_final = is_final0; step = step0 } = x_ 7818in101 let rec trans_system_rect_Type4 h_mk_trans_system x_5847 = 102 let { is_final = is_final0; step = step0 } = x_5847 in 99 103 h_mk_trans_system __ __ is_final0 step0 100 104 … … 103 107 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 104 108 'a2) trans_system > 'a3 **) 105 let rec trans_system_rect_Type5 h_mk_trans_system x_ 7820=106 let { is_final = is_final0; step = step0 } = x_ 7820in109 let rec trans_system_rect_Type5 h_mk_trans_system x_5849 = 110 let { is_final = is_final0; step = step0 } = x_5849 in 107 111 h_mk_trans_system __ __ is_final0 step0 108 112 … … 111 115 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 112 116 'a2) trans_system > 'a3 **) 113 let rec trans_system_rect_Type3 h_mk_trans_system x_ 7822=114 let { is_final = is_final0; step = step0 } = x_ 7822in117 let rec trans_system_rect_Type3 h_mk_trans_system x_5851 = 118 let { is_final = is_final0; step = step0 } = x_5851 in 115 119 h_mk_trans_system __ __ is_final0 step0 116 120 … … 119 123 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 120 124 'a2) trans_system > 'a3 **) 121 let rec trans_system_rect_Type2 h_mk_trans_system x_ 7824=122 let { is_final = is_final0; step = step0 } = x_ 7824in125 let rec trans_system_rect_Type2 h_mk_trans_system x_5853 = 126 let { is_final = is_final0; step = step0 } = x_5853 in 123 127 h_mk_trans_system __ __ is_final0 step0 124 128 … … 127 131 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 128 132 'a2) trans_system > 'a3 **) 129 let rec trans_system_rect_Type1 h_mk_trans_system x_ 7826=130 let { is_final = is_final0; step = step0 } = x_ 7826in133 let rec trans_system_rect_Type1 h_mk_trans_system x_5855 = 134 let { is_final = is_final0; step = step0 } = x_5855 in 131 135 h_mk_trans_system __ __ is_final0 step0 132 136 … … 135 139 ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) > 'a3) > ('a1, 136 140 'a2) trans_system > 'a3 **) 137 let rec trans_system_rect_Type0 h_mk_trans_system x_ 7828=138 let { is_final = is_final0; step = step0 } = x_ 7828in141 let rec trans_system_rect_Type0 h_mk_trans_system x_5857 = 142 let { is_final = is_final0; step = step0 } = x_5857 in 139 143 h_mk_trans_system __ __ is_final0 step0 140 144 … … 223 227 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 224 228 await_value_stuff > 'a1 **) 225 let rec await_value_stuff_rect_Type4 h_mk_await_value_stuff x_ 7990=226 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 7990229 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_6019 227 231 in 228 232 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 231 235 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 232 236 await_value_stuff > 'a1 **) 233 let rec await_value_stuff_rect_Type5 h_mk_await_value_stuff x_ 7992=234 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 7992237 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_6021 235 239 in 236 240 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 239 243 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 240 244 await_value_stuff > 'a1 **) 241 let rec await_value_stuff_rect_Type3 h_mk_await_value_stuff x_ 7994=242 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 7994245 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_6023 243 247 in 244 248 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 247 251 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 248 252 await_value_stuff > 'a1 **) 249 let rec await_value_stuff_rect_Type2 h_mk_await_value_stuff x_ 7996=250 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 7996253 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_6025 251 255 in 252 256 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 255 259 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 256 260 await_value_stuff > 'a1 **) 257 let rec await_value_stuff_rect_Type1 h_mk_await_value_stuff x_ 7998=258 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 7998261 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_6027 259 263 in 260 264 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 263 267 (__ > __ > (__, __) trans_system > __ > (__ > Bool.bool) > 'a1) > 264 268 await_value_stuff > 'a1 **) 265 let rec await_value_stuff_rect_Type0 h_mk_await_value_stuff x_ 8000=266 let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_ 8000269 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_6029 267 271 in 268 272 h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0 … … 317 321 318 322 type assert0 = __ 323 324 type assert_nz = __ 319 325 320 326 type after_aux = __ … … 450 456 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 451 457 'a3) > ('a1, 'a2) fullexec > 'a3 **) 452 let rec fullexec_rect_Type4 h_mk_fullexec x_ 8018=458 let rec fullexec_rect_Type4 h_mk_fullexec x_6047 = 453 459 let { es1 = es2; make_global = make_global0; make_initial_state = 454 make_initial_state0 } = x_ 8018460 make_initial_state0 } = x_6047 455 461 in 456 462 h_mk_fullexec __ es2 make_global0 make_initial_state0 … … 459 465 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 460 466 'a3) > ('a1, 'a2) fullexec > 'a3 **) 461 let rec fullexec_rect_Type5 h_mk_fullexec x_ 8020=467 let rec fullexec_rect_Type5 h_mk_fullexec x_6049 = 462 468 let { es1 = es2; make_global = make_global0; make_initial_state = 463 make_initial_state0 } = x_ 8020469 make_initial_state0 } = x_6049 464 470 in 465 471 h_mk_fullexec __ es2 make_global0 make_initial_state0 … … 468 474 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 469 475 'a3) > ('a1, 'a2) fullexec > 'a3 **) 470 let rec fullexec_rect_Type3 h_mk_fullexec x_ 8022=476 let rec fullexec_rect_Type3 h_mk_fullexec x_6051 = 471 477 let { es1 = es2; make_global = make_global0; make_initial_state = 472 make_initial_state0 } = x_ 8022478 make_initial_state0 } = x_6051 473 479 in 474 480 h_mk_fullexec __ es2 make_global0 make_initial_state0 … … 477 483 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 478 484 'a3) > ('a1, 'a2) fullexec > 'a3 **) 479 let rec fullexec_rect_Type2 h_mk_fullexec x_ 8024=485 let rec fullexec_rect_Type2 h_mk_fullexec x_6053 = 480 486 let { es1 = es2; make_global = make_global0; make_initial_state = 481 make_initial_state0 } = x_ 8024487 make_initial_state0 } = x_6053 482 488 in 483 489 h_mk_fullexec __ es2 make_global0 make_initial_state0 … … 486 492 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 487 493 'a3) > ('a1, 'a2) fullexec > 'a3 **) 488 let rec fullexec_rect_Type1 h_mk_fullexec x_ 8026=494 let rec fullexec_rect_Type1 h_mk_fullexec x_6055 = 489 495 let { es1 = es2; make_global = make_global0; make_initial_state = 490 make_initial_state0 } = x_ 8026496 make_initial_state0 } = x_6055 491 497 in 492 498 h_mk_fullexec __ es2 make_global0 make_initial_state0 … … 495 501 (__ > ('a1, 'a2) trans_system > (__ > __) > (__ > __ Errors.res) > 496 502 'a3) > ('a1, 'a2) fullexec > 'a3 **) 497 let rec fullexec_rect_Type0 h_mk_fullexec x_ 8028=503 let rec fullexec_rect_Type0 h_mk_fullexec x_6057 = 498 504 let { es1 = es2; make_global = make_global0; make_initial_state = 499 make_initial_state0 } = x_ 8028505 make_initial_state0 } = x_6057 500 506 in 501 507 h_mk_fullexec __ es2 make_global0 make_initial_state0 … … 578 584  E_interact (x0, x1) > Types.None) 579 585 586 (** val exec_steps : 587 Nat.nat > ('a1, 'a2) fullexec > __ > __ > ((__, Events.trace) 588 Types.prod List.list, __) Types.prod Errors.res **) 589 let rec exec_steps n fx g0 s = 590 match n with 591  Nat.O > 592 Obj.magic 593 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = List.Nil; 594 Types.snd = s }) 595  Nat.S m > 596 (match fx.es1.is_final g0 s with 597  Types.None > 598 (match fx.es1.step g0 s with 599  IOMonad.Interact (x, x0) > 600 Errors.Error (Errors.msg ErrorMessages.UnexpectedIO) 601  IOMonad.Value trs > 602 Obj.magic 603 (Monad.m_bind2 (Monad.max_def Errors.res0) 604 (Obj.magic (exec_steps m fx g0 trs.Types.snd)) (fun tl s' > 605 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = 606 (List.Cons ({ Types.fst = s; Types.snd = trs.Types.fst }, 607 tl)); Types.snd = s' })) 608  IOMonad.Wrong m0 > Errors.Error m0) 609  Types.Some r > 610 Errors.Error (Errors.msg ErrorMessages.TerminatedEarly)) 611 612 (** val gather_trace : 613 ('a1, Events.trace) Types.prod List.list > Events.trace **) 614 let rec gather_trace = function 615  List.Nil > Events.e0 616  List.Cons (h, t) > Events.eapp h.Types.snd (gather_trace t) 617 618 (** val switch_trace_aux : 619 Events.trace > ('a1, Events.trace) Types.prod List.list > 'a1 > 620 (Events.trace, 'a1) Types.prod List.list **) 621 let rec switch_trace_aux tr l s' = 622 match l with 623  List.Nil > List.Cons ({ Types.fst = tr; Types.snd = s' }, List.Nil) 624  List.Cons (h, t) > 625 List.Cons ({ Types.fst = tr; Types.snd = h.Types.fst }, 626 (switch_trace_aux h.Types.snd t s')) 627 628 (** val switch_trace : 629 ('a1, Events.trace) Types.prod List.list > 'a1 > (Events.trace, 'a1) 630 Types.prod List.list **) 631 let switch_trace l s' = 632 match l with 633  List.Nil > List.Nil 634  List.Cons (h, t) > switch_trace_aux h.Types.snd t s' 635
Note: See TracChangeset
for help on using the changeset viewer.