source: extracted/toCminor.ml @ 2717

open Preamble

open BitVectorTrie

open CostLabel

open Coqlib

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Setoids

open Monad

open Option

open Lists

open Positive

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open FoldStuff

open BitVector

open Extranat

open Bool

open Relations

open Nat

open Integers

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open AST

open Csyntax

open TypeComparison

open ClassifyOp

open Fresh

(** val gather_mem_vars_expr : Csyntax.expr -> Identifiers.identifier_set **)
let rec gather_mem_vars_expr = function
| Csyntax.Expr (ed, ty) ->
  (match ed with
   | Csyntax.Econst_int (x, x0) ->
     Identifiers.empty_set PreIdentifiers.SymbolTag
   | Csyntax.Evar x -> Identifiers.empty_set PreIdentifiers.SymbolTag
   | Csyntax.Ederef e1 -> gather_mem_vars_expr e1
   | Csyntax.Eaddrof e1 -> gather_mem_vars_addr e1
   | Csyntax.Eunop (x, e1) -> gather_mem_vars_expr e1
   | Csyntax.Ebinop (x, e1, e2) ->
     Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
       (gather_mem_vars_expr e2)
   | Csyntax.Ecast (x, e1) -> gather_mem_vars_expr e1
   | Csyntax.Econdition (e1, e2, e3) ->
     Identifiers.union_set PreIdentifiers.SymbolTag
       (Identifiers.union_set PreIdentifiers.SymbolTag
         (gather_mem_vars_expr e1) (gather_mem_vars_expr e2))
       (gather_mem_vars_expr e3)
   | Csyntax.Eandbool (e1, e2) ->
     Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
       (gather_mem_vars_expr e2)
   | Csyntax.Eorbool (e1, e2) ->
     Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
       (gather_mem_vars_expr e2)
   | Csyntax.Esizeof x -> Identifiers.empty_set PreIdentifiers.SymbolTag
   | Csyntax.Efield (e1, x) -> gather_mem_vars_expr e1
   | Csyntax.Ecost (x, e1) -> gather_mem_vars_expr e1)
