open Preamble

open CostLabel

open Coqlib

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Jmeq

open Russell

open List

open Setoids

open Monad

open Option

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 Smallstep

open Extra_bool

open FrontEndVal

open Hide

open ByteValues

open GenMem

open FrontEndMem

open Globalenvs

open Csem

open SmallstepExec

open Division

open Z

open BitVectorZ

open Pointers

open Values

open Events

open IOMonad

open IO

open Cexec

open Casts

open CexecInd

open Sets

open Listb

open Star

open Frontend_misc

(** val reduce_bits :
    Nat.nat -> Nat.nat -> Bool.bool -> BitVector.bitVector ->
    BitVector.bitVector Types.option **)
let rec reduce_bits n m exp v =
  (match n with
   | Nat.O -> (fun v0 -> Types.Some v0)
   | Nat.S n' ->
     (fun v0 ->
       match BitVector.eq_b (Vector.head' (Nat.plus n' (Nat.S m)) v0) exp with
       | Bool.True ->
         reduce_bits n' m exp (Vector.tail (Nat.plus n' (Nat.S m)) v0)
       | Bool.False -> Types.None)) v

(** val pred_bitsize_of_intsize : AST.intsize -> Nat.nat **)
let pred_bitsize_of_intsize sz =
  Nat.pred (AST.bitsize_of_intsize sz)

(** val signed : AST.signedness -> Bool.bool **)
let signed = function
| AST.Signed -> Bool.True
| AST.Unsigned -> Bool.False

(** val simplify_int :
    AST.intsize -> AST.intsize -> AST.signedness -> AST.signedness ->
    AST.bvint -> AST.bvint Types.option **)
