extracted/smallstepExec.ml

   1 open Preamble
   2
   3 open Div_and_mod
   4
   5 open Jmeq
   6
   7 open Russell
   8
   9 open Util
  10
  11 open Bool
  12
  13 open Relations
  14
  15 open Nat
  16
  17 open List
  18
  19 open Hints_declaration
  20
  21 open Core_notation
  22
  23 open Pts
  24
  25 open Logic
  26
  27 open Types
  28
  29 open Extralib
  30
  31 open Proper
  32
  33 open ErrorMessages
  34
  35 open Option
  36
  37 open Setoids
  38
  39 open Monad
  40
  41 open Positive
  42
  43 open PreIdentifiers
  44
  45 open Errors
  46
  47 open IOMonad
  48
  49 open Exp
  50
  51 open Arithmetic
  52
  53 open Vector
  54
  55 open FoldStuff
  56
  57 open BitVector
  58
  59 open Extranat
  60
  61 open Integers
  62
  63 open CostLabel
  64
  65 open PositiveMap
  66
  67 open Deqsets
  68
  69 open Lists
  70
  71 open Identifiers
  72
  73 open AST
  74
  75 open Division
  76
  77 open Z
  78
  79 open BitVectorZ
  80
  81 open Pointers
  82
  83 open Coqlib
  84
  85 open Values
  86
  87 open Events
  88
  89 type ('outty, 'inty) trans_system = { is_final : (__ -> __ -> Integers.int
  90                                                  Types.option);
  91                                       step : (__ -> __ -> ('outty, 'inty,
  92                                              (Events.trace, __) Types.prod)
  93                                              IOMonad.iO) }
  94
  95 (** val trans_system_rect_Type4 :
  96     (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
  97     ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
  98     'a2) trans_system -> 'a3 **)
  99 let rec trans_system_rect_Type4 h_mk_trans_system x_5925 =
 100   let { is_final = is_final0; step = step0 } = x_5925 in
 101   h_mk_trans_system __ __ is_final0 step0
 102
 103 (** val trans_system_rect_Type5 :
 104     (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
 105     ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
 106     'a2) trans_system -> 'a3 **)
 107 let rec trans_system_rect_Type5 h_mk_trans_system x_5927 =
 108   let { is_final = is_final0; step = step0 } = x_5927 in
 109   h_mk_trans_system __ __ is_final0 step0
 110
 111 (** val trans_system_rect_Type3 :
 112     (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
 113     ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
 114     'a2) trans_system -> 'a3 **)
 115 let rec trans_system_rect_Type3 h_mk_trans_system x_5929 =
 116   let { is_final = is_final0; step = step0 } = x_5929 in
 117   h_mk_trans_system __ __ is_final0 step0
 118
 119 (** val trans_system_rect_Type2 :
 120     (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
 121     ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
 122     'a2) trans_system -> 'a3 **)
 123 let rec trans_system_rect_Type2 h_mk_trans_system x_5931 =
 124   let { is_final = is_final0; step = step0 } = x_5931 in
 125   h_mk_trans_system __ __ is_final0 step0
 126
 127 (** val trans_system_rect_Type1 :
 128     (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
 129     ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
 130     'a2) trans_system -> 'a3 **)
 131 let rec trans_system_rect_Type1 h_mk_trans_system x_5933 =
 132   let { is_final = is_final0; step = step0 } = x_5933 in
 133   h_mk_trans_system __ __ is_final0 step0
 134
 135 (** val trans_system_rect_Type0 :
 136     (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
 137     ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
 138     'a2) trans_system -> 'a3 **)
 139 let rec trans_system_rect_Type0 h_mk_trans_system x_5935 =
 140   let { is_final = is_final0; step = step0 } = x_5935 in
 141   h_mk_trans_system __ __ is_final0 step0
 142
 143 type ('x, 'x0) global = __
 144
 145 type ('x, 'x0) state = __
 146
 147 (** val is_final :
 148     ('a1, 'a2) trans_system -> __ -> __ -> Integers.int Types.option **)
 149 let rec is_final xxx =
 150   xxx.is_final
 151
 152 (** val step :
 153     ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2, (Events.trace, __)
 154     Types.prod) IOMonad.iO **)
 155 let rec step xxx =
 156   xxx.step
 157
 158 (** val trans_system_inv_rect_Type4 :
 159     ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
 160     Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
 161     IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
 162 let trans_system_inv_rect_Type4 hterm h1 =
 163   let hcut = trans_system_rect_Type4 h1 hterm in hcut __
 164
 165 (** val trans_system_inv_rect_Type3 :
 166     ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
 167     Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
 168     IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
 169 let trans_system_inv_rect_Type3 hterm h1 =
 170   let hcut = trans_system_rect_Type3 h1 hterm in hcut __
 171
 172 (** val trans_system_inv_rect_Type2 :
 173     ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
 174     Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
 175     IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
 176 let trans_system_inv_rect_Type2 hterm h1 =
 177   let hcut = trans_system_rect_Type2 h1 hterm in hcut __
 178
 179 (** val trans_system_inv_rect_Type1 :
 180     ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
 181     Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
 182     IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
 183 let trans_system_inv_rect_Type1 hterm h1 =
 184   let hcut = trans_system_rect_Type1 h1 hterm in hcut __
 185
 186 (** val trans_system_inv_rect_Type0 :
 187     ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
 188     Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
 189     IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
 190 let trans_system_inv_rect_Type0 hterm h1 =
 191   let hcut = trans_system_rect_Type0 h1 hterm in hcut __
 192
 193 (** val repeat :
 194     Nat.nat -> ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2,
 195     (Events.trace, __) Types.prod) IOMonad.iO **)
 196 let rec repeat n exec g s =
 197   match n with
 198   | Nat.O -> IOMonad.Value { Types.fst = Events.e0; Types.snd = s }
 199   | Nat.S n' ->
 200     Obj.magic
 201       (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
 202         (Obj.magic (exec.step g s)) (fun t1 s1 ->
 203         Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
 204           (Obj.magic (repeat n' exec g s1)) (fun tn sn ->
 205           Obj.magic (IOMonad.Value { Types.fst = (Events.eapp t1 tn);
 206             Types.snd = sn }))))
 207
 208 (** val trace_map :
 209     ('a1 -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list ->
 210     (Events.trace, 'a2 List.list) Types.prod Errors.res **)
 211 let rec trace_map f = function
 212 | List.Nil -> Errors.OK { Types.fst = Events.e0; Types.snd = List.Nil }
 213 | List.Cons (h, t) ->
 214   Obj.magic
 215     (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic f h) (fun tr h' ->
 216       Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (trace_map f t))
 217         (fun tr' t' ->
 218         Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr'); Types.snd =
 219           (List.Cons (h', t')) }))))
 220
 221 type await_value_stuff = { avs_exec : (__, __) trans_system; avs_g :
 222                            __; avs_inv : (__ -> Bool.bool) }
 223
 224 (** val await_value_stuff_rect_Type4 :
 225     (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
 226     await_value_stuff -> 'a1 **)
 227 let rec await_value_stuff_rect_Type4 h_mk_await_value_stuff x_6097 =
 228   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6097
 229   in
 230   h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
 231
 232 (** val await_value_stuff_rect_Type5 :
 233     (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
 234     await_value_stuff -> 'a1 **)
 235 let rec await_value_stuff_rect_Type5 h_mk_await_value_stuff x_6099 =
 236   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6099
 237   in
 238   h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
 239
 240 (** val await_value_stuff_rect_Type3 :
 241     (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
 242     await_value_stuff -> 'a1 **)
 243 let rec await_value_stuff_rect_Type3 h_mk_await_value_stuff x_6101 =
 244   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6101
 245   in
 246   h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
 247
 248 (** val await_value_stuff_rect_Type2 :
 249     (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
 250     await_value_stuff -> 'a1 **)
 251 let rec await_value_stuff_rect_Type2 h_mk_await_value_stuff x_6103 =
 252   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6103
 253   in
 254   h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
 255
 256 (** val await_value_stuff_rect_Type1 :
 257     (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
 258     await_value_stuff -> 'a1 **)
 259 let rec await_value_stuff_rect_Type1 h_mk_await_value_stuff x_6105 =
 260   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6105
 261   in
 262   h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
 263
 264 (** val await_value_stuff_rect_Type0 :
 265     (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
 266     await_value_stuff -> 'a1 **)
 267 let rec await_value_stuff_rect_Type0 h_mk_await_value_stuff x_6107 =
 268   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6107
 269   in
 270   h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
 271
 272 type avs_O = __
 273
 274 type avs_I = __
 275
 276 (** val avs_exec : await_value_stuff -> (__, __) trans_system **)
 277 let rec avs_exec xxx =
 278   xxx.avs_exec
 279
 280 (** val avs_g : await_value_stuff -> __ **)
 281 let rec avs_g xxx =
 282   xxx.avs_g
 283
 284 (** val avs_inv : await_value_stuff -> __ -> Bool.bool **)
 285 let rec avs_inv xxx =
 286   xxx.avs_inv
 287
 288 (** val await_value_stuff_inv_rect_Type4 :
 289     await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
 290     Bool.bool) -> __ -> 'a1) -> 'a1 **)
 291 let await_value_stuff_inv_rect_Type4 hterm h1 =
 292   let hcut = await_value_stuff_rect_Type4 h1 hterm in hcut __
 293
 294 (** val await_value_stuff_inv_rect_Type3 :
 295     await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
 296     Bool.bool) -> __ -> 'a1) -> 'a1 **)
 297 let await_value_stuff_inv_rect_Type3 hterm h1 =
 298   let hcut = await_value_stuff_rect_Type3 h1 hterm in hcut __
 299
 300 (** val await_value_stuff_inv_rect_Type2 :
 301     await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
 302     Bool.bool) -> __ -> 'a1) -> 'a1 **)
 303 let await_value_stuff_inv_rect_Type2 hterm h1 =
 304   let hcut = await_value_stuff_rect_Type2 h1 hterm in hcut __
 305
 306 (** val await_value_stuff_inv_rect_Type1 :
 307     await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
 308     Bool.bool) -> __ -> 'a1) -> 'a1 **)
 309 let await_value_stuff_inv_rect_Type1 hterm h1 =
 310   let hcut = await_value_stuff_rect_Type1 h1 hterm in hcut __
 311
 312 (** val await_value_stuff_inv_rect_Type0 :
 313     await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
 314     Bool.bool) -> __ -> 'a1) -> 'a1 **)
 315 let await_value_stuff_inv_rect_Type0 hterm h1 =
 316   let hcut = await_value_stuff_rect_Type0 h1 hterm in hcut __
 317
 318 type ('state, 'output, 'input) execution = ('state, 'output, 'input) __execution Lazy.t
 319 and ('state, 'output, 'input) __execution =
 320 | E_stop of Events.trace * Integers.int * 'state
 321 | E_step of Events.trace * 'state * ('state, 'output, 'input) execution
 322 | E_wrong of Errors.errmsg
 323 | E_interact of 'output * ('input -> ('state, 'output, 'input) execution)
 324
 325 (** val execution_inv_rect_Type4 :
 326     ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
 327     -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
 328     'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
 329     execution) -> __ -> 'a4) -> 'a4 **)
 330 let execution_inv_rect_Type4 hterm h1 h2 h3 h4 =
 331   let hcut =
 332     match Lazy.force
 333     hterm with
 334     | E_stop (x, x0, x1) -> h1 x x0 x1
 335     | E_step (x, x0, x1) -> h2 x x0 x1
 336     | E_wrong x -> h3 x
 337     | E_interact (x, x0) -> h4 x x0
 338   in
 339   hcut __
 340
 341 (** val execution_inv_rect_Type3 :
 342     ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
 343     -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
 344     'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
 345     execution) -> __ -> 'a4) -> 'a4 **)
 346 let execution_inv_rect_Type3 hterm h1 h2 h3 h4 =
 347   let hcut =
 348     match Lazy.force
 349     hterm with
 350     | E_stop (x, x0, x1) -> h1 x x0 x1
 351     | E_step (x, x0, x1) -> h2 x x0 x1
 352     | E_wrong x -> h3 x
 353     | E_interact (x, x0) -> h4 x x0
 354   in
 355   hcut __
 356
 357 (** val execution_inv_rect_Type2 :
 358     ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
 359     -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
 360     'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
 361     execution) -> __ -> 'a4) -> 'a4 **)
 362 let execution_inv_rect_Type2 hterm h1 h2 h3 h4 =
 363   let hcut =
 364     match Lazy.force
 365     hterm with
 366     | E_stop (x, x0, x1) -> h1 x x0 x1
 367     | E_step (x, x0, x1) -> h2 x x0 x1
 368     | E_wrong x -> h3 x
 369     | E_interact (x, x0) -> h4 x x0
 370   in
 371   hcut __
 372
 373 (** val execution_inv_rect_Type1 :
 374     ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
 375     -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
 376     'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
 377     execution) -> __ -> 'a4) -> 'a4 **)
 378 let execution_inv_rect_Type1 hterm h1 h2 h3 h4 =
 379   let hcut =
 380     match Lazy.force
 381     hterm with
 382     | E_stop (x, x0, x1) -> h1 x x0 x1
 383     | E_step (x, x0, x1) -> h2 x x0 x1
 384     | E_wrong x -> h3 x
 385     | E_interact (x, x0) -> h4 x x0
 386   in
 387   hcut __
 388
 389 (** val execution_inv_rect_Type0 :
 390     ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
 391     -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
 392     'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
 393     execution) -> __ -> 'a4) -> 'a4 **)
 394 let execution_inv_rect_Type0 hterm h1 h2 h3 h4 =
 395   let hcut =
 396     match Lazy.force
 397     hterm with
 398     | E_stop (x, x0, x1) -> h1 x x0 x1
 399     | E_step (x, x0, x1) -> h2 x x0 x1
 400     | E_wrong x -> h3 x
 401     | E_interact (x, x0) -> h4 x x0
 402   in
 403   hcut __
 404
 405 (** val execution_discr :
 406     ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __ **)
 407 let execution_discr x y =
 408   Logic.eq_rect_Type2 x
 409     (match Lazy.force
 410      x with
 411      | E_stop (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
 412      | E_step (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
 413      | E_wrong a0 -> Obj.magic (fun _ dH -> dH __)
 414      | E_interact (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 415
 416 (** val execution_jmdiscr :
 417     ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __ **)
 418 let execution_jmdiscr x y =
 419   Logic.eq_rect_Type2 x
 420     (match Lazy.force
 421      x with
 422      | E_stop (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
 423      | E_step (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
 424      | E_wrong a0 -> Obj.magic (fun _ dH -> dH __)
 425      | E_interact (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 426
 427 (** val exec_inf_aux :
 428     ('a1, 'a2) trans_system -> __ -> ('a1, 'a2, (Events.trace, __)
 429     Types.prod) IOMonad.iO -> (__, 'a1, 'a2) execution **)
 430 let rec exec_inf_aux exec g = function
 431 | IOMonad.Interact (out, k') ->
 432   lazy (E_interact (out, (fun v -> exec_inf_aux exec g (k' v))))
 433 | IOMonad.Value v ->
 434   let { Types.fst = t; Types.snd = s' } = v in
 435   (match exec.is_final g s' with
 436    | Types.None ->
 437      lazy (E_step (t, s', (exec_inf_aux exec g (exec.step g s'))))
 438    | Types.Some r -> lazy (E_stop (t, r, s')))
 439 | IOMonad.Wrong m -> lazy (E_wrong m)
 440
 441 type ('outty, 'inty) fullexec = { es1 : ('outty, 'inty) trans_system;
 442                                   make_global : (__ -> __);
 443                                   make_initial_state : (__ -> __ Errors.res) }
 444
 445 (** val fullexec_rect_Type4 :
 446     (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
 447     'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
 448 let rec fullexec_rect_Type4 h_mk_fullexec x_6125 =
 449   let { es1 = es2; make_global = make_global0; make_initial_state =
 450     make_initial_state0 } = x_6125
 451   in
 452   h_mk_fullexec __ es2 make_global0 make_initial_state0
 453
 454 (** val fullexec_rect_Type5 :
 455     (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
 456     'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
 457 let rec fullexec_rect_Type5 h_mk_fullexec x_6127 =
 458   let { es1 = es2; make_global = make_global0; make_initial_state =
 459     make_initial_state0 } = x_6127
 460   in
 461   h_mk_fullexec __ es2 make_global0 make_initial_state0
 462
 463 (** val fullexec_rect_Type3 :
 464     (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
 465     'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
 466 let rec fullexec_rect_Type3 h_mk_fullexec x_6129 =
 467   let { es1 = es2; make_global = make_global0; make_initial_state =
 468     make_initial_state0 } = x_6129
 469   in
 470   h_mk_fullexec __ es2 make_global0 make_initial_state0
 471
 472 (** val fullexec_rect_Type2 :
 473     (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
 474     'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
 475 let rec fullexec_rect_Type2 h_mk_fullexec x_6131 =
 476   let { es1 = es2; make_global = make_global0; make_initial_state =
 477     make_initial_state0 } = x_6131
 478   in
 479   h_mk_fullexec __ es2 make_global0 make_initial_state0
 480
 481 (** val fullexec_rect_Type1 :
 482     (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
 483     'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
 484 let rec fullexec_rect_Type1 h_mk_fullexec x_6133 =
 485   let { es1 = es2; make_global = make_global0; make_initial_state =
 486     make_initial_state0 } = x_6133
 487   in
 488   h_mk_fullexec __ es2 make_global0 make_initial_state0
 489
 490 (** val fullexec_rect_Type0 :
 491     (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
 492     'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
 493 let rec fullexec_rect_Type0 h_mk_fullexec x_6135 =
 494   let { es1 = es2; make_global = make_global0; make_initial_state =
 495     make_initial_state0 } = x_6135
 496   in
 497   h_mk_fullexec __ es2 make_global0 make_initial_state0
 498
 499 type ('x, 'x0) program = __
 500
 501 (** val es1 : ('a1, 'a2) fullexec -> ('a1, 'a2) trans_system **)
 502 let rec es1 xxx =
 503   xxx.es1
 504
 505 (** val make_global : ('a1, 'a2) fullexec -> __ -> __ **)
 506 let rec make_global xxx =
 507   xxx.make_global
 508
 509 (** val make_initial_state : ('a1, 'a2) fullexec -> __ -> __ Errors.res **)
 510 let rec make_initial_state xxx =
 511   xxx.make_initial_state
 512
 513 (** val fullexec_inv_rect_Type4 :
 514     ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
 515     (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
 516 let fullexec_inv_rect_Type4 hterm h1 =
 517   let hcut = fullexec_rect_Type4 h1 hterm in hcut __
 518
 519 (** val fullexec_inv_rect_Type3 :
 520     ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
 521     (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
 522 let fullexec_inv_rect_Type3 hterm h1 =
 523   let hcut = fullexec_rect_Type3 h1 hterm in hcut __
 524
 525 (** val fullexec_inv_rect_Type2 :
 526     ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
 527     (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
 528 let fullexec_inv_rect_Type2 hterm h1 =
 529   let hcut = fullexec_rect_Type2 h1 hterm in hcut __
 530
 531 (** val fullexec_inv_rect_Type1 :
 532     ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
 533     (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
 534 let fullexec_inv_rect_Type1 hterm h1 =
 535   let hcut = fullexec_rect_Type1 h1 hterm in hcut __
 536
 537 (** val fullexec_inv_rect_Type0 :
 538     ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
 539     (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
 540 let fullexec_inv_rect_Type0 hterm h1 =
 541   let hcut = fullexec_rect_Type0 h1 hterm in hcut __
 542
 543 (** val exec_inf : ('a1, 'a2) fullexec -> __ -> (__, 'a1, 'a2) execution **)
 544 let exec_inf fx p =
 545   match fx.make_initial_state p with
 546   | Errors.OK s ->
 547     exec_inf_aux fx.es1 (fx.make_global p) (IOMonad.Value { Types.fst =
 548       Events.e0; Types.snd = s })
 549   | Errors.Error m -> lazy (E_wrong m)
 550
 551 type 'x execution_prefix = (Events.trace, 'x) Types.prod List.list
 552
 553 (** val split_trace :
 554     ('a3, 'a1, 'a2) execution -> Nat.nat -> ('a3 execution_prefix, ('a3, 'a1,
 555     'a2) execution) Types.prod Types.option **)
 556 let rec split_trace x = function
 557 | Nat.O -> Types.Some { Types.fst = List.Nil; Types.snd = x }
 558 | Nat.S n' ->
 559   (match Lazy.force
 560    x with
 561    | E_stop (tr, r, s) ->
 562      (match n' with
 563       | Nat.O ->
 564         Types.Some { Types.fst = (List.Cons ({ Types.fst = tr; Types.snd =
 565           s }, List.Nil)); Types.snd = x }
 566       | Nat.S x0 -> Types.None)
 567    | E_step (tr, s, x') ->
 568      Obj.magic
 569        (Monad.m_bind2 (Monad.max_def Option.option)
 570          (Obj.magic (split_trace x' n')) (fun pre x'' ->
 571          Obj.magic (Types.Some { Types.fst = (List.Cons ({ Types.fst = tr;
 572            Types.snd = s }, pre)); Types.snd = x'' })))
 573    | E_wrong x0 -> Types.None
 574    | E_interact (x0, x1) -> Types.None)
 575
 576 (** val exec_steps :
 577     Nat.nat -> ('a1, 'a2) fullexec -> __ -> __ -> ((__, Events.trace)
 578     Types.prod List.list, __) Types.prod Errors.res **)
 579 let rec exec_steps n fx g s =
 580   match n with
 581   | Nat.O ->
 582     Obj.magic
 583       (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = List.Nil;
 584         Types.snd = s })
 585   | Nat.S m ->
 586     (match fx.es1.is_final g s with
 587      | Types.None ->
 588        (match fx.es1.step g s with
 589         | IOMonad.Interact (x, x0) ->
 590           Errors.Error (Errors.msg ErrorMessages.UnexpectedIO)
 591         | IOMonad.Value trs ->
 592           Obj.magic
 593             (Monad.m_bind2 (Monad.max_def Errors.res0)
 594               (Obj.magic (exec_steps m fx g trs.Types.snd)) (fun tl s' ->
 595               Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 596                 (List.Cons ({ Types.fst = s; Types.snd = trs.Types.fst },
 597                 tl)); Types.snd = s' }))
 598         | IOMonad.Wrong m0 -> Errors.Error m0)
 599      | Types.Some r ->
 600        Errors.Error (Errors.msg ErrorMessages.TerminatedEarly))
 601
 602 (** val gather_trace :
 603     ('a1, Events.trace) Types.prod List.list -> Events.trace **)
 604 let rec gather_trace = function
 605 | List.Nil -> Events.e0
 606 | List.Cons (h, t) -> Events.eapp h.Types.snd (gather_trace t)
 607
 608 (** val switch_trace_aux :
 609     Events.trace -> ('a1, Events.trace) Types.prod List.list -> 'a1 ->
 610     (Events.trace, 'a1) Types.prod List.list **)
 611 let rec switch_trace_aux tr l s' =
 612   match l with
 613   | List.Nil -> List.Cons ({ Types.fst = tr; Types.snd = s' }, List.Nil)
 614   | List.Cons (h, t) ->
 615     List.Cons ({ Types.fst = tr; Types.snd = h.Types.fst },
 616       (switch_trace_aux h.Types.snd t s'))
 617
 618 (** val switch_trace :
 619     ('a1, Events.trace) Types.prod List.list -> 'a1 -> (Events.trace, 'a1)
 620     Types.prod List.list **)
 621 let switch_trace l s' =
 622   match l with
 623   | List.Nil -> List.Nil
 624   | List.Cons (h, t) -> switch_trace_aux h.Types.snd t s'
 625