(** val gather_mem_vars_addr : Csyntax.expr -> Identifiers.identifier_set **)
and gather_mem_vars_addr = function
| Csyntax.Expr (ed, ty) ->
  (match ed with
   | Csyntax.Econst_int (x, x0) ->
     Identifiers.empty_set PreIdentifiers.SymbolTag
   | Csyntax.Evar x ->
     Identifiers.add_set PreIdentifiers.SymbolTag
       (Identifiers.empty_set PreIdentifiers.SymbolTag) x
   | Csyntax.Ederef e1 -> gather_mem_vars_expr e1
   | Csyntax.Eaddrof x -> Identifiers.empty_set PreIdentifiers.SymbolTag
   | Csyntax.Eunop (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag
   | Csyntax.Ebinop (x, x0, x1) ->
     Identifiers.empty_set PreIdentifiers.SymbolTag
   | Csyntax.Ecast (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag
   | Csyntax.Econdition (x, x0, x1) ->
     Identifiers.empty_set PreIdentifiers.SymbolTag
   | Csyntax.Eandbool (x, x0) ->
     Identifiers.empty_set PreIdentifiers.SymbolTag
   | Csyntax.Eorbool (x, x0) ->
     Identifiers.empty_set PreIdentifiers.SymbolTag
   | Csyntax.Esizeof x -> Identifiers.empty_set PreIdentifiers.SymbolTag
   | Csyntax.Efield (e1, x) -> gather_mem_vars_addr e1
   | Csyntax.Ecost (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag)

(** val gather_mem_vars_stmt :
    Csyntax.statement -> Identifiers.identifier_set **)
let rec gather_mem_vars_stmt = function
| Csyntax.Sskip -> Identifiers.empty_set PreIdentifiers.SymbolTag
| Csyntax.Sassign (e1, e2) ->
  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
    (gather_mem_vars_expr e2)
| Csyntax.Scall (oe1, e2, es) ->
  Identifiers.union_set PreIdentifiers.SymbolTag
    (Identifiers.union_set PreIdentifiers.SymbolTag
      (match oe1 with
       | Types.None -> Identifiers.empty_set PreIdentifiers.SymbolTag
       | Types.Some e1 -> gather_mem_vars_expr e1) (gather_mem_vars_expr e2))
    (Util.foldl (fun s0 e0 ->
      Identifiers.union_set PreIdentifiers.SymbolTag s0
        (gather_mem_vars_expr e0))
      (Identifiers.empty_set PreIdentifiers.SymbolTag) es)
| Csyntax.Ssequence (s1, s2) ->
  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_stmt s1)
    (gather_mem_vars_stmt s2)
| Csyntax.Sifthenelse (e1, s1, s2) ->
  Identifiers.union_set PreIdentifiers.SymbolTag
    (Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
      (gather_mem_vars_stmt s1)) (gather_mem_vars_stmt s2)
| Csyntax.Swhile (e1, s1) ->
  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
    (gather_mem_vars_stmt s1)
| Csyntax.Sdowhile (e1, s1) ->
  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
    (gather_mem_vars_stmt s1)
| Csyntax.Sfor (s1, e1, s2, s3) ->
  Identifiers.union_set PreIdentifiers.SymbolTag
    (Identifiers.union_set PreIdentifiers.SymbolTag
      (Identifiers.union_set PreIdentifiers.SymbolTag
        (gather_mem_vars_stmt s1) (gather_mem_vars_expr e1))
      (gather_mem_vars_stmt s2)) (gather_mem_vars_stmt s3)
| Csyntax.Sbreak -> Identifiers.empty_set PreIdentifiers.SymbolTag
| Csyntax.Scontinue -> Identifiers.empty_set PreIdentifiers.SymbolTag
| Csyntax.Sreturn oe1 ->
  (match oe1 with
   | Types.None -> Identifiers.empty_set PreIdentifiers.SymbolTag
   | Types.Some e1 -> gather_mem_vars_expr e1)
| Csyntax.Sswitch (e1, ls) ->
  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
    (gather_mem_vars_ls ls)
| Csyntax.Slabel (x, s1) -> gather_mem_vars_stmt s1
| Csyntax.Sgoto x -> Identifiers.empty_set PreIdentifiers.SymbolTag
| Csyntax.Scost (x, s1) -> gather_mem_vars_stmt s1
(** val gather_mem_vars_ls :
    Csyntax.labeled_statements -> Identifiers.identifier_set **)
and gather_mem_vars_ls = function
| Csyntax.LSdefault s1 -> gather_mem_vars_stmt s1
| Csyntax.LScase (x, x0, s1, ls1) ->
  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_stmt s1)
    (gather_mem_vars_ls ls1)

type var_type =
| Global of AST.region
| Stack of Nat.nat
| Local

(** val var_type_rect_Type4 :
    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
let rec var_type_rect_Type4 h_Global h_Stack h_Local = function
| Global x_12977 -> h_Global x_12977
| Stack x_12978 -> h_Stack x_12978
| Local -> h_Local

(** val var_type_rect_Type5 :
    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
let rec var_type_rect_Type5 h_Global h_Stack h_Local = function
| Global x_12983 -> h_Global x_12983
| Stack x_12984 -> h_Stack x_12984
| Local -> h_Local

(** val var_type_rect_Type3 :
    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
let rec var_type_rect_Type3 h_Global h_Stack h_Local = function
| Global x_12989 -> h_Global x_12989
| Stack x_12990 -> h_Stack x_12990
| Local -> h_Local

(** val var_type_rect_Type2 :
    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
let rec var_type_rect_Type2 h_Global h_Stack h_Local = function
| Global x_12995 -> h_Global x_12995
| Stack x_12996 -> h_Stack x_12996
| Local -> h_Local

(** val var_type_rect_Type1 :
    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
let rec var_type_rect_Type1 h_Global h_Stack h_Local = function
| Global x_13001 -> h_Global x_13001
| Stack x_13002 -> h_Stack x_13002
| Local -> h_Local

(** val var_type_rect_Type0 :
    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
let rec var_type_rect_Type0 h_Global h_Stack h_Local = function
| Global x_13007 -> h_Global x_13007
| Stack x_13008 -> h_Stack x_13008
| Local -> h_Local

(** val var_type_inv_rect_Type4 :
    var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
    'a1) -> 'a1 **)
let var_type_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = var_type_rect_Type4 h1 h2 h3 hterm in hcut __

(** val var_type_inv_rect_Type3 :
    var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
    'a1) -> 'a1 **)
let var_type_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = var_type_rect_Type3 h1 h2 h3 hterm in hcut __

(** val var_type_inv_rect_Type2 :
    var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
    'a1) -> 'a1 **)
let var_type_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = var_type_rect_Type2 h1 h2 h3 hterm in hcut __

(** val var_type_inv_rect_Type1 :
    var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
    'a1) -> 'a1 **)
let var_type_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = var_type_rect_Type1 h1 h2 h3 hterm in hcut __

(** val var_type_inv_rect_Type0 :
    var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
    'a1) -> 'a1 **)
let var_type_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = var_type_rect_Type0 h1 h2 h3 hterm in hcut __

(** val var_type_discr : var_type -> var_type -> __ **)
let var_type_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Global a0 -> Obj.magic (fun _ dH -> dH __)
     | Stack a0 -> Obj.magic (fun _ dH -> dH __)
     | Local -> Obj.magic (fun _ dH -> dH)) y

(** val var_type_jmdiscr : var_type -> var_type -> __ **)
let var_type_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Global a0 -> Obj.magic (fun _ dH -> dH __)
     | Stack a0 -> Obj.magic (fun _ dH -> dH __)
     | Local -> Obj.magic (fun _ dH -> dH)) y

type var_types =
  (var_type, Csyntax.type0) Types.prod Identifiers.identifier_map

(** val lookup' :
    var_types -> PreIdentifiers.identifier -> (var_type, Csyntax.type0)
    Types.prod Errors.res **)
let lookup' vars id =
  Errors.opt_to_res (List.Cons ((Errors.MSG
    ErrorMessages.UndeclaredIdentifier), (List.Cons ((Errors.CTX
    (PreIdentifiers.SymbolTag, id)), List.Nil))))
    (Identifiers.lookup0 PreIdentifiers.SymbolTag vars id)

(** val always_alloc : Csyntax.type0 -> Bool.bool **)
let always_alloc = function
| Csyntax.Tvoid -> Bool.False
| Csyntax.Tint (x, x0) -> Bool.False
| Csyntax.Tpointer x -> Bool.False
| Csyntax.Tarray (x, x0) -> Bool.True
| Csyntax.Tfunction (x, x0) -> Bool.False
| Csyntax.Tstruct (x, x0) -> Bool.True
| Csyntax.Tunion (x, x0) -> Bool.True
| Csyntax.Tcomp_ptr x -> Bool.False

(** val characterise_vars :
    ((AST.ident, AST.region) Types.prod, Csyntax.type0) Types.prod List.list
    -> Csyntax.function0 -> (var_types, Nat.nat) Types.prod **)
let characterise_vars globals f =
  let m =
    List.foldr (fun idrt m ->
      Identifiers.add PreIdentifiers.SymbolTag m idrt.Types.fst.Types.fst
        { Types.fst = (Global idrt.Types.fst.Types.snd); Types.snd =
        idrt.Types.snd }) (Identifiers.empty_map PreIdentifiers.SymbolTag)
      globals
  in
  let mem_vars = gather_mem_vars_stmt f.Csyntax.fn_body in
  let { Types.fst = m0; Types.snd = stacksize } =
    List.foldr (fun v ms ->
      let { Types.fst = m0; Types.snd = stack_high } = ms in
      let { Types.fst = id; Types.snd = ty } = v in
      let { Types.fst = c; Types.snd = stack_high0 } =
        match Bool.orb (always_alloc ty)
                (Identifiers.member0 PreIdentifiers.SymbolTag mem_vars id) with
        | Bool.True ->
          { Types.fst = (Stack stack_high); Types.snd =
            (Nat.plus stack_high (Csyntax.sizeof ty)) }
        | Bool.False -> { Types.fst = Local; Types.snd = stack_high }
      in
      { Types.fst =
      (Identifiers.add PreIdentifiers.SymbolTag m0 id { Types.fst = c;
        Types.snd = ty }); Types.snd = stack_high0 }) { Types.fst = m;
      Types.snd = Nat.O } (List.append f.Csyntax.fn_params f.Csyntax.fn_vars)
  in
  { Types.fst = m0; Types.snd = stacksize }

open FrontEndVal

open Hide

open ByteValues

open GenMem

open FrontEndMem

open Division

open Z

open BitVectorZ

open Pointers

open Values

open FrontEndOps

open Cminor_syntax

(** val type_should_eq :
    Csyntax.type0 -> Csyntax.type0 -> 'a1 -> 'a1 Errors.res **)
let type_should_eq ty1 ty2 p =
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (TypeComparison.assert_type_eq ty1 ty2)) (fun _ ->
      Obj.magic (Errors.OK ((fun p0 -> p0) p))))

(** val region_should_eq :
    AST.region -> AST.region -> 'a1 -> 'a1 Errors.res **)
let region_should_eq clearme r5 x =
  (match clearme with
   | AST.XData ->
     (fun clearme0 ->
       match clearme0 with
       | AST.XData -> (fun _ p -> Errors.OK p)
       | AST.Code ->
         (fun _ p -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
   | AST.Code ->
     (fun clearme0 ->
       match clearme0 with
       | AST.XData ->
         (fun _ p -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
       | AST.Code -> (fun _ p -> Errors.OK p))) r5 __ x

(** val typ_should_eq : AST.typ -> AST.typ -> 'a1 -> 'a1 Errors.res **)
let typ_should_eq ty1 ty2 p =
  match AST.typ_eq ty1 ty2 with
  | Types.Inl _ -> Errors.OK p
  | Types.Inr _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)

(** val translate_unop :
    AST.typ -> AST.typ -> Csyntax.unary_operation ->
    FrontEndOps.unary_operation Errors.res **)
let translate_unop t t' = function
| Csyntax.Onotbool ->
  (match t with
   | AST.ASTint (sz, sg) ->
     (match t' with
      | AST.ASTint (sz', sg') ->
        Errors.OK (FrontEndOps.Onotbool ((AST.ASTint (sz, sg)), sz', sg'))
      | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
   | AST.ASTptr ->
     (match t' with
      | AST.ASTint (sz', sg') ->
        Errors.OK (FrontEndOps.Onotbool (AST.ASTptr, sz', sg'))
      | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
| Csyntax.Onotint ->
  (match t' with
   | AST.ASTint (sz, sg) ->
     typ_should_eq (AST.ASTint (sz, sg)) t (FrontEndOps.Onotint (sz, sg))
   | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
| Csyntax.Oneg ->
  (match t' with
   | AST.ASTint (sz, sg) ->
     typ_should_eq (AST.ASTint (sz, sg)) t (FrontEndOps.Onegint (sz, sg))
   | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))

(** val fix_ptr_type :
    Csyntax.type0 -> Nat.nat Types.option -> Cminor_syntax.expr ->
    Cminor_syntax.expr **)
let fix_ptr_type ty n e0 =
  e0

(** val translate_add :
    Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
    Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
let translate_add ty1 ty2 ty' =
  let ty1' = Csyntax.typ_of_type ty1 in
  let ty2' = Csyntax.typ_of_type ty2 in
  (match ClassifyOp.classify_add ty1 ty2 with
   | ClassifyOp.Add_case_ii (sz, sg) ->
     (fun e1 e2 ->
       typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty')
         (Cminor_syntax.Op2 ((AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)),
         (AST.ASTint (sz, sg)), (FrontEndOps.Oadd (sz, sg)), e1, e2)))
   | ClassifyOp.Add_case_pi (n, ty, sz, sg) ->
     (fun e1 e2 ->
       typ_should_eq AST.ASTptr (Csyntax.typ_of_type ty') (Cminor_syntax.Op2
         (AST.ASTptr, (AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr,
         (FrontEndOps.Oaddpi AST.I16), (fix_ptr_type ty n e1),
         (Cminor_syntax.Op2 ((AST.ASTint (AST.I16, AST.Signed)), (AST.ASTint
         (AST.I16, AST.Signed)), (AST.ASTint (AST.I16, AST.Signed)),
         (FrontEndOps.Omul (AST.I16, AST.Signed)), (Cminor_syntax.Op1
         ((AST.ASTint (sz, sg)), (AST.ASTint (AST.I16, AST.Signed)),
         (FrontEndOps.Ocastint (sz, sg, AST.I16, AST.Signed)), e2)),
         (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)),
         (FrontEndOps.Ointconst (AST.I16, AST.Signed,
         (AST.repr0 AST.I16 (Csyntax.sizeof ty)))))))))))
   | ClassifyOp.Add_case_ip (n, sz, sg, ty) ->
     (fun e1 e2 ->
       typ_should_eq AST.ASTptr (Csyntax.typ_of_type ty') (Cminor_syntax.Op2
         ((AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr, AST.ASTptr,
         (FrontEndOps.Oaddip AST.I16), (Cminor_syntax.Op2 ((AST.ASTint
         (AST.I16, AST.Signed)), (AST.ASTint (AST.I16, AST.Signed)),
         (AST.ASTint (AST.I16, AST.Signed)), (FrontEndOps.Omul (AST.I16,
         AST.Signed)), (Cminor_syntax.Op1 ((AST.ASTint (sz, sg)), (AST.ASTint
         (AST.I16, AST.Signed)), (FrontEndOps.Ocastint (sz, sg, AST.I16,
         AST.Signed)), e1)), (Cminor_syntax.Cst ((AST.ASTint (AST.I16,
         AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed,
         (AST.repr0 AST.I16 (Csyntax.sizeof ty)))))))),
         (fix_ptr_type ty n e2))))
   | ClassifyOp.Add_default (x, x0) ->
     (fun e1 e2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))

(** val translate_sub :
    Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
    Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
let translate_sub ty1 ty2 ty' =
  let ty1' = Csyntax.typ_of_type ty1 in
  let ty2' = Csyntax.typ_of_type ty2 in
  (match ClassifyOp.classify_sub ty1 ty2 with
   | ClassifyOp.Sub_case_ii (sz, sg) ->
     (fun e1 e2 ->
       typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty')
         (Cminor_syntax.Op2 ((AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)),
         (AST.ASTint (sz, sg)), (FrontEndOps.Osub (sz, sg)), e1, e2)))
   | ClassifyOp.Sub_case_pi (n, ty, sz, sg) ->
     (fun e1 e2 ->
       typ_should_eq AST.ASTptr (Csyntax.typ_of_type ty') (Cminor_syntax.Op2
         (AST.ASTptr, (AST.ASTint (AST.I32, AST.Signed)), AST.ASTptr,
         (FrontEndOps.Osubpi AST.I32), (fix_ptr_type ty n e1),
         (Cminor_syntax.Op1 ((AST.ASTint (AST.I16, sg)), (AST.ASTint
         (AST.I32, AST.Signed)), (FrontEndOps.Ocastint (AST.I16, sg, AST.I32,
         AST.Signed)), (Cminor_syntax.Op2 ((AST.ASTint (AST.I16, sg)),
         (AST.ASTint (AST.I16, sg)), (AST.ASTint (AST.I16, sg)),
         (FrontEndOps.Omul (AST.I16, sg)), (Cminor_syntax.Op1 ((AST.ASTint
         (sz, sg)), (AST.ASTint (AST.I16, sg)), (FrontEndOps.Ocastint (sz,
         sg, AST.I16, sg)), e2)), (Cminor_syntax.Cst ((AST.ASTint (AST.I16,
         sg)), (FrontEndOps.Ointconst (AST.I16, sg,
         (AST.repr0 AST.I16 (Csyntax.sizeof ty)))))))))))))
   | ClassifyOp.Sub_case_pp (n1, n2, ty10, ty20) ->
     (fun e1 e2 ->
       match ty' with
       | Csyntax.Tvoid ->
         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
       | Csyntax.Tint (sz, sg) ->
         Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (AST.I32, AST.Unsigned)),
           (AST.ASTint (sz, sg)), (FrontEndOps.Ocastint (AST.I32,
           AST.Unsigned, sz, sg)), (Cminor_syntax.Op2 ((AST.ASTint (AST.I32,
           AST.Unsigned)), (AST.ASTint (AST.I32, AST.Unsigned)), (AST.ASTint
           (AST.I32, AST.Unsigned)), (FrontEndOps.Odivu AST.I32),
           (Cminor_syntax.Op2 (AST.ASTptr, AST.ASTptr, (AST.ASTint (AST.I32,
           AST.Unsigned)), (FrontEndOps.Osubpp AST.I32),
           (fix_ptr_type ty10 n1 e1), (fix_ptr_type ty20 n2 e2))),
           (Cminor_syntax.Cst ((AST.ASTint (AST.I32, AST.Unsigned)),
           (FrontEndOps.Ointconst (AST.I32, AST.Unsigned,
           (AST.repr0 AST.I32 (Csyntax.sizeof ty10))))))))))
       | Csyntax.Tpointer x ->
         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
       | Csyntax.Tarray (x, x0) ->
         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
       | Csyntax.Tfunction (x, x0) ->
         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
       | Csyntax.Tstruct (x, x0) ->
         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
       | Csyntax.Tunion (x, x0) ->
         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
       | Csyntax.Tcomp_ptr x ->
         Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
   | ClassifyOp.Sub_default (x, x0) ->
     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))

(** val translate_mul :
    Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
    Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
let translate_mul ty1 ty2 ty' =
  let ty1' = Csyntax.typ_of_type ty1 in
  let ty2' = Csyntax.typ_of_type ty2 in
  (match ClassifyOp.classify_aop ty1 ty2 with
   | ClassifyOp.Aop_case_ii (sz, sg) ->
     (fun e1 e2 ->
       typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty')
         (Cminor_syntax.Op2 ((AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)),
         (AST.ASTint (sz, sg)), (FrontEndOps.Omul (sz, sg)), e1, e2)))
   | ClassifyOp.Aop_default (x, x0) ->
     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))

(** val translate_div :
    Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
    Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
let translate_div ty1 ty2 ty' =
  let ty1' = Csyntax.typ_of_type ty1 in
  let ty2' = Csyntax.typ_of_type ty2 in
  (match ClassifyOp.classify_aop ty1 ty2 with
   | ClassifyOp.Aop_case_ii (sz, sg) ->
     (match sg with
      | AST.Signed ->
        (fun e1 e2 ->
          typ_should_eq (AST.ASTint (sz, AST.Signed))
            (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
            AST.Signed)), (AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz,
            AST.Signed)), (FrontEndOps.Odiv sz), e1, e2)))
      | AST.Unsigned ->
        (fun e1 e2 ->
          typ_should_eq (AST.ASTint (sz, AST.Unsigned))
            (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
            AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz,
            AST.Unsigned)), (FrontEndOps.Odivu sz), e1, e2))))
   | ClassifyOp.Aop_default (x, x0) ->
     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))