let rec simplify_int sz sz' sg sg' i =
  let bit =
    Bool.andb (signed sg)
      (Vector.head'
        (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          Nat.O)))))))
          (Nat.times (AST.pred_size_intsize sz) (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) i)
  in
  (match Extranat.nat_compare (pred_bitsize_of_intsize sz)
           (pred_bitsize_of_intsize sz') with
   | Extranat.Nat_lt (x, x0) -> (fun i0 -> Types.None)
   | Extranat.Nat_eq x -> (fun i0 -> Types.Some i0)
   | Extranat.Nat_gt (x, y) ->
     (fun i0 ->
       match reduce_bits (Nat.S x) y bit i0 with
       | Types.None -> Types.None
       | Types.Some i' ->
         (match signed sg' with
          | Bool.True ->
            (match BitVector.eq_b bit (Vector.head' y i') with
             | Bool.True -> Types.Some i'
             | Bool.False -> Types.None)
          | Bool.False -> Types.Some i'))) i

(** val size_lt_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum **)
let size_lt_dec = function
| AST.I8 ->
  (fun clearme0 ->
    match clearme0 with
    | AST.I8 -> Types.Inr __
    | AST.I16 -> Types.Inl __
    | AST.I32 -> Types.Inl __)
| AST.I16 ->
  (fun clearme0 ->
    match clearme0 with
    | AST.I8 -> Types.Inr __
    | AST.I16 -> Types.Inr __
    | AST.I32 -> Types.Inl __)
| AST.I32 ->
  (fun clearme0 ->
    match clearme0 with
    | AST.I8 -> Types.Inr __
    | AST.I16 -> Types.Inr __
    | AST.I32 -> Types.Inr __)

(** val size_not_lt_to_ge :
    AST.intsize -> AST.intsize -> (__, __) Types.sum **)
let size_not_lt_to_ge clearme sz2 =
  (match clearme with
   | AST.I8 ->
     (fun clearme0 ->
       match clearme0 with
       | AST.I8 -> (fun _ -> Types.Inl __)
       | AST.I16 -> (fun _ -> Types.Inr __)
       | AST.I32 -> (fun _ -> Types.Inr __))
   | AST.I16 ->
     (fun clearme0 ->
       match clearme0 with
       | AST.I8 -> (fun _ -> Types.Inr __)
       | AST.I16 -> (fun _ -> Types.Inl __)
       | AST.I32 -> (fun _ -> Types.Inr __))
   | AST.I32 ->
     (fun clearme0 ->
       match clearme0 with
       | AST.I8 -> (fun _ -> Types.Inr __)
       | AST.I16 -> (fun _ -> Types.Inr __)
       | AST.I32 -> (fun _ -> Types.Inl __))) sz2 __

(** val sign_eq_dect :
    AST.signedness -> AST.signedness -> (__, __) Types.sum **)
let sign_eq_dect = function
| AST.Signed ->
  (fun clearme0 ->
    match clearme0 with
    | AST.Signed -> TypeComparison.sg_eq_dec AST.Signed AST.Signed
    | AST.Unsigned -> TypeComparison.sg_eq_dec AST.Signed AST.Unsigned)
| AST.Unsigned ->
  (fun clearme0 ->
    match clearme0 with
    | AST.Signed -> TypeComparison.sg_eq_dec AST.Unsigned AST.Signed
    | AST.Unsigned -> TypeComparison.sg_eq_dec AST.Unsigned AST.Unsigned)

(** val necessary_conditions :
    AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness ->
    Bool.bool **)
let necessary_conditions src_sz src_sg target_sz target_sg =
  match size_lt_dec target_sz src_sz with
  | Types.Inl _ -> Bool.True
  | Types.Inr _ ->
    (match TypeComparison.sz_eq_dec target_sz src_sz with
     | Types.Inl _ ->
       (match sign_eq_dect src_sg target_sg with
        | Types.Inl _ -> Bool.False
        | Types.Inr _ -> Bool.True)
     | Types.Inr _ -> Bool.False)

(** val assert_int_value :
    Values.val0 Types.option -> AST.intsize -> BitVector.bitVector
    Types.option **)
let rec assert_int_value v expected_size =
  match v with
  | Types.None -> Types.None
  | Types.Some v0 ->
    (match v0 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz, i) ->
       (match TypeComparison.sz_eq_dec sz expected_size with
        | Types.Inl _ ->
          Types.Some
            (Extralib.eq_rect_Type0_r expected_size (fun i0 -> i0) sz i)
        | Types.Inr _ -> Types.None)
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)

(** val binop_simplifiable : Csyntax.binary_operation -> Bool.bool **)
let binop_simplifiable = function
| Csyntax.Oadd -> Bool.True
| Csyntax.Osub -> Bool.True
| Csyntax.Omul -> Bool.False
| Csyntax.Odiv -> Bool.False
| Csyntax.Omod -> Bool.False
| Csyntax.Oand -> Bool.False
| Csyntax.Oor -> Bool.False
| Csyntax.Oxor -> Bool.False
| Csyntax.Oshl -> Bool.False
| Csyntax.Oshr -> Bool.False
| Csyntax.Oeq -> Bool.False
| Csyntax.One -> Bool.False
| Csyntax.Olt -> Bool.False
| Csyntax.Ogt -> Bool.False
| Csyntax.Ole -> Bool.False
| Csyntax.Oge -> Bool.False

(** val simplify_expr :
    Csyntax.expr -> AST.intsize -> AST.signedness -> (Bool.bool,
    Csyntax.expr) Types.prod Types.sig0 **)
let rec simplify_expr e target_sz target_sg =
  (let Csyntax.Expr (ed, ty) = e in
  (fun _ ->
  (match ed with
   | Csyntax.Econst_int (cst_sz, i) ->
     (fun _ ->
       (match ty with
        | Csyntax.Tvoid ->
          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
        | Csyntax.Tint (ty_sz, sg) ->
          (fun _ ->
            match TypeComparison.sz_eq_dec cst_sz ty_sz with
            | Types.Inl _ ->
              (match TypeComparison.type_eq_dec ty (Csyntax.Tint (target_sz,
                       target_sg)) with
               | Types.Inl _ -> { Types.fst = Bool.True; Types.snd = e }
               | Types.Inr _ ->
                 (match simplify_int cst_sz target_sz sg target_sg i with
                  | Types.None ->
                    (fun _ -> { Types.fst = Bool.False; Types.snd = e })
                  | Types.Some i' ->
                    (fun _ -> { Types.fst = Bool.True; Types.snd =
                      (Csyntax.Expr ((Csyntax.Econst_int (target_sz, i')),
                      (Csyntax.Tint (target_sz, target_sg)))) })) __)
            | Types.Inr _ -> { Types.fst = Bool.False; Types.snd = e })
        | Csyntax.Tpointer x ->
          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
        | Csyntax.Tarray (x, x0) ->
          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
        | Csyntax.Tfunction (x, x0) ->
          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
        | Csyntax.Tstruct (x, x0) ->
          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
        | Csyntax.Tunion (x, x0) ->
          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
        | Csyntax.Tcomp_ptr x ->
          (fun _ -> { Types.fst = Bool.False; Types.snd = e })) __)
   | Csyntax.Evar id ->
     (fun _ -> { Types.fst =
       (TypeComparison.type_eq ty (Csyntax.Tint (target_sz, target_sg)));
       Types.snd = (Csyntax.Expr (ed, ty)) })
   | Csyntax.Ederef e1 ->
     (fun _ ->
       (let e2 = simplify_inside e1 in
         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
         ((Csyntax.Ederef e2), ty)) })) __)
   | Csyntax.Eaddrof e1 ->
     (fun _ ->
       (let e2 = simplify_inside e1 in
         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
         ((Csyntax.Eaddrof e2), ty)) })) __)
   | Csyntax.Eunop (op, e1) ->
     (fun _ ->
       (let e2 = simplify_inside e1 in
         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
         ((Csyntax.Eunop (op, e2)), ty)) })) __)
   | Csyntax.Ebinop (op, lhs, rhs) ->
     (fun _ ->
       (match binop_simplifiable op with
        | Bool.True ->
          (fun _ ->
            match TypeComparison.assert_type_eq ty (Csyntax.typeof lhs) with
            | Errors.OK _ ->
              (match TypeComparison.assert_type_eq (Csyntax.typeof lhs)
                       (Csyntax.typeof rhs) with
               | Errors.OK _ ->
                 (let eta2033 = simplify_expr lhs target_sz target_sg in
                   (fun _ ->
                   (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } =
                      eta2033
                    in
                   (fun _ ->
                   (let eta2032 = simplify_expr rhs target_sz target_sg in
                     (fun _ ->
                     (let { Types.fst = desired_type_rhs; Types.snd =
                        rhs1 } = eta2032
                      in
                     (fun _ ->
                     (match Bool.andb desired_type_lhs desired_type_rhs with
                      | Bool.True ->
                        (fun _ -> { Types.fst = Bool.True; Types.snd =
                          (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)),
                          (Csyntax.Tint (target_sz, target_sg)))) })
                      | Bool.False ->
                        (fun _ ->
                          (let lhs10 = simplify_inside lhs in
                            (fun _ ->
                            (let rhs10 = simplify_inside rhs in
                              (fun _ -> { Types.fst = Bool.False; Types.snd =
                              (Csyntax.Expr ((Csyntax.Ebinop (op, lhs10,
                              rhs10)), ty)) })) __)) __)) __)) __)) __)) __))
                   __
               | Errors.Error x ->
                 (let lhs1 = simplify_inside lhs in
                   (fun _ ->
                   (let rhs1 = simplify_inside rhs in
                     (fun _ -> { Types.fst = Bool.False; Types.snd =
                     (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)),
                     ty)) })) __)) __)
            | Errors.Error x ->
              (let lhs1 = simplify_inside lhs in
                (fun _ ->
                (let rhs1 = simplify_inside rhs in
                  (fun _ -> { Types.fst = Bool.False; Types.snd =
                  (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)) }))
                  __)) __)
        | Bool.False ->
          (fun _ ->
            (let lhs1 = simplify_inside lhs in
              (fun _ ->
              (let rhs1 = simplify_inside rhs in
                (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
                ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)) })) __)) __)) __)
   | Csyntax.Ecast (cast_ty, castee) ->
     (fun _ ->
       (match cast_ty with
        | Csyntax.Tvoid ->
          (fun _ ->
            (let castee1 = simplify_inside castee in
              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
        | Csyntax.Tint (cast_sz, cast_sg) ->
          (fun _ ->
            match TypeComparison.type_eq_dec ty cast_ty with
            | Types.Inl _ ->
              (match necessary_conditions cast_sz cast_sg target_sz target_sg with
               | Bool.True ->
                 (fun _ ->
                   (let eta2035 = simplify_expr castee target_sz target_sg in
                     (fun _ ->
                     (let { Types.fst = desired_type; Types.snd = castee1 } =
                        eta2035
                      in
                     (fun _ ->
                     (match desired_type with
                      | Bool.True ->
                        (fun _ -> { Types.fst = Bool.True; Types.snd =
                          castee1 })
                      | Bool.False ->
                        (fun _ ->
                          (let eta2034 = simplify_expr castee cast_sz cast_sg
                           in
                            (fun _ ->
                            (let { Types.fst = desired_type2; Types.snd =
                               castee2 } = eta2034
                             in
                            (fun _ ->
                            (match desired_type2 with
                             | Bool.True ->
                               (fun _ -> { Types.fst = Bool.False;
                                 Types.snd = castee2 })
                             | Bool.False ->
                               (fun _ -> { Types.fst = Bool.False;
                                 Types.snd = (Csyntax.Expr ((Csyntax.Ecast
                                 (ty, castee2)), cast_ty)) })) __)) __)) __))
                       __)) __)) __)
               | Bool.False ->
                 (fun _ ->
                   (let eta2036 = simplify_expr castee cast_sz cast_sg in
                     (fun _ ->
                     (let { Types.fst = desired_type2; Types.snd =
                        castee2 } = eta2036
                      in
                     (fun _ ->
                     (match desired_type2 with
                      | Bool.True ->
                        (fun _ -> { Types.fst = Bool.False; Types.snd =
                          castee2 })
                      | Bool.False ->
                        (fun _ -> { Types.fst = Bool.False; Types.snd =
                          (Csyntax.Expr ((Csyntax.Ecast (ty, castee2)),
                          cast_ty)) })) __)) __)) __)) __
            | Types.Inr _ ->
              (let castee1 = simplify_inside castee in
                (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
                ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
        | Csyntax.Tpointer x ->
          (fun _ ->
            (let castee1 = simplify_inside castee in
              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
        | Csyntax.Tarray (x, x0) ->
          (fun _ ->
            (let castee1 = simplify_inside castee in
              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
        | Csyntax.Tfunction (x, x0) ->
          (fun _ ->
            (let castee1 = simplify_inside castee in
              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
        | Csyntax.Tstruct (x, x0) ->
          (fun _ ->
            (let castee1 = simplify_inside castee in
              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
        | Csyntax.Tunion (x, x0) ->
          (fun _ ->
            (let castee1 = simplify_inside castee in
              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
        | Csyntax.Tcomp_ptr x ->
          (fun _ ->
            (let castee1 = simplify_inside castee in
              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)) __)
   | Csyntax.Econdition (cond, iftrue, iffalse) ->
     (fun _ ->
       (let cond1 = simplify_inside cond in
         (fun _ ->
         match TypeComparison.assert_type_eq ty (Csyntax.typeof iftrue) with
         | Errors.OK _ ->
           (match TypeComparison.assert_type_eq (Csyntax.typeof iftrue)
                    (Csyntax.typeof iffalse) with
            | Errors.OK _ ->
              (let eta2038 = simplify_expr iftrue target_sz target_sg in
                (fun _ ->
                (let { Types.fst = desired_true; Types.snd = iftrue1 } =
                   eta2038
                 in
                (fun _ ->
                (let eta2037 = simplify_expr iffalse target_sz target_sg in
                  (fun _ ->
                  (let { Types.fst = desired_false; Types.snd = iffalse1 } =
                     eta2037
                   in
                  (fun _ ->
                  (match Bool.andb desired_true desired_false with
                   | Bool.True ->
                     (fun _ -> { Types.fst = Bool.True; Types.snd =
                       (Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
                       iffalse1)), (Csyntax.Tint (target_sz, target_sg)))) })
                   | Bool.False ->
                     (fun _ ->
                       (let iftrue10 = simplify_inside iftrue in
                         (fun _ ->
                         (let iffalse10 = simplify_inside iffalse in
                           (fun _ -> { Types.fst = Bool.False; Types.snd =
                           (Csyntax.Expr ((Csyntax.Econdition (cond1,
                           iftrue10, iffalse10)), ty)) })) __)) __)) __)) __))
                  __)) __)) __
            | Errors.Error x ->
              (let iftrue1 = simplify_inside iftrue in
                (fun _ ->
                (let iffalse1 = simplify_inside iffalse in
                  (fun _ -> { Types.fst = Bool.False; Types.snd =
                  (Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
                  iffalse1)), ty)) })) __)) __)
         | Errors.Error x ->
           (let iftrue1 = simplify_inside iftrue in
             (fun _ ->
             (let iffalse1 = simplify_inside iffalse in
               (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
               ((Csyntax.Econdition (cond1, iftrue1, iffalse1)), ty)) })) __))
             __)) __)
   | Csyntax.Eandbool (lhs, rhs) ->
     (fun _ ->
       (let lhs1 = simplify_inside lhs in
         (fun _ ->
         (let rhs1 = simplify_inside rhs in
           (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
           ((Csyntax.Eandbool (lhs1, rhs1)), ty)) })) __)) __)
   | Csyntax.Eorbool (lhs, rhs) ->
     (fun _ ->
       (let lhs1 = simplify_inside lhs in
         (fun _ ->
         (let rhs1 = simplify_inside rhs in
           (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
           ((Csyntax.Eorbool (lhs1, rhs1)), ty)) })) __)) __)
   | Csyntax.Esizeof t ->
     (fun _ -> { Types.fst =
       (TypeComparison.type_eq ty (Csyntax.Tint (target_sz, target_sg)));
       Types.snd = (Csyntax.Expr (ed, ty)) })
   | Csyntax.Efield (rec_expr, f) ->
     (fun _ ->
       (let rec_expr1 = simplify_inside rec_expr in
         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
         ((Csyntax.Efield (rec_expr1, f)), ty)) })) __)
   | Csyntax.Ecost (l, e1) ->
     (fun _ ->
       match TypeComparison.type_eq_dec ty (Csyntax.typeof e1) with
       | Types.Inl _ ->
         (let eta2039 = simplify_expr e1 target_sz target_sg in
           (fun _ ->
           (let { Types.fst = desired_type; Types.snd = e2 } = eta2039 in
           (fun _ -> { Types.fst = desired_type; Types.snd = (Csyntax.Expr
           ((Csyntax.Ecost (l, e2)), (Csyntax.typeof e2))) })) __)) __
       | Types.Inr _ ->
         (let e2 = simplify_inside e1 in
           (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
           ((Csyntax.Ecost (l, e2)), ty)) })) __)) __)) __
