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 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 Star

open IOMonad

open IO

open Sets

open Listb

(** val typ_eq_dec : AST.typ -> AST.typ -> (__, __) Types.sum **)
let typ_eq_dec t1 t2 =
  match t1 with
  | AST.ASTint (x, x0) ->
    (match t2 with
     | AST.ASTint (sz, sg) ->
       (fun sz' sg' ->
         match sz with
         | AST.I8 ->
           (match sz' with
            | AST.I8 ->
              AST.typ_eq (AST.ASTint (AST.I8, sg')) (AST.ASTint (AST.I8, sg))
            | AST.I16 ->
              AST.typ_eq (AST.ASTint (AST.I16, sg')) (AST.ASTint (AST.I8,
                sg))
            | AST.I32 ->
              AST.typ_eq (AST.ASTint (AST.I32, sg')) (AST.ASTint (AST.I8,
                sg)))
         | AST.I16 ->
           (match sz' with
            | AST.I8 ->
              AST.typ_eq (AST.ASTint (AST.I8, sg')) (AST.ASTint (AST.I16,
                sg))
            | AST.I16 ->
              AST.typ_eq (AST.ASTint (AST.I16, sg')) (AST.ASTint (AST.I16,
                sg))
            | AST.I32 ->
              AST.typ_eq (AST.ASTint (AST.I32, sg')) (AST.ASTint (AST.I16,
                sg)))
         | AST.I32 ->
           (match sz' with
            | AST.I8 ->
              AST.typ_eq (AST.ASTint (AST.I8, sg')) (AST.ASTint (AST.I32,
                sg))
            | AST.I16 ->
              AST.typ_eq (AST.ASTint (AST.I16, sg')) (AST.ASTint (AST.I32,
                sg))
            | AST.I32 ->
              AST.typ_eq (AST.ASTint (AST.I32, sg')) (AST.ASTint (AST.I32,
                sg))))
     | AST.ASTptr -> (fun sz sg -> Types.Inr __)) x x0
  | AST.ASTptr ->
    (match t2 with
     | AST.ASTint (sz, sg) -> Types.Inr __
     | AST.ASTptr -> Types.Inl __)

(** val block_DeqSet : Deqsets.deqSet **)
let block_DeqSet =
  Obj.magic Pointers.eq_block

(** val mem_assoc_env :
    AST.ident -> (AST.ident, Csyntax.type0) Types.prod List.list -> Bool.bool **)
let rec mem_assoc_env i = function
| List.Nil -> Bool.False
| List.Cons (hd, tl) ->
  let { Types.fst = id; Types.snd = ty } = hd in
  (match Identifiers.identifier_eq PreIdentifiers.SymbolTag i id with
   | Types.Inl _ -> Bool.True
   | Types.Inr _ -> mem_assoc_env i tl)

type 'a lset = 'a List.list

(** val empty_lset : 'a1 List.list **)
let empty_lset =
  List.Nil

(** val lset_union : 'a1 lset -> 'a1 lset -> 'a1 List.list **)
let lset_union l1 l2 =
  List.append l1 l2

(** val lset_remove : Deqsets.deqSet -> __ lset -> __ -> __ List.list **)
let lset_remove a l elt =
  List.filter (fun x -> Bool.notb (Deqsets.eqb a x elt)) l

(** val lset_difference :
    Deqsets.deqSet -> __ lset -> __ lset -> __ List.list **)
let lset_difference a l1 l2 =
  List.filter (fun x -> Bool.notb (Listb.memb a x l2)) l1

(** val wF_rect : ('a1 -> __ -> ('a1 -> __ -> 'a2) -> 'a2) -> 'a1 -> 'a2 **)
let rec wF_rect f x =
  f x __ (fun y _ -> wF_rect f y)

(** val one_bv : Nat.nat -> BitVector.bitVector **)
let one_bv n =
  (Arithmetic.add_with_carries n (BitVector.zero n) (BitVector.zero n)
    Bool.True).Types.fst

(** val ith_carry :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
    Bool.bool **)
let rec ith_carry n a b init =
  (match n with
   | Nat.O -> (fun x x0 -> init)
   | Nat.S x ->
     (fun a' b' ->
       let hd_a = Vector.head' x a' in
       let hd_b = Vector.head' x b' in
       let tl_a = Vector.tail x a' in
       let tl_b = Vector.tail x b' in
       Arithmetic.carry_of hd_a hd_b (ith_carry x tl_a tl_b init))) a b

(** val ith_bit :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
    Bool.bool **)
let ith_bit n a b init =
  (match n with
   | Nat.O -> (fun x x0 -> init)
   | Nat.S x ->
     (fun a' b' ->
       let hd_a = Vector.head' x a' in
       let hd_b = Vector.head' x b' in
       let tl_a = Vector.tail x a' in
       let tl_b = Vector.tail x b' in
       Bool.xorb (Bool.xorb hd_a hd_b) (ith_carry x tl_a tl_b init))) a b

(** val bitvector_fold :
    Nat.nat -> BitVector.bitVector -> (Nat.nat -> BitVector.bitVector ->
    Bool.bool) -> BitVector.bitVector **)
let rec bitvector_fold n v f =
  match v with
  | Vector.VEmpty -> Vector.VEmpty
  | Vector.VCons (sz, elt, tl) ->
    let bit = f n v in Vector.VCons (sz, bit, (bitvector_fold sz tl f))

(** val bitvector_fold2 :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (Nat.nat ->
    BitVector.bitVector -> BitVector.bitVector -> Bool.bool) ->
    BitVector.bitVector **)
let rec bitvector_fold2 n v1 v2 f =
  (match v1 with
   | Vector.VEmpty -> (fun x -> Vector.VEmpty)
   | Vector.VCons (sz, elt, tl) ->
     (fun v2' ->
       let bit = f n v1 v2 in
       Vector.VCons (sz, bit, (bitvector_fold2 sz tl (Vector.tail sz v2') f))))
    v2

(** val addition_n_direct :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
    BitVector.bitVector **)
let addition_n_direct n v1 v2 init =
  bitvector_fold2 n v1 v2 (fun n0 v10 v20 -> ith_bit n0 v10 v20 init)

(** val increment_direct :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
let increment_direct n v =
  addition_n_direct n v (one_bv n) Bool.False

(** val twocomp_neg_direct :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
let twocomp_neg_direct n v =
  increment_direct n (BitVector.negation_bv n v)

(** val andb_fold : Nat.nat -> BitVector.bitVector -> Bool.bool **)
let rec andb_fold n = function
| Vector.VEmpty -> Bool.True
| Vector.VCons (sz, elt, tl) -> Bool.andb elt (andb_fold sz tl)