(** val translate_mod :
    Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
    Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
let translate_mod ty1 ty2 ty' =
  let ty1' = Csyntax.typ_of_type ty1 in
  let ty2' = Csyntax.typ_of_type ty2 in
  (match ClassifyOp.classify_aop ty1 ty2 with
   | ClassifyOp.Aop_case_ii (sz, sg) ->
     (match sg with
      | AST.Signed ->
        (fun e1 e2 ->
          typ_should_eq (AST.ASTint (sz, AST.Signed))
            (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
            AST.Signed)), (AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz,
            AST.Signed)), (FrontEndOps.Omod sz), e1, e2)))
      | AST.Unsigned ->
        (fun e1 e2 ->
          typ_should_eq (AST.ASTint (sz, AST.Unsigned))
            (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
            AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz,
            AST.Unsigned)), (FrontEndOps.Omodu sz), e1, e2))))
   | ClassifyOp.Aop_default (x, x0) ->
     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))

(** val translate_shr :
    Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
    Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
let translate_shr ty1 ty2 ty' =
  let ty1' = Csyntax.typ_of_type ty1 in
  let ty2' = Csyntax.typ_of_type ty2 in
  (match ClassifyOp.classify_aop ty1 ty2 with
   | ClassifyOp.Aop_case_ii (sz, sg) ->
     (match sg with
      | AST.Signed ->
        (fun e1 e2 ->
          typ_should_eq (AST.ASTint (sz, AST.Signed))
            (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
            AST.Signed)), (AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz,
            AST.Signed)), (FrontEndOps.Oshr (sz, AST.Signed)), e1, e2)))
      | AST.Unsigned ->
        (fun e1 e2 ->
          typ_should_eq (AST.ASTint (sz, AST.Unsigned))
            (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
            AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz,
            AST.Unsigned)), (FrontEndOps.Oshru (sz, AST.Unsigned)), e1, e2))))
   | ClassifyOp.Aop_default (x, x0) ->
     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))

(** val complete_cmp :
    Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
let complete_cmp ty' e0 =
  match ty' with
  | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
  | Csyntax.Tint (sz, sg) ->
    Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (AST.I8, AST.Unsigned)),
      (AST.ASTint (sz, sg)), (FrontEndOps.Ocastint (AST.I8, AST.Unsigned, sz,
      sg)), e0))
  | Csyntax.Tpointer x ->
    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
  | Csyntax.Tarray (x, x0) ->
    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
  | Csyntax.Tfunction (x, x0) ->
    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
  | Csyntax.Tstruct (x, x0) ->
    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
  | Csyntax.Tunion (x, x0) ->
    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
  | Csyntax.Tcomp_ptr x ->
    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)

(** val translate_cmp :
    Integers.comparison -> Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 ->
    Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
let translate_cmp c ty1 ty2 ty' =
  let ty1' = Csyntax.typ_of_type ty1 in
  let ty2' = Csyntax.typ_of_type ty2 in
  (match ClassifyOp.classify_cmp ty1 ty2 with
   | ClassifyOp.Cmp_case_ii (sz, sg) ->
     (match sg with
      | AST.Signed ->
        (fun e1 e2 ->
          complete_cmp ty' (Cminor_syntax.Op2 ((AST.ASTint (sz, AST.Signed)),
            (AST.ASTint (sz, AST.Signed)), (AST.ASTint (AST.I8,
            AST.Unsigned)), (FrontEndOps.Ocmp (sz, AST.Signed, AST.Unsigned,
            c)), e1, e2)))
      | AST.Unsigned ->
        (fun e1 e2 ->
          complete_cmp ty' (Cminor_syntax.Op2 ((AST.ASTint (sz,
            AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint
            (AST.I8, AST.Unsigned)), (FrontEndOps.Ocmpu (sz, AST.Unsigned,
            c)), e1, e2))))
   | ClassifyOp.Cmp_case_pp (n, ty) ->
     (fun e1 e2 ->
       complete_cmp ty' (Cminor_syntax.Op2 (AST.ASTptr, AST.ASTptr,
         (AST.ASTint (AST.I8, AST.Unsigned)), (FrontEndOps.Ocmpp
         (AST.Unsigned, c)), (fix_ptr_type ty n e1), (fix_ptr_type ty n e2))))
   | ClassifyOp.Cmp_default (x, x0) ->
     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))

(** val translate_misc_aop :
    Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> (AST.intsize ->
    AST.signedness -> FrontEndOps.binary_operation) -> Cminor_syntax.expr ->
    Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
let translate_misc_aop ty1 ty2 ty' op0 =
  let ty1' = Csyntax.typ_of_type ty1 in
  let ty2' = Csyntax.typ_of_type ty2 in
  (match ClassifyOp.classify_aop ty1 ty2 with
   | ClassifyOp.Aop_case_ii (sz, sg) ->
     (fun e1 e2 ->
       typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty')
         (Cminor_syntax.Op2 ((Csyntax.typ_of_type (Csyntax.Tint (sz, sg))),
         (Csyntax.typ_of_type (Csyntax.Tint (sz, sg))), (AST.ASTint (sz,
         sg)), (op0 sz sg), e1, e2)))
   | ClassifyOp.Aop_default (x, x0) ->
     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))

(** val translate_binop :
    Csyntax.binary_operation -> Csyntax.type0 -> Cminor_syntax.expr ->
    Csyntax.type0 -> Cminor_syntax.expr -> Csyntax.type0 ->
    Cminor_syntax.expr Errors.res **)
let translate_binop op0 ty1 e1 ty2 e2 ty =
  let ty' = Csyntax.typ_of_type ty in
  (match op0 with
   | Csyntax.Oadd -> translate_add ty1 ty2 ty e1 e2
   | Csyntax.Osub -> translate_sub ty1 ty2 ty e1 e2
   | Csyntax.Omul -> translate_mul ty1 ty2 ty e1 e2
   | Csyntax.Odiv -> translate_div ty1 ty2 ty e1 e2
   | Csyntax.Omod -> translate_mod ty1 ty2 ty e1 e2
   | Csyntax.Oand ->
     translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oand (x, x0)) e1
       e2
   | Csyntax.Oor ->
     translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oor (x, x0)) e1
       e2
   | Csyntax.Oxor ->
     translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oxor (x, x0)) e1
       e2
   | Csyntax.Oshl ->
     translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oshl (x, x0)) e1
       e2
   | Csyntax.Oshr -> translate_shr ty1 ty2 ty e1 e2
   | Csyntax.Oeq -> translate_cmp Integers.Ceq ty1 ty2 ty e1 e2
   | Csyntax.One0 -> translate_cmp Integers.Cne ty1 ty2 ty e1 e2
   | Csyntax.Olt -> translate_cmp Integers.Clt ty1 ty2 ty e1 e2
   | Csyntax.Ogt -> translate_cmp Integers.Cgt ty1 ty2 ty e1 e2
   | Csyntax.Ole -> translate_cmp Integers.Cle ty1 ty2 ty e1 e2
   | Csyntax.Oge -> translate_cmp Integers.Cge ty1 ty2 ty e1 e2)

(** val translate_cast :
    Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr Types.sig0 ->
    Cminor_syntax.expr Types.sig0 Errors.res **)
let translate_cast ty1 ty2 =
  match ty1 with
  | Csyntax.Tvoid ->
    (fun x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
  | Csyntax.Tint (sz1, sg1) ->
    (fun e0 ->
      match ty2 with
      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tint (sz2, sg2) ->
        Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), (AST.ASTint
          (sz2, sg2)), (FrontEndOps.Ocastint (sz1, sg1, sz2, sg2)),
          (Types.pi1 e0)))
      | Csyntax.Tpointer x ->
        Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), AST.ASTptr,
          (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e0)))
      | Csyntax.Tarray (x, x0) ->
        Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), AST.ASTptr,
          (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e0)))
      | Csyntax.Tfunction (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tstruct (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tunion (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tcomp_ptr x ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
  | Csyntax.Tpointer x ->
    (fun e0 ->
      match ty2 with
      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tint (sz2, sg2) ->
        Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)),
          (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e0)))
      | Csyntax.Tpointer x0 -> Errors.OK e0
      | Csyntax.Tarray (x0, x1) -> Errors.OK e0
      | Csyntax.Tfunction (x0, x1) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tstruct (x0, x1) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tunion (x0, x1) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tcomp_ptr x0 ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
  | Csyntax.Tarray (x, x0) ->
    (fun e0 ->
      match ty2 with
      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tint (sz2, sg2) ->
        Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)),
          (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e0)))
      | Csyntax.Tpointer x1 -> Errors.OK e0
      | Csyntax.Tarray (x1, x2) -> Errors.OK e0
      | Csyntax.Tfunction (x1, x2) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tstruct (x1, x2) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tunion (x1, x2) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tcomp_ptr x1 ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
  | Csyntax.Tfunction (x, x0) ->
    (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
  | Csyntax.Tstruct (x, x0) ->
    (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
  | Csyntax.Tunion (x, x0) ->
    (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
  | Csyntax.Tcomp_ptr x ->
    (fun x0 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))

(** val cm_zero : AST.intsize -> AST.signedness -> Cminor_syntax.expr **)
let cm_zero sz sg =
  Cminor_syntax.Cst ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg,
    (BitVector.zero (AST.bitsize_of_intsize sz)))))

(** val cm_one : AST.intsize -> AST.signedness -> Cminor_syntax.expr **)
let cm_one sz sg =
  Cminor_syntax.Cst ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg,
    (AST.repr0 sz (Nat.S Nat.O)))))

(** val translate_expr :
    var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res **)