(** val simplify_inside : Csyntax.expr -> Csyntax.expr Types.sig0 **)
and simplify_inside e =
  (let Csyntax.Expr (ed, ty) = e in
  (fun _ ->
  (match ed with
   | Csyntax.Econst_int (x, x0) -> (fun _ -> e)
   | Csyntax.Evar x -> (fun _ -> e)
   | Csyntax.Ederef e1 ->
     (fun _ ->
       (let e2 = simplify_inside e1 in
         (fun _ -> Csyntax.Expr ((Csyntax.Ederef e2), ty))) __)
   | Csyntax.Eaddrof e1 ->
     (fun _ ->
       (let e2 = simplify_inside e1 in
         (fun _ -> Csyntax.Expr ((Csyntax.Eaddrof e2), ty))) __)
   | Csyntax.Eunop (op, e1) ->
     (fun _ ->
       (let e2 = simplify_inside e1 in
         (fun _ -> Csyntax.Expr ((Csyntax.Eunop (op, e2)), ty))) __)
   | Csyntax.Ebinop (op, lhs, rhs) ->
     (fun _ ->
       (let lhs1 = simplify_inside lhs in
         (fun _ ->
         (let rhs1 = simplify_inside rhs in
           (fun _ -> Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)))
           __)) __)
   | Csyntax.Ecast (cast_ty, castee) ->
     (fun _ ->
       match TypeComparison.type_eq_dec ty cast_ty with
       | Types.Inl _ ->
         (match cast_ty with
          | Csyntax.Tvoid -> (fun _ -> e)
          | Csyntax.Tint (cast_sz, cast_sg) ->
            (fun _ ->
              (let eta2040 = simplify_expr castee cast_sz cast_sg in
                (fun _ ->
                (let { Types.fst = success; Types.snd = castee1 } = eta2040
                 in
                (fun _ ->
                (match success with
                 | Bool.True -> (fun _ -> castee1)
                 | Bool.False ->
                   (fun _ -> Csyntax.Expr ((Csyntax.Ecast (cast_ty,
                     castee1)), ty))) __)) __)) __)
          | Csyntax.Tpointer x -> (fun _ -> e)
          | Csyntax.Tarray (x, x0) -> (fun _ -> e)
          | Csyntax.Tfunction (x, x0) -> (fun _ -> e)
          | Csyntax.Tstruct (x, x0) -> (fun _ -> e)
          | Csyntax.Tunion (x, x0) -> (fun _ -> e)
          | Csyntax.Tcomp_ptr x -> (fun _ -> e)) __
       | Types.Inr _ -> e)
   | Csyntax.Econdition (cond, iftrue, iffalse) ->
     (fun _ ->
       (let cond1 = simplify_inside cond in
         (fun _ ->
         (let iftrue1 = simplify_inside iftrue in
           (fun _ ->
           (let iffalse1 = simplify_inside iffalse in
             (fun _ -> Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
             iffalse1)), ty))) __)) __)) __)
   | Csyntax.Eandbool (lhs, rhs) ->
     (fun _ ->
       (let lhs1 = simplify_inside lhs in
         (fun _ ->
         (let rhs1 = simplify_inside rhs in
           (fun _ -> Csyntax.Expr ((Csyntax.Eandbool (lhs1, rhs1)), ty))) __))
         __)
   | Csyntax.Eorbool (lhs, rhs) ->
     (fun _ ->
       (let lhs1 = simplify_inside lhs in
         (fun _ ->
         (let rhs1 = simplify_inside rhs in
           (fun _ -> Csyntax.Expr ((Csyntax.Eorbool (lhs1, rhs1)), ty))) __))
         __)
   | Csyntax.Esizeof x -> (fun _ -> e)
   | Csyntax.Efield (rec_expr, f) ->
     (fun _ ->
       (let rec_expr1 = simplify_inside rec_expr in
         (fun _ -> Csyntax.Expr ((Csyntax.Efield (rec_expr1, f)), ty))) __)
   | Csyntax.Ecost (l, e1) ->
     (fun _ ->
       (let e2 = simplify_inside e1 in
         (fun _ -> Csyntax.Expr ((Csyntax.Ecost (l, e2)), ty))) __)) __)) __

