extracted/toCminor.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 open TypeComparison
  78
  79 open ClassifyOp
  80
  81 open Fresh
  82
  83 (** val gather_mem_vars_expr : Csyntax.expr -> Identifiers.identifier_set **)
  84 let rec gather_mem_vars_expr = function
  85 | Csyntax.Expr (ed, ty) ->
  86   (match ed with
  87    | Csyntax.Econst_int (x, x0) ->
  88      Identifiers.empty_set PreIdentifiers.SymbolTag
  89    | Csyntax.Evar x -> Identifiers.empty_set PreIdentifiers.SymbolTag
  90    | Csyntax.Ederef e1 -> gather_mem_vars_expr e1
  91    | Csyntax.Eaddrof e1 -> gather_mem_vars_addr e1
  92    | Csyntax.Eunop (x, e1) -> gather_mem_vars_expr e1
  93    | Csyntax.Ebinop (x, e1, e2) ->
  94      Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
  95        (gather_mem_vars_expr e2)
  96    | Csyntax.Ecast (x, e1) -> gather_mem_vars_expr e1
  97    | Csyntax.Econdition (e1, e2, e3) ->
  98      Identifiers.union_set PreIdentifiers.SymbolTag
  99        (Identifiers.union_set PreIdentifiers.SymbolTag
 100          (gather_mem_vars_expr e1) (gather_mem_vars_expr e2))
 101        (gather_mem_vars_expr e3)
 102    | Csyntax.Eandbool (e1, e2) ->
 103      Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
 104        (gather_mem_vars_expr e2)
 105    | Csyntax.Eorbool (e1, e2) ->
 106      Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
 107        (gather_mem_vars_expr e2)
 108    | Csyntax.Esizeof x -> Identifiers.empty_set PreIdentifiers.SymbolTag
 109    | Csyntax.Efield (e1, x) -> gather_mem_vars_expr e1
 110    | Csyntax.Ecost (x, e1) -> gather_mem_vars_expr e1)
 111 (** val gather_mem_vars_addr : Csyntax.expr -> Identifiers.identifier_set **)
 112 and gather_mem_vars_addr = function
 113 | Csyntax.Expr (ed, ty) ->
 114   (match ed with
 115    | Csyntax.Econst_int (x, x0) ->
 116      Identifiers.empty_set PreIdentifiers.SymbolTag
 117    | Csyntax.Evar x ->
 118      Identifiers.add_set PreIdentifiers.SymbolTag
 119        (Identifiers.empty_set PreIdentifiers.SymbolTag) x
 120    | Csyntax.Ederef e1 -> gather_mem_vars_expr e1
 121    | Csyntax.Eaddrof x -> Identifiers.empty_set PreIdentifiers.SymbolTag
 122    | Csyntax.Eunop (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag
 123    | Csyntax.Ebinop (x, x0, x1) ->
 124      Identifiers.empty_set PreIdentifiers.SymbolTag
 125    | Csyntax.Ecast (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag
 126    | Csyntax.Econdition (x, x0, x1) ->
 127      Identifiers.empty_set PreIdentifiers.SymbolTag
 128    | Csyntax.Eandbool (x, x0) ->
 129      Identifiers.empty_set PreIdentifiers.SymbolTag
 130    | Csyntax.Eorbool (x, x0) ->
 131      Identifiers.empty_set PreIdentifiers.SymbolTag
 132    | Csyntax.Esizeof x -> Identifiers.empty_set PreIdentifiers.SymbolTag
 133    | Csyntax.Efield (e1, x) -> gather_mem_vars_addr e1
 134    | Csyntax.Ecost (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag)
 135
 136 (** val gather_mem_vars_stmt :
 137     Csyntax.statement -> Identifiers.identifier_set **)
 138 let rec gather_mem_vars_stmt = function
 139 | Csyntax.Sskip -> Identifiers.empty_set PreIdentifiers.SymbolTag
 140 | Csyntax.Sassign (e1, e2) ->
 141   Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
 142     (gather_mem_vars_expr e2)
 143 | Csyntax.Scall (oe1, e2, es) ->
 144   Identifiers.union_set PreIdentifiers.SymbolTag
 145     (Identifiers.union_set PreIdentifiers.SymbolTag
 146       (match oe1 with
 147        | Types.None -> Identifiers.empty_set PreIdentifiers.SymbolTag
 148        | Types.Some e1 -> gather_mem_vars_expr e1) (gather_mem_vars_expr e2))
 149     (Util.foldl (fun s0 e ->
 150       Identifiers.union_set PreIdentifiers.SymbolTag s0
 151         (gather_mem_vars_expr e))
 152       (Identifiers.empty_set PreIdentifiers.SymbolTag) es)
 153 | Csyntax.Ssequence (s1, s2) ->
 154   Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_stmt s1)
 155     (gather_mem_vars_stmt s2)
 156 | Csyntax.Sifthenelse (e1, s1, s2) ->
 157   Identifiers.union_set PreIdentifiers.SymbolTag
 158     (Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
 159       (gather_mem_vars_stmt s1)) (gather_mem_vars_stmt s2)
 160 | Csyntax.Swhile (e1, s1) ->
 161   Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
 162     (gather_mem_vars_stmt s1)
 163 | Csyntax.Sdowhile (e1, s1) ->
 164   Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
 165     (gather_mem_vars_stmt s1)
 166 | Csyntax.Sfor (s1, e1, s2, s3) ->
 167   Identifiers.union_set PreIdentifiers.SymbolTag
 168     (Identifiers.union_set PreIdentifiers.SymbolTag
 169       (Identifiers.union_set PreIdentifiers.SymbolTag
 170         (gather_mem_vars_stmt s1) (gather_mem_vars_expr e1))
 171       (gather_mem_vars_stmt s2)) (gather_mem_vars_stmt s3)
 172 | Csyntax.Sbreak -> Identifiers.empty_set PreIdentifiers.SymbolTag
 173 | Csyntax.Scontinue -> Identifiers.empty_set PreIdentifiers.SymbolTag
 174 | Csyntax.Sreturn oe1 ->
 175   (match oe1 with
 176    | Types.None -> Identifiers.empty_set PreIdentifiers.SymbolTag
 177    | Types.Some e1 -> gather_mem_vars_expr e1)
 178 | Csyntax.Sswitch (e1, ls) ->
 179   Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
 180     (gather_mem_vars_ls ls)
 181 | Csyntax.Slabel (x, s1) -> gather_mem_vars_stmt s1
 182 | Csyntax.Sgoto x -> Identifiers.empty_set PreIdentifiers.SymbolTag
 183 | Csyntax.Scost (x, s1) -> gather_mem_vars_stmt s1
 184 (** val gather_mem_vars_ls :
 185     Csyntax.labeled_statements -> Identifiers.identifier_set **)
 186 and gather_mem_vars_ls = function
 187 | Csyntax.LSdefault s1 -> gather_mem_vars_stmt s1
 188 | Csyntax.LScase (x, x0, s1, ls1) ->
 189   Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_stmt s1)
 190     (gather_mem_vars_ls ls1)
 191
 192 type var_type =
 193 | Global of AST.region
 194 | Stack of Nat.nat
 195 | Local
 196
 197 (** val var_type_rect_Type4 :
 198     (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
 199 let rec var_type_rect_Type4 h_Global h_Stack h_Local = function
 200 | Global x_13038 -> h_Global x_13038
 201 | Stack x_13039 -> h_Stack x_13039
 202 | Local -> h_Local
 203
 204 (** val var_type_rect_Type5 :
 205     (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
 206 let rec var_type_rect_Type5 h_Global h_Stack h_Local = function
 207 | Global x_13044 -> h_Global x_13044
 208 | Stack x_13045 -> h_Stack x_13045
 209 | Local -> h_Local
 210
 211 (** val var_type_rect_Type3 :
 212     (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
 213 let rec var_type_rect_Type3 h_Global h_Stack h_Local = function
 214 | Global x_13050 -> h_Global x_13050
 215 | Stack x_13051 -> h_Stack x_13051
 216 | Local -> h_Local
 217
 218 (** val var_type_rect_Type2 :
 219     (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
 220 let rec var_type_rect_Type2 h_Global h_Stack h_Local = function
 221 | Global x_13056 -> h_Global x_13056
 222 | Stack x_13057 -> h_Stack x_13057
 223 | Local -> h_Local
 224
 225 (** val var_type_rect_Type1 :
 226     (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
 227 let rec var_type_rect_Type1 h_Global h_Stack h_Local = function
 228 | Global x_13062 -> h_Global x_13062
 229 | Stack x_13063 -> h_Stack x_13063
 230 | Local -> h_Local
 231
 232 (** val var_type_rect_Type0 :
 233     (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
 234 let rec var_type_rect_Type0 h_Global h_Stack h_Local = function
 235 | Global x_13068 -> h_Global x_13068
 236 | Stack x_13069 -> h_Stack x_13069
 237 | Local -> h_Local
 238
 239 (** val var_type_inv_rect_Type4 :
 240     var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
 241     'a1) -> 'a1 **)
 242 let var_type_inv_rect_Type4 hterm h1 h2 h3 =
 243   let hcut = var_type_rect_Type4 h1 h2 h3 hterm in hcut __
 244
 245 (** val var_type_inv_rect_Type3 :
 246     var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
 247     'a1) -> 'a1 **)
 248 let var_type_inv_rect_Type3 hterm h1 h2 h3 =
 249   let hcut = var_type_rect_Type3 h1 h2 h3 hterm in hcut __
 250
 251 (** val var_type_inv_rect_Type2 :
 252     var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
 253     'a1) -> 'a1 **)
 254 let var_type_inv_rect_Type2 hterm h1 h2 h3 =
 255   let hcut = var_type_rect_Type2 h1 h2 h3 hterm in hcut __
 256
 257 (** val var_type_inv_rect_Type1 :
 258     var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
 259     'a1) -> 'a1 **)
 260 let var_type_inv_rect_Type1 hterm h1 h2 h3 =
 261   let hcut = var_type_rect_Type1 h1 h2 h3 hterm in hcut __
 262
 263 (** val var_type_inv_rect_Type0 :
 264     var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
 265     'a1) -> 'a1 **)
 266 let var_type_inv_rect_Type0 hterm h1 h2 h3 =
 267   let hcut = var_type_rect_Type0 h1 h2 h3 hterm in hcut __
 268
 269 (** val var_type_discr : var_type -> var_type -> __ **)
 270 let var_type_discr x y =
 271   Logic.eq_rect_Type2 x
 272     (match x with
 273      | Global a0 -> Obj.magic (fun _ dH -> dH __)
 274      | Stack a0 -> Obj.magic (fun _ dH -> dH __)
 275      | Local -> Obj.magic (fun _ dH -> dH)) y
 276
 277 (** val var_type_jmdiscr : var_type -> var_type -> __ **)
 278 let var_type_jmdiscr x y =
 279   Logic.eq_rect_Type2 x
 280     (match x with
 281      | Global a0 -> Obj.magic (fun _ dH -> dH __)
 282      | Stack a0 -> Obj.magic (fun _ dH -> dH __)
 283      | Local -> Obj.magic (fun _ dH -> dH)) y
 284
 285 type var_types =
 286   (var_type, Csyntax.type0) Types.prod Identifiers.identifier_map
 287
 288 (** val lookup' :
 289     var_types -> PreIdentifiers.identifier -> (var_type, Csyntax.type0)
 290     Types.prod Errors.res **)
 291 let lookup' vars id =
 292   Errors.opt_to_res (List.Cons ((Errors.MSG
 293     ErrorMessages.UndeclaredIdentifier), (List.Cons ((Errors.CTX
 294     (PreIdentifiers.SymbolTag, id)), List.Nil))))
 295     (Identifiers.lookup PreIdentifiers.SymbolTag vars id)
 296
 297 (** val always_alloc : Csyntax.type0 -> Bool.bool **)
 298 let always_alloc = function
 299 | Csyntax.Tvoid -> Bool.False
 300 | Csyntax.Tint (x, x0) -> Bool.False
 301 | Csyntax.Tpointer x -> Bool.False
 302 | Csyntax.Tarray (x, x0) -> Bool.True
 303 | Csyntax.Tfunction (x, x0) -> Bool.False
 304 | Csyntax.Tstruct (x, x0) -> Bool.True
 305 | Csyntax.Tunion (x, x0) -> Bool.True
 306 | Csyntax.Tcomp_ptr x -> Bool.False
 307
 308 (** val characterise_vars :
 309     ((AST.ident, AST.region) Types.prod, Csyntax.type0) Types.prod List.list
 310     -> Csyntax.function0 -> (var_types, Nat.nat) Types.prod **)
 311 let characterise_vars globals f =
 312   let m =
 313     List.foldr (fun idrt m ->
 314       Identifiers.add PreIdentifiers.SymbolTag m idrt.Types.fst.Types.fst
 315         { Types.fst = (Global idrt.Types.fst.Types.snd); Types.snd =
 316         idrt.Types.snd }) (Identifiers.empty_map PreIdentifiers.SymbolTag)
 317       globals
 318   in
 319   let mem_vars = gather_mem_vars_stmt f.Csyntax.fn_body in
 320   let { Types.fst = m0; Types.snd = stacksize } =
 321     List.foldr (fun v ms ->
 322       let { Types.fst = m0; Types.snd = stack_high } = ms in
 323       let { Types.fst = id; Types.snd = ty } = v in
 324       let { Types.fst = c; Types.snd = stack_high0 } =
 325         match Bool.orb (always_alloc ty)
 326                 (Identifiers.member PreIdentifiers.SymbolTag mem_vars id) with
 327         | Bool.True ->
 328           { Types.fst = (Stack stack_high); Types.snd =
 329             (Nat.plus stack_high (Csyntax.sizeof ty)) }
 330         | Bool.False -> { Types.fst = Local; Types.snd = stack_high }
 331       in
 332       { Types.fst =
 333       (Identifiers.add PreIdentifiers.SymbolTag m0 id { Types.fst = c;
 334         Types.snd = ty }); Types.snd = stack_high0 }) { Types.fst = m;
 335       Types.snd = Nat.O } (List.append f.Csyntax.fn_params f.Csyntax.fn_vars)
 336   in
 337   { Types.fst = m0; Types.snd = stacksize }
 338
 339 open FrontEndVal
 340
 341 open Hide
 342
 343 open ByteValues
 344
 345 open GenMem
 346
 347 open FrontEndMem
 348
 349 open Division
 350
 351 open Z
 352
 353 open BitVectorZ
 354
 355 open Pointers
 356
 357 open Values
 358
 359 open FrontEndOps
 360
 361 open Cminor_syntax
 362
 363 (** val type_should_eq :
 364     Csyntax.type0 -> Csyntax.type0 -> 'a1 -> 'a1 Errors.res **)
 365 let type_should_eq ty1 ty2 p =
 366   Obj.magic
 367     (Monad.m_bind0 (Monad.max_def Errors.res0)
 368       (Obj.magic (TypeComparison.assert_type_eq ty1 ty2)) (fun _ ->
 369       Obj.magic (Errors.OK ((fun p0 -> p0) p))))
 370
 371 (** val region_should_eq :
 372     AST.region -> AST.region -> 'a1 -> 'a1 Errors.res **)
 373 let region_should_eq clearme r2 x =
 374   (match clearme with
 375    | AST.XData ->
 376      (fun clearme0 ->
 377        match clearme0 with
 378        | AST.XData -> (fun _ p -> Errors.OK p)
 379        | AST.Code ->
 380          (fun _ p -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
 381    | AST.Code ->
 382      (fun clearme0 ->
 383        match clearme0 with
 384        | AST.XData ->
 385          (fun _ p -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 386        | AST.Code -> (fun _ p -> Errors.OK p))) r2 __ x
 387
 388 (** val typ_should_eq : AST.typ -> AST.typ -> 'a1 -> 'a1 Errors.res **)
 389 let typ_should_eq ty1 ty2 p =
 390   match AST.typ_eq ty1 ty2 with
 391   | Types.Inl _ -> Errors.OK p
 392   | Types.Inr _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 393
 394 (** val translate_unop :
 395     AST.typ -> AST.typ -> Csyntax.unary_operation ->
 396     FrontEndOps.unary_operation Errors.res **)
 397 let translate_unop t t' = function
 398 | Csyntax.Onotbool ->
 399   (match t with
 400    | AST.ASTint (sz, sg) ->
 401      (match t' with
 402       | AST.ASTint (sz', sg') ->
 403         Errors.OK (FrontEndOps.Onotbool ((AST.ASTint (sz, sg)), sz', sg'))
 404       | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 405    | AST.ASTptr ->
 406      (match t' with
 407       | AST.ASTint (sz', sg') ->
 408         Errors.OK (FrontEndOps.Onotbool (AST.ASTptr, sz', sg'))
 409       | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
 410 | Csyntax.Onotint ->
 411   (match t' with
 412    | AST.ASTint (sz, sg) ->
 413      typ_should_eq (AST.ASTint (sz, sg)) t (FrontEndOps.Onotint (sz, sg))
 414    | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 415 | Csyntax.Oneg ->
 416   (match t' with
 417    | AST.ASTint (sz, sg) ->
 418      typ_should_eq (AST.ASTint (sz, sg)) t (FrontEndOps.Onegint (sz, sg))
 419    | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 420
 421 (** val fix_ptr_type :
 422     Csyntax.type0 -> Nat.nat Types.option -> Cminor_syntax.expr ->
 423     Cminor_syntax.expr **)
 424 let fix_ptr_type ty n e =
 425   e
 426
 427 (** val translate_add :
 428     Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
 429     Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
 430 let translate_add ty1 ty2 ty' =
 431   let ty1' = Csyntax.typ_of_type ty1 in
 432   let ty2' = Csyntax.typ_of_type ty2 in
 433   (match ClassifyOp.classify_add ty1 ty2 with
 434    | ClassifyOp.Add_case_ii (sz, sg) ->
 435      (fun e1 e2 ->
 436        typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty')
 437          (Cminor_syntax.Op2 ((AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)),
 438          (AST.ASTint (sz, sg)), (FrontEndOps.Oadd (sz, sg)), e1, e2)))
 439    | ClassifyOp.Add_case_pi (n, ty, sz, sg) ->
 440      (fun e1 e2 ->
 441        typ_should_eq AST.ASTptr (Csyntax.typ_of_type ty') (Cminor_syntax.Op2
 442          (AST.ASTptr, (AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr,
 443          (FrontEndOps.Oaddpi AST.I16), (fix_ptr_type ty n e1),
 444          (Cminor_syntax.Op2 ((AST.ASTint (AST.I16, AST.Signed)), (AST.ASTint
 445          (AST.I16, AST.Signed)), (AST.ASTint (AST.I16, AST.Signed)),
 446          (FrontEndOps.Omul (AST.I16, AST.Signed)), (Cminor_syntax.Op1
 447          ((AST.ASTint (sz, sg)), (AST.ASTint (AST.I16, AST.Signed)),
 448          (FrontEndOps.Ocastint (sz, sg, AST.I16, AST.Signed)), e2)),
 449          (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)),
 450          (FrontEndOps.Ointconst (AST.I16, AST.Signed,
 451          (AST.repr AST.I16 (Csyntax.sizeof ty)))))))))))
 452    | ClassifyOp.Add_case_ip (n, sz, sg, ty) ->
 453      (fun e1 e2 ->
 454        typ_should_eq AST.ASTptr (Csyntax.typ_of_type ty') (Cminor_syntax.Op2
 455          ((AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr, AST.ASTptr,
 456          (FrontEndOps.Oaddip AST.I16), (Cminor_syntax.Op2 ((AST.ASTint
 457          (AST.I16, AST.Signed)), (AST.ASTint (AST.I16, AST.Signed)),
 458          (AST.ASTint (AST.I16, AST.Signed)), (FrontEndOps.Omul (AST.I16,
 459          AST.Signed)), (Cminor_syntax.Op1 ((AST.ASTint (sz, sg)), (AST.ASTint
 460          (AST.I16, AST.Signed)), (FrontEndOps.Ocastint (sz, sg, AST.I16,
 461          AST.Signed)), e1)), (Cminor_syntax.Cst ((AST.ASTint (AST.I16,
 462          AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed,
 463          (AST.repr AST.I16 (Csyntax.sizeof ty)))))))),
 464          (fix_ptr_type ty n e2))))
 465    | ClassifyOp.Add_default (x, x0) ->
 466      (fun e1 e2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
 467
 468 (** val translate_sub :
 469     Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
 470     Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
 471 let translate_sub ty1 ty2 ty' =
 472   let ty1' = Csyntax.typ_of_type ty1 in
 473   let ty2' = Csyntax.typ_of_type ty2 in
 474   (match ClassifyOp.classify_sub ty1 ty2 with
 475    | ClassifyOp.Sub_case_ii (sz, sg) ->
 476      (fun e1 e2 ->
 477        typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty')
 478          (Cminor_syntax.Op2 ((AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)),
 479          (AST.ASTint (sz, sg)), (FrontEndOps.Osub (sz, sg)), e1, e2)))
 480    | ClassifyOp.Sub_case_pi (n, ty, sz, sg) ->
 481      (fun e1 e2 ->
 482        typ_should_eq AST.ASTptr (Csyntax.typ_of_type ty') (Cminor_syntax.Op2
 483          (AST.ASTptr, (AST.ASTint (AST.I32, AST.Signed)), AST.ASTptr,
 484          (FrontEndOps.Osubpi AST.I32), (fix_ptr_type ty n e1),
 485          (Cminor_syntax.Op1 ((AST.ASTint (AST.I16, sg)), (AST.ASTint
 486          (AST.I32, AST.Signed)), (FrontEndOps.Ocastint (AST.I16, sg, AST.I32,
 487          AST.Signed)), (Cminor_syntax.Op2 ((AST.ASTint (AST.I16, sg)),
 488          (AST.ASTint (AST.I16, sg)), (AST.ASTint (AST.I16, sg)),
 489          (FrontEndOps.Omul (AST.I16, sg)), (Cminor_syntax.Op1 ((AST.ASTint
 490          (sz, sg)), (AST.ASTint (AST.I16, sg)), (FrontEndOps.Ocastint (sz,
 491          sg, AST.I16, sg)), e2)), (Cminor_syntax.Cst ((AST.ASTint (AST.I16,
 492          sg)), (FrontEndOps.Ointconst (AST.I16, sg,
 493          (AST.repr AST.I16 (Csyntax.sizeof ty)))))))))))))
 494    | ClassifyOp.Sub_case_pp (n1, n2, ty10, ty20) ->
 495      (fun e1 e2 ->
 496        match ty' with
 497        | Csyntax.Tvoid ->
 498          Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 499        | Csyntax.Tint (sz, sg) ->
 500          Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (AST.I32, AST.Unsigned)),
 501            (AST.ASTint (sz, sg)), (FrontEndOps.Ocastint (AST.I32,
 502            AST.Unsigned, sz, sg)), (Cminor_syntax.Op2 ((AST.ASTint (AST.I32,
 503            AST.Unsigned)), (AST.ASTint (AST.I32, AST.Unsigned)), (AST.ASTint
 504            (AST.I32, AST.Unsigned)), (FrontEndOps.Odivu AST.I32),
 505            (Cminor_syntax.Op2 (AST.ASTptr, AST.ASTptr, (AST.ASTint (AST.I32,
 506            AST.Unsigned)), (FrontEndOps.Osubpp AST.I32),
 507            (fix_ptr_type ty10 n1 e1), (fix_ptr_type ty20 n2 e2))),
 508            (Cminor_syntax.Cst ((AST.ASTint (AST.I32, AST.Unsigned)),
 509            (FrontEndOps.Ointconst (AST.I32, AST.Unsigned,
 510            (AST.repr AST.I32 (Csyntax.sizeof ty10))))))))))
 511        | Csyntax.Tpointer x ->
 512          Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 513        | Csyntax.Tarray (x, x0) ->
 514          Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 515        | Csyntax.Tfunction (x, x0) ->
 516          Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 517        | Csyntax.Tstruct (x, x0) ->
 518          Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 519        | Csyntax.Tunion (x, x0) ->
 520          Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 521        | Csyntax.Tcomp_ptr x ->
 522          Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 523    | ClassifyOp.Sub_default (x, x0) ->
 524      (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
 525
 526 (** val translate_mul :
 527     Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
 528     Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
 529 let translate_mul ty1 ty2 ty' =
 530   let ty1' = Csyntax.typ_of_type ty1 in
 531   let ty2' = Csyntax.typ_of_type ty2 in
 532   (match ClassifyOp.classify_aop ty1 ty2 with
 533    | ClassifyOp.Aop_case_ii (sz, sg) ->
 534      (fun e1 e2 ->
 535        typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty')
 536          (Cminor_syntax.Op2 ((AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)),
 537          (AST.ASTint (sz, sg)), (FrontEndOps.Omul (sz, sg)), e1, e2)))
 538    | ClassifyOp.Aop_default (x, x0) ->
 539      (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
 540
 541 (** val translate_div :
 542     Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
 543     Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
 544 let translate_div ty1 ty2 ty' =
 545   let ty1' = Csyntax.typ_of_type ty1 in
 546   let ty2' = Csyntax.typ_of_type ty2 in
 547   (match ClassifyOp.classify_aop ty1 ty2 with
 548    | ClassifyOp.Aop_case_ii (sz, sg) ->
 549      (match sg with
 550       | AST.Signed ->
 551         (fun e1 e2 ->
 552           typ_should_eq (AST.ASTint (sz, AST.Signed))
 553             (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
 554             AST.Signed)), (AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz,
 555             AST.Signed)), (FrontEndOps.Odiv sz), e1, e2)))
 556       | AST.Unsigned ->
 557         (fun e1 e2 ->
 558           typ_should_eq (AST.ASTint (sz, AST.Unsigned))
 559             (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
 560             AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz,
 561             AST.Unsigned)), (FrontEndOps.Odivu sz), e1, e2))))
 562    | ClassifyOp.Aop_default (x, x0) ->
 563      (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
 564
 565 (** val translate_mod :
 566     Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
 567     Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
 568 let translate_mod ty1 ty2 ty' =
 569   let ty1' = Csyntax.typ_of_type ty1 in
 570   let ty2' = Csyntax.typ_of_type ty2 in
 571   (match ClassifyOp.classify_aop ty1 ty2 with
 572    | ClassifyOp.Aop_case_ii (sz, sg) ->
 573      (match sg with
 574       | AST.Signed ->
 575         (fun e1 e2 ->
 576           typ_should_eq (AST.ASTint (sz, AST.Signed))
 577             (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
 578             AST.Signed)), (AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz,
 579             AST.Signed)), (FrontEndOps.Omod sz), e1, e2)))
 580       | AST.Unsigned ->
 581         (fun e1 e2 ->
 582           typ_should_eq (AST.ASTint (sz, AST.Unsigned))
 583             (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
 584             AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz,
 585             AST.Unsigned)), (FrontEndOps.Omodu sz), e1, e2))))
 586    | ClassifyOp.Aop_default (x, x0) ->
 587      (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
 588
 589 (** val translate_shr :
 590     Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
 591     Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
 592 let translate_shr ty1 ty2 ty' =
 593   let ty1' = Csyntax.typ_of_type ty1 in
 594   let ty2' = Csyntax.typ_of_type ty2 in
 595   (match ClassifyOp.classify_aop ty1 ty2 with
 596    | ClassifyOp.Aop_case_ii (sz, sg) ->
 597      (match sg with
 598       | AST.Signed ->
 599         (fun e1 e2 ->
 600           typ_should_eq (AST.ASTint (sz, AST.Signed))
 601             (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
 602             AST.Signed)), (AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz,
 603             AST.Signed)), (FrontEndOps.Oshr (sz, AST.Signed)), e1, e2)))
 604       | AST.Unsigned ->
 605         (fun e1 e2 ->
 606           typ_should_eq (AST.ASTint (sz, AST.Unsigned))
 607             (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
 608             AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz,
 609             AST.Unsigned)), (FrontEndOps.Oshru (sz, AST.Unsigned)), e1, e2))))
 610    | ClassifyOp.Aop_default (x, x0) ->
 611      (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
 612
 613 (** val complete_cmp :
 614     Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
 615 let complete_cmp ty' e =
 616   match ty' with
 617   | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 618   | Csyntax.Tint (sz, sg) ->
 619     Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (AST.I8, AST.Unsigned)),
 620       (AST.ASTint (sz, sg)), (FrontEndOps.Ocastint (AST.I8, AST.Unsigned, sz,
 621       sg)), e))
 622   | Csyntax.Tpointer x ->
 623     Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 624   | Csyntax.Tarray (x, x0) ->
 625     Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 626   | Csyntax.Tfunction (x, x0) ->
 627     Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 628   | Csyntax.Tstruct (x, x0) ->
 629     Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 630   | Csyntax.Tunion (x, x0) ->
 631     Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 632   | Csyntax.Tcomp_ptr x ->
 633     Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 634
 635 (** val translate_cmp :
 636     Integers.comparison -> Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 ->
 637     Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
 638 let translate_cmp c ty1 ty2 ty' =
 639   let ty1' = Csyntax.typ_of_type ty1 in
 640   let ty2' = Csyntax.typ_of_type ty2 in
 641   (match ClassifyOp.classify_cmp ty1 ty2 with
 642    | ClassifyOp.Cmp_case_ii (sz, sg) ->
 643      (match sg with
 644       | AST.Signed ->
 645         (fun e1 e2 ->
 646           complete_cmp ty' (Cminor_syntax.Op2 ((AST.ASTint (sz, AST.Signed)),
 647             (AST.ASTint (sz, AST.Signed)), (AST.ASTint (AST.I8,
 648             AST.Unsigned)), (FrontEndOps.Ocmp (sz, AST.Signed, AST.Unsigned,
 649             c)), e1, e2)))
 650       | AST.Unsigned ->
 651         (fun e1 e2 ->
 652           complete_cmp ty' (Cminor_syntax.Op2 ((AST.ASTint (sz,
 653             AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint
 654             (AST.I8, AST.Unsigned)), (FrontEndOps.Ocmpu (sz, AST.Unsigned,
 655             c)), e1, e2))))
 656    | ClassifyOp.Cmp_case_pp (n, ty) ->
 657      (fun e1 e2 ->
 658        complete_cmp ty' (Cminor_syntax.Op2 (AST.ASTptr, AST.ASTptr,
 659          (AST.ASTint (AST.I8, AST.Unsigned)), (FrontEndOps.Ocmpp
 660          (AST.Unsigned, c)), (fix_ptr_type ty n e1), (fix_ptr_type ty n e2))))
 661    | ClassifyOp.Cmp_default (x, x0) ->
 662      (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
 663
 664 (** val translate_misc_aop :
 665     Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> (AST.intsize ->
 666     AST.signedness -> FrontEndOps.binary_operation) -> Cminor_syntax.expr ->
 667     Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
 668 let translate_misc_aop ty1 ty2 ty' op =
 669   let ty1' = Csyntax.typ_of_type ty1 in
 670   let ty2' = Csyntax.typ_of_type ty2 in
 671   (match ClassifyOp.classify_aop ty1 ty2 with
 672    | ClassifyOp.Aop_case_ii (sz, sg) ->
 673      (fun e1 e2 ->
 674        typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty')
 675          (Cminor_syntax.Op2 ((Csyntax.typ_of_type (Csyntax.Tint (sz, sg))),
 676          (Csyntax.typ_of_type (Csyntax.Tint (sz, sg))), (AST.ASTint (sz,
 677          sg)), (op sz sg), e1, e2)))
 678    | ClassifyOp.Aop_default (x, x0) ->
 679      (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
 680
 681 (** val translate_binop :
 682     Csyntax.binary_operation -> Csyntax.type0 -> Cminor_syntax.expr ->
 683     Csyntax.type0 -> Cminor_syntax.expr -> Csyntax.type0 ->
 684     Cminor_syntax.expr Errors.res **)
 685 let translate_binop op ty1 e1 ty2 e2 ty =
 686   let ty' = Csyntax.typ_of_type ty in
 687   (match op with
 688    | Csyntax.Oadd -> translate_add ty1 ty2 ty e1 e2
 689    | Csyntax.Osub -> translate_sub ty1 ty2 ty e1 e2
 690    | Csyntax.Omul -> translate_mul ty1 ty2 ty e1 e2
 691    | Csyntax.Odiv -> translate_div ty1 ty2 ty e1 e2
 692    | Csyntax.Omod -> translate_mod ty1 ty2 ty e1 e2
 693    | Csyntax.Oand ->
 694      translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oand (x, x0)) e1
 695        e2
 696    | Csyntax.Oor ->
 697      translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oor (x, x0)) e1
 698        e2
 699    | Csyntax.Oxor ->
 700      translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oxor (x, x0)) e1
 701        e2
 702    | Csyntax.Oshl ->
 703      translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oshl (x, x0)) e1
 704        e2
 705    | Csyntax.Oshr -> translate_shr ty1 ty2 ty e1 e2
 706    | Csyntax.Oeq -> translate_cmp Integers.Ceq ty1 ty2 ty e1 e2
 707    | Csyntax.One -> translate_cmp Integers.Cne ty1 ty2 ty e1 e2
 708    | Csyntax.Olt -> translate_cmp Integers.Clt ty1 ty2 ty e1 e2
 709    | Csyntax.Ogt -> translate_cmp Integers.Cgt ty1 ty2 ty e1 e2
 710    | Csyntax.Ole -> translate_cmp Integers.Cle ty1 ty2 ty e1 e2
 711    | Csyntax.Oge -> translate_cmp Integers.Cge ty1 ty2 ty e1 e2)
 712
 713 (** val translate_cast :
 714     Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr Types.sig0 ->
 715     Cminor_syntax.expr Types.sig0 Errors.res **)
 716 let translate_cast ty1 ty2 =
 717   match ty1 with
 718   | Csyntax.Tvoid ->
 719     (fun x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 720   | Csyntax.Tint (sz1, sg1) ->
 721     (fun e ->
 722       match ty2 with
 723       | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 724       | Csyntax.Tint (sz2, sg2) ->
 725         Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), (AST.ASTint
 726           (sz2, sg2)), (FrontEndOps.Ocastint (sz1, sg1, sz2, sg2)),
 727           (Types.pi1 e)))
 728       | Csyntax.Tpointer x ->
 729         Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), AST.ASTptr,
 730           (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e)))
 731       | Csyntax.Tarray (x, x0) ->
 732         Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), AST.ASTptr,
 733           (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e)))
 734       | Csyntax.Tfunction (x, x0) ->
 735         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 736       | Csyntax.Tstruct (x, x0) ->
 737         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 738       | Csyntax.Tunion (x, x0) ->
 739         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 740       | Csyntax.Tcomp_ptr x ->
 741         Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 742   | Csyntax.Tpointer x ->
 743     (fun e ->
 744       match ty2 with
 745       | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 746       | Csyntax.Tint (sz2, sg2) ->
 747         Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)),
 748           (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e)))
 749       | Csyntax.Tpointer x0 -> Errors.OK e
 750       | Csyntax.Tarray (x0, x1) -> Errors.OK e
 751       | Csyntax.Tfunction (x0, x1) ->
 752         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 753       | Csyntax.Tstruct (x0, x1) ->
 754         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 755       | Csyntax.Tunion (x0, x1) ->
 756         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 757       | Csyntax.Tcomp_ptr x0 ->
 758         Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 759   | Csyntax.Tarray (x, x0) ->
 760     (fun e ->
 761       match ty2 with
 762       | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 763       | Csyntax.Tint (sz2, sg2) ->
 764         Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)),
 765           (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e)))
 766       | Csyntax.Tpointer x1 -> Errors.OK e
 767       | Csyntax.Tarray (x1, x2) -> Errors.OK e
 768       | Csyntax.Tfunction (x1, x2) ->
 769         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 770       | Csyntax.Tstruct (x1, x2) ->
 771         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 772       | Csyntax.Tunion (x1, x2) ->
 773         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 774       | Csyntax.Tcomp_ptr x1 ->
 775         Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 776   | Csyntax.Tfunction (x, x0) ->
 777     (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 778   | Csyntax.Tstruct (x, x0) ->
 779     (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 780   | Csyntax.Tunion (x, x0) ->
 781     (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 782   | Csyntax.Tcomp_ptr x ->
 783     (fun x0 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 784
 785 (** val cm_zero : AST.intsize -> AST.signedness -> Cminor_syntax.expr **)
 786 let cm_zero sz sg =
 787   Cminor_syntax.Cst ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg,
 788     (BitVector.zero (AST.bitsize_of_intsize sz)))))
 789
 790 (** val cm_one : AST.intsize -> AST.signedness -> Cminor_syntax.expr **)
 791 let cm_one sz sg =
 792   Cminor_syntax.Cst ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg,
 793     (AST.repr sz (Nat.S Nat.O)))))
 794
 795 (** val translate_expr :
 796     var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res **)
 797 let rec translate_expr vars = function
 798 | Csyntax.Expr (ed, ty) ->
 799   (match ed with
 800    | Csyntax.Econst_int (sz, i) ->
 801      (match ty with
 802       | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 803       | Csyntax.Tint (sz', sg) ->
 804         AST.intsize_eq_elim' sz sz' (Errors.OK (Cminor_syntax.Cst
 805           ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg, i)))))
 806           (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 807       | Csyntax.Tpointer x ->
 808         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 809       | Csyntax.Tarray (x, x0) ->
 810         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 811       | Csyntax.Tfunction (x, x0) ->
 812         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 813       | Csyntax.Tstruct (x, x0) ->
 814         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 815       | Csyntax.Tunion (x, x0) ->
 816         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
 817       | Csyntax.Tcomp_ptr x ->
 818         Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 819    | Csyntax.Evar id ->
 820      Errors.bind2_eq (lookup' vars id) (fun c t _ ->
 821        (match c with
 822         | Global r ->
 823           (fun _ ->
 824             match Csyntax.access_mode ty with
 825             | Csyntax.By_value t0 ->
 826               Errors.OK (Cminor_syntax.Mem (t0, (Cminor_syntax.Cst
 827                 (AST.ASTptr, (FrontEndOps.Oaddrsymbol (id, Nat.O))))))
 828             | Csyntax.By_reference ->
 829               Errors.OK (Cminor_syntax.Cst (AST.ASTptr,
 830                 (FrontEndOps.Oaddrsymbol (id, Nat.O))))
 831             | Csyntax.By_nothing x ->
 832               Errors.Error (List.Cons ((Errors.MSG
 833                 ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX
 834                 (PreIdentifiers.SymbolTag, id)), List.Nil)))))
 835         | Stack n ->
 836           (fun _ ->
 837             match Csyntax.access_mode ty with
 838             | Csyntax.By_value t0 ->
 839               Errors.OK (Cminor_syntax.Mem (t0, (Cminor_syntax.Cst
 840                 (AST.ASTptr, (FrontEndOps.Oaddrstack n)))))
 841             | Csyntax.By_reference ->
 842               Errors.OK (Cminor_syntax.Cst (AST.ASTptr,
 843                 (FrontEndOps.Oaddrstack n)))
 844             | Csyntax.By_nothing x ->
 845               Errors.Error (List.Cons ((Errors.MSG
 846                 ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX
 847                 (PreIdentifiers.SymbolTag, id)), List.Nil)))))
 848         | Local ->
 849           (fun _ ->
 850             type_should_eq t ty (Cminor_syntax.Id ((Csyntax.typ_of_type t),
 851               id)))) __)
 852    | Csyntax.Ederef e1 ->
 853      Obj.magic
 854        (Monad.m_bind0 (Monad.max_def Errors.res0)
 855          (Obj.magic (translate_expr vars e1)) (fun e1' ->
 856          (match Csyntax.typ_of_type (Csyntax.typeof e1) with
 857           | AST.ASTint (x, x0) ->
 858             (fun x1 ->
 859               Obj.magic (Errors.Error
 860                 (Errors.msg ErrorMessages.TypeMismatch)))
 861           | AST.ASTptr ->
 862             (fun e1'0 ->
 863               match Csyntax.access_mode ty with
 864               | Csyntax.By_value t ->
 865                 Obj.magic (Errors.OK (Cminor_syntax.Mem (t,
 866                   (Types.pi1 e1'0))))
 867               | Csyntax.By_reference -> Obj.magic (Errors.OK e1'0)
 868               | Csyntax.By_nothing x ->
 869                 Obj.magic (Errors.Error
 870                   (Errors.msg ErrorMessages.BadlyTypedAccess)))) e1'))
 871    | Csyntax.Eaddrof e1 ->
 872      Obj.magic
 873        (Monad.m_bind0 (Monad.max_def Errors.res0)
 874          (Obj.magic (translate_addr vars e1)) (fun e1' ->
 875          match Csyntax.typ_of_type ty with
 876          | AST.ASTint (x, x0) ->
 877            Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 878          | AST.ASTptr -> Obj.magic (Errors.OK e1')))
 879    | Csyntax.Eunop (op, e1) ->
 880      (match op with
 881       | Csyntax.Onotbool ->
 882         (fun _ ->
 883           (match Csyntax.typ_of_type ty with
 884            | AST.ASTint (sz, sg) ->
 885              (fun _ ->
 886                (match sz with
 887                 | AST.I8 ->
 888                   (fun _ -> Errors.Error
 889                     (Errors.msg ErrorMessages.TypeMismatch))
 890                 | AST.I16 ->
 891                   (fun _ -> Errors.Error
 892                     (Errors.msg ErrorMessages.TypeMismatch))
 893                 | AST.I32 ->
 894                   (fun _ ->
 895                     Obj.magic
 896                       (Monad.m_bind0 (Monad.max_def Errors.res0)
 897                         (Obj.magic
 898                           (translate_unop
 899                             (Csyntax.typ_of_type (Csyntax.typeof e1))
 900                             (Csyntax.typ_of_type ty) op)) (fun op' ->
 901                         Monad.m_bind0 (Monad.max_def Errors.res0)
 902                           (Obj.magic (translate_expr vars e1)) (fun e1' ->
 903                           Obj.magic (Errors.OK (Cminor_syntax.Op1
 904                             ((Csyntax.typ_of_type (Csyntax.typeof e1)),
 905                             (Csyntax.typ_of_type ty), op', (Types.pi1 e1')))))))))
 906                  __)
 907            | AST.ASTptr ->
 908              (fun _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
 909             __)
 910       | Csyntax.Onotint ->
 911         (fun _ ->
 912           Obj.magic
 913             (Monad.m_bind0 (Monad.max_def Errors.res0)
 914               (Obj.magic
 915                 (translate_unop (Csyntax.typ_of_type (Csyntax.typeof e1))
 916                   (Csyntax.typ_of_type ty) op)) (fun op' ->
 917               Monad.m_bind0 (Monad.max_def Errors.res0)
 918                 (Obj.magic (translate_expr vars e1)) (fun e1' ->
 919                 Obj.magic (Errors.OK (Cminor_syntax.Op1
 920                   ((Csyntax.typ_of_type (Csyntax.typeof e1)),
 921                   (Csyntax.typ_of_type ty), op', (Types.pi1 e1'))))))))
 922       | Csyntax.Oneg ->
 923         (fun _ ->
 924           Obj.magic
 925             (Monad.m_bind0 (Monad.max_def Errors.res0)
 926               (Obj.magic
 927                 (translate_unop (Csyntax.typ_of_type (Csyntax.typeof e1))
 928                   (Csyntax.typ_of_type ty) op)) (fun op' ->
 929               Monad.m_bind0 (Monad.max_def Errors.res0)
 930                 (Obj.magic (translate_expr vars e1)) (fun e1' ->
 931                 Obj.magic (Errors.OK (Cminor_syntax.Op1
 932                   ((Csyntax.typ_of_type (Csyntax.typeof e1)),
 933                   (Csyntax.typ_of_type ty), op', (Types.pi1 e1'))))))))) __
 934    | Csyntax.Ebinop (op, e1, e2) ->
 935      Obj.magic
 936        (Monad.m_bind0 (Monad.max_def Errors.res0)
 937          (Obj.magic (translate_expr vars e1)) (fun e1' ->
 938          Monad.m_bind0 (Monad.max_def Errors.res0)
 939            (Obj.magic (translate_expr vars e2)) (fun e2' ->
 940            Obj.magic
 941              (Errors.bind_eq
 942                (translate_binop op (Csyntax.typeof e1) (Types.pi1 e1')
 943                  (Csyntax.typeof e2) (Types.pi1 e2') ty) (fun e' _ ->
 944                Errors.OK e')))))
 945    | Csyntax.Ecast (ty1, e1) ->
 946      Obj.magic
 947        (Monad.m_bind0 (Monad.max_def Errors.res0)
 948          (Obj.magic (translate_expr vars e1)) (fun e1' ->
 949          Monad.m_bind0 (Monad.max_def Errors.res0)
 950            (Obj.magic (translate_cast (Csyntax.typeof e1) ty1 e1'))
 951            (fun e' ->
 952            Monad.m_bind0 (Monad.max_def Errors.res0)
 953              (Obj.magic
 954                (typ_should_eq (Csyntax.typ_of_type ty1)
 955                  (Csyntax.typ_of_type ty) e')) (fun e'0 ->
 956              Obj.magic (Errors.OK e'0)))))
 957    | Csyntax.Econdition (e1, e2, e3) ->
 958      Obj.magic
 959        (Monad.m_bind0 (Monad.max_def Errors.res0)
 960          (Obj.magic (translate_expr vars e1)) (fun e1' ->
 961          Monad.m_bind0 (Monad.max_def Errors.res0)
 962            (Obj.magic (translate_expr vars e2)) (fun e2' ->
 963            Monad.m_bind0 (Monad.max_def Errors.res0)
 964              (Obj.magic
 965                (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e2))
 966                  (Csyntax.typ_of_type ty) e2')) (fun e2'0 ->
 967              Monad.m_bind0 (Monad.max_def Errors.res0)
 968                (Obj.magic (translate_expr vars e3)) (fun e3' ->
 969                Monad.m_bind0 (Monad.max_def Errors.res0)
 970                  (Obj.magic
 971                    (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e3))
 972                      (Csyntax.typ_of_type ty) e3')) (fun e3'0 ->
 973                  (match Csyntax.typ_of_type (Csyntax.typeof e1) with
 974                   | AST.ASTint (x, x0) ->
 975                     (fun e1'0 ->
 976                       Obj.magic (Errors.OK (Cminor_syntax.Cond (x, x0,
 977                         (Csyntax.typ_of_type ty), (Types.pi1 e1'0),
 978                         (Types.pi1 e2'0), (Types.pi1 e3'0)))))
 979                   | AST.ASTptr ->
 980                     (fun x ->
 981                       Obj.magic (Errors.Error
 982                         (Errors.msg ErrorMessages.TypeMismatch)))) e1'))))))
 983    | Csyntax.Eandbool (e1, e2) ->
 984      Obj.magic
 985        (Monad.m_bind0 (Monad.max_def Errors.res0)
 986          (Obj.magic (translate_expr vars e1)) (fun e1' ->
 987          Monad.m_bind0 (Monad.max_def Errors.res0)
 988            (Obj.magic (translate_expr vars e2)) (fun e2' ->
 989            match ty with
 990            | Csyntax.Tvoid ->
 991              Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
 992            | Csyntax.Tint (sz, sg) ->
 993              Monad.m_bind0 (Monad.max_def Errors.res0)
 994                (Obj.magic
 995                  (type_should_eq (Csyntax.typeof e2) (Csyntax.Tint (sz, sg))
 996                    e2')) (fun e2'0 ->
 997                (match Csyntax.typ_of_type (Csyntax.typeof e1) with
 998                 | AST.ASTint (sz1, x) ->
 999                   (fun e1'0 ->
1000                     Obj.magic (Errors.OK (Cminor_syntax.Cond (sz1, x,
1001                       (AST.ASTint (sz, sg)), (Types.pi1 e1'0),
1002                       (Cminor_syntax.Cond (sz, sg, (AST.ASTint (sz, sg)),
1003                       (Types.pi1 e2'0), (cm_one sz sg), (cm_zero sz sg))),
1004                       (cm_zero sz sg)))))
1005                 | AST.ASTptr ->
1006                   (fun x ->
1007                     Obj.magic (Errors.Error
1008                       (Errors.msg ErrorMessages.TypeMismatch)))) e1')
1009            | Csyntax.Tpointer x ->
1010              Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1011            | Csyntax.Tarray (x, x0) ->
1012              Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1013            | Csyntax.Tfunction (x, x0) ->
1014              Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1015            | Csyntax.Tstruct (x, x0) ->
1016              Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1017            | Csyntax.Tunion (x, x0) ->
1018              Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1019            | Csyntax.Tcomp_ptr x ->
1020              Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))))
1021    | Csyntax.Eorbool (e1, e2) ->
1022      Obj.magic
1023        (Monad.m_bind0 (Monad.max_def Errors.res0)
1024          (Obj.magic (translate_expr vars e1)) (fun e1' ->
1025          Monad.m_bind0 (Monad.max_def Errors.res0)
1026            (Obj.magic (translate_expr vars e2)) (fun e2' ->
1027            match ty with
1028            | Csyntax.Tvoid ->
1029              Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1030            | Csyntax.Tint (sz, sg) ->
1031              Monad.m_bind0 (Monad.max_def Errors.res0)
1032                (Obj.magic
1033                  (type_should_eq (Csyntax.typeof e2) (Csyntax.Tint (sz, sg))
1034                    e2')) (fun e2'0 ->
1035                (match Csyntax.typ_of_type (Csyntax.typeof e1) with
1036                 | AST.ASTint (x, x0) ->
1037                   (fun e1'0 ->
1038                     Obj.magic (Errors.OK (Cminor_syntax.Cond (x, x0,
1039                       (AST.ASTint (sz, sg)), (Types.pi1 e1'0),
1040                       (cm_one sz sg), (Cminor_syntax.Cond (sz, sg,
1041                       (AST.ASTint (sz, sg)), (Types.pi1 e2'0),
1042                       (cm_one sz sg), (cm_zero sz sg)))))))
1043                 | AST.ASTptr ->
1044                   (fun x ->
1045                     Obj.magic (Errors.Error
1046                       (Errors.msg ErrorMessages.TypeMismatch)))) e1')
1047            | Csyntax.Tpointer x ->
1048              Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1049            | Csyntax.Tarray (x, x0) ->
1050              Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1051            | Csyntax.Tfunction (x, x0) ->
1052              Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1053            | Csyntax.Tstruct (x, x0) ->
1054              Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1055            | Csyntax.Tunion (x, x0) ->
1056              Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1057            | Csyntax.Tcomp_ptr x ->
1058              Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))))
1059    | Csyntax.Esizeof ty1 ->
1060      (match ty with
1061       | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
1062       | Csyntax.Tint (sz, sg) ->
1063         Errors.OK (Cminor_syntax.Cst ((AST.ASTint (sz, sg)),
1064           (FrontEndOps.Ointconst (sz, sg,
1065           (AST.repr sz (Csyntax.sizeof ty1))))))
1066       | Csyntax.Tpointer x ->
1067         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
1068       | Csyntax.Tarray (x, x0) ->
1069         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
1070       | Csyntax.Tfunction (x, x0) ->
1071         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
1072       | Csyntax.Tstruct (x, x0) ->
1073         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
1074       | Csyntax.Tunion (x, x0) ->
1075         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
1076       | Csyntax.Tcomp_ptr x ->
1077         Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1078    | Csyntax.Efield (e1, id) ->
1079      (match Csyntax.typeof e1 with
1080       | Csyntax.Tvoid ->
1081         Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1082       | Csyntax.Tint (x, x0) ->
1083         Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1084       | Csyntax.Tpointer x ->
1085         Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1086       | Csyntax.Tarray (x, x0) ->
1087         Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1088       | Csyntax.Tfunction (x, x0) ->
1089         Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1090       | Csyntax.Tstruct (x, fl) ->
1091         Obj.magic
1092           (Monad.m_bind0 (Monad.max_def Errors.res0)
1093             (Obj.magic (translate_addr vars e1)) (fun e1' ->
1094             Monad.m_bind0 (Monad.max_def Errors.res0)
1095               (Obj.magic (Csyntax.field_offset id fl)) (fun off ->
1096               match Csyntax.access_mode ty with
1097               | Csyntax.By_value t ->
1098                 Obj.magic (Errors.OK (Cminor_syntax.Mem (t,
1099                   (Cminor_syntax.Op2 (AST.ASTptr, (AST.ASTint (AST.I16,
1100                   AST.Signed)), AST.ASTptr, (FrontEndOps.Oaddpi AST.I16),
1101                   (Types.pi1 e1'), (Cminor_syntax.Cst ((AST.ASTint (AST.I16,
1102                   AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed,
1103                   (AST.repr AST.I16 off))))))))))
1104               | Csyntax.By_reference ->
1105                 Obj.magic (Errors.OK (Cminor_syntax.Op2 (AST.ASTptr,
1106                   (AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr,
1107                   (FrontEndOps.Oaddpi AST.I16), (Types.pi1 e1'),
1108                   (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)),
1109                   (FrontEndOps.Ointconst (AST.I16, AST.Signed,
1110                   (AST.repr AST.I16 off))))))))
1111               | Csyntax.By_nothing x0 ->
1112                 Obj.magic (Errors.Error
1113                   (Errors.msg ErrorMessages.BadlyTypedAccess)))))
1114       | Csyntax.Tunion (x, x0) ->
1115         Obj.magic
1116           (Monad.m_bind0 (Monad.max_def Errors.res0)
1117             (Obj.magic (translate_addr vars e1)) (fun e1' ->
1118             match Csyntax.access_mode ty with
1119             | Csyntax.By_value t ->
1120               Obj.magic (Errors.OK (Cminor_syntax.Mem (t, (Types.pi1 e1'))))
1121             | Csyntax.By_reference -> Obj.magic (Errors.OK e1')
1122             | Csyntax.By_nothing x1 ->
1123               Obj.magic (Errors.Error
1124                 (Errors.msg ErrorMessages.BadlyTypedAccess))))
1125       | Csyntax.Tcomp_ptr x ->
1126         Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess))
1127    | Csyntax.Ecost (l, e1) ->
1128      Obj.magic
1129        (Monad.m_bind0 (Monad.max_def Errors.res0)
1130          (Obj.magic (translate_expr vars e1)) (fun e1' ->
1131          Monad.m_bind0 (Monad.max_def Errors.res0)
1132            (Obj.magic (Errors.OK (Cminor_syntax.Ecost
1133              ((Csyntax.typ_of_type (Csyntax.typeof e1)), l,
1134              (Types.pi1 e1'))))) (fun e' ->
1135            Obj.magic
1136              (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e1))
1137                (Csyntax.typ_of_type ty) e')))))
1138 (** val translate_addr :
1139     var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res **)
1140 and translate_addr vars = function
1141 | Csyntax.Expr (ed, x) ->
1142   (match ed with
1143    | Csyntax.Econst_int (x0, x1) ->
1144      Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1145    | Csyntax.Evar id ->
1146      Obj.magic
1147        (Monad.m_bind2 (Monad.max_def Errors.res0)
1148          (Obj.magic (lookup' vars id)) (fun c t ->
1149          match c with
1150          | Global r ->
1151            Obj.magic (Errors.OK (Cminor_syntax.Cst (AST.ASTptr,
1152              (FrontEndOps.Oaddrsymbol (id, Nat.O)))))
1153          | Stack n ->
1154            Obj.magic (Errors.OK (Cminor_syntax.Cst (AST.ASTptr,
1155              (FrontEndOps.Oaddrstack n))))
1156          | Local ->
1157            Obj.magic (Errors.Error (List.Cons ((Errors.MSG
1158              ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX
1159              (PreIdentifiers.SymbolTag, id)), List.Nil)))))))
1160    | Csyntax.Ederef e1 ->
1161      Obj.magic
1162        (Monad.m_bind0 (Monad.max_def Errors.res0)
1163          (Obj.magic (translate_expr vars e1)) (fun e1' ->
1164          (match Csyntax.typ_of_type (Csyntax.typeof e1) with
1165           | AST.ASTint (x0, x1) ->
1166             (fun x2 ->
1167               Obj.magic (Errors.Error
1168                 (Errors.msg ErrorMessages.BadlyTypedAccess)))
1169           | AST.ASTptr -> (fun e1'0 -> Obj.magic (Errors.OK e1'0))) e1'))
1170    | Csyntax.Eaddrof x0 -> Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1171    | Csyntax.Eunop (x0, x1) ->
1172      Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1173    | Csyntax.Ebinop (x0, x1, x2) ->
1174      Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1175    | Csyntax.Ecast (x0, x1) ->
1176      Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1177    | Csyntax.Econdition (x0, x1, x2) ->
1178      Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1179    | Csyntax.Eandbool (x0, x1) ->
1180      Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1181    | Csyntax.Eorbool (x0, x1) ->
1182      Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1183    | Csyntax.Esizeof x0 -> Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1184    | Csyntax.Efield (e1, id) ->
1185      (match Csyntax.typeof e1 with
1186       | Csyntax.Tvoid ->
1187         Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1188       | Csyntax.Tint (x0, x1) ->
1189         Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1190       | Csyntax.Tpointer x0 ->
1191         Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1192       | Csyntax.Tarray (x0, x1) ->
1193         Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1194       | Csyntax.Tfunction (x0, x1) ->
1195         Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1196       | Csyntax.Tstruct (x0, fl) ->
1197         Obj.magic
1198           (Monad.m_bind0 (Monad.max_def Errors.res0)
1199             (Obj.magic (translate_addr vars e1)) (fun e1' ->
1200             Monad.m_bind0 (Monad.max_def Errors.res0)
1201               (Obj.magic (Csyntax.field_offset id fl)) (fun off ->
1202               Obj.magic (Errors.OK (Cminor_syntax.Op2 (AST.ASTptr,
1203                 (AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr,
1204                 (FrontEndOps.Oaddpi AST.I16), (Types.pi1 e1'),
1205                 (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)),
1206                 (FrontEndOps.Ointconst (AST.I16, AST.Signed,
1207                 (AST.repr AST.I16 off)))))))))))
1208       | Csyntax.Tunion (x0, x1) -> translate_addr vars e1
1209       | Csyntax.Tcomp_ptr x0 ->
1210         Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess))
1211    | Csyntax.Ecost (x0, x1) ->
1212      Errors.Error (Errors.msg ErrorMessages.BadLvalue))
1213
1214 type destination =
1215 | IdDest of AST.ident
1216 | MemDest of Cminor_syntax.expr Types.sig0
1217
1218 (** val destination_rect_Type4 :
1219     var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
1220     Types.sig0 -> 'a1) -> destination -> 'a1 **)
1221 let rec destination_rect_Type4 vars t h_IdDest h_MemDest = function
1222 | IdDest id -> h_IdDest id __
1223 | MemDest x_14524 -> h_MemDest x_14524
1224
1225 (** val destination_rect_Type5 :
1226     var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
1227     Types.sig0 -> 'a1) -> destination -> 'a1 **)
1228 let rec destination_rect_Type5 vars t h_IdDest h_MemDest = function
1229 | IdDest id -> h_IdDest id __
1230 | MemDest x_14529 -> h_MemDest x_14529
1231
1232 (** val destination_rect_Type3 :
1233     var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
1234     Types.sig0 -> 'a1) -> destination -> 'a1 **)
1235 let rec destination_rect_Type3 vars t h_IdDest h_MemDest = function
1236 | IdDest id -> h_IdDest id __
1237 | MemDest x_14534 -> h_MemDest x_14534
1238
1239 (** val destination_rect_Type2 :
1240     var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
1241     Types.sig0 -> 'a1) -> destination -> 'a1 **)
1242 let rec destination_rect_Type2 vars t h_IdDest h_MemDest = function
1243 | IdDest id -> h_IdDest id __
1244 | MemDest x_14539 -> h_MemDest x_14539
1245
1246 (** val destination_rect_Type1 :
1247     var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
1248     Types.sig0 -> 'a1) -> destination -> 'a1 **)
1249 let rec destination_rect_Type1 vars t h_IdDest h_MemDest = function
1250 | IdDest id -> h_IdDest id __
1251 | MemDest x_14544 -> h_MemDest x_14544
1252
1253 (** val destination_rect_Type0 :
1254     var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
1255     Types.sig0 -> 'a1) -> destination -> 'a1 **)
1256 let rec destination_rect_Type0 vars t h_IdDest h_MemDest = function
1257 | IdDest id -> h_IdDest id __
1258 | MemDest x_14549 -> h_MemDest x_14549
1259
1260 (** val destination_inv_rect_Type4 :
1261     var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
1262     (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
1263 let destination_inv_rect_Type4 x1 x2 hterm h1 h2 =
1264   let hcut = destination_rect_Type4 x1 x2 h1 h2 hterm in hcut __
1265
1266 (** val destination_inv_rect_Type3 :
1267     var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
1268     (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
1269 let destination_inv_rect_Type3 x1 x2 hterm h1 h2 =
1270   let hcut = destination_rect_Type3 x1 x2 h1 h2 hterm in hcut __
1271
1272 (** val destination_inv_rect_Type2 :
1273     var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
1274     (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
1275 let destination_inv_rect_Type2 x1 x2 hterm h1 h2 =
1276   let hcut = destination_rect_Type2 x1 x2 h1 h2 hterm in hcut __
1277
1278 (** val destination_inv_rect_Type1 :
1279     var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
1280     (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
1281 let destination_inv_rect_Type1 x1 x2 hterm h1 h2 =
1282   let hcut = destination_rect_Type1 x1 x2 h1 h2 hterm in hcut __
1283
1284 (** val destination_inv_rect_Type0 :
1285     var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
1286     (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
1287 let destination_inv_rect_Type0 x1 x2 hterm h1 h2 =
1288   let hcut = destination_rect_Type0 x1 x2 h1 h2 hterm in hcut __
1289
1290 (** val destination_discr :
1291     var_types -> AST.typ -> destination -> destination -> __ **)
1292 let destination_discr a1 a2 x y =
1293   Logic.eq_rect_Type2 x
1294     (match x with
1295      | IdDest a0 -> Obj.magic (fun _ dH -> dH __ __)
1296      | MemDest a0 -> Obj.magic (fun _ dH -> dH __)) y
1297
1298 (** val destination_jmdiscr :
1299     var_types -> AST.typ -> destination -> destination -> __ **)
1300 let destination_jmdiscr a1 a2 x y =
1301   Logic.eq_rect_Type2 x
1302     (match x with
1303      | IdDest a0 -> Obj.magic (fun _ dH -> dH __ __)
1304      | MemDest a0 -> Obj.magic (fun _ dH -> dH __)) y
1305
1306 (** val translate_dest :
1307     var_types -> Csyntax.expr -> destination Errors.res **)
1308 let translate_dest vars e1 = match e1 with
1309 | Csyntax.Expr (ed1, ty1) ->
1310   (match ed1 with
1311    | Csyntax.Econst_int (x, x0) ->
1312      Obj.magic
1313        (Monad.m_bind0 (Monad.max_def Errors.res0)
1314          (Obj.magic (translate_addr vars e1)) (fun e1' ->
1315          Obj.magic (Errors.OK (MemDest e1'))))
1316    | Csyntax.Evar id ->
1317      Errors.bind2_eq (lookup' vars id) (fun c t _ ->
1318        (match c with
1319         | Global r ->
1320           (fun _ -> Errors.OK (MemDest (Cminor_syntax.Cst (AST.ASTptr,
1321             (FrontEndOps.Oaddrsymbol (id, Nat.O))))))
1322         | Stack n ->
1323           (fun _ -> Errors.OK (MemDest (Cminor_syntax.Cst (AST.ASTptr,
1324             (FrontEndOps.Oaddrstack n)))))
1325         | Local ->
1326           (fun _ ->
1327             match AST.typ_eq (Csyntax.typ_of_type ty1)
1328                     (Csyntax.typ_of_type t) with
1329             | Types.Inl _ -> Errors.OK (IdDest id)
1330             | Types.Inr _ ->
1331               Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) __)
1332    | Csyntax.Ederef x ->
1333      Obj.magic
1334        (Monad.m_bind0 (Monad.max_def Errors.res0)
1335          (Obj.magic (translate_addr vars e1)) (fun e1' ->
1336          Obj.magic (Errors.OK (MemDest e1'))))
1337    | Csyntax.Eaddrof x ->
1338      Obj.magic
1339        (Monad.m_bind0 (Monad.max_def Errors.res0)
1340          (Obj.magic (translate_addr vars e1)) (fun e1' ->
1341          Obj.magic (Errors.OK (MemDest e1'))))
1342    | Csyntax.Eunop (x, x0) ->
1343      Obj.magic
1344        (Monad.m_bind0 (Monad.max_def Errors.res0)
1345          (Obj.magic (translate_addr vars e1)) (fun e1' ->
1346          Obj.magic (Errors.OK (MemDest e1'))))
1347    | Csyntax.Ebinop (x, x0, x1) ->
1348      Obj.magic
1349        (Monad.m_bind0 (Monad.max_def Errors.res0)
1350          (Obj.magic (translate_addr vars e1)) (fun e1' ->
1351          Obj.magic (Errors.OK (MemDest e1'))))
1352    | Csyntax.Ecast (x, x0) ->
1353      Obj.magic
1354        (Monad.m_bind0 (Monad.max_def Errors.res0)
1355          (Obj.magic (translate_addr vars e1)) (fun e1' ->
1356          Obj.magic (Errors.OK (MemDest e1'))))
1357    | Csyntax.Econdition (x, x0, x1) ->
1358      Obj.magic
1359        (Monad.m_bind0 (Monad.max_def Errors.res0)
1360          (Obj.magic (translate_addr vars e1)) (fun e1' ->
1361          Obj.magic (Errors.OK (MemDest e1'))))
1362    | Csyntax.Eandbool (x, x0) ->
1363      Obj.magic
1364        (Monad.m_bind0 (Monad.max_def Errors.res0)
1365          (Obj.magic (translate_addr vars e1)) (fun e1' ->
1366          Obj.magic (Errors.OK (MemDest e1'))))
1367    | Csyntax.Eorbool (x, x0) ->
1368      Obj.magic
1369        (Monad.m_bind0 (Monad.max_def Errors.res0)
1370          (Obj.magic (translate_addr vars e1)) (fun e1' ->
1371          Obj.magic (Errors.OK (MemDest e1'))))
1372    | Csyntax.Esizeof x ->
1373      Obj.magic
1374        (Monad.m_bind0 (Monad.max_def Errors.res0)
1375          (Obj.magic (translate_addr vars e1)) (fun e1' ->
1376          Obj.magic (Errors.OK (MemDest e1'))))
1377    | Csyntax.Efield (x, x0) ->
1378      Obj.magic
1379        (Monad.m_bind0 (Monad.max_def Errors.res0)
1380          (Obj.magic (translate_addr vars e1)) (fun e1' ->
1381          Obj.magic (Errors.OK (MemDest e1'))))
1382    | Csyntax.Ecost (x, x0) ->
1383      Obj.magic
1384        (Monad.m_bind0 (Monad.max_def Errors.res0)
1385          (Obj.magic (translate_addr vars e1)) (fun e1' ->
1386          Obj.magic (Errors.OK (MemDest e1')))))
1387
1388 type lenv = PreIdentifiers.identifier Identifiers.identifier_map
1389
1390 (** val lookup_label :
1391     lenv -> PreIdentifiers.identifier -> PreIdentifiers.identifier Errors.res **)
1392 let lookup_label lbls l =
1393   Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingLabel),
1394     (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, l)), List.Nil))))
1395     (Identifiers.lookup PreIdentifiers.SymbolTag lbls l)
1396
1397 type labgen = { labuniverse : Identifiers.universe;
1398                 label_genlist : PreIdentifiers.identifier List.list }
1399
1400 (** val labgen_rect_Type4 :
1401     (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1402     'a1) -> labgen -> 'a1 **)
1403 let rec labgen_rect_Type4 h_mk_labgen x_14584 =
1404   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1405     x_14584
1406   in
1407   h_mk_labgen labuniverse0 label_genlist0 __
1408
1409 (** val labgen_rect_Type5 :
1410     (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1411     'a1) -> labgen -> 'a1 **)
1412 let rec labgen_rect_Type5 h_mk_labgen x_14586 =
1413   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1414     x_14586
1415   in
1416   h_mk_labgen labuniverse0 label_genlist0 __
1417
1418 (** val labgen_rect_Type3 :
1419     (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1420     'a1) -> labgen -> 'a1 **)
1421 let rec labgen_rect_Type3 h_mk_labgen x_14588 =
1422   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1423     x_14588
1424   in
1425   h_mk_labgen labuniverse0 label_genlist0 __
1426
1427 (** val labgen_rect_Type2 :
1428     (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1429     'a1) -> labgen -> 'a1 **)
1430 let rec labgen_rect_Type2 h_mk_labgen x_14590 =
1431   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1432     x_14590
1433   in
1434   h_mk_labgen labuniverse0 label_genlist0 __
1435
1436 (** val labgen_rect_Type1 :
1437     (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1438     'a1) -> labgen -> 'a1 **)
1439 let rec labgen_rect_Type1 h_mk_labgen x_14592 =
1440   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1441     x_14592
1442   in
1443   h_mk_labgen labuniverse0 label_genlist0 __
1444
1445 (** val labgen_rect_Type0 :
1446     (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1447     'a1) -> labgen -> 'a1 **)
1448 let rec labgen_rect_Type0 h_mk_labgen x_14594 =
1449   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1450     x_14594
1451   in
1452   h_mk_labgen labuniverse0 label_genlist0 __
1453
1454 (** val labuniverse : labgen -> Identifiers.universe **)
1455 let rec labuniverse xxx =
1456   xxx.labuniverse
1457
1458 (** val label_genlist : labgen -> PreIdentifiers.identifier List.list **)
1459 let rec label_genlist xxx =
1460   xxx.label_genlist
1461
1462 (** val labgen_inv_rect_Type4 :
1463     labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
1464     __ -> __ -> 'a1) -> 'a1 **)
1465 let labgen_inv_rect_Type4 hterm h1 =
1466   let hcut = labgen_rect_Type4 h1 hterm in hcut __
1467
1468 (** val labgen_inv_rect_Type3 :
1469     labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
1470     __ -> __ -> 'a1) -> 'a1 **)
1471 let labgen_inv_rect_Type3 hterm h1 =
1472   let hcut = labgen_rect_Type3 h1 hterm in hcut __
1473
1474 (** val labgen_inv_rect_Type2 :
1475     labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
1476     __ -> __ -> 'a1) -> 'a1 **)
1477 let labgen_inv_rect_Type2 hterm h1 =
1478   let hcut = labgen_rect_Type2 h1 hterm in hcut __
1479
1480 (** val labgen_inv_rect_Type1 :
1481     labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
1482     __ -> __ -> 'a1) -> 'a1 **)
1483 let labgen_inv_rect_Type1 hterm h1 =
1484   let hcut = labgen_rect_Type1 h1 hterm in hcut __
1485
1486 (** val labgen_inv_rect_Type0 :
1487     labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
1488     __ -> __ -> 'a1) -> 'a1 **)
1489 let labgen_inv_rect_Type0 hterm h1 =
1490   let hcut = labgen_rect_Type0 h1 hterm in hcut __
1491
1492 (** val labgen_discr : labgen -> labgen -> __ **)
1493 let labgen_discr x y =
1494   Logic.eq_rect_Type2 x
1495     (let { labuniverse = a0; label_genlist = a1 } = x in
1496     Obj.magic (fun _ dH -> dH __ __ __)) y
1497
1498 (** val labgen_jmdiscr : labgen -> labgen -> __ **)
1499 let labgen_jmdiscr x y =
1500   Logic.eq_rect_Type2 x
1501     (let { labuniverse = a0; label_genlist = a1 } = x in
1502     Obj.magic (fun _ dH -> dH __ __ __)) y
1503
1504 (** val generate_fresh_label :
1505     labgen -> (PreIdentifiers.identifier, labgen) Types.prod Types.sig0 **)
1506 let generate_fresh_label ul =
1507   (let { Types.fst = tmp; Types.snd = u } =
1508      Identifiers.fresh PreIdentifiers.Label ul.labuniverse
1509    in
1510   (fun _ -> { Types.fst = tmp; Types.snd = { labuniverse = u; label_genlist =
1511   (List.Cons (tmp, ul.label_genlist)) } })) __
1512
1513 (** val labels_defined : Csyntax.statement -> AST.ident List.list **)
1514 let rec labels_defined = function
1515 | Csyntax.Sskip -> List.Nil
1516 | Csyntax.Sassign (x, x0) -> List.Nil
1517 | Csyntax.Scall (x, x0, x1) -> List.Nil
1518 | Csyntax.Ssequence (s1, s2) ->
1519   List.append (labels_defined s1) (labels_defined s2)
1520 | Csyntax.Sifthenelse (x, s1, s2) ->
1521   List.append (labels_defined s1) (labels_defined s2)
1522 | Csyntax.Swhile (x, s0) -> labels_defined s0
1523 | Csyntax.Sdowhile (x, s0) -> labels_defined s0
1524 | Csyntax.Sfor (s1, x, s2, s3) ->
1525   List.append (labels_defined s1)
1526     (List.append (labels_defined s2) (labels_defined s3))
1527 | Csyntax.Sbreak -> List.Nil
1528 | Csyntax.Scontinue -> List.Nil
1529 | Csyntax.Sreturn x -> List.Nil
1530 | Csyntax.Sswitch (x, ls) -> labels_defined_switch ls
1531 | Csyntax.Slabel (l, s0) -> List.Cons (l, (labels_defined s0))
1532 | Csyntax.Sgoto x -> List.Nil
1533 | Csyntax.Scost (x, s0) -> labels_defined s0
1534 (** val labels_defined_switch :
1535     Csyntax.labeled_statements -> AST.ident List.list **)
1536 and labels_defined_switch = function
1537 | Csyntax.LSdefault s -> labels_defined s
1538 | Csyntax.LScase (x, x0, s, ls0) ->
1539   List.append (labels_defined s) (labels_defined_switch ls0)
1540
1541 (** val m_option_map :
1542     ('a1 -> 'a2 Errors.res) -> 'a1 Types.option -> 'a2 Types.option
1543     Errors.res **)
1544 let m_option_map f = function
1545 | Types.None -> Errors.OK Types.None
1546 | Types.Some a ->
1547   Obj.magic
1548     (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f a) (fun b ->
1549       Obj.magic (Errors.OK (Types.Some b))))
1550
1551 (** val translate_expr_sigma :
1552     var_types -> Csyntax.expr -> (AST.typ, Cminor_syntax.expr) Types.dPair
1553     Types.sig0 Errors.res **)
1554 let translate_expr_sigma v e =
1555   Obj.magic
1556     (Monad.m_bind0 (Monad.max_def Errors.res0)
1557       (Obj.magic (translate_expr v e)) (fun e' ->
1558       Obj.magic (Errors.OK { Types.dpi1 =
1559         (Csyntax.typ_of_type (Csyntax.typeof e)); Types.dpi2 =
1560         (Types.pi1 e') })))
1561
1562 (** val add_tmps :
1563     var_types -> (AST.ident, Csyntax.type0) Types.prod List.list -> var_types **)
1564 let add_tmps vs tmpenv =
1565   List.foldr (fun idty vs0 ->
1566     Identifiers.add PreIdentifiers.SymbolTag vs0 idty.Types.fst { Types.fst =
1567       Local; Types.snd = idty.Types.snd }) vs tmpenv
1568
1569 type tmpgen = { tmp_universe : Identifiers.universe;
1570                 tmp_env : (AST.ident, Csyntax.type0) Types.prod List.list }
1571
1572 (** val tmpgen_rect_Type4 :
1573     var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1574     Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
1575 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14610 =
1576   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14610 in
1577   h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1578
1579 (** val tmpgen_rect_Type5 :
1580     var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1581     Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
1582 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14612 =
1583   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14612 in
1584   h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1585
1586 (** val tmpgen_rect_Type3 :
1587     var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1588     Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
1589 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14614 =
1590   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14614 in
1591   h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1592
1593 (** val tmpgen_rect_Type2 :
1594     var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1595     Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
1596 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14616 =
1597   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14616 in
1598   h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1599
1600 (** val tmpgen_rect_Type1 :
1601     var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1602     Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
1603 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14618 =
1604   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14618 in
1605   h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1606
1607 (** val tmpgen_rect_Type0 :
1608     var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1609     Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
1610 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14620 =
1611   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14620 in
1612   h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1613
1614 (** val tmp_universe : var_types -> tmpgen -> Identifiers.universe **)
1615 let rec tmp_universe vars xxx =
1616   xxx.tmp_universe
1617
1618 (** val tmp_env :
1619     var_types -> tmpgen -> (AST.ident, Csyntax.type0) Types.prod List.list **)
1620 let rec tmp_env vars xxx =
1621   xxx.tmp_env
1622
1623 (** val tmpgen_inv_rect_Type4 :
1624     var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
1625     Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1626 let tmpgen_inv_rect_Type4 x1 hterm h1 =
1627   let hcut = tmpgen_rect_Type4 x1 h1 hterm in hcut __
1628
1629 (** val tmpgen_inv_rect_Type3 :
1630     var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
1631     Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1632 let tmpgen_inv_rect_Type3 x1 hterm h1 =
1633   let hcut = tmpgen_rect_Type3 x1 h1 hterm in hcut __
1634
1635 (** val tmpgen_inv_rect_Type2 :
1636     var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
1637     Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1638 let tmpgen_inv_rect_Type2 x1 hterm h1 =
1639   let hcut = tmpgen_rect_Type2 x1 h1 hterm in hcut __
1640
1641 (** val tmpgen_inv_rect_Type1 :
1642     var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
1643     Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1644 let tmpgen_inv_rect_Type1 x1 hterm h1 =
1645   let hcut = tmpgen_rect_Type1 x1 h1 hterm in hcut __
1646
1647 (** val tmpgen_inv_rect_Type0 :
1648     var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
1649     Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1650 let tmpgen_inv_rect_Type0 x1 hterm h1 =
1651   let hcut = tmpgen_rect_Type0 x1 h1 hterm in hcut __
1652
1653 (** val tmpgen_discr : var_types -> tmpgen -> tmpgen -> __ **)
1654 let tmpgen_discr a1 x y =
1655   Logic.eq_rect_Type2 x
1656     (let { tmp_universe = a0; tmp_env = a10 } = x in
1657     Obj.magic (fun _ dH -> dH __ __ __ __)) y
1658
1659 (** val tmpgen_jmdiscr : var_types -> tmpgen -> tmpgen -> __ **)
1660 let tmpgen_jmdiscr a1 x y =
1661   Logic.eq_rect_Type2 x
1662     (let { tmp_universe = a0; tmp_env = a10 } = x in
1663     Obj.magic (fun _ dH -> dH __ __ __ __)) y
1664
1665 (** val alloc_tmp :
1666     var_types -> Csyntax.type0 -> tmpgen -> (AST.ident, tmpgen) Types.prod **)
1667 let alloc_tmp vars ty g =
1668   (let { Types.fst = tmp; Types.snd = u } =
1669      Identifiers.fresh PreIdentifiers.SymbolTag g.tmp_universe
1670    in
1671   (fun _ -> { Types.fst = tmp; Types.snd = { tmp_universe = u; tmp_env =
1672   (List.Cons ({ Types.fst = tmp; Types.snd = ty }, g.tmp_env)) } })) __
1673
1674 (** val mklabels :
1675     labgen -> ((PreIdentifiers.identifier, PreIdentifiers.identifier)
1676     Types.prod, labgen) Types.prod **)
1677 let rec mklabels ul =
1678   let res1 = generate_fresh_label ul in
1679   (let { Types.fst = entry_label; Types.snd = ul1 } = res1 in
1680   (fun _ ->
1681   let res2 = generate_fresh_label ul1 in
1682   (let { Types.fst = exit_label; Types.snd = ul2 } = res2 in
1683   (fun _ -> { Types.fst = { Types.fst = entry_label; Types.snd =
1684   exit_label }; Types.snd = ul2 })) __)) __
1685
1686 type convert_flag =
1687 | DoNotConvert
1688 | ConvertTo of PreIdentifiers.identifier * PreIdentifiers.identifier
1689
1690 (** val convert_flag_rect_Type4 :
1691     'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1692     convert_flag -> 'a1 **)
1693 let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function
1694 | DoNotConvert -> h_DoNotConvert
1695 | ConvertTo (x_14642, x_14641) -> h_ConvertTo x_14642 x_14641
1696
1697 (** val convert_flag_rect_Type5 :
1698     'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1699     convert_flag -> 'a1 **)
1700 let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function
1701 | DoNotConvert -> h_DoNotConvert
1702 | ConvertTo (x_14647, x_14646) -> h_ConvertTo x_14647 x_14646
1703
1704 (** val convert_flag_rect_Type3 :
1705     'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1706     convert_flag -> 'a1 **)
1707 let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function
1708 | DoNotConvert -> h_DoNotConvert
1709 | ConvertTo (x_14652, x_14651) -> h_ConvertTo x_14652 x_14651
1710
1711 (** val convert_flag_rect_Type2 :
1712     'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1713     convert_flag -> 'a1 **)
1714 let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function
1715 | DoNotConvert -> h_DoNotConvert
1716 | ConvertTo (x_14657, x_14656) -> h_ConvertTo x_14657 x_14656
1717
1718 (** val convert_flag_rect_Type1 :
1719     'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1720     convert_flag -> 'a1 **)
1721 let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function
1722 | DoNotConvert -> h_DoNotConvert
1723 | ConvertTo (x_14662, x_14661) -> h_ConvertTo x_14662 x_14661
1724
1725 (** val convert_flag_rect_Type0 :
1726     'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1727     convert_flag -> 'a1 **)
1728 let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function
1729 | DoNotConvert -> h_DoNotConvert
1730 | ConvertTo (x_14667, x_14666) -> h_ConvertTo x_14667 x_14666
1731
1732 (** val convert_flag_inv_rect_Type4 :
1733     convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
1734     PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
1735 let convert_flag_inv_rect_Type4 hterm h1 h2 =
1736   let hcut = convert_flag_rect_Type4 h1 h2 hterm in hcut __
1737
1738 (** val convert_flag_inv_rect_Type3 :
1739     convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
1740     PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
1741 let convert_flag_inv_rect_Type3 hterm h1 h2 =
1742   let hcut = convert_flag_rect_Type3 h1 h2 hterm in hcut __
1743
1744 (** val convert_flag_inv_rect_Type2 :
1745     convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
1746     PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
1747 let convert_flag_inv_rect_Type2 hterm h1 h2 =
1748   let hcut = convert_flag_rect_Type2 h1 h2 hterm in hcut __
1749
1750 (** val convert_flag_inv_rect_Type1 :
1751     convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
1752     PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
1753 let convert_flag_inv_rect_Type1 hterm h1 h2 =
1754   let hcut = convert_flag_rect_Type1 h1 h2 hterm in hcut __
1755
1756 (** val convert_flag_inv_rect_Type0 :
1757     convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
1758     PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
1759 let convert_flag_inv_rect_Type0 hterm h1 h2 =
1760   let hcut = convert_flag_rect_Type0 h1 h2 hterm in hcut __
1761
1762 (** val convert_flag_discr : convert_flag -> convert_flag -> __ **)
1763 let convert_flag_discr x y =
1764   Logic.eq_rect_Type2 x
1765     (match x with
1766      | DoNotConvert -> Obj.magic (fun _ dH -> dH)
1767      | ConvertTo (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
1768
1769 (** val convert_flag_jmdiscr : convert_flag -> convert_flag -> __ **)
1770 let convert_flag_jmdiscr x y =
1771   Logic.eq_rect_Type2 x
1772     (match x with
1773      | DoNotConvert -> Obj.magic (fun _ dH -> dH)
1774      | ConvertTo (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
1775
1776 (** val labels_of_flag :
1777     convert_flag -> PreIdentifiers.identifier List.list **)
1778 let rec labels_of_flag = function
1779 | DoNotConvert -> List.Nil
1780 | ConvertTo (continue, break) ->
1781   List.Cons (continue, (List.Cons (break, List.Nil)))
1782
1783 (** val translate_statement :
1784     var_types -> tmpgen -> labgen -> lenv -> convert_flag -> AST.typ
1785     Types.option -> Csyntax.statement -> ((tmpgen, labgen) Types.prod,
1786     Cminor_syntax.stmt) Types.prod Types.sig0 Errors.res **)
1787 let rec translate_statement vars uv ul lbls flag rettyp = function
1788 | Csyntax.Sskip ->
1789   Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; Types.snd =
1790     Cminor_syntax.St_skip }
1791 | Csyntax.Sassign (e1, e2) ->
1792   Obj.magic
1793     (Monad.m_bind0 (Monad.max_def Errors.res0)
1794       (Obj.magic (translate_expr vars e2)) (fun e2' ->
1795       Monad.m_bind0 (Monad.max_def Errors.res0)
1796         (Obj.magic (translate_dest vars e1)) (fun dest ->
1797         match dest with
1798         | IdDest id ->
1799           Monad.m_bind0 (Monad.max_def Errors.res0)
1800             (Obj.magic
1801               (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e2))
1802                 (Csyntax.typ_of_type (Csyntax.typeof e1)) e2')) (fun e2'0 ->
1803             Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd =
1804               ul }; Types.snd = (Cminor_syntax.St_assign
1805               ((Csyntax.typ_of_type (Csyntax.typeof e1)), id,
1806               (Types.pi1 e2'0))) }))
1807         | MemDest e1' ->
1808           (match TypeComparison.type_eq_dec (Csyntax.typeof e1)
1809                    (Csyntax.typeof e2) with
1810            | Types.Inl _ ->
1811              Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd =
1812                ul }; Types.snd = (Cminor_syntax.St_store
1813                ((Csyntax.typ_of_type (Csyntax.typeof e2)), (Types.pi1 e1'),
1814                (Types.pi1 e2'))) })
1815            | Types.Inr _ ->
1816              Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))))
1817 | Csyntax.Scall (ret, ef, args) ->
1818   Obj.magic
1819     (Monad.m_bind0 (Monad.max_def Errors.res0)
1820       (Obj.magic (translate_expr vars ef)) (fun ef' ->
1821       Monad.m_bind0 (Monad.max_def Errors.res0)
1822         (Obj.magic
1823           (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof ef)) AST.ASTptr
1824             ef')) (fun ef'0 ->
1825         Monad.m_bind0 (Monad.max_def Errors.res0)
1826           (Errors.mmap_sigma (Obj.magic (translate_expr_sigma vars)) args)
1827           (fun args' ->
1828           match ret with
1829           | Types.None ->
1830             Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd =
1831               ul }; Types.snd = (Cminor_syntax.St_call (Types.None,
1832               (Types.pi1 ef'0), (Types.pi1 args'))) })
1833           | Types.Some e1 ->
1834             Monad.m_bind0 (Monad.max_def Errors.res0)
1835               (Obj.magic (translate_dest vars e1)) (fun dest ->
1836               match dest with
1837               | IdDest id ->
1838                 Obj.magic (Errors.OK { Types.fst = { Types.fst = uv;
1839                   Types.snd = ul }; Types.snd = (Cminor_syntax.St_call
1840                   ((Types.Some { Types.fst = id; Types.snd =
1841                   (Csyntax.typ_of_type (Csyntax.typeof e1)) }),
1842                   (Types.pi1 ef'0), (Types.pi1 args'))) })
1843               | MemDest e1' ->
1844                 (let { Types.fst = tmp; Types.snd = uv1 } =
1845                    alloc_tmp vars (Csyntax.typeof e1) uv
1846                  in
1847                 (fun _ ->
1848                 (let { Types.fst = tmp2; Types.snd = uv2 } =
1849                    alloc_tmp vars (Csyntax.Tpointer (Csyntax.typeof e1)) uv1
1850                  in
1851                 (fun _ ->
1852                 Obj.magic (Errors.OK { Types.fst = { Types.fst = uv2;
1853                   Types.snd = ul }; Types.snd = (Cminor_syntax.St_seq
1854                   ((Cminor_syntax.St_assign (AST.ASTptr, tmp2,
1855                   (Types.pi1 e1'))), (Cminor_syntax.St_seq
1856                   ((Cminor_syntax.St_call ((Types.Some { Types.fst = tmp;
1857                   Types.snd = (Csyntax.typ_of_type (Csyntax.typeof e1)) }),
1858                   (Types.pi1 ef'0), (Types.pi1 args'))),
1859                   (Cminor_syntax.St_store
1860                   ((Csyntax.typ_of_type (Csyntax.typeof e1)),
1861                   (Cminor_syntax.Id (AST.ASTptr, tmp2)), (Cminor_syntax.Id
1862                   ((Csyntax.typ_of_type (Csyntax.typeof e1)), tmp)))))))) })))
1863                   __)) __)))))
1864 | Csyntax.Ssequence (s1, s2) ->
1865   Obj.magic
1866     (Monad.m_sigbind2 (Monad.max_def Errors.res0)
1867       (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1))
1868       (fun fgens1 s1' _ ->
1869       Monad.m_sigbind2 (Monad.max_def Errors.res0)
1870         (Obj.magic
1871           (translate_statement vars fgens1.Types.fst fgens1.Types.snd lbls
1872             flag rettyp s2)) (fun fgens2 s2' _ ->
1873         Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd =
1874           (Cminor_syntax.St_seq (s1', s2')) }))))
1875 | Csyntax.Sifthenelse (e1, s1, s2) ->
1876   Obj.magic
1877     (Monad.m_bind0 (Monad.max_def Errors.res0)
1878       (Obj.magic (translate_expr vars e1)) (fun e1' ->
1879       (match Csyntax.typ_of_type (Csyntax.typeof e1) with
1880        | AST.ASTint (x, x0) ->
1881          (fun e1'0 ->
1882            Monad.m_sigbind2 (Monad.max_def Errors.res0)
1883              (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1))
1884              (fun fgens1 s1' _ ->
1885              Monad.m_sigbind2 (Monad.max_def Errors.res0)
1886                (Obj.magic
1887                  (translate_statement vars fgens1.Types.fst fgens1.Types.snd
1888                    lbls flag rettyp s2)) (fun fgens2 s2' _ ->
1889                Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd =
1890                  (Cminor_syntax.St_ifthenelse (x, x0, (Types.pi1 e1'0), s1',
1891                  s2')) }))))
1892        | AST.ASTptr ->
1893          (fun x ->
1894            Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
1895         e1'))
1896 | Csyntax.Swhile (e1, s1) ->
1897   Obj.magic
1898     (Monad.m_bind0 (Monad.max_def Errors.res0)
1899       (Obj.magic (translate_expr vars e1)) (fun e1' ->
1900       (match Csyntax.typ_of_type (Csyntax.typeof e1) with
1901        | AST.ASTint (x, x0) ->
1902          (fun e1'0 ->
1903            (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in
1904            (fun _ ->
1905            (let { Types.fst = entry; Types.snd = exit } = labels in
1906            (fun _ ->
1907            Monad.m_sigbind2 (Monad.max_def Errors.res0)
1908              (Obj.magic
1909                (translate_statement vars uv ul1 lbls (ConvertTo (entry,
1910                  exit)) rettyp s1)) (fun fgens2 s1' _ ->
1911              let converted_loop = Cminor_syntax.St_label (entry,
1912                (Cminor_syntax.St_seq ((Cminor_syntax.St_ifthenelse (x, x0,
1913                (Types.pi1 e1'0), (Cminor_syntax.St_seq (s1',
1914                (Cminor_syntax.St_goto entry))), Cminor_syntax.St_skip)),
1915                (Cminor_syntax.St_label (exit, Cminor_syntax.St_skip)))))
1916              in
1917              Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd =
1918                converted_loop })))) __)) __)
1919        | AST.ASTptr ->
1920          (fun x ->
1921            Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
1922         e1'))
1923 | Csyntax.Sdowhile (e1, s1) ->
1924   Obj.magic
1925     (Monad.m_bind0 (Monad.max_def Errors.res0)
1926       (Obj.magic (translate_expr vars e1)) (fun e1' ->
1927       (match Csyntax.typ_of_type (Csyntax.typeof e1) with
1928        | AST.ASTint (x, x0) ->
1929          (fun e1'0 ->
1930            (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in
1931            (fun _ ->
1932            (let { Types.fst = condexpr; Types.snd = exit } = labels in
1933            (fun _ ->
1934            let { Types.fst = body; Types.snd = ul2 } =
1935              Types.pi1 (generate_fresh_label ul1)
1936            in
1937            Monad.m_sigbind2 (Monad.max_def Errors.res0)
1938              (Obj.magic
1939                (translate_statement vars uv ul2 lbls (ConvertTo (condexpr,
1940                  exit)) rettyp s1)) (fun fgens2 s1' _ ->
1941              let converted_loop = Cminor_syntax.St_seq ((Cminor_syntax.St_seq
1942                ((Cminor_syntax.St_goto body), (Cminor_syntax.St_label
1943                (condexpr, (Cminor_syntax.St_ifthenelse (x, x0,
1944                (Types.pi1 e1'0), (Cminor_syntax.St_label (body,
1945                (Cminor_syntax.St_seq (s1', (Cminor_syntax.St_goto
1946                condexpr))))), Cminor_syntax.St_skip)))))),
1947                (Cminor_syntax.St_label (exit, Cminor_syntax.St_skip)))
1948              in
1949              Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd =
1950                converted_loop })))) __)) __)
1951        | AST.ASTptr ->
1952          (fun x ->
1953            Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
1954         e1'))
1955 | Csyntax.Sfor (s1, e1, s2, s3) ->
1956   Obj.magic
1957     (Monad.m_bind0 (Monad.max_def Errors.res0)
1958       (Obj.magic (translate_expr vars e1)) (fun e1' ->
1959       (match Csyntax.typ_of_type (Csyntax.typeof e1) with
1960        | AST.ASTint (x, x0) ->
1961          (fun e1'0 ->
1962            (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in
1963            (fun _ ->
1964            (let { Types.fst = continue; Types.snd = exit } = labels in
1965            (fun _ ->
1966            let { Types.fst = entry; Types.snd = ul2 } =
1967              Types.pi1 (generate_fresh_label ul1)
1968            in
1969            Monad.m_sigbind2 (Monad.max_def Errors.res0)
1970              (Obj.magic
1971                (translate_statement vars uv ul2 lbls flag rettyp s1))
1972              (fun fgens2 s1' _ ->
1973              Monad.m_sigbind2 (Monad.max_def Errors.res0)
1974                (Obj.magic
1975                  (translate_statement vars fgens2.Types.fst fgens2.Types.snd
1976                    lbls flag rettyp s2)) (fun fgens3 s2' _ ->
1977                Monad.m_sigbind2 (Monad.max_def Errors.res0)
1978                  (Obj.magic
1979                    (translate_statement vars fgens3.Types.fst
1980                      fgens3.Types.snd lbls (ConvertTo (continue, exit))
1981                      rettyp s3)) (fun fgens4 s3' _ ->
1982                  let converted_loop = Cminor_syntax.St_seq (s1',
1983                    (Cminor_syntax.St_label (entry, (Cminor_syntax.St_seq
1984                    ((Cminor_syntax.St_ifthenelse (x, x0, (Types.pi1 e1'0),
1985                    (Cminor_syntax.St_seq (s3', (Cminor_syntax.St_label
1986                    (continue, (Cminor_syntax.St_seq (s2',
1987                    (Cminor_syntax.St_goto entry))))))),
1988                    Cminor_syntax.St_skip)), (Cminor_syntax.St_label (exit,
1989                    Cminor_syntax.St_skip)))))))
1990                  in
1991                  Obj.magic (Errors.OK { Types.fst = fgens4; Types.snd =
1992                    converted_loop })))))) __)) __)
1993        | AST.ASTptr ->
1994          (fun x ->
1995            Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
1996         e1'))
1997 | Csyntax.Sbreak ->
1998   (match flag with
1999    | DoNotConvert -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.FIXME))
2000    | ConvertTo (continue_label, break_label) ->
2001      (fun _ -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul };
2002        Types.snd = (Cminor_syntax.St_goto break_label) })) __
2003 | Csyntax.Scontinue ->
2004   (match flag with
2005    | DoNotConvert -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.FIXME))
2006    | ConvertTo (continue_label, break_label) ->
2007      (fun _ -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul };
2008        Types.snd = (Cminor_syntax.St_goto continue_label) })) __
2009 | Csyntax.Sreturn ret ->
2010   (match ret with
2011    | Types.None ->
2012      (match rettyp with
2013       | Types.None ->
2014         Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul };
2015           Types.snd = (Cminor_syntax.St_return Types.None) }
2016       | Types.Some x ->
2017         Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))
2018    | Types.Some e1 ->
2019      (match rettyp with
2020       | Types.None -> Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
2021       | Types.Some rty ->
2022         Obj.magic
2023           (Monad.m_bind0 (Monad.max_def Errors.res0)
2024             (Obj.magic (translate_expr vars e1)) (fun e1' ->
2025             Monad.m_bind0 (Monad.max_def Errors.res0)
2026               (Obj.magic
2027                 (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e1)) rty
2028                   e1')) (fun e1'0 ->
2029               Obj.magic (Errors.OK { Types.fst = { Types.fst = uv;
2030                 Types.snd = ul }; Types.snd = (Cminor_syntax.St_return
2031                 (Types.Some { Types.dpi1 = rty; Types.dpi2 =
2032                 (Types.pi1 e1'0) })) }))))))
2033 | Csyntax.Sswitch (e1, ls) -> Errors.Error (Errors.msg ErrorMessages.FIXME)
2034 | Csyntax.Slabel (l, s1) ->
2035   Errors.bind_eq (lookup_label lbls l) (fun l' _ ->
2036     Obj.magic
2037       (Monad.m_sigbind2 (Monad.max_def Errors.res0)
2038         (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1))
2039         (fun fgens1 s1' _ ->
2040         Obj.magic (Errors.OK { Types.fst = fgens1; Types.snd =
2041           (Cminor_syntax.St_label (l', s1')) }))))
2042 | Csyntax.Sgoto l ->
2043   Errors.bind_eq (lookup_label lbls l) (fun l' _ -> Errors.OK { Types.fst =
2044     { Types.fst = uv; Types.snd = ul }; Types.snd = (Cminor_syntax.St_goto
2045     l') })
2046 | Csyntax.Scost (l, s1) ->
2047   Obj.magic
2048     (Monad.m_sigbind2 (Monad.max_def Errors.res0)
2049       (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1))
2050       (fun fgens1 s1' _ ->
2051       Obj.magic (Errors.OK { Types.fst = fgens1; Types.snd =
2052         (Cminor_syntax.St_cost (l, s1')) })))
2053
2054 (** val alloc_params_main :
2055     var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag ->
2056     AST.typ Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list
2057     -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod
2058     Types.sig0 -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt)
2059     Types.prod Types.sig0 Errors.res **)
2060 let alloc_params_main vars lbls statement uv ul rettyp params s =
2061   Util.foldl (fun su it ->
2062     let { Types.fst = id; Types.snd = ty } = it in
2063     Obj.magic
2064       (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
2065         (fun eta2378 ->
2066         let result = eta2378 in
2067         (let { Types.fst = fgens1; Types.snd = s0 } = result in
2068         (fun _ ->
2069         Obj.magic
2070           (Errors.bind2_eq (lookup' vars id) (fun t ty' _ ->
2071             (match t with
2072              | Global x ->
2073                (fun _ -> Errors.Error (List.Cons ((Errors.MSG
2074                  ErrorMessages.ParamGlobalMixup), (List.Cons ((Errors.CTX
2075                  (PreIdentifiers.SymbolTag, id)), List.Nil)))))
2076              | Stack n ->
2077                (fun _ -> Errors.OK { Types.fst = fgens1; Types.snd =
2078                  (Cminor_syntax.St_seq ((Cminor_syntax.St_store
2079                  ((Csyntax.typ_of_type ty'), (Cminor_syntax.Cst (AST.ASTptr,
2080                  (FrontEndOps.Oaddrstack n))), (Cminor_syntax.Id
2081                  ((Csyntax.typ_of_type ty'), id)))), s0)) })
2082              | Local -> (fun _ -> Errors.OK result)) __)))) __))) (Errors.OK
2083     s) params
2084
2085 (** val alloc_params :
2086     var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag ->
2087     AST.typ Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list
2088     -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod
2089     Types.sig0 -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt)
2090     Types.prod Types.sig0 Errors.res **)
2091 let alloc_params vars lbls statement uv ul rettyp params su =
2092   (let { Types.fst = tl; Types.snd = s0 } = Types.pi1 su in
2093   (match s0 with
2094    | Cminor_syntax.St_skip ->
2095      (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2096    | Cminor_syntax.St_assign (x, x0, x1) ->
2097      (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2098    | Cminor_syntax.St_store (x, x0, x1) ->
2099      (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2100    | Cminor_syntax.St_call (x, x0, x1) ->
2101      (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2102    | Cminor_syntax.St_seq (x, x0) ->
2103      (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2104    | Cminor_syntax.St_ifthenelse (x, x0, x1, x2, x3) ->
2105      (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2106    | Cminor_syntax.St_return x ->
2107      (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2108    | Cminor_syntax.St_label (x, x0) ->
2109      (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2110    | Cminor_syntax.St_goto x ->
2111      (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2112    | Cminor_syntax.St_cost (cl, s') ->
2113      (fun _ ->
2114        Obj.magic
2115          (Monad.m_bind0 (Monad.max_def Errors.res0)
2116            (Obj.magic
2117              (alloc_params_main vars lbls statement uv ul rettyp params
2118                { Types.fst = tl; Types.snd = s' })) (fun tls ->
2119            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
2120              (Types.pi1 tls).Types.fst; Types.snd = (Cminor_syntax.St_cost
2121              (cl, (Types.pi1 tls).Types.snd)) }))))) __
2122
2123 (** val populate_lenv :
2124     AST.ident List.list -> labgen -> lenv -> (lenv Types.sig0, labgen)
2125     Types.prod Errors.res **)
2126 let rec populate_lenv ls ul lbls =
2127   match ls with
2128   | List.Nil -> Errors.OK { Types.fst = lbls; Types.snd = ul }
2129   | List.Cons (l, t) ->
2130     (match lookup_label lbls l with
2131      | Errors.OK x ->
2132        (fun _ -> Errors.Error (Errors.msg ErrorMessages.DuplicateLabel))
2133      | Errors.Error x ->
2134        (fun _ ->
2135          let ret = generate_fresh_label ul in
2136          Obj.magic
2137            (Monad.m_bind2 (Monad.max_def Errors.res0)
2138              (Obj.magic
2139                (populate_lenv t ret.Types.snd
2140                  (Identifiers.add PreIdentifiers.SymbolTag lbls l
2141                    ret.Types.fst))) (fun packed_lbls ul1 ->
2142              let lbls' = packed_lbls in
2143              Obj.magic (Errors.OK { Types.fst = lbls'; Types.snd = ul1 })))))
2144       __
2145
2146 (** val build_label_env :
2147     Csyntax.statement -> (lenv Types.sig0, labgen) Types.prod Errors.res **)
2148 let build_label_env body =
2149   let initial_labgen = { labuniverse =
2150     (Identifiers.new_universe PreIdentifiers.Label); label_genlist =
2151     List.Nil }
2152   in
2153   Obj.magic
2154     (Monad.m_bind2 (Monad.max_def Errors.res0)
2155       (Obj.magic
2156         (populate_lenv (labels_defined body) initial_labgen
2157           (Identifiers.empty_map PreIdentifiers.SymbolTag)))
2158       (fun label_map u ->
2159       let lbls = Types.pi1 label_map in
2160       Obj.magic (Errors.OK { Types.fst = lbls; Types.snd = u })))
2161
2162 (** val translate_function :
2163     Identifiers.universe -> ((AST.ident, AST.region) Types.prod,
2164     Csyntax.type0) Types.prod List.list -> Csyntax.function0 ->
2165     Cminor_syntax.internal_function Errors.res **)
2166 let translate_function tmpuniverse globals f =
2167   Obj.magic
2168     (Monad.m_bind2 (Monad.max_def Errors.res0)
2169       (Obj.magic (build_label_env f.Csyntax.fn_body)) (fun env_pack ul ->
2170       let lbls = env_pack in
2171       (let { Types.fst = vartypes; Types.snd = stacksize } =
2172          characterise_vars globals f
2173        in
2174       (fun _ ->
2175       let uv = { tmp_universe = tmpuniverse; tmp_env = List.Nil } in
2176       Monad.m_bind0 (Monad.max_def Errors.res0)
2177         (Obj.magic
2178           (translate_statement vartypes uv ul lbls DoNotConvert
2179             (Csyntax.opttyp_of_type f.Csyntax.fn_return) f.Csyntax.fn_body))
2180         (fun s0 ->
2181         Monad.m_sigbind2 (Monad.max_def Errors.res0)
2182           (Obj.magic
2183             (alloc_params vartypes lbls f.Csyntax.fn_body uv DoNotConvert
2184               (Csyntax.opttyp_of_type f.Csyntax.fn_return)
2185               f.Csyntax.fn_params s0)) (fun fgens s1 _ ->
2186           let params =
2187             List.map (fun v -> { Types.fst = v.Types.fst; Types.snd =
2188               (Csyntax.typ_of_type v.Types.snd) }) f.Csyntax.fn_params
2189           in
2190           let vars =
2191             List.map (fun v -> { Types.fst = v.Types.fst; Types.snd =
2192               (Csyntax.typ_of_type v.Types.snd) })
2193               (List.append fgens.Types.fst.tmp_env f.Csyntax.fn_vars)
2194           in
2195           Monad.m_bind0 (Monad.max_def Errors.res0)
2196             (Obj.magic
2197               (Identifiers.check_distinct_env PreIdentifiers.SymbolTag
2198                 (List.append params vars))) (fun _ ->
2199             Obj.magic (Errors.OK { Cminor_syntax.f_return =
2200               (Csyntax.opttyp_of_type f.Csyntax.fn_return);
2201               Cminor_syntax.f_params = params; Cminor_syntax.f_vars = vars;
2202               Cminor_syntax.f_stacksize = stacksize; Cminor_syntax.f_body =
2203               s1 })))))) __))
2204
2205 (** val translate_fundef :
2206     Identifiers.universe -> ((AST.ident, AST.region) Types.prod,
2207     Csyntax.type0) Types.prod List.list -> Csyntax.clight_fundef ->
2208     Cminor_syntax.internal_function AST.fundef Errors.res **)
2209 let translate_fundef tmpuniverse globals f =
2210   (match f with
2211    | Csyntax.CL_Internal fn ->
2212      (fun _ ->
2213        Obj.magic
2214          (Monad.m_bind0 (Monad.max_def Errors.res0)
2215            (Obj.magic (translate_function tmpuniverse globals fn))
2216            (fun fn' -> Obj.magic (Errors.OK (AST.Internal fn')))))
2217    | Csyntax.CL_External (fn, argtys, retty) ->
2218      (fun _ -> Errors.OK (AST.External { AST.ef_id = fn; AST.ef_sig =
2219        (Csyntax.signature_of_type argtys retty) }))) __
2220
2221 (** val map_partial_All :
2222     ('a1 -> __ -> 'a2 Errors.res) -> 'a1 List.list -> 'a2 List.list
2223     Errors.res **)
2224 let rec map_partial_All f l =
2225   (match l with
2226    | List.Nil -> (fun _ -> Errors.OK List.Nil)
2227    | List.Cons (hd, tl) ->
2228      (fun _ ->
2229        Obj.magic
2230          (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f hd __)
2231            (fun b_hd ->
2232            Monad.m_bind0 (Monad.max_def Errors.res0)
2233              (Obj.magic (map_partial_All f tl)) (fun b_tl ->
2234              Obj.magic (Errors.OK (List.Cons (b_hd, b_tl)))))))) __
2235
2236 (** val clight_to_cminor :
2237     Csyntax.clight_program -> Cminor_syntax.cminor_program Errors.res **)
2238 let clight_to_cminor p =
2239   let tmpuniverse = Fresh.universe_for_program p in
2240   let fun_globals =
2241     List.map (fun idf -> { Types.fst = { Types.fst = idf.Types.fst;
2242       Types.snd = AST.Code }; Types.snd =
2243       (Csyntax.type_of_fundef idf.Types.snd) }) p.AST.prog_funct
2244   in
2245   let var_globals =
2246     List.map (fun v -> { Types.fst = { Types.fst = v.Types.fst.Types.fst;
2247       Types.snd = v.Types.fst.Types.snd }; Types.snd =
2248       v.Types.snd.Types.snd }) p.AST.prog_vars
2249   in
2250   let globals = List.append fun_globals var_globals in
2251   Obj.magic
2252     (Monad.m_bind0 (Monad.max_def Errors.res0)
2253       (Obj.magic
2254         (map_partial_All (fun x _ ->
2255           Obj.magic
2256             (Monad.m_bind0 (Monad.max_def Errors.res0)
2257               (Obj.magic (translate_fundef tmpuniverse globals x.Types.snd))
2258               (fun f ->
2259               Obj.magic (Errors.OK { Types.fst = x.Types.fst; Types.snd =
2260                 f })))) p.AST.prog_funct)) (fun fns ->
2261       Obj.magic (Errors.OK { AST.prog_vars =
2262         (List.map (fun v -> { Types.fst = v.Types.fst; Types.snd =
2263           v.Types.snd.Types.fst }) p.AST.prog_vars); AST.prog_funct = fns;
2264         AST.prog_main = p.AST.prog_main })))
2265