Changeset 2649 for extracted/toCminor.ml


Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/toCminor.ml

    r2601 r2649  
    33open CostLabel
    44
     5open Coqlib
     6
    57open Proper
    68
     
    911open Deqsets
    1012
     13open ErrorMessages
     14
    1115open PreIdentifiers
    1216
     
    2731open Identifiers
    2832
    29 open Coqlib
    30 
    31 open Floats
    32 
    3333open Arithmetic
    34 
    35 open Char
    36 
    37 open String
    3834
    3935open Vector
     
    8783| Csyntax.Expr (ed, ty) ->
    8884  (match ed with
    89    | Csyntax.Econst_int (x, x0) -> Identifiers.empty_set AST.symbolTag
    90    | Csyntax.Evar x -> Identifiers.empty_set AST.symbolTag
     85   | Csyntax.Econst_int (x, x0) ->
     86     Identifiers.empty_set PreIdentifiers.SymbolTag
     87   | Csyntax.Evar x -> Identifiers.empty_set PreIdentifiers.SymbolTag
    9188   | Csyntax.Ederef e1 -> gather_mem_vars_expr e1
    9289   | Csyntax.Eaddrof e1 -> gather_mem_vars_addr e1
    9390   | Csyntax.Eunop (x, e1) -> gather_mem_vars_expr e1
    9491   | Csyntax.Ebinop (x, e1, e2) ->
    95      Identifiers.union_set AST.symbolTag (gather_mem_vars_expr e1)
     92     Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
    9693       (gather_mem_vars_expr e2)
    9794   | Csyntax.Ecast (x, e1) -> gather_mem_vars_expr e1
    9895   | Csyntax.Econdition (e1, e2, e3) ->
    99      Identifiers.union_set AST.symbolTag
    100        (Identifiers.union_set AST.symbolTag (gather_mem_vars_expr e1)
    101          (gather_mem_vars_expr e2)) (gather_mem_vars_expr e3)
     96     Identifiers.union_set PreIdentifiers.SymbolTag
     97       (Identifiers.union_set PreIdentifiers.SymbolTag
     98         (gather_mem_vars_expr e1) (gather_mem_vars_expr e2))
     99       (gather_mem_vars_expr e3)
    102100   | Csyntax.Eandbool (e1, e2) ->
    103      Identifiers.union_set AST.symbolTag (gather_mem_vars_expr e1)
     101     Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
    104102       (gather_mem_vars_expr e2)
    105103   | Csyntax.Eorbool (e1, e2) ->
    106      Identifiers.union_set AST.symbolTag (gather_mem_vars_expr e1)
     104     Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
    107105       (gather_mem_vars_expr e2)
    108    | Csyntax.Esizeof x -> Identifiers.empty_set AST.symbolTag
     106   | Csyntax.Esizeof x -> Identifiers.empty_set PreIdentifiers.SymbolTag
    109107   | Csyntax.Efield (e1, x) -> gather_mem_vars_expr e1
    110108   | Csyntax.Ecost (x, e1) -> gather_mem_vars_expr e1)
     
    113111| Csyntax.Expr (ed, ty) ->
    114112  (match ed with
    115    | Csyntax.Econst_int (x, x0) -> Identifiers.empty_set AST.symbolTag
     113   | Csyntax.Econst_int (x, x0) ->
     114     Identifiers.empty_set PreIdentifiers.SymbolTag
    116115   | Csyntax.Evar x ->
    117      Identifiers.add_set AST.symbolTag (Identifiers.empty_set AST.symbolTag)
    118        x
     116     Identifiers.add_set PreIdentifiers.SymbolTag
     117       (Identifiers.empty_set PreIdentifiers.SymbolTag) x
    119118   | Csyntax.Ederef e1 -> gather_mem_vars_expr e1
    120    | Csyntax.Eaddrof x -> Identifiers.empty_set AST.symbolTag
    121    | Csyntax.Eunop (x, x0) -> Identifiers.empty_set AST.symbolTag
    122    | Csyntax.Ebinop (x, x0, x1) -> Identifiers.empty_set AST.symbolTag
    123    | Csyntax.Ecast (x, x0) -> Identifiers.empty_set AST.symbolTag
    124    | Csyntax.Econdition (x, x0, x1) -> Identifiers.empty_set AST.symbolTag
    125    | Csyntax.Eandbool (x, x0) -> Identifiers.empty_set AST.symbolTag
    126    | Csyntax.Eorbool (x, x0) -> Identifiers.empty_set AST.symbolTag
    127    | Csyntax.Esizeof x -> Identifiers.empty_set AST.symbolTag
     119   | Csyntax.Eaddrof x -> Identifiers.empty_set PreIdentifiers.SymbolTag
     120   | Csyntax.Eunop (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag
     121   | Csyntax.Ebinop (x, x0, x1) ->
     122     Identifiers.empty_set PreIdentifiers.SymbolTag
     123   | Csyntax.Ecast (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag
     124   | Csyntax.Econdition (x, x0, x1) ->
     125     Identifiers.empty_set PreIdentifiers.SymbolTag
     126   | Csyntax.Eandbool (x, x0) ->
     127     Identifiers.empty_set PreIdentifiers.SymbolTag
     128   | Csyntax.Eorbool (x, x0) ->
     129     Identifiers.empty_set PreIdentifiers.SymbolTag
     130   | Csyntax.Esizeof x -> Identifiers.empty_set PreIdentifiers.SymbolTag
    128131   | Csyntax.Efield (e1, x) -> gather_mem_vars_addr e1
    129    | Csyntax.Ecost (x, x0) -> Identifiers.empty_set AST.symbolTag)
     132   | Csyntax.Ecost (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag)
    130133
    131134(** val gather_mem_vars_stmt :
    132135    Csyntax.statement -> Identifiers.identifier_set **)
    133136let rec gather_mem_vars_stmt = function
    134 | Csyntax.Sskip -> Identifiers.empty_set AST.symbolTag
     137| Csyntax.Sskip -> Identifiers.empty_set PreIdentifiers.SymbolTag
    135138| Csyntax.Sassign (e1, e2) ->
    136   Identifiers.union_set AST.symbolTag (gather_mem_vars_expr e1)
     139  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
    137140    (gather_mem_vars_expr e2)
    138141| Csyntax.Scall (oe1, e2, es) ->
    139   Identifiers.union_set AST.symbolTag
    140     (Identifiers.union_set AST.symbolTag
     142  Identifiers.union_set PreIdentifiers.SymbolTag
     143    (Identifiers.union_set PreIdentifiers.SymbolTag
    141144      (match oe1 with
    142        | Types.None -> Identifiers.empty_set AST.symbolTag
     145       | Types.None -> Identifiers.empty_set PreIdentifiers.SymbolTag
    143146       | Types.Some e1 -> gather_mem_vars_expr e1) (gather_mem_vars_expr e2))
    144147    (Util.foldl (fun s0 e0 ->
    145       Identifiers.union_set AST.symbolTag s0 (gather_mem_vars_expr e0))
    146       (Identifiers.empty_set AST.symbolTag) es)
     148      Identifiers.union_set PreIdentifiers.SymbolTag s0
     149        (gather_mem_vars_expr e0))
     150      (Identifiers.empty_set PreIdentifiers.SymbolTag) es)
    147151| Csyntax.Ssequence (s1, s2) ->
    148   Identifiers.union_set AST.symbolTag (gather_mem_vars_stmt s1)
     152  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_stmt s1)
    149153    (gather_mem_vars_stmt s2)
    150154| Csyntax.Sifthenelse (e1, s1, s2) ->
    151   Identifiers.union_set AST.symbolTag
    152     (Identifiers.union_set AST.symbolTag (gather_mem_vars_expr e1)
     155  Identifiers.union_set PreIdentifiers.SymbolTag
     156    (Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
    153157      (gather_mem_vars_stmt s1)) (gather_mem_vars_stmt s2)
    154158| Csyntax.Swhile (e1, s1) ->
    155   Identifiers.union_set AST.symbolTag (gather_mem_vars_expr e1)
     159  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
    156160    (gather_mem_vars_stmt s1)
    157161| Csyntax.Sdowhile (e1, s1) ->
    158   Identifiers.union_set AST.symbolTag (gather_mem_vars_expr e1)
     162  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
    159163    (gather_mem_vars_stmt s1)
    160164| Csyntax.Sfor (s1, e1, s2, s3) ->
    161   Identifiers.union_set AST.symbolTag
    162     (Identifiers.union_set AST.symbolTag
    163       (Identifiers.union_set AST.symbolTag (gather_mem_vars_stmt s1)
    164         (gather_mem_vars_expr e1)) (gather_mem_vars_stmt s2))
    165     (gather_mem_vars_stmt s3)
    166 | Csyntax.Sbreak -> Identifiers.empty_set AST.symbolTag
    167 | Csyntax.Scontinue -> Identifiers.empty_set AST.symbolTag
     165  Identifiers.union_set PreIdentifiers.SymbolTag
     166    (Identifiers.union_set PreIdentifiers.SymbolTag
     167      (Identifiers.union_set PreIdentifiers.SymbolTag
     168        (gather_mem_vars_stmt s1) (gather_mem_vars_expr e1))
     169      (gather_mem_vars_stmt s2)) (gather_mem_vars_stmt s3)
     170| Csyntax.Sbreak -> Identifiers.empty_set PreIdentifiers.SymbolTag
     171| Csyntax.Scontinue -> Identifiers.empty_set PreIdentifiers.SymbolTag
    168172| Csyntax.Sreturn oe1 ->
    169173  (match oe1 with
    170    | Types.None -> Identifiers.empty_set AST.symbolTag
     174   | Types.None -> Identifiers.empty_set PreIdentifiers.SymbolTag
    171175   | Types.Some e1 -> gather_mem_vars_expr e1)
    172176| Csyntax.Sswitch (e1, ls) ->
    173   Identifiers.union_set AST.symbolTag (gather_mem_vars_expr e1)
     177  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
    174178    (gather_mem_vars_ls ls)
    175179| Csyntax.Slabel (x, s1) -> gather_mem_vars_stmt s1
    176 | Csyntax.Sgoto x -> Identifiers.empty_set AST.symbolTag
     180| Csyntax.Sgoto x -> Identifiers.empty_set PreIdentifiers.SymbolTag
    177181| Csyntax.Scost (x, s1) -> gather_mem_vars_stmt s1
    178182(** val gather_mem_vars_ls :
     
    181185| Csyntax.LSdefault s1 -> gather_mem_vars_stmt s1
    182186| Csyntax.LScase (x, x0, s1, ls1) ->
    183   Identifiers.union_set AST.symbolTag (gather_mem_vars_stmt s1)
     187  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_stmt s1)
    184188    (gather_mem_vars_ls ls1)
    185189
     
    192196    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    193197let rec var_type_rect_Type4 h_Global h_Stack h_Local = function
    194 | Global x_11976 -> h_Global x_11976
    195 | Stack x_11977 -> h_Stack x_11977
     198| Global x_11147 -> h_Global x_11147
     199| Stack x_11148 -> h_Stack x_11148
    196200| Local -> h_Local
    197201
     
    199203    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    200204let rec var_type_rect_Type5 h_Global h_Stack h_Local = function
    201 | Global x_11982 -> h_Global x_11982
    202 | Stack x_11983 -> h_Stack x_11983
     205| Global x_11153 -> h_Global x_11153
     206| Stack x_11154 -> h_Stack x_11154
    203207| Local -> h_Local
    204208
     
    206210    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    207211let rec var_type_rect_Type3 h_Global h_Stack h_Local = function
    208 | Global x_11988 -> h_Global x_11988
    209 | Stack x_11989 -> h_Stack x_11989
     212| Global x_11159 -> h_Global x_11159
     213| Stack x_11160 -> h_Stack x_11160
    210214| Local -> h_Local
    211215
     
    213217    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    214218let rec var_type_rect_Type2 h_Global h_Stack h_Local = function
    215 | Global x_11994 -> h_Global x_11994
    216 | Stack x_11995 -> h_Stack x_11995
     219| Global x_11165 -> h_Global x_11165
     220| Stack x_11166 -> h_Stack x_11166
    217221| Local -> h_Local
    218222
     
    220224    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    221225let rec var_type_rect_Type1 h_Global h_Stack h_Local = function
    222 | Global x_12000 -> h_Global x_12000
    223 | Stack x_12001 -> h_Stack x_12001
     226| Global x_11171 -> h_Global x_11171
     227| Stack x_11172 -> h_Stack x_11172
    224228| Local -> h_Local
    225229
     
    227231    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    228232let rec var_type_rect_Type0 h_Global h_Stack h_Local = function
    229 | Global x_12006 -> h_Global x_12006
    230 | Stack x_12007 -> h_Stack x_12007
     233| Global x_11177 -> h_Global x_11177
     234| Stack x_11178 -> h_Stack x_11178
    231235| Local -> h_Local
    232236
     
    280284  (var_type, Csyntax.type0) Types.prod Identifiers.identifier_map
    281285
    282 (** val undeclaredIdentifier : String.string **)
    283 let undeclaredIdentifier = "undeclared identifier"
    284   (*failwith "AXIOM TO BE REALIZED"*)
    285 
    286286(** val lookup' :
    287287    var_types -> PreIdentifiers.identifier -> (var_type, Csyntax.type0)
    288288    Types.prod Errors.res **)
    289289let lookup' vars id =
    290   Errors.opt_to_res (List.Cons ((Errors.MSG undeclaredIdentifier), (List.Cons
    291     ((Errors.CTX (AST.symbolTag, id)), List.Nil))))
    292     (Identifiers.lookup0 AST.symbolTag vars id)
     290  Errors.opt_to_res (List.Cons ((Errors.MSG
     291    ErrorMessages.UndeclaredIdentifier), (List.Cons ((Errors.CTX
     292    (PreIdentifiers.SymbolTag, id)), List.Nil))))
     293    (Identifiers.lookup0 PreIdentifiers.SymbolTag vars id)
    293294
    294295(** val always_alloc : Csyntax.type0 -> Bool.bool **)
     
    309310  let m =
    310311    List.foldr (fun idrt m ->
    311       Identifiers.add AST.symbolTag m idrt.Types.fst.Types.fst { Types.fst =
    312         (Global idrt.Types.fst.Types.snd); Types.snd = idrt.Types.snd })
    313       (Identifiers.empty_map AST.symbolTag) globals
     312      Identifiers.add PreIdentifiers.SymbolTag m idrt.Types.fst.Types.fst
     313        { Types.fst = (Global idrt.Types.fst.Types.snd); Types.snd =
     314        idrt.Types.snd }) (Identifiers.empty_map PreIdentifiers.SymbolTag)
     315      globals
    314316  in
    315317  let mem_vars = gather_mem_vars_stmt f.Csyntax.fn_body in
     
    320322      let { Types.fst = c; Types.snd = stack_high0 } =
    321323        match Bool.orb (always_alloc ty)
    322                 (Identifiers.member0 AST.symbolTag mem_vars id) with
     324                (Identifiers.member0 PreIdentifiers.SymbolTag mem_vars id) with
    323325        | Bool.True ->
    324326          { Types.fst = (Stack stack_high); Types.snd =
     
    327329      in
    328330      { Types.fst =
    329       (Identifiers.add AST.symbolTag m0 id { Types.fst = c; Types.snd = ty });
    330       Types.snd = stack_high0 }) { Types.fst = m; Types.snd = Nat.O }
    331       (List.append f.Csyntax.fn_params f.Csyntax.fn_vars)
     331      (Identifiers.add PreIdentifiers.SymbolTag m0 id { Types.fst = c;
     332        Types.snd = ty }); Types.snd = stack_high0 }) { Types.fst = m;
     333      Types.snd = Nat.O } (List.append f.Csyntax.fn_params f.Csyntax.fn_vars)
    332334  in
    333335  { Types.fst = m0; Types.snd = stacksize }
     
    356358
    357359open Cminor_syntax
    358 
    359 (** val badlyTypedAccess : String.string **)
    360 let badlyTypedAccess = "badly typed access"
    361   (*failwith "AXIOM TO BE REALIZED"*)
    362 
    363 (** val badLvalue : String.string **)
    364 let badLvalue = "bad lvalue"
    365   (*failwith "AXIOM TO BE REALIZED"*)
    366 
    367 (** val missingField : String.string **)
    368 let missingField = "missing field"
    369   (*failwith "AXIOM TO BE REALIZED"*)
    370360
    371361(** val type_should_eq :
     
    386376       | AST.XData -> (fun _ p -> Errors.OK p)
    387377       | AST.Code ->
    388          (fun _ p -> Errors.Error (Errors.msg TypeComparison.typeMismatch)))
     378         (fun _ p -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
    389379   | AST.Code ->
    390380     (fun clearme0 ->
    391381       match clearme0 with
    392382       | AST.XData ->
    393          (fun _ p -> Errors.Error (Errors.msg TypeComparison.typeMismatch))
     383         (fun _ p -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    394384       | AST.Code -> (fun _ p -> Errors.OK p))) r5 __ x
    395385
     
    398388  match AST.typ_eq ty1 ty2 with
    399389  | Types.Inl _ -> Errors.OK p
    400   | Types.Inr _ -> Errors.Error (Errors.msg TypeComparison.typeMismatch)
     390  | Types.Inr _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    401391
    402392(** val translate_unop :
     
    410400      | AST.ASTint (sz', sg') ->
    411401        Errors.OK (FrontEndOps.Onotbool ((AST.ASTint (sz, sg)), sz', sg'))
    412       | AST.ASTptr -> Errors.Error (Errors.msg TypeComparison.typeMismatch))
     402      | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    413403   | AST.ASTptr ->
    414404     (match t' with
    415405      | AST.ASTint (sz', sg') ->
    416406        Errors.OK (FrontEndOps.Onotbool (AST.ASTptr, sz', sg'))
    417       | AST.ASTptr -> Errors.Error (Errors.msg TypeComparison.typeMismatch)))
     407      | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
    418408| Csyntax.Onotint ->
    419409  (match t' with
    420410   | AST.ASTint (sz, sg) ->
    421411     typ_should_eq (AST.ASTint (sz, sg)) t (FrontEndOps.Onotint (sz, sg))
    422    | AST.ASTptr -> Errors.Error (Errors.msg TypeComparison.typeMismatch))
     412   | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    423413| Csyntax.Oneg ->
    424414  (match t' with
    425415   | AST.ASTint (sz, sg) ->
    426416     typ_should_eq (AST.ASTint (sz, sg)) t (FrontEndOps.Onegint (sz, sg))
    427    | AST.ASTptr -> Errors.Error (Errors.msg TypeComparison.typeMismatch))
     417   | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    428418
    429419(** val fix_ptr_type :
     
    472462         (fix_ptr_type ty n e2))))
    473463   | ClassifyOp.Add_default (x, x0) ->
    474      (fun e1 e2 -> Errors.Error (Errors.msg TypeComparison.typeMismatch)))
     464     (fun e1 e2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
    475465
    476466(** val translate_sub :
     
    504494       match ty' with
    505495       | Csyntax.Tvoid ->
    506          Errors.Error (Errors.msg TypeComparison.typeMismatch)
     496         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    507497       | Csyntax.Tint (sz, sg) ->
    508498         Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (AST.I32, AST.Unsigned)),
     
    518508           (AST.repr0 AST.I32 (Csyntax.sizeof ty10))))))))))
    519509       | Csyntax.Tpointer x ->
    520          Errors.Error (Errors.msg TypeComparison.typeMismatch)
     510         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    521511       | Csyntax.Tarray (x, x0) ->
    522          Errors.Error (Errors.msg TypeComparison.typeMismatch)
     512         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    523513       | Csyntax.Tfunction (x, x0) ->
    524          Errors.Error (Errors.msg TypeComparison.typeMismatch)
     514         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    525515       | Csyntax.Tstruct (x, x0) ->
    526          Errors.Error (Errors.msg TypeComparison.typeMismatch)
     516         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    527517       | Csyntax.Tunion (x, x0) ->
    528          Errors.Error (Errors.msg TypeComparison.typeMismatch)
     518         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    529519       | Csyntax.Tcomp_ptr x ->
    530          Errors.Error (Errors.msg TypeComparison.typeMismatch))
     520         Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    531521   | ClassifyOp.Sub_default (x, x0) ->
    532      (fun x1 x2 -> Errors.Error (Errors.msg TypeComparison.typeMismatch)))
     522     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
    533523
    534524(** val translate_mul :
     
    545535         (AST.ASTint (sz, sg)), (FrontEndOps.Omul (sz, sg)), e1, e2)))
    546536   | ClassifyOp.Aop_default (x, x0) ->
    547      (fun x1 x2 -> Errors.Error (Errors.msg TypeComparison.typeMismatch)))
     537     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
    548538
    549539(** val translate_div :
     
    569559            AST.Unsigned)), (FrontEndOps.Odivu sz), e1, e2))))
    570560   | ClassifyOp.Aop_default (x, x0) ->
    571      (fun x1 x2 -> Errors.Error (Errors.msg TypeComparison.typeMismatch)))
     561     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
    572562
    573563(** val translate_mod :
     
    593583            AST.Unsigned)), (FrontEndOps.Omodu sz), e1, e2))))
    594584   | ClassifyOp.Aop_default (x, x0) ->
    595      (fun x1 x2 -> Errors.Error (Errors.msg TypeComparison.typeMismatch)))
     585     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
    596586
    597587(** val translate_shr :
     
    617607            AST.Unsigned)), (FrontEndOps.Oshru (sz, AST.Unsigned)), e1, e2))))
    618608   | ClassifyOp.Aop_default (x, x0) ->
    619      (fun x1 x2 -> Errors.Error (Errors.msg TypeComparison.typeMismatch)))
     609     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
    620610
    621611(** val complete_cmp :
     
    623613let complete_cmp ty' e0 =
    624614  match ty' with
    625   | Csyntax.Tvoid -> Errors.Error (Errors.msg TypeComparison.typeMismatch)
     615  | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    626616  | Csyntax.Tint (sz, sg) ->
    627617    Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (AST.I8, AST.Unsigned)),
     
    629619      sg)), e0))
    630620  | Csyntax.Tpointer x ->
    631     Errors.Error (Errors.msg TypeComparison.typeMismatch)
     621    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    632622  | Csyntax.Tarray (x, x0) ->
    633     Errors.Error (Errors.msg TypeComparison.typeMismatch)
     623    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    634624  | Csyntax.Tfunction (x, x0) ->
    635     Errors.Error (Errors.msg TypeComparison.typeMismatch)
     625    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    636626  | Csyntax.Tstruct (x, x0) ->
    637     Errors.Error (Errors.msg TypeComparison.typeMismatch)
     627    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    638628  | Csyntax.Tunion (x, x0) ->
    639     Errors.Error (Errors.msg TypeComparison.typeMismatch)
     629    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    640630  | Csyntax.Tcomp_ptr x ->
    641     Errors.Error (Errors.msg TypeComparison.typeMismatch)
     631    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    642632
    643633(** val translate_cmp :
     
    668658         (AST.Unsigned, c)), (fix_ptr_type ty n e1), (fix_ptr_type ty n e2))))
    669659   | ClassifyOp.Cmp_default (x, x0) ->
    670      (fun x1 x2 -> Errors.Error (Errors.msg TypeComparison.typeMismatch)))
     660     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
    671661
    672662(** val translate_misc_aop :
     
    685675         sg)), (op0 sz sg), e1, e2)))
    686676   | ClassifyOp.Aop_default (x, x0) ->
    687      (fun x1 x2 -> Errors.Error (Errors.msg TypeComparison.typeMismatch)))
     677     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
    688678
    689679(** val translate_binop :
     
    719709   | Csyntax.Oge -> translate_cmp Integers.Cge ty1 ty2 ty e1 e2)
    720710
    721 (** val fIXME : String.string **)
    722 let fIXME = "fixme"
    723   (*failwith "AXIOM TO BE REALIZED"*)
    724 
    725711(** val translate_cast :
    726712    Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr Types.sig0 ->
     
    729715  match ty1 with
    730716  | Csyntax.Tvoid ->
    731     (fun x -> Errors.Error (Errors.msg TypeComparison.typeMismatch))
     717    (fun x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    732718  | Csyntax.Tint (sz1, sg1) ->
    733719    (fun e0 ->
    734720      match ty2 with
    735       | Csyntax.Tvoid ->
    736         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     721      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    737722      | Csyntax.Tint (sz2, sg2) ->
    738723        Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), (AST.ASTint
     
    746731          (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e0)))
    747732      | Csyntax.Tfunction (x, x0) ->
    748         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     733        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    749734      | Csyntax.Tstruct (x, x0) ->
    750         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     735        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    751736      | Csyntax.Tunion (x, x0) ->
    752         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     737        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    753738      | Csyntax.Tcomp_ptr x ->
    754         Errors.Error (Errors.msg TypeComparison.typeMismatch))
     739        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    755740  | Csyntax.Tpointer x ->
    756741    (fun e0 ->
    757742      match ty2 with
    758       | Csyntax.Tvoid ->
    759         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     743      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    760744      | Csyntax.Tint (sz2, sg2) ->
    761745        Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)),
     
    764748      | Csyntax.Tarray (x0, x1) -> Errors.OK e0
    765749      | Csyntax.Tfunction (x0, x1) ->
    766         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     750        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    767751      | Csyntax.Tstruct (x0, x1) ->
    768         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     752        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    769753      | Csyntax.Tunion (x0, x1) ->
    770         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     754        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    771755      | Csyntax.Tcomp_ptr x0 ->
    772         Errors.Error (Errors.msg TypeComparison.typeMismatch))
     756        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    773757  | Csyntax.Tarray (x, x0) ->
    774758    (fun e0 ->
    775759      match ty2 with
    776       | Csyntax.Tvoid ->
    777         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     760      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    778761      | Csyntax.Tint (sz2, sg2) ->
    779762        Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)),
     
    782765      | Csyntax.Tarray (x1, x2) -> Errors.OK e0
    783766      | Csyntax.Tfunction (x1, x2) ->
    784         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     767        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    785768      | Csyntax.Tstruct (x1, x2) ->
    786         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     769        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    787770      | Csyntax.Tunion (x1, x2) ->
    788         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     771        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    789772      | Csyntax.Tcomp_ptr x1 ->
    790         Errors.Error (Errors.msg TypeComparison.typeMismatch))
     773        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    791774  | Csyntax.Tfunction (x, x0) ->
    792     (fun x1 -> Errors.Error (Errors.msg TypeComparison.typeMismatch))
     775    (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    793776  | Csyntax.Tstruct (x, x0) ->
    794     (fun x1 -> Errors.Error (Errors.msg TypeComparison.typeMismatch))
     777    (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    795778  | Csyntax.Tunion (x, x0) ->
    796     (fun x1 -> Errors.Error (Errors.msg TypeComparison.typeMismatch))
     779    (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    797780  | Csyntax.Tcomp_ptr x ->
    798     (fun x0 -> Errors.Error (Errors.msg TypeComparison.typeMismatch))
     781    (fun x0 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    799782
    800783(** val cm_zero : AST.intsize -> AST.signedness -> Cminor_syntax.expr **)
     
    815798   | Csyntax.Econst_int (sz, i) ->
    816799     (match ty with
    817       | Csyntax.Tvoid ->
    818         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     800      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    819801      | Csyntax.Tint (sz', sg) ->
    820802        AST.intsize_eq_elim' sz sz' (Errors.OK (Cminor_syntax.Cst
    821803          ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg, i)))))
    822           (Errors.Error (Errors.msg TypeComparison.typeMismatch))
     804          (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    823805      | Csyntax.Tpointer x ->
    824         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     806        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    825807      | Csyntax.Tarray (x, x0) ->
    826         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     808        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    827809      | Csyntax.Tfunction (x, x0) ->
    828         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     810        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    829811      | Csyntax.Tstruct (x, x0) ->
    830         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     812        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    831813      | Csyntax.Tunion (x, x0) ->
    832         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     814        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    833815      | Csyntax.Tcomp_ptr x ->
    834         Errors.Error (Errors.msg TypeComparison.typeMismatch))
     816        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    835817   | Csyntax.Evar id ->
    836818     Errors.bind2_eq (lookup' vars id) (fun c t _ ->
     
    846828                (FrontEndOps.Oaddrsymbol (id, Nat.O))))
    847829            | Csyntax.By_nothing x ->
    848               Errors.Error (List.Cons ((Errors.MSG badlyTypedAccess),
    849                 (List.Cons ((Errors.CTX (AST.symbolTag, id)), List.Nil)))))
     830              Errors.Error (List.Cons ((Errors.MSG
     831                ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX
     832                (PreIdentifiers.SymbolTag, id)), List.Nil)))))
    850833        | Stack n ->
    851834          (fun _ ->
     
    858841                (FrontEndOps.Oaddrstack n)))
    859842            | Csyntax.By_nothing x ->
    860               Errors.Error (List.Cons ((Errors.MSG badlyTypedAccess),
    861                 (List.Cons ((Errors.CTX (AST.symbolTag, id)), List.Nil)))))
     843              Errors.Error (List.Cons ((Errors.MSG
     844                ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX
     845                (PreIdentifiers.SymbolTag, id)), List.Nil)))))
    862846        | Local ->
    863847          (fun _ ->
     
    872856            (fun x1 ->
    873857              Obj.magic (Errors.Error
    874                 (Errors.msg TypeComparison.typeMismatch)))
     858                (Errors.msg ErrorMessages.TypeMismatch)))
    875859          | AST.ASTptr ->
    876860            (fun e1'0 ->
     
    881865              | Csyntax.By_reference -> Obj.magic (Errors.OK e1'0)
    882866              | Csyntax.By_nothing x ->
    883                 Obj.magic (Errors.Error (Errors.msg badlyTypedAccess)))) e1'))
     867                Obj.magic (Errors.Error
     868                  (Errors.msg ErrorMessages.BadlyTypedAccess)))) e1'))
    884869   | Csyntax.Eaddrof e1 ->
    885870     Obj.magic
     
    888873         match Csyntax.typ_of_type ty with
    889874         | AST.ASTint (x, x0) ->
    890            Obj.magic (Errors.Error (Errors.msg TypeComparison.typeMismatch))
     875           Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    891876         | AST.ASTptr -> Obj.magic (Errors.OK e1')))
    892877   | Csyntax.Eunop (op0, e1) ->
     
    900885                | AST.I8 ->
    901886                  (fun _ -> Errors.Error
    902                     (Errors.msg TypeComparison.typeMismatch))
     887                    (Errors.msg ErrorMessages.TypeMismatch))
    903888                | AST.I16 ->
    904889                  (fun _ -> Errors.Error
    905                     (Errors.msg TypeComparison.typeMismatch))
     890                    (Errors.msg ErrorMessages.TypeMismatch))
    906891                | AST.I32 ->
    907892                  (fun _ ->
     
    919904                 __)
    920905           | AST.ASTptr ->
    921              (fun _ -> Errors.Error (Errors.msg TypeComparison.typeMismatch)))
     906             (fun _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
    922907            __)
    923908      | Csyntax.Onotint ->
     
    993978                    (fun x ->
    994979                      Obj.magic (Errors.Error
    995                         (Errors.msg TypeComparison.typeMismatch)))) e1'))))))
     980                        (Errors.msg ErrorMessages.TypeMismatch)))) e1'))))))
    996981   | Csyntax.Eandbool (e1, e2) ->
    997982     Obj.magic
     
    1002987           match ty with
    1003988           | Csyntax.Tvoid ->
    1004              Obj.magic (Errors.Error
    1005                (Errors.msg TypeComparison.typeMismatch))
     989             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    1006990           | Csyntax.Tint (sz, sg) ->
    1007991             Monad.m_bind0 (Monad.max_def Errors.res0)
     
    10201004                  (fun x ->
    10211005                    Obj.magic (Errors.Error
    1022                       (Errors.msg TypeComparison.typeMismatch)))) e1')
     1006                      (Errors.msg ErrorMessages.TypeMismatch)))) e1')
    10231007           | Csyntax.Tpointer x ->
    1024              Obj.magic (Errors.Error
    1025                (Errors.msg TypeComparison.typeMismatch))
     1008             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    10261009           | Csyntax.Tarray (x, x0) ->
    1027              Obj.magic (Errors.Error
    1028                (Errors.msg TypeComparison.typeMismatch))
     1010             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    10291011           | Csyntax.Tfunction (x, x0) ->
    1030              Obj.magic (Errors.Error
    1031                (Errors.msg TypeComparison.typeMismatch))
     1012             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    10321013           | Csyntax.Tstruct (x, x0) ->
    1033              Obj.magic (Errors.Error
    1034                (Errors.msg TypeComparison.typeMismatch))
     1014             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    10351015           | Csyntax.Tunion (x, x0) ->
    1036              Obj.magic (Errors.Error
    1037                (Errors.msg TypeComparison.typeMismatch))
     1016             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    10381017           | Csyntax.Tcomp_ptr x ->
    1039              Obj.magic (Errors.Error
    1040                (Errors.msg TypeComparison.typeMismatch)))))
     1018             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))))
    10411019   | Csyntax.Eorbool (e1, e2) ->
    10421020     Obj.magic
     
    10471025           match ty with
    10481026           | Csyntax.Tvoid ->
    1049              Obj.magic (Errors.Error
    1050                (Errors.msg TypeComparison.typeMismatch))
     1027             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    10511028           | Csyntax.Tint (sz, sg) ->
    10521029             Monad.m_bind0 (Monad.max_def Errors.res0)
     
    10651042                  (fun x ->
    10661043                    Obj.magic (Errors.Error
    1067                       (Errors.msg TypeComparison.typeMismatch)))) e1')
     1044                      (Errors.msg ErrorMessages.TypeMismatch)))) e1')
    10681045           | Csyntax.Tpointer x ->
    1069              Obj.magic (Errors.Error
    1070                (Errors.msg TypeComparison.typeMismatch))
     1046             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    10711047           | Csyntax.Tarray (x, x0) ->
    1072              Obj.magic (Errors.Error
    1073                (Errors.msg TypeComparison.typeMismatch))
     1048             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    10741049           | Csyntax.Tfunction (x, x0) ->
    1075              Obj.magic (Errors.Error
    1076                (Errors.msg TypeComparison.typeMismatch))
     1050             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    10771051           | Csyntax.Tstruct (x, x0) ->
    1078              Obj.magic (Errors.Error
    1079                (Errors.msg TypeComparison.typeMismatch))
     1052             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    10801053           | Csyntax.Tunion (x, x0) ->
    1081              Obj.magic (Errors.Error
    1082                (Errors.msg TypeComparison.typeMismatch))
     1054             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    10831055           | Csyntax.Tcomp_ptr x ->
    1084              Obj.magic (Errors.Error
    1085                (Errors.msg TypeComparison.typeMismatch)))))
     1056             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))))
    10861057   | Csyntax.Esizeof ty1 ->
    10871058     (match ty with
    1088       | Csyntax.Tvoid ->
    1089         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     1059      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    10901060      | Csyntax.Tint (sz, sg) ->
    10911061        Errors.OK (Cminor_syntax.Cst ((AST.ASTint (sz, sg)),
     
    10931063          (AST.repr0 sz (Csyntax.sizeof ty1))))))
    10941064      | Csyntax.Tpointer x ->
    1095         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     1065        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    10961066      | Csyntax.Tarray (x, x0) ->
    1097         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     1067        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    10981068      | Csyntax.Tfunction (x, x0) ->
    1099         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     1069        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    11001070      | Csyntax.Tstruct (x, x0) ->
    1101         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     1071        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    11021072      | Csyntax.Tunion (x, x0) ->
    1103         Errors.Error (Errors.msg TypeComparison.typeMismatch)
     1073        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    11041074      | Csyntax.Tcomp_ptr x ->
    1105         Errors.Error (Errors.msg TypeComparison.typeMismatch))
     1075        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    11061076   | Csyntax.Efield (e1, id) ->
    11071077     (match Csyntax.typeof e1 with
    1108       | Csyntax.Tvoid -> Errors.Error (Errors.msg badlyTypedAccess)
    1109       | Csyntax.Tint (x, x0) -> Errors.Error (Errors.msg badlyTypedAccess)
    1110       | Csyntax.Tpointer x -> Errors.Error (Errors.msg badlyTypedAccess)
    1111       | Csyntax.Tarray (x, x0) -> Errors.Error (Errors.msg badlyTypedAccess)
     1078      | Csyntax.Tvoid ->
     1079        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
     1080      | Csyntax.Tint (x, x0) ->
     1081        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
     1082      | Csyntax.Tpointer x ->
     1083        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
     1084      | Csyntax.Tarray (x, x0) ->
     1085        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
    11121086      | Csyntax.Tfunction (x, x0) ->
    1113         Errors.Error (Errors.msg badlyTypedAccess)
     1087        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
    11141088      | Csyntax.Tstruct (x, fl) ->
    11151089        Obj.magic
     
    11341108                  (AST.repr0 AST.I16 off))))))))
    11351109              | Csyntax.By_nothing x0 ->
    1136                 Obj.magic (Errors.Error (Errors.msg badlyTypedAccess)))))
     1110                Obj.magic (Errors.Error
     1111                  (Errors.msg ErrorMessages.BadlyTypedAccess)))))
    11371112      | Csyntax.Tunion (x, x0) ->
    11381113        Obj.magic
     
    11441119            | Csyntax.By_reference -> Obj.magic (Errors.OK e1')
    11451120            | Csyntax.By_nothing x1 ->
    1146               Obj.magic (Errors.Error (Errors.msg badlyTypedAccess))))
    1147       | Csyntax.Tcomp_ptr x -> Errors.Error (Errors.msg badlyTypedAccess))
     1121              Obj.magic (Errors.Error
     1122                (Errors.msg ErrorMessages.BadlyTypedAccess))))
     1123      | Csyntax.Tcomp_ptr x ->
     1124        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess))
    11481125   | Csyntax.Ecost (l, e1) ->
    11491126     Obj.magic
     
    11621139| Csyntax.Expr (ed, x) ->
    11631140  (match ed with
    1164    | Csyntax.Econst_int (x0, x1) -> Errors.Error (Errors.msg badLvalue)
     1141   | Csyntax.Econst_int (x0, x1) ->
     1142     Errors.Error (Errors.msg ErrorMessages.BadLvalue)
    11651143   | Csyntax.Evar id ->
    11661144     Obj.magic
     
    11751153             (FrontEndOps.Oaddrstack n))))
    11761154         | Local ->
    1177            Obj.magic (Errors.Error (List.Cons ((Errors.MSG badlyTypedAccess),
    1178              (List.Cons ((Errors.CTX (AST.symbolTag, id)), List.Nil)))))))
     1155           Obj.magic (Errors.Error (List.Cons ((Errors.MSG
     1156             ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX
     1157             (PreIdentifiers.SymbolTag, id)), List.Nil)))))))
    11791158   | Csyntax.Ederef e1 ->
    11801159     Obj.magic
     
    11841163          | AST.ASTint (x0, x1) ->
    11851164            (fun x2 ->
    1186               Obj.magic (Errors.Error (Errors.msg badlyTypedAccess)))
     1165              Obj.magic (Errors.Error
     1166                (Errors.msg ErrorMessages.BadlyTypedAccess)))
    11871167          | AST.ASTptr -> (fun e1'0 -> Obj.magic (Errors.OK e1'0))) e1'))
    1188    | Csyntax.Eaddrof x0 -> Errors.Error (Errors.msg badLvalue)
    1189    | Csyntax.Eunop (x0, x1) -> Errors.Error (Errors.msg badLvalue)
    1190    | Csyntax.Ebinop (x0, x1, x2) -> Errors.Error (Errors.msg badLvalue)
    1191    | Csyntax.Ecast (x0, x1) -> Errors.Error (Errors.msg badLvalue)
    1192    | Csyntax.Econdition (x0, x1, x2) -> Errors.Error (Errors.msg badLvalue)
    1193    | Csyntax.Eandbool (x0, x1) -> Errors.Error (Errors.msg badLvalue)
    1194    | Csyntax.Eorbool (x0, x1) -> Errors.Error (Errors.msg badLvalue)
    1195    | Csyntax.Esizeof x0 -> Errors.Error (Errors.msg badLvalue)
     1168   | Csyntax.Eaddrof x0 -> Errors.Error (Errors.msg ErrorMessages.BadLvalue)
     1169   | Csyntax.Eunop (x0, x1) ->
     1170     Errors.Error (Errors.msg ErrorMessages.BadLvalue)
     1171   | Csyntax.Ebinop (x0, x1, x2) ->
     1172     Errors.Error (Errors.msg ErrorMessages.BadLvalue)
     1173   | Csyntax.Ecast (x0, x1) ->
     1174     Errors.Error (Errors.msg ErrorMessages.BadLvalue)
     1175   | Csyntax.Econdition (x0, x1, x2) ->
     1176     Errors.Error (Errors.msg ErrorMessages.BadLvalue)
     1177   | Csyntax.Eandbool (x0, x1) ->
     1178     Errors.Error (Errors.msg ErrorMessages.BadLvalue)
     1179   | Csyntax.Eorbool (x0, x1) ->
     1180     Errors.Error (Errors.msg ErrorMessages.BadLvalue)
     1181   | Csyntax.Esizeof x0 -> Errors.Error (Errors.msg ErrorMessages.BadLvalue)
    11961182   | Csyntax.Efield (e1, id) ->
    11971183     (match Csyntax.typeof e1 with
    1198       | Csyntax.Tvoid -> Errors.Error (Errors.msg badlyTypedAccess)
    1199       | Csyntax.Tint (x0, x1) -> Errors.Error (Errors.msg badlyTypedAccess)
    1200       | Csyntax.Tpointer x0 -> Errors.Error (Errors.msg badlyTypedAccess)
    1201       | Csyntax.Tarray (x0, x1) -> Errors.Error (Errors.msg badlyTypedAccess)
     1184      | Csyntax.Tvoid ->
     1185        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
     1186      | Csyntax.Tint (x0, x1) ->
     1187        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
     1188      | Csyntax.Tpointer x0 ->
     1189        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
     1190      | Csyntax.Tarray (x0, x1) ->
     1191        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
    12021192      | Csyntax.Tfunction (x0, x1) ->
    1203         Errors.Error (Errors.msg badlyTypedAccess)
     1193        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
    12041194      | Csyntax.Tstruct (x0, fl) ->
    12051195        Obj.magic
     
    12151205                (AST.repr0 AST.I16 off)))))))))))
    12161206      | Csyntax.Tunion (x0, x1) -> translate_addr vars e1
    1217       | Csyntax.Tcomp_ptr x0 -> Errors.Error (Errors.msg badlyTypedAccess))
    1218    | Csyntax.Ecost (x0, x1) -> Errors.Error (Errors.msg badLvalue))
     1207      | Csyntax.Tcomp_ptr x0 ->
     1208        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess))
     1209   | Csyntax.Ecost (x0, x1) ->
     1210     Errors.Error (Errors.msg ErrorMessages.BadLvalue))
    12191211
    12201212type destination =
     
    12271219let rec destination_rect_Type4 vars h_IdDest h_MemDest = function
    12281220| IdDest (id, ty) -> h_IdDest id ty __
    1229 | MemDest x_13462 -> h_MemDest x_13462
     1221| MemDest x_11225 -> h_MemDest x_11225
    12301222
    12311223(** val destination_rect_Type5 :
     
    12341226let rec destination_rect_Type5 vars h_IdDest h_MemDest = function
    12351227| IdDest (id, ty) -> h_IdDest id ty __
    1236 | MemDest x_13467 -> h_MemDest x_13467
     1228| MemDest x_11230 -> h_MemDest x_11230
    12371229
    12381230(** val destination_rect_Type3 :
     
    12411233let rec destination_rect_Type3 vars h_IdDest h_MemDest = function
    12421234| IdDest (id, ty) -> h_IdDest id ty __
    1243 | MemDest x_13472 -> h_MemDest x_13472
     1235| MemDest x_11235 -> h_MemDest x_11235
    12441236
    12451237(** val destination_rect_Type2 :
     
    12481240let rec destination_rect_Type2 vars h_IdDest h_MemDest = function
    12491241| IdDest (id, ty) -> h_IdDest id ty __
    1250 | MemDest x_13477 -> h_MemDest x_13477
     1242| MemDest x_11240 -> h_MemDest x_11240
    12511243
    12521244(** val destination_rect_Type1 :
     
    12551247let rec destination_rect_Type1 vars h_IdDest h_MemDest = function
    12561248| IdDest (id, ty) -> h_IdDest id ty __
    1257 | MemDest x_13482 -> h_MemDest x_13482
     1249| MemDest x_11245 -> h_MemDest x_11245
    12581250
    12591251(** val destination_rect_Type0 :
     
    12621254let rec destination_rect_Type0 vars h_IdDest h_MemDest = function
    12631255| IdDest (id, ty) -> h_IdDest id ty __
    1264 | MemDest x_13487 -> h_MemDest x_13487
     1256| MemDest x_11250 -> h_MemDest x_11250
    12651257
    12661258(** val destination_inv_rect_Type4 :
     
    13751367type lenv = PreIdentifiers.identifier Identifiers.identifier_map
    13761368
    1377 (** val missingLabel : String.string **)
    1378 let missingLabel = "missing label"
    1379   (*failwith "AXIOM TO BE REALIZED"*)
    1380 
    13811369(** val lookup_label :
    13821370    lenv -> PreIdentifiers.identifier -> PreIdentifiers.identifier Errors.res **)
    13831371let lookup_label lbls l =
    1384   Errors.opt_to_res (List.Cons ((Errors.MSG missingLabel), (List.Cons
    1385     ((Errors.CTX (AST.symbolTag, l)), List.Nil))))
    1386     (Identifiers.lookup0 AST.symbolTag lbls l)
     1372  Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingLabel),
     1373    (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, l)), List.Nil))))
     1374    (Identifiers.lookup0 PreIdentifiers.SymbolTag lbls l)
    13871375
    13881376type fresh_list_for_univ = __
     
    13941382    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13951383    'a1) -> labgen -> 'a1 **)
    1396 let rec labgen_rect_Type4 h_mk_labgen x_13522 =
     1384let rec labgen_rect_Type4 h_mk_labgen x_11285 =
    13971385  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1398     x_13522
     1386    x_11285
    13991387  in
    14001388  h_mk_labgen labuniverse0 label_genlist0 __
     
    14031391    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14041392    'a1) -> labgen -> 'a1 **)
    1405 let rec labgen_rect_Type5 h_mk_labgen x_13524 =
     1393let rec labgen_rect_Type5 h_mk_labgen x_11287 =
    14061394  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1407     x_13524
     1395    x_11287
    14081396  in
    14091397  h_mk_labgen labuniverse0 label_genlist0 __
     
    14121400    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14131401    'a1) -> labgen -> 'a1 **)
    1414 let rec labgen_rect_Type3 h_mk_labgen x_13526 =
     1402let rec labgen_rect_Type3 h_mk_labgen x_11289 =
    14151403  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1416     x_13526
     1404    x_11289
    14171405  in
    14181406  h_mk_labgen labuniverse0 label_genlist0 __
     
    14211409    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14221410    'a1) -> labgen -> 'a1 **)
    1423 let rec labgen_rect_Type2 h_mk_labgen x_13528 =
     1411let rec labgen_rect_Type2 h_mk_labgen x_11291 =
    14241412  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1425     x_13528
     1413    x_11291
    14261414  in
    14271415  h_mk_labgen labuniverse0 label_genlist0 __
     
    14301418    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14311419    'a1) -> labgen -> 'a1 **)
    1432 let rec labgen_rect_Type1 h_mk_labgen x_13530 =
     1420let rec labgen_rect_Type1 h_mk_labgen x_11293 =
    14331421  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1434     x_13530
     1422    x_11293
    14351423  in
    14361424  h_mk_labgen labuniverse0 label_genlist0 __
     
    14391427    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14401428    'a1) -> labgen -> 'a1 **)
    1441 let rec labgen_rect_Type0 h_mk_labgen x_13532 =
     1429let rec labgen_rect_Type0 h_mk_labgen x_11295 =
    14421430  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1443     x_13532
     1431    x_11295
    14441432  in
    14451433  h_mk_labgen labuniverse0 label_genlist0 __
     
    14991487let generate_fresh_label ul =
    15001488  (let { Types.fst = tmp; Types.snd = u } =
    1501      Identifiers.fresh Cminor_syntax.label ul.labuniverse
     1489     Identifiers.fresh PreIdentifiers.Label ul.labuniverse
    15021490   in
    15031491  (fun _ -> { Types.fst = tmp; Types.snd = { labuniverse = u; label_genlist =
     
    15571545let add_tmps vs tmpenv =
    15581546  List.foldr (fun idty vs0 ->
    1559     Identifiers.add AST.symbolTag vs0 idty.Types.fst { Types.fst = Local;
    1560       Types.snd = idty.Types.snd }) vs tmpenv
     1547    Identifiers.add PreIdentifiers.SymbolTag vs0 idty.Types.fst { Types.fst =
     1548      Local; Types.snd = idty.Types.snd }) vs tmpenv
    15611549
    15621550type tmpgen = { tmp_universe : Identifiers.universe;
     
    15661554    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15671555    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1568 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_13548 =
    1569   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_13548 in
     1556let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_11311 =
     1557  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11311 in
    15701558  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15711559
     
    15731561    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15741562    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1575 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_13550 =
    1576   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_13550 in
     1563let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_11313 =
     1564  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11313 in
    15771565  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15781566
     
    15801568    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15811569    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1582 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_13552 =
    1583   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_13552 in
     1570let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_11315 =
     1571  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11315 in
    15841572  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15851573
     
    15871575    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15881576    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1589 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_13554 =
    1590   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_13554 in
     1577let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_11317 =
     1578  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11317 in
    15911579  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15921580
     
    15941582    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15951583    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1596 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_13556 =
    1597   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_13556 in
     1584let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_11319 =
     1585  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11319 in
    15981586  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15991587
     
    16011589    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    16021590    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1603 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_13558 =
    1604   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_13558 in
     1591let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_11321 =
     1592  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11321 in
    16051593  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    16061594
     
    16601648let alloc_tmp vars ty g0 =
    16611649  (let { Types.fst = tmp; Types.snd = u } =
    1662      Identifiers.fresh AST.symbolTag g0.tmp_universe
     1650     Identifiers.fresh PreIdentifiers.SymbolTag g0.tmp_universe
    16631651   in
    16641652  (fun _ -> { Types.fst = tmp; Types.snd = { tmp_universe = u; tmp_env =
     
    16861674let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function
    16871675| DoNotConvert -> h_DoNotConvert
    1688 | ConvertTo (x_13580, x_13579) -> h_ConvertTo x_13580 x_13579
     1676| ConvertTo (x_11343, x_11342) -> h_ConvertTo x_11343 x_11342
    16891677
    16901678(** val convert_flag_rect_Type5 :
     
    16931681let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function
    16941682| DoNotConvert -> h_DoNotConvert
    1695 | ConvertTo (x_13585, x_13584) -> h_ConvertTo x_13585 x_13584
     1683| ConvertTo (x_11348, x_11347) -> h_ConvertTo x_11348 x_11347
    16961684
    16971685(** val convert_flag_rect_Type3 :
     
    17001688let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function
    17011689| DoNotConvert -> h_DoNotConvert
    1702 | ConvertTo (x_13590, x_13589) -> h_ConvertTo x_13590 x_13589
     1690| ConvertTo (x_11353, x_11352) -> h_ConvertTo x_11353 x_11352
    17031691
    17041692(** val convert_flag_rect_Type2 :
     
    17071695let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function
    17081696| DoNotConvert -> h_DoNotConvert
    1709 | ConvertTo (x_13595, x_13594) -> h_ConvertTo x_13595 x_13594
     1697| ConvertTo (x_11358, x_11357) -> h_ConvertTo x_11358 x_11357
    17101698
    17111699(** val convert_flag_rect_Type1 :
     
    17141702let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function
    17151703| DoNotConvert -> h_DoNotConvert
    1716 | ConvertTo (x_13600, x_13599) -> h_ConvertTo x_13600 x_13599
     1704| ConvertTo (x_11363, x_11362) -> h_ConvertTo x_11363 x_11362
    17171705
    17181706(** val convert_flag_rect_Type0 :
     
    17211709let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function
    17221710| DoNotConvert -> h_DoNotConvert
    1723 | ConvertTo (x_13605, x_13604) -> h_ConvertTo x_13605 x_13604
     1711| ConvertTo (x_11368, x_11367) -> h_ConvertTo x_11368 x_11367
    17241712
    17251713(** val convert_flag_inv_rect_Type4 :
     
    17731761| ConvertTo (continue, break) ->
    17741762  List.Cons (continue, (List.Cons (break, List.Nil)))
    1775 
    1776 (** val returnMismatch : String.string **)
    1777 let returnMismatch = "return mismatch"
    1778   (*failwith "AXIOM TO BE REALIZED"*)
    17791763
    17801764(** val translate_statement :
     
    18771861       | AST.ASTptr ->
    18781862         (fun x ->
    1879            Obj.magic (Errors.Error (Errors.msg TypeComparison.typeMismatch))))
     1863           Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
    18801864        e1'))
    18811865| Csyntax.Swhile (e1, s1) ->
     
    19041888       | AST.ASTptr ->
    19051889         (fun x ->
    1906            Obj.magic (Errors.Error (Errors.msg TypeComparison.typeMismatch))))
     1890           Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
    19071891        e1'))
    19081892| Csyntax.Sdowhile (e1, s1) ->
     
    19361920       | AST.ASTptr ->
    19371921         (fun x ->
    1938            Obj.magic (Errors.Error (Errors.msg TypeComparison.typeMismatch))))
     1922           Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
    19391923        e1'))
    19401924| Csyntax.Sfor (s1, e1, s2, s3) ->
     
    19781962       | AST.ASTptr ->
    19791963         (fun x ->
    1980            Obj.magic (Errors.Error (Errors.msg TypeComparison.typeMismatch))))
     1964           Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
    19811965        e1'))
    19821966| Csyntax.Sbreak ->
    19831967  (match flag with
    1984    | DoNotConvert -> (fun _ -> Errors.Error (Errors.msg fIXME))
     1968   | DoNotConvert -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.FIXME))
    19851969   | ConvertTo (continue_label, break_label) ->
    19861970     (fun _ -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul };
     
    19881972| Csyntax.Scontinue ->
    19891973  (match flag with
    1990    | DoNotConvert -> (fun _ -> Errors.Error (Errors.msg fIXME))
     1974   | DoNotConvert -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.FIXME))
    19911975   | ConvertTo (continue_label, break_label) ->
    19921976     (fun _ -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul };
     
    19991983        Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul };
    20001984          Types.snd = (Cminor_syntax.St_return Types.None) }
    2001       | Types.Some x -> Errors.Error (Errors.msg returnMismatch))
     1985      | Types.Some x ->
     1986        Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))
    20021987   | Types.Some e1 ->
    20031988     (match rettyp with
    2004       | Types.None -> Errors.Error (Errors.msg returnMismatch)
     1989      | Types.None -> Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
    20051990      | Types.Some rty ->
    20061991        Obj.magic
     
    20152000                (Types.Some { Types.dpi1 = rty; Types.dpi2 =
    20162001                (Types.pi1 e1'0) })) }))))))
    2017 | Csyntax.Sswitch (e1, ls) -> Errors.Error (Errors.msg fIXME)
     2002| Csyntax.Sswitch (e1, ls) -> Errors.Error (Errors.msg ErrorMessages.FIXME)
    20182003| Csyntax.Slabel (l, s1) ->
    20192004  Errors.bind_eq (lookup_label lbls l) (fun l' _ ->
     
    20362021        (Cminor_syntax.St_cost (l, s1')) })))
    20372022
    2038 (** val paramGlobalMixup : String.string **)
    2039 let paramGlobalMixup = "param global mixup"
    2040   (*failwith "AXIOM TO BE REALIZED"*)
    2041 
    20422023(** val alloc_params :
    20432024    var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag ->
     
    20512032    Obj.magic
    20522033      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
    2053         (fun eta2362 ->
    2054         let result = eta2362 in
     2034        (fun eta1273 ->
     2035        let result = eta1273 in
    20552036        (let { Types.fst = fgens1; Types.snd = s0 } = result in
    20562037        (fun _ ->
     
    20602041             | Global x ->
    20612042               (fun _ -> Errors.Error (List.Cons ((Errors.MSG
    2062                  paramGlobalMixup), (List.Cons ((Errors.CTX (AST.symbolTag,
    2063                  id)), List.Nil)))))
     2043                 ErrorMessages.ParamGlobalMixup), (List.Cons ((Errors.CTX
     2044                 (PreIdentifiers.SymbolTag, id)), List.Nil)))))
    20642045             | Stack n ->
    20652046               (fun _ -> Errors.OK { Types.fst = fgens1; Types.snd =
     
    20712052    s) params
    20722053
    2073 (** val duplicateLabel : String.string **)
    2074 let duplicateLabel = "duplicate label"
    2075   (*failwith "AXIOM TO BE REALIZED"*)
    2076 
    20772054(** val populate_lenv :
    20782055    AST.ident List.list -> labgen -> lenv -> (lenv Types.sig0, labgen)
     
    20832060  | List.Cons (l, t) ->
    20842061    (match lookup_label lbls l with
    2085      | Errors.OK x -> (fun _ -> Errors.Error (Errors.msg duplicateLabel))
     2062     | Errors.OK x ->
     2063       (fun _ -> Errors.Error (Errors.msg ErrorMessages.DuplicateLabel))
    20862064     | Errors.Error x ->
    20872065       (fun _ ->
     
    20912069             (Obj.magic
    20922070               (populate_lenv t ret.Types.snd
    2093                  (Identifiers.add AST.symbolTag lbls l ret.Types.fst)))
    2094              (fun packed_lbls ul1 ->
     2071                 (Identifiers.add PreIdentifiers.SymbolTag lbls l
     2072                   ret.Types.fst))) (fun packed_lbls ul1 ->
    20952073             let lbls' = packed_lbls in
    20962074             Obj.magic (Errors.OK { Types.fst = lbls'; Types.snd = ul1 })))))
     
    21012079let build_label_env body =
    21022080  let initial_labgen = { labuniverse =
    2103     (Identifiers.new_universe Cminor_syntax.label); label_genlist =
     2081    (Identifiers.new_universe PreIdentifiers.Label); label_genlist =
    21042082    List.Nil }
    21052083  in
     
    21082086      (Obj.magic
    21092087        (populate_lenv (labels_defined body) initial_labgen
    2110           (Identifiers.empty_map AST.symbolTag))) (fun label_map u ->
     2088          (Identifiers.empty_map PreIdentifiers.SymbolTag)))
     2089      (fun label_map u ->
    21112090      let lbls = Types.pi1 label_map in
    21122091      Obj.magic (Errors.OK { Types.fst = lbls; Types.snd = u })))
     
    21472126          Monad.m_bind0 (Monad.max_def Errors.res0)
    21482127            (Obj.magic
    2149               (Identifiers.check_distinct_env AST.symbolTag
     2128              (Identifiers.check_distinct_env PreIdentifiers.SymbolTag
    21502129                (List.append params vars))) (fun _ ->
    21512130            Obj.magic (Errors.OK { Cminor_syntax.f_return =
Note: See TracChangeset for help on using the changeset viewer.