(** val simplify_e : Csyntax.expr -> Csyntax.expr **)
let simplify_e e =
  Types.pi1 (simplify_inside e)

(** val simplify_statement : Csyntax.statement -> Csyntax.statement **)
let rec simplify_statement = function
| Csyntax.Sskip -> Csyntax.Sskip
| Csyntax.Sassign (e1, e2) ->
  Csyntax.Sassign ((simplify_e e1), (simplify_e e2))
| Csyntax.Scall (eo, e, es) ->
  Csyntax.Scall ((Types.option_map simplify_e eo), (simplify_e e),
    (List.map simplify_e es))
| Csyntax.Ssequence (s1, s2) ->
  Csyntax.Ssequence ((simplify_statement s1), (simplify_statement s2))
| Csyntax.Sifthenelse (e, s1, s2) ->
  Csyntax.Sifthenelse ((simplify_e e), (simplify_statement s1),
    (simplify_statement s2))
| Csyntax.Swhile (e, s1) ->
  Csyntax.Swhile ((simplify_e e), (simplify_statement s1))
| Csyntax.Sdowhile (e, s1) ->
  Csyntax.Sdowhile ((simplify_e e), (simplify_statement s1))
| Csyntax.Sfor (s1, e, s2, s3) ->
  Csyntax.Sfor ((simplify_statement s1), (simplify_e e),
    (simplify_statement s2), (simplify_statement s3))
