open Preamble

open Deqsets

open Sets

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open Listb

open Proper

open PositiveMap

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Setoids

open Monad

open Option

open Div_and_mod

open Jmeq

open Russell

open Util

open Lists

open Positive

open Identifiers

open CostLabel

open Coqlib

open Exp

open Arithmetic

open Vector

open FoldStuff

open BitVector

open Extranat

open Integers

open AST

open Csyntax

open Fresh

open CexecInd

open SmallstepExec

open Cexec

open IO

open IOMonad

open Star

open ClassifyOp

open Events

open Smallstep

open Extra_bool

open Values

open FrontEndVal

open Hide

open ByteValues

open Division

open Z

open BitVectorZ

open Pointers

open GenMem

open FrontEndMem

open Globalenvs

open Csem

open TypeComparison

open Frontend_misc

open MemProperties

open MemoryInjections

(** val convert_break_to_goto :
    Csyntax.statement -> Csyntax.label -> Csyntax.statement **)
let rec convert_break_to_goto st lab =
  match st with
  | Csyntax.Sskip -> st
  | Csyntax.Sassign (x, x0) -> st
  | Csyntax.Scall (x, x0, x1) -> st
  | Csyntax.Ssequence (s1, s2) ->
    Csyntax.Ssequence ((convert_break_to_goto s1 lab),
      (convert_break_to_goto s2 lab))
  | Csyntax.Sifthenelse (e, iftrue, iffalse) ->
    Csyntax.Sifthenelse (e, (convert_break_to_goto iftrue lab),
      (convert_break_to_goto iffalse lab))
  | Csyntax.Swhile (x, x0) -> st
  | Csyntax.Sdowhile (x, x0) -> st
  | Csyntax.Sfor (init, e, update, body) ->
    Csyntax.Sfor ((convert_break_to_goto init lab), e, update, body)
  | Csyntax.Sbreak -> Csyntax.Sgoto lab
  | Csyntax.Scontinue -> st
  | Csyntax.Sreturn x -> st
  | Csyntax.Sswitch (x, x0) -> st
  | Csyntax.Slabel (l, body) ->
    Csyntax.Slabel (l, (convert_break_to_goto body lab))
  | Csyntax.Sgoto x -> st
  | Csyntax.Scost (cost, body) ->
    Csyntax.Scost (cost, (convert_break_to_goto body lab))

(** val produce_cond :
    Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
    Csyntax.label -> ((Csyntax.statement, Csyntax.label) Types.prod,
    Identifiers.universe) Types.prod **)
