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

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

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

(** val type_eq_dec :
    Csyntax.type0 -> Csyntax.type0 -> (__, __) Types.sum **)
let rec type_eq_dec t1 t2 =
  match t1 with
  | Csyntax.Tvoid ->
    (match t2 with
     | Csyntax.Tvoid -> Types.Inl __
     | Csyntax.Tint (x, x0) -> Types.Inr __
     | Csyntax.Tpointer x -> Types.Inr __
     | Csyntax.Tarray (x, x0) -> Types.Inr __
     | Csyntax.Tfunction (x, x0) -> Types.Inr __
     | Csyntax.Tstruct (x, x0) -> Types.Inr __
     | Csyntax.Tunion (x, x0) -> Types.Inr __
     | Csyntax.Tcomp_ptr x -> Types.Inr __)
  | Csyntax.Tint (sz, sg) ->
    (match t2 with
     | Csyntax.Tvoid -> Types.Inr __
     | Csyntax.Tint (sz', sg') ->
       (match sz_eq_dec sz sz' with
        | Types.Inl _ ->
          (match sg_eq_dec sg sg' with
           | Types.Inl _ -> Types.Inl __
           | Types.Inr _ -> Types.Inr __)
        | Types.Inr _ -> Types.Inr __)
     | Csyntax.Tpointer x -> Types.Inr __
     | Csyntax.Tarray (x, x0) -> Types.Inr __
     | Csyntax.Tfunction (x, x0) -> Types.Inr __
     | Csyntax.Tstruct (x, x0) -> Types.Inr __
     | Csyntax.Tunion (x, x0) -> Types.Inr __
     | Csyntax.Tcomp_ptr x -> Types.Inr __)
  | Csyntax.Tpointer t ->
    (match t2 with
     | Csyntax.Tvoid -> Types.Inr __
     | Csyntax.Tint (x, x0) -> Types.Inr __
     | Csyntax.Tpointer t' ->
       (match type_eq_dec t t' with
        | Types.Inl _ -> Types.Inl __
        | Types.Inr _ -> Types.Inr __)
     | Csyntax.Tarray (x, x0) -> Types.Inr __
     | Csyntax.Tfunction (x, x0) -> Types.Inr __
     | Csyntax.Tstruct (x, x0) -> Types.Inr __
     | Csyntax.Tunion (x, x0) -> Types.Inr __
     | Csyntax.Tcomp_ptr x -> Types.Inr __)
  | Csyntax.Tarray (t, n) ->
    (match t2 with
     | Csyntax.Tvoid -> Types.Inr __
     | Csyntax.Tint (x, x0) -> Types.Inr __
     | Csyntax.Tpointer x -> Types.Inr __
     | Csyntax.Tarray (t', n') ->
       (match type_eq_dec t t' with
        | Types.Inl _ ->
          (match Extranat.eq_nat_dec n n' with
           | Types.Inl _ -> Types.Inl __
           | Types.Inr _ -> Types.Inr __)
        | Types.Inr _ -> Types.Inr __)
     | Csyntax.Tfunction (x, x0) -> Types.Inr __
     | Csyntax.Tstruct (x, x0) -> Types.Inr __
     | Csyntax.Tunion (x, x0) -> Types.Inr __
     | Csyntax.Tcomp_ptr x -> Types.Inr __)
  | Csyntax.Tfunction (tl, t) ->
    (match t2 with
     | Csyntax.Tvoid -> Types.Inr __
     | Csyntax.Tint (x, x0) -> Types.Inr __
     | Csyntax.Tpointer x -> Types.Inr __
     | Csyntax.Tarray (x, x0) -> Types.Inr __
     | Csyntax.Tfunction (tl', t') ->
       (match typelist_eq_dec tl tl' with
        | Types.Inl _ ->
          (match type_eq_dec t t' with
           | Types.Inl _ -> Types.Inl __
           | Types.Inr _ -> Types.Inr __)
        | Types.Inr _ -> Types.Inr __)
     | Csyntax.Tstruct (x, x0) -> Types.Inr __
     | Csyntax.Tunion (x, x0) -> Types.Inr __
     | Csyntax.Tcomp_ptr x -> Types.Inr __)
  | Csyntax.Tstruct (i, fl) ->
    (match t2 with
     | Csyntax.Tvoid -> Types.Inr __
     | Csyntax.Tint (x, x0) -> Types.Inr __
     | Csyntax.Tpointer x -> Types.Inr __
     | Csyntax.Tarray (x, x0) -> Types.Inr __
     | Csyntax.Tfunction (x, x0) -> Types.Inr __
     | Csyntax.Tstruct (i', fl') ->
       (match AST.ident_eq i i' with
        | Types.Inl _ ->
          (match fieldlist_eq_dec fl fl' with
           | Types.Inl _ -> Types.Inl __
           | Types.Inr _ -> Types.Inr __)
        | Types.Inr _ -> Types.Inr __)
     | Csyntax.Tunion (x, x0) -> Types.Inr __
     | Csyntax.Tcomp_ptr x -> Types.Inr __)
  | Csyntax.Tunion (i, fl) ->
    (match t2 with
     | Csyntax.Tvoid -> Types.Inr __
     | Csyntax.Tint (x, x0) -> Types.Inr __
     | Csyntax.Tpointer x -> Types.Inr __
     | Csyntax.Tarray (x, x0) -> Types.Inr __
     | Csyntax.Tfunction (x, x0) -> Types.Inr __
     | Csyntax.Tstruct (x, x0) -> Types.Inr __
     | Csyntax.Tunion (i', fl') ->
       (match AST.ident_eq i i' with
        | Types.Inl _ ->
          (match fieldlist_eq_dec fl fl' with
           | Types.Inl _ -> Types.Inl __
           | Types.Inr _ -> Types.Inr __)
        | Types.Inr _ -> Types.Inr __)
     | Csyntax.Tcomp_ptr x -> Types.Inr __)
  | Csyntax.Tcomp_ptr i ->
    (match t2 with
     | Csyntax.Tvoid -> Types.Inr __
     | Csyntax.Tint (x, x0) -> Types.Inr __
     | Csyntax.Tpointer x -> Types.Inr __
     | Csyntax.Tarray (x, x0) -> Types.Inr __
     | Csyntax.Tfunction (x, x0) -> Types.Inr __
     | Csyntax.Tstruct (x, x0) -> Types.Inr __
     | Csyntax.Tunion (x, x0) -> Types.Inr __
     | Csyntax.Tcomp_ptr i' ->
       (match AST.ident_eq i i' with
        | Types.Inl _ -> Types.Inl __
        | Types.Inr _ -> Types.Inr __))
