Changeset 2773 for extracted/toCminor.ml
 Timestamp:
 Mar 4, 2013, 10:03:33 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/toCminor.ml
r2743 r2773 1 1 open Preamble 2 2 3 open BitVectorTrie4 5 3 open CostLabel 6 4 … … 21 19 open Extralib 22 20 21 open Lists 22 23 open Positive 24 25 open Identifiers 26 27 open Exp 28 29 open Arithmetic 30 31 open Vector 32 33 open Div_and_mod 34 35 open Util 36 37 open FoldStuff 38 39 open BitVector 40 41 open Jmeq 42 43 open Russell 44 45 open List 46 23 47 open Setoids 24 48 … … 26 50 27 51 open Option 28 29 open Lists30 31 open Positive32 33 open Identifiers34 35 open Exp36 37 open Arithmetic38 39 open Vector40 41 open Div_and_mod42 43 open Jmeq44 45 open Russell46 47 open List48 49 open Util50 51 open FoldStuff52 53 open BitVector54 52 55 53 open Extranat … … 149 147  Types.None > Identifiers.empty_set PreIdentifiers.SymbolTag 150 148  Types.Some e1 > gather_mem_vars_expr e1) (gather_mem_vars_expr e2)) 151 (Util.foldl (fun s0 e 0>149 (Util.foldl (fun s0 e > 152 150 Identifiers.union_set PreIdentifiers.SymbolTag s0 153 (gather_mem_vars_expr e 0))151 (gather_mem_vars_expr e)) 154 152 (Identifiers.empty_set PreIdentifiers.SymbolTag) es) 155 153  Csyntax.Ssequence (s1, s2) > … … 200 198 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 201 199 let rec var_type_rect_Type4 h_Global h_Stack h_Local = function 202  Global x_ 13003 > h_Global x_13003203  Stack x_ 13004 > h_Stack x_13004200  Global x_8081 > h_Global x_8081 201  Stack x_8082 > h_Stack x_8082 204 202  Local > h_Local 205 203 … … 207 205 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 208 206 let rec var_type_rect_Type5 h_Global h_Stack h_Local = function 209  Global x_ 13009 > h_Global x_13009210  Stack x_ 13010 > h_Stack x_13010207  Global x_8087 > h_Global x_8087 208  Stack x_8088 > h_Stack x_8088 211 209  Local > h_Local 212 210 … … 214 212 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 215 213 let rec var_type_rect_Type3 h_Global h_Stack h_Local = function 216  Global x_ 13015 > h_Global x_13015217  Stack x_ 13016 > h_Stack x_13016214  Global x_8093 > h_Global x_8093 215  Stack x_8094 > h_Stack x_8094 218 216  Local > h_Local 219 217 … … 221 219 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 222 220 let rec var_type_rect_Type2 h_Global h_Stack h_Local = function 223  Global x_ 13021 > h_Global x_13021224  Stack x_ 13022 > h_Stack x_13022221  Global x_8099 > h_Global x_8099 222  Stack x_8100 > h_Stack x_8100 225 223  Local > h_Local 226 224 … … 228 226 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 229 227 let rec var_type_rect_Type1 h_Global h_Stack h_Local = function 230  Global x_ 13027 > h_Global x_13027231  Stack x_ 13028 > h_Stack x_13028228  Global x_8105 > h_Global x_8105 229  Stack x_8106 > h_Stack x_8106 232 230  Local > h_Local 233 231 … … 235 233 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 236 234 let rec var_type_rect_Type0 h_Global h_Stack h_Local = function 237  Global x_ 13033 > h_Global x_13033238  Stack x_ 13034 > h_Stack x_13034235  Global x_8111 > h_Global x_8111 236  Stack x_8112 > h_Stack x_8112 239 237  Local > h_Local 240 238 … … 295 293 ErrorMessages.UndeclaredIdentifier), (List.Cons ((Errors.CTX 296 294 (PreIdentifiers.SymbolTag, id)), List.Nil)))) 297 (Identifiers.lookup 0PreIdentifiers.SymbolTag vars id)295 (Identifiers.lookup PreIdentifiers.SymbolTag vars id) 298 296 299 297 (** val always_alloc : Csyntax.type0 > Bool.bool **) … … 326 324 let { Types.fst = c; Types.snd = stack_high0 } = 327 325 match Bool.orb (always_alloc ty) 328 (Identifiers.member 0PreIdentifiers.SymbolTag mem_vars id) with326 (Identifiers.member PreIdentifiers.SymbolTag mem_vars id) with 329 327  Bool.True > 330 328 { Types.fst = (Stack stack_high); Types.snd = … … 373 371 (** val region_should_eq : 374 372 AST.region > AST.region > 'a1 > 'a1 Errors.res **) 375 let region_should_eq clearme r 5x =373 let region_should_eq clearme r2 x = 376 374 (match clearme with 377 375  AST.XData > … … 386 384  AST.XData > 387 385 (fun _ p > Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 388  AST.Code > (fun _ p > Errors.OK p))) r 5__ x386  AST.Code > (fun _ p > Errors.OK p))) r2 __ x 389 387 390 388 (** val typ_should_eq : AST.typ > AST.typ > 'a1 > 'a1 Errors.res **) … … 424 422 Csyntax.type0 > Nat.nat Types.option > Cminor_syntax.expr > 425 423 Cminor_syntax.expr **) 426 let fix_ptr_type ty n e 0=427 e 0424 let fix_ptr_type ty n e = 425 e 428 426 429 427 (** val translate_add : … … 451 449 (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)), 452 450 (FrontEndOps.Ointconst (AST.I16, AST.Signed, 453 (AST.repr 0AST.I16 (Csyntax.sizeof ty)))))))))))451 (AST.repr AST.I16 (Csyntax.sizeof ty))))))))))) 454 452  ClassifyOp.Add_case_ip (n, sz, sg, ty) > 455 453 (fun e1 e2 > … … 463 461 AST.Signed)), e1)), (Cminor_syntax.Cst ((AST.ASTint (AST.I16, 464 462 AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed, 465 (AST.repr 0AST.I16 (Csyntax.sizeof ty)))))))),463 (AST.repr AST.I16 (Csyntax.sizeof ty)))))))), 466 464 (fix_ptr_type ty n e2)))) 467 465  ClassifyOp.Add_default (x, x0) > … … 493 491 sg, AST.I16, sg)), e2)), (Cminor_syntax.Cst ((AST.ASTint (AST.I16, 494 492 sg)), (FrontEndOps.Ointconst (AST.I16, sg, 495 (AST.repr 0AST.I16 (Csyntax.sizeof ty)))))))))))))493 (AST.repr AST.I16 (Csyntax.sizeof ty))))))))))))) 496 494  ClassifyOp.Sub_case_pp (n1, n2, ty10, ty20) > 497 495 (fun e1 e2 > … … 510 508 (Cminor_syntax.Cst ((AST.ASTint (AST.I32, AST.Unsigned)), 511 509 (FrontEndOps.Ointconst (AST.I32, AST.Unsigned, 512 (AST.repr 0AST.I32 (Csyntax.sizeof ty10))))))))))510 (AST.repr AST.I32 (Csyntax.sizeof ty10)))))))))) 513 511  Csyntax.Tpointer x > 514 512 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) … … 615 613 (** val complete_cmp : 616 614 Csyntax.type0 > Cminor_syntax.expr > Cminor_syntax.expr Errors.res **) 617 let complete_cmp ty' e 0=615 let complete_cmp ty' e = 618 616 match ty' with 619 617  Csyntax.Tvoid > Errors.Error (Errors.msg ErrorMessages.TypeMismatch) … … 621 619 Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (AST.I8, AST.Unsigned)), 622 620 (AST.ASTint (sz, sg)), (FrontEndOps.Ocastint (AST.I8, AST.Unsigned, sz, 623 sg)), e 0))621 sg)), e)) 624 622  Csyntax.Tpointer x > 625 623 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) … … 668 666 AST.signedness > FrontEndOps.binary_operation) > Cminor_syntax.expr > 669 667 Cminor_syntax.expr > Cminor_syntax.expr Errors.res **) 670 let translate_misc_aop ty1 ty2 ty' op 0=668 let translate_misc_aop ty1 ty2 ty' op = 671 669 let ty1' = Csyntax.typ_of_type ty1 in 672 670 let ty2' = Csyntax.typ_of_type ty2 in … … 677 675 (Cminor_syntax.Op2 ((Csyntax.typ_of_type (Csyntax.Tint (sz, sg))), 678 676 (Csyntax.typ_of_type (Csyntax.Tint (sz, sg))), (AST.ASTint (sz, 679 sg)), (op 0sz sg), e1, e2)))677 sg)), (op sz sg), e1, e2))) 680 678  ClassifyOp.Aop_default (x, x0) > 681 679 (fun x1 x2 > Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) … … 685 683 Csyntax.type0 > Cminor_syntax.expr > Csyntax.type0 > 686 684 Cminor_syntax.expr Errors.res **) 687 let translate_binop op 0ty1 e1 ty2 e2 ty =685 let translate_binop op ty1 e1 ty2 e2 ty = 688 686 let ty' = Csyntax.typ_of_type ty in 689 (match op 0with687 (match op with 690 688  Csyntax.Oadd > translate_add ty1 ty2 ty e1 e2 691 689  Csyntax.Osub > translate_sub ty1 ty2 ty e1 e2 … … 707 705  Csyntax.Oshr > translate_shr ty1 ty2 ty e1 e2 708 706  Csyntax.Oeq > translate_cmp Integers.Ceq ty1 ty2 ty e1 e2 709  Csyntax.One 0> translate_cmp Integers.Cne ty1 ty2 ty e1 e2707  Csyntax.One > translate_cmp Integers.Cne ty1 ty2 ty e1 e2 710 708  Csyntax.Olt > translate_cmp Integers.Clt ty1 ty2 ty e1 e2 711 709  Csyntax.Ogt > translate_cmp Integers.Cgt ty1 ty2 ty e1 e2 … … 721 719 (fun x > Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 722 720  Csyntax.Tint (sz1, sg1) > 723 (fun e 0>721 (fun e > 724 722 match ty2 with 725 723  Csyntax.Tvoid > Errors.Error (Errors.msg ErrorMessages.TypeMismatch) … … 727 725 Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), (AST.ASTint 728 726 (sz2, sg2)), (FrontEndOps.Ocastint (sz1, sg1, sz2, sg2)), 729 (Types.pi1 e 0)))727 (Types.pi1 e))) 730 728  Csyntax.Tpointer x > 731 729 Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), AST.ASTptr, 732 (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e 0)))730 (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e))) 733 731  Csyntax.Tarray (x, x0) > 734 732 Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), AST.ASTptr, 735 (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e 0)))733 (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e))) 736 734  Csyntax.Tfunction (x, x0) > 737 735 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) … … 743 741 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 744 742  Csyntax.Tpointer x > 745 (fun e 0>743 (fun e > 746 744 match ty2 with 747 745  Csyntax.Tvoid > Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 748 746  Csyntax.Tint (sz2, sg2) > 749 747 Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)), 750 (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e 0)))751  Csyntax.Tpointer x0 > Errors.OK e 0752  Csyntax.Tarray (x0, x1) > Errors.OK e 0748 (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e))) 749  Csyntax.Tpointer x0 > Errors.OK e 750  Csyntax.Tarray (x0, x1) > Errors.OK e 753 751  Csyntax.Tfunction (x0, x1) > 754 752 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) … … 760 758 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 761 759  Csyntax.Tarray (x, x0) > 762 (fun e 0>760 (fun e > 763 761 match ty2 with 764 762  Csyntax.Tvoid > Errors.Error (Errors.msg ErrorMessages.TypeMismatch) 765 763  Csyntax.Tint (sz2, sg2) > 766 764 Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)), 767 (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e 0)))768  Csyntax.Tpointer x1 > Errors.OK e 0769  Csyntax.Tarray (x1, x2) > Errors.OK e 0765 (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e))) 766  Csyntax.Tpointer x1 > Errors.OK e 767  Csyntax.Tarray (x1, x2) > Errors.OK e 770 768  Csyntax.Tfunction (x1, x2) > 771 769 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) … … 793 791 let cm_one sz sg = 794 792 Cminor_syntax.Cst ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg, 795 (AST.repr 0sz (Nat.S Nat.O)))))793 (AST.repr sz (Nat.S Nat.O))))) 796 794 797 795 (** val translate_expr : … … 879 877 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) 880 878  AST.ASTptr > Obj.magic (Errors.OK e1'))) 881  Csyntax.Eunop (op 0, e1) >882 (match op 0with879  Csyntax.Eunop (op, e1) > 880 (match op with 883 881  Csyntax.Onotbool > 884 882 (fun _ > … … 900 898 (translate_unop 901 899 (Csyntax.typ_of_type (Csyntax.typeof e1)) 902 (Csyntax.typ_of_type ty) op 0)) (fun op' >900 (Csyntax.typ_of_type ty) op)) (fun op' > 903 901 Monad.m_bind0 (Monad.max_def Errors.res0) 904 902 (Obj.magic (translate_expr vars e1)) (fun e1' > … … 916 914 (Obj.magic 917 915 (translate_unop (Csyntax.typ_of_type (Csyntax.typeof e1)) 918 (Csyntax.typ_of_type ty) op 0)) (fun op' >916 (Csyntax.typ_of_type ty) op)) (fun op' > 919 917 Monad.m_bind0 (Monad.max_def Errors.res0) 920 918 (Obj.magic (translate_expr vars e1)) (fun e1' > … … 928 926 (Obj.magic 929 927 (translate_unop (Csyntax.typ_of_type (Csyntax.typeof e1)) 930 (Csyntax.typ_of_type ty) op 0)) (fun op' >928 (Csyntax.typ_of_type ty) op)) (fun op' > 931 929 Monad.m_bind0 (Monad.max_def Errors.res0) 932 930 (Obj.magic (translate_expr vars e1)) (fun e1' > … … 934 932 ((Csyntax.typ_of_type (Csyntax.typeof e1)), 935 933 (Csyntax.typ_of_type ty), op', (Types.pi1 e1'))))))))) __ 936  Csyntax.Ebinop (op 0, e1, e2) >934  Csyntax.Ebinop (op, e1, e2) > 937 935 Obj.magic 938 936 (Monad.m_bind0 (Monad.max_def Errors.res0) … … 942 940 Obj.magic 943 941 (Errors.bind_eq 944 (translate_binop op 0(Csyntax.typeof e1) (Types.pi1 e1')942 (translate_binop op (Csyntax.typeof e1) (Types.pi1 e1') 945 943 (Csyntax.typeof e2) (Types.pi1 e2') ty) (fun e' _ > 946 944 Errors.OK e'))))) … … 1065 1063 Errors.OK (Cminor_syntax.Cst ((AST.ASTint (sz, sg)), 1066 1064 (FrontEndOps.Ointconst (sz, sg, 1067 (AST.repr 0sz (Csyntax.sizeof ty1))))))1065 (AST.repr sz (Csyntax.sizeof ty1)))))) 1068 1066  Csyntax.Tpointer x > 1069 1067 Errors.Error (Errors.msg ErrorMessages.TypeMismatch) … … 1103 1101 (Types.pi1 e1'), (Cminor_syntax.Cst ((AST.ASTint (AST.I16, 1104 1102 AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed, 1105 (AST.repr 0AST.I16 off))))))))))1103 (AST.repr AST.I16 off)))))))))) 1106 1104  Csyntax.By_reference > 1107 1105 Obj.magic (Errors.OK (Cminor_syntax.Op2 (AST.ASTptr, … … 1110 1108 (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)), 1111 1109 (FrontEndOps.Ointconst (AST.I16, AST.Signed, 1112 (AST.repr 0AST.I16 off))))))))1110 (AST.repr AST.I16 off)))))))) 1113 1111  Csyntax.By_nothing x0 > 1114 1112 Obj.magic (Errors.Error … … 1207 1205 (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)), 1208 1206 (FrontEndOps.Ointconst (AST.I16, AST.Signed, 1209 (AST.repr 0AST.I16 off)))))))))))1207 (AST.repr AST.I16 off))))))))))) 1210 1208  Csyntax.Tunion (x0, x1) > translate_addr vars e1 1211 1209  Csyntax.Tcomp_ptr x0 > … … 1223 1221 let rec destination_rect_Type4 vars h_IdDest h_MemDest = function 1224 1222  IdDest (id, ty) > h_IdDest id ty __ 1225  MemDest x_ 14489 > h_MemDest x_144891223  MemDest x_9567 > h_MemDest x_9567 1226 1224 1227 1225 (** val destination_rect_Type5 : … … 1230 1228 let rec destination_rect_Type5 vars h_IdDest h_MemDest = function 1231 1229  IdDest (id, ty) > h_IdDest id ty __ 1232  MemDest x_ 14494 > h_MemDest x_144941230  MemDest x_9572 > h_MemDest x_9572 1233 1231 1234 1232 (** val destination_rect_Type3 : … … 1237 1235 let rec destination_rect_Type3 vars h_IdDest h_MemDest = function 1238 1236  IdDest (id, ty) > h_IdDest id ty __ 1239  MemDest x_ 14499 > h_MemDest x_144991237  MemDest x_9577 > h_MemDest x_9577 1240 1238 1241 1239 (** val destination_rect_Type2 : … … 1244 1242 let rec destination_rect_Type2 vars h_IdDest h_MemDest = function 1245 1243  IdDest (id, ty) > h_IdDest id ty __ 1246  MemDest x_ 14504 > h_MemDest x_145041244  MemDest x_9582 > h_MemDest x_9582 1247 1245 1248 1246 (** val destination_rect_Type1 : … … 1251 1249 let rec destination_rect_Type1 vars h_IdDest h_MemDest = function 1252 1250  IdDest (id, ty) > h_IdDest id ty __ 1253  MemDest x_ 14509 > h_MemDest x_145091251  MemDest x_9587 > h_MemDest x_9587 1254 1252 1255 1253 (** val destination_rect_Type0 : … … 1258 1256 let rec destination_rect_Type0 vars h_IdDest h_MemDest = function 1259 1257  IdDest (id, ty) > h_IdDest id ty __ 1260  MemDest x_ 14514 > h_MemDest x_145141258  MemDest x_9592 > h_MemDest x_9592 1261 1259 1262 1260 (** val destination_inv_rect_Type4 : … … 1376 1374 Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingLabel), 1377 1375 (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, l)), List.Nil)))) 1378 (Identifiers.lookup0 PreIdentifiers.SymbolTag lbls l) 1379 1380 type fresh_list_for_univ = __ 1376 (Identifiers.lookup PreIdentifiers.SymbolTag lbls l) 1381 1377 1382 1378 type labgen = { labuniverse : Identifiers.universe; … … 1386 1382 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1387 1383 'a1) > labgen > 'a1 **) 1388 let rec labgen_rect_Type4 h_mk_labgen x_14549 = 1389 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1390 x_14549 1384 let rec labgen_rect_Type4 h_mk_labgen x_9627 = 1385 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9627 1391 1386 in 1392 1387 h_mk_labgen labuniverse0 label_genlist0 __ … … 1395 1390 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1396 1391 'a1) > labgen > 'a1 **) 1397 let rec labgen_rect_Type5 h_mk_labgen x_14551 = 1398 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1399 x_14551 1392 let rec labgen_rect_Type5 h_mk_labgen x_9629 = 1393 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9629 1400 1394 in 1401 1395 h_mk_labgen labuniverse0 label_genlist0 __ … … 1404 1398 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1405 1399 'a1) > labgen > 'a1 **) 1406 let rec labgen_rect_Type3 h_mk_labgen x_14553 = 1407 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1408 x_14553 1400 let rec labgen_rect_Type3 h_mk_labgen x_9631 = 1401 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9631 1409 1402 in 1410 1403 h_mk_labgen labuniverse0 label_genlist0 __ … … 1413 1406 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1414 1407 'a1) > labgen > 'a1 **) 1415 let rec labgen_rect_Type2 h_mk_labgen x_14555 = 1416 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1417 x_14555 1408 let rec labgen_rect_Type2 h_mk_labgen x_9633 = 1409 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9633 1418 1410 in 1419 1411 h_mk_labgen labuniverse0 label_genlist0 __ … … 1422 1414 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1423 1415 'a1) > labgen > 'a1 **) 1424 let rec labgen_rect_Type1 h_mk_labgen x_14557 = 1425 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1426 x_14557 1416 let rec labgen_rect_Type1 h_mk_labgen x_9635 = 1417 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9635 1427 1418 in 1428 1419 h_mk_labgen labuniverse0 label_genlist0 __ … … 1431 1422 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1432 1423 'a1) > labgen > 'a1 **) 1433 let rec labgen_rect_Type0 h_mk_labgen x_14559 = 1434 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1435 x_14559 1424 let rec labgen_rect_Type0 h_mk_labgen x_9637 = 1425 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9637 1436 1426 in 1437 1427 h_mk_labgen labuniverse0 label_genlist0 __ … … 1537 1527 var_types > Csyntax.expr > (AST.typ, Cminor_syntax.expr) Types.dPair 1538 1528 Types.sig0 Errors.res **) 1539 let translate_expr_sigma v e 0=1529 let translate_expr_sigma v e = 1540 1530 Obj.magic 1541 1531 (Monad.m_bind0 (Monad.max_def Errors.res0) 1542 (Obj.magic (translate_expr v e 0)) (fun e' >1532 (Obj.magic (translate_expr v e)) (fun e' > 1543 1533 Obj.magic (Errors.OK { Types.dpi1 = 1544 (Csyntax.typ_of_type (Csyntax.typeof e 0)); Types.dpi2 =1534 (Csyntax.typ_of_type (Csyntax.typeof e)); Types.dpi2 = 1545 1535 (Types.pi1 e') }))) 1546 1536 … … 1558 1548 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1559 1549 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1560 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_ 14575=1561 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14575in1550 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_9653 = 1551 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9653 in 1562 1552 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1563 1553 … … 1565 1555 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1566 1556 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1567 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_ 14577=1568 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14577in1557 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_9655 = 1558 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9655 in 1569 1559 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1570 1560 … … 1572 1562 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1573 1563 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1574 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_ 14579=1575 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14579in1564 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_9657 = 1565 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9657 in 1576 1566 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1577 1567 … … 1579 1569 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1580 1570 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1581 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_ 14581=1582 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14581in1571 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_9659 = 1572 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9659 in 1583 1573 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1584 1574 … … 1586 1576 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1587 1577 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1588 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_ 14583=1589 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14583in1578 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_9661 = 1579 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9661 in 1590 1580 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1591 1581 … … 1593 1583 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1594 1584 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1595 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_ 14585=1596 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14585in1585 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_9663 = 1586 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9663 in 1597 1587 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1598 1588 … … 1650 1640 (** val alloc_tmp : 1651 1641 var_types > Csyntax.type0 > tmpgen > (AST.ident, tmpgen) Types.prod **) 1652 let alloc_tmp vars ty g 0=1642 let alloc_tmp vars ty g = 1653 1643 (let { Types.fst = tmp; Types.snd = u } = 1654 Identifiers.fresh PreIdentifiers.SymbolTag g 0.tmp_universe1644 Identifiers.fresh PreIdentifiers.SymbolTag g.tmp_universe 1655 1645 in 1656 1646 (fun _ > { Types.fst = tmp; Types.snd = { tmp_universe = u; tmp_env = 1657 (List.Cons ({ Types.fst = tmp; Types.snd = ty }, g 0.tmp_env)) } })) __1647 (List.Cons ({ Types.fst = tmp; Types.snd = ty }, g.tmp_env)) } })) __ 1658 1648 1659 1649 (** val mklabels : … … 1678 1668 let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function 1679 1669  DoNotConvert > h_DoNotConvert 1680  ConvertTo (x_ 14607, x_14606) > h_ConvertTo x_14607 x_146061670  ConvertTo (x_9685, x_9684) > h_ConvertTo x_9685 x_9684 1681 1671 1682 1672 (** val convert_flag_rect_Type5 : … … 1685 1675 let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function 1686 1676  DoNotConvert > h_DoNotConvert 1687  ConvertTo (x_ 14612, x_14611) > h_ConvertTo x_14612 x_146111677  ConvertTo (x_9690, x_9689) > h_ConvertTo x_9690 x_9689 1688 1678 1689 1679 (** val convert_flag_rect_Type3 : … … 1692 1682 let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function 1693 1683  DoNotConvert > h_DoNotConvert 1694  ConvertTo (x_ 14617, x_14616) > h_ConvertTo x_14617 x_146161684  ConvertTo (x_9695, x_9694) > h_ConvertTo x_9695 x_9694 1695 1685 1696 1686 (** val convert_flag_rect_Type2 : … … 1699 1689 let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function 1700 1690  DoNotConvert > h_DoNotConvert 1701  ConvertTo (x_ 14622, x_14621) > h_ConvertTo x_14622 x_146211691  ConvertTo (x_9700, x_9699) > h_ConvertTo x_9700 x_9699 1702 1692 1703 1693 (** val convert_flag_rect_Type1 : … … 1706 1696 let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function 1707 1697  DoNotConvert > h_DoNotConvert 1708  ConvertTo (x_ 14627, x_14626) > h_ConvertTo x_14627 x_146261698  ConvertTo (x_9705, x_9704) > h_ConvertTo x_9705 x_9704 1709 1699 1710 1700 (** val convert_flag_rect_Type0 : … … 1713 1703 let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function 1714 1704  DoNotConvert > h_DoNotConvert 1715  ConvertTo (x_ 14632, x_14631) > h_ConvertTo x_14632 x_146311705  ConvertTo (x_9710, x_9709) > h_ConvertTo x_9710 x_9709 1716 1706 1717 1707 (** val convert_flag_inv_rect_Type4 : … … 2031 2021 Types.sig0 > ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) 2032 2022 Types.prod Types.sig0 Errors.res **) 2033 let alloc_params vars lbls statement 0uv ul rettyp params s =2023 let alloc_params vars lbls statement uv ul rettyp params s = 2034 2024 Util.foldl (fun su it > 2035 2025 let { Types.fst = id; Types.snd = ty } = it in 2036 2026 Obj.magic 2037 2027 (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su) 2038 (fun eta 2887>2039 let result = eta 2887in2028 (fun eta1212 > 2029 let result = eta1212 in 2040 2030 (let { Types.fst = fgens1; Types.snd = s0 } = result in 2041 2031 (fun _ > … … 2160 2150 (match l with 2161 2151  List.Nil > (fun _ > Errors.OK List.Nil) 2162  List.Cons (hd 0, tl) >2152  List.Cons (hd, tl) > 2163 2153 (fun _ > 2164 2154 Obj.magic 2165 (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f hd 0__)2155 (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f hd __) 2166 2156 (fun b_hd > 2167 2157 Monad.m_bind0 (Monad.max_def Errors.res0)
Note: See TracChangeset
for help on using the changeset viewer.