| Csyntax.Sbreak -> Csyntax.Sbreak
| Csyntax.Scontinue -> Csyntax.Scontinue
| Csyntax.Sreturn eo -> Csyntax.Sreturn (Types.option_map simplify_e eo)
| Csyntax.Sswitch (e, ls) ->
  Csyntax.Sswitch ((simplify_e e), (simplify_ls ls))
| Csyntax.Slabel (l, s1) -> Csyntax.Slabel (l, (simplify_statement s1))
| Csyntax.Sgoto l -> Csyntax.Sgoto l
| Csyntax.Scost (l, s1) -> Csyntax.Scost (l, (simplify_statement s1))
(** val simplify_ls :
    Csyntax.labeled_statements -> Csyntax.labeled_statements **)
and simplify_ls = function
| Csyntax.LSdefault s -> Csyntax.LSdefault (simplify_statement s)
| Csyntax.LScase (sz, i, s, ls') ->
  Csyntax.LScase (sz, i, (simplify_statement s), (simplify_ls ls'))

(** val simplify_function : Csyntax.function0 -> Csyntax.function0 **)
let simplify_function f =
  { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
    f.Csyntax.fn_params; Csyntax.fn_vars = f.Csyntax.fn_vars;
    Csyntax.fn_body = (simplify_statement f.Csyntax.fn_body) }

(** val simplify_fundef : Csyntax.clight_fundef -> Csyntax.clight_fundef **)
let simplify_fundef f = match f with
| Csyntax.CL_Internal f0 -> Csyntax.CL_Internal (simplify_function f0)
| Csyntax.CL_External (x, x0, x1) -> f

(** val simplify_program :
    Csyntax.clight_program -> Csyntax.clight_program **)
let simplify_program p =
  AST.transform_program p (fun x -> simplify_fundef)