let rec translate_expr vars = function
| Csyntax.Expr (ed, ty) ->
  (match ed with
   | Csyntax.Econst_int (sz, i) ->
     (match ty with
      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tint (sz', sg) ->
        AST.intsize_eq_elim' sz sz' (Errors.OK (Cminor_syntax.Cst
          ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg, i)))))
          (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
      | Csyntax.Tpointer x ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tarray (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tfunction (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tstruct (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tunion (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tcomp_ptr x ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
   | Csyntax.Evar id ->
     Errors.bind2_eq (lookup' vars id) (fun c t _ ->
       (match c with
        | Global r ->
          (fun _ ->
            match Csyntax.access_mode ty with
            | Csyntax.By_value t0 ->
              Errors.OK (Cminor_syntax.Mem (t0, (Cminor_syntax.Cst
                (AST.ASTptr, (FrontEndOps.Oaddrsymbol (id, Nat.O))))))
            | Csyntax.By_reference ->
              Errors.OK (Cminor_syntax.Cst (AST.ASTptr,
                (FrontEndOps.Oaddrsymbol (id, Nat.O))))
            | Csyntax.By_nothing x ->
              Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX
                (PreIdentifiers.SymbolTag, id)), List.Nil)))))
        | Stack n ->
          (fun _ ->
            match Csyntax.access_mode ty with
            | Csyntax.By_value t0 ->
              Errors.OK (Cminor_syntax.Mem (t0, (Cminor_syntax.Cst
                (AST.ASTptr, (FrontEndOps.Oaddrstack n)))))
            | Csyntax.By_reference ->
              Errors.OK (Cminor_syntax.Cst (AST.ASTptr,
                (FrontEndOps.Oaddrstack n)))
            | Csyntax.By_nothing x ->
              Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX
                (PreIdentifiers.SymbolTag, id)), List.Nil)))))
        | Local ->
          (fun _ ->
            type_should_eq t ty (Cminor_syntax.Id ((Csyntax.typ_of_type t),
              id)))) __)
   | Csyntax.Ederef e1 ->
     Obj.magic
       (Monad.m_bind0 (Monad.max_def Errors.res0)
         (Obj.magic (translate_expr vars e1)) (fun e1' ->
         (match Csyntax.typ_of_type (Csyntax.typeof e1) with
          | AST.ASTint (x, x0) ->
            (fun x1 ->
              Obj.magic (Errors.Error
                (Errors.msg ErrorMessages.TypeMismatch)))
          | AST.ASTptr ->
            (fun e1'0 ->
              match Csyntax.access_mode ty with
              | Csyntax.By_value t ->
                Obj.magic (Errors.OK (Cminor_syntax.Mem (t,
                  (Types.pi1 e1'0))))
              | Csyntax.By_reference -> Obj.magic (Errors.OK e1'0)
              | Csyntax.By_nothing x ->
                Obj.magic (Errors.Error
                  (Errors.msg ErrorMessages.BadlyTypedAccess)))) e1'))
   | Csyntax.Eaddrof e1 ->
     Obj.magic
       (Monad.m_bind0 (Monad.max_def Errors.res0)
         (Obj.magic (translate_addr vars e1)) (fun e1' ->
         match Csyntax.typ_of_type ty with
         | AST.ASTint (x, x0) ->
           Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
         | AST.ASTptr -> Obj.magic (Errors.OK e1')))
   | Csyntax.Eunop (op0, e1) ->
     (match op0 with
      | Csyntax.Onotbool ->
        (fun _ ->
          (match Csyntax.typ_of_type ty with
           | AST.ASTint (sz, sg) ->
             (fun _ ->
               (match sz with
                | AST.I8 ->
                  (fun _ -> Errors.Error
                    (Errors.msg ErrorMessages.TypeMismatch))
                | AST.I16 ->
                  (fun _ -> Errors.Error
                    (Errors.msg ErrorMessages.TypeMismatch))
                | AST.I32 ->
                  (fun _ ->
                    Obj.magic
                      (Monad.m_bind0 (Monad.max_def Errors.res0)
                        (Obj.magic
                          (translate_unop
                            (Csyntax.typ_of_type (Csyntax.typeof e1))
                            (Csyntax.typ_of_type ty) op0)) (fun op' ->
                        Monad.m_bind0 (Monad.max_def Errors.res0)
                          (Obj.magic (translate_expr vars e1)) (fun e1' ->
                          Obj.magic (Errors.OK (Cminor_syntax.Op1
                            ((Csyntax.typ_of_type (Csyntax.typeof e1)),
                            (Csyntax.typ_of_type ty), op', (Types.pi1 e1')))))))))
                 __)
           | AST.ASTptr ->
             (fun _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
            __)
      | Csyntax.Onotint ->
        (fun _ ->
          Obj.magic
            (Monad.m_bind0 (Monad.max_def Errors.res0)
              (Obj.magic
                (translate_unop (Csyntax.typ_of_type (Csyntax.typeof e1))
                  (Csyntax.typ_of_type ty) op0)) (fun op' ->
              Monad.m_bind0 (Monad.max_def Errors.res0)
                (Obj.magic (translate_expr vars e1)) (fun e1' ->
                Obj.magic (Errors.OK (Cminor_syntax.Op1
                  ((Csyntax.typ_of_type (Csyntax.typeof e1)),
                  (Csyntax.typ_of_type ty), op', (Types.pi1 e1'))))))))
      | Csyntax.Oneg ->
        (fun _ ->
          Obj.magic
            (Monad.m_bind0 (Monad.max_def Errors.res0)
              (Obj.magic
                (translate_unop (Csyntax.typ_of_type (Csyntax.typeof e1))
                  (Csyntax.typ_of_type ty) op0)) (fun op' ->
              Monad.m_bind0 (Monad.max_def Errors.res0)
                (Obj.magic (translate_expr vars e1)) (fun e1' ->
                Obj.magic (Errors.OK (Cminor_syntax.Op1
                  ((Csyntax.typ_of_type (Csyntax.typeof e1)),
                  (Csyntax.typ_of_type ty), op', (Types.pi1 e1'))))))))) __
   | Csyntax.Ebinop (op0, e1, e2) ->
     Obj.magic
       (Monad.m_bind0 (Monad.max_def Errors.res0)
         (Obj.magic (translate_expr vars e1)) (fun e1' ->
         Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (translate_expr vars e2)) (fun e2' ->
           Obj.magic
             (Errors.bind_eq
               (translate_binop op0 (Csyntax.typeof e1) (Types.pi1 e1')
                 (Csyntax.typeof e2) (Types.pi1 e2') ty) (fun e' _ ->
               Errors.OK e')))))
   | Csyntax.Ecast (ty1, e1) ->
     Obj.magic
       (Monad.m_bind0 (Monad.max_def Errors.res0)
         (Obj.magic (translate_expr vars e1)) (fun e1' ->
         Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (translate_cast (Csyntax.typeof e1) ty1 e1'))
           (fun e' ->
           Monad.m_bind0 (Monad.max_def Errors.res0)
             (Obj.magic
               (typ_should_eq (Csyntax.typ_of_type ty1)
                 (Csyntax.typ_of_type ty) e')) (fun e'0 ->
             Obj.magic (Errors.OK e'0)))))
   | Csyntax.Econdition (e1, e2, e3) ->
     Obj.magic
       (Monad.m_bind0 (Monad.max_def Errors.res0)
         (Obj.magic (translate_expr vars e1)) (fun e1' ->
         Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (translate_expr vars e2)) (fun e2' ->
           Monad.m_bind0 (Monad.max_def Errors.res0)
             (Obj.magic
               (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e2))
                 (Csyntax.typ_of_type ty) e2')) (fun e2'0 ->
             Monad.m_bind0 (Monad.max_def Errors.res0)
               (Obj.magic (translate_expr vars e3)) (fun e3' ->
               Monad.m_bind0 (Monad.max_def Errors.res0)
                 (Obj.magic
                   (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e3))
                     (Csyntax.typ_of_type ty) e3')) (fun e3'0 ->
                 (match Csyntax.typ_of_type (Csyntax.typeof e1) with
                  | AST.ASTint (x, x0) ->
                    (fun e1'0 ->
                      Obj.magic (Errors.OK (Cminor_syntax.Cond (x, x0,
                        (Csyntax.typ_of_type ty), (Types.pi1 e1'0),
                        (Types.pi1 e2'0), (Types.pi1 e3'0)))))
                  | AST.ASTptr ->
                    (fun x ->
                      Obj.magic (Errors.Error
                        (Errors.msg ErrorMessages.TypeMismatch)))) e1'))))))
   | Csyntax.Eandbool (e1, e2) ->
     Obj.magic
       (Monad.m_bind0 (Monad.max_def Errors.res0)
         (Obj.magic (translate_expr vars e1)) (fun e1' ->
         Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (translate_expr vars e2)) (fun e2' ->
           match ty with
           | Csyntax.Tvoid ->
             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
           | Csyntax.Tint (sz, sg) ->
             Monad.m_bind0 (Monad.max_def Errors.res0)
               (Obj.magic
                 (type_should_eq (Csyntax.typeof e2) (Csyntax.Tint (sz, sg))
                   e2')) (fun e2'0 ->
               (match Csyntax.typ_of_type (Csyntax.typeof e1) with
                | AST.ASTint (sz1, x) ->
                  (fun e1'0 ->
                    Obj.magic (Errors.OK (Cminor_syntax.Cond (sz1, x,
                      (AST.ASTint (sz, sg)), (Types.pi1 e1'0),
                      (Cminor_syntax.Cond (sz, sg, (AST.ASTint (sz, sg)),
                      (Types.pi1 e2'0), (cm_one sz sg), (cm_zero sz sg))),
                      (cm_zero sz sg)))))
                | AST.ASTptr ->
                  (fun x ->
                    Obj.magic (Errors.Error
                      (Errors.msg ErrorMessages.TypeMismatch)))) e1')
           | Csyntax.Tpointer x ->
             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
           | Csyntax.Tarray (x, x0) ->
             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
           | Csyntax.Tfunction (x, x0) ->
             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
           | Csyntax.Tstruct (x, x0) ->
             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
           | Csyntax.Tunion (x, x0) ->
             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
           | Csyntax.Tcomp_ptr x ->
             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))))
   | Csyntax.Eorbool (e1, e2) ->
     Obj.magic
       (Monad.m_bind0 (Monad.max_def Errors.res0)
         (Obj.magic (translate_expr vars e1)) (fun e1' ->
         Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (translate_expr vars e2)) (fun e2' ->
           match ty with
           | Csyntax.Tvoid ->
             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
           | Csyntax.Tint (sz, sg) ->
             Monad.m_bind0 (Monad.max_def Errors.res0)
               (Obj.magic
                 (type_should_eq (Csyntax.typeof e2) (Csyntax.Tint (sz, sg))
                   e2')) (fun e2'0 ->
               (match Csyntax.typ_of_type (Csyntax.typeof e1) with
                | AST.ASTint (x, x0) ->
                  (fun e1'0 ->
                    Obj.magic (Errors.OK (Cminor_syntax.Cond (x, x0,
                      (AST.ASTint (sz, sg)), (Types.pi1 e1'0),
                      (cm_one sz sg), (Cminor_syntax.Cond (sz, sg,
                      (AST.ASTint (sz, sg)), (Types.pi1 e2'0),
                      (cm_one sz sg), (cm_zero sz sg)))))))
                | AST.ASTptr ->
                  (fun x ->
                    Obj.magic (Errors.Error
                      (Errors.msg ErrorMessages.TypeMismatch)))) e1')
           | Csyntax.Tpointer x ->
             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
           | Csyntax.Tarray (x, x0) ->
             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
           | Csyntax.Tfunction (x, x0) ->
             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
           | Csyntax.Tstruct (x, x0) ->
             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
           | Csyntax.Tunion (x, x0) ->
             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
           | Csyntax.Tcomp_ptr x ->
             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))))
   | Csyntax.Esizeof ty1 ->
     (match ty with
      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tint (sz, sg) ->
        Errors.OK (Cminor_syntax.Cst ((AST.ASTint (sz, sg)),
          (FrontEndOps.Ointconst (sz, sg,
          (AST.repr0 sz (Csyntax.sizeof ty1))))))
      | Csyntax.Tpointer x ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tarray (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tfunction (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tstruct (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tunion (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
      | Csyntax.Tcomp_ptr x ->
        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
   | Csyntax.Efield (e1, id) ->
     (match Csyntax.typeof e1 with
      | Csyntax.Tvoid ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
      | Csyntax.Tint (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
      | Csyntax.Tpointer x ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
      | Csyntax.Tarray (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
      | Csyntax.Tfunction (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
      | Csyntax.Tstruct (x, fl) ->
        Obj.magic
          (Monad.m_bind0 (Monad.max_def Errors.res0)
            (Obj.magic (translate_addr vars e1)) (fun e1' ->
            Monad.m_bind0 (Monad.max_def Errors.res0)
              (Obj.magic (Csyntax.field_offset id fl)) (fun off ->
              match Csyntax.access_mode ty with
              | Csyntax.By_value t ->
                Obj.magic (Errors.OK (Cminor_syntax.Mem (t,
                  (Cminor_syntax.Op2 (AST.ASTptr, (AST.ASTint (AST.I16,
                  AST.Signed)), AST.ASTptr, (FrontEndOps.Oaddpi AST.I16),
                  (Types.pi1 e1'), (Cminor_syntax.Cst ((AST.ASTint (AST.I16,
                  AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed,
                  (AST.repr0 AST.I16 off))))))))))
              | Csyntax.By_reference ->
                Obj.magic (Errors.OK (Cminor_syntax.Op2 (AST.ASTptr,
                  (AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr,
                  (FrontEndOps.Oaddpi AST.I16), (Types.pi1 e1'),
                  (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)),
                  (FrontEndOps.Ointconst (AST.I16, AST.Signed,
                  (AST.repr0 AST.I16 off))))))))
              | Csyntax.By_nothing x0 ->
                Obj.magic (Errors.Error
                  (Errors.msg ErrorMessages.BadlyTypedAccess)))))
      | Csyntax.Tunion (x, x0) ->
        Obj.magic
          (Monad.m_bind0 (Monad.max_def Errors.res0)
            (Obj.magic (translate_addr vars e1)) (fun e1' ->
            match Csyntax.access_mode ty with
            | Csyntax.By_value t ->
              Obj.magic (Errors.OK (Cminor_syntax.Mem (t, (Types.pi1 e1'))))
            | Csyntax.By_reference -> Obj.magic (Errors.OK e1')
            | Csyntax.By_nothing x1 ->
              Obj.magic (Errors.Error
                (Errors.msg ErrorMessages.BadlyTypedAccess))))
      | Csyntax.Tcomp_ptr x ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess))
   | Csyntax.Ecost (l, e1) ->
     Obj.magic
       (Monad.m_bind0 (Monad.max_def Errors.res0)
         (Obj.magic (translate_expr vars e1)) (fun e1' ->
         Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (Errors.OK (Cminor_syntax.Ecost
             ((Csyntax.typ_of_type (Csyntax.typeof e1)), l,
             (Types.pi1 e1'))))) (fun e' ->
           Obj.magic
             (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e1))
               (Csyntax.typ_of_type ty) e')))))
(** val translate_addr :
    var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res **)
and translate_addr vars = function
| Csyntax.Expr (ed, x) ->
  (match ed with
   | Csyntax.Econst_int (x0, x1) ->
     Errors.Error (Errors.msg ErrorMessages.BadLvalue)
   | Csyntax.Evar id ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def Errors.res0)
         (Obj.magic (lookup' vars id)) (fun c t ->
         match c with
         | Global r ->
           Obj.magic (Errors.OK (Cminor_syntax.Cst (AST.ASTptr,
             (FrontEndOps.Oaddrsymbol (id, Nat.O)))))
         | Stack n ->
           Obj.magic (Errors.OK (Cminor_syntax.Cst (AST.ASTptr,
             (FrontEndOps.Oaddrstack n))))
         | Local ->
           Obj.magic (Errors.Error (List.Cons ((Errors.MSG
             ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX
             (PreIdentifiers.SymbolTag, id)), List.Nil)))))))
   | Csyntax.Ederef e1 ->
     Obj.magic
       (Monad.m_bind0 (Monad.max_def Errors.res0)
         (Obj.magic (translate_expr vars e1)) (fun e1' ->
         (match Csyntax.typ_of_type (Csyntax.typeof e1) with
          | AST.ASTint (x0, x1) ->
            (fun x2 ->
              Obj.magic (Errors.Error
                (Errors.msg ErrorMessages.BadlyTypedAccess)))
          | AST.ASTptr -> (fun e1'0 -> Obj.magic (Errors.OK e1'0))) e1'))
   | Csyntax.Eaddrof x0 -> Errors.Error (Errors.msg ErrorMessages.BadLvalue)
   | Csyntax.Eunop (x0, x1) ->
     Errors.Error (Errors.msg ErrorMessages.BadLvalue)
   | Csyntax.Ebinop (x0, x1, x2) ->
     Errors.Error (Errors.msg ErrorMessages.BadLvalue)
   | Csyntax.Ecast (x0, x1) ->
     Errors.Error (Errors.msg ErrorMessages.BadLvalue)
   | Csyntax.Econdition (x0, x1, x2) ->
     Errors.Error (Errors.msg ErrorMessages.BadLvalue)
   | Csyntax.Eandbool (x0, x1) ->
     Errors.Error (Errors.msg ErrorMessages.BadLvalue)
   | Csyntax.Eorbool (x0, x1) ->
     Errors.Error (Errors.msg ErrorMessages.BadLvalue)
   | Csyntax.Esizeof x0 -> Errors.Error (Errors.msg ErrorMessages.BadLvalue)
   | Csyntax.Efield (e1, id) ->
     (match Csyntax.typeof e1 with
      | Csyntax.Tvoid ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
      | Csyntax.Tint (x0, x1) ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
      | Csyntax.Tpointer x0 ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
      | Csyntax.Tarray (x0, x1) ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
      | Csyntax.Tfunction (x0, x1) ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
      | Csyntax.Tstruct (x0, fl) ->
        Obj.magic
          (Monad.m_bind0 (Monad.max_def Errors.res0)
            (Obj.magic (translate_addr vars e1)) (fun e1' ->
            Monad.m_bind0 (Monad.max_def Errors.res0)
              (Obj.magic (Csyntax.field_offset id fl)) (fun off ->
              Obj.magic (Errors.OK (Cminor_syntax.Op2 (AST.ASTptr,
                (AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr,
                (FrontEndOps.Oaddpi AST.I16), (Types.pi1 e1'),
                (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)),
                (FrontEndOps.Ointconst (AST.I16, AST.Signed,
                (AST.repr0 AST.I16 off)))))))))))
      | Csyntax.Tunion (x0, x1) -> translate_addr vars e1
      | Csyntax.Tcomp_ptr x0 ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess))
   | Csyntax.Ecost (x0, x1) ->
     Errors.Error (Errors.msg ErrorMessages.BadLvalue))

type destination =
| IdDest of AST.ident * Csyntax.type0
| MemDest of Cminor_syntax.expr Types.sig0

(** val destination_rect_Type4 :
    var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
    (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **)
let rec destination_rect_Type4 vars h_IdDest h_MemDest = function
| IdDest (id, ty) -> h_IdDest id ty __
| MemDest x_14463 -> h_MemDest x_14463

(** val destination_rect_Type5 :
    var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
    (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **)
let rec destination_rect_Type5 vars h_IdDest h_MemDest = function
| IdDest (id, ty) -> h_IdDest id ty __
| MemDest x_14468 -> h_MemDest x_14468

(** val destination_rect_Type3 :
    var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
    (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **)
let rec destination_rect_Type3 vars h_IdDest h_MemDest = function
| IdDest (id, ty) -> h_IdDest id ty __
| MemDest x_14473 -> h_MemDest x_14473

(** val destination_rect_Type2 :
    var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
    (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **)
let rec destination_rect_Type2 vars h_IdDest h_MemDest = function
| IdDest (id, ty) -> h_IdDest id ty __
| MemDest x_14478 -> h_MemDest x_14478

(** val destination_rect_Type1 :
    var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
    (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **)
let rec destination_rect_Type1 vars h_IdDest h_MemDest = function
| IdDest (id, ty) -> h_IdDest id ty __
| MemDest x_14483 -> h_MemDest x_14483

(** val destination_rect_Type0 :
    var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
    (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **)
let rec destination_rect_Type0 vars h_IdDest h_MemDest = function
| IdDest (id, ty) -> h_IdDest id ty __
| MemDest x_14488 -> h_MemDest x_14488

(** val destination_inv_rect_Type4 :
    var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ ->
    'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
let destination_inv_rect_Type4 x1 hterm h1 h2 =
  let hcut = destination_rect_Type4 x1 h1 h2 hterm in hcut __

(** val destination_inv_rect_Type3 :
    var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ ->
    'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
let destination_inv_rect_Type3 x1 hterm h1 h2 =
  let hcut = destination_rect_Type3 x1 h1 h2 hterm in hcut __

(** val destination_inv_rect_Type2 :
    var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ ->
    'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
let destination_inv_rect_Type2 x1 hterm h1 h2 =
  let hcut = destination_rect_Type2 x1 h1 h2 hterm in hcut __

(** val destination_inv_rect_Type1 :
    var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ ->
    'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
let destination_inv_rect_Type1 x1 hterm h1 h2 =
  let hcut = destination_rect_Type1 x1 h1 h2 hterm in hcut __

(** val destination_inv_rect_Type0 :
    var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ ->
    'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
let destination_inv_rect_Type0 x1 hterm h1 h2 =
  let hcut = destination_rect_Type0 x1 h1 h2 hterm in hcut __

(** val destination_discr : var_types -> destination -> destination -> __ **)
let destination_discr a1 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | IdDest (a0, a10) -> Obj.magic (fun _ dH -> dH __ __ __)
     | MemDest a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val destination_jmdiscr :
    var_types -> destination -> destination -> __ **)
let destination_jmdiscr a1 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | IdDest (a0, a10) -> Obj.magic (fun _ dH -> dH __ __ __)
     | MemDest a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val translate_dest : var_types -> Csyntax.expr -> __ **)
let translate_dest vars e1 = match e1 with
| Csyntax.Expr (ed1, ty1) ->
  (match ed1 with
   | Csyntax.Econst_int (x, x0) ->
     Monad.m_bind0 (Monad.max_def Errors.res0)
       (Obj.magic (translate_addr vars e1)) (fun e1' ->
       Obj.magic (Errors.OK (MemDest e1')))
   | Csyntax.Evar id ->
     Obj.magic
       (Errors.bind2_eq (lookup' vars id) (fun c t _ ->
         (match c with
          | Global r ->
            (fun _ -> Errors.OK (MemDest (Cminor_syntax.Cst (AST.ASTptr,
              (FrontEndOps.Oaddrsymbol (id, Nat.O))))))
          | Stack n ->
            (fun _ -> Errors.OK (MemDest (Cminor_syntax.Cst (AST.ASTptr,
              (FrontEndOps.Oaddrstack n)))))
          | Local -> (fun _ -> Errors.OK (IdDest (id, t)))) __))
   | Csyntax.Ederef x ->
     Monad.m_bind0 (Monad.max_def Errors.res0)
       (Obj.magic (translate_addr vars e1)) (fun e1' ->
       Obj.magic (Errors.OK (MemDest e1')))
   | Csyntax.Eaddrof x ->
     Monad.m_bind0 (Monad.max_def Errors.res0)
       (Obj.magic (translate_addr vars e1)) (fun e1' ->
       Obj.magic (Errors.OK (MemDest e1')))
   | Csyntax.Eunop (x, x0) ->
     Monad.m_bind0 (Monad.max_def Errors.res0)
       (Obj.magic (translate_addr vars e1)) (fun e1' ->
       Obj.magic (Errors.OK (MemDest e1')))
   | Csyntax.Ebinop (x, x0, x1) ->
     Monad.m_bind0 (Monad.max_def Errors.res0)
       (Obj.magic (translate_addr vars e1)) (fun e1' ->
       Obj.magic (Errors.OK (MemDest e1')))
   | Csyntax.Ecast (x, x0) ->
     Monad.m_bind0 (Monad.max_def Errors.res0)
       (Obj.magic (translate_addr vars e1)) (fun e1' ->
       Obj.magic (Errors.OK (MemDest e1')))
   | Csyntax.Econdition (x, x0, x1) ->
     Monad.m_bind0 (Monad.max_def Errors.res0)
       (Obj.magic (translate_addr vars e1)) (fun e1' ->
       Obj.magic (Errors.OK (MemDest e1')))
   | Csyntax.Eandbool (x, x0) ->
     Monad.m_bind0 (Monad.max_def Errors.res0)
       (Obj.magic (translate_addr vars e1)) (fun e1' ->
       Obj.magic (Errors.OK (MemDest e1')))
   | Csyntax.Eorbool (x, x0) ->
     Monad.m_bind0 (Monad.max_def Errors.res0)
       (Obj.magic (translate_addr vars e1)) (fun e1' ->
       Obj.magic (Errors.OK (MemDest e1')))
   | Csyntax.Esizeof x ->
     Monad.m_bind0 (Monad.max_def Errors.res0)
       (Obj.magic (translate_addr vars e1)) (fun e1' ->
       Obj.magic (Errors.OK (MemDest e1')))
   | Csyntax.Efield (x, x0) ->
     Monad.m_bind0 (Monad.max_def Errors.res0)
       (Obj.magic (translate_addr vars e1)) (fun e1' ->
       Obj.magic (Errors.OK (MemDest e1')))
   | Csyntax.Ecost (x, x0) ->
     Monad.m_bind0 (Monad.max_def Errors.res0)
       (Obj.magic (translate_addr vars e1)) (fun e1' ->
       Obj.magic (Errors.OK (MemDest e1'))))

type lenv = PreIdentifiers.identifier Identifiers.identifier_map

(** val lookup_label :
    lenv -> PreIdentifiers.identifier -> PreIdentifiers.identifier Errors.res **)
let lookup_label lbls l =
  Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingLabel),
    (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, l)), List.Nil))))
    (Identifiers.lookup0 PreIdentifiers.SymbolTag lbls l)

type fresh_list_for_univ = __

type labgen = { labuniverse : Identifiers.universe;
                label_genlist : PreIdentifiers.identifier List.list }

(** val labgen_rect_Type4 :
    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    'a1) -> labgen -> 'a1 **)
let rec labgen_rect_Type4 h_mk_labgen x_14523 =
  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    x_14523
  in
  h_mk_labgen labuniverse0 label_genlist0 __

(** val labgen_rect_Type5 :
    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    'a1) -> labgen -> 'a1 **)
let rec labgen_rect_Type5 h_mk_labgen x_14525 =
  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    x_14525
  in
  h_mk_labgen labuniverse0 label_genlist0 __

(** val labgen_rect_Type3 :
    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    'a1) -> labgen -> 'a1 **)
let rec labgen_rect_Type3 h_mk_labgen x_14527 =
  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    x_14527
  in
  h_mk_labgen labuniverse0 label_genlist0 __

(** val labgen_rect_Type2 :
    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    'a1) -> labgen -> 'a1 **)
let rec labgen_rect_Type2 h_mk_labgen x_14529 =
  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    x_14529
  in
  h_mk_labgen labuniverse0 label_genlist0 __

(** val labgen_rect_Type1 :
    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    'a1) -> labgen -> 'a1 **)
let rec labgen_rect_Type1 h_mk_labgen x_14531 =
  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    x_14531
  in
  h_mk_labgen labuniverse0 label_genlist0 __

(** val labgen_rect_Type0 :
    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    'a1) -> labgen -> 'a1 **)
let rec labgen_rect_Type0 h_mk_labgen x_14533 =
  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    x_14533
  in
  h_mk_labgen labuniverse0 label_genlist0 __

(** val labuniverse : labgen -> Identifiers.universe **)
let rec labuniverse xxx =
  xxx.labuniverse

(** val label_genlist : labgen -> PreIdentifiers.identifier List.list **)
let rec label_genlist xxx =
  xxx.label_genlist

(** val labgen_inv_rect_Type4 :
    labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
    __ -> __ -> 'a1) -> 'a1 **)
let labgen_inv_rect_Type4 hterm h1 =
  let hcut = labgen_rect_Type4 h1 hterm in hcut __

(** val labgen_inv_rect_Type3 :
    labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
    __ -> __ -> 'a1) -> 'a1 **)
let labgen_inv_rect_Type3 hterm h1 =
  let hcut = labgen_rect_Type3 h1 hterm in hcut __

(** val labgen_inv_rect_Type2 :
    labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
    __ -> __ -> 'a1) -> 'a1 **)
let labgen_inv_rect_Type2 hterm h1 =
  let hcut = labgen_rect_Type2 h1 hterm in hcut __

(** val labgen_inv_rect_Type1 :
    labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
    __ -> __ -> 'a1) -> 'a1 **)
let labgen_inv_rect_Type1 hterm h1 =
  let hcut = labgen_rect_Type1 h1 hterm in hcut __

(** val labgen_inv_rect_Type0 :
    labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
    __ -> __ -> 'a1) -> 'a1 **)
let labgen_inv_rect_Type0 hterm h1 =
  let hcut = labgen_rect_Type0 h1 hterm in hcut __

(** val labgen_discr : labgen -> labgen -> __ **)
let labgen_discr x y =
  Logic.eq_rect_Type2 x
    (let { labuniverse = a0; label_genlist = a1 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val labgen_jmdiscr : labgen -> labgen -> __ **)
let labgen_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { labuniverse = a0; label_genlist = a1 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val generate_fresh_label :
    labgen -> (PreIdentifiers.identifier, labgen) Types.prod Types.sig0 **)
let generate_fresh_label ul =
  (let { Types.fst = tmp; Types.snd = u } =
     Identifiers.fresh PreIdentifiers.Label ul.labuniverse
   in
  (fun _ -> { Types.fst = tmp; Types.snd = { labuniverse = u; label_genlist =
  (List.Cons (tmp, ul.label_genlist)) } })) __

(** val labels_defined : Csyntax.statement -> AST.ident List.list **)
let rec labels_defined = function
| Csyntax.Sskip -> List.Nil
| Csyntax.Sassign (x, x0) -> List.Nil
| Csyntax.Scall (x, x0, x1) -> List.Nil
| Csyntax.Ssequence (s1, s2) ->
  List.append (labels_defined s1) (labels_defined s2)
| Csyntax.Sifthenelse (x, s1, s2) ->
  List.append (labels_defined s1) (labels_defined s2)
| Csyntax.Swhile (x, s0) -> labels_defined s0
| Csyntax.Sdowhile (x, s0) -> labels_defined s0
| Csyntax.Sfor (s1, x, s2, s3) ->
  List.append (labels_defined s1)
    (List.append (labels_defined s2) (labels_defined s3))
| Csyntax.Sbreak -> List.Nil
| Csyntax.Scontinue -> List.Nil
| Csyntax.Sreturn x -> List.Nil
| Csyntax.Sswitch (x, ls) -> labels_defined_switch ls
| Csyntax.Slabel (l, s0) -> List.Cons (l, (labels_defined s0))
| Csyntax.Sgoto x -> List.Nil
| Csyntax.Scost (x, s0) -> labels_defined s0
(** val labels_defined_switch :
    Csyntax.labeled_statements -> AST.ident List.list **)
and labels_defined_switch = function
| Csyntax.LSdefault s -> labels_defined s
| Csyntax.LScase (x, x0, s, ls0) ->
  List.append (labels_defined s) (labels_defined_switch ls0)

(** val m_option_map :
    ('a1 -> 'a2 Errors.res) -> 'a1 Types.option -> 'a2 Types.option
    Errors.res **)
let m_option_map f = function
| Types.None -> Errors.OK Types.None
| Types.Some a ->
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f a) (fun b ->
      Obj.magic (Errors.OK (Types.Some b))))

(** val translate_expr_sigma :
    var_types -> Csyntax.expr -> (AST.typ, Cminor_syntax.expr) Types.dPair
    Types.sig0 Errors.res **)
let translate_expr_sigma v e0 =
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (translate_expr v e0)) (fun e' ->
      Obj.magic (Errors.OK { Types.dpi1 =
        (Csyntax.typ_of_type (Csyntax.typeof e0)); Types.dpi2 =
        (Types.pi1 e') })))

(** val add_tmps :
    var_types -> (AST.ident, Csyntax.type0) Types.prod List.list -> var_types **)
let add_tmps vs tmpenv =
  List.foldr (fun idty vs0 ->
    Identifiers.add PreIdentifiers.SymbolTag vs0 idty.Types.fst { Types.fst =
      Local; Types.snd = idty.Types.snd }) vs tmpenv

type tmpgen = { tmp_universe : Identifiers.universe;
                tmp_env : (AST.ident, Csyntax.type0) Types.prod List.list }

(** val tmpgen_rect_Type4 :
    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14549 =
  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14549 in
  h_mk_tmpgen tmp_universe0 tmp_env0 __ __

(** val tmpgen_rect_Type5 :
    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14551 =
  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14551 in
  h_mk_tmpgen tmp_universe0 tmp_env0 __ __

(** val tmpgen_rect_Type3 :
    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14553 =
  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14553 in
  h_mk_tmpgen tmp_universe0 tmp_env0 __ __

(** val tmpgen_rect_Type2 :
    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14555 =
  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14555 in
  h_mk_tmpgen tmp_universe0 tmp_env0 __ __

(** val tmpgen_rect_Type1 :
    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14557 =
  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14557 in
  h_mk_tmpgen tmp_universe0 tmp_env0 __ __

(** val tmpgen_rect_Type0 :
    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14559 =
  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14559 in
  h_mk_tmpgen tmp_universe0 tmp_env0 __ __

(** val tmp_universe : var_types -> tmpgen -> Identifiers.universe **)
let rec tmp_universe vars xxx =
  xxx.tmp_universe

(** val tmp_env :
    var_types -> tmpgen -> (AST.ident, Csyntax.type0) Types.prod List.list **)
let rec tmp_env vars xxx =
  xxx.tmp_env

(** val tmpgen_inv_rect_Type4 :
    var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
    Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let tmpgen_inv_rect_Type4 x1 hterm h1 =
  let hcut = tmpgen_rect_Type4 x1 h1 hterm in hcut __

(** val tmpgen_inv_rect_Type3 :
    var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
    Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let tmpgen_inv_rect_Type3 x1 hterm h1 =
  let hcut = tmpgen_rect_Type3 x1 h1 hterm in hcut __

(** val tmpgen_inv_rect_Type2 :
    var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
    Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let tmpgen_inv_rect_Type2 x1 hterm h1 =
  let hcut = tmpgen_rect_Type2 x1 h1 hterm in hcut __

(** val tmpgen_inv_rect_Type1 :
    var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
    Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let tmpgen_inv_rect_Type1 x1 hterm h1 =
  let hcut = tmpgen_rect_Type1 x1 h1 hterm in hcut __

(** val tmpgen_inv_rect_Type0 :
    var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
    Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let tmpgen_inv_rect_Type0 x1 hterm h1 =
  let hcut = tmpgen_rect_Type0 x1 h1 hterm in hcut __

(** val tmpgen_discr : var_types -> tmpgen -> tmpgen -> __ **)
let tmpgen_discr a1 x y =
  Logic.eq_rect_Type2 x
    (let { tmp_universe = a0; tmp_env = a10 } = x in
    Obj.magic (fun _ dH -> dH __ __ __ __)) y

(** val tmpgen_jmdiscr : var_types -> tmpgen -> tmpgen -> __ **)
let tmpgen_jmdiscr a1 x y =
  Logic.eq_rect_Type2 x
    (let { tmp_universe = a0; tmp_env = a10 } = x in
    Obj.magic (fun _ dH -> dH __ __ __ __)) y

(** val alloc_tmp :
    var_types -> Csyntax.type0 -> tmpgen -> (AST.ident, tmpgen) Types.prod **)
let alloc_tmp vars ty g0 =
  (let { Types.fst = tmp; Types.snd = u } =
     Identifiers.fresh PreIdentifiers.SymbolTag g0.tmp_universe
   in
  (fun _ -> { Types.fst = tmp; Types.snd = { tmp_universe = u; tmp_env =
  (List.Cons ({ Types.fst = tmp; Types.snd = ty }, g0.tmp_env)) } })) __

(** val mklabels :
    labgen -> ((PreIdentifiers.identifier, PreIdentifiers.identifier)
    Types.prod, labgen) Types.prod **)
let rec mklabels ul =
  let res1 = generate_fresh_label ul in
  (let { Types.fst = entry_label; Types.snd = ul1 } = res1 in
  (fun _ ->
  let res2 = generate_fresh_label ul1 in
  (let { Types.fst = exit_label; Types.snd = ul2 } = res2 in
  (fun _ -> { Types.fst = { Types.fst = entry_label; Types.snd =
  exit_label }; Types.snd = ul2 })) __)) __

type convert_flag =
| DoNotConvert
| ConvertTo of PreIdentifiers.identifier * PreIdentifiers.identifier

(** val convert_flag_rect_Type4 :
    'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
    convert_flag -> 'a1 **)
let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function
| DoNotConvert -> h_DoNotConvert
| ConvertTo (x_14581, x_14580) -> h_ConvertTo x_14581 x_14580

(** val convert_flag_rect_Type5 :
    'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
    convert_flag -> 'a1 **)
let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function
| DoNotConvert -> h_DoNotConvert
| ConvertTo (x_14586, x_14585) -> h_ConvertTo x_14586 x_14585

(** val convert_flag_rect_Type3 :
    'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
    convert_flag -> 'a1 **)
let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function
| DoNotConvert -> h_DoNotConvert
| ConvertTo (x_14591, x_14590) -> h_ConvertTo x_14591 x_14590

(** val convert_flag_rect_Type2 :
    'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
    convert_flag -> 'a1 **)
let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function
| DoNotConvert -> h_DoNotConvert
| ConvertTo (x_14596, x_14595) -> h_ConvertTo x_14596 x_14595

(** val convert_flag_rect_Type1 :
    'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
    convert_flag -> 'a1 **)
let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function
| DoNotConvert -> h_DoNotConvert
| ConvertTo (x_14601, x_14600) -> h_ConvertTo x_14601 x_14600

(** val convert_flag_rect_Type0 :
    'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
    convert_flag -> 'a1 **)
let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function
| DoNotConvert -> h_DoNotConvert
| ConvertTo (x_14606, x_14605) -> h_ConvertTo x_14606 x_14605

(** val convert_flag_inv_rect_Type4 :
    convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
    PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
let convert_flag_inv_rect_Type4 hterm h1 h2 =
  let hcut = convert_flag_rect_Type4 h1 h2 hterm in hcut __

(** val convert_flag_inv_rect_Type3 :
    convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
    PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
let convert_flag_inv_rect_Type3 hterm h1 h2 =
  let hcut = convert_flag_rect_Type3 h1 h2 hterm in hcut __

(** val convert_flag_inv_rect_Type2 :
    convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
    PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
let convert_flag_inv_rect_Type2 hterm h1 h2 =
  let hcut = convert_flag_rect_Type2 h1 h2 hterm in hcut __

(** val convert_flag_inv_rect_Type1 :
    convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
    PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
let convert_flag_inv_rect_Type1 hterm h1 h2 =
  let hcut = convert_flag_rect_Type1 h1 h2 hterm in hcut __

(** val convert_flag_inv_rect_Type0 :
    convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
    PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
let convert_flag_inv_rect_Type0 hterm h1 h2 =
  let hcut = convert_flag_rect_Type0 h1 h2 hterm in hcut __

(** val convert_flag_discr : convert_flag -> convert_flag -> __ **)
let convert_flag_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | DoNotConvert -> Obj.magic (fun _ dH -> dH)
     | ConvertTo (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val convert_flag_jmdiscr : convert_flag -> convert_flag -> __ **)
let convert_flag_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | DoNotConvert -> Obj.magic (fun _ dH -> dH)
     | ConvertTo (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val labels_of_flag :
    convert_flag -> PreIdentifiers.identifier List.list **)
let rec labels_of_flag = function
| DoNotConvert -> List.Nil
| ConvertTo (continue, break) ->
  List.Cons (continue, (List.Cons (break, List.Nil)))

(** val translate_statement :
    var_types -> tmpgen -> labgen -> lenv -> convert_flag -> AST.typ
    Types.option -> Csyntax.statement -> ((tmpgen, labgen) Types.prod,
    Cminor_syntax.stmt) Types.prod Types.sig0 Errors.res **)
let rec translate_statement vars uv ul lbls flag rettyp = function
| Csyntax.Sskip ->
  Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; Types.snd =
    Cminor_syntax.St_skip }
| Csyntax.Sassign (e1, e2) ->
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (translate_expr vars e2)) (fun e2' ->
      Monad.m_bind0 (Monad.max_def Errors.res0) (translate_dest vars e1)
        (fun dest ->
        match dest with
        | IdDest (id, ty) ->
          Monad.m_bind0 (Monad.max_def Errors.res0)
            (Obj.magic
              (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e2))
                (Csyntax.typ_of_type ty) e2')) (fun e2'0 ->
            Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd =
              ul }; Types.snd = (Cminor_syntax.St_assign
              ((Csyntax.typ_of_type ty), id, (Types.pi1 e2'0))) }))
        | MemDest e1' ->
          Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd =
            ul }; Types.snd = (Cminor_syntax.St_store
            ((Csyntax.typ_of_type (Csyntax.typeof e2)), (Types.pi1 e1'),
            (Types.pi1 e2'))) }))))
| Csyntax.Scall (ret, ef, args) ->
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (translate_expr vars ef)) (fun ef' ->
      Monad.m_bind0 (Monad.max_def Errors.res0)
        (Obj.magic
          (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof ef)) AST.ASTptr
            ef')) (fun ef'0 ->
        Monad.m_bind0 (Monad.max_def Errors.res0)
          (Errors.mmap_sigma (Obj.magic (translate_expr_sigma vars)) args)
          (fun args' ->
          match ret with
          | Types.None ->
            Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd =
              ul }; Types.snd = (Cminor_syntax.St_call (Types.None,
              (Types.pi1 ef'0), (Types.pi1 args'))) })
          | Types.Some e1 ->
            Monad.m_bind0 (Monad.max_def Errors.res0)
              (translate_dest vars e1) (fun dest ->
              match dest with
              | IdDest (id, ty) ->
                Obj.magic (Errors.OK { Types.fst = { Types.fst = uv;
                  Types.snd = ul }; Types.snd = (Cminor_syntax.St_call
                  ((Types.Some { Types.fst = id; Types.snd =
                  (Csyntax.typ_of_type ty) }), (Types.pi1 ef'0),
                  (Types.pi1 args'))) })
              | MemDest e1' ->
                (let { Types.fst = tmp; Types.snd = uv1 } =
                   alloc_tmp vars (Csyntax.typeof e1) uv
                 in
                (fun _ ->
                Obj.magic (Errors.OK { Types.fst = { Types.fst = uv1;
                  Types.snd = ul }; Types.snd = (Cminor_syntax.St_seq
                  ((Cminor_syntax.St_call ((Types.Some { Types.fst = tmp;
                  Types.snd = (Csyntax.typ_of_type (Csyntax.typeof e1)) }),
                  (Types.pi1 ef'0), (Types.pi1 args'))),
                  (Cminor_syntax.St_store
                  ((Csyntax.typ_of_type (Csyntax.typeof e1)),
                  (Types.pi1 e1'), (Cminor_syntax.Id
                  ((Csyntax.typ_of_type (Csyntax.typeof e1)), tmp)))))) })))
                  __)))))
| Csyntax.Ssequence (s1, s2) ->
  Obj.magic
    (Monad.m_sigbind2 (Monad.max_def Errors.res0)
      (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1))
      (fun fgens1 s1' _ ->
      Monad.m_sigbind2 (Monad.max_def Errors.res0)
        (Obj.magic
          (translate_statement vars fgens1.Types.fst fgens1.Types.snd lbls
            flag rettyp s2)) (fun fgens2 s2' _ ->
        Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd =
          (Cminor_syntax.St_seq (s1', s2')) }))))
| Csyntax.Sifthenelse (e1, s1, s2) ->
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (translate_expr vars e1)) (fun e1' ->
      (match Csyntax.typ_of_type (Csyntax.typeof e1) with
       | AST.ASTint (x, x0) ->
         (fun e1'0 ->
           Monad.m_sigbind2 (Monad.max_def Errors.res0)
             (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1))
             (fun fgens1 s1' _ ->
             Monad.m_sigbind2 (Monad.max_def Errors.res0)
               (Obj.magic
                 (translate_statement vars fgens1.Types.fst fgens1.Types.snd
                   lbls flag rettyp s2)) (fun fgens2 s2' _ ->
               Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd =
                 (Cminor_syntax.St_ifthenelse (x, x0, (Types.pi1 e1'0), s1',
                 s2')) }))))
       | AST.ASTptr ->
         (fun x ->
           Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
        e1'))
| Csyntax.Swhile (e1, s1) ->
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (translate_expr vars e1)) (fun e1' ->
      (match Csyntax.typ_of_type (Csyntax.typeof e1) with
       | AST.ASTint (x, x0) ->
         (fun e1'0 ->
           (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in
           (fun _ ->
           (let { Types.fst = entry; Types.snd = exit } = labels in
           (fun _ ->
           Monad.m_sigbind2 (Monad.max_def Errors.res0)
             (Obj.magic
               (translate_statement vars uv ul1 lbls (ConvertTo (entry,
                 exit)) rettyp s1)) (fun fgens2 s1' _ ->
             let converted_loop = Cminor_syntax.St_label (entry,
               (Cminor_syntax.St_seq ((Cminor_syntax.St_ifthenelse (x, x0,
               (Types.pi1 e1'0), (Cminor_syntax.St_seq (s1',
               (Cminor_syntax.St_goto entry))), Cminor_syntax.St_skip)),
               (Cminor_syntax.St_label (exit, Cminor_syntax.St_skip)))))
             in
             Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd =
               converted_loop })))) __)) __)
       | AST.ASTptr ->
         (fun x ->
           Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
        e1'))
| Csyntax.Sdowhile (e1, s1) ->
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (translate_expr vars e1)) (fun e1' ->
      (match Csyntax.typ_of_type (Csyntax.typeof e1) with
       | AST.ASTint (x, x0) ->
         (fun e1'0 ->
           (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in
           (fun _ ->
           (let { Types.fst = condexpr; Types.snd = exit } = labels in
           (fun _ ->
           let { Types.fst = body; Types.snd = ul2 } =
             Types.pi1 (generate_fresh_label ul1)
           in
           Monad.m_sigbind2 (Monad.max_def Errors.res0)
             (Obj.magic
               (translate_statement vars uv ul2 lbls (ConvertTo (condexpr,
                 exit)) rettyp s1)) (fun fgens2 s1' _ ->
             let converted_loop = Cminor_syntax.St_seq ((Cminor_syntax.St_seq
               ((Cminor_syntax.St_goto body), (Cminor_syntax.St_label
               (condexpr, (Cminor_syntax.St_ifthenelse (x, x0,
               (Types.pi1 e1'0), (Cminor_syntax.St_label (body,
               (Cminor_syntax.St_seq (s1', (Cminor_syntax.St_goto
               condexpr))))), Cminor_syntax.St_skip)))))),
               (Cminor_syntax.St_label (exit, Cminor_syntax.St_skip)))
             in
             Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd =
               converted_loop })))) __)) __)
       | AST.ASTptr ->
         (fun x ->
           Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
        e1'))
| Csyntax.Sfor (s1, e1, s2, s3) ->
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (translate_expr vars e1)) (fun e1' ->
      (match Csyntax.typ_of_type (Csyntax.typeof e1) with
       | AST.ASTint (x, x0) ->
         (fun e1'0 ->
           (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in
           (fun _ ->
           (let { Types.fst = continue; Types.snd = exit } = labels in
           (fun _ ->
           let { Types.fst = entry; Types.snd = ul2 } =
             Types.pi1 (generate_fresh_label ul1)
           in
           Monad.m_sigbind2 (Monad.max_def Errors.res0)
             (Obj.magic
               (translate_statement vars uv ul2 lbls flag rettyp s1))
             (fun fgens2 s1' _ ->
             Monad.m_sigbind2 (Monad.max_def Errors.res0)
               (Obj.magic
                 (translate_statement vars fgens2.Types.fst fgens2.Types.snd
                   lbls flag rettyp s2)) (fun fgens3 s2' _ ->
               Monad.m_sigbind2 (Monad.max_def Errors.res0)
                 (Obj.magic
                   (translate_statement vars fgens3.Types.fst
                     fgens3.Types.snd lbls (ConvertTo (continue, exit))
                     rettyp s3)) (fun fgens4 s3' _ ->
                 let converted_loop = Cminor_syntax.St_seq (s1',
                   (Cminor_syntax.St_label (entry, (Cminor_syntax.St_seq
                   ((Cminor_syntax.St_ifthenelse (x, x0, (Types.pi1 e1'0),
                   (Cminor_syntax.St_seq (s3', (Cminor_syntax.St_label
                   (continue, (Cminor_syntax.St_seq (s2',
                   (Cminor_syntax.St_goto entry))))))),
                   Cminor_syntax.St_skip)), (Cminor_syntax.St_label (exit,
                   Cminor_syntax.St_skip)))))))
                 in
                 Obj.magic (Errors.OK { Types.fst = fgens4; Types.snd =
                   converted_loop })))))) __)) __)
       | AST.ASTptr ->
         (fun x ->
           Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
        e1'))
| Csyntax.Sbreak ->
  (match flag with
   | DoNotConvert -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.FIXME))
   | ConvertTo (continue_label, break_label) ->
     (fun _ -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul };
       Types.snd = (Cminor_syntax.St_goto break_label) })) __
| Csyntax.Scontinue ->
  (match flag with
   | DoNotConvert -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.FIXME))
   | ConvertTo (continue_label, break_label) ->
     (fun _ -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul };
       Types.snd = (Cminor_syntax.St_goto continue_label) })) __
| Csyntax.Sreturn ret ->
  (match ret with
   | Types.None ->
     (match rettyp with
      | Types.None ->
        Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul };
          Types.snd = (Cminor_syntax.St_return Types.None) }
      | Types.Some x ->
        Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))
   | Types.Some e1 ->
     (match rettyp with
      | Types.None -> Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
      | Types.Some rty ->
        Obj.magic
          (Monad.m_bind0 (Monad.max_def Errors.res0)
            (Obj.magic (translate_expr vars e1)) (fun e1' ->
            Monad.m_bind0 (Monad.max_def Errors.res0)
              (Obj.magic
                (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e1)) rty
                  e1')) (fun e1'0 ->
              Obj.magic (Errors.OK { Types.fst = { Types.fst = uv;
                Types.snd = ul }; Types.snd = (Cminor_syntax.St_return
                (Types.Some { Types.dpi1 = rty; Types.dpi2 =
                (Types.pi1 e1'0) })) }))))))
| Csyntax.Sswitch (e1, ls) -> Errors.Error (Errors.msg ErrorMessages.FIXME)
| Csyntax.Slabel (l, s1) ->
  Errors.bind_eq (lookup_label lbls l) (fun l' _ ->
    Obj.magic
      (Monad.m_sigbind2 (Monad.max_def Errors.res0)
        (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1))
        (fun fgens1 s1' _ ->
        Obj.magic (Errors.OK { Types.fst = fgens1; Types.snd =
          (Cminor_syntax.St_label (l', s1')) }))))
| Csyntax.Sgoto l ->
  Errors.bind_eq (lookup_label lbls l) (fun l' _ -> Errors.OK { Types.fst =
    { Types.fst = uv; Types.snd = ul }; Types.snd = (Cminor_syntax.St_goto
    l') })
| Csyntax.Scost (l, s1) ->
  Obj.magic
    (Monad.m_sigbind2 (Monad.max_def Errors.res0)
      (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1))
      (fun fgens1 s1' _ ->
      Obj.magic (Errors.OK { Types.fst = fgens1; Types.snd =
        (Cminor_syntax.St_cost (l, s1')) })))

(** val alloc_params :
    var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag ->
    AST.typ Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list
    -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod
    Types.sig0 -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt)
    Types.prod Types.sig0 Errors.res **)
let alloc_params vars lbls statement0 uv ul rettyp params s =
  Util.foldl (fun su it ->
    let { Types.fst = id; Types.snd = ty } = it in
    Obj.magic
      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
        (fun eta2862 ->
        let result = eta2862 in
        (let { Types.fst = fgens1; Types.snd = s0 } = result in
        (fun _ ->
        Obj.magic
          (Errors.bind2_eq (lookup' vars id) (fun t ty' _ ->
            (match t with
             | Global x ->
               (fun _ -> Errors.Error (List.Cons ((Errors.MSG
                 ErrorMessages.ParamGlobalMixup), (List.Cons ((Errors.CTX
                 (PreIdentifiers.SymbolTag, id)), List.Nil)))))
             | Stack n ->
               (fun _ -> Errors.OK { Types.fst = fgens1; Types.snd =
                 (Cminor_syntax.St_seq ((Cminor_syntax.St_store
                 ((Csyntax.typ_of_type ty'), (Cminor_syntax.Cst (AST.ASTptr,
                 (FrontEndOps.Oaddrstack n))), (Cminor_syntax.Id
                 ((Csyntax.typ_of_type ty'), id)))), s0)) })
             | Local -> (fun _ -> Errors.OK result)) __)))) __))) (Errors.OK
    s) params

(** val populate_lenv :
    AST.ident List.list -> labgen -> lenv -> (lenv Types.sig0, labgen)
    Types.prod Errors.res **)
let rec populate_lenv ls ul lbls =
  match ls with
  | List.Nil -> Errors.OK { Types.fst = lbls; Types.snd = ul }
  | List.Cons (l, t) ->
    (match lookup_label lbls l with
     | Errors.OK x ->
       (fun _ -> Errors.Error (Errors.msg ErrorMessages.DuplicateLabel))
     | Errors.Error x ->
       (fun _ ->
         let ret = generate_fresh_label ul in
         Obj.magic
           (Monad.m_bind2 (Monad.max_def Errors.res0)
             (Obj.magic
               (populate_lenv t ret.Types.snd
                 (Identifiers.add PreIdentifiers.SymbolTag lbls l
                   ret.Types.fst))) (fun packed_lbls ul1 ->
             let lbls' = packed_lbls in
             Obj.magic (Errors.OK { Types.fst = lbls'; Types.snd = ul1 })))))
      __

(** val build_label_env :
    Csyntax.statement -> (lenv Types.sig0, labgen) Types.prod Errors.res **)
let build_label_env body =
  let initial_labgen = { labuniverse =
    (Identifiers.new_universe PreIdentifiers.Label); label_genlist =
    List.Nil }
  in
  Obj.magic
    (Monad.m_bind2 (Monad.max_def Errors.res0)
      (Obj.magic
        (populate_lenv (labels_defined body) initial_labgen
          (Identifiers.empty_map PreIdentifiers.SymbolTag)))
      (fun label_map u ->
      let lbls = Types.pi1 label_map in
      Obj.magic (Errors.OK { Types.fst = lbls; Types.snd = u })))

(** val translate_function :
    Identifiers.universe -> ((AST.ident, AST.region) Types.prod,
    Csyntax.type0) Types.prod List.list -> Csyntax.function0 ->
    Cminor_syntax.internal_function Errors.res **)
let translate_function tmpuniverse globals f =
  Obj.magic
    (Monad.m_bind2 (Monad.max_def Errors.res0)
      (Obj.magic (build_label_env f.Csyntax.fn_body)) (fun env_pack ul ->
      let lbls = env_pack in
      (let { Types.fst = vartypes; Types.snd = stacksize } =
         characterise_vars globals f
       in
      (fun _ ->
      let uv = { tmp_universe = tmpuniverse; tmp_env = List.Nil } in
      Monad.m_bind0 (Monad.max_def Errors.res0)
        (Obj.magic
          (translate_statement vartypes uv ul lbls DoNotConvert
            (Csyntax.opttyp_of_type f.Csyntax.fn_return) f.Csyntax.fn_body))
        (fun s0 ->
        Monad.m_sigbind2 (Monad.max_def Errors.res0)
          (Obj.magic
            (alloc_params vartypes lbls f.Csyntax.fn_body uv DoNotConvert
              (Csyntax.opttyp_of_type f.Csyntax.fn_return)
              f.Csyntax.fn_params s0)) (fun fgens s1 _ ->
          let params =
            List.map (fun v -> { Types.fst = v.Types.fst; Types.snd =
              (Csyntax.typ_of_type v.Types.snd) }) f.Csyntax.fn_params
          in
          let vars =
            List.map (fun v -> { Types.fst = v.Types.fst; Types.snd =
              (Csyntax.typ_of_type v.Types.snd) })
              (List.append fgens.Types.fst.tmp_env f.Csyntax.fn_vars)
          in
          Monad.m_bind0 (Monad.max_def Errors.res0)
            (Obj.magic
              (Identifiers.check_distinct_env PreIdentifiers.SymbolTag
                (List.append params vars))) (fun _ ->
            Obj.magic (Errors.OK { Cminor_syntax.f_return =
              (Csyntax.opttyp_of_type f.Csyntax.fn_return);
              Cminor_syntax.f_params = params; Cminor_syntax.f_vars = vars;
              Cminor_syntax.f_stacksize = stacksize; Cminor_syntax.f_body =
              s1 })))))) __))

(** val translate_fundef :
    Identifiers.universe -> ((AST.ident, AST.region) Types.prod,
    Csyntax.type0) Types.prod List.list -> Csyntax.clight_fundef ->
    Cminor_syntax.internal_function AST.fundef Errors.res **)
let translate_fundef tmpuniverse globals f =
  (match f with
   | Csyntax.CL_Internal fn ->
     (fun _ ->
       Obj.magic
         (Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (translate_function tmpuniverse globals fn))
           (fun fn' -> Obj.magic (Errors.OK (AST.Internal fn')))))
   | Csyntax.CL_External (fn, argtys, retty) ->
     (fun _ -> Errors.OK (AST.External { AST.ef_id = fn; AST.ef_sig =
       (Csyntax.signature_of_type argtys retty) }))) __

(** val map_partial_All :
    ('a1 -> __ -> 'a2 Errors.res) -> 'a1 List.list -> 'a2 List.list
    Errors.res **)
let rec map_partial_All f l =
  (match l with
   | List.Nil -> (fun _ -> Errors.OK List.Nil)
   | List.Cons (hd0, tl) ->
     (fun _ ->
       Obj.magic
         (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f hd0 __)
           (fun b_hd ->
           Monad.m_bind0 (Monad.max_def Errors.res0)
             (Obj.magic (map_partial_All f tl)) (fun b_tl ->
             Obj.magic (Errors.OK (List.Cons (b_hd, b_tl)))))))) __

(** val clight_to_cminor :
    Csyntax.clight_program -> Cminor_syntax.cminor_program Errors.res **)
let clight_to_cminor p =
  let tmpuniverse = Fresh.universe_for_program p in
  let fun_globals =
    List.map (fun idf -> { Types.fst = { Types.fst = idf.Types.fst;
      Types.snd = AST.Code }; Types.snd =
      (Csyntax.type_of_fundef idf.Types.snd) }) p.AST.prog_funct
  in
  let var_globals =
    List.map (fun v -> { Types.fst = { Types.fst = v.Types.fst.Types.fst;
      Types.snd = v.Types.fst.Types.snd }; Types.snd =
      v.Types.snd.Types.snd }) p.AST.prog_vars
  in
  let globals = List.append fun_globals var_globals in
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic
        (map_partial_All (fun x _ ->
          Obj.magic
            (Monad.m_bind0 (Monad.max_def Errors.res0)
              (Obj.magic (translate_fundef tmpuniverse globals x.Types.snd))
              (fun f ->
              Obj.magic (Errors.OK { Types.fst = x.Types.fst; Types.snd =
                f })))) p.AST.prog_funct)) (fun fns ->
      Obj.magic (Errors.OK { AST.prog_vars =
        (List.map (fun v -> { Types.fst = v.Types.fst; Types.snd =
          v.Types.snd.Types.fst }) p.AST.prog_vars); AST.prog_funct = fns;
        AST.prog_main = p.AST.prog_main })))