open Preamble open CostLabel open Coqlib open Proper open PositiveMap open Deqsets open ErrorMessages open PreIdentifiers open Errors open Extralib open Lists open Positive open Identifiers open Exp open Arithmetic open Vector open Div_and_mod open Util open FoldStuff open BitVector open Jmeq open Russell open List open Setoids open Monad open Option open Extranat open Bool open Relations open Nat open Integers open Hints_declaration open Core_notation open Pts open Logic open Types open AST open Csyntax open TypeComparison open ClassifyOp open Fresh (** val gather_mem_vars_expr : Csyntax.expr -> Identifiers.identifier_set **) let rec gather_mem_vars_expr = function | Csyntax.Expr (ed, ty) -> (match ed with | Csyntax.Econst_int (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag | Csyntax.Evar x -> Identifiers.empty_set PreIdentifiers.SymbolTag | Csyntax.Ederef e1 -> gather_mem_vars_expr e1 | Csyntax.Eaddrof e1 -> gather_mem_vars_addr e1 | Csyntax.Eunop (x, e1) -> gather_mem_vars_expr e1 | Csyntax.Ebinop (x, e1, e2) -> Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) (gather_mem_vars_expr e2) | Csyntax.Ecast (x, e1) -> gather_mem_vars_expr e1 | Csyntax.Econdition (e1, e2, e3) -> Identifiers.union_set PreIdentifiers.SymbolTag (Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) (gather_mem_vars_expr e2)) (gather_mem_vars_expr e3) | Csyntax.Eandbool (e1, e2) -> Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) (gather_mem_vars_expr e2) | Csyntax.Eorbool (e1, e2) -> Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) (gather_mem_vars_expr e2) | Csyntax.Esizeof x -> Identifiers.empty_set PreIdentifiers.SymbolTag | Csyntax.Efield (e1, x) -> gather_mem_vars_expr e1 | Csyntax.Ecost (x, e1) -> gather_mem_vars_expr e1) (** val gather_mem_vars_addr : Csyntax.expr -> Identifiers.identifier_set **) and gather_mem_vars_addr = function | Csyntax.Expr (ed, ty) -> (match ed with | Csyntax.Econst_int (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag | Csyntax.Evar x -> Identifiers.add_set PreIdentifiers.SymbolTag (Identifiers.empty_set PreIdentifiers.SymbolTag) x | Csyntax.Ederef e1 -> gather_mem_vars_expr e1 | Csyntax.Eaddrof x -> Identifiers.empty_set PreIdentifiers.SymbolTag | Csyntax.Eunop (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag | Csyntax.Ebinop (x, x0, x1) -> Identifiers.empty_set PreIdentifiers.SymbolTag | Csyntax.Ecast (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag | Csyntax.Econdition (x, x0, x1) -> Identifiers.empty_set PreIdentifiers.SymbolTag | Csyntax.Eandbool (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag | Csyntax.Eorbool (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag | Csyntax.Esizeof x -> Identifiers.empty_set PreIdentifiers.SymbolTag | Csyntax.Efield (e1, x) -> gather_mem_vars_addr e1 | Csyntax.Ecost (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag) (** val gather_mem_vars_stmt : Csyntax.statement -> Identifiers.identifier_set **) let rec gather_mem_vars_stmt = function | Csyntax.Sskip -> Identifiers.empty_set PreIdentifiers.SymbolTag | Csyntax.Sassign (e1, e2) -> Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) (gather_mem_vars_expr e2) | Csyntax.Scall (oe1, e2, es) -> Identifiers.union_set PreIdentifiers.SymbolTag (Identifiers.union_set PreIdentifiers.SymbolTag (match oe1 with | Types.None -> Identifiers.empty_set PreIdentifiers.SymbolTag | Types.Some e1 -> gather_mem_vars_expr e1) (gather_mem_vars_expr e2)) (Util.foldl (fun s0 e -> Identifiers.union_set PreIdentifiers.SymbolTag s0 (gather_mem_vars_expr e)) (Identifiers.empty_set PreIdentifiers.SymbolTag) es) | Csyntax.Ssequence (s1, s2) -> Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_stmt s1) (gather_mem_vars_stmt s2) | Csyntax.Sifthenelse (e1, s1, s2) -> Identifiers.union_set PreIdentifiers.SymbolTag (Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) (gather_mem_vars_stmt s1)) (gather_mem_vars_stmt s2) | Csyntax.Swhile (e1, s1) -> Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) (gather_mem_vars_stmt s1) | Csyntax.Sdowhile (e1, s1) -> Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) (gather_mem_vars_stmt s1) | Csyntax.Sfor (s1, e1, s2, s3) -> Identifiers.union_set PreIdentifiers.SymbolTag (Identifiers.union_set PreIdentifiers.SymbolTag (Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_stmt s1) (gather_mem_vars_expr e1)) (gather_mem_vars_stmt s2)) (gather_mem_vars_stmt s3) | Csyntax.Sbreak -> Identifiers.empty_set PreIdentifiers.SymbolTag | Csyntax.Scontinue -> Identifiers.empty_set PreIdentifiers.SymbolTag | Csyntax.Sreturn oe1 -> (match oe1 with | Types.None -> Identifiers.empty_set PreIdentifiers.SymbolTag | Types.Some e1 -> gather_mem_vars_expr e1) | Csyntax.Sswitch (e1, ls) -> Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) (gather_mem_vars_ls ls) | Csyntax.Slabel (x, s1) -> gather_mem_vars_stmt s1 | Csyntax.Sgoto x -> Identifiers.empty_set PreIdentifiers.SymbolTag | Csyntax.Scost (x, s1) -> gather_mem_vars_stmt s1 (** val gather_mem_vars_ls : Csyntax.labeled_statements -> Identifiers.identifier_set **) and gather_mem_vars_ls = function | Csyntax.LSdefault s1 -> gather_mem_vars_stmt s1 | Csyntax.LScase (x, x0, s1, ls1) -> Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_stmt s1) (gather_mem_vars_ls ls1) type var_type = | Global of AST.region | Stack of Nat.nat | Local (** val var_type_rect_Type4 : (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **) let rec var_type_rect_Type4 h_Global h_Stack h_Local = function | Global x_13038 -> h_Global x_13038 | Stack x_13039 -> h_Stack x_13039 | Local -> h_Local (** val var_type_rect_Type5 : (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **) let rec var_type_rect_Type5 h_Global h_Stack h_Local = function | Global x_13044 -> h_Global x_13044 | Stack x_13045 -> h_Stack x_13045 | Local -> h_Local (** val var_type_rect_Type3 : (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **) let rec var_type_rect_Type3 h_Global h_Stack h_Local = function | Global x_13050 -> h_Global x_13050 | Stack x_13051 -> h_Stack x_13051 | Local -> h_Local (** val var_type_rect_Type2 : (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **) let rec var_type_rect_Type2 h_Global h_Stack h_Local = function | Global x_13056 -> h_Global x_13056 | Stack x_13057 -> h_Stack x_13057 | Local -> h_Local (** val var_type_rect_Type1 : (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **) let rec var_type_rect_Type1 h_Global h_Stack h_Local = function | Global x_13062 -> h_Global x_13062 | Stack x_13063 -> h_Stack x_13063 | Local -> h_Local (** val var_type_rect_Type0 : (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **) let rec var_type_rect_Type0 h_Global h_Stack h_Local = function | Global x_13068 -> h_Global x_13068 | Stack x_13069 -> h_Stack x_13069 | Local -> h_Local (** val var_type_inv_rect_Type4 : var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let var_type_inv_rect_Type4 hterm h1 h2 h3 = let hcut = var_type_rect_Type4 h1 h2 h3 hterm in hcut __ (** val var_type_inv_rect_Type3 : var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let var_type_inv_rect_Type3 hterm h1 h2 h3 = let hcut = var_type_rect_Type3 h1 h2 h3 hterm in hcut __ (** val var_type_inv_rect_Type2 : var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let var_type_inv_rect_Type2 hterm h1 h2 h3 = let hcut = var_type_rect_Type2 h1 h2 h3 hterm in hcut __ (** val var_type_inv_rect_Type1 : var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let var_type_inv_rect_Type1 hterm h1 h2 h3 = let hcut = var_type_rect_Type1 h1 h2 h3 hterm in hcut __ (** val var_type_inv_rect_Type0 : var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let var_type_inv_rect_Type0 hterm h1 h2 h3 = let hcut = var_type_rect_Type0 h1 h2 h3 hterm in hcut __ (** val var_type_discr : var_type -> var_type -> __ **) let var_type_discr x y = Logic.eq_rect_Type2 x (match x with | Global a0 -> Obj.magic (fun _ dH -> dH __) | Stack a0 -> Obj.magic (fun _ dH -> dH __) | Local -> Obj.magic (fun _ dH -> dH)) y (** val var_type_jmdiscr : var_type -> var_type -> __ **) let var_type_jmdiscr x y = Logic.eq_rect_Type2 x (match x with | Global a0 -> Obj.magic (fun _ dH -> dH __) | Stack a0 -> Obj.magic (fun _ dH -> dH __) | Local -> Obj.magic (fun _ dH -> dH)) y type var_types = (var_type, Csyntax.type0) Types.prod Identifiers.identifier_map (** val lookup' : var_types -> PreIdentifiers.identifier -> (var_type, Csyntax.type0) Types.prod Errors.res **) let lookup' vars id = Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.UndeclaredIdentifier), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil)))) (Identifiers.lookup PreIdentifiers.SymbolTag vars id) (** val always_alloc : Csyntax.type0 -> Bool.bool **) let always_alloc = function | Csyntax.Tvoid -> Bool.False | Csyntax.Tint (x, x0) -> Bool.False | Csyntax.Tpointer x -> Bool.False | Csyntax.Tarray (x, x0) -> Bool.True | Csyntax.Tfunction (x, x0) -> Bool.False | Csyntax.Tstruct (x, x0) -> Bool.True | Csyntax.Tunion (x, x0) -> Bool.True | Csyntax.Tcomp_ptr x -> Bool.False (** val characterise_vars : ((AST.ident, AST.region) Types.prod, Csyntax.type0) Types.prod List.list -> Csyntax.function0 -> (var_types, Nat.nat) Types.prod **) let characterise_vars globals f = let m = List.foldr (fun idrt m -> Identifiers.add PreIdentifiers.SymbolTag m idrt.Types.fst.Types.fst { Types.fst = (Global idrt.Types.fst.Types.snd); Types.snd = idrt.Types.snd }) (Identifiers.empty_map PreIdentifiers.SymbolTag) globals in let mem_vars = gather_mem_vars_stmt f.Csyntax.fn_body in let { Types.fst = m0; Types.snd = stacksize } = List.foldr (fun v ms -> let { Types.fst = m0; Types.snd = stack_high } = ms in let { Types.fst = id; Types.snd = ty } = v in let { Types.fst = c; Types.snd = stack_high0 } = match Bool.orb (always_alloc ty) (Identifiers.member PreIdentifiers.SymbolTag mem_vars id) with | Bool.True -> { Types.fst = (Stack stack_high); Types.snd = (Nat.plus stack_high (Csyntax.sizeof ty)) } | Bool.False -> { Types.fst = Local; Types.snd = stack_high } in { Types.fst = (Identifiers.add PreIdentifiers.SymbolTag m0 id { Types.fst = c; Types.snd = ty }); Types.snd = stack_high0 }) { Types.fst = m; Types.snd = Nat.O } (List.append f.Csyntax.fn_params f.Csyntax.fn_vars) in { Types.fst = m0; Types.snd = stacksize } open FrontEndVal open Hide open ByteValues open GenMem open FrontEndMem open Division open Z open BitVectorZ open Pointers open Values open FrontEndOps open Cminor_syntax (** val type_should_eq : Csyntax.type0 -> Csyntax.type0 -> 'a1 -> 'a1 Errors.res **) let type_should_eq ty1 ty2 p = Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (TypeComparison.assert_type_eq ty1 ty2)) (fun _ -> Obj.magic (Errors.OK ((fun p0 -> p0) p)))) (** val region_should_eq : AST.region -> AST.region -> 'a1 -> 'a1 Errors.res **) let region_should_eq clearme r2 x = (match clearme with | AST.XData -> (fun clearme0 -> match clearme0 with | AST.XData -> (fun _ p -> Errors.OK p) | AST.Code -> (fun _ p -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) | AST.Code -> (fun clearme0 -> match clearme0 with | AST.XData -> (fun _ p -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | AST.Code -> (fun _ p -> Errors.OK p))) r2 __ x (** val typ_should_eq : AST.typ -> AST.typ -> 'a1 -> 'a1 Errors.res **) let typ_should_eq ty1 ty2 p = match AST.typ_eq ty1 ty2 with | Types.Inl _ -> Errors.OK p | Types.Inr _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) (** val translate_unop : AST.typ -> AST.typ -> Csyntax.unary_operation -> FrontEndOps.unary_operation Errors.res **) let translate_unop t t' = function | Csyntax.Onotbool -> (match t with | AST.ASTint (sz, sg) -> (match t' with | AST.ASTint (sz', sg') -> Errors.OK (FrontEndOps.Onotbool ((AST.ASTint (sz, sg)), sz', sg')) | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | AST.ASTptr -> (match t' with | AST.ASTint (sz', sg') -> Errors.OK (FrontEndOps.Onotbool (AST.ASTptr, sz', sg')) | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) | Csyntax.Onotint -> (match t' with | AST.ASTint (sz, sg) -> typ_should_eq (AST.ASTint (sz, sg)) t (FrontEndOps.Onotint (sz, sg)) | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Oneg -> (match t' with | AST.ASTint (sz, sg) -> typ_should_eq (AST.ASTint (sz, sg)) t (FrontEndOps.Onegint (sz, sg)) | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) (** val fix_ptr_type : Csyntax.type0 -> Nat.nat Types.option -> Cminor_syntax.expr -> Cminor_syntax.expr **) let fix_ptr_type ty n e = e (** val translate_add : Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) let translate_add ty1 ty2 ty' = let ty1' = Csyntax.typ_of_type ty1 in let ty2' = Csyntax.typ_of_type ty2 in (match ClassifyOp.classify_add ty1 ty2 with | ClassifyOp.Add_case_ii (sz, sg) -> (fun e1 e2 -> typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)), (FrontEndOps.Oadd (sz, sg)), e1, e2))) | ClassifyOp.Add_case_pi (n, ty, sz, sg) -> (fun e1 e2 -> typ_should_eq AST.ASTptr (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 (AST.ASTptr, (AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr, (FrontEndOps.Oaddpi AST.I16), (fix_ptr_type ty n e1), (Cminor_syntax.Op2 ((AST.ASTint (AST.I16, AST.Signed)), (AST.ASTint (AST.I16, AST.Signed)), (AST.ASTint (AST.I16, AST.Signed)), (FrontEndOps.Omul (AST.I16, AST.Signed)), (Cminor_syntax.Op1 ((AST.ASTint (sz, sg)), (AST.ASTint (AST.I16, AST.Signed)), (FrontEndOps.Ocastint (sz, sg, AST.I16, AST.Signed)), e2)), (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed, (AST.repr AST.I16 (Csyntax.sizeof ty))))))))))) | ClassifyOp.Add_case_ip (n, sz, sg, ty) -> (fun e1 e2 -> typ_should_eq AST.ASTptr (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr, AST.ASTptr, (FrontEndOps.Oaddip AST.I16), (Cminor_syntax.Op2 ((AST.ASTint (AST.I16, AST.Signed)), (AST.ASTint (AST.I16, AST.Signed)), (AST.ASTint (AST.I16, AST.Signed)), (FrontEndOps.Omul (AST.I16, AST.Signed)), (Cminor_syntax.Op1 ((AST.ASTint (sz, sg)), (AST.ASTint (AST.I16, AST.Signed)), (FrontEndOps.Ocastint (sz, sg, AST.I16, AST.Signed)), e1)), (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed, (AST.repr AST.I16 (Csyntax.sizeof ty)))))))), (fix_ptr_type ty n e2)))) | ClassifyOp.Add_default (x, x0) -> (fun e1 e2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) (** val translate_sub : Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) let translate_sub ty1 ty2 ty' = let ty1' = Csyntax.typ_of_type ty1 in let ty2' = Csyntax.typ_of_type ty2 in (match ClassifyOp.classify_sub ty1 ty2 with | ClassifyOp.Sub_case_ii (sz, sg) -> (fun e1 e2 -> typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)), (FrontEndOps.Osub (sz, sg)), e1, e2))) | ClassifyOp.Sub_case_pi (n, ty, sz, sg) -> (fun e1 e2 -> typ_should_eq AST.ASTptr (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 (AST.ASTptr, (AST.ASTint (AST.I32, AST.Signed)), AST.ASTptr, (FrontEndOps.Osubpi AST.I32), (fix_ptr_type ty n e1), (Cminor_syntax.Op1 ((AST.ASTint (AST.I16, sg)), (AST.ASTint (AST.I32, AST.Signed)), (FrontEndOps.Ocastint (AST.I16, sg, AST.I32, AST.Signed)), (Cminor_syntax.Op2 ((AST.ASTint (AST.I16, sg)), (AST.ASTint (AST.I16, sg)), (AST.ASTint (AST.I16, sg)), (FrontEndOps.Omul (AST.I16, sg)), (Cminor_syntax.Op1 ((AST.ASTint (sz, sg)), (AST.ASTint (AST.I16, sg)), (FrontEndOps.Ocastint (sz, sg, AST.I16, sg)), e2)), (Cminor_syntax.Cst ((AST.ASTint (AST.I16, sg)), (FrontEndOps.Ointconst (AST.I16, sg, (AST.repr AST.I16 (Csyntax.sizeof ty))))))))))))) | ClassifyOp.Sub_case_pp (n1, n2, ty10, ty20) -> (fun e1 e2 -> match ty' with | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tint (sz, sg) -> Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (AST.I32, AST.Unsigned)), (AST.ASTint (sz, sg)), (FrontEndOps.Ocastint (AST.I32, AST.Unsigned, sz, sg)), (Cminor_syntax.Op2 ((AST.ASTint (AST.I32, AST.Unsigned)), (AST.ASTint (AST.I32, AST.Unsigned)), (AST.ASTint (AST.I32, AST.Unsigned)), (FrontEndOps.Odivu AST.I32), (Cminor_syntax.Op2 (AST.ASTptr, AST.ASTptr, (AST.ASTint (AST.I32, AST.Unsigned)), (FrontEndOps.Osubpp AST.I32), (fix_ptr_type ty10 n1 e1), (fix_ptr_type ty20 n2 e2))), (Cminor_syntax.Cst ((AST.ASTint (AST.I32, AST.Unsigned)), (FrontEndOps.Ointconst (AST.I32, AST.Unsigned, (AST.repr AST.I32 (Csyntax.sizeof ty10)))))))))) | Csyntax.Tpointer x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tarray (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tfunction (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tstruct (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tunion (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tcomp_ptr x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | ClassifyOp.Sub_default (x, x0) -> (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) (** val translate_mul : Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) let translate_mul ty1 ty2 ty' = let ty1' = Csyntax.typ_of_type ty1 in let ty2' = Csyntax.typ_of_type ty2 in (match ClassifyOp.classify_aop ty1 ty2 with | ClassifyOp.Aop_case_ii (sz, sg) -> (fun e1 e2 -> typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)), (FrontEndOps.Omul (sz, sg)), e1, e2))) | ClassifyOp.Aop_default (x, x0) -> (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) (** val translate_div : Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) let translate_div ty1 ty2 ty' = let ty1' = Csyntax.typ_of_type ty1 in let ty2' = Csyntax.typ_of_type ty2 in (match ClassifyOp.classify_aop ty1 ty2 with | ClassifyOp.Aop_case_ii (sz, sg) -> (match sg with | AST.Signed -> (fun e1 e2 -> typ_should_eq (AST.ASTint (sz, AST.Signed)) (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz, AST.Signed)), (FrontEndOps.Odiv sz), e1, e2))) | AST.Unsigned -> (fun e1 e2 -> typ_should_eq (AST.ASTint (sz, AST.Unsigned)) (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (FrontEndOps.Odivu sz), e1, e2)))) | ClassifyOp.Aop_default (x, x0) -> (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) (** val translate_mod : Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) let translate_mod ty1 ty2 ty' = let ty1' = Csyntax.typ_of_type ty1 in let ty2' = Csyntax.typ_of_type ty2 in (match ClassifyOp.classify_aop ty1 ty2 with | ClassifyOp.Aop_case_ii (sz, sg) -> (match sg with | AST.Signed -> (fun e1 e2 -> typ_should_eq (AST.ASTint (sz, AST.Signed)) (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz, AST.Signed)), (FrontEndOps.Omod sz), e1, e2))) | AST.Unsigned -> (fun e1 e2 -> typ_should_eq (AST.ASTint (sz, AST.Unsigned)) (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (FrontEndOps.Omodu sz), e1, e2)))) | ClassifyOp.Aop_default (x, x0) -> (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) (** val translate_shr : Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) let translate_shr ty1 ty2 ty' = let ty1' = Csyntax.typ_of_type ty1 in let ty2' = Csyntax.typ_of_type ty2 in (match ClassifyOp.classify_aop ty1 ty2 with | ClassifyOp.Aop_case_ii (sz, sg) -> (match sg with | AST.Signed -> (fun e1 e2 -> typ_should_eq (AST.ASTint (sz, AST.Signed)) (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz, AST.Signed)), (FrontEndOps.Oshr (sz, AST.Signed)), e1, e2))) | AST.Unsigned -> (fun e1 e2 -> typ_should_eq (AST.ASTint (sz, AST.Unsigned)) (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (FrontEndOps.Oshru (sz, AST.Unsigned)), e1, e2)))) | ClassifyOp.Aop_default (x, x0) -> (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) (** val complete_cmp : Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) let complete_cmp ty' e = match ty' with | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tint (sz, sg) -> Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (AST.I8, AST.Unsigned)), (AST.ASTint (sz, sg)), (FrontEndOps.Ocastint (AST.I8, AST.Unsigned, sz, sg)), e)) | Csyntax.Tpointer x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tarray (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tfunction (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tstruct (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tunion (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tcomp_ptr x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) (** val translate_cmp : Integers.comparison -> Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) let translate_cmp c ty1 ty2 ty' = let ty1' = Csyntax.typ_of_type ty1 in let ty2' = Csyntax.typ_of_type ty2 in (match ClassifyOp.classify_cmp ty1 ty2 with | ClassifyOp.Cmp_case_ii (sz, sg) -> (match sg with | AST.Signed -> (fun e1 e2 -> complete_cmp ty' (Cminor_syntax.Op2 ((AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz, AST.Signed)), (AST.ASTint (AST.I8, AST.Unsigned)), (FrontEndOps.Ocmp (sz, AST.Signed, AST.Unsigned, c)), e1, e2))) | AST.Unsigned -> (fun e1 e2 -> complete_cmp ty' (Cminor_syntax.Op2 ((AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (AST.I8, AST.Unsigned)), (FrontEndOps.Ocmpu (sz, AST.Unsigned, c)), e1, e2)))) | ClassifyOp.Cmp_case_pp (n, ty) -> (fun e1 e2 -> complete_cmp ty' (Cminor_syntax.Op2 (AST.ASTptr, AST.ASTptr, (AST.ASTint (AST.I8, AST.Unsigned)), (FrontEndOps.Ocmpp (AST.Unsigned, c)), (fix_ptr_type ty n e1), (fix_ptr_type ty n e2)))) | ClassifyOp.Cmp_default (x, x0) -> (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) (** val translate_misc_aop : Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> (AST.intsize -> AST.signedness -> FrontEndOps.binary_operation) -> Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) let translate_misc_aop ty1 ty2 ty' op = let ty1' = Csyntax.typ_of_type ty1 in let ty2' = Csyntax.typ_of_type ty2 in (match ClassifyOp.classify_aop ty1 ty2 with | ClassifyOp.Aop_case_ii (sz, sg) -> (fun e1 e2 -> typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((Csyntax.typ_of_type (Csyntax.Tint (sz, sg))), (Csyntax.typ_of_type (Csyntax.Tint (sz, sg))), (AST.ASTint (sz, sg)), (op sz sg), e1, e2))) | ClassifyOp.Aop_default (x, x0) -> (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) (** val translate_binop : Csyntax.binary_operation -> Csyntax.type0 -> Cminor_syntax.expr -> Csyntax.type0 -> Cminor_syntax.expr -> Csyntax.type0 -> Cminor_syntax.expr Errors.res **) let translate_binop op ty1 e1 ty2 e2 ty = let ty' = Csyntax.typ_of_type ty in (match op with | Csyntax.Oadd -> translate_add ty1 ty2 ty e1 e2 | Csyntax.Osub -> translate_sub ty1 ty2 ty e1 e2 | Csyntax.Omul -> translate_mul ty1 ty2 ty e1 e2 | Csyntax.Odiv -> translate_div ty1 ty2 ty e1 e2 | Csyntax.Omod -> translate_mod ty1 ty2 ty e1 e2 | Csyntax.Oand -> translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oand (x, x0)) e1 e2 | Csyntax.Oor -> translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oor (x, x0)) e1 e2 | Csyntax.Oxor -> translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oxor (x, x0)) e1 e2 | Csyntax.Oshl -> translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oshl (x, x0)) e1 e2 | Csyntax.Oshr -> translate_shr ty1 ty2 ty e1 e2 | Csyntax.Oeq -> translate_cmp Integers.Ceq ty1 ty2 ty e1 e2 | Csyntax.One -> translate_cmp Integers.Cne ty1 ty2 ty e1 e2 | Csyntax.Olt -> translate_cmp Integers.Clt ty1 ty2 ty e1 e2 | Csyntax.Ogt -> translate_cmp Integers.Cgt ty1 ty2 ty e1 e2 | Csyntax.Ole -> translate_cmp Integers.Cle ty1 ty2 ty e1 e2 | Csyntax.Oge -> translate_cmp Integers.Cge ty1 ty2 ty e1 e2) (** val translate_cast : Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr Types.sig0 -> Cminor_syntax.expr Types.sig0 Errors.res **) let translate_cast ty1 ty2 = match ty1 with | Csyntax.Tvoid -> (fun x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tint (sz1, sg1) -> (fun e -> match ty2 with | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tint (sz2, sg2) -> Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), (AST.ASTint (sz2, sg2)), (FrontEndOps.Ocastint (sz1, sg1, sz2, sg2)), (Types.pi1 e))) | Csyntax.Tpointer x -> Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), AST.ASTptr, (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e))) | Csyntax.Tarray (x, x0) -> Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), AST.ASTptr, (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e))) | Csyntax.Tfunction (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tstruct (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tunion (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tcomp_ptr x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tpointer x -> (fun e -> match ty2 with | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tint (sz2, sg2) -> Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)), (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e))) | Csyntax.Tpointer x0 -> Errors.OK e | Csyntax.Tarray (x0, x1) -> Errors.OK e | Csyntax.Tfunction (x0, x1) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tstruct (x0, x1) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tunion (x0, x1) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tcomp_ptr x0 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tarray (x, x0) -> (fun e -> match ty2 with | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tint (sz2, sg2) -> Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)), (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e))) | Csyntax.Tpointer x1 -> Errors.OK e | Csyntax.Tarray (x1, x2) -> Errors.OK e | Csyntax.Tfunction (x1, x2) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tstruct (x1, x2) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tunion (x1, x2) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tcomp_ptr x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tfunction (x, x0) -> (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tstruct (x, x0) -> (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tunion (x, x0) -> (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tcomp_ptr x -> (fun x0 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) (** val cm_zero : AST.intsize -> AST.signedness -> Cminor_syntax.expr **) let cm_zero sz sg = Cminor_syntax.Cst ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg, (BitVector.zero (AST.bitsize_of_intsize sz))))) (** val cm_one : AST.intsize -> AST.signedness -> Cminor_syntax.expr **) let cm_one sz sg = Cminor_syntax.Cst ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg, (AST.repr sz (Nat.S Nat.O))))) (** val translate_expr : var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res **) let rec translate_expr vars = function | Csyntax.Expr (ed, ty) -> (match ed with | Csyntax.Econst_int (sz, i) -> (match ty with | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tint (sz', sg) -> AST.intsize_eq_elim' sz sz' (Errors.OK (Cminor_syntax.Cst ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg, i))))) (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tpointer x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tarray (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tfunction (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tstruct (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tunion (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tcomp_ptr x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Evar id -> Errors.bind2_eq (lookup' vars id) (fun c t _ -> (match c with | Global r -> (fun _ -> match Csyntax.access_mode ty with | Csyntax.By_value t0 -> Errors.OK (Cminor_syntax.Mem (t0, (Cminor_syntax.Cst (AST.ASTptr, (FrontEndOps.Oaddrsymbol (id, Nat.O)))))) | Csyntax.By_reference -> Errors.OK (Cminor_syntax.Cst (AST.ASTptr, (FrontEndOps.Oaddrsymbol (id, Nat.O)))) | Csyntax.By_nothing x -> Errors.Error (List.Cons ((Errors.MSG ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))) | Stack n -> (fun _ -> match Csyntax.access_mode ty with | Csyntax.By_value t0 -> Errors.OK (Cminor_syntax.Mem (t0, (Cminor_syntax.Cst (AST.ASTptr, (FrontEndOps.Oaddrstack n))))) | Csyntax.By_reference -> Errors.OK (Cminor_syntax.Cst (AST.ASTptr, (FrontEndOps.Oaddrstack n))) | Csyntax.By_nothing x -> Errors.Error (List.Cons ((Errors.MSG ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))) | Local -> (fun _ -> type_should_eq t ty (Cminor_syntax.Id ((Csyntax.typ_of_type t), id)))) __) | Csyntax.Ederef e1 -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e1)) (fun e1' -> (match Csyntax.typ_of_type (Csyntax.typeof e1) with | AST.ASTint (x, x0) -> (fun x1 -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) | AST.ASTptr -> (fun e1'0 -> match Csyntax.access_mode ty with | Csyntax.By_value t -> Obj.magic (Errors.OK (Cminor_syntax.Mem (t, (Types.pi1 e1'0)))) | Csyntax.By_reference -> Obj.magic (Errors.OK e1'0) | Csyntax.By_nothing x -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)))) e1')) | Csyntax.Eaddrof e1 -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_addr vars e1)) (fun e1' -> match Csyntax.typ_of_type ty with | AST.ASTint (x, x0) -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | AST.ASTptr -> Obj.magic (Errors.OK e1'))) | Csyntax.Eunop (op, e1) -> (match op with | Csyntax.Onotbool -> (fun _ -> (match Csyntax.typ_of_type ty with | AST.ASTint (sz, sg) -> (fun _ -> (match sz with | AST.I8 -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | AST.I16 -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | AST.I32 -> (fun _ -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_unop (Csyntax.typ_of_type (Csyntax.typeof e1)) (Csyntax.typ_of_type ty) op)) (fun op' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e1)) (fun e1' -> Obj.magic (Errors.OK (Cminor_syntax.Op1 ((Csyntax.typ_of_type (Csyntax.typeof e1)), (Csyntax.typ_of_type ty), op', (Types.pi1 e1'))))))))) __) | AST.ASTptr -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) __) | Csyntax.Onotint -> (fun _ -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_unop (Csyntax.typ_of_type (Csyntax.typeof e1)) (Csyntax.typ_of_type ty) op)) (fun op' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e1)) (fun e1' -> Obj.magic (Errors.OK (Cminor_syntax.Op1 ((Csyntax.typ_of_type (Csyntax.typeof e1)), (Csyntax.typ_of_type ty), op', (Types.pi1 e1')))))))) | Csyntax.Oneg -> (fun _ -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_unop (Csyntax.typ_of_type (Csyntax.typeof e1)) (Csyntax.typ_of_type ty) op)) (fun op' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e1)) (fun e1' -> Obj.magic (Errors.OK (Cminor_syntax.Op1 ((Csyntax.typ_of_type (Csyntax.typeof e1)), (Csyntax.typ_of_type ty), op', (Types.pi1 e1'))))))))) __ | Csyntax.Ebinop (op, e1, e2) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e1)) (fun e1' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e2)) (fun e2' -> Obj.magic (Errors.bind_eq (translate_binop op (Csyntax.typeof e1) (Types.pi1 e1') (Csyntax.typeof e2) (Types.pi1 e2') ty) (fun e' _ -> Errors.OK e'))))) | Csyntax.Ecast (ty1, e1) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e1)) (fun e1' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_cast (Csyntax.typeof e1) ty1 e1')) (fun e' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (typ_should_eq (Csyntax.typ_of_type ty1) (Csyntax.typ_of_type ty) e')) (fun e'0 -> Obj.magic (Errors.OK e'0))))) | Csyntax.Econdition (e1, e2, e3) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e1)) (fun e1' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e2)) (fun e2' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e2)) (Csyntax.typ_of_type ty) e2')) (fun e2'0 -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e3)) (fun e3' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e3)) (Csyntax.typ_of_type ty) e3')) (fun e3'0 -> (match Csyntax.typ_of_type (Csyntax.typeof e1) with | AST.ASTint (x, x0) -> (fun e1'0 -> Obj.magic (Errors.OK (Cminor_syntax.Cond (x, x0, (Csyntax.typ_of_type ty), (Types.pi1 e1'0), (Types.pi1 e2'0), (Types.pi1 e3'0))))) | AST.ASTptr -> (fun x -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))) e1')))))) | Csyntax.Eandbool (e1, e2) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e1)) (fun e1' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e2)) (fun e2' -> match ty with | Csyntax.Tvoid -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tint (sz, sg) -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (type_should_eq (Csyntax.typeof e2) (Csyntax.Tint (sz, sg)) e2')) (fun e2'0 -> (match Csyntax.typ_of_type (Csyntax.typeof e1) with | AST.ASTint (sz1, x) -> (fun e1'0 -> Obj.magic (Errors.OK (Cminor_syntax.Cond (sz1, x, (AST.ASTint (sz, sg)), (Types.pi1 e1'0), (Cminor_syntax.Cond (sz, sg, (AST.ASTint (sz, sg)), (Types.pi1 e2'0), (cm_one sz sg), (cm_zero sz sg))), (cm_zero sz sg))))) | AST.ASTptr -> (fun x -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))) e1') | Csyntax.Tpointer x -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tarray (x, x0) -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tfunction (x, x0) -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tstruct (x, x0) -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tunion (x, x0) -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tcomp_ptr x -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))) | Csyntax.Eorbool (e1, e2) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e1)) (fun e1' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e2)) (fun e2' -> match ty with | Csyntax.Tvoid -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tint (sz, sg) -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (type_should_eq (Csyntax.typeof e2) (Csyntax.Tint (sz, sg)) e2')) (fun e2'0 -> (match Csyntax.typ_of_type (Csyntax.typeof e1) with | AST.ASTint (x, x0) -> (fun e1'0 -> Obj.magic (Errors.OK (Cminor_syntax.Cond (x, x0, (AST.ASTint (sz, sg)), (Types.pi1 e1'0), (cm_one sz sg), (Cminor_syntax.Cond (sz, sg, (AST.ASTint (sz, sg)), (Types.pi1 e2'0), (cm_one sz sg), (cm_zero sz sg))))))) | AST.ASTptr -> (fun x -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))) e1') | Csyntax.Tpointer x -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tarray (x, x0) -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tfunction (x, x0) -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tstruct (x, x0) -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tunion (x, x0) -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Tcomp_ptr x -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))) | Csyntax.Esizeof ty1 -> (match ty with | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tint (sz, sg) -> Errors.OK (Cminor_syntax.Cst ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg, (AST.repr sz (Csyntax.sizeof ty1)))))) | Csyntax.Tpointer x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tarray (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tfunction (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tstruct (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tunion (x, x0) -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) | Csyntax.Tcomp_ptr x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) | Csyntax.Efield (e1, id) -> (match Csyntax.typeof e1 with | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) | Csyntax.Tint (x, x0) -> Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) | Csyntax.Tpointer x -> Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) | Csyntax.Tarray (x, x0) -> Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) | Csyntax.Tfunction (x, x0) -> Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) | Csyntax.Tstruct (x, fl) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_addr vars e1)) (fun e1' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Csyntax.field_offset id fl)) (fun off -> match Csyntax.access_mode ty with | Csyntax.By_value t -> Obj.magic (Errors.OK (Cminor_syntax.Mem (t, (Cminor_syntax.Op2 (AST.ASTptr, (AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr, (FrontEndOps.Oaddpi AST.I16), (Types.pi1 e1'), (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed, (AST.repr AST.I16 off)))))))))) | Csyntax.By_reference -> Obj.magic (Errors.OK (Cminor_syntax.Op2 (AST.ASTptr, (AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr, (FrontEndOps.Oaddpi AST.I16), (Types.pi1 e1'), (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed, (AST.repr AST.I16 off)))))))) | Csyntax.By_nothing x0 -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess))))) | Csyntax.Tunion (x, x0) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_addr vars e1)) (fun e1' -> match Csyntax.access_mode ty with | Csyntax.By_value t -> Obj.magic (Errors.OK (Cminor_syntax.Mem (t, (Types.pi1 e1')))) | Csyntax.By_reference -> Obj.magic (Errors.OK e1') | Csyntax.By_nothing x1 -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)))) | Csyntax.Tcomp_ptr x -> Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)) | Csyntax.Ecost (l, e1) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e1)) (fun e1' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.OK (Cminor_syntax.Ecost ((Csyntax.typ_of_type (Csyntax.typeof e1)), l, (Types.pi1 e1'))))) (fun e' -> Obj.magic (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e1)) (Csyntax.typ_of_type ty) e'))))) (** val translate_addr : var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res **) and translate_addr vars = function | Csyntax.Expr (ed, x) -> (match ed with | Csyntax.Econst_int (x0, x1) -> Errors.Error (Errors.msg ErrorMessages.BadLvalue) | Csyntax.Evar id -> Obj.magic (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (lookup' vars id)) (fun c t -> match c with | Global r -> Obj.magic (Errors.OK (Cminor_syntax.Cst (AST.ASTptr, (FrontEndOps.Oaddrsymbol (id, Nat.O))))) | Stack n -> Obj.magic (Errors.OK (Cminor_syntax.Cst (AST.ASTptr, (FrontEndOps.Oaddrstack n)))) | Local -> Obj.magic (Errors.Error (List.Cons ((Errors.MSG ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))))) | Csyntax.Ederef e1 -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e1)) (fun e1' -> (match Csyntax.typ_of_type (Csyntax.typeof e1) with | AST.ASTint (x0, x1) -> (fun x2 -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess))) | AST.ASTptr -> (fun e1'0 -> Obj.magic (Errors.OK e1'0))) e1')) | Csyntax.Eaddrof x0 -> Errors.Error (Errors.msg ErrorMessages.BadLvalue) | Csyntax.Eunop (x0, x1) -> Errors.Error (Errors.msg ErrorMessages.BadLvalue) | Csyntax.Ebinop (x0, x1, x2) -> Errors.Error (Errors.msg ErrorMessages.BadLvalue) | Csyntax.Ecast (x0, x1) -> Errors.Error (Errors.msg ErrorMessages.BadLvalue) | Csyntax.Econdition (x0, x1, x2) -> Errors.Error (Errors.msg ErrorMessages.BadLvalue) | Csyntax.Eandbool (x0, x1) -> Errors.Error (Errors.msg ErrorMessages.BadLvalue) | Csyntax.Eorbool (x0, x1) -> Errors.Error (Errors.msg ErrorMessages.BadLvalue) | Csyntax.Esizeof x0 -> Errors.Error (Errors.msg ErrorMessages.BadLvalue) | Csyntax.Efield (e1, id) -> (match Csyntax.typeof e1 with | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) | Csyntax.Tint (x0, x1) -> Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) | Csyntax.Tpointer x0 -> Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) | Csyntax.Tarray (x0, x1) -> Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) | Csyntax.Tfunction (x0, x1) -> Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) | Csyntax.Tstruct (x0, fl) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_addr vars e1)) (fun e1' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Csyntax.field_offset id fl)) (fun off -> Obj.magic (Errors.OK (Cminor_syntax.Op2 (AST.ASTptr, (AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr, (FrontEndOps.Oaddpi AST.I16), (Types.pi1 e1'), (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed, (AST.repr AST.I16 off))))))))))) | Csyntax.Tunion (x0, x1) -> translate_addr vars e1 | Csyntax.Tcomp_ptr x0 -> Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)) | Csyntax.Ecost (x0, x1) -> Errors.Error (Errors.msg ErrorMessages.BadLvalue)) type destination = | IdDest of AST.ident | MemDest of Cminor_syntax.expr Types.sig0 (** val destination_rect_Type4 : var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **) let rec destination_rect_Type4 vars t h_IdDest h_MemDest = function | IdDest id -> h_IdDest id __ | MemDest x_14524 -> h_MemDest x_14524 (** val destination_rect_Type5 : var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **) let rec destination_rect_Type5 vars t h_IdDest h_MemDest = function | IdDest id -> h_IdDest id __ | MemDest x_14529 -> h_MemDest x_14529 (** val destination_rect_Type3 : var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **) let rec destination_rect_Type3 vars t h_IdDest h_MemDest = function | IdDest id -> h_IdDest id __ | MemDest x_14534 -> h_MemDest x_14534 (** val destination_rect_Type2 : var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **) let rec destination_rect_Type2 vars t h_IdDest h_MemDest = function | IdDest id -> h_IdDest id __ | MemDest x_14539 -> h_MemDest x_14539 (** val destination_rect_Type1 : var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **) let rec destination_rect_Type1 vars t h_IdDest h_MemDest = function | IdDest id -> h_IdDest id __ | MemDest x_14544 -> h_MemDest x_14544 (** val destination_rect_Type0 : var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **) let rec destination_rect_Type0 vars t h_IdDest h_MemDest = function | IdDest id -> h_IdDest id __ | MemDest x_14549 -> h_MemDest x_14549 (** val destination_inv_rect_Type4 : var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **) let destination_inv_rect_Type4 x1 x2 hterm h1 h2 = let hcut = destination_rect_Type4 x1 x2 h1 h2 hterm in hcut __ (** val destination_inv_rect_Type3 : var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **) let destination_inv_rect_Type3 x1 x2 hterm h1 h2 = let hcut = destination_rect_Type3 x1 x2 h1 h2 hterm in hcut __ (** val destination_inv_rect_Type2 : var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **) let destination_inv_rect_Type2 x1 x2 hterm h1 h2 = let hcut = destination_rect_Type2 x1 x2 h1 h2 hterm in hcut __ (** val destination_inv_rect_Type1 : var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **) let destination_inv_rect_Type1 x1 x2 hterm h1 h2 = let hcut = destination_rect_Type1 x1 x2 h1 h2 hterm in hcut __ (** val destination_inv_rect_Type0 : var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **) let destination_inv_rect_Type0 x1 x2 hterm h1 h2 = let hcut = destination_rect_Type0 x1 x2 h1 h2 hterm in hcut __ (** val destination_discr : var_types -> AST.typ -> destination -> destination -> __ **) let destination_discr a1 a2 x y = Logic.eq_rect_Type2 x (match x with | IdDest a0 -> Obj.magic (fun _ dH -> dH __ __) | MemDest a0 -> Obj.magic (fun _ dH -> dH __)) y (** val destination_jmdiscr : var_types -> AST.typ -> destination -> destination -> __ **) let destination_jmdiscr a1 a2 x y = Logic.eq_rect_Type2 x (match x with | IdDest a0 -> Obj.magic (fun _ dH -> dH __ __) | MemDest a0 -> Obj.magic (fun _ dH -> dH __)) y (** val translate_dest : var_types -> Csyntax.expr -> destination Errors.res **) let translate_dest vars e1 = match e1 with | Csyntax.Expr (ed1, ty1) -> (match ed1 with | Csyntax.Econst_int (x, x0) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_addr vars e1)) (fun e1' -> Obj.magic (Errors.OK (MemDest e1')))) | Csyntax.Evar id -> Errors.bind2_eq (lookup' vars id) (fun c t _ -> (match c with | Global r -> (fun _ -> Errors.OK (MemDest (Cminor_syntax.Cst (AST.ASTptr, (FrontEndOps.Oaddrsymbol (id, Nat.O)))))) | Stack n -> (fun _ -> Errors.OK (MemDest (Cminor_syntax.Cst (AST.ASTptr, (FrontEndOps.Oaddrstack n))))) | Local -> (fun _ -> match AST.typ_eq (Csyntax.typ_of_type ty1) (Csyntax.typ_of_type t) with | Types.Inl _ -> Errors.OK (IdDest id) | Types.Inr _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) __) | Csyntax.Ederef x -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_addr vars e1)) (fun e1' -> Obj.magic (Errors.OK (MemDest e1')))) | Csyntax.Eaddrof x -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_addr vars e1)) (fun e1' -> Obj.magic (Errors.OK (MemDest e1')))) | Csyntax.Eunop (x, x0) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_addr vars e1)) (fun e1' -> Obj.magic (Errors.OK (MemDest e1')))) | Csyntax.Ebinop (x, x0, x1) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_addr vars e1)) (fun e1' -> Obj.magic (Errors.OK (MemDest e1')))) | Csyntax.Ecast (x, x0) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_addr vars e1)) (fun e1' -> Obj.magic (Errors.OK (MemDest e1')))) | Csyntax.Econdition (x, x0, x1) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_addr vars e1)) (fun e1' -> Obj.magic (Errors.OK (MemDest e1')))) | Csyntax.Eandbool (x, x0) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_addr vars e1)) (fun e1' -> Obj.magic (Errors.OK (MemDest e1')))) | Csyntax.Eorbool (x, x0) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_addr vars e1)) (fun e1' -> Obj.magic (Errors.OK (MemDest e1')))) | Csyntax.Esizeof x -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_addr vars e1)) (fun e1' -> Obj.magic (Errors.OK (MemDest e1')))) | Csyntax.Efield (x, x0) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_addr vars e1)) (fun e1' -> Obj.magic (Errors.OK (MemDest e1')))) | Csyntax.Ecost (x, x0) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_addr vars e1)) (fun e1' -> Obj.magic (Errors.OK (MemDest e1'))))) type lenv = PreIdentifiers.identifier Identifiers.identifier_map (** val lookup_label : lenv -> PreIdentifiers.identifier -> PreIdentifiers.identifier Errors.res **) let lookup_label lbls l = Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingLabel), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, l)), List.Nil)))) (Identifiers.lookup PreIdentifiers.SymbolTag lbls l) type labgen = { labuniverse : Identifiers.universe; label_genlist : PreIdentifiers.identifier List.list } (** val labgen_rect_Type4 : (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1) -> labgen -> 'a1 **) let rec labgen_rect_Type4 h_mk_labgen x_14584 = let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_14584 in h_mk_labgen labuniverse0 label_genlist0 __ (** val labgen_rect_Type5 : (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1) -> labgen -> 'a1 **) let rec labgen_rect_Type5 h_mk_labgen x_14586 = let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_14586 in h_mk_labgen labuniverse0 label_genlist0 __ (** val labgen_rect_Type3 : (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1) -> labgen -> 'a1 **) let rec labgen_rect_Type3 h_mk_labgen x_14588 = let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_14588 in h_mk_labgen labuniverse0 label_genlist0 __ (** val labgen_rect_Type2 : (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1) -> labgen -> 'a1 **) let rec labgen_rect_Type2 h_mk_labgen x_14590 = let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_14590 in h_mk_labgen labuniverse0 label_genlist0 __ (** val labgen_rect_Type1 : (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1) -> labgen -> 'a1 **) let rec labgen_rect_Type1 h_mk_labgen x_14592 = let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_14592 in h_mk_labgen labuniverse0 label_genlist0 __ (** val labgen_rect_Type0 : (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1) -> labgen -> 'a1 **) let rec labgen_rect_Type0 h_mk_labgen x_14594 = let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_14594 in h_mk_labgen labuniverse0 label_genlist0 __ (** val labuniverse : labgen -> Identifiers.universe **) let rec labuniverse xxx = xxx.labuniverse (** val label_genlist : labgen -> PreIdentifiers.identifier List.list **) let rec label_genlist xxx = xxx.label_genlist (** val labgen_inv_rect_Type4 : labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> __ -> 'a1) -> 'a1 **) let labgen_inv_rect_Type4 hterm h1 = let hcut = labgen_rect_Type4 h1 hterm in hcut __ (** val labgen_inv_rect_Type3 : labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> __ -> 'a1) -> 'a1 **) let labgen_inv_rect_Type3 hterm h1 = let hcut = labgen_rect_Type3 h1 hterm in hcut __ (** val labgen_inv_rect_Type2 : labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> __ -> 'a1) -> 'a1 **) let labgen_inv_rect_Type2 hterm h1 = let hcut = labgen_rect_Type2 h1 hterm in hcut __ (** val labgen_inv_rect_Type1 : labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> __ -> 'a1) -> 'a1 **) let labgen_inv_rect_Type1 hterm h1 = let hcut = labgen_rect_Type1 h1 hterm in hcut __ (** val labgen_inv_rect_Type0 : labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> __ -> 'a1) -> 'a1 **) let labgen_inv_rect_Type0 hterm h1 = let hcut = labgen_rect_Type0 h1 hterm in hcut __ (** val labgen_discr : labgen -> labgen -> __ **) let labgen_discr x y = Logic.eq_rect_Type2 x (let { labuniverse = a0; label_genlist = a1 } = x in Obj.magic (fun _ dH -> dH __ __ __)) y (** val labgen_jmdiscr : labgen -> labgen -> __ **) let labgen_jmdiscr x y = Logic.eq_rect_Type2 x (let { labuniverse = a0; label_genlist = a1 } = x in Obj.magic (fun _ dH -> dH __ __ __)) y (** val generate_fresh_label : labgen -> (PreIdentifiers.identifier, labgen) Types.prod Types.sig0 **) let generate_fresh_label ul = (let { Types.fst = tmp; Types.snd = u } = Identifiers.fresh PreIdentifiers.Label ul.labuniverse in (fun _ -> { Types.fst = tmp; Types.snd = { labuniverse = u; label_genlist = (List.Cons (tmp, ul.label_genlist)) } })) __ (** val labels_defined : Csyntax.statement -> AST.ident List.list **) let rec labels_defined = function | Csyntax.Sskip -> List.Nil | Csyntax.Sassign (x, x0) -> List.Nil | Csyntax.Scall (x, x0, x1) -> List.Nil | Csyntax.Ssequence (s1, s2) -> List.append (labels_defined s1) (labels_defined s2) | Csyntax.Sifthenelse (x, s1, s2) -> List.append (labels_defined s1) (labels_defined s2) | Csyntax.Swhile (x, s0) -> labels_defined s0 | Csyntax.Sdowhile (x, s0) -> labels_defined s0 | Csyntax.Sfor (s1, x, s2, s3) -> List.append (labels_defined s1) (List.append (labels_defined s2) (labels_defined s3)) | Csyntax.Sbreak -> List.Nil | Csyntax.Scontinue -> List.Nil | Csyntax.Sreturn x -> List.Nil | Csyntax.Sswitch (x, ls) -> labels_defined_switch ls | Csyntax.Slabel (l, s0) -> List.Cons (l, (labels_defined s0)) | Csyntax.Sgoto x -> List.Nil | Csyntax.Scost (x, s0) -> labels_defined s0 (** val labels_defined_switch : Csyntax.labeled_statements -> AST.ident List.list **) and labels_defined_switch = function | Csyntax.LSdefault s -> labels_defined s | Csyntax.LScase (x, x0, s, ls0) -> List.append (labels_defined s) (labels_defined_switch ls0) (** val m_option_map : ('a1 -> 'a2 Errors.res) -> 'a1 Types.option -> 'a2 Types.option Errors.res **) let m_option_map f = function | Types.None -> Errors.OK Types.None | Types.Some a -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f a) (fun b -> Obj.magic (Errors.OK (Types.Some b)))) (** val translate_expr_sigma : var_types -> Csyntax.expr -> (AST.typ, Cminor_syntax.expr) Types.dPair Types.sig0 Errors.res **) let translate_expr_sigma v e = Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr v e)) (fun e' -> Obj.magic (Errors.OK { Types.dpi1 = (Csyntax.typ_of_type (Csyntax.typeof e)); Types.dpi2 = (Types.pi1 e') }))) (** val add_tmps : var_types -> (AST.ident, Csyntax.type0) Types.prod List.list -> var_types **) let add_tmps vs tmpenv = List.foldr (fun idty vs0 -> Identifiers.add PreIdentifiers.SymbolTag vs0 idty.Types.fst { Types.fst = Local; Types.snd = idty.Types.snd }) vs tmpenv type tmpgen = { tmp_universe : Identifiers.universe; tmp_env : (AST.ident, Csyntax.type0) Types.prod List.list } (** val tmpgen_rect_Type4 : var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **) let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14610 = let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14610 in h_mk_tmpgen tmp_universe0 tmp_env0 __ __ (** val tmpgen_rect_Type5 : var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **) let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14612 = let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14612 in h_mk_tmpgen tmp_universe0 tmp_env0 __ __ (** val tmpgen_rect_Type3 : var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **) let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14614 = let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14614 in h_mk_tmpgen tmp_universe0 tmp_env0 __ __ (** val tmpgen_rect_Type2 : var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **) let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14616 = let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14616 in h_mk_tmpgen tmp_universe0 tmp_env0 __ __ (** val tmpgen_rect_Type1 : var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **) let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14618 = let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14618 in h_mk_tmpgen tmp_universe0 tmp_env0 __ __ (** val tmpgen_rect_Type0 : var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **) let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14620 = let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14620 in h_mk_tmpgen tmp_universe0 tmp_env0 __ __ (** val tmp_universe : var_types -> tmpgen -> Identifiers.universe **) let rec tmp_universe vars xxx = xxx.tmp_universe (** val tmp_env : var_types -> tmpgen -> (AST.ident, Csyntax.type0) Types.prod List.list **) let rec tmp_env vars xxx = xxx.tmp_env (** val tmpgen_inv_rect_Type4 : var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **) let tmpgen_inv_rect_Type4 x1 hterm h1 = let hcut = tmpgen_rect_Type4 x1 h1 hterm in hcut __ (** val tmpgen_inv_rect_Type3 : var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **) let tmpgen_inv_rect_Type3 x1 hterm h1 = let hcut = tmpgen_rect_Type3 x1 h1 hterm in hcut __ (** val tmpgen_inv_rect_Type2 : var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **) let tmpgen_inv_rect_Type2 x1 hterm h1 = let hcut = tmpgen_rect_Type2 x1 h1 hterm in hcut __ (** val tmpgen_inv_rect_Type1 : var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **) let tmpgen_inv_rect_Type1 x1 hterm h1 = let hcut = tmpgen_rect_Type1 x1 h1 hterm in hcut __ (** val tmpgen_inv_rect_Type0 : var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **) let tmpgen_inv_rect_Type0 x1 hterm h1 = let hcut = tmpgen_rect_Type0 x1 h1 hterm in hcut __ (** val tmpgen_discr : var_types -> tmpgen -> tmpgen -> __ **) let tmpgen_discr a1 x y = Logic.eq_rect_Type2 x (let { tmp_universe = a0; tmp_env = a10 } = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y (** val tmpgen_jmdiscr : var_types -> tmpgen -> tmpgen -> __ **) let tmpgen_jmdiscr a1 x y = Logic.eq_rect_Type2 x (let { tmp_universe = a0; tmp_env = a10 } = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y (** val alloc_tmp : var_types -> Csyntax.type0 -> tmpgen -> (AST.ident, tmpgen) Types.prod **) let alloc_tmp vars ty g = (let { Types.fst = tmp; Types.snd = u } = Identifiers.fresh PreIdentifiers.SymbolTag g.tmp_universe in (fun _ -> { Types.fst = tmp; Types.snd = { tmp_universe = u; tmp_env = (List.Cons ({ Types.fst = tmp; Types.snd = ty }, g.tmp_env)) } })) __ (** val mklabels : labgen -> ((PreIdentifiers.identifier, PreIdentifiers.identifier) Types.prod, labgen) Types.prod **) let rec mklabels ul = let res1 = generate_fresh_label ul in (let { Types.fst = entry_label; Types.snd = ul1 } = res1 in (fun _ -> let res2 = generate_fresh_label ul1 in (let { Types.fst = exit_label; Types.snd = ul2 } = res2 in (fun _ -> { Types.fst = { Types.fst = entry_label; Types.snd = exit_label }; Types.snd = ul2 })) __)) __ type convert_flag = | DoNotConvert | ConvertTo of PreIdentifiers.identifier * PreIdentifiers.identifier (** val convert_flag_rect_Type4 : 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) -> convert_flag -> 'a1 **) let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function | DoNotConvert -> h_DoNotConvert | ConvertTo (x_14642, x_14641) -> h_ConvertTo x_14642 x_14641 (** val convert_flag_rect_Type5 : 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) -> convert_flag -> 'a1 **) let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function | DoNotConvert -> h_DoNotConvert | ConvertTo (x_14647, x_14646) -> h_ConvertTo x_14647 x_14646 (** val convert_flag_rect_Type3 : 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) -> convert_flag -> 'a1 **) let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function | DoNotConvert -> h_DoNotConvert | ConvertTo (x_14652, x_14651) -> h_ConvertTo x_14652 x_14651 (** val convert_flag_rect_Type2 : 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) -> convert_flag -> 'a1 **) let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function | DoNotConvert -> h_DoNotConvert | ConvertTo (x_14657, x_14656) -> h_ConvertTo x_14657 x_14656 (** val convert_flag_rect_Type1 : 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) -> convert_flag -> 'a1 **) let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function | DoNotConvert -> h_DoNotConvert | ConvertTo (x_14662, x_14661) -> h_ConvertTo x_14662 x_14661 (** val convert_flag_rect_Type0 : 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) -> convert_flag -> 'a1 **) let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function | DoNotConvert -> h_DoNotConvert | ConvertTo (x_14667, x_14666) -> h_ConvertTo x_14667 x_14666 (** val convert_flag_inv_rect_Type4 : convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **) let convert_flag_inv_rect_Type4 hterm h1 h2 = let hcut = convert_flag_rect_Type4 h1 h2 hterm in hcut __ (** val convert_flag_inv_rect_Type3 : convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **) let convert_flag_inv_rect_Type3 hterm h1 h2 = let hcut = convert_flag_rect_Type3 h1 h2 hterm in hcut __ (** val convert_flag_inv_rect_Type2 : convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **) let convert_flag_inv_rect_Type2 hterm h1 h2 = let hcut = convert_flag_rect_Type2 h1 h2 hterm in hcut __ (** val convert_flag_inv_rect_Type1 : convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **) let convert_flag_inv_rect_Type1 hterm h1 h2 = let hcut = convert_flag_rect_Type1 h1 h2 hterm in hcut __ (** val convert_flag_inv_rect_Type0 : convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **) let convert_flag_inv_rect_Type0 hterm h1 h2 = let hcut = convert_flag_rect_Type0 h1 h2 hterm in hcut __ (** val convert_flag_discr : convert_flag -> convert_flag -> __ **) let convert_flag_discr x y = Logic.eq_rect_Type2 x (match x with | DoNotConvert -> Obj.magic (fun _ dH -> dH) | ConvertTo (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y (** val convert_flag_jmdiscr : convert_flag -> convert_flag -> __ **) let convert_flag_jmdiscr x y = Logic.eq_rect_Type2 x (match x with | DoNotConvert -> Obj.magic (fun _ dH -> dH) | ConvertTo (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y (** val labels_of_flag : convert_flag -> PreIdentifiers.identifier List.list **) let rec labels_of_flag = function | DoNotConvert -> List.Nil | ConvertTo (continue, break) -> List.Cons (continue, (List.Cons (break, List.Nil))) (** val translate_statement : var_types -> tmpgen -> labgen -> lenv -> convert_flag -> AST.typ Types.option -> Csyntax.statement -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0 Errors.res **) let rec translate_statement vars uv ul lbls flag rettyp = function | Csyntax.Sskip -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; Types.snd = Cminor_syntax.St_skip } | Csyntax.Sassign (e1, e2) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e2)) (fun e2' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_dest vars e1)) (fun dest -> match dest with | IdDest id -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e2)) (Csyntax.typ_of_type (Csyntax.typeof e1)) e2')) (fun e2'0 -> Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; Types.snd = (Cminor_syntax.St_assign ((Csyntax.typ_of_type (Csyntax.typeof e1)), id, (Types.pi1 e2'0))) })) | MemDest e1' -> (match TypeComparison.type_eq_dec (Csyntax.typeof e1) (Csyntax.typeof e2) with | Types.Inl _ -> Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; Types.snd = (Cminor_syntax.St_store ((Csyntax.typ_of_type (Csyntax.typeof e2)), (Types.pi1 e1'), (Types.pi1 e2'))) }) | Types.Inr _ -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))))) | Csyntax.Scall (ret, ef, args) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars ef)) (fun ef' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof ef)) AST.ASTptr ef')) (fun ef'0 -> Monad.m_bind0 (Monad.max_def Errors.res0) (Errors.mmap_sigma (Obj.magic (translate_expr_sigma vars)) args) (fun args' -> match ret with | Types.None -> Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; Types.snd = (Cminor_syntax.St_call (Types.None, (Types.pi1 ef'0), (Types.pi1 args'))) }) | Types.Some e1 -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_dest vars e1)) (fun dest -> match dest with | IdDest id -> Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; Types.snd = (Cminor_syntax.St_call ((Types.Some { Types.fst = id; Types.snd = (Csyntax.typ_of_type (Csyntax.typeof e1)) }), (Types.pi1 ef'0), (Types.pi1 args'))) }) | MemDest e1' -> (let { Types.fst = tmp; Types.snd = uv1 } = alloc_tmp vars (Csyntax.typeof e1) uv in (fun _ -> (let { Types.fst = tmp2; Types.snd = uv2 } = alloc_tmp vars (Csyntax.Tpointer (Csyntax.typeof e1)) uv1 in (fun _ -> Obj.magic (Errors.OK { Types.fst = { Types.fst = uv2; Types.snd = ul }; Types.snd = (Cminor_syntax.St_seq ((Cminor_syntax.St_assign (AST.ASTptr, tmp2, (Types.pi1 e1'))), (Cminor_syntax.St_seq ((Cminor_syntax.St_call ((Types.Some { Types.fst = tmp; Types.snd = (Csyntax.typ_of_type (Csyntax.typeof e1)) }), (Types.pi1 ef'0), (Types.pi1 args'))), (Cminor_syntax.St_store ((Csyntax.typ_of_type (Csyntax.typeof e1)), (Cminor_syntax.Id (AST.ASTptr, tmp2)), (Cminor_syntax.Id ((Csyntax.typ_of_type (Csyntax.typeof e1)), tmp)))))))) }))) __)) __))))) | Csyntax.Ssequence (s1, s2) -> Obj.magic (Monad.m_sigbind2 (Monad.max_def Errors.res0) (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1)) (fun fgens1 s1' _ -> Monad.m_sigbind2 (Monad.max_def Errors.res0) (Obj.magic (translate_statement vars fgens1.Types.fst fgens1.Types.snd lbls flag rettyp s2)) (fun fgens2 s2' _ -> Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd = (Cminor_syntax.St_seq (s1', s2')) })))) | Csyntax.Sifthenelse (e1, s1, s2) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e1)) (fun e1' -> (match Csyntax.typ_of_type (Csyntax.typeof e1) with | AST.ASTint (x, x0) -> (fun e1'0 -> Monad.m_sigbind2 (Monad.max_def Errors.res0) (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1)) (fun fgens1 s1' _ -> Monad.m_sigbind2 (Monad.max_def Errors.res0) (Obj.magic (translate_statement vars fgens1.Types.fst fgens1.Types.snd lbls flag rettyp s2)) (fun fgens2 s2' _ -> Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd = (Cminor_syntax.St_ifthenelse (x, x0, (Types.pi1 e1'0), s1', s2')) })))) | AST.ASTptr -> (fun x -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))) e1')) | Csyntax.Swhile (e1, s1) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e1)) (fun e1' -> (match Csyntax.typ_of_type (Csyntax.typeof e1) with | AST.ASTint (x, x0) -> (fun e1'0 -> (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in (fun _ -> (let { Types.fst = entry; Types.snd = exit } = labels in (fun _ -> Monad.m_sigbind2 (Monad.max_def Errors.res0) (Obj.magic (translate_statement vars uv ul1 lbls (ConvertTo (entry, exit)) rettyp s1)) (fun fgens2 s1' _ -> let converted_loop = Cminor_syntax.St_label (entry, (Cminor_syntax.St_seq ((Cminor_syntax.St_ifthenelse (x, x0, (Types.pi1 e1'0), (Cminor_syntax.St_seq (s1', (Cminor_syntax.St_goto entry))), Cminor_syntax.St_skip)), (Cminor_syntax.St_label (exit, Cminor_syntax.St_skip))))) in Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd = converted_loop })))) __)) __) | AST.ASTptr -> (fun x -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))) e1')) | Csyntax.Sdowhile (e1, s1) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e1)) (fun e1' -> (match Csyntax.typ_of_type (Csyntax.typeof e1) with | AST.ASTint (x, x0) -> (fun e1'0 -> (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in (fun _ -> (let { Types.fst = condexpr; Types.snd = exit } = labels in (fun _ -> let { Types.fst = body; Types.snd = ul2 } = Types.pi1 (generate_fresh_label ul1) in Monad.m_sigbind2 (Monad.max_def Errors.res0) (Obj.magic (translate_statement vars uv ul2 lbls (ConvertTo (condexpr, exit)) rettyp s1)) (fun fgens2 s1' _ -> let converted_loop = Cminor_syntax.St_seq ((Cminor_syntax.St_seq ((Cminor_syntax.St_goto body), (Cminor_syntax.St_label (condexpr, (Cminor_syntax.St_ifthenelse (x, x0, (Types.pi1 e1'0), (Cminor_syntax.St_label (body, (Cminor_syntax.St_seq (s1', (Cminor_syntax.St_goto condexpr))))), Cminor_syntax.St_skip)))))), (Cminor_syntax.St_label (exit, Cminor_syntax.St_skip))) in Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd = converted_loop })))) __)) __) | AST.ASTptr -> (fun x -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))) e1')) | Csyntax.Sfor (s1, e1, s2, s3) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e1)) (fun e1' -> (match Csyntax.typ_of_type (Csyntax.typeof e1) with | AST.ASTint (x, x0) -> (fun e1'0 -> (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in (fun _ -> (let { Types.fst = continue; Types.snd = exit } = labels in (fun _ -> let { Types.fst = entry; Types.snd = ul2 } = Types.pi1 (generate_fresh_label ul1) in Monad.m_sigbind2 (Monad.max_def Errors.res0) (Obj.magic (translate_statement vars uv ul2 lbls flag rettyp s1)) (fun fgens2 s1' _ -> Monad.m_sigbind2 (Monad.max_def Errors.res0) (Obj.magic (translate_statement vars fgens2.Types.fst fgens2.Types.snd lbls flag rettyp s2)) (fun fgens3 s2' _ -> Monad.m_sigbind2 (Monad.max_def Errors.res0) (Obj.magic (translate_statement vars fgens3.Types.fst fgens3.Types.snd lbls (ConvertTo (continue, exit)) rettyp s3)) (fun fgens4 s3' _ -> let converted_loop = Cminor_syntax.St_seq (s1', (Cminor_syntax.St_label (entry, (Cminor_syntax.St_seq ((Cminor_syntax.St_ifthenelse (x, x0, (Types.pi1 e1'0), (Cminor_syntax.St_seq (s3', (Cminor_syntax.St_label (continue, (Cminor_syntax.St_seq (s2', (Cminor_syntax.St_goto entry))))))), Cminor_syntax.St_skip)), (Cminor_syntax.St_label (exit, Cminor_syntax.St_skip))))))) in Obj.magic (Errors.OK { Types.fst = fgens4; Types.snd = converted_loop })))))) __)) __) | AST.ASTptr -> (fun x -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))) e1')) | Csyntax.Sbreak -> (match flag with | DoNotConvert -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.FIXME)) | ConvertTo (continue_label, break_label) -> (fun _ -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; Types.snd = (Cminor_syntax.St_goto break_label) })) __ | Csyntax.Scontinue -> (match flag with | DoNotConvert -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.FIXME)) | ConvertTo (continue_label, break_label) -> (fun _ -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; Types.snd = (Cminor_syntax.St_goto continue_label) })) __ | Csyntax.Sreturn ret -> (match ret with | Types.None -> (match rettyp with | Types.None -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; Types.snd = (Cminor_syntax.St_return Types.None) } | Types.Some x -> Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)) | Types.Some e1 -> (match rettyp with | Types.None -> Errors.Error (Errors.msg ErrorMessages.ReturnMismatch) | Types.Some rty -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_expr vars e1)) (fun e1' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e1)) rty e1')) (fun e1'0 -> Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; Types.snd = (Cminor_syntax.St_return (Types.Some { Types.dpi1 = rty; Types.dpi2 = (Types.pi1 e1'0) })) })))))) | Csyntax.Sswitch (e1, ls) -> Errors.Error (Errors.msg ErrorMessages.FIXME) | Csyntax.Slabel (l, s1) -> Errors.bind_eq (lookup_label lbls l) (fun l' _ -> Obj.magic (Monad.m_sigbind2 (Monad.max_def Errors.res0) (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1)) (fun fgens1 s1' _ -> Obj.magic (Errors.OK { Types.fst = fgens1; Types.snd = (Cminor_syntax.St_label (l', s1')) })))) | Csyntax.Sgoto l -> Errors.bind_eq (lookup_label lbls l) (fun l' _ -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; Types.snd = (Cminor_syntax.St_goto l') }) | Csyntax.Scost (l, s1) -> Obj.magic (Monad.m_sigbind2 (Monad.max_def Errors.res0) (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1)) (fun fgens1 s1' _ -> Obj.magic (Errors.OK { Types.fst = fgens1; Types.snd = (Cminor_syntax.St_cost (l, s1')) }))) (** val alloc_params_main : var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag -> AST.typ Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0 -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0 Errors.res **) let alloc_params_main vars lbls statement uv ul rettyp params s = Util.foldl (fun su it -> let { Types.fst = id; Types.snd = ty } = it in Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su) (fun eta2378 -> let result = eta2378 in (let { Types.fst = fgens1; Types.snd = s0 } = result in (fun _ -> Obj.magic (Errors.bind2_eq (lookup' vars id) (fun t ty' _ -> (match t with | Global x -> (fun _ -> Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ParamGlobalMixup), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))) | Stack n -> (fun _ -> Errors.OK { Types.fst = fgens1; Types.snd = (Cminor_syntax.St_seq ((Cminor_syntax.St_store ((Csyntax.typ_of_type ty'), (Cminor_syntax.Cst (AST.ASTptr, (FrontEndOps.Oaddrstack n))), (Cminor_syntax.Id ((Csyntax.typ_of_type ty'), id)))), s0)) }) | Local -> (fun _ -> Errors.OK result)) __)))) __))) (Errors.OK s) params (** val alloc_params : var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag -> AST.typ Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0 -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0 Errors.res **) let alloc_params vars lbls statement uv ul rettyp params su = (let { Types.fst = tl; Types.snd = s0 } = Types.pi1 su in (match s0 with | Cminor_syntax.St_skip -> (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su) | Cminor_syntax.St_assign (x, x0, x1) -> (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su) | Cminor_syntax.St_store (x, x0, x1) -> (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su) | Cminor_syntax.St_call (x, x0, x1) -> (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su) | Cminor_syntax.St_seq (x, x0) -> (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su) | Cminor_syntax.St_ifthenelse (x, x0, x1, x2, x3) -> (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su) | Cminor_syntax.St_return x -> (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su) | Cminor_syntax.St_label (x, x0) -> (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su) | Cminor_syntax.St_goto x -> (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su) | Cminor_syntax.St_cost (cl, s') -> (fun _ -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (alloc_params_main vars lbls statement uv ul rettyp params { Types.fst = tl; Types.snd = s' })) (fun tls -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = (Types.pi1 tls).Types.fst; Types.snd = (Cminor_syntax.St_cost (cl, (Types.pi1 tls).Types.snd)) }))))) __ (** val populate_lenv : AST.ident List.list -> labgen -> lenv -> (lenv Types.sig0, labgen) Types.prod Errors.res **) let rec populate_lenv ls ul lbls = match ls with | List.Nil -> Errors.OK { Types.fst = lbls; Types.snd = ul } | List.Cons (l, t) -> (match lookup_label lbls l with | Errors.OK x -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.DuplicateLabel)) | Errors.Error x -> (fun _ -> let ret = generate_fresh_label ul in Obj.magic (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (populate_lenv t ret.Types.snd (Identifiers.add PreIdentifiers.SymbolTag lbls l ret.Types.fst))) (fun packed_lbls ul1 -> let lbls' = packed_lbls in Obj.magic (Errors.OK { Types.fst = lbls'; Types.snd = ul1 }))))) __ (** val build_label_env : Csyntax.statement -> (lenv Types.sig0, labgen) Types.prod Errors.res **) let build_label_env body = let initial_labgen = { labuniverse = (Identifiers.new_universe PreIdentifiers.Label); label_genlist = List.Nil } in Obj.magic (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (populate_lenv (labels_defined body) initial_labgen (Identifiers.empty_map PreIdentifiers.SymbolTag))) (fun label_map u -> let lbls = Types.pi1 label_map in Obj.magic (Errors.OK { Types.fst = lbls; Types.snd = u }))) (** val translate_function : Identifiers.universe -> ((AST.ident, AST.region) Types.prod, Csyntax.type0) Types.prod List.list -> Csyntax.function0 -> Cminor_syntax.internal_function Errors.res **) let translate_function tmpuniverse globals f = Obj.magic (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (build_label_env f.Csyntax.fn_body)) (fun env_pack ul -> let lbls = env_pack in (let { Types.fst = vartypes; Types.snd = stacksize } = characterise_vars globals f in (fun _ -> let uv = { tmp_universe = tmpuniverse; tmp_env = List.Nil } in Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_statement vartypes uv ul lbls DoNotConvert (Csyntax.opttyp_of_type f.Csyntax.fn_return) f.Csyntax.fn_body)) (fun s0 -> Monad.m_sigbind2 (Monad.max_def Errors.res0) (Obj.magic (alloc_params vartypes lbls f.Csyntax.fn_body uv DoNotConvert (Csyntax.opttyp_of_type f.Csyntax.fn_return) f.Csyntax.fn_params s0)) (fun fgens s1 _ -> let params = List.map (fun v -> { Types.fst = v.Types.fst; Types.snd = (Csyntax.typ_of_type v.Types.snd) }) f.Csyntax.fn_params in let vars = List.map (fun v -> { Types.fst = v.Types.fst; Types.snd = (Csyntax.typ_of_type v.Types.snd) }) (List.append fgens.Types.fst.tmp_env f.Csyntax.fn_vars) in Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Identifiers.check_distinct_env PreIdentifiers.SymbolTag (List.append params vars))) (fun _ -> Obj.magic (Errors.OK { Cminor_syntax.f_return = (Csyntax.opttyp_of_type f.Csyntax.fn_return); Cminor_syntax.f_params = params; Cminor_syntax.f_vars = vars; Cminor_syntax.f_stacksize = stacksize; Cminor_syntax.f_body = s1 })))))) __)) (** val translate_fundef : Identifiers.universe -> ((AST.ident, AST.region) Types.prod, Csyntax.type0) Types.prod List.list -> Csyntax.clight_fundef -> Cminor_syntax.internal_function AST.fundef Errors.res **) let translate_fundef tmpuniverse globals f = (match f with | Csyntax.CL_Internal fn -> (fun _ -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_function tmpuniverse globals fn)) (fun fn' -> Obj.magic (Errors.OK (AST.Internal fn'))))) | Csyntax.CL_External (fn, argtys, retty) -> (fun _ -> Errors.OK (AST.External { AST.ef_id = fn; AST.ef_sig = (Csyntax.signature_of_type argtys retty) }))) __ (** val map_partial_All : ('a1 -> __ -> 'a2 Errors.res) -> 'a1 List.list -> 'a2 List.list Errors.res **) let rec map_partial_All f l = (match l with | List.Nil -> (fun _ -> Errors.OK List.Nil) | List.Cons (hd, tl) -> (fun _ -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f hd __) (fun b_hd -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (map_partial_All f tl)) (fun b_tl -> Obj.magic (Errors.OK (List.Cons (b_hd, b_tl)))))))) __ (** val clight_to_cminor : Csyntax.clight_program -> Cminor_syntax.cminor_program Errors.res **) let clight_to_cminor p = let tmpuniverse = Fresh.universe_for_program p in let fun_globals = List.map (fun idf -> { Types.fst = { Types.fst = idf.Types.fst; Types.snd = AST.Code }; Types.snd = (Csyntax.type_of_fundef idf.Types.snd) }) p.AST.prog_funct in let var_globals = List.map (fun v -> { Types.fst = { Types.fst = v.Types.fst.Types.fst; Types.snd = v.Types.fst.Types.snd }; Types.snd = v.Types.snd.Types.snd }) p.AST.prog_vars in let globals = List.append fun_globals var_globals in Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (map_partial_All (fun x _ -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (translate_fundef tmpuniverse globals x.Types.snd)) (fun f -> Obj.magic (Errors.OK { Types.fst = x.Types.fst; Types.snd = f })))) p.AST.prog_funct)) (fun fns -> Obj.magic (Errors.OK { AST.prog_vars = (List.map (fun v -> { Types.fst = v.Types.fst; Types.snd = v.Types.snd.Types.fst }) p.AST.prog_vars); AST.prog_funct = fns; AST.prog_main = p.AST.prog_main })))