Changeset 2649 for extracted/toCminor.ml
 Timestamp:
 Feb 7, 2013, 10:43:49 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/toCminor.ml
r2601 r2649 3 3 open CostLabel 4 4 5 open Coqlib 6 5 7 open Proper 6 8 … … 9 11 open Deqsets 10 12 13 open ErrorMessages 14 11 15 open PreIdentifiers 12 16 … … 27 31 open Identifiers 28 32 29 open Coqlib30 31 open Floats32 33 33 open Arithmetic 34 35 open Char36 37 open String38 34 39 35 open Vector … … 87 83  Csyntax.Expr (ed, ty) > 88 84 (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 91 88  Csyntax.Ederef e1 > gather_mem_vars_expr e1 92 89  Csyntax.Eaddrof e1 > gather_mem_vars_addr e1 93 90  Csyntax.Eunop (x, e1) > gather_mem_vars_expr e1 94 91  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) 96 93 (gather_mem_vars_expr e2) 97 94  Csyntax.Ecast (x, e1) > gather_mem_vars_expr e1 98 95  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) 102 100  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) 104 102 (gather_mem_vars_expr e2) 105 103  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) 107 105 (gather_mem_vars_expr e2) 108  Csyntax.Esizeof x > Identifiers.empty_set AST.symbolTag106  Csyntax.Esizeof x > Identifiers.empty_set PreIdentifiers.SymbolTag 109 107  Csyntax.Efield (e1, x) > gather_mem_vars_expr e1 110 108  Csyntax.Ecost (x, e1) > gather_mem_vars_expr e1) … … 113 111  Csyntax.Expr (ed, ty) > 114 112 (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 116 115  Csyntax.Evar x > 117 Identifiers.add_set AST.symbolTag (Identifiers.empty_set AST.symbolTag)118 x116 Identifiers.add_set PreIdentifiers.SymbolTag 117 (Identifiers.empty_set PreIdentifiers.SymbolTag) x 119 118  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 128 131  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) 130 133 131 134 (** val gather_mem_vars_stmt : 132 135 Csyntax.statement > Identifiers.identifier_set **) 133 136 let rec gather_mem_vars_stmt = function 134  Csyntax.Sskip > Identifiers.empty_set AST.symbolTag137  Csyntax.Sskip > Identifiers.empty_set PreIdentifiers.SymbolTag 135 138  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) 137 140 (gather_mem_vars_expr e2) 138 141  Csyntax.Scall (oe1, e2, es) > 139 Identifiers.union_set AST.symbolTag140 (Identifiers.union_set AST.symbolTag142 Identifiers.union_set PreIdentifiers.SymbolTag 143 (Identifiers.union_set PreIdentifiers.SymbolTag 141 144 (match oe1 with 142  Types.None > Identifiers.empty_set AST.symbolTag145  Types.None > Identifiers.empty_set PreIdentifiers.SymbolTag 143 146  Types.Some e1 > gather_mem_vars_expr e1) (gather_mem_vars_expr e2)) 144 147 (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) 147 151  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) 149 153 (gather_mem_vars_stmt s2) 150 154  Csyntax.Sifthenelse (e1, s1, s2) > 151 Identifiers.union_set AST.symbolTag152 (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) 153 157 (gather_mem_vars_stmt s1)) (gather_mem_vars_stmt s2) 154 158  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) 156 160 (gather_mem_vars_stmt s1) 157 161  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) 159 163 (gather_mem_vars_stmt s1) 160 164  Csyntax.Sfor (s1, e1, s2, s3) > 161 Identifiers.union_set AST.symbolTag162 (Identifiers.union_set AST.symbolTag163 (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.symbolTag167  Csyntax.Scontinue > Identifiers.empty_set AST.symbolTag165 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 168 172  Csyntax.Sreturn oe1 > 169 173 (match oe1 with 170  Types.None > Identifiers.empty_set AST.symbolTag174  Types.None > Identifiers.empty_set PreIdentifiers.SymbolTag 171 175  Types.Some e1 > gather_mem_vars_expr e1) 172 176  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) 174 178 (gather_mem_vars_ls ls) 175 179  Csyntax.Slabel (x, s1) > gather_mem_vars_stmt s1 176  Csyntax.Sgoto x > Identifiers.empty_set AST.symbolTag180  Csyntax.Sgoto x > Identifiers.empty_set PreIdentifiers.SymbolTag 177 181  Csyntax.Scost (x, s1) > gather_mem_vars_stmt s1 178 182 (** val gather_mem_vars_ls : … … 181 185  Csyntax.LSdefault s1 > gather_mem_vars_stmt s1 182 186  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) 184 188 (gather_mem_vars_ls ls1) 185 189 … … 192 196 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 193 197 let rec var_type_rect_Type4 h_Global h_Stack h_Local = function 194  Global x_11 976 > h_Global x_11976195  Stack x_11 977 > h_Stack x_11977198  Global x_11147 > h_Global x_11147 199  Stack x_11148 > h_Stack x_11148 196 200  Local > h_Local 197 201 … … 199 203 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 200 204 let rec var_type_rect_Type5 h_Global h_Stack h_Local = function 201  Global x_11 982 > h_Global x_11982202  Stack x_11 983 > h_Stack x_11983205  Global x_11153 > h_Global x_11153 206  Stack x_11154 > h_Stack x_11154 203 207  Local > h_Local 204 208 … … 206 210 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 207 211 let rec var_type_rect_Type3 h_Global h_Stack h_Local = function 208  Global x_11 988 > h_Global x_11988209  Stack x_11 989 > h_Stack x_11989212  Global x_11159 > h_Global x_11159 213  Stack x_11160 > h_Stack x_11160 210 214  Local > h_Local 211 215 … … 213 217 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 214 218 let rec var_type_rect_Type2 h_Global h_Stack h_Local = function 215  Global x_11 994 > h_Global x_11994216  Stack x_11 995 > h_Stack x_11995219  Global x_11165 > h_Global x_11165 220  Stack x_11166 > h_Stack x_11166 217 221  Local > h_Local 218 222 … … 220 224 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 221 225 let rec var_type_rect_Type1 h_Global h_Stack h_Local = function 222  Global x_1 2000 > h_Global x_12000223  Stack x_1 2001 > h_Stack x_12001226  Global x_11171 > h_Global x_11171 227  Stack x_11172 > h_Stack x_11172 224 228  Local > h_Local 225 229 … … 227 231 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 228 232 let rec var_type_rect_Type0 h_Global h_Stack h_Local = function 229  Global x_1 2006 > h_Global x_12006230  Stack x_1 2007 > h_Stack x_12007233  Global x_11177 > h_Global x_11177 234  Stack x_11178 > h_Stack x_11178 231 235  Local > h_Local 232 236 … … 280 284 (var_type, Csyntax.type0) Types.prod Identifiers.identifier_map 281 285 282 (** val undeclaredIdentifier : String.string **)283 let undeclaredIdentifier = "undeclared identifier"284 (*failwith "AXIOM TO BE REALIZED"*)285 286 286 (** val lookup' : 287 287 var_types > PreIdentifiers.identifier > (var_type, Csyntax.type0) 288 288 Types.prod Errors.res **) 289 289 let 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) 293 294 294 295 (** val always_alloc : Csyntax.type0 > Bool.bool **) … … 309 310 let m = 310 311 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 314 316 in 315 317 let mem_vars = gather_mem_vars_stmt f.Csyntax.fn_body in … … 320 322 let { Types.fst = c; Types.snd = stack_high0 } = 321 323 match Bool.orb (always_alloc ty) 322 (Identifiers.member0 AST.symbolTag mem_vars id) with324 (Identifiers.member0 PreIdentifiers.SymbolTag mem_vars id) with 323 325  Bool.True > 324 326 { Types.fst = (Stack stack_high); Types.snd = … … 327 329 in 328 330 { 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) 332 334 in 333 335 { Types.fst = m0; Types.snd = stacksize } … … 356 358 357 359 open 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"*)370 360 371 361 (** val type_should_eq : … … 386 376  AST.XData > (fun _ p > Errors.OK p) 387 377  AST.Code > 388 (fun _ p > Errors.Error (Errors.msg TypeComparison.typeMismatch)))378 (fun _ p > Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) 389 379  AST.Code > 390 380 (fun clearme0 > 391 381 match clearme0 with 392 382  AST.XData > 393 (fun _ p > Errors.Error (Errors.msg TypeComparison.typeMismatch))383 (fun _ p > Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 394 384  AST.Code > (fun _ p > Errors.OK p))) r5 __ x 395 385 … … 398 388 match AST.typ_eq ty1 ty2 with 399 389  Types.Inl _ > Errors.OK p 400  Types.Inr _ > Errors.Error (Errors.msg TypeComparison.typeMismatch)390  Types.Inr _ > Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 401 391 402 392 (** val translate_unop : … … 410 400  AST.ASTint (sz', sg') > 411 401 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)) 413 403  AST.ASTptr > 414 404 (match t' with 415 405  AST.ASTint (sz', sg') > 416 406 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))) 418 408  Csyntax.Onotint > 419 409 (match t' with 420 410  AST.ASTint (sz, sg) > 421 411 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)) 423 413  Csyntax.Oneg > 424 414 (match t' with 425 415  AST.ASTint (sz, sg) > 426 416 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)) 428 418 429 419 (** val fix_ptr_type : … … 472 462 (fix_ptr_type ty n e2)))) 473 463  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))) 475 465 476 466 (** val translate_sub : … … 504 494 match ty' with 505 495  Csyntax.Tvoid > 506 Errors.Error (Errors.msg TypeComparison.typeMismatch)496 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 507 497  Csyntax.Tint (sz, sg) > 508 498 Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (AST.I32, AST.Unsigned)), … … 518 508 (AST.repr0 AST.I32 (Csyntax.sizeof ty10)))))))))) 519 509  Csyntax.Tpointer x > 520 Errors.Error (Errors.msg TypeComparison.typeMismatch)510 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 521 511  Csyntax.Tarray (x, x0) > 522 Errors.Error (Errors.msg TypeComparison.typeMismatch)512 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 523 513  Csyntax.Tfunction (x, x0) > 524 Errors.Error (Errors.msg TypeComparison.typeMismatch)514 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 525 515  Csyntax.Tstruct (x, x0) > 526 Errors.Error (Errors.msg TypeComparison.typeMismatch)516 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 527 517  Csyntax.Tunion (x, x0) > 528 Errors.Error (Errors.msg TypeComparison.typeMismatch)518 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 529 519  Csyntax.Tcomp_ptr x > 530 Errors.Error (Errors.msg TypeComparison.typeMismatch))520 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 531 521  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))) 533 523 534 524 (** val translate_mul : … … 545 535 (AST.ASTint (sz, sg)), (FrontEndOps.Omul (sz, sg)), e1, e2))) 546 536  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))) 548 538 549 539 (** val translate_div : … … 569 559 AST.Unsigned)), (FrontEndOps.Odivu sz), e1, e2)))) 570 560  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))) 572 562 573 563 (** val translate_mod : … … 593 583 AST.Unsigned)), (FrontEndOps.Omodu sz), e1, e2)))) 594 584  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))) 596 586 597 587 (** val translate_shr : … … 617 607 AST.Unsigned)), (FrontEndOps.Oshru (sz, AST.Unsigned)), e1, e2)))) 618 608  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))) 620 610 621 611 (** val complete_cmp : … … 623 613 let complete_cmp ty' e0 = 624 614 match ty' with 625  Csyntax.Tvoid > Errors.Error (Errors.msg TypeComparison.typeMismatch)615  Csyntax.Tvoid > Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 626 616  Csyntax.Tint (sz, sg) > 627 617 Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (AST.I8, AST.Unsigned)), … … 629 619 sg)), e0)) 630 620  Csyntax.Tpointer x > 631 Errors.Error (Errors.msg TypeComparison.typeMismatch)621 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 632 622  Csyntax.Tarray (x, x0) > 633 Errors.Error (Errors.msg TypeComparison.typeMismatch)623 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 634 624  Csyntax.Tfunction (x, x0) > 635 Errors.Error (Errors.msg TypeComparison.typeMismatch)625 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 636 626  Csyntax.Tstruct (x, x0) > 637 Errors.Error (Errors.msg TypeComparison.typeMismatch)627 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 638 628  Csyntax.Tunion (x, x0) > 639 Errors.Error (Errors.msg TypeComparison.typeMismatch)629 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 640 630  Csyntax.Tcomp_ptr x > 641 Errors.Error (Errors.msg TypeComparison.typeMismatch)631 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 642 632 643 633 (** val translate_cmp : … … 668 658 (AST.Unsigned, c)), (fix_ptr_type ty n e1), (fix_ptr_type ty n e2)))) 669 659  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))) 671 661 672 662 (** val translate_misc_aop : … … 685 675 sg)), (op0 sz sg), e1, e2))) 686 676  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))) 688 678 689 679 (** val translate_binop : … … 719 709  Csyntax.Oge > translate_cmp Integers.Cge ty1 ty2 ty e1 e2) 720 710 721 (** val fIXME : String.string **)722 let fIXME = "fixme"723 (*failwith "AXIOM TO BE REALIZED"*)724 725 711 (** val translate_cast : 726 712 Csyntax.type0 > Csyntax.type0 > Cminor_syntax.expr Types.sig0 > … … 729 715 match ty1 with 730 716  Csyntax.Tvoid > 731 (fun x > Errors.Error (Errors.msg TypeComparison.typeMismatch))717 (fun x > Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 732 718  Csyntax.Tint (sz1, sg1) > 733 719 (fun e0 > 734 720 match ty2 with 735  Csyntax.Tvoid > 736 Errors.Error (Errors.msg TypeComparison.typeMismatch) 721  Csyntax.Tvoid > Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 737 722  Csyntax.Tint (sz2, sg2) > 738 723 Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), (AST.ASTint … … 746 731 (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e0))) 747 732  Csyntax.Tfunction (x, x0) > 748 Errors.Error (Errors.msg TypeComparison.typeMismatch)733 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 749 734  Csyntax.Tstruct (x, x0) > 750 Errors.Error (Errors.msg TypeComparison.typeMismatch)735 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 751 736  Csyntax.Tunion (x, x0) > 752 Errors.Error (Errors.msg TypeComparison.typeMismatch)737 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 753 738  Csyntax.Tcomp_ptr x > 754 Errors.Error (Errors.msg TypeComparison.typeMismatch))739 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 755 740  Csyntax.Tpointer x > 756 741 (fun e0 > 757 742 match ty2 with 758  Csyntax.Tvoid > 759 Errors.Error (Errors.msg TypeComparison.typeMismatch) 743  Csyntax.Tvoid > Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 760 744  Csyntax.Tint (sz2, sg2) > 761 745 Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)), … … 764 748  Csyntax.Tarray (x0, x1) > Errors.OK e0 765 749  Csyntax.Tfunction (x0, x1) > 766 Errors.Error (Errors.msg TypeComparison.typeMismatch)750 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 767 751  Csyntax.Tstruct (x0, x1) > 768 Errors.Error (Errors.msg TypeComparison.typeMismatch)752 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 769 753  Csyntax.Tunion (x0, x1) > 770 Errors.Error (Errors.msg TypeComparison.typeMismatch)754 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 771 755  Csyntax.Tcomp_ptr x0 > 772 Errors.Error (Errors.msg TypeComparison.typeMismatch))756 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 773 757  Csyntax.Tarray (x, x0) > 774 758 (fun e0 > 775 759 match ty2 with 776  Csyntax.Tvoid > 777 Errors.Error (Errors.msg TypeComparison.typeMismatch) 760  Csyntax.Tvoid > Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 778 761  Csyntax.Tint (sz2, sg2) > 779 762 Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)), … … 782 765  Csyntax.Tarray (x1, x2) > Errors.OK e0 783 766  Csyntax.Tfunction (x1, x2) > 784 Errors.Error (Errors.msg TypeComparison.typeMismatch)767 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 785 768  Csyntax.Tstruct (x1, x2) > 786 Errors.Error (Errors.msg TypeComparison.typeMismatch)769 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 787 770  Csyntax.Tunion (x1, x2) > 788 Errors.Error (Errors.msg TypeComparison.typeMismatch)771 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 789 772  Csyntax.Tcomp_ptr x1 > 790 Errors.Error (Errors.msg TypeComparison.typeMismatch))773 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 791 774  Csyntax.Tfunction (x, x0) > 792 (fun x1 > Errors.Error (Errors.msg TypeComparison.typeMismatch))775 (fun x1 > Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 793 776  Csyntax.Tstruct (x, x0) > 794 (fun x1 > Errors.Error (Errors.msg TypeComparison.typeMismatch))777 (fun x1 > Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 795 778  Csyntax.Tunion (x, x0) > 796 (fun x1 > Errors.Error (Errors.msg TypeComparison.typeMismatch))779 (fun x1 > Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 797 780  Csyntax.Tcomp_ptr x > 798 (fun x0 > Errors.Error (Errors.msg TypeComparison.typeMismatch))781 (fun x0 > Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 799 782 800 783 (** val cm_zero : AST.intsize > AST.signedness > Cminor_syntax.expr **) … … 815 798  Csyntax.Econst_int (sz, i) > 816 799 (match ty with 817  Csyntax.Tvoid > 818 Errors.Error (Errors.msg TypeComparison.typeMismatch) 800  Csyntax.Tvoid > Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 819 801  Csyntax.Tint (sz', sg) > 820 802 AST.intsize_eq_elim' sz sz' (Errors.OK (Cminor_syntax.Cst 821 803 ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg, i))))) 822 (Errors.Error (Errors.msg TypeComparison.typeMismatch))804 (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 823 805  Csyntax.Tpointer x > 824 Errors.Error (Errors.msg TypeComparison.typeMismatch)806 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 825 807  Csyntax.Tarray (x, x0) > 826 Errors.Error (Errors.msg TypeComparison.typeMismatch)808 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 827 809  Csyntax.Tfunction (x, x0) > 828 Errors.Error (Errors.msg TypeComparison.typeMismatch)810 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 829 811  Csyntax.Tstruct (x, x0) > 830 Errors.Error (Errors.msg TypeComparison.typeMismatch)812 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 831 813  Csyntax.Tunion (x, x0) > 832 Errors.Error (Errors.msg TypeComparison.typeMismatch)814 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 833 815  Csyntax.Tcomp_ptr x > 834 Errors.Error (Errors.msg TypeComparison.typeMismatch))816 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 835 817  Csyntax.Evar id > 836 818 Errors.bind2_eq (lookup' vars id) (fun c t _ > … … 846 828 (FrontEndOps.Oaddrsymbol (id, Nat.O)))) 847 829  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))))) 850 833  Stack n > 851 834 (fun _ > … … 858 841 (FrontEndOps.Oaddrstack n))) 859 842  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))))) 862 846  Local > 863 847 (fun _ > … … 872 856 (fun x1 > 873 857 Obj.magic (Errors.Error 874 (Errors.msg TypeComparison.typeMismatch)))858 (Errors.msg ErrorMessages.TypeMismatch))) 875 859  AST.ASTptr > 876 860 (fun e1'0 > … … 881 865  Csyntax.By_reference > Obj.magic (Errors.OK e1'0) 882 866  Csyntax.By_nothing x > 883 Obj.magic (Errors.Error (Errors.msg badlyTypedAccess)))) e1')) 867 Obj.magic (Errors.Error 868 (Errors.msg ErrorMessages.BadlyTypedAccess)))) e1')) 884 869  Csyntax.Eaddrof e1 > 885 870 Obj.magic … … 888 873 match Csyntax.typ_of_type ty with 889 874  AST.ASTint (x, x0) > 890 Obj.magic (Errors.Error (Errors.msg TypeComparison.typeMismatch))875 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 891 876  AST.ASTptr > Obj.magic (Errors.OK e1'))) 892 877  Csyntax.Eunop (op0, e1) > … … 900 885  AST.I8 > 901 886 (fun _ > Errors.Error 902 (Errors.msg TypeComparison.typeMismatch))887 (Errors.msg ErrorMessages.TypeMismatch)) 903 888  AST.I16 > 904 889 (fun _ > Errors.Error 905 (Errors.msg TypeComparison.typeMismatch))890 (Errors.msg ErrorMessages.TypeMismatch)) 906 891  AST.I32 > 907 892 (fun _ > … … 919 904 __) 920 905  AST.ASTptr > 921 (fun _ > Errors.Error (Errors.msg TypeComparison.typeMismatch)))906 (fun _ > Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) 922 907 __) 923 908  Csyntax.Onotint > … … 993 978 (fun x > 994 979 Obj.magic (Errors.Error 995 (Errors.msg TypeComparison.typeMismatch)))) e1'))))))980 (Errors.msg ErrorMessages.TypeMismatch)))) e1')))))) 996 981  Csyntax.Eandbool (e1, e2) > 997 982 Obj.magic … … 1002 987 match ty with 1003 988  Csyntax.Tvoid > 1004 Obj.magic (Errors.Error 1005 (Errors.msg TypeComparison.typeMismatch)) 989 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 1006 990  Csyntax.Tint (sz, sg) > 1007 991 Monad.m_bind0 (Monad.max_def Errors.res0) … … 1020 1004 (fun x > 1021 1005 Obj.magic (Errors.Error 1022 (Errors.msg TypeComparison.typeMismatch)))) e1')1006 (Errors.msg ErrorMessages.TypeMismatch)))) e1') 1023 1007  Csyntax.Tpointer x > 1024 Obj.magic (Errors.Error 1025 (Errors.msg TypeComparison.typeMismatch)) 1008 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 1026 1009  Csyntax.Tarray (x, x0) > 1027 Obj.magic (Errors.Error 1028 (Errors.msg TypeComparison.typeMismatch)) 1010 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 1029 1011  Csyntax.Tfunction (x, x0) > 1030 Obj.magic (Errors.Error 1031 (Errors.msg TypeComparison.typeMismatch)) 1012 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 1032 1013  Csyntax.Tstruct (x, x0) > 1033 Obj.magic (Errors.Error 1034 (Errors.msg TypeComparison.typeMismatch)) 1014 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 1035 1015  Csyntax.Tunion (x, x0) > 1036 Obj.magic (Errors.Error 1037 (Errors.msg TypeComparison.typeMismatch)) 1016 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 1038 1017  Csyntax.Tcomp_ptr x > 1039 Obj.magic (Errors.Error 1040 (Errors.msg TypeComparison.typeMismatch))))) 1018 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))) 1041 1019  Csyntax.Eorbool (e1, e2) > 1042 1020 Obj.magic … … 1047 1025 match ty with 1048 1026  Csyntax.Tvoid > 1049 Obj.magic (Errors.Error 1050 (Errors.msg TypeComparison.typeMismatch)) 1027 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 1051 1028  Csyntax.Tint (sz, sg) > 1052 1029 Monad.m_bind0 (Monad.max_def Errors.res0) … … 1065 1042 (fun x > 1066 1043 Obj.magic (Errors.Error 1067 (Errors.msg TypeComparison.typeMismatch)))) e1')1044 (Errors.msg ErrorMessages.TypeMismatch)))) e1') 1068 1045  Csyntax.Tpointer x > 1069 Obj.magic (Errors.Error 1070 (Errors.msg TypeComparison.typeMismatch)) 1046 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 1071 1047  Csyntax.Tarray (x, x0) > 1072 Obj.magic (Errors.Error 1073 (Errors.msg TypeComparison.typeMismatch)) 1048 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 1074 1049  Csyntax.Tfunction (x, x0) > 1075 Obj.magic (Errors.Error 1076 (Errors.msg TypeComparison.typeMismatch)) 1050 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 1077 1051  Csyntax.Tstruct (x, x0) > 1078 Obj.magic (Errors.Error 1079 (Errors.msg TypeComparison.typeMismatch)) 1052 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 1080 1053  Csyntax.Tunion (x, x0) > 1081 Obj.magic (Errors.Error 1082 (Errors.msg TypeComparison.typeMismatch)) 1054 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 1083 1055  Csyntax.Tcomp_ptr x > 1084 Obj.magic (Errors.Error 1085 (Errors.msg TypeComparison.typeMismatch))))) 1056 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))) 1086 1057  Csyntax.Esizeof ty1 > 1087 1058 (match ty with 1088  Csyntax.Tvoid > 1089 Errors.Error (Errors.msg TypeComparison.typeMismatch) 1059  Csyntax.Tvoid > Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 1090 1060  Csyntax.Tint (sz, sg) > 1091 1061 Errors.OK (Cminor_syntax.Cst ((AST.ASTint (sz, sg)), … … 1093 1063 (AST.repr0 sz (Csyntax.sizeof ty1)))))) 1094 1064  Csyntax.Tpointer x > 1095 Errors.Error (Errors.msg TypeComparison.typeMismatch)1065 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 1096 1066  Csyntax.Tarray (x, x0) > 1097 Errors.Error (Errors.msg TypeComparison.typeMismatch)1067 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 1098 1068  Csyntax.Tfunction (x, x0) > 1099 Errors.Error (Errors.msg TypeComparison.typeMismatch)1069 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 1100 1070  Csyntax.Tstruct (x, x0) > 1101 Errors.Error (Errors.msg TypeComparison.typeMismatch)1071 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 1102 1072  Csyntax.Tunion (x, x0) > 1103 Errors.Error (Errors.msg TypeComparison.typeMismatch)1073 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 1104 1074  Csyntax.Tcomp_ptr x > 1105 Errors.Error (Errors.msg TypeComparison.typeMismatch))1075 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 1106 1076  Csyntax.Efield (e1, id) > 1107 1077 (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) 1112 1086  Csyntax.Tfunction (x, x0) > 1113 Errors.Error (Errors.msg badlyTypedAccess)1087 Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) 1114 1088  Csyntax.Tstruct (x, fl) > 1115 1089 Obj.magic … … 1134 1108 (AST.repr0 AST.I16 off)))))))) 1135 1109  Csyntax.By_nothing x0 > 1136 Obj.magic (Errors.Error (Errors.msg badlyTypedAccess))))) 1110 Obj.magic (Errors.Error 1111 (Errors.msg ErrorMessages.BadlyTypedAccess))))) 1137 1112  Csyntax.Tunion (x, x0) > 1138 1113 Obj.magic … … 1144 1119  Csyntax.By_reference > Obj.magic (Errors.OK e1') 1145 1120  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)) 1148 1125  Csyntax.Ecost (l, e1) > 1149 1126 Obj.magic … … 1162 1139  Csyntax.Expr (ed, x) > 1163 1140 (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) 1165 1143  Csyntax.Evar id > 1166 1144 Obj.magic … … 1175 1153 (FrontEndOps.Oaddrstack n)))) 1176 1154  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))))))) 1179 1158  Csyntax.Ederef e1 > 1180 1159 Obj.magic … … 1184 1163  AST.ASTint (x0, x1) > 1185 1164 (fun x2 > 1186 Obj.magic (Errors.Error (Errors.msg badlyTypedAccess))) 1165 Obj.magic (Errors.Error 1166 (Errors.msg ErrorMessages.BadlyTypedAccess))) 1187 1167  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) 1196 1182  Csyntax.Efield (e1, id) > 1197 1183 (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) 1202 1192  Csyntax.Tfunction (x0, x1) > 1203 Errors.Error (Errors.msg badlyTypedAccess)1193 Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) 1204 1194  Csyntax.Tstruct (x0, fl) > 1205 1195 Obj.magic … … 1215 1205 (AST.repr0 AST.I16 off))))))))))) 1216 1206  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)) 1219 1211 1220 1212 type destination = … … 1227 1219 let rec destination_rect_Type4 vars h_IdDest h_MemDest = function 1228 1220  IdDest (id, ty) > h_IdDest id ty __ 1229  MemDest x_1 3462 > h_MemDest x_134621221  MemDest x_11225 > h_MemDest x_11225 1230 1222 1231 1223 (** val destination_rect_Type5 : … … 1234 1226 let rec destination_rect_Type5 vars h_IdDest h_MemDest = function 1235 1227  IdDest (id, ty) > h_IdDest id ty __ 1236  MemDest x_1 3467 > h_MemDest x_134671228  MemDest x_11230 > h_MemDest x_11230 1237 1229 1238 1230 (** val destination_rect_Type3 : … … 1241 1233 let rec destination_rect_Type3 vars h_IdDest h_MemDest = function 1242 1234  IdDest (id, ty) > h_IdDest id ty __ 1243  MemDest x_1 3472 > h_MemDest x_134721235  MemDest x_11235 > h_MemDest x_11235 1244 1236 1245 1237 (** val destination_rect_Type2 : … … 1248 1240 let rec destination_rect_Type2 vars h_IdDest h_MemDest = function 1249 1241  IdDest (id, ty) > h_IdDest id ty __ 1250  MemDest x_1 3477 > h_MemDest x_134771242  MemDest x_11240 > h_MemDest x_11240 1251 1243 1252 1244 (** val destination_rect_Type1 : … … 1255 1247 let rec destination_rect_Type1 vars h_IdDest h_MemDest = function 1256 1248  IdDest (id, ty) > h_IdDest id ty __ 1257  MemDest x_1 3482 > h_MemDest x_134821249  MemDest x_11245 > h_MemDest x_11245 1258 1250 1259 1251 (** val destination_rect_Type0 : … … 1262 1254 let rec destination_rect_Type0 vars h_IdDest h_MemDest = function 1263 1255  IdDest (id, ty) > h_IdDest id ty __ 1264  MemDest x_1 3487 > h_MemDest x_134871256  MemDest x_11250 > h_MemDest x_11250 1265 1257 1266 1258 (** val destination_inv_rect_Type4 : … … 1375 1367 type lenv = PreIdentifiers.identifier Identifiers.identifier_map 1376 1368 1377 (** val missingLabel : String.string **)1378 let missingLabel = "missing label"1379 (*failwith "AXIOM TO BE REALIZED"*)1380 1381 1369 (** val lookup_label : 1382 1370 lenv > PreIdentifiers.identifier > PreIdentifiers.identifier Errors.res **) 1383 1371 let lookup_label lbls l = 1384 Errors.opt_to_res (List.Cons ((Errors.MSG missingLabel), (List.Cons1385 ( (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) 1387 1375 1388 1376 type fresh_list_for_univ = __ … … 1394 1382 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1395 1383 'a1) > labgen > 'a1 **) 1396 let rec labgen_rect_Type4 h_mk_labgen x_1 3522=1384 let rec labgen_rect_Type4 h_mk_labgen x_11285 = 1397 1385 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1398 x_1 35221386 x_11285 1399 1387 in 1400 1388 h_mk_labgen labuniverse0 label_genlist0 __ … … 1403 1391 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1404 1392 'a1) > labgen > 'a1 **) 1405 let rec labgen_rect_Type5 h_mk_labgen x_1 3524=1393 let rec labgen_rect_Type5 h_mk_labgen x_11287 = 1406 1394 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1407 x_1 35241395 x_11287 1408 1396 in 1409 1397 h_mk_labgen labuniverse0 label_genlist0 __ … … 1412 1400 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1413 1401 'a1) > labgen > 'a1 **) 1414 let rec labgen_rect_Type3 h_mk_labgen x_1 3526=1402 let rec labgen_rect_Type3 h_mk_labgen x_11289 = 1415 1403 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1416 x_1 35261404 x_11289 1417 1405 in 1418 1406 h_mk_labgen labuniverse0 label_genlist0 __ … … 1421 1409 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1422 1410 'a1) > labgen > 'a1 **) 1423 let rec labgen_rect_Type2 h_mk_labgen x_1 3528=1411 let rec labgen_rect_Type2 h_mk_labgen x_11291 = 1424 1412 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1425 x_1 35281413 x_11291 1426 1414 in 1427 1415 h_mk_labgen labuniverse0 label_genlist0 __ … … 1430 1418 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1431 1419 'a1) > labgen > 'a1 **) 1432 let rec labgen_rect_Type1 h_mk_labgen x_1 3530=1420 let rec labgen_rect_Type1 h_mk_labgen x_11293 = 1433 1421 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1434 x_1 35301422 x_11293 1435 1423 in 1436 1424 h_mk_labgen labuniverse0 label_genlist0 __ … … 1439 1427 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1440 1428 'a1) > labgen > 'a1 **) 1441 let rec labgen_rect_Type0 h_mk_labgen x_1 3532=1429 let rec labgen_rect_Type0 h_mk_labgen x_11295 = 1442 1430 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1443 x_1 35321431 x_11295 1444 1432 in 1445 1433 h_mk_labgen labuniverse0 label_genlist0 __ … … 1499 1487 let generate_fresh_label ul = 1500 1488 (let { Types.fst = tmp; Types.snd = u } = 1501 Identifiers.fresh Cminor_syntax.label ul.labuniverse1489 Identifiers.fresh PreIdentifiers.Label ul.labuniverse 1502 1490 in 1503 1491 (fun _ > { Types.fst = tmp; Types.snd = { labuniverse = u; label_genlist = … … 1557 1545 let add_tmps vs tmpenv = 1558 1546 List.foldr (fun idty vs0 > 1559 Identifiers.add AST.symbolTag vs0 idty.Types.fst { Types.fst = Local;1560 Types.snd = idty.Types.snd }) vs tmpenv1547 Identifiers.add PreIdentifiers.SymbolTag vs0 idty.Types.fst { Types.fst = 1548 Local; Types.snd = idty.Types.snd }) vs tmpenv 1561 1549 1562 1550 type tmpgen = { tmp_universe : Identifiers.universe; … … 1566 1554 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1567 1555 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1568 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_1 3548=1569 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_1 3548in1556 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_11311 = 1557 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11311 in 1570 1558 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1571 1559 … … 1573 1561 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1574 1562 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1575 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_1 3550=1576 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_1 3550in1563 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_11313 = 1564 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11313 in 1577 1565 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1578 1566 … … 1580 1568 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1581 1569 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1582 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_1 3552=1583 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_1 3552in1570 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_11315 = 1571 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11315 in 1584 1572 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1585 1573 … … 1587 1575 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1588 1576 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1589 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_1 3554=1590 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_1 3554in1577 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_11317 = 1578 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11317 in 1591 1579 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1592 1580 … … 1594 1582 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1595 1583 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1596 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_1 3556=1597 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_1 3556in1584 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_11319 = 1585 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11319 in 1598 1586 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1599 1587 … … 1601 1589 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1602 1590 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1603 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_1 3558=1604 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_1 3558in1591 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_11321 = 1592 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11321 in 1605 1593 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1606 1594 … … 1660 1648 let alloc_tmp vars ty g0 = 1661 1649 (let { Types.fst = tmp; Types.snd = u } = 1662 Identifiers.fresh AST.symbolTag g0.tmp_universe1650 Identifiers.fresh PreIdentifiers.SymbolTag g0.tmp_universe 1663 1651 in 1664 1652 (fun _ > { Types.fst = tmp; Types.snd = { tmp_universe = u; tmp_env = … … 1686 1674 let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function 1687 1675  DoNotConvert > h_DoNotConvert 1688  ConvertTo (x_1 3580, x_13579) > h_ConvertTo x_13580 x_135791676  ConvertTo (x_11343, x_11342) > h_ConvertTo x_11343 x_11342 1689 1677 1690 1678 (** val convert_flag_rect_Type5 : … … 1693 1681 let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function 1694 1682  DoNotConvert > h_DoNotConvert 1695  ConvertTo (x_1 3585, x_13584) > h_ConvertTo x_13585 x_135841683  ConvertTo (x_11348, x_11347) > h_ConvertTo x_11348 x_11347 1696 1684 1697 1685 (** val convert_flag_rect_Type3 : … … 1700 1688 let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function 1701 1689  DoNotConvert > h_DoNotConvert 1702  ConvertTo (x_1 3590, x_13589) > h_ConvertTo x_13590 x_135891690  ConvertTo (x_11353, x_11352) > h_ConvertTo x_11353 x_11352 1703 1691 1704 1692 (** val convert_flag_rect_Type2 : … … 1707 1695 let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function 1708 1696  DoNotConvert > h_DoNotConvert 1709  ConvertTo (x_1 3595, x_13594) > h_ConvertTo x_13595 x_135941697  ConvertTo (x_11358, x_11357) > h_ConvertTo x_11358 x_11357 1710 1698 1711 1699 (** val convert_flag_rect_Type1 : … … 1714 1702 let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function 1715 1703  DoNotConvert > h_DoNotConvert 1716  ConvertTo (x_1 3600, x_13599) > h_ConvertTo x_13600 x_135991704  ConvertTo (x_11363, x_11362) > h_ConvertTo x_11363 x_11362 1717 1705 1718 1706 (** val convert_flag_rect_Type0 : … … 1721 1709 let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function 1722 1710  DoNotConvert > h_DoNotConvert 1723  ConvertTo (x_1 3605, x_13604) > h_ConvertTo x_13605 x_136041711  ConvertTo (x_11368, x_11367) > h_ConvertTo x_11368 x_11367 1724 1712 1725 1713 (** val convert_flag_inv_rect_Type4 : … … 1773 1761  ConvertTo (continue, break) > 1774 1762 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"*)1779 1763 1780 1764 (** val translate_statement : … … 1877 1861  AST.ASTptr > 1878 1862 (fun x > 1879 Obj.magic (Errors.Error (Errors.msg TypeComparison.typeMismatch))))1863 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))) 1880 1864 e1')) 1881 1865  Csyntax.Swhile (e1, s1) > … … 1904 1888  AST.ASTptr > 1905 1889 (fun x > 1906 Obj.magic (Errors.Error (Errors.msg TypeComparison.typeMismatch))))1890 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))) 1907 1891 e1')) 1908 1892  Csyntax.Sdowhile (e1, s1) > … … 1936 1920  AST.ASTptr > 1937 1921 (fun x > 1938 Obj.magic (Errors.Error (Errors.msg TypeComparison.typeMismatch))))1922 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))) 1939 1923 e1')) 1940 1924  Csyntax.Sfor (s1, e1, s2, s3) > … … 1978 1962  AST.ASTptr > 1979 1963 (fun x > 1980 Obj.magic (Errors.Error (Errors.msg TypeComparison.typeMismatch))))1964 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))) 1981 1965 e1')) 1982 1966  Csyntax.Sbreak > 1983 1967 (match flag with 1984  DoNotConvert > (fun _ > Errors.Error (Errors.msg fIXME))1968  DoNotConvert > (fun _ > Errors.Error (Errors.msg ErrorMessages.FIXME)) 1985 1969  ConvertTo (continue_label, break_label) > 1986 1970 (fun _ > Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; … … 1988 1972  Csyntax.Scontinue > 1989 1973 (match flag with 1990  DoNotConvert > (fun _ > Errors.Error (Errors.msg fIXME))1974  DoNotConvert > (fun _ > Errors.Error (Errors.msg ErrorMessages.FIXME)) 1991 1975  ConvertTo (continue_label, break_label) > 1992 1976 (fun _ > Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; … … 1999 1983 Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; 2000 1984 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)) 2002 1987  Types.Some e1 > 2003 1988 (match rettyp with 2004  Types.None > Errors.Error (Errors.msg returnMismatch)1989  Types.None > Errors.Error (Errors.msg ErrorMessages.ReturnMismatch) 2005 1990  Types.Some rty > 2006 1991 Obj.magic … … 2015 2000 (Types.Some { Types.dpi1 = rty; Types.dpi2 = 2016 2001 (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) 2018 2003  Csyntax.Slabel (l, s1) > 2019 2004 Errors.bind_eq (lookup_label lbls l) (fun l' _ > … … 2036 2021 (Cminor_syntax.St_cost (l, s1')) }))) 2037 2022 2038 (** val paramGlobalMixup : String.string **)2039 let paramGlobalMixup = "param global mixup"2040 (*failwith "AXIOM TO BE REALIZED"*)2041 2042 2023 (** val alloc_params : 2043 2024 var_types > lenv > Csyntax.statement > tmpgen > convert_flag > … … 2051 2032 Obj.magic 2052 2033 (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su) 2053 (fun eta 2362>2054 let result = eta 2362in2034 (fun eta1273 > 2035 let result = eta1273 in 2055 2036 (let { Types.fst = fgens1; Types.snd = s0 } = result in 2056 2037 (fun _ > … … 2060 2041  Global x > 2061 2042 (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))))) 2064 2045  Stack n > 2065 2046 (fun _ > Errors.OK { Types.fst = fgens1; Types.snd = … … 2071 2052 s) params 2072 2053 2073 (** val duplicateLabel : String.string **)2074 let duplicateLabel = "duplicate label"2075 (*failwith "AXIOM TO BE REALIZED"*)2076 2077 2054 (** val populate_lenv : 2078 2055 AST.ident List.list > labgen > lenv > (lenv Types.sig0, labgen) … … 2083 2060  List.Cons (l, t) > 2084 2061 (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)) 2086 2064  Errors.Error x > 2087 2065 (fun _ > … … 2091 2069 (Obj.magic 2092 2070 (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 > 2095 2073 let lbls' = packed_lbls in 2096 2074 Obj.magic (Errors.OK { Types.fst = lbls'; Types.snd = ul1 }))))) … … 2101 2079 let build_label_env body = 2102 2080 let initial_labgen = { labuniverse = 2103 (Identifiers.new_universe Cminor_syntax.label); label_genlist =2081 (Identifiers.new_universe PreIdentifiers.Label); label_genlist = 2104 2082 List.Nil } 2105 2083 in … … 2108 2086 (Obj.magic 2109 2087 (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 > 2111 2090 let lbls = Types.pi1 label_map in 2112 2091 Obj.magic (Errors.OK { Types.fst = lbls; Types.snd = u }))) … … 2147 2126 Monad.m_bind0 (Monad.max_def Errors.res0) 2148 2127 (Obj.magic 2149 (Identifiers.check_distinct_env AST.symbolTag2128 (Identifiers.check_distinct_env PreIdentifiers.SymbolTag 2150 2129 (List.append params vars))) (fun _ > 2151 2130 Obj.magic (Errors.OK { Cminor_syntax.f_return =
Note: See TracChangeset
for help on using the changeset viewer.