(** val typelist_eq_dec :
    Csyntax.typelist -> Csyntax.typelist -> (__, __) Types.sum **)
and typelist_eq_dec tl1 tl2 =
  match tl1 with
  | Csyntax.Tnil ->
    (match tl2 with
     | Csyntax.Tnil -> Types.Inl __
     | Csyntax.Tcons (x, x0) -> Types.Inr __)
  | Csyntax.Tcons (t1, ts1) ->
    (match tl2 with
     | Csyntax.Tnil -> Types.Inr __
     | Csyntax.Tcons (t2, ts2) ->
       (match type_eq_dec t1 t2 with
        | Types.Inl _ ->
          (match typelist_eq_dec ts1 ts2 with
           | Types.Inl _ -> Types.Inl __
           | Types.Inr _ -> Types.Inr __)
        | Types.Inr _ -> Types.Inr __))
(** val fieldlist_eq_dec :
    Csyntax.fieldlist -> Csyntax.fieldlist -> (__, __) Types.sum **)
and fieldlist_eq_dec fl1 fl2 =
  match fl1 with
  | Csyntax.Fnil ->
    (match fl2 with
     | Csyntax.Fnil -> Types.Inl __
     | Csyntax.Fcons (x, x0, x1) -> Types.Inr __)
  | Csyntax.Fcons (i1, t1, fs1) ->
    (match fl2 with
     | Csyntax.Fnil -> Types.Inr __
     | Csyntax.Fcons (i2, t2, fs2) ->
       (match AST.ident_eq i1 i2 with
        | Types.Inl _ ->
          (match type_eq_dec t1 t2 with
           | Types.Inl _ ->
             (match fieldlist_eq_dec fs1 fs2 with
              | Types.Inl _ -> Types.Inl __
              | Types.Inr _ -> Types.Inr __)
           | Types.Inr _ -> Types.Inr __)
        | Types.Inr _ -> Types.Inr __))

(** val assert_type_eq : Csyntax.type0 -> Csyntax.type0 -> __ Errors.res **)
let assert_type_eq t1 t2 =
  match type_eq_dec t1 t2 with
  | Types.Inl _ -> Errors.OK __
  | Types.Inr _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)

(** val type_eq : Csyntax.type0 -> Csyntax.type0 -> Bool.bool **)
let type_eq t1 t2 =
  match type_eq_dec t1 t2 with
  | Types.Inl _ -> Bool.True
  | Types.Inr _ -> Bool.False

(** val if_type_eq : Csyntax.type0 -> Csyntax.type0 -> 'a1 -> 'a1 -> 'a1 **)
let if_type_eq t1 t2 =
  match type_eq_dec t1 t2 with
  | Types.Inl _ -> (fun x d -> x)
  | Types.Inr _ -> (fun x d -> d)