let rec produce_cond e switch_cases u exit =
  match switch_cases with
  | Csyntax.LSdefault st ->
    let { Types.fst = lab; Types.snd = u1 } =
      Identifiers.fresh PreIdentifiers.SymbolTag u
    in
    let st' = convert_break_to_goto st exit in
    { Types.fst = { Types.fst = (Csyntax.Slabel (lab, st')); Types.snd =
    lab }; Types.snd = u1 }
  | Csyntax.LScase (sz, tag, st, other_cases) ->
    let { Types.fst = eta2130; Types.snd = u1 } =
      produce_cond e other_cases u exit
    in
    let { Types.fst = sub_statements; Types.snd = sub_label } = eta2130 in
    let st' = convert_break_to_goto st exit in
    let { Types.fst = lab; Types.snd = u2 } =
      Identifiers.fresh PreIdentifiers.SymbolTag u1
    in
    let test = Csyntax.Expr ((Csyntax.Ebinop (Csyntax.Oeq, e, (Csyntax.Expr
      ((Csyntax.Econst_int (sz, tag)), (Csyntax.typeof e))))), (Csyntax.Tint
      (AST.I32, AST.Signed)))
    in
    let case_statement = Csyntax.Sifthenelse (test, (Csyntax.Slabel (lab,
      (Csyntax.Ssequence (st', (Csyntax.Sgoto sub_label))))), Csyntax.Sskip)
    in
    { Types.fst = { Types.fst = (Csyntax.Ssequence (case_statement,
    sub_statements)); Types.snd = lab }; Types.snd = u2 }

(** val simplify_switch :
    Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
    (Csyntax.statement, Identifiers.universe) Types.prod **)
let simplify_switch e switch_cases uv =
  let { Types.fst = exit_label; Types.snd = uv1 } =
    Identifiers.fresh PreIdentifiers.SymbolTag uv
  in
  let { Types.fst = eta2131; Types.snd = uv2 } =
    produce_cond e switch_cases uv1 exit_label
  in
  let { Types.fst = result; Types.snd = useless_label } = eta2131 in
  { Types.fst = (Csyntax.Ssequence (result, (Csyntax.Slabel (exit_label,
  Csyntax.Sskip)))); Types.snd = uv2 }

(** val switch_removal :
    Csyntax.statement -> Identifiers.universe -> ((Csyntax.statement,
    (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
    Identifiers.universe) Types.prod **)
let rec switch_removal st u =
  match st with
  | Csyntax.Sskip ->
    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
  | Csyntax.Sassign (x, x0) ->
    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
  | Csyntax.Scall (x, x0, x1) ->
    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
  | Csyntax.Ssequence (s1, s2) ->
    let { Types.fst = eta2145; Types.snd = u' } = switch_removal s1 u in
    let { Types.fst = s1'; Types.snd = acc1 } = eta2145 in
    let { Types.fst = eta2144; Types.snd = u'' } = switch_removal s2 u' in
    let { Types.fst = s2'; Types.snd = acc2 } = eta2144 in
    { Types.fst = { Types.fst = (Csyntax.Ssequence (s1', s2')); Types.snd =
    (List.append acc1 acc2) }; Types.snd = u'' }
  | Csyntax.Sifthenelse (e, s1, s2) ->
    let { Types.fst = eta2147; Types.snd = u' } = switch_removal s1 u in
    let { Types.fst = s1'; Types.snd = acc1 } = eta2147 in
    let { Types.fst = eta2146; Types.snd = u'' } = switch_removal s2 u' in
    let { Types.fst = s2'; Types.snd = acc2 } = eta2146 in
    { Types.fst = { Types.fst = (Csyntax.Sifthenelse (e, s1', s2'));
    Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
  | Csyntax.Swhile (e, body) ->
    let { Types.fst = eta2148; Types.snd = u' } = switch_removal body u in
    let { Types.fst = body'; Types.snd = acc } = eta2148 in
    { Types.fst = { Types.fst = (Csyntax.Swhile (e, body')); Types.snd =
    acc }; Types.snd = u' }
  | Csyntax.Sdowhile (e, body) ->
    let { Types.fst = eta2149; Types.snd = u' } = switch_removal body u in
    let { Types.fst = body'; Types.snd = acc } = eta2149 in
    { Types.fst = { Types.fst = (Csyntax.Sdowhile (e, body')); Types.snd =
    acc }; Types.snd = u' }
  | Csyntax.Sfor (s1, e, s2, s3) ->
    let { Types.fst = eta2152; Types.snd = u' } = switch_removal s1 u in
    let { Types.fst = s1'; Types.snd = acc1 } = eta2152 in
    let { Types.fst = eta2151; Types.snd = u'' } = switch_removal s2 u' in
    let { Types.fst = s2'; Types.snd = acc2 } = eta2151 in
    let { Types.fst = eta2150; Types.snd = u''' } = switch_removal s3 u'' in
    let { Types.fst = s3'; Types.snd = acc3 } = eta2150 in
    { Types.fst = { Types.fst = (Csyntax.Sfor (s1', e, s2', s3'));
    Types.snd = (List.append acc1 (List.append acc2 acc3)) }; Types.snd =
    u''' }
  | Csyntax.Sbreak ->
    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
  | Csyntax.Scontinue ->
    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
  | Csyntax.Sreturn x ->
    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
  | Csyntax.Sswitch (e, branches) ->
    let { Types.fst = eta2153; Types.snd = u' } =
      switch_removal_branches branches u
    in
    let { Types.fst = sf_branches; Types.snd = acc } = eta2153 in
    let { Types.fst = switch_tmp; Types.snd = u'' } =
      Identifiers.fresh PreIdentifiers.SymbolTag u'
    in
    let ident = Csyntax.Expr ((Csyntax.Evar switch_tmp), (Csyntax.typeof e))
    in
    let assign = Csyntax.Sassign (ident, e) in
    let { Types.fst = result; Types.snd = u''' } =
      simplify_switch ident sf_branches u''
    in
    { Types.fst = { Types.fst = (Csyntax.Ssequence (assign, result));
    Types.snd = (List.Cons ({ Types.fst = switch_tmp; Types.snd =
    (Csyntax.typeof e) }, acc)) }; Types.snd = u''' }
  | Csyntax.Slabel (label, body) ->
    let { Types.fst = eta2154; Types.snd = u' } = switch_removal body u in
    let { Types.fst = body'; Types.snd = acc } = eta2154 in
    { Types.fst = { Types.fst = (Csyntax.Slabel (label, body')); Types.snd =
    acc }; Types.snd = u' }
  | Csyntax.Sgoto x ->
    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
  | Csyntax.Scost (cost, body) ->
    let { Types.fst = eta2155; Types.snd = u' } = switch_removal body u in
    let { Types.fst = body'; Types.snd = acc } = eta2155 in
    { Types.fst = { Types.fst = (Csyntax.Scost (cost, body')); Types.snd =
    acc }; Types.snd = u' }
(** val switch_removal_branches :
    Csyntax.labeled_statements -> Identifiers.universe ->
    ((Csyntax.labeled_statements, (AST.ident, Csyntax.type0) Types.prod
    List.list) Types.prod, Identifiers.universe) Types.prod **)
and switch_removal_branches l u =
  match l with
  | Csyntax.LSdefault st ->
    let { Types.fst = eta2156; Types.snd = u' } = switch_removal st u in
    let { Types.fst = st'; Types.snd = acc1 } = eta2156 in
    { Types.fst = { Types.fst = (Csyntax.LSdefault st'); Types.snd = acc1 };
    Types.snd = u' }
  | Csyntax.LScase (sz, int, st, tl) ->
    let { Types.fst = eta2158; Types.snd = u' } =
      switch_removal_branches tl u
    in
    let { Types.fst = tl_result; Types.snd = acc1 } = eta2158 in
    let { Types.fst = eta2157; Types.snd = u'' } = switch_removal st u' in
    let { Types.fst = st'; Types.snd = acc2 } = eta2157 in
    { Types.fst = { Types.fst = (Csyntax.LScase (sz, int, st', tl_result));
    Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }

(** val ret_st :
    (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
    Identifiers.universe) Types.prod -> 'a1 **)
let ret_st x =
  let { Types.fst = eta2159; Types.snd = u } = x in eta2159.Types.fst

(** val ret_vars :
    (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
    Identifiers.universe) Types.prod -> (AST.ident, Csyntax.type0) Types.prod
    List.list **)
let ret_vars x =
  let { Types.fst = eta2160; Types.snd = u } = x in eta2160.Types.snd

(** val ret_u :
    (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
    Identifiers.universe) Types.prod -> Identifiers.universe **)
let ret_u x =
  let { Types.fst = eta2161; Types.snd = u } = x in
  let { Types.fst = s; Types.snd = vars } = eta2161 in u

(** val least_identifier : PreIdentifiers.identifier **)
let least_identifier =
  Positive.One

(** val max_of_expr : Csyntax.expr -> AST.ident **)
let rec max_of_expr = function
| Csyntax.Expr (ed, x) ->
  (match ed with
   | Csyntax.Econst_int (x0, x1) -> least_identifier
   | Csyntax.Evar id -> id
   | Csyntax.Ederef e1 -> max_of_expr e1
   | Csyntax.Eaddrof e1 -> max_of_expr e1
   | Csyntax.Eunop (x0, e1) -> max_of_expr e1
   | Csyntax.Ebinop (x0, e1, e2) ->
     Fresh.max_id (max_of_expr e1) (max_of_expr e2)
   | Csyntax.Ecast (x0, e1) -> max_of_expr e1
   | Csyntax.Econdition (e1, e2, e3) ->
     Fresh.max_id (max_of_expr e1)
       (Fresh.max_id (max_of_expr e2) (max_of_expr e3))
   | Csyntax.Eandbool (e1, e2) ->
     Fresh.max_id (max_of_expr e1) (max_of_expr e2)
   | Csyntax.Eorbool (e1, e2) ->
     Fresh.max_id (max_of_expr e1) (max_of_expr e2)
   | Csyntax.Esizeof x0 -> least_identifier
   | Csyntax.Efield (r, f) -> Fresh.max_id f (max_of_expr r)
   | Csyntax.Ecost (x0, e1) -> max_of_expr e1)

(** val max_of_statement : Csyntax.statement -> AST.ident **)
let rec max_of_statement = function
| Csyntax.Sskip -> least_identifier
| Csyntax.Sassign (e1, e2) -> Fresh.max_id (max_of_expr e1) (max_of_expr e2)
| Csyntax.Scall (r, f, args) ->
  let retmax =
    match r with
    | Types.None -> least_identifier
    | Types.Some e -> max_of_expr e
  in
  Fresh.max_id (max_of_expr f)
    (Fresh.max_id retmax
      (List.foldr (fun elt acc -> Fresh.max_id (max_of_expr elt) acc)
        least_identifier args))
| Csyntax.Ssequence (s1, s2) ->
  Fresh.max_id (max_of_statement s1) (max_of_statement s2)
| Csyntax.Sifthenelse (e, s1, s2) ->
  Fresh.max_id (max_of_expr e)
    (Fresh.max_id (max_of_statement s1) (max_of_statement s2))
| Csyntax.Swhile (e, body) ->
  Fresh.max_id (max_of_expr e) (max_of_statement body)
| Csyntax.Sdowhile (e, body) ->
  Fresh.max_id (max_of_expr e) (max_of_statement body)
| Csyntax.Sfor (init, test, incr, body) ->
  Fresh.max_id (Fresh.max_id (max_of_statement init) (max_of_expr test))
    (Fresh.max_id (max_of_statement incr) (max_of_statement body))
| Csyntax.Sbreak -> least_identifier
| Csyntax.Scontinue -> least_identifier
| Csyntax.Sreturn opt ->
  (match opt with
   | Types.None -> least_identifier
   | Types.Some e -> max_of_expr e)
| Csyntax.Sswitch (e, ls) -> Fresh.max_id (max_of_expr e) (max_of_ls ls)
| Csyntax.Slabel (lab, body) -> Fresh.max_id lab (max_of_statement body)
| Csyntax.Sgoto lab -> lab
| Csyntax.Scost (x, body) -> max_of_statement body
(** val max_of_ls : Csyntax.labeled_statements -> AST.ident **)
and max_of_ls = function
| Csyntax.LSdefault s -> max_of_statement s
| Csyntax.LScase (x, x0, s, ls') ->
  Fresh.max_id (max_of_ls ls') (max_of_statement s)

(** val max_id_of_function : Csyntax.function0 -> AST.ident **)
let max_id_of_function f =
  Fresh.max_id (max_of_statement f.Csyntax.fn_body) (Fresh.max_id_of_fn f)

(** val function_switch_removal :
    Csyntax.function0 -> (Csyntax.function0, (AST.ident, Csyntax.type0)
    Types.prod List.list) Types.prod **)
let function_switch_removal f =
  let u = Fresh.universe_of_max (max_id_of_function f) in
  let { Types.fst = eta2162; Types.snd = u' } =
    switch_removal f.Csyntax.fn_body u
  in
  let { Types.fst = st; Types.snd = vars } = eta2162 in
  let result = { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
    f.Csyntax.fn_params; Csyntax.fn_vars =
    (List.append vars f.Csyntax.fn_vars); Csyntax.fn_body = st }
  in
  { Types.fst = result; Types.snd = vars }

(** val fundef_switch_removal :
    Csyntax.clight_fundef -> Csyntax.clight_fundef **)
let rec fundef_switch_removal f = match f with
| Csyntax.CL_Internal f0 ->
  Csyntax.CL_Internal (function_switch_removal f0).Types.fst
| Csyntax.CL_External (x, x0, x1) -> f

(** val program_switch_removal :
    Csyntax.clight_program -> Csyntax.clight_program **)
let rec program_switch_removal p =
  AST.transform_program p (fun x -> fundef_switch_removal)

(** val nonempty_block_rect_Type4 :
    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
let rec nonempty_block_rect_Type4 m b h_mk_nonempty_block =
  h_mk_nonempty_block __ __

(** val nonempty_block_rect_Type5 :
    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
let rec nonempty_block_rect_Type5 m b h_mk_nonempty_block =
  h_mk_nonempty_block __ __

(** val nonempty_block_rect_Type3 :
    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
let rec nonempty_block_rect_Type3 m b h_mk_nonempty_block =
  h_mk_nonempty_block __ __

(** val nonempty_block_rect_Type2 :
    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
let rec nonempty_block_rect_Type2 m b h_mk_nonempty_block =
  h_mk_nonempty_block __ __

(** val nonempty_block_rect_Type1 :
    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
let rec nonempty_block_rect_Type1 m b h_mk_nonempty_block =
  h_mk_nonempty_block __ __

(** val nonempty_block_rect_Type0 :
    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
let rec nonempty_block_rect_Type0 m b h_mk_nonempty_block =
  h_mk_nonempty_block __ __

(** val nonempty_block_inv_rect_Type4 :
    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let nonempty_block_inv_rect_Type4 x1 x2 h1 =
  let hcut = nonempty_block_rect_Type4 x1 x2 h1 in hcut __

(** val nonempty_block_inv_rect_Type3 :
    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let nonempty_block_inv_rect_Type3 x1 x2 h1 =
  let hcut = nonempty_block_rect_Type3 x1 x2 h1 in hcut __

(** val nonempty_block_inv_rect_Type2 :
    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let nonempty_block_inv_rect_Type2 x1 x2 h1 =
  let hcut = nonempty_block_rect_Type2 x1 x2 h1 in hcut __

(** val nonempty_block_inv_rect_Type1 :
    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let nonempty_block_inv_rect_Type1 x1 x2 h1 =
  let hcut = nonempty_block_rect_Type1 x1 x2 h1 in hcut __

(** val nonempty_block_inv_rect_Type0 :
    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let nonempty_block_inv_rect_Type0 x1 x2 h1 =
  let hcut = nonempty_block_rect_Type0 x1 x2 h1 in hcut __

(** val nonempty_block_discr : GenMem.mem -> Pointers.block -> __ **)
let nonempty_block_discr a1 a2 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __

(** val nonempty_block_jmdiscr : GenMem.mem -> Pointers.block -> __ **)
let nonempty_block_jmdiscr a1 a2 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __

(** val sr_memext_rect_Type4 :
    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
    -> 'a1) -> 'a1 **)
let rec sr_memext_rect_Type4 m1 m2 writeable h_mk_sr_memext =
  h_mk_sr_memext __ __ __

(** val sr_memext_rect_Type5 :
    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
    -> 'a1) -> 'a1 **)
let rec sr_memext_rect_Type5 m1 m2 writeable h_mk_sr_memext =
  h_mk_sr_memext __ __ __

(** val sr_memext_rect_Type3 :
    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
    -> 'a1) -> 'a1 **)
let rec sr_memext_rect_Type3 m1 m2 writeable h_mk_sr_memext =
  h_mk_sr_memext __ __ __

(** val sr_memext_rect_Type2 :
    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
    -> 'a1) -> 'a1 **)
let rec sr_memext_rect_Type2 m1 m2 writeable h_mk_sr_memext =
  h_mk_sr_memext __ __ __

(** val sr_memext_rect_Type1 :
    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
    -> 'a1) -> 'a1 **)
let rec sr_memext_rect_Type1 m1 m2 writeable h_mk_sr_memext =
  h_mk_sr_memext __ __ __

(** val sr_memext_rect_Type0 :
    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
    -> 'a1) -> 'a1 **)
let rec sr_memext_rect_Type0 m1 m2 writeable h_mk_sr_memext =
  h_mk_sr_memext __ __ __

(** val sr_memext_inv_rect_Type4 :
    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
    -> __ -> 'a1) -> 'a1 **)
let sr_memext_inv_rect_Type4 x1 x2 x3 h1 =
  let hcut = sr_memext_rect_Type4 x1 x2 x3 h1 in hcut __

(** val sr_memext_inv_rect_Type3 :
    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
    -> __ -> 'a1) -> 'a1 **)
let sr_memext_inv_rect_Type3 x1 x2 x3 h1 =
  let hcut = sr_memext_rect_Type3 x1 x2 x3 h1 in hcut __

(** val sr_memext_inv_rect_Type2 :
    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
    -> __ -> 'a1) -> 'a1 **)
let sr_memext_inv_rect_Type2 x1 x2 x3 h1 =
  let hcut = sr_memext_rect_Type2 x1 x2 x3 h1 in hcut __

(** val sr_memext_inv_rect_Type1 :
    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
    -> __ -> 'a1) -> 'a1 **)
let sr_memext_inv_rect_Type1 x1 x2 x3 h1 =
  let hcut = sr_memext_rect_Type1 x1 x2 x3 h1 in hcut __

(** val sr_memext_inv_rect_Type0 :
    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
    -> __ -> 'a1) -> 'a1 **)
let sr_memext_inv_rect_Type0 x1 x2 x3 h1 =
  let hcut = sr_memext_rect_Type0 x1 x2 x3 h1 in hcut __

(** val sr_memext_discr :
    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __ **)
let sr_memext_discr a1 a2 a3 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __

(** val sr_memext_jmdiscr :
    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __ **)
let sr_memext_jmdiscr a1 a2 a3 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __

(** val env_codomain :
    Csem.env -> (AST.ident, Csyntax.type0) Types.prod List.list ->
    Pointers.block Frontend_misc.lset **)
let env_codomain e l =
  Identifiers.foldi PreIdentifiers.SymbolTag (fun id block acc ->
    match Frontend_misc.mem_assoc_env id l with
    | Bool.True -> List.Cons (block, acc)
    | Bool.False -> acc) e List.Nil