extracted/typeComparison.ml

   1 open Preamble
   2
   3 open CostLabel
   4
   5 open Coqlib
   6
   7 open Proper
   8
   9 open PositiveMap
  10
  11 open Deqsets
  12
  13 open ErrorMessages
  14
  15 open PreIdentifiers
  16
  17 open Errors
  18
  19 open Extralib
  20
  21 open Lists
  22
  23 open Positive
  24
  25 open Identifiers
  26
  27 open Exp
  28
  29 open Arithmetic
  30
  31 open Vector
  32
  33 open Div_and_mod
  34
  35 open Util
  36
  37 open FoldStuff
  38
  39 open BitVector
  40
  41 open Jmeq
  42
  43 open Russell
  44
  45 open List
  46
  47 open Setoids
  48
  49 open Monad
  50
  51 open Option
  52
  53 open Extranat
  54
  55 open Bool
  56
  57 open Relations
  58
  59 open Nat
  60
  61 open Integers
  62
  63 open Hints_declaration
  64
  65 open Core_notation
  66
  67 open Pts
  68
  69 open Logic
  70
  71 open Types
  72
  73 open AST
  74
  75 open Csyntax
  76
  77 (** val sz_eq_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum **)
  78 let sz_eq_dec = function
  79 | AST.I8 ->
  80   (fun s2 ->
  81     match s2 with
  82     | AST.I8 -> Types.Inl __
  83     | AST.I16 -> Types.Inr __
  84     | AST.I32 -> Types.Inr __)
  85 | AST.I16 ->
  86   (fun s2 ->
  87     match s2 with
  88     | AST.I8 -> Types.Inr __
  89     | AST.I16 -> Types.Inl __
  90     | AST.I32 -> Types.Inr __)
  91 | AST.I32 ->
  92   (fun s2 ->
  93     match s2 with
  94     | AST.I8 -> Types.Inr __
  95     | AST.I16 -> Types.Inr __
  96     | AST.I32 -> Types.Inl __)
  97
  98 (** val sg_eq_dec :
  99     AST.signedness -> AST.signedness -> (__, __) Types.sum **)
 100 let sg_eq_dec = function
 101 | AST.Signed ->
 102   (fun s2 ->
 103     match s2 with
 104     | AST.Signed -> Types.Inl __
 105     | AST.Unsigned -> Types.Inr __)
 106 | AST.Unsigned ->
 107   (fun s2 ->
 108     match s2 with
 109     | AST.Signed -> Types.Inr __
 110     | AST.Unsigned -> Types.Inl __)
 111
 112 (** val type_eq_dec :
 113     Csyntax.type0 -> Csyntax.type0 -> (__, __) Types.sum **)
 114 let rec type_eq_dec t1 t2 =
 115   match t1 with
 116   | Csyntax.Tvoid ->
 117     (match t2 with
 118      | Csyntax.Tvoid -> Types.Inl __
 119      | Csyntax.Tint (x, x0) -> Types.Inr __
 120      | Csyntax.Tpointer x -> Types.Inr __
 121      | Csyntax.Tarray (x, x0) -> Types.Inr __
 122      | Csyntax.Tfunction (x, x0) -> Types.Inr __
 123      | Csyntax.Tstruct (x, x0) -> Types.Inr __
 124      | Csyntax.Tunion (x, x0) -> Types.Inr __
 125      | Csyntax.Tcomp_ptr x -> Types.Inr __)
 126   | Csyntax.Tint (sz, sg) ->
 127     (match t2 with
 128      | Csyntax.Tvoid -> Types.Inr __
 129      | Csyntax.Tint (sz', sg') ->
 130        (match sz_eq_dec sz sz' with
 131         | Types.Inl _ ->
 132           (match sg_eq_dec sg sg' with
 133            | Types.Inl _ -> Types.Inl __
 134            | Types.Inr _ -> Types.Inr __)
 135         | Types.Inr _ -> Types.Inr __)
 136      | Csyntax.Tpointer x -> Types.Inr __
 137      | Csyntax.Tarray (x, x0) -> Types.Inr __
 138      | Csyntax.Tfunction (x, x0) -> Types.Inr __
 139      | Csyntax.Tstruct (x, x0) -> Types.Inr __
 140      | Csyntax.Tunion (x, x0) -> Types.Inr __
 141      | Csyntax.Tcomp_ptr x -> Types.Inr __)
 142   | Csyntax.Tpointer t ->
 143     (match t2 with
 144      | Csyntax.Tvoid -> Types.Inr __
 145      | Csyntax.Tint (x, x0) -> Types.Inr __
 146      | Csyntax.Tpointer t' ->
 147        (match type_eq_dec t t' with
 148         | Types.Inl _ -> Types.Inl __
 149         | Types.Inr _ -> Types.Inr __)
 150      | Csyntax.Tarray (x, x0) -> Types.Inr __
 151      | Csyntax.Tfunction (x, x0) -> Types.Inr __
 152      | Csyntax.Tstruct (x, x0) -> Types.Inr __
 153      | Csyntax.Tunion (x, x0) -> Types.Inr __
 154      | Csyntax.Tcomp_ptr x -> Types.Inr __)
 155   | Csyntax.Tarray (t, n) ->
 156     (match t2 with
 157      | Csyntax.Tvoid -> Types.Inr __
 158      | Csyntax.Tint (x, x0) -> Types.Inr __
 159      | Csyntax.Tpointer x -> Types.Inr __
 160      | Csyntax.Tarray (t', n') ->
 161        (match type_eq_dec t t' with
 162         | Types.Inl _ ->
 163           (match Extranat.eq_nat_dec n n' with
 164            | Types.Inl _ -> Types.Inl __
 165            | Types.Inr _ -> Types.Inr __)
 166         | Types.Inr _ -> Types.Inr __)
 167      | Csyntax.Tfunction (x, x0) -> Types.Inr __
 168      | Csyntax.Tstruct (x, x0) -> Types.Inr __
 169      | Csyntax.Tunion (x, x0) -> Types.Inr __
 170      | Csyntax.Tcomp_ptr x -> Types.Inr __)
 171   | Csyntax.Tfunction (tl, t) ->
 172     (match t2 with
 173      | Csyntax.Tvoid -> Types.Inr __
 174      | Csyntax.Tint (x, x0) -> Types.Inr __
 175      | Csyntax.Tpointer x -> Types.Inr __
 176      | Csyntax.Tarray (x, x0) -> Types.Inr __
 177      | Csyntax.Tfunction (tl', t') ->
 178        (match typelist_eq_dec tl tl' with
 179         | Types.Inl _ ->
 180           (match type_eq_dec t t' with
 181            | Types.Inl _ -> Types.Inl __
 182            | Types.Inr _ -> Types.Inr __)
 183         | Types.Inr _ -> Types.Inr __)
 184      | Csyntax.Tstruct (x, x0) -> Types.Inr __
 185      | Csyntax.Tunion (x, x0) -> Types.Inr __
 186      | Csyntax.Tcomp_ptr x -> Types.Inr __)
 187   | Csyntax.Tstruct (i, fl) ->
 188     (match t2 with
 189      | Csyntax.Tvoid -> Types.Inr __
 190      | Csyntax.Tint (x, x0) -> Types.Inr __
 191      | Csyntax.Tpointer x -> Types.Inr __
 192      | Csyntax.Tarray (x, x0) -> Types.Inr __
 193      | Csyntax.Tfunction (x, x0) -> Types.Inr __
 194      | Csyntax.Tstruct (i', fl') ->
 195        (match AST.ident_eq i i' with
 196         | Types.Inl _ ->
 197           (match fieldlist_eq_dec fl fl' with
 198            | Types.Inl _ -> Types.Inl __
 199            | Types.Inr _ -> Types.Inr __)
 200         | Types.Inr _ -> Types.Inr __)
 201      | Csyntax.Tunion (x, x0) -> Types.Inr __
 202      | Csyntax.Tcomp_ptr x -> Types.Inr __)
 203   | Csyntax.Tunion (i, fl) ->
 204     (match t2 with
 205      | Csyntax.Tvoid -> Types.Inr __
 206      | Csyntax.Tint (x, x0) -> Types.Inr __
 207      | Csyntax.Tpointer x -> Types.Inr __
 208      | Csyntax.Tarray (x, x0) -> Types.Inr __
 209      | Csyntax.Tfunction (x, x0) -> Types.Inr __
 210      | Csyntax.Tstruct (x, x0) -> Types.Inr __
 211      | Csyntax.Tunion (i', fl') ->
 212        (match AST.ident_eq i i' with
 213         | Types.Inl _ ->
 214           (match fieldlist_eq_dec fl fl' with
 215            | Types.Inl _ -> Types.Inl __
 216            | Types.Inr _ -> Types.Inr __)
 217         | Types.Inr _ -> Types.Inr __)
 218      | Csyntax.Tcomp_ptr x -> Types.Inr __)
 219   | Csyntax.Tcomp_ptr i ->
 220     (match t2 with
 221      | Csyntax.Tvoid -> Types.Inr __
 222      | Csyntax.Tint (x, x0) -> Types.Inr __
 223      | Csyntax.Tpointer x -> Types.Inr __
 224      | Csyntax.Tarray (x, x0) -> Types.Inr __
 225      | Csyntax.Tfunction (x, x0) -> Types.Inr __
 226      | Csyntax.Tstruct (x, x0) -> Types.Inr __
 227      | Csyntax.Tunion (x, x0) -> Types.Inr __
 228      | Csyntax.Tcomp_ptr i' ->
 229        (match AST.ident_eq i i' with
 230         | Types.Inl _ -> Types.Inl __
 231         | Types.Inr _ -> Types.Inr __))
 232 (** val typelist_eq_dec :
 233     Csyntax.typelist -> Csyntax.typelist -> (__, __) Types.sum **)
 234 and typelist_eq_dec tl1 tl2 =
 235   match tl1 with
 236   | Csyntax.Tnil ->
 237     (match tl2 with
 238      | Csyntax.Tnil -> Types.Inl __
 239      | Csyntax.Tcons (x, x0) -> Types.Inr __)
 240   | Csyntax.Tcons (t1, ts1) ->
 241     (match tl2 with
 242      | Csyntax.Tnil -> Types.Inr __
 243      | Csyntax.Tcons (t2, ts2) ->
 244        (match type_eq_dec t1 t2 with
 245         | Types.Inl _ ->
 246           (match typelist_eq_dec ts1 ts2 with
 247            | Types.Inl _ -> Types.Inl __
 248            | Types.Inr _ -> Types.Inr __)
 249         | Types.Inr _ -> Types.Inr __))
 250 (** val fieldlist_eq_dec :
 251     Csyntax.fieldlist -> Csyntax.fieldlist -> (__, __) Types.sum **)
 252 and fieldlist_eq_dec fl1 fl2 =
 253   match fl1 with
 254   | Csyntax.Fnil ->
 255     (match fl2 with
 256      | Csyntax.Fnil -> Types.Inl __
 257      | Csyntax.Fcons (x, x0, x1) -> Types.Inr __)
 258   | Csyntax.Fcons (i1, t1, fs1) ->
 259     (match fl2 with
 260      | Csyntax.Fnil -> Types.Inr __
 261      | Csyntax.Fcons (i2, t2, fs2) ->
 262        (match AST.ident_eq i1 i2 with
 263         | Types.Inl _ ->
 264           (match type_eq_dec t1 t2 with
 265            | Types.Inl _ ->
 266              (match fieldlist_eq_dec fs1 fs2 with
 267               | Types.Inl _ -> Types.Inl __
 268               | Types.Inr _ -> Types.Inr __)
 269            | Types.Inr _ -> Types.Inr __)
 270         | Types.Inr _ -> Types.Inr __))
 271
 272 (** val assert_type_eq : Csyntax.type0 -> Csyntax.type0 -> __ Errors.res **)
 273 let assert_type_eq t1 t2 =
 274   match type_eq_dec t1 t2 with
 275   | Types.Inl _ -> Errors.OK __
 276   | Types.Inr _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 277
 278 (** val type_eq : Csyntax.type0 -> Csyntax.type0 -> Bool.bool **)
 279 let type_eq t1 t2 =
 280   match type_eq_dec t1 t2 with
 281   | Types.Inl _ -> Bool.True
 282   | Types.Inr _ -> Bool.False
 283
 284 (** val if_type_eq : Csyntax.type0 -> Csyntax.type0 -> 'a1 -> 'a1 -> 'a1 **)
 285 let if_type_eq t1 t2 =
 286   match type_eq_dec t1 t2 with
 287   | Types.Inl _ -> (fun x d -> x)
 288   | Types.Inr _ -> (fun x d -> d)
 289