extracted/rTLabs_traces.ml

   1 open Preamble
   2
   3 open Deqsets_extra
   4
   5 open CostSpec
   6
   7 open Sets
   8
   9 open Listb
  10
  11 open StructuredTraces
  12
  13 open BitVectorTrie
  14
  15 open Graphs
  16
  17 open Order
  18
  19 open Registers
  20
  21 open FrontEndOps
  22
  23 open RTLabs_syntax
  24
  25 open SmallstepExec
  26
  27 open CostLabel
  28
  29 open Events
  30
  31 open IOMonad
  32
  33 open IO
  34
  35 open Extra_bool
  36
  37 open Coqlib
  38
  39 open Values
  40
  41 open FrontEndVal
  42
  43 open Hide
  44
  45 open ByteValues
  46
  47 open Division
  48
  49 open Z
  50
  51 open BitVectorZ
  52
  53 open Pointers
  54
  55 open GenMem
  56
  57 open FrontEndMem
  58
  59 open Proper
  60
  61 open PositiveMap
  62
  63 open Deqsets
  64
  65 open Extralib
  66
  67 open Lists
  68
  69 open Identifiers
  70
  71 open Exp
  72
  73 open Arithmetic
  74
  75 open Vector
  76
  77 open Div_and_mod
  78
  79 open Util
  80
  81 open FoldStuff
  82
  83 open BitVector
  84
  85 open Extranat
  86
  87 open Integers
  88
  89 open AST
  90
  91 open Globalenvs
  92
  93 open ErrorMessages
  94
  95 open Option
  96
  97 open Setoids
  98
  99 open Monad
 100
 101 open Jmeq
 102
 103 open Russell
 104
 105 open Positive
 106
 107 open PreIdentifiers
 108
 109 open Errors
 110
 111 open Bool
 112
 113 open Relations
 114
 115 open Nat
 116
 117 open Hints_declaration
 118
 119 open Core_notation
 120
 121 open Pts
 122
 123 open Logic
 124
 125 open Types
 126
 127 open List
 128
 129 open RTLabs_semantics
 130
 131 open RTLabs_abstract
 132
 133 open CostMisc
 134
 135 open Executions
 136
 137 open Listb_extra
 138
 139 type ('o, 'i) flat_trace = ('o, 'i) __flat_trace Lazy.t
 140 and ('o, 'i) __flat_trace =
 141 | Ft_stop of RTLabs_semantics.state
 142 | Ft_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
 143    * ('o, 'i) flat_trace
 144
 145 (** val flat_trace_inv_rect_Type4 :
 146     RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace
 147     -> (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
 148     (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __
 149     -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
 150 let flat_trace_inv_rect_Type4 x3 x4 hterm h1 h2 =
 151   let hcut =
 152     match Lazy.force
 153     hterm with
 154     | Ft_stop x -> h1 x __
 155     | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2
 156   in
 157   hcut __ __
 158
 159 (** val flat_trace_inv_rect_Type3 :
 160     RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace
 161     -> (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
 162     (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __
 163     -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
 164 let flat_trace_inv_rect_Type3 x3 x4 hterm h1 h2 =
 165   let hcut =
 166     match Lazy.force
 167     hterm with
 168     | Ft_stop x -> h1 x __
 169     | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2
 170   in
 171   hcut __ __
 172
 173 (** val flat_trace_inv_rect_Type2 :
 174     RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace
 175     -> (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
 176     (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __
 177     -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
 178 let flat_trace_inv_rect_Type2 x3 x4 hterm h1 h2 =
 179   let hcut =
 180     match Lazy.force
 181     hterm with
 182     | Ft_stop x -> h1 x __
 183     | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2
 184   in
 185   hcut __ __
 186
 187 (** val flat_trace_inv_rect_Type1 :
 188     RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace
 189     -> (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
 190     (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __
 191     -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
 192 let flat_trace_inv_rect_Type1 x3 x4 hterm h1 h2 =
 193   let hcut =
 194     match Lazy.force
 195     hterm with
 196     | Ft_stop x -> h1 x __
 197     | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2
 198   in
 199   hcut __ __
 200
 201 (** val flat_trace_inv_rect_Type0 :
 202     RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace
 203     -> (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
 204     (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __
 205     -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
 206 let flat_trace_inv_rect_Type0 x3 x4 hterm h1 h2 =
 207   let hcut =
 208     match Lazy.force
 209     hterm with
 210     | Ft_stop x -> h1 x __
 211     | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2
 212   in
 213   hcut __ __
 214
 215 (** val flat_trace_discr :
 216     RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace
 217     -> ('a1, 'a2) flat_trace -> __ **)
 218 let flat_trace_discr a3 a4 x y =
 219   Logic.eq_rect_Type2 x
 220     (match Lazy.force
 221      x with
 222      | Ft_stop a0 -> Obj.magic (fun _ dH -> dH __ __)
 223      | Ft_step (a0, a10, a20, a40) ->
 224        Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
 225
 226 (** val flat_trace_jmdiscr :
 227     RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace
 228     -> ('a1, 'a2) flat_trace -> __ **)
 229 let flat_trace_jmdiscr a3 a4 x y =
 230   Logic.eq_rect_Type2 x
 231     (match Lazy.force
 232      x with
 233      | Ft_stop a0 -> Obj.magic (fun _ dH -> dH __ __)
 234      | Ft_step (a0, a10, a20, a40) ->
 235        Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
 236
 237 (** val make_flat_trace :
 238     __ -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace **)
 239 let rec make_flat_trace ge s =
 240   let e =
 241     SmallstepExec.exec_inf_aux
 242       RTLabs_semantics.rTLabs_fullexec.SmallstepExec.es1 ge
 243       (Obj.magic (RTLabs_semantics.eval_statement (Obj.magic ge) s))
 244   in
 245   (match Lazy.force
 246    e with
 247    | SmallstepExec.E_stop (tr, i, s') ->
 248      (fun _ -> lazy (Ft_step (s, tr, (Obj.magic s'), (lazy (Ft_stop
 249        (Obj.magic s'))))))
 250    | SmallstepExec.E_step (tr, s', e') ->
 251      (fun _ -> lazy (Ft_step (s, tr, (Obj.magic s'),
 252        (make_flat_trace ge (Obj.magic s')))))
 253    | SmallstepExec.E_wrong m -> (fun _ -> assert false (* absurd case *))
 254    | SmallstepExec.E_interact (o, f) ->
 255      (fun _ -> assert false (* absurd case *))) __
 256
 257 (** val make_whole_flat_trace :
 258     __ -> __ -> (IO.io_out, IO.io_in) flat_trace **)
 259 let make_whole_flat_trace p s =
 260   let ge = RTLabs_semantics.rTLabs_fullexec.SmallstepExec.make_global p in
 261   let e =
 262     SmallstepExec.exec_inf_aux
 263       RTLabs_semantics.rTLabs_fullexec.SmallstepExec.es1 ge (IOMonad.Value
 264       { Types.fst = Events.e0; Types.snd = s })
 265   in
 266   (match Lazy.force
 267    e with
 268    | SmallstepExec.E_stop (tr, i, s') ->
 269      (fun _ -> lazy (Ft_stop (Obj.magic s)))
 270    | SmallstepExec.E_step (x, x0, e') ->
 271      (fun _ -> make_flat_trace ge (Obj.magic s))
 272    | SmallstepExec.E_wrong m -> (fun _ -> assert false (* absurd case *))
 273    | SmallstepExec.E_interact (o, f) ->
 274      (fun _ -> assert false (* absurd case *))) __
 275
 276 type will_return =
 277 | Wr_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
 278    * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
 279 | Wr_call of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
 280    * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
 281 | Wr_ret of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
 282    * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
 283 | Wr_base of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
 284    * (IO.io_out, IO.io_in) flat_trace
 285
 286 (** val will_return_rect_Type4 :
 287     RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
 288     RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
 289     flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state
 290     -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 291     IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
 292     (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
 293     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
 294     'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
 295     RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
 296     'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
 297     flat_trace -> will_return -> 'a1 **)
 298 let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1409 s x_1408 = function
 299 | Wr_step (s0, tr, s', depth, trace, x_1411) ->
 300   h_wr_step s0 tr s' depth __ trace __ x_1411
 301     (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
 302       s' trace x_1411)
 303 | Wr_call (s0, tr, s', depth, trace, x_1413) ->
 304   h_wr_call s0 tr s' depth __ trace __ x_1413
 305     (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
 306       depth) s' trace x_1413)
 307 | Wr_ret (s0, tr, s', depth, trace, x_1415) ->
 308   h_wr_ret s0 tr s' depth __ trace __ x_1415
 309     (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
 310       s' trace x_1415)
 311 | Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
 312
 313 (** val will_return_rect_Type3 :
 314     RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
 315     RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
 316     flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state
 317     -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 318     IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
 319     (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
 320     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
 321     'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
 322     RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
 323     'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
 324     flat_trace -> will_return -> 'a1 **)
 325 let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1437 s x_1436 = function
 326 | Wr_step (s0, tr, s', depth, trace, x_1439) ->
 327   h_wr_step s0 tr s' depth __ trace __ x_1439
 328     (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
 329       s' trace x_1439)
 330 | Wr_call (s0, tr, s', depth, trace, x_1441) ->
 331   h_wr_call s0 tr s' depth __ trace __ x_1441
 332     (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
 333       depth) s' trace x_1441)
 334 | Wr_ret (s0, tr, s', depth, trace, x_1443) ->
 335   h_wr_ret s0 tr s' depth __ trace __ x_1443
 336     (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
 337       s' trace x_1443)
 338 | Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
 339
 340 (** val will_return_rect_Type2 :
 341     RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
 342     RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
 343     flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state
 344     -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 345     IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
 346     (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
 347     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
 348     'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
 349     RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
 350     'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
 351     flat_trace -> will_return -> 'a1 **)
 352 let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1451 s x_1450 = function
 353 | Wr_step (s0, tr, s', depth, trace, x_1453) ->
 354   h_wr_step s0 tr s' depth __ trace __ x_1453
 355     (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
 356       s' trace x_1453)
 357 | Wr_call (s0, tr, s', depth, trace, x_1455) ->
 358   h_wr_call s0 tr s' depth __ trace __ x_1455
 359     (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
 360       depth) s' trace x_1455)
 361 | Wr_ret (s0, tr, s', depth, trace, x_1457) ->
 362   h_wr_ret s0 tr s' depth __ trace __ x_1457
 363     (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
 364       s' trace x_1457)
 365 | Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
 366
 367 (** val will_return_rect_Type1 :
 368     RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
 369     RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
 370     flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state
 371     -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 372     IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
 373     (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
 374     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
 375     'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
 376     RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
 377     'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
 378     flat_trace -> will_return -> 'a1 **)
 379 let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1465 s x_1464 = function
 380 | Wr_step (s0, tr, s', depth, trace, x_1467) ->
 381   h_wr_step s0 tr s' depth __ trace __ x_1467
 382     (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
 383       s' trace x_1467)
 384 | Wr_call (s0, tr, s', depth, trace, x_1469) ->
 385   h_wr_call s0 tr s' depth __ trace __ x_1469
 386     (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
 387       depth) s' trace x_1469)
 388 | Wr_ret (s0, tr, s', depth, trace, x_1471) ->
 389   h_wr_ret s0 tr s' depth __ trace __ x_1471
 390     (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
 391       s' trace x_1471)
 392 | Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
 393
 394 (** val will_return_rect_Type0 :
 395     RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
 396     RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
 397     flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state
 398     -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 399     IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
 400     (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
 401     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
 402     'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
 403     RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
 404     'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
 405     flat_trace -> will_return -> 'a1 **)
 406 let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1479 s x_1478 = function
 407 | Wr_step (s0, tr, s', depth, trace, x_1481) ->
 408   h_wr_step s0 tr s' depth __ trace __ x_1481
 409     (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
 410       s' trace x_1481)
 411 | Wr_call (s0, tr, s', depth, trace, x_1483) ->
 412   h_wr_call s0 tr s' depth __ trace __ x_1483
 413     (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
 414       depth) s' trace x_1483)
 415 | Wr_ret (s0, tr, s', depth, trace, x_1485) ->
 416   h_wr_ret s0 tr s' depth __ trace __ x_1485
 417     (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
 418       s' trace x_1485)
 419 | Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
 420
 421 (** val will_return_inv_rect_Type4 :
 422     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
 423     IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
 424     Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 425     IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
 426     'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
 427     Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 428     IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
 429     'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
 430     Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 431     IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
 432     'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
 433     Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in)
 434     flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 435 let will_return_inv_rect_Type4 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
 436   let hcut = will_return_rect_Type4 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
 437   hcut __ __ __ __
 438
 439 (** val will_return_inv_rect_Type3 :
 440     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
 441     IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
 442     Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 443     IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
 444     'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
 445     Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 446     IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
 447     'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
 448     Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 449     IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
 450     'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
 451     Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in)
 452     flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 453 let will_return_inv_rect_Type3 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
 454   let hcut = will_return_rect_Type3 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
 455   hcut __ __ __ __
 456
 457 (** val will_return_inv_rect_Type2 :
 458     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
 459     IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
 460     Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 461     IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
 462     'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
 463     Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 464     IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
 465     'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
 466     Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 467     IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
 468     'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
 469     Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in)
 470     flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 471 let will_return_inv_rect_Type2 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
 472   let hcut = will_return_rect_Type2 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
 473   hcut __ __ __ __
 474
 475 (** val will_return_inv_rect_Type1 :
 476     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
 477     IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
 478     Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 479     IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
 480     'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
 481     Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 482     IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
 483     'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
 484     Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 485     IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
 486     'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
 487     Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in)
 488     flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 489 let will_return_inv_rect_Type1 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
 490   let hcut = will_return_rect_Type1 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
 491   hcut __ __ __ __
 492
 493 (** val will_return_inv_rect_Type0 :
 494     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
 495     IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
 496     Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 497     IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
 498     'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
 499     Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 500     IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
 501     'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
 502     Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
 503     IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
 504     'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
 505     Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in)
 506     flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 507 let will_return_inv_rect_Type0 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
 508   let hcut = will_return_rect_Type0 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
 509   hcut __ __ __ __
 510
 511 (** val will_return_jmdiscr :
 512     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
 513     IO.io_in) flat_trace -> will_return -> will_return -> __ **)
 514 let will_return_jmdiscr a1 a2 a3 a4 x y =
 515   Logic.eq_rect_Type2 x
 516     (match x with
 517      | Wr_step (a0, a10, a20, a30, a5, a7) ->
 518        Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
 519      | Wr_call (a0, a10, a20, a30, a5, a7) ->
 520        Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
 521      | Wr_ret (a0, a10, a20, a30, a5, a7) ->
 522        Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
 523      | Wr_base (a0, a10, a20, a40) ->
 524        Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
 525
 526 (** val will_return_length :
 527     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
 528     IO.io_in) flat_trace -> will_return -> Nat.nat **)
 529 let rec will_return_length ge d s tr = function
 530 | Wr_step (x, x0, x1, x2, x4, t') ->
 531   Nat.S (will_return_length ge x2 x1 x4 t')
 532 | Wr_call (x, x0, x1, x2, x4, t') ->
 533   Nat.S (will_return_length ge (Nat.S x2) x1 x4 t')
 534 | Wr_ret (x, x0, x1, x2, x4, t') -> Nat.S (will_return_length ge x2 x1 x4 t')
 535 | Wr_base (x, x0, x1, x3) -> Nat.S Nat.O
 536
 537 (** val will_return_end :
 538     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
 539     IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state,
 540     (IO.io_out, IO.io_in) flat_trace) Types.dPair **)
 541 let rec will_return_end ge d s tr = function
 542 | Wr_step (x, x0, x1, x2, x4, t') -> will_return_end ge x2 x1 x4 t'
 543 | Wr_call (x, x0, x1, x2, x4, t') -> will_return_end ge (Nat.S x2) x1 x4 t'
 544 | Wr_ret (x, x0, x1, x2, x4, t') -> will_return_end ge x2 x1 x4 t'
 545 | Wr_base (x, x0, x1, tr') -> { Types.dpi1 = x1; Types.dpi2 = tr' }
 546
 547 (** val will_return_call :
 548     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state ->
 549     Events.trace -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
 550     flat_trace -> will_return -> will_return Types.sig0 **)
 551 let will_return_call ge d s tr s' trace tERM =
 552   will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace))) tERM
 553     (fun h19 h20 h21 h22 _ h24 _ h26 h27 _ _ _ _ -> assert false
 554     (* absurd case *)) (fun h33 h34 h35 h36 _ h38 _ h40 h41 _ _ _ _ ->
 555     Logic.eq_rect_Type0_r h36 (fun tERM0 h410 _ ->
 556       Logic.eq_rect_Type0_r h33 (fun _ _ _ tERM1 h411 _ ->
 557         Obj.magic flat_trace_jmdiscr ge h33 (lazy (Ft_step (h33, tr, s',
 558           trace))) (lazy (Ft_step (h33, h34, h35, h38))) __ (fun _ ->
 559           Logic.streicherK h33 (fun _ ->
 560             Logic.eq_rect_Type0_r h34 (fun _ _ tERM2 h412 _ _ ->
 561               Logic.eq_rect_Type0_r h35 (fun trace0 _ _ tERM3 h413 _ _ ->
 562                 Logic.eq_rect_Type0_r __ (fun _ tERM4 h414 _ _ ->
 563                   Logic.eq_rect_Type0_r h38 (fun _ tERM5 h415 _ ->
 564                     Logic.streicherK (lazy (Ft_step (h33, h34, h35, h38)))
 565                       (Logic.eq_rect_Type0_r (Wr_call (h33, h34, h35, h36,
 566                         h38, h40)) (fun h416 -> h40) tERM5 h415)) trace0 __
 567                     tERM4 h414 __) __ __ tERM3 h413 __) s' trace __ __ tERM2
 568                 h412 __) tr __ __ tERM1 h411 __))) s __ __ __ tERM0 h410 __)
 569       d tERM h41 __) (fun h47 h48 h49 h50 _ h52 _ h54 h55 _ _ _ _ ->
 570     assert false (* absurd case *)) (fun h61 h62 h63 _ h65 _ _ _ _ _ ->
 571     assert false (* absurd case *))
 572
 573 (** val will_return_return :
 574     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state ->
 575     Events.trace -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
 576     flat_trace -> will_return -> __ **)
 577 let will_return_return ge d s tr s' trace tERM =
 578   will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace))) tERM
 579     (fun h19 h20 h21 h22 _ h24 _ h26 h27 _ _ _ _ -> assert false
 580     (* absurd case *)) (fun h33 h34 h35 h36 _ h38 _ h40 h41 _ _ _ _ ->
 581     assert false (* absurd case *))
 582     (fun h47 h48 h49 h50 _ h52 _ h54 h55 _ _ _ _ ->
 583     Logic.eq_rect_Type0_r (Nat.S h50) (fun tERM0 h550 _ ->
 584       Logic.eq_rect_Type0_r h47 (fun _ _ _ tERM1 h551 _ ->
 585         Obj.magic flat_trace_jmdiscr ge h47 (lazy (Ft_step (h47, tr, s',
 586           trace))) (lazy (Ft_step (h47, h48, h49, h52))) __ (fun _ ->
 587           Logic.streicherK h47 (fun _ ->
 588             Logic.eq_rect_Type0_r h48 (fun _ _ tERM2 h552 _ _ ->
 589               Logic.eq_rect_Type0_r h49 (fun trace0 _ _ tERM3 h553 _ _ ->
 590                 Logic.eq_rect_Type0_r __ (fun _ tERM4 h554 _ _ ->
 591                   Logic.eq_rect_Type0_r h52 (fun _ tERM5 h555 _ ->
 592                     Logic.streicherK (lazy (Ft_step (h47, h48, h49, h52)))
 593                       (Logic.eq_rect_Type0_r (Wr_ret (h47, h48, h49, h50,
 594                         h52, h54)) (fun h556 -> h54) tERM5 h555)) trace0 __
 595                     tERM4 h554 __) __ __ tERM3 h553 __) s' trace __ __ tERM2
 596                 h552 __) tr __ __ tERM1 h551 __))) s __ __ __ tERM0 h550 __)
 597       d tERM h55 __) (Obj.magic __)
 598
 599 (** val will_return_notfn :
 600     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state ->
 601     Events.trace -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
 602     flat_trace -> (__, __) Types.sum -> will_return -> will_return Types.sig0 **)
 603 let will_return_notfn ge d s tr s' trace = function
 604 | Types.Inl _ ->
 605   (fun tERM ->
 606     will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace)))
 607       tERM (fun h290 h291 h292 h293 _ h295 _ h297 h298 _ _ _ _ ->
 608       Logic.eq_rect_Type0_r h293 (fun tERM0 h2980 _ ->
 609         Logic.eq_rect_Type0_r h290 (fun _ _ _ tERM1 h2981 _ ->
 610           Obj.magic flat_trace_jmdiscr ge h290 (lazy (Ft_step (h290, tr, s',
 611             trace))) (lazy (Ft_step (h290, h291, h292, h295))) __ (fun _ ->
 612             Logic.streicherK h290 (fun _ ->
 613               Logic.eq_rect_Type0_r h291 (fun _ _ tERM2 h2982 _ _ ->
 614                 Logic.eq_rect_Type0_r h292 (fun trace0 _ _ tERM3 h2983 _ _ ->
 615                   Logic.eq_rect_Type0_r __ (fun _ tERM4 h2984 _ _ ->
 616                     Logic.eq_rect_Type0_r h295 (fun _ tERM5 h2985 _ ->
 617                       Logic.streicherK (lazy (Ft_step (h290, h291, h292,
 618                         h295)))
 619                         (Logic.eq_rect_Type0_r (Wr_step (h290, h291, h292,
 620                           h293, h295, h297)) (fun h2986 -> h297) tERM5 h2985))
 621                       trace0 __ tERM4 h2984 __) __ __ tERM3 h2983 __) s'
 622                   trace __ __ tERM2 h2982 __) tr __ __ tERM1 h2981 __))) s __
 623           __ __ tERM0 h2980 __) d tERM h298 __)
 624       (fun h304 h305 h306 h307 _ h309 _ h311 h312 _ _ _ _ -> assert false
 625       (* absurd case *))
 626       (fun h318 h319 h320 h321 _ h323 _ h325 h326 _ _ _ _ -> assert false
 627       (* absurd case *)) (fun h332 h333 h334 _ h336 _ _ _ _ _ -> assert false
 628       (* absurd case *)))
 629 | Types.Inr _ ->
 630   (fun tERM ->
 631     will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace)))
 632       tERM (fun h343 h344 h345 h346 _ h348 _ h350 h351 _ _ _ _ ->
 633       Logic.eq_rect_Type0_r h346 (fun tERM0 h3510 _ ->
 634         Logic.eq_rect_Type0_r h343 (fun _ _ _ tERM1 h3511 _ ->
 635           Obj.magic flat_trace_jmdiscr ge h343 (lazy (Ft_step (h343, tr, s',
 636             trace))) (lazy (Ft_step (h343, h344, h345, h348))) __ (fun _ ->
 637             Logic.streicherK h343 (fun _ ->
 638               Logic.eq_rect_Type0_r h344 (fun _ _ tERM2 h3512 _ _ ->
 639                 Logic.eq_rect_Type0_r h345 (fun trace0 _ _ tERM3 h3513 _ _ ->
 640                   Logic.eq_rect_Type0_r __ (fun _ tERM4 h3514 _ _ ->
 641                     Logic.eq_rect_Type0_r h348 (fun _ tERM5 h3515 _ ->
 642                       Logic.streicherK (lazy (Ft_step (h343, h344, h345,
 643                         h348)))
 644                         (Logic.eq_rect_Type0_r (Wr_step (h343, h344, h345,
 645                           h346, h348, h350)) (fun h3516 -> h350) tERM5 h3515))
 646                       trace0 __ tERM4 h3514 __) __ __ tERM3 h3513 __) s'
 647                   trace __ __ tERM2 h3512 __) tr __ __ tERM1 h3511 __))) s __
 648           __ __ tERM0 h3510 __) d tERM h351 __)
 649       (fun h357 h358 h359 h360 _ h362 _ h364 h365 _ _ _ _ -> assert false
 650       (* absurd case *))
 651       (fun h371 h372 h373 h374 _ h376 _ h378 h379 _ _ _ _ -> assert false
 652       (* absurd case *)) (fun h385 h386 h387 _ h389 _ _ _ _ _ -> assert false
 653       (* absurd case *)))
 654
 655 (** val will_return_prepend :
 656     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
 657     IO.io_in) flat_trace -> will_return -> Nat.nat -> RTLabs_semantics.state
 658     -> (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return **)
 659 let will_return_prepend ge d1 s1 tr1 t1 d2 s2 t2 x =
 660   will_return_rect_Type0 ge (fun s tr s' depth _ t _ t0 iH d3 s3 t3 t4 _ ->
 661     Wr_step (s, tr, s', (Nat.plus depth (Nat.S d3)), t, (iH d3 s3 t3 t4 __)))
 662     (fun s tr s' depth _ t _ t0 iH d3 s3 t3 t4 _ -> Wr_call (s, tr, s',
 663     (Nat.plus depth (Nat.S d3)), t, (iH d3 s3 t3 t4 __)))
 664     (fun s tr s' depth _ t _ t0 iH s3 s20 t3 t4 _ -> Wr_ret (s, tr, s',
 665     (Nat.plus depth (Nat.S s3)), t, (iH s3 s20 t3 t4 __)))
 666     (fun s tr s' _ t _ d3 s3 t3 t4 _ ->
 667     Obj.magic Types.dPair_discr { Types.dpi1 = s'; Types.dpi2 = t }
 668       { Types.dpi1 = s3; Types.dpi2 = t3 } __ (fun _ ->
 669       Logic.eq_rect_Type0_r s3 (fun _ t0 _ _ ->
 670         Logic.eq_rect_Type0_r t3 (fun _ ->
 671           Logic.streicherK { Types.dpi1 = s3; Types.dpi2 = t3 } (Wr_ret (s,
 672             tr, s3, d3, t3, t4))) t0 __) s' __ t __)) d1 s1 tr1 t1 d2 s2 t2 x
 673     __
 674
 675 (** val nat_jmdiscr : Nat.nat -> Nat.nat -> __ **)
 676 let nat_jmdiscr x y =
 677   Logic.eq_rect_Type2 x
 678     (match x with
 679      | Nat.O -> Obj.magic (fun _ dH -> dH)
 680      | Nat.S a0 -> Obj.magic (fun _ dH -> dH __)) y
 681
 682 (** val will_return_remove_call :
 683     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
 684     IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return ->
 685     RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return **)
 686 let will_return_remove_call ge d1x s1x t1x t1 d2 x s2 t2 =
 687   will_return_rect_Type0 ge (fun s tr s' d1 _ t _ t0 iH d3 t3 s3 t4 _ ->
 688     iH d3
 689       (will_return_inv_rect_Type0 ge (Nat.plus d1 (Nat.S d3)) s
 690         (lazy (Ft_step (s, tr, s', t))) t3
 691         (fun h1 h2 h3 h4 _ h6 _ h8 h9 _ _ _ _ ->
 692         Logic.eq_rect_Type0 (Nat.plus d1 (Nat.S d3)) (fun h80 h90 _ ->
 693           Logic.eq_rect_Type0_r h1 (fun _ _ t20 _ _ h91 _ ->
 694             Obj.magic flat_trace_jmdiscr ge h1 (lazy (Ft_step (h1, tr, s',
 695               t))) (lazy (Ft_step (h1, h2, h3, h6))) __ (fun _ ->
 696               Logic.streicherK h1 (fun _ ->
 697                 Logic.eq_rect_Type0_r h2 (fun _ t21 _ _ h92 _ _ ->
 698                   Logic.eq_rect_Type0_r h3
 699                     (fun t5 t6 iH0 _ t22 _ _ h93 _ _ ->
 700                     Logic.eq_rect_Type0_r __ (fun t23 _ _ h94 _ _ ->
 701                       Logic.eq_rect_Type0_r h6 (fun t7 iH1 t24 _ _ h95 _ ->
 702                         Logic.streicherK (lazy (Ft_step (h1, h2, h3, h6)))
 703                           (Logic.eq_rect_Type0_r (Wr_step (h1, h2, h3,
 704                             (Nat.plus d1 (Nat.S d3)), h6, h80)) (fun h96 ->
 705                             h80) t24 h95)) t5 t6 iH0 t23 __ __ h94 __) __ t22
 706                       __ __ h93 __) s' t t0 iH __ t21 __ __ h92 __) tr __ t20
 707                   __ __ h91 __))) s __ __ t3 __ __ h90 __) h4 h8 h9 __)
 708         (fun h15 h16 h17 h18 _ h20 _ h22 h23 _ _ _ _ -> assert false
 709         (* absurd case *)) (fun h29 h30 h31 h32 _ h34 _ h36 h37 _ _ _ _ ->
 710         assert false (* absurd case *)) (fun h43 h44 h45 _ h47 _ _ _ _ _ ->
 711         assert false (* absurd case *))) s3 t4 __)
 712     (fun s tr s' d1 _ t _ t0 iH d3 t3 s3 t4 _ ->
 713     iH d3
 714       (will_return_inv_rect_Type0 ge (Nat.plus d1 (Nat.S d3)) s
 715         (lazy (Ft_step (s, tr, s', t))) t3
 716         (fun h1 h2 h3 h4 _ h6 _ h8 h9 _ _ _ _ -> assert false
 717         (* absurd case *)) (fun h15 h16 h17 h18 _ h20 _ h22 h23 _ _ _ _ ->
 718         Logic.eq_rect_Type0 (Nat.plus d1 (Nat.S d3)) (fun h220 h230 _ ->
 719           Logic.eq_rect_Type0_r h15 (fun _ _ t20 _ _ h231 _ ->
 720             Obj.magic flat_trace_jmdiscr ge h15 (lazy (Ft_step (h15, tr, s',
 721               t))) (lazy (Ft_step (h15, h16, h17, h20))) __ (fun _ ->
 722               Logic.streicherK h15 (fun _ ->
 723                 Logic.eq_rect_Type0_r h16 (fun _ t21 _ _ h232 _ _ ->
 724                   Logic.eq_rect_Type0_r h17
 725                     (fun t5 t6 iH0 _ t22 _ _ h233 _ _ ->
 726                     Logic.eq_rect_Type0_r __ (fun t23 _ _ h234 _ _ ->
 727                       Logic.eq_rect_Type0_r h20 (fun t7 iH1 t24 _ _ h235 _ ->
 728                         Logic.streicherK (lazy (Ft_step (h15, h16, h17,
 729                           h20)))
 730                           (Logic.eq_rect_Type0_r (Wr_call (h15, h16, h17,
 731                             (Nat.plus d1 (Nat.S d3)), h20, h220))
 732                             (fun h236 -> h220) t24 h235)) t5 t6 iH0 t23 __ __
 733                         h234 __) __ t22 __ __ h233 __) s' t t0 iH __ t21 __
 734                     __ h232 __) tr __ t20 __ __ h231 __))) s __ __ t3 __ __
 735             h230 __) h18 h22 h23 __)
 736         (fun h29 h30 h31 h32 _ h34 _ h36 h37 _ _ _ _ -> assert false
 737         (* absurd case *)) (fun h43 h44 h45 _ h47 _ _ _ _ _ -> assert false
 738         (* absurd case *))) s3 t4 __)
 739     (fun s tr s' d1 _ t _ t0 iH d3 t3 s3 t4 _ ->
 740     iH d3
 741       (will_return_inv_rect_Type0 ge (Nat.plus (Nat.S d1) (Nat.S d3)) s
 742         (lazy (Ft_step (s, tr, s', t))) t3
 743         (fun h1 h2 h3 h4 _ h6 _ h8 h9 _ _ _ _ -> assert false
 744         (* absurd case *)) (fun h15 h16 h17 h18 _ h20 _ h22 h23 _ _ _ _ ->
 745         assert false (* absurd case *))
 746         (fun h29 h30 h31 h32 _ h34 _ h36 h37 _ _ _ _ ->
 747         Obj.magic nat_jmdiscr (Nat.S (Nat.plus d1 (Nat.S d3))) (Nat.S h32) __
 748           (Logic.eq_rect_Type0_r h29 (fun _ _ t20 _ h370 _ _ ->
 749             Obj.magic flat_trace_jmdiscr ge h29 (lazy (Ft_step (h29, tr, s',
 750               t))) (lazy (Ft_step (h29, h30, h31, h34))) __ (fun _ ->
 751               Logic.streicherK h29 (fun _ ->
 752                 Logic.eq_rect_Type0_r h30 (fun _ t21 _ h371 _ _ _ ->
 753                   Logic.eq_rect_Type0_r h31
 754                     (fun t5 t6 iH0 _ t22 _ h372 _ _ _ ->
 755                     Logic.eq_rect_Type0_r __ (fun t23 _ h373 _ _ _ ->
 756                       Logic.eq_rect_Type0_r h34 (fun t7 iH1 t24 _ h374 _ _ ->
 757                         Logic.streicherK (lazy (Ft_step (h29, h30, h31,
 758                           h34))) (fun _ ->
 759                           Logic.eq_rect_Type0 (Nat.plus d1 (Nat.S d3))
 760                             (fun h360 _ h375 _ ->
 761                             Logic.streicherK (Nat.S (Nat.plus d1 (Nat.S d3)))
 762                               (Logic.eq_rect_Type0_r (Wr_ret (h29, h30, h31,
 763                                 (Nat.plus d1 (Nat.S d3)), h34, h360))
 764                                 (fun h376 -> h360) t24 h375)) h32 h36 __ h374
 765                             __)) t5 t6 iH0 t23 __ h373 __ __) __ t22 __ h372
 766                       __ __) s' t t0 iH __ t21 __ h371 __ __) tr __ t20 __
 767                   h370 __ __))) s __ __ t3 __ h37 __ __))
 768         (fun h43 h44 h45 _ h47 _ _ _ _ _ -> assert false (* absurd case *)))
 769       s3 t4 __) (fun s tr s' _ t _ d3 t3 s3 t4 _ ->
 770     Obj.magic Types.dPair_discr { Types.dpi1 = s'; Types.dpi2 = t }
 771       { Types.dpi1 = s3; Types.dpi2 = t4 } __ (fun _ ->
 772       Logic.eq_rect_Type0_r s3 (fun _ t0 t20 _ _ ->
 773         Logic.eq_rect_Type0_r t4 (fun t21 _ ->
 774           Logic.streicherK { Types.dpi1 = s3; Types.dpi2 = t4 }
 775             (will_return_inv_rect_Type0 ge (Nat.plus Nat.O (Nat.S d3)) s
 776               (lazy (Ft_step (s, tr, s3, t4))) t21
 777               (fun h1 h2 h3 h4 _ h6 _ h8 h9 _ _ _ _ -> assert false
 778               (* absurd case *))
 779               (fun h15 h16 h17 h18 _ h20 _ h22 h23 _ _ _ _ -> assert false
 780               (* absurd case *))
 781               (fun h29 h30 h31 h32 _ h34 _ h36 h37 _ _ _ _ ->
 782               Obj.magic nat_jmdiscr (Nat.S d3) (Nat.S h32) __
 783                 (Logic.eq_rect_Type0_r h29 (fun _ _ t22 h370 _ _ ->
 784                   Obj.magic flat_trace_jmdiscr ge h29 (lazy (Ft_step (h29,
 785                     tr, s3, t4))) (lazy (Ft_step (h29, h30, h31, h34))) __
 786                     (fun _ ->
 787                     Logic.streicherK h29 (fun _ ->
 788                       Logic.eq_rect_Type0_r h30 (fun _ t23 h371 _ _ _ ->
 789                         Logic.eq_rect_Type0_r h31
 790                           (fun t24 _ t25 h372 _ _ _ ->
 791                           Logic.eq_rect_Type0_r __ (fun t26 h373 _ _ _ ->
 792                             Logic.eq_rect_Type0_r h34 (fun t27 h374 _ _ ->
 793                               Logic.streicherK (lazy (Ft_step (h29, h30, h31,
 794                                 h34))) (fun _ ->
 795                                 Logic.eq_rect_Type0_r h32
 796                                   (fun _ t28 h375 _ ->
 797                                   Logic.streicherK (Nat.S h32)
 798                                     (Logic.eq_rect_Type0_r (Wr_ret (h29, h30,
 799                                       h31, h32, h34, h36)) (fun h376 -> h36)
 800                                       t28 h375)) d3 __ t27 h374 __)) t24 t26
 801                               h373 __ __) __ t25 h372 __ __) s3 t4 __ t23
 802                           h371 __ __) tr __ t22 h370 __ __))) s __ __ t21 h37
 803                   __ __)) (fun h43 h44 h45 _ h47 _ _ _ _ _ -> assert false
 804               (* absurd case *)))) t0 t20 __) s' __ t t3 __)) d1x s1x t1x t1
 805     d2 x s2 t2 __
 806
 807 (** val will_return_lower :
 808     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
 809     IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return **)
 810 let will_return_lower ge d0 s0 t0 tM d' =
 811   will_return_rect_Type0 ge (fun s tr s' d _ tr0 _ tM1 iH d'0 _ -> Wr_step
 812     (s, tr, s', d'0, tr0, (iH d'0 __)))
 813     (fun s tr s' d _ tr0 _ tM1 iH d'0 _ -> Wr_call (s, tr, s', d'0, tr0,
 814     (iH (Nat.S d'0) __))) (fun s tr s' d _ tr0 _ tM1 iH clearme ->
 815     match clearme with
 816     | Nat.O -> (fun _ -> Wr_base (s, tr, s', tr0))
 817     | Nat.S d'0 -> (fun _ -> Wr_ret (s, tr, s', d'0, tr0, (iH d'0 __))))
 818     (fun s tr s' _ tr0 _ clearme ->
 819     match clearme with
 820     | Nat.O -> (fun _ -> Wr_base (s, tr, s', tr0))
 821     | Nat.S d'0 -> (fun _ -> assert false (* absurd case *))) d0 s0 t0 tM d'
 822     __
 823
 824 (** val list_jmdiscr : 'a1 List.list -> 'a1 List.list -> __ **)
 825 let list_jmdiscr x y =
 826   Logic.eq_rect_Type2 x
 827     (match x with
 828      | List.Nil -> Obj.magic (fun _ dH -> dH)
 829      | List.Cons (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 830
 831 type 't trace_result = { new_state : RTLabs_abstract.rTLabs_ext_state;
 832                          remainder : (IO.io_out, IO.io_in) flat_trace;
 833                          new_trace : 't; terminates : __ }
 834
 835 (** val trace_result_rect_Type4 :
 836     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
 837     -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
 838     -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
 839     (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
 840     trace_result -> 'a2 **)
 841 let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_2020 =
 842   let { new_state = new_state0; remainder = remainder0; new_trace =
 843     new_trace0; terminates = terminates0 } = x_2020
 844   in
 845   h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
 846
 847 (** val trace_result_rect_Type5 :
 848     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
 849     -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
 850     -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
 851     (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
 852     trace_result -> 'a2 **)
 853 let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_2022 =
 854   let { new_state = new_state0; remainder = remainder0; new_trace =
 855     new_trace0; terminates = terminates0 } = x_2022
 856   in
 857   h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
 858
 859 (** val trace_result_rect_Type3 :
 860     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
 861     -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
 862     -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
 863     (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
 864     trace_result -> 'a2 **)
 865 let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_2024 =
 866   let { new_state = new_state0; remainder = remainder0; new_trace =
 867     new_trace0; terminates = terminates0 } = x_2024
 868   in
 869   h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
 870
 871 (** val trace_result_rect_Type2 :
 872     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
 873     -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
 874     -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
 875     (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
 876     trace_result -> 'a2 **)
 877 let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_2026 =
 878   let { new_state = new_state0; remainder = remainder0; new_trace =
 879     new_trace0; terminates = terminates0 } = x_2026
 880   in
 881   h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
 882
 883 (** val trace_result_rect_Type1 :
 884     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
 885     -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
 886     -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
 887     (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
 888     trace_result -> 'a2 **)
 889 let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_2028 =
 890   let { new_state = new_state0; remainder = remainder0; new_trace =
 891     new_trace0; terminates = terminates0 } = x_2028
 892   in
 893   h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
 894
 895 (** val trace_result_rect_Type0 :
 896     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
 897     -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
 898     -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
 899     (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
 900     trace_result -> 'a2 **)
 901 let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_2030 =
 902   let { new_state = new_state0; remainder = remainder0; new_trace =
 903     new_trace0; terminates = terminates0 } = x_2030
 904   in
 905   h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
 906
 907 (** val new_state :
 908     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
 909     -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
 910     -> will_return -> Nat.nat -> 'a1 trace_result ->
 911     RTLabs_abstract.rTLabs_ext_state **)
 912 let rec new_state ge depth ends start full original_terminates limit xxx =
 913   xxx.new_state
 914
 915 (** val remainder :
 916     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
 917     -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
 918     -> will_return -> Nat.nat -> 'a1 trace_result -> (IO.io_out, IO.io_in)
 919     flat_trace **)
 920 let rec remainder ge depth ends start full original_terminates limit xxx =
 921   xxx.remainder
 922
 923 (** val new_trace :
 924     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
 925     -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
 926     -> will_return -> Nat.nat -> 'a1 trace_result -> 'a1 **)
 927 let rec new_trace ge depth ends start full original_terminates limit xxx =
 928   xxx.new_trace
 929
 930 (** val terminates :
 931     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
 932     -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
 933     -> will_return -> Nat.nat -> 'a1 trace_result -> __ **)
 934 let rec terminates ge depth ends start full original_terminates limit xxx =
 935   xxx.terminates
 936
 937 (** val trace_result_inv_rect_Type4 :
 938     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
 939     -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
 940     -> will_return -> Nat.nat -> 'a1 trace_result ->
 941     (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 942     __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **)
 943 let trace_result_inv_rect_Type4 x1 x2 x3 x4 x5 x6 x8 hterm h1 =
 944   let hcut = trace_result_rect_Type4 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __
 945
 946 (** val trace_result_inv_rect_Type3 :
 947     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
 948     -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
 949     -> will_return -> Nat.nat -> 'a1 trace_result ->
 950     (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 951     __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **)
 952 let trace_result_inv_rect_Type3 x1 x2 x3 x4 x5 x6 x8 hterm h1 =
 953   let hcut = trace_result_rect_Type3 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __
 954
 955 (** val trace_result_inv_rect_Type2 :
 956     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
 957     -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
 958     -> will_return -> Nat.nat -> 'a1 trace_result ->
 959     (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 960     __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **)
 961 let trace_result_inv_rect_Type2 x1 x2 x3 x4 x5 x6 x8 hterm h1 =
 962   let hcut = trace_result_rect_Type2 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __
 963
 964 (** val trace_result_inv_rect_Type1 :
 965     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
 966     -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
 967     -> will_return -> Nat.nat -> 'a1 trace_result ->
 968     (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 969     __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **)
 970 let trace_result_inv_rect_Type1 x1 x2 x3 x4 x5 x6 x8 hterm h1 =
 971   let hcut = trace_result_rect_Type1 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __
 972
 973 (** val trace_result_inv_rect_Type0 :
 974     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
 975     -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
 976     -> will_return -> Nat.nat -> 'a1 trace_result ->
 977     (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 978     __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **)
 979 let trace_result_inv_rect_Type0 x1 x2 x3 x4 x5 x6 x8 hterm h1 =
 980   let hcut = trace_result_rect_Type0 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __
 981
 982 (** val trace_result_jmdiscr :
 983     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
 984     -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
 985     -> will_return -> Nat.nat -> 'a1 trace_result -> 'a1 trace_result -> __ **)
 986 let trace_result_jmdiscr a1 a2 a3 a4 a5 a6 a8 x y =
 987   Logic.eq_rect_Type2 x
 988     (let { new_state = a0; remainder = a10; new_trace = a30; terminates =
 989        a50 } = x
 990      in
 991     Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
 992
 993 type 't sub_trace_result = { ends : StructuredTraces.trace_ends_with_ret;
 994                              trace_res : 't trace_result }
 995
 996 (** val sub_trace_result_rect_Type4 :
 997     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 998     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
 999     (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1000     sub_trace_result -> 'a2 **)
1001 let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_2048 =
1002   let { ends = ends0; trace_res = trace_res0 } = x_2048 in
1003   h_mk_sub_trace_result ends0 trace_res0
1004
1005 (** val sub_trace_result_rect_Type5 :
1006     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1007     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1008     (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1009     sub_trace_result -> 'a2 **)
1010 let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_2050 =
1011   let { ends = ends0; trace_res = trace_res0 } = x_2050 in
1012   h_mk_sub_trace_result ends0 trace_res0
1013
1014 (** val sub_trace_result_rect_Type3 :
1015     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1016     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1017     (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1018     sub_trace_result -> 'a2 **)
1019 let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_2052 =
1020   let { ends = ends0; trace_res = trace_res0 } = x_2052 in
1021   h_mk_sub_trace_result ends0 trace_res0
1022
1023 (** val sub_trace_result_rect_Type2 :
1024     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1025     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1026     (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1027     sub_trace_result -> 'a2 **)
1028 let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_2054 =
1029   let { ends = ends0; trace_res = trace_res0 } = x_2054 in
1030   h_mk_sub_trace_result ends0 trace_res0
1031
1032 (** val sub_trace_result_rect_Type1 :
1033     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1034     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1035     (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1036     sub_trace_result -> 'a2 **)
1037 let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_2056 =
1038   let { ends = ends0; trace_res = trace_res0 } = x_2056 in
1039   h_mk_sub_trace_result ends0 trace_res0
1040
1041 (** val sub_trace_result_rect_Type0 :
1042     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1043     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1044     (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1045     sub_trace_result -> 'a2 **)
1046 let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_2058 =
1047   let { ends = ends0; trace_res = trace_res0 } = x_2058 in
1048   h_mk_sub_trace_result ends0 trace_res0
1049
1050 (** val ends :
1051     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1052     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1053     sub_trace_result -> StructuredTraces.trace_ends_with_ret **)
1054 let rec ends ge depth start full original_terminates limit xxx =
1055   xxx.ends
1056
1057 (** val trace_res :
1058     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1059     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1060     sub_trace_result -> 'a1 trace_result **)
1061 let rec trace_res ge depth start full original_terminates limit xxx =
1062   xxx.trace_res
1063
1064 (** val sub_trace_result_inv_rect_Type4 :
1065     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1066     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1067     sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
1068     trace_result -> __ -> 'a2) -> 'a2 **)
1069 let sub_trace_result_inv_rect_Type4 x1 x2 x3 x4 x5 x7 hterm h1 =
1070   let hcut = sub_trace_result_rect_Type4 x1 x2 x3 x4 x5 x7 h1 hterm in
1071   hcut __
1072
1073 (** val sub_trace_result_inv_rect_Type3 :
1074     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1075     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1076     sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
1077     trace_result -> __ -> 'a2) -> 'a2 **)
1078 let sub_trace_result_inv_rect_Type3 x1 x2 x3 x4 x5 x7 hterm h1 =
1079   let hcut = sub_trace_result_rect_Type3 x1 x2 x3 x4 x5 x7 h1 hterm in
1080   hcut __
1081
1082 (** val sub_trace_result_inv_rect_Type2 :
1083     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1084     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1085     sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
1086     trace_result -> __ -> 'a2) -> 'a2 **)
1087 let sub_trace_result_inv_rect_Type2 x1 x2 x3 x4 x5 x7 hterm h1 =
1088   let hcut = sub_trace_result_rect_Type2 x1 x2 x3 x4 x5 x7 h1 hterm in
1089   hcut __
1090
1091 (** val sub_trace_result_inv_rect_Type1 :
1092     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1093     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1094     sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
1095     trace_result -> __ -> 'a2) -> 'a2 **)
1096 let sub_trace_result_inv_rect_Type1 x1 x2 x3 x4 x5 x7 hterm h1 =
1097   let hcut = sub_trace_result_rect_Type1 x1 x2 x3 x4 x5 x7 h1 hterm in
1098   hcut __
1099
1100 (** val sub_trace_result_inv_rect_Type0 :
1101     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1102     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1103     sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
1104     trace_result -> __ -> 'a2) -> 'a2 **)
1105 let sub_trace_result_inv_rect_Type0 x1 x2 x3 x4 x5 x7 hterm h1 =
1106   let hcut = sub_trace_result_rect_Type0 x1 x2 x3 x4 x5 x7 h1 hterm in
1107   hcut __
1108
1109 (** val sub_trace_result_discr :
1110     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1111     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1112     sub_trace_result -> 'a1 sub_trace_result -> __ **)
1113 let sub_trace_result_discr a1 a2 a3 a4 a5 a7 x y =
1114   Logic.eq_rect_Type2 x
1115     (let { ends = a0; trace_res = a10 } = x in
1116     Obj.magic (fun _ dH -> dH __ __)) y
1117
1118 (** val sub_trace_result_jmdiscr :
1119     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1120     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1121     sub_trace_result -> 'a1 sub_trace_result -> __ **)
1122 let sub_trace_result_jmdiscr a1 a2 a3 a4 a5 a7 x y =
1123   Logic.eq_rect_Type2 x
1124     (let { ends = a0; trace_res = a10 } = x in
1125     Obj.magic (fun _ dH -> dH __ __)) y
1126
1127 (** val replace_trace :
1128     RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
1129     -> RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state
1130     -> (IO.io_out, IO.io_in) flat_trace -> (IO.io_out, IO.io_in) flat_trace
1131     -> will_return -> will_return -> Nat.nat -> Nat.nat -> 'a1 trace_result
1132     -> 'a2 -> 'a2 trace_result **)
1133 let replace_trace ge d e s1 s2 t1 t2 tM1 tM2 l1 l2 r trace =
1134   { new_state = r.new_state; remainder = r.remainder; new_trace = trace;
1135     terminates =
1136     ((match e with
1137       | StructuredTraces.Ends_with_ret ->
1138         Logic.eq_rect_Type0
1139           (will_return_end ge d s1.RTLabs_abstract.ras_state t1 tM1)
1140           (fun clearme ->
1141           let { new_state = x; remainder = x0; new_trace = x1; terminates =
1142             x2 } = clearme
1143           in
1144           (match d with
1145            | Nat.O -> Obj.magic __
1146            | Nat.S d' ->
1147              (fun tM10 tM20 ns rem _ t1NS _ clearme0 ->
1148                let tMa = Obj.magic clearme0 in Obj.magic tMa)) tM1 tM2 x x0
1149             __ x1 __ x2)
1150           (will_return_end ge d s2.RTLabs_abstract.ras_state t2 tM2)
1151       | StructuredTraces.Doesnt_end_with_ret ->
1152         Logic.eq_rect_Type0
1153           (will_return_end ge d s1.RTLabs_abstract.ras_state t1 tM1)
1154           (fun clearme ->
1155           let { new_state = ns; remainder = rem; new_trace = t1NS;
1156             terminates = clearme0 } = clearme
1157           in
1158           let tMa = Obj.magic clearme0 in Obj.magic tMa)
1159           (will_return_end ge d s2.RTLabs_abstract.ras_state t2 tM2)) r) }
1160
1161 (** val replace_sub_trace :
1162     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1163     RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
1164     (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return -> Nat.nat
1165     -> Nat.nat -> 'a1 sub_trace_result -> 'a2 -> 'a2 sub_trace_result **)
1166 let replace_sub_trace ge d s1 s2 t1 t2 tM1 tM2 l1 l2 r trace =
1167   { ends = r.ends; trace_res =
1168     (replace_trace ge d r.ends s1 s2 t1 t2 tM1 tM2 l1 l2 r.trace_res trace) }
1169
1170 (** val make_label_return :
1171     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1172     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1173     StructuredTraces.trace_label_return trace_result **)
1174 let rec make_label_return ge depth s trace tERMINATES tIME =
1175   (match tIME with
1176    | Nat.O -> (fun _ -> assert false (* absurd case *))
1177    | Nat.S tIME0 ->
1178      (fun _ ->
1179        let r = make_label_label ge depth s trace tERMINATES tIME0 in
1180        (match r.ends with
1181         | StructuredTraces.Ends_with_ret ->
1182           (fun r0 ->
1183             replace_trace ge depth StructuredTraces.Ends_with_ret s s trace
1184               trace tERMINATES tERMINATES
1185               (will_return_length ge depth s.RTLabs_abstract.ras_state trace
1186                 tERMINATES)
1187               (will_return_length ge depth s.RTLabs_abstract.ras_state trace
1188                 tERMINATES) r0 (StructuredTraces.Tlr_base ((Obj.magic s),
1189               (Obj.magic r0.new_state), r0.new_trace)))
1190         | StructuredTraces.Doesnt_end_with_ret ->
1191           (fun r0 ->
1192             let r' =
1193               make_label_return ge depth r0.new_state r0.remainder
1194                 (Types.pi1 (Obj.magic r0.terminates)) tIME0
1195             in
1196             replace_trace ge depth StructuredTraces.Ends_with_ret
1197               r0.new_state s r0.remainder trace
1198               (Types.pi1 (Obj.magic r0.terminates)) tERMINATES
1199               (will_return_length ge depth
1200                 r0.new_state.RTLabs_abstract.ras_state r0.remainder
1201                 (Types.pi1 (Obj.magic r0.terminates)))
1202               (will_return_length ge depth s.RTLabs_abstract.ras_state trace
1203                 tERMINATES) r' (StructuredTraces.Tlr_step ((Obj.magic s),
1204               (Obj.magic r0.new_state), (Obj.magic r'.new_state),
1205               r0.new_trace, r'.new_trace)))) r.trace_res)) __
1206 (** val make_label_label :
1207     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1208     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1209     StructuredTraces.trace_label_label sub_trace_result **)
1210 and make_label_label ge depth s trace tERMINATES tIME =
1211   (match tIME with
1212    | Nat.O -> (fun _ -> assert false (* absurd case *))
1213    | Nat.S tIME0 ->
1214      (fun _ ->
1215        let r = make_any_label ge depth s trace tERMINATES tIME0 in
1216        replace_sub_trace ge depth s s trace trace tERMINATES tERMINATES
1217          (will_return_length ge depth s.RTLabs_abstract.ras_state trace
1218            tERMINATES)
1219          (will_return_length ge depth s.RTLabs_abstract.ras_state trace
1220            tERMINATES) r (StructuredTraces.Tll_base (r.ends, (Obj.magic s),
1221          (Obj.magic r.trace_res.new_state), r.trace_res.new_trace)))) __
1222 (** val make_any_label :
1223     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1224     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1225     StructuredTraces.trace_any_label sub_trace_result **)
1226 and make_any_label ge depth s0 trace tERMINATES tIME =
1227   (match tIME with
1228    | Nat.O -> (fun _ -> assert false (* absurd case *))
1229    | Nat.S tIME0 ->
1230      (fun _ ->
1231        (let { RTLabs_abstract.ras_state = s; RTLabs_abstract.ras_fn_stack =
1232           stk } = s0
1233         in
1234        (fun trace0 _ tM _ ->
1235        (match Lazy.force
1236         trace0 with
1237         | Ft_stop st ->
1238           (fun _ _ tERMINATES0 _ -> assert false (* absurd case *))
1239         | Ft_step (start, tr, next, trace') ->
1240           (fun _ _ tERMINATES0 _ ->
1241             let start' = { RTLabs_abstract.ras_state = start;
1242               RTLabs_abstract.ras_fn_stack = stk }
1243             in
1244             let next' = RTLabs_abstract.next_state ge start' next tr in
1245             (match RTLabs_abstract.rTLabs_classify start with
1246              | StructuredTraces.Cl_return ->
1247                (fun _ -> { ends = StructuredTraces.Ends_with_ret; trace_res =
1248                  { new_state = next'; remainder = trace'; new_trace =
1249                  (StructuredTraces.Tal_base_return ((Obj.magic start'),
1250                  (Obj.magic next'))); terminates =
1251                  (will_return_return ge depth start tr next trace'
1252                    tERMINATES0) } })
1253              | StructuredTraces.Cl_jump ->
1254                (fun _ -> { ends = StructuredTraces.Doesnt_end_with_ret;
1255                  trace_res = { new_state = next'; remainder = trace';
1256                  new_trace = (StructuredTraces.Tal_base_not_return
1257                  ((Obj.magic start'), (Obj.magic next'))); terminates =
1258                  (Obj.magic
1259                    (will_return_notfn ge depth start tr next trace'
1260                      (Types.Inr __) tERMINATES0)) } })
1261              | StructuredTraces.Cl_call ->
1262                (fun _ ->
1263                  let r =
1264                    make_label_return ge (Nat.S depth) next' trace'
1265                      (Types.pi1
1266                        (will_return_call ge depth start tr next trace'
1267                          tERMINATES0)) tIME0
1268                  in
1269                  (match RTLabs_abstract.rTLabs_cost
1270                           r.new_state.RTLabs_abstract.ras_state with
1271                   | Bool.True ->
1272                     (fun _ -> { ends = StructuredTraces.Doesnt_end_with_ret;
1273                       trace_res = { new_state = r.new_state; remainder =
1274                       r.remainder; new_trace =
1275                       (StructuredTraces.Tal_base_call ((Obj.magic start'),
1276                       (Obj.magic next'), (Obj.magic r.new_state),
1277                       r.new_trace)); terminates =
1278                       (let tMr = Obj.magic r.terminates in Obj.magic tMr) } })
1279                   | Bool.False ->
1280                     (fun _ ->
1281                       let r' =
1282                         make_any_label ge depth r.new_state r.remainder
1283                           (Types.pi1 (Obj.magic r.terminates)) tIME0
1284                       in
1285                       replace_sub_trace ge depth r.new_state start'
1286                         r.remainder (lazy (Ft_step (start, tr, next,
1287                         trace'))) (Types.pi1 (Obj.magic r.terminates))
1288                         tERMINATES0
1289                         (will_return_length ge depth
1290                           r.new_state.RTLabs_abstract.ras_state r.remainder
1291                           (Types.pi1 (Obj.magic r.terminates)))
1292                         (will_return_length ge depth start (lazy (Ft_step
1293                           (start, tr, next, trace'))) tERMINATES0) r'
1294                         (StructuredTraces.Tal_step_call (r'.ends,
1295                         (Obj.magic start'), (Obj.magic next'),
1296                         (Obj.magic r.new_state),
1297                         (Obj.magic r'.trace_res.new_state), r.new_trace,
1298                         r'.trace_res.new_trace)))) __)
1299              | StructuredTraces.Cl_tailcall ->
1300                (fun _ -> assert false (* absurd case *))
1301              | StructuredTraces.Cl_other ->
1302                (fun _ ->
1303                  (match RTLabs_abstract.rTLabs_cost next with
1304                   | Bool.True ->
1305                     (fun _ -> { ends = StructuredTraces.Doesnt_end_with_ret;
1306                       trace_res = { new_state = next'; remainder = trace';
1307                       new_trace = (StructuredTraces.Tal_base_not_return
1308                       ((Obj.magic start'), (Obj.magic next'))); terminates =
1309                       (Obj.magic
1310                         (will_return_notfn ge depth start tr next trace'
1311                           (Types.Inl __) tERMINATES0)) } })
1312                   | Bool.False ->
1313                     (fun _ ->
1314                       let r =
1315                         make_any_label ge depth next' trace'
1316                           (Types.pi1
1317                             (will_return_notfn ge depth start tr next trace'
1318                               (Types.Inl __) tERMINATES0)) tIME0
1319                       in
1320                       replace_sub_trace ge depth next' start' trace'
1321                         (lazy (Ft_step (start, tr, next, trace')))
1322                         (Types.pi1
1323                           (will_return_notfn ge depth start tr next trace'
1324                             (Types.Inl __) tERMINATES0)) tERMINATES0
1325                         (will_return_length ge depth
1326                           next'.RTLabs_abstract.ras_state trace'
1327                           (Types.pi1
1328                             (will_return_notfn ge depth start tr next trace'
1329                               (Types.Inl __) tERMINATES0)))
1330                         (will_return_length ge depth start (lazy (Ft_step
1331                           (start, tr, next, trace'))) tERMINATES0) r
1332                         (StructuredTraces.Tal_step_default (r.ends,
1333                         (Obj.magic start'), (Obj.magic next'),
1334                         (Obj.magic r.trace_res.new_state),
1335                         r.trace_res.new_trace)))) __)) __)) __ __ tM __))
1336          trace __ tERMINATES __)) __
1337
1338 (** val make_label_return' :
1339     RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1340     (IO.io_out, IO.io_in) flat_trace -> will_return ->
1341     StructuredTraces.trace_label_return trace_result **)
1342 let rec make_label_return' ge depth s trace tERMINATES =
1343   make_label_return ge depth s trace tERMINATES
1344     (Nat.plus (Nat.S (Nat.S Nat.O))
1345       (Nat.times (Nat.S (Nat.S (Nat.S Nat.O)))
1346         (will_return_length ge depth s.RTLabs_abstract.ras_state trace
1347           tERMINATES)))
1348
1349 (** val actual_successor :
1350     RTLabs_semantics.state -> Graphs.label Types.option **)
1351 let actual_successor = function
1352 | RTLabs_semantics.State (f, fs, m) -> Types.Some f.RTLabs_semantics.next
1353 | RTLabs_semantics.Callstate (x, x0, x1, x2, fs, x3) ->
1354   (match fs with
1355    | List.Nil -> Types.None
1356    | List.Cons (f, x4) -> Types.Some f.RTLabs_semantics.next)
1357 | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Types.None
1358 | RTLabs_semantics.Finalstate x -> Types.None
1359
1360 (** val steps_for_statement : RTLabs_syntax.statement -> Nat.nat **)
1361 let steps_for_statement s =
1362   Nat.S
1363     (match s with
1364      | RTLabs_syntax.St_skip x -> Nat.O
1365      | RTLabs_syntax.St_cost (x, x0) -> Nat.O
1366      | RTLabs_syntax.St_const (x, x0, x1, x2) -> Nat.O
1367      | RTLabs_syntax.St_op1 (x, x0, x1, x2, x3, x4) -> Nat.O
1368      | RTLabs_syntax.St_op2 (x, x0, x1, x2, x3, x4, x5, x6) -> Nat.O
1369      | RTLabs_syntax.St_load (x, x0, x1, x2) -> Nat.O
1370      | RTLabs_syntax.St_store (x, x0, x1, x2) -> Nat.O
1371      | RTLabs_syntax.St_call_id (x, x0, x1, x2) -> Nat.S Nat.O
1372      | RTLabs_syntax.St_call_ptr (x, x0, x1, x2) -> Nat.S Nat.O
1373      | RTLabs_syntax.St_cond (x, x0, x1) -> Nat.O
1374      | RTLabs_syntax.St_return -> Nat.S Nat.O)
1375
1376 type remainder_ok =
1377 | Mk_remainder_ok
1378
1379 (** val remainder_ok_rect_Type4 :
1380     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1381     IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1382     'a1 **)
1383 let rec remainder_ok_rect_Type4 ge s t h_mk_remainder_ok = function
1384 | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1385
1386 (** val remainder_ok_rect_Type5 :
1387     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1388     IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1389     'a1 **)
1390 let rec remainder_ok_rect_Type5 ge s t h_mk_remainder_ok = function
1391 | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1392
1393 (** val remainder_ok_rect_Type3 :
1394     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1395     IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1396     'a1 **)
1397 let rec remainder_ok_rect_Type3 ge s t h_mk_remainder_ok = function
1398 | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1399
1400 (** val remainder_ok_rect_Type2 :
1401     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1402     IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1403     'a1 **)
1404 let rec remainder_ok_rect_Type2 ge s t h_mk_remainder_ok = function
1405 | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1406
1407 (** val remainder_ok_rect_Type1 :
1408     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1409     IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1410     'a1 **)
1411 let rec remainder_ok_rect_Type1 ge s t h_mk_remainder_ok = function
1412 | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1413
1414 (** val remainder_ok_rect_Type0 :
1415     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1416     IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1417     'a1 **)
1418 let rec remainder_ok_rect_Type0 ge s t h_mk_remainder_ok = function
1419 | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1420
1421 (** val remainder_ok_inv_rect_Type4 :
1422     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1423     IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ ->
1424     'a1) -> 'a1 **)
1425 let remainder_ok_inv_rect_Type4 x1 x2 x3 hterm h1 =
1426   let hcut = remainder_ok_rect_Type4 x1 x2 x3 h1 hterm in hcut __
1427
1428 (** val remainder_ok_inv_rect_Type3 :
1429     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1430     IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ ->
1431     'a1) -> 'a1 **)
1432 let remainder_ok_inv_rect_Type3 x1 x2 x3 hterm h1 =
1433   let hcut = remainder_ok_rect_Type3 x1 x2 x3 h1 hterm in hcut __
1434
1435 (** val remainder_ok_inv_rect_Type2 :
1436     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1437     IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ ->
1438     'a1) -> 'a1 **)
1439 let remainder_ok_inv_rect_Type2 x1 x2 x3 hterm h1 =
1440   let hcut = remainder_ok_rect_Type2 x1 x2 x3 h1 hterm in hcut __
1441
1442 (** val remainder_ok_inv_rect_Type1 :
1443     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1444     IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ ->
1445     'a1) -> 'a1 **)
1446 let remainder_ok_inv_rect_Type1 x1 x2 x3 hterm h1 =
1447   let hcut = remainder_ok_rect_Type1 x1 x2 x3 h1 hterm in hcut __
1448
1449 (** val remainder_ok_inv_rect_Type0 :
1450     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1451     IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ ->
1452     'a1) -> 'a1 **)
1453 let remainder_ok_inv_rect_Type0 x1 x2 x3 hterm h1 =
1454   let hcut = remainder_ok_rect_Type0 x1 x2 x3 h1 hterm in hcut __
1455
1456 (** val remainder_ok_discr :
1457     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1458     IO.io_in) flat_trace -> remainder_ok -> remainder_ok -> __ **)
1459 let remainder_ok_discr a1 a2 a3 x y =
1460   Logic.eq_rect_Type2 x
1461     (let Mk_remainder_ok = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
1462
1463 (** val remainder_ok_jmdiscr :
1464     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1465     IO.io_in) flat_trace -> remainder_ok -> remainder_ok -> __ **)
1466 let remainder_ok_jmdiscr a1 a2 a3 x y =
1467   Logic.eq_rect_Type2 x
1468     (let Mk_remainder_ok = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
1469
1470 (** val init_state_is :
1471     RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state ->
1472     (Pointers.block, __) Types.dPair **)
1473 let init_state_is p s =
1474   RTLabs_semantics.bind_ok (Globalenvs.init_mem (fun x -> x) p) (fun x ->
1475     let main = p.AST.prog_main in
1476     Obj.magic
1477       (Monad.m_bind0 (Monad.max_def Errors.res0)
1478         (Obj.magic
1479           (Errors.opt_to_res (List.Cons ((Errors.MSG
1480             ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
1481             (PreIdentifiers.SymbolTag, main)), List.Nil))))
1482             (Globalenvs.find_symbol (RTLabs_semantics.make_global p) main)))
1483         (fun b ->
1484         Monad.m_bind0 (Monad.max_def Errors.res0)
1485           (Obj.magic
1486             (Errors.opt_to_res (List.Cons ((Errors.MSG
1487               ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
1488               (PreIdentifiers.SymbolTag, main)), List.Nil))))
1489               (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global p) b)))
1490           (fun f ->
1491           Obj.magic (Errors.OK (RTLabs_semantics.Callstate (main, f,
1492             List.Nil, Types.None, List.Nil, x))))))) s (fun m _ _ ->
1493     RTLabs_semantics.bind_ok
1494       (Errors.opt_to_res (List.Cons ((Errors.MSG
1495         ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
1496         (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil))))
1497         (Globalenvs.find_symbol (RTLabs_semantics.make_global p)
1498           p.AST.prog_main)) (fun x ->
1499       Obj.magic
1500         (Monad.m_bind0 (Monad.max_def Errors.res0)
1501           (Obj.magic
1502             (Errors.opt_to_res (List.Cons ((Errors.MSG
1503               ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
1504               (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil))))
1505               (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global p) x)))
1506           (fun f ->
1507           Obj.magic (Errors.OK (RTLabs_semantics.Callstate (p.AST.prog_main,
1508             f, List.Nil, Types.None, List.Nil, m)))))) s (fun b _ _ ->
1509       RTLabs_semantics.bind_ok
1510         (Errors.opt_to_res (List.Cons ((Errors.MSG
1511           ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
1512           (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil))))
1513           (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global p) b))
1514         (fun x -> Errors.OK (RTLabs_semantics.Callstate (p.AST.prog_main, x,
1515         List.Nil, Types.None, List.Nil, m))) s (fun f _ _ ->
1516         Obj.magic Errors.res_discr (Errors.OK (RTLabs_semantics.Callstate
1517           (p.AST.prog_main, f, List.Nil, Types.None, List.Nil, m)))
1518           (Errors.OK s) __ (fun _ ->
1519           Logic.eq_rect_Type0 (RTLabs_semantics.Callstate (p.AST.prog_main,
1520             f, List.Nil, Types.None, List.Nil, m)) (fun _ ->
1521             Logic.streicherK (Errors.OK (RTLabs_semantics.Callstate
1522               (p.AST.prog_main, f, List.Nil, Types.None, List.Nil, m)))
1523               { Types.dpi1 = b; Types.dpi2 = __ }) s __))))
1524
1525 (** val ras_state_initial :
1526     RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state ->
1527     RTLabs_abstract.rTLabs_ext_state **)
1528 let ras_state_initial p s =
1529   { RTLabs_abstract.ras_state = s; RTLabs_abstract.ras_fn_stack = (List.Cons
1530     ((init_state_is p s).Types.dpi1, List.Nil)) }
1531
1532 (** val deprop_execute :
1533     RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1534     -> Events.trace Types.sig0 **)
1535 let rec deprop_execute ge s s' =
1536   (match RTLabs_semantics.eval_statement ge s with
1537    | IOMonad.Interact (x, x0) -> (fun _ -> assert false (* absurd case *))
1538    | IOMonad.Value ts -> (fun _ -> ts.Types.fst)
1539    | IOMonad.Wrong x -> (fun _ -> assert false (* absurd case *))) __
1540
1541 (** val deprop_as_execute :
1542     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1543     RTLabs_abstract.rTLabs_ext_state -> Events.trace Types.sig0 **)
1544 let rec deprop_as_execute ge s s' =
1545   deprop_execute ge s.RTLabs_abstract.ras_state s'.RTLabs_abstract.ras_state
1546
1547 type ('o, 'i) partial_flat_trace =
1548 | Pft_base of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
1549 | Pft_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
1550    * RTLabs_semantics.state * ('o, 'i) partial_flat_trace
1551
1552 (** val partial_flat_trace_rect_Type4 :
1553     RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
1554     RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
1555     Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
1556     ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
1557     RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
1558 let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_2393 x_2392 = function
1559 | Pft_base (s, tr, s') -> h_pft_base s tr s' __
1560 | Pft_step (s, tr, s', s'', x_2396) ->
1561   h_pft_step s tr s' s'' __ x_2396
1562     (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_2396)
1563
1564 (** val partial_flat_trace_rect_Type3 :
1565     RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
1566     RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
1567     Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
1568     ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
1569     RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
1570 let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_2409 x_2408 = function
1571 | Pft_base (s, tr, s') -> h_pft_base s tr s' __
1572 | Pft_step (s, tr, s', s'', x_2412) ->
1573   h_pft_step s tr s' s'' __ x_2412
1574     (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_2412)
1575
1576 (** val partial_flat_trace_rect_Type2 :
1577     RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
1578     RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
1579     Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
1580     ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
1581     RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
1582 let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_2417 x_2416 = function
1583 | Pft_base (s, tr, s') -> h_pft_base s tr s' __
1584 | Pft_step (s, tr, s', s'', x_2420) ->
1585   h_pft_step s tr s' s'' __ x_2420
1586     (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_2420)
1587
1588 (** val partial_flat_trace_rect_Type1 :
1589     RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
1590     RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
1591     Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
1592     ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
1593     RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
1594 let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_2425 x_2424 = function
1595 | Pft_base (s, tr, s') -> h_pft_base s tr s' __
1596 | Pft_step (s, tr, s', s'', x_2428) ->
1597   h_pft_step s tr s' s'' __ x_2428
1598     (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_2428)
1599
1600 (** val partial_flat_trace_rect_Type0 :
1601     RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
1602     RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
1603     Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
1604     ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
1605     RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
1606 let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_2433 x_2432 = function
1607 | Pft_base (s, tr, s') -> h_pft_base s tr s' __
1608 | Pft_step (s, tr, s', s'', x_2436) ->
1609   h_pft_step s tr s' s'' __ x_2436
1610     (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_2436)
1611
1612 (** val partial_flat_trace_inv_rect_Type4 :
1613     RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1614     -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
1615     Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
1616     (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
1617     RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
1618     __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
1619 let partial_flat_trace_inv_rect_Type4 x3 x4 x5 hterm h1 h2 =
1620   let hcut = partial_flat_trace_rect_Type4 x3 h1 h2 x4 x5 hterm in
1621   hcut __ __ __
1622
1623 (** val partial_flat_trace_inv_rect_Type3 :
1624     RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1625     -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
1626     Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
1627     (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
1628     RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
1629     __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
1630 let partial_flat_trace_inv_rect_Type3 x3 x4 x5 hterm h1 h2 =
1631   let hcut = partial_flat_trace_rect_Type3 x3 h1 h2 x4 x5 hterm in
1632   hcut __ __ __
1633
1634 (** val partial_flat_trace_inv_rect_Type2 :
1635     RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1636     -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
1637     Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
1638     (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
1639     RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
1640     __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
1641 let partial_flat_trace_inv_rect_Type2 x3 x4 x5 hterm h1 h2 =
1642   let hcut = partial_flat_trace_rect_Type2 x3 h1 h2 x4 x5 hterm in
1643   hcut __ __ __
1644
1645 (** val partial_flat_trace_inv_rect_Type1 :
1646     RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1647     -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
1648     Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
1649     (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
1650     RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
1651     __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
1652 let partial_flat_trace_inv_rect_Type1 x3 x4 x5 hterm h1 h2 =
1653   let hcut = partial_flat_trace_rect_Type1 x3 h1 h2 x4 x5 hterm in
1654   hcut __ __ __
1655
1656 (** val partial_flat_trace_inv_rect_Type0 :
1657     RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1658     -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
1659     Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
1660     (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
1661     RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
1662     __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
1663 let partial_flat_trace_inv_rect_Type0 x3 x4 x5 hterm h1 h2 =
1664   let hcut = partial_flat_trace_rect_Type0 x3 h1 h2 x4 x5 hterm in
1665   hcut __ __ __
1666
1667 (** val partial_flat_trace_jmdiscr :
1668     RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1669     -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) partial_flat_trace -> __ **)
1670 let partial_flat_trace_jmdiscr a3 a4 a5 x y =
1671   Logic.eq_rect_Type2 x
1672     (match x with
1673      | Pft_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1674      | Pft_step (a0, a10, a20, a30, a50) ->
1675        Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1676
1677 (** val append_partial_flat_trace :
1678     RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1679     -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2)
1680     partial_flat_trace -> ('a1, 'a2) partial_flat_trace **)
1681 let rec append_partial_flat_trace ge s1 s2 s3 = function
1682 | Pft_base (s, tr, s') -> (fun x -> Pft_step (s, tr, s', s3, x))
1683 | Pft_step (s, tr, s', s'', tr') ->
1684   (fun tr2 -> Pft_step (s, tr, s', s3,
1685     (append_partial_flat_trace ge s' s'' s3 tr' tr2)))
1686
1687 (** val partial_to_flat_trace :
1688     RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1689     -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) flat_trace -> ('a1, 'a2)
1690     flat_trace **)
1691 let rec partial_to_flat_trace ge s1 s2 = function
1692 | Pft_base (s, tr0, s') -> (fun x -> lazy (Ft_step (s, tr0, s', x)))
1693 | Pft_step (s, tr0, s', s'', tr') ->
1694   (fun tr'' -> lazy (Ft_step (s, tr0, s',
1695     (partial_to_flat_trace ge s' s'' tr' tr''))))
1696
1697 (** val flat_trace_of_label_return :
1698     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1699     RTLabs_abstract.rTLabs_ext_state -> StructuredTraces.trace_label_return
1700     -> (IO.io_out, IO.io_in) partial_flat_trace **)
1701 let rec flat_trace_of_label_return ge s s' = function
1702 | StructuredTraces.Tlr_base (s1, s2, tll) ->
1703   flat_trace_of_label_label ge StructuredTraces.Ends_with_ret (Obj.magic s1)
1704     (Obj.magic s2) tll
1705 | StructuredTraces.Tlr_step (s1, s2, s3, tll, tlr) ->
1706   append_partial_flat_trace ge (Obj.magic s1).RTLabs_abstract.ras_state
1707     (Obj.magic s2).RTLabs_abstract.ras_state
1708     (Obj.magic s3).RTLabs_abstract.ras_state
1709     (flat_trace_of_label_label ge StructuredTraces.Doesnt_end_with_ret
1710       (Obj.magic s1) (Obj.magic s2) tll)
1711     (flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic s3) tlr)
1712 (** val flat_trace_of_label_label :
1713     RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
1714     RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
1715     StructuredTraces.trace_label_label -> (IO.io_out, IO.io_in)
1716     partial_flat_trace **)
1717 and flat_trace_of_label_label ge ends0 s s' = function
1718 | StructuredTraces.Tll_base (e, s1, s2, tal) ->
1719   flat_trace_of_any_label ge e (Obj.magic s1) (Obj.magic s2) tal
1720 (** val flat_trace_of_any_label :
1721     RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
1722     RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
1723     StructuredTraces.trace_any_label -> (IO.io_out, IO.io_in)
1724     partial_flat_trace **)
1725 and flat_trace_of_any_label ge ends0 s s' = function
1726 | StructuredTraces.Tal_base_not_return (s1, s2) ->
1727   let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1728   Pft_base ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1729   (Obj.magic s2).RTLabs_abstract.ras_state)
1730 | StructuredTraces.Tal_base_return (s1, s2) ->
1731   let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1732   Pft_base ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1733   (Obj.magic s2).RTLabs_abstract.ras_state)
1734 | StructuredTraces.Tal_base_call (s1, s2, s3, tlr) ->
1735   let suffix' =
1736     flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic s3) tlr
1737   in
1738   let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1739   Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1740   (Obj.magic s2).RTLabs_abstract.ras_state,
1741   (Obj.magic s3).RTLabs_abstract.ras_state, suffix')
1742 | StructuredTraces.Tal_base_tailcall (s1, s2, s3, tlr) ->
1743   assert false (* absurd case *)
1744 | StructuredTraces.Tal_step_call (ends1, s1, s2, s3, s4, tlr, tal) ->
1745   let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1746   Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1747   (Obj.magic s2).RTLabs_abstract.ras_state,
1748   (Obj.magic s4).RTLabs_abstract.ras_state,
1749   (append_partial_flat_trace ge (Obj.magic s2).RTLabs_abstract.ras_state
1750     (Obj.magic s3).RTLabs_abstract.ras_state
1751     (Obj.magic s4).RTLabs_abstract.ras_state
1752     (flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic s3) tlr)
1753     (flat_trace_of_any_label ge ends1 (Obj.magic s3) (Obj.magic s4) tal)))
1754 | StructuredTraces.Tal_step_default (ends1, s1, s2, s3, tal) ->
1755   let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1756   Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1757   (Obj.magic s2).RTLabs_abstract.ras_state,
1758   (Obj.magic s3).RTLabs_abstract.ras_state,
1759   (flat_trace_of_any_label ge ends1 (Obj.magic s2) (Obj.magic s3) tal))
1760
1761 (** val flat_trace_of_any_call :
1762     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1763     RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
1764     Events.trace -> StructuredTraces.trace_any_call -> (IO.io_out, IO.io_in)
1765     partial_flat_trace **)
1766 let rec flat_trace_of_any_call ge s s' s'' et tr =
1767   (match tr with
1768    | StructuredTraces.Tac_base s1 ->
1769      (fun _ -> Pft_base ((Obj.magic s1).RTLabs_abstract.ras_state, et,
1770        s''.RTLabs_abstract.ras_state))
1771    | StructuredTraces.Tac_step_call (s1, s2, s3, s4, tlr, tac) ->
1772      (fun _ ->
1773        let et0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s4) in
1774        Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, et0,
1775        (Obj.magic s4).RTLabs_abstract.ras_state,
1776        s''.RTLabs_abstract.ras_state,
1777        (append_partial_flat_trace ge (Obj.magic s4).RTLabs_abstract.ras_state
1778          (Obj.magic s2).RTLabs_abstract.ras_state
1779          s''.RTLabs_abstract.ras_state
1780          (flat_trace_of_label_return ge (Obj.magic s4) (Obj.magic s2) tlr)
1781          (flat_trace_of_any_call ge (Obj.magic s2) (Obj.magic s3) s'' et tac))))
1782    | StructuredTraces.Tac_step_default (s1, s2, s3, tal) ->
1783      (fun _ ->
1784        let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s3) in
1785        Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1786        (Obj.magic s3).RTLabs_abstract.ras_state,
1787        s''.RTLabs_abstract.ras_state,
1788        (flat_trace_of_any_call ge (Obj.magic s3) (Obj.magic s2) s'' et tal))))
1789     __
1790
1791 (** val flat_trace_of_label_call :
1792     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1793     RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
1794     Events.trace -> StructuredTraces.trace_label_call -> (IO.io_out,
1795     IO.io_in) partial_flat_trace **)
1796 let rec flat_trace_of_label_call ge s s' s'' et tr =
1797   (let StructuredTraces.Tlc_base (s1, s2, tac) = tr in
1798   (fun _ ->
1799   flat_trace_of_any_call ge (Obj.magic s1) (Obj.magic s2) s'' et tac)) __
1800
1801 (** val flat_trace_of_label_diverges :
1802     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1803     StructuredTraces.trace_label_diverges -> (IO.io_out, IO.io_in) flat_trace **)
1804 let rec flat_trace_of_label_diverges ge s tr =
1805   match Lazy.force
1806   tr with
1807   | StructuredTraces.Tld_step (sx, sy, tll, tld) ->
1808     (let { RTLabs_abstract.ras_state = sy'; RTLabs_abstract.ras_fn_stack =
1809        stk } = Obj.magic sy
1810      in
1811     (fun tll0 ->
1812     (match flat_trace_of_label_label ge StructuredTraces.Doesnt_end_with_ret
1813              (Obj.magic sx) { RTLabs_abstract.ras_state = sy';
1814              RTLabs_abstract.ras_fn_stack = stk } tll0 with
1815      | Pft_base (s1, tr0, s2) ->
1816        (fun _ tld0 -> lazy (Ft_step (s1, tr0, s2,
1817          (flat_trace_of_label_diverges ge { RTLabs_abstract.ras_state = s2;
1818            RTLabs_abstract.ras_fn_stack = stk } tld0))))
1819      | Pft_step (s1, et, s2, s3, tr') ->
1820        (fun _ tld0 -> lazy (Ft_step (s1, et, s2,
1821          (add_partial_flat_trace ge s2 { RTLabs_abstract.ras_state = s3;
1822            RTLabs_abstract.ras_fn_stack = stk } tr' tld0))))) __)) tll tld
1823   | StructuredTraces.Tld_base (s1, s2, s3, tlc, tld) ->
1824     (let { RTLabs_abstract.ras_state = s3'; RTLabs_abstract.ras_fn_stack =
1825        stk } = Obj.magic s3
1826      in
1827     (fun _ ->
1828     let tr0 =
1829       deprop_as_execute ge (Obj.magic s2) { RTLabs_abstract.ras_state = s3';
1830         RTLabs_abstract.ras_fn_stack = stk }
1831     in
1832     (match flat_trace_of_label_call ge (Obj.magic s1) (Obj.magic s2)
1833              { RTLabs_abstract.ras_state = s3';
1834              RTLabs_abstract.ras_fn_stack = stk } tr0 tlc with
1835      | Pft_base (s10, tr1, s20) ->
1836        (fun _ tld0 -> lazy (Ft_step (s10, tr1, s20,
1837          (flat_trace_of_label_diverges ge { RTLabs_abstract.ras_state = s20;
1838            RTLabs_abstract.ras_fn_stack = stk } tld0))))
1839      | Pft_step (s10, et, s20, s30, tr') ->
1840        (fun _ tld0 -> lazy (Ft_step (s10, et, s20,
1841          (add_partial_flat_trace ge s20 { RTLabs_abstract.ras_state = s30;
1842            RTLabs_abstract.ras_fn_stack = stk } tr' tld0))))) __)) __ tld
1843 (** val add_partial_flat_trace :
1844     RTLabs_semantics.genv -> RTLabs_semantics.state ->
1845     RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in)
1846     partial_flat_trace -> StructuredTraces.trace_label_diverges ->
1847     (IO.io_out, IO.io_in) flat_trace **)
1848 and add_partial_flat_trace ge s s' =
1849   let { RTLabs_abstract.ras_state = sx; RTLabs_abstract.ras_fn_stack =
1850     stk } = s'
1851   in
1852   (fun ptr ->
1853   (match ptr with
1854    | Pft_base (s0, tr, s'0) ->
1855      (fun _ tr0 -> lazy (Ft_step (s0, tr, s'0,
1856        (flat_trace_of_label_diverges ge { RTLabs_abstract.ras_state = s'0;
1857          RTLabs_abstract.ras_fn_stack = stk } tr0))))
1858    | Pft_step (s1, et, s2, s3, tr') ->
1859      (fun _ tr -> lazy (Ft_step (s1, et, s2,
1860        (add_partial_flat_trace ge s2 { RTLabs_abstract.ras_state = s3;
1861          RTLabs_abstract.ras_fn_stack = stk } tr' tr))))) __)
1862
1863 (** val flat_trace_of_whole_program :
1864     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1865     StructuredTraces.trace_whole_program -> (IO.io_out, IO.io_in) flat_trace **)
1866 let rec flat_trace_of_whole_program ge s = function
1867 | StructuredTraces.Twp_terminating (s1, s2, sf, tlr) ->
1868   let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1869   lazy (Ft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1870   (Obj.magic s2).RTLabs_abstract.ras_state,
1871   (partial_to_flat_trace ge (Obj.magic s2).RTLabs_abstract.ras_state
1872     (Obj.magic sf).RTLabs_abstract.ras_state
1873     (flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic sf) tlr)
1874     (lazy (Ft_stop (Obj.magic sf).RTLabs_abstract.ras_state)))))
1875 | StructuredTraces.Twp_diverges (s1, s2, tld) ->
1876   let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1877   lazy (Ft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1878   (Obj.magic s2).RTLabs_abstract.ras_state,
1879   (flat_trace_of_label_diverges ge (Obj.magic s2) tld)))
1880
1881 (** val state_fn :
1882     RTLabs_semantics.genv -> __ -> Pointers.block Types.option **)
1883 let state_fn ge s =
1884   match (Obj.magic s).RTLabs_abstract.ras_fn_stack with
1885   | List.Nil -> Types.None
1886   | List.Cons (h, t) ->
1887     (match (Obj.magic s).RTLabs_abstract.ras_state with
1888      | RTLabs_semantics.State (x, x0, x1) -> Types.Some h
1889      | RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) ->
1890        (match t with
1891         | List.Nil -> Types.None
1892         | List.Cons (h', x5) -> Types.Some h')
1893      | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Types.Some h
1894      | RTLabs_semantics.Finalstate x -> Types.Some h)
1895
1896 (** val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __ **)
1897 let option_jmdiscr x y =
1898   Logic.eq_rect_Type2 x
1899     (match x with
1900      | Types.None -> Obj.magic (fun _ dH -> dH)
1901      | Types.Some a0 -> Obj.magic (fun _ dH -> dH __)) y
1902