open Preamble

open CostLabel

open Proper

open PositiveMap

open Deqsets

open Extralib

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Extranat

open Vector

open FoldStuff

open BitVector

open Z

open BitVectorZ

open Pointers

open ErrorMessages

open Option

open Setoids

open Monad

open Positive

open PreIdentifiers

open Errors

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Coqlib

open Values

open Events

open FrontEndVal

open Hide

open ByteValues

open GenMem

open FrontEndMem

open IOMonad

open IO

open Extra_bool

open Globalenvs

open SmallstepExec

open FrontEndOps

open Cminor_syntax

type env = Values.val0 Identifiers.identifier_map

type genv = Cminor_syntax.internal_function AST.fundef Globalenvs.genv_t

type cont =
| Kend
| Kseq of Cminor_syntax.stmt * cont
| Kblock of cont

(** val cont_rect_Type4 :
    'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
    -> cont -> 'a1 **)
let rec cont_rect_Type4 h_Kend h_Kseq h_Kblock = function
| Kend -> h_Kend
| Kseq (x_23729, x_23728) ->
  h_Kseq x_23729 x_23728 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_23728)
| Kblock x_23730 ->
  h_Kblock x_23730 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_23730)

(** val cont_rect_Type3 :
    'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
    -> cont -> 'a1 **)
let rec cont_rect_Type3 h_Kend h_Kseq h_Kblock = function
| Kend -> h_Kend
| Kseq (x_23743, x_23742) ->
  h_Kseq x_23743 x_23742 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_23742)
| Kblock x_23744 ->
  h_Kblock x_23744 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_23744)

(** val cont_rect_Type2 :
    'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
    -> cont -> 'a1 **)
let rec cont_rect_Type2 h_Kend h_Kseq h_Kblock = function
| Kend -> h_Kend
| Kseq (x_23750, x_23749) ->
  h_Kseq x_23750 x_23749 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_23749)
| Kblock x_23751 ->
  h_Kblock x_23751 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_23751)

(** val cont_rect_Type1 :
    'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
    -> cont -> 'a1 **)
let rec cont_rect_Type1 h_Kend h_Kseq h_Kblock = function
| Kend -> h_Kend
| Kseq (x_23757, x_23756) ->
  h_Kseq x_23757 x_23756 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_23756)
| Kblock x_23758 ->
  h_Kblock x_23758 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_23758)

(** val cont_rect_Type0 :
    'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
    -> cont -> 'a1 **)
let rec cont_rect_Type0 h_Kend h_Kseq h_Kblock = function
| Kend -> h_Kend
| Kseq (x_23764, x_23763) ->
  h_Kseq x_23764 x_23763 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_23763)
| Kblock x_23765 ->
  h_Kblock x_23765 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_23765)

(** val cont_inv_rect_Type4 :
    cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
    -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let cont_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = cont_rect_Type4 h1 h2 h3 hterm in hcut __

(** val cont_inv_rect_Type3 :
    cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
    -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let cont_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = cont_rect_Type3 h1 h2 h3 hterm in hcut __

(** val cont_inv_rect_Type2 :
    cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
    -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let cont_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = cont_rect_Type2 h1 h2 h3 hterm in hcut __

(** val cont_inv_rect_Type1 :
    cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
    -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let cont_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = cont_rect_Type1 h1 h2 h3 hterm in hcut __

(** val cont_inv_rect_Type0 :
    cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
    -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let cont_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = cont_rect_Type0 h1 h2 h3 hterm in hcut __

(** val cont_discr : cont -> cont -> __ **)
let cont_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Kend -> Obj.magic (fun _ dH -> dH)
     | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Kblock a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val cont_jmdiscr : cont -> cont -> __ **)
let cont_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Kend -> Obj.magic (fun _ dH -> dH)
     | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Kblock a0 -> Obj.magic (fun _ dH -> dH __)) y

type stack =
| SStop
| Scall of (AST.ident, AST.typ) Types.prod Types.option
   * Cminor_syntax.internal_function * Pointers.block * env * cont * 
   stack

(** val stack_rect_Type4 :
    'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
    cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
let rec stack_rect_Type4 h_SStop h_Scall = function
| SStop -> h_SStop
| Scall (dest, f, x_23824, en, k, x_23820) ->
  h_Scall dest f x_23824 en __ __ k __ x_23820
    (stack_rect_Type4 h_SStop h_Scall x_23820)

(** val stack_rect_Type3 :
    'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
    cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
let rec stack_rect_Type3 h_SStop h_Scall = function
| SStop -> h_SStop
| Scall (dest, f, x_23840, en, k, x_23836) ->
  h_Scall dest f x_23840 en __ __ k __ x_23836
    (stack_rect_Type3 h_SStop h_Scall x_23836)

(** val stack_rect_Type2 :
    'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
    cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
let rec stack_rect_Type2 h_SStop h_Scall = function
| SStop -> h_SStop
| Scall (dest, f, x_23848, en, k, x_23844) ->
  h_Scall dest f x_23848 en __ __ k __ x_23844
    (stack_rect_Type2 h_SStop h_Scall x_23844)

(** val stack_rect_Type1 :
    'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
    cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
let rec stack_rect_Type1 h_SStop h_Scall = function
| SStop -> h_SStop
| Scall (dest, f, x_23856, en, k, x_23852) ->
  h_Scall dest f x_23856 en __ __ k __ x_23852
    (stack_rect_Type1 h_SStop h_Scall x_23852)

(** val stack_rect_Type0 :
    'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
    cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
let rec stack_rect_Type0 h_SStop h_Scall = function
| SStop -> h_SStop
| Scall (dest, f, x_23864, en, k, x_23860) ->
  h_Scall dest f x_23864 en __ __ k __ x_23860
    (stack_rect_Type0 h_SStop h_Scall x_23860)

(** val stack_inv_rect_Type4 :
    stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
    cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let stack_inv_rect_Type4 hterm h1 h2 =
  let hcut = stack_rect_Type4 h1 h2 hterm in hcut __

(** val stack_inv_rect_Type3 :
    stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
    cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let stack_inv_rect_Type3 hterm h1 h2 =
  let hcut = stack_rect_Type3 h1 h2 hterm in hcut __

(** val stack_inv_rect_Type2 :
    stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
    cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let stack_inv_rect_Type2 hterm h1 h2 =
  let hcut = stack_rect_Type2 h1 h2 hterm in hcut __

(** val stack_inv_rect_Type1 :
    stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
    cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let stack_inv_rect_Type1 hterm h1 h2 =
  let hcut = stack_rect_Type1 h1 h2 hterm in hcut __

(** val stack_inv_rect_Type0 :
    stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
    cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let stack_inv_rect_Type0 hterm h1 h2 =
  let hcut = stack_rect_Type0 h1 h2 hterm in hcut __

(** val stack_jmdiscr : stack -> stack -> __ **)
let stack_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | SStop -> Obj.magic (fun _ dH -> dH)
     | Scall (a0, a1, a2, a3, a6, a8) ->
       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __)) y

type state =
| State of Cminor_syntax.internal_function * Cminor_syntax.stmt * env
   * GenMem.mem * Pointers.block * cont * stack
| Callstate of AST.ident * Cminor_syntax.internal_function AST.fundef
   * Values.val0 List.list * GenMem.mem * stack
| Returnstate of Values.val0 Types.option * GenMem.mem * stack
| Finalstate of Integers.int

(** val state_rect_Type4 :
    (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
    -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
    (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
    List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
    GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function
| State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
| Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
| Returnstate (v, m, st) -> h_Returnstate v m st
| Finalstate r -> h_Finalstate r

(** val state_rect_Type5 :
    (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
    -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
    (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
    List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
    GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function
| State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
| Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
| Returnstate (v, m, st) -> h_Returnstate v m st
| Finalstate r -> h_Finalstate r

(** val state_rect_Type3 :
    (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
    -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
    (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
    List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
    GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function
| State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
| Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
| Returnstate (v, m, st) -> h_Returnstate v m st
| Finalstate r -> h_Finalstate r

(** val state_rect_Type2 :
    (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
    -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
    (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
    List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
    GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function
| State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
| Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
| Returnstate (v, m, st) -> h_Returnstate v m st
| Finalstate r -> h_Finalstate r

(** val state_rect_Type1 :
    (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
    -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
    (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
    List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
    GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function
| State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
| Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
| Returnstate (v, m, st) -> h_Returnstate v m st
| Finalstate r -> h_Finalstate r

(** val state_rect_Type0 :
    (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
    -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
    (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
    List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
    GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function
| State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
| Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
| Returnstate (v, m, st) -> h_Returnstate v m st
| Finalstate r -> h_Finalstate r

(** val state_inv_rect_Type4 :
    state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
    __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
    'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
    Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
    (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
    (Integers.int -> __ -> 'a1) -> 'a1 **)
let state_inv_rect_Type4 hterm h1 h2 h3 h4 =
  let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __

(** val state_inv_rect_Type3 :
    state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
    __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
    'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
    Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
    (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
    (Integers.int -> __ -> 'a1) -> 'a1 **)
let state_inv_rect_Type3 hterm h1 h2 h3 h4 =
  let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __

(** val state_inv_rect_Type2 :
    state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
    __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
    'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
    Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
    (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
    (Integers.int -> __ -> 'a1) -> 'a1 **)
let state_inv_rect_Type2 hterm h1 h2 h3 h4 =
  let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __

(** val state_inv_rect_Type1 :
    state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
    __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
    'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
    Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
    (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
    (Integers.int -> __ -> 'a1) -> 'a1 **)
let state_inv_rect_Type1 hterm h1 h2 h3 h4 =
  let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __

(** val state_inv_rect_Type0 :
    state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
    __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
    'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
    Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
    (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
    (Integers.int -> __ -> 'a1) -> 'a1 **)
let state_inv_rect_Type0 hterm h1 h2 h3 h4 =
  let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __

(** val state_jmdiscr : state -> state -> __ **)
let state_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | State (a0, a1, a2, a5, a6, a7, a9) ->
       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)
     | Callstate (a0, a1, a2, a3, a4) ->
       Obj.magic (fun _ dH -> dH __ __ __ __ __)
     | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val eval_expr :
    genv -> AST.typ -> Cminor_syntax.expr -> env -> Pointers.block ->
    GenMem.mem -> (Events.trace, Values.val0) Types.prod Errors.res **)
let rec eval_expr ge ty0 e en sp m =
  (match e with
   | Cminor_syntax.Id (x, i) ->
     (fun _ ->
       let r = Identifiers.lookup_present PreIdentifiers.SymbolTag en i in
       Errors.OK { Types.fst = Events.e0; Types.snd = r })
   | Cminor_syntax.Cst (x, c) ->
     (fun _ ->
       Obj.magic
         (Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic
             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedConstant)
               (FrontEndOps.eval_constant x (Globalenvs.find_symbol ge) sp c)))
           (fun r ->
           Obj.magic (Errors.OK { Types.fst = Events.e0; Types.snd = r }))))
   | Cminor_syntax.Op1 (ty, ty', op, e') ->
     (fun _ ->
       Obj.magic
         (Monad.m_bind2 (Monad.max_def Errors.res0)
           (Obj.magic (eval_expr ge ty e' en sp m)) (fun tr v ->
           Monad.m_bind0 (Monad.max_def Errors.res0)
             (Obj.magic
               (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
                 (FrontEndOps.eval_unop ty ty' op v))) (fun r ->
             Obj.magic (Errors.OK { Types.fst = tr; Types.snd = r })))))
   | Cminor_syntax.Op2 (ty1, ty2, ty', op, e1, e2) ->
     (fun _ ->
       Obj.magic
         (Monad.m_bind2 (Monad.max_def Errors.res0)
           (Obj.magic (eval_expr ge ty1 e1 en sp m)) (fun tr1 v1 ->
           Monad.m_bind2 (Monad.max_def Errors.res0)
             (Obj.magic (eval_expr ge ty2 e2 en sp m)) (fun tr2 v2 ->
             Monad.m_bind0 (Monad.max_def Errors.res0)
               (Obj.magic
                 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
                   (FrontEndOps.eval_binop m ty1 ty2 ty' op v1 v2)))
               (fun r ->
               Obj.magic (Errors.OK { Types.fst = (Events.eapp tr1 tr2);
                 Types.snd = r }))))))
   | Cminor_syntax.Mem (ty, e0) ->
     (fun _ ->
       Obj.magic
         (Monad.m_bind2 (Monad.max_def Errors.res0)
           (Obj.magic (eval_expr ge AST.ASTptr e0 en sp m)) (fun tr v ->
           Monad.m_bind0 (Monad.max_def Errors.res0)
             (Obj.magic
               (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
                 (FrontEndMem.loadv ty m v))) (fun r ->
             Obj.magic (Errors.OK { Types.fst = tr; Types.snd = r })))))
   | Cminor_syntax.Cond (sz, sg, ty, e', e1, e2) ->
     (fun _ ->
       Obj.magic
         (Monad.m_bind2 (Monad.max_def Errors.res0)
           (Obj.magic (eval_expr ge (AST.ASTint (sz, sg)) e' en sp m))
           (fun tr v ->
           Monad.m_bind0 (Monad.max_def Errors.res0)
             (Obj.magic (Values.eval_bool_of_val v)) (fun b ->
             Monad.m_bind2 (Monad.max_def Errors.res0)
               (Obj.magic
                 (eval_expr ge ty
                   (match b with
                    | Bool.True -> e1
                    | Bool.False -> e2) en sp m)) (fun tr' r ->
               Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr');
                 Types.snd = r }))))))
   | Cminor_syntax.Ecost (ty, l, e') ->
     (fun _ ->
       Obj.magic
         (Monad.m_bind2 (Monad.max_def Errors.res0)
           (Obj.magic (eval_expr ge ty e' en sp m)) (fun tr r ->
           Obj.magic (Errors.OK { Types.fst =
             (Events.eapp (Events.echarge l) tr); Types.snd = r }))))) __

(** val k_exit :
    Nat.nat -> cont -> Cminor_syntax.internal_function -> env -> cont
    Types.sig0 Errors.res **)
let rec k_exit n k f en =
  (match k with
   | Kend -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.BadState))
   | Kseq (x, k') -> (fun _ -> k_exit n k' f en)
   | Kblock k' ->
     (fun _ ->
       match n with
       | Nat.O -> Errors.OK k'
       | Nat.S m -> k_exit m k' f en)) __

(** val find_case :
    AST.intsize -> AST.bvint -> (AST.bvint, 'a1) Types.prod List.list -> 'a1
    -> 'a1 **)
let rec find_case sz i cs default =
  match cs with
  | List.Nil -> default
  | List.Cons (h, t) ->
    let { Types.fst = hi; Types.snd = a } = h in
    (match BitVector.eq_bv (AST.bitsize_of_intsize sz) i hi with
     | Bool.True -> a
     | Bool.False -> find_case sz i t default)

(** val find_label :
    PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
    Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
    Types.prod Types.sig0 Types.option **)
let rec find_label l s k f en =
  (match s with
   | Cminor_syntax.St_skip -> (fun _ -> Types.None)
   | Cminor_syntax.St_assign (x, x0, x1) -> (fun _ -> Types.None)
   | Cminor_syntax.St_store (x, x0, x1) -> (fun _ -> Types.None)
   | Cminor_syntax.St_call (x, x0, x1) -> (fun _ -> Types.None)
   | Cminor_syntax.St_seq (s1, s2) ->
     (fun _ ->
       match find_label l s1 (Kseq (s2, k)) f en with
       | Types.None -> find_label l s2 k f en
       | Types.Some sk -> Types.Some sk)
   | Cminor_syntax.St_ifthenelse (x, x0, x1, s1, s2) ->
     (fun _ ->
       match find_label l s1 k f en with
       | Types.None -> find_label l s2 k f en
       | Types.Some sk -> Types.Some sk)
   | Cminor_syntax.St_return x -> (fun _ -> Types.None)
   | Cminor_syntax.St_label (l', s') ->
     (fun _ ->
       match Identifiers.identifier_eq PreIdentifiers.Label l l' with
       | Types.Inl _ -> Types.Some { Types.fst = s'; Types.snd = k }
       | Types.Inr _ -> find_label l s' k f en)
   | Cminor_syntax.St_goto x -> (fun _ -> Types.None)
   | Cminor_syntax.St_cost (x, s') -> (fun _ -> find_label l s' k f en)) __

(** val find_label_always :
    PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
    Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
    Types.prod Types.sig0 **)
let find_label_always l s k f en =
  (match find_label l s k f en with
   | Types.None -> (fun _ -> assert false (* absurd case *))
   | Types.Some sk -> (fun _ -> sk)) __

(** val bind_params :
    Values.val0 List.list -> (AST.ident, AST.typ) Types.prod List.list -> env
    Types.sig0 Errors.res **)
let rec bind_params vs ids =
  match vs with
  | List.Nil ->
    (match ids with
     | List.Nil -> Errors.OK (Identifiers.empty_map PreIdentifiers.SymbolTag)
     | List.Cons (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters))
  | List.Cons (v, vt) ->
    (match ids with
     | List.Nil ->
       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters)
     | List.Cons (idh, idt) ->
       let { Types.fst = id; Types.snd = ty } = idh in
       Obj.magic
         (Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (bind_params vt idt)) (fun en ->
           Obj.magic (Errors.OK
             (Identifiers.add PreIdentifiers.SymbolTag (Types.pi1 en)
               idh.Types.fst v)))))

(** val init_locals :
    env -> (AST.ident, AST.typ) Types.prod List.list -> env **)
let init_locals =
  List.foldr (fun idty en ->
    Identifiers.add PreIdentifiers.SymbolTag en idty.Types.fst Values.Vundef)

(** val trace_map_inv :
    ('a1 -> __ -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list
    -> (Events.trace, 'a2 List.list) Types.prod Errors.res **)
let rec trace_map_inv f l =
  (match l with
   | List.Nil ->
     (fun _ -> Errors.OK { Types.fst = Events.e0; Types.snd = List.Nil })
   | List.Cons (h, t) ->
     (fun _ ->
       Obj.magic
         (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic f h __)
           (fun tr h' ->
           Monad.m_bind2 (Monad.max_def Errors.res0)
             (Obj.magic (trace_map_inv f t)) (fun tr' t' ->
             Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr');
               Types.snd = (List.Cons (h', t')) })))))) __

(** val eval_step :
    genv -> state -> (IO.io_out, IO.io_in, (Events.trace, state) Types.prod)
    IOMonad.iO **)
let eval_step ge = function
| State (f, s, en, m, sp, k, st0) ->
  IOMonad.err_to_io
    ((match s with
      | Cminor_syntax.St_skip ->
        (fun _ ->
          (match k with
           | Kend ->
             (fun _ ->
               Obj.magic
                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                   Events.e0; Types.snd = (Returnstate (Types.None,
                   (GenMem.free m sp), st0)) }))
           | Kseq (s', k') ->
             (fun _ ->
               Obj.magic
                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                   Events.e0; Types.snd = (State (f, s', en, m, sp, k',
                   st0)) }))
           | Kblock k' ->
             (fun _ ->
               Obj.magic
                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                   Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip,
                   en, m, sp, k', st0)) }))) __)
      | Cminor_syntax.St_assign (x, id, e) ->
        (fun _ ->
          Obj.magic
            (Monad.m_bind2 (Monad.max_def Errors.res0)
              (Obj.magic (eval_expr ge x e en sp m)) (fun tr v ->
              let en' =
                Identifiers.update_present PreIdentifiers.SymbolTag en id v
              in
              Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
                Types.snd = (State (f, Cminor_syntax.St_skip, en', m, sp, k,
                st0)) })))
      | Cminor_syntax.St_store (ty, edst, e) ->
        (fun _ ->
          Obj.magic
            (Monad.m_bind2 (Monad.max_def Errors.res0)
              (Obj.magic (eval_expr ge AST.ASTptr edst en sp m))
              (fun tr vdst ->
              Monad.m_bind2 (Monad.max_def Errors.res0)
                (Obj.magic (eval_expr ge ty e en sp m)) (fun tr' v ->
                Monad.m_bind0 (Monad.max_def Errors.res0)
                  (Obj.magic
                    (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
                      (FrontEndMem.storev ty m vdst v))) (fun m' ->
                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                    (Events.eapp tr tr'); Types.snd = (State (f,
                    Cminor_syntax.St_skip, en, m', sp, k, st0)) })))))
      | Cminor_syntax.St_call (dst, ef, args) ->
        (fun _ ->
          Obj.magic
            (Monad.m_bind2 (Monad.max_def Errors.res0)
              (Obj.magic (eval_expr ge AST.ASTptr ef en sp m)) (fun tr vf ->
              Monad.m_bind2 (Monad.max_def Errors.res0)
                (Obj.magic
                  (Errors.opt_to_res
                    (Errors.msg ErrorMessages.BadFunctionValue)
                    (Globalenvs.find_funct_id ge vf))) (fun fd id ->
                Monad.m_bind2 (Monad.max_def Errors.res0)
                  (Obj.magic
                    (trace_map_inv (fun e ->
                      let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in
                      (fun _ -> eval_expr ge ty e0 en sp m)) args))
                  (fun tr' vargs ->
                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                    (Events.eapp tr tr'); Types.snd = (Callstate (id, fd,
                    vargs, m, (Scall (dst, f, sp, en, k, st0)))) })))))
      | Cminor_syntax.St_seq (s1, s2) ->
        (fun _ ->
          Obj.magic
            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
              Events.e0; Types.snd = (State (f, s1, en, m, sp, (Kseq (s2,
              k)), st0)) }))
      | Cminor_syntax.St_ifthenelse (x, x0, e, strue, sfalse) ->
        (fun _ ->
          Obj.magic
            (Monad.m_bind2 (Monad.max_def Errors.res0)
              (Obj.magic (eval_expr ge (AST.ASTint (x, x0)) e en sp m))
              (fun tr v ->
              Monad.m_bind0 (Monad.max_def Errors.res0)
                (Obj.magic (Values.eval_bool_of_val v)) (fun b ->
                Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
                  Types.snd = (State (f,
                  (match b with
                   | Bool.True -> strue
                   | Bool.False -> sfalse), en, m, sp, k, st0)) }))))
      | Cminor_syntax.St_return eo ->
        (match eo with
         | Types.None ->
           (fun _ ->
             Obj.magic
               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                 Events.e0; Types.snd = (Returnstate (Types.None,
                 (GenMem.free m sp), st0)) }))
         | Types.Some e ->
           let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in
           (fun _ ->
           Obj.magic
             (Monad.m_bind2 (Monad.max_def Errors.res0)
               (Obj.magic (eval_expr ge ty e0 en sp m)) (fun tr v ->
               Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
                 Types.snd = (Returnstate ((Types.Some v),
                 (GenMem.free m sp), st0)) }))))
      | Cminor_syntax.St_label (l, s') ->
        (fun _ ->
          Obj.magic
            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
              Events.e0; Types.snd = (State (f, s', en, m, sp, k, st0)) }))
      | Cminor_syntax.St_goto l ->
        (fun _ ->
          let sk = find_label_always l f.Cminor_syntax.f_body Kend f en in
          Obj.magic
            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
              Events.e0; Types.snd = (State (f, sk.Types.fst, en, m, sp,
              sk.Types.snd, st0)) }))
      | Cminor_syntax.St_cost (l, s') ->
        (fun _ ->
          Obj.magic
            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
              (Events.echarge l); Types.snd = (State (f, s', en, m, sp, k,
              st0)) }))) __)
| Callstate (x, fd, args, m, st0) ->
  (match fd with
   | AST.Internal f ->
     IOMonad.err_to_io
       (let { Types.fst = m'; Types.snd = sp } =
          GenMem.alloc m (Z.z_of_nat Nat.O)
            (Z.z_of_nat f.Cminor_syntax.f_stacksize)
        in
       Obj.magic
         (Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (bind_params args f.Cminor_syntax.f_params)) (fun en ->
           Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
             Events.e0; Types.snd = (State (f, f.Cminor_syntax.f_body,
             (init_locals (Types.pi1 en) f.Cminor_syntax.f_vars), m', sp,
             Kend, st0)) })))
   | AST.External fn ->
     Obj.magic
       (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
         (Obj.magic
           (IOMonad.err_to_io
             (IO.check_eventval_list args fn.AST.ef_sig.AST.sig_args)))
         (fun evargs ->
         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
           (Obj.magic
             (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig)))
           (fun evres ->
           let res =
             match fn.AST.ef_sig.AST.sig_res with
             | Types.None -> Types.None
             | Types.Some x0 ->
               Types.Some (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)
           in
           Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
             (Events.eextcall fn.AST.ef_id evargs
               (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));
             Types.snd = (Returnstate (res, m, st0)) }))))
| Returnstate (result, m, st0) ->
  IOMonad.err_to_io
    (match st0 with
     | SStop ->
       (match result with
        | Types.None ->
          Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
        | Types.Some v ->
          (match v with
           | Values.Vundef ->
             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
           | Values.Vint (sz, r) ->
             (match sz with
              | AST.I8 ->
                (fun x -> Errors.Error
                  (Errors.msg ErrorMessages.ReturnMismatch))
              | AST.I16 ->
                (fun x -> Errors.Error
                  (Errors.msg ErrorMessages.ReturnMismatch))
              | AST.I32 ->
                (fun r0 ->
                  Obj.magic
                    (Monad.m_return0 (Monad.max_def Errors.res0)
                      { Types.fst = Events.e0; Types.snd = (Finalstate r0) })))
               r
           | Values.Vnull ->
             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
           | Values.Vptr x ->
             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)))
     | Scall (dst, f, sp, en, k, st') ->
       (match result with
        | Types.None ->
          (match dst with
           | Types.None ->
             Obj.magic
               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                 Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip, en,
                 m, sp, k, st')) })
           | Types.Some x ->
             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))
        | Types.Some v ->
          (match dst with
           | Types.None ->
             (fun _ -> Errors.Error
               (Errors.msg ErrorMessages.ReturnMismatch))
           | Types.Some idty ->
             (fun _ ->
               Obj.magic
                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                   Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip,
                   (Identifiers.update_present PreIdentifiers.SymbolTag en
                     idty.Types.fst v), m, sp, k, st')) }))) __))
| Finalstate r ->
  IOMonad.err_to_io (Errors.Error (Errors.msg ErrorMessages.BadState))

(** val is_final : state -> Integers.int Types.option **)
let is_final = function
| State (x, x0, x1, x4, x5, x6, x8) -> Types.None
| Callstate (x, x0, x1, x2, x3) -> Types.None
| Returnstate (x, x0, x1) -> Types.None
| Finalstate r -> Types.Some r

(** val cminor_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
let cminor_exec =
  { SmallstepExec.is_final = (fun x -> Obj.magic is_final);
    SmallstepExec.step = (Obj.magic eval_step) }

(** val make_global : Cminor_syntax.cminor_program -> genv **)
let make_global p =
  Globalenvs.globalenv (fun x -> x) p

(** val make_initial_state :
    Cminor_syntax.cminor_program -> state Errors.res **)
let make_initial_state p =
  let ge = make_global p in
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (Globalenvs.init_mem (fun x -> x) p)) (fun m ->
      Monad.m_bind0 (Monad.max_def Errors.res0)
        (Obj.magic
          (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
            (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
        Monad.m_bind0 (Monad.max_def Errors.res0)
          (Obj.magic
            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
              (Globalenvs.find_funct_ptr ge b))) (fun f ->
          Obj.magic (Errors.OK (Callstate (p.AST.prog_main, f, List.Nil, m,
            SStop)))))))

(** val cminor_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
let cminor_fullexec =
  { SmallstepExec.es1 = cminor_exec; SmallstepExec.make_global =
    (Obj.magic make_global); SmallstepExec.make_initial_state =
    (Obj.magic make_initial_state) }

(** val make_noinit_global : Cminor_syntax.cminor_noinit_program -> genv **)
let make_noinit_global p =
  Globalenvs.globalenv (fun x -> List.Cons ((AST.Init_space x), List.Nil)) p

(** val make_initial_noinit_state :
    Cminor_syntax.cminor_noinit_program -> state Errors.res **)
let make_initial_noinit_state p =
  let ge = make_noinit_global p in
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic
        (Globalenvs.init_mem (fun x -> List.Cons ((AST.Init_space x),
          List.Nil)) p)) (fun m ->
      Monad.m_bind0 (Monad.max_def Errors.res0)
        (Obj.magic
          (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
            (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
        Monad.m_bind0 (Monad.max_def Errors.res0)
          (Obj.magic
            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
              (Globalenvs.find_funct_ptr ge b))) (fun f ->
          Obj.magic (Errors.OK (Callstate (p.AST.prog_main, f, List.Nil, m,
            SStop)))))))

(** val cminor_noinit_fullexec :
    (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
let cminor_noinit_fullexec =
  { SmallstepExec.es1 = cminor_exec; SmallstepExec.make_global =
    (Obj.magic make_noinit_global); SmallstepExec.make_initial_state =
    (Obj.magic make_initial_noinit_state) }