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

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/cminor_semantics.ml
r2636 r2649 15 15 open Identifiers 16 16 17 open Floats18 19 17 open Integers 20 18 … … 39 37 open Pointers 40 38 39 open ErrorMessages 40 41 41 open Option 42 42 … … 46 46 47 47 open Positive 48 49 open Char50 51 open String52 48 53 49 open PreIdentifiers … … 452 448  Finalstate a0 > Obj.magic (fun _ dH > dH __)) y 453 449 454 (** val unknownLocal : String.string **)455 let unknownLocal = "unknown local"456 (*failwith "AXIOM TO BE REALIZED"*)457 458 (** val failedConstant : String.string **)459 let failedConstant = "failed constant"460 (*failwith "AXIOM TO BE REALIZED"*)461 462 (** val failedOp : String.string **)463 let failedOp = "failed op"464 (*failwith "AXIOM TO BE REALIZED"*)465 466 (** val failedLoad : String.string **)467 let failedLoad = "failed load"468 (*failwith "AXIOM TO BE REALIZED"*)469 470 450 (** val eval_expr : 471 451 genv > AST.typ > Cminor_syntax.expr > env > Pointers.block > … … 475 455  Cminor_syntax.Id (x, i) > 476 456 (fun _ > 477 let r = Identifiers.lookup_present AST.symbolTag en i in457 let r = Identifiers.lookup_present PreIdentifiers.SymbolTag en i in 478 458 Errors.OK { Types.fst = Events.e0; Types.snd = r }) 479 459  Cminor_syntax.Cst (x, c) > … … 482 462 (Monad.m_bind0 (Monad.max_def Errors.res0) 483 463 (Obj.magic 484 (Errors.opt_to_res (Errors.msg failedConstant)464 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedConstant) 485 465 (FrontEndOps.eval_constant x (Globalenvs.find_symbol ge) sp c))) 486 466 (fun r > … … 493 473 Monad.m_bind0 (Monad.max_def Errors.res0) 494 474 (Obj.magic 495 (Errors.opt_to_res (Errors.msg failedOp)475 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp) 496 476 (FrontEndOps.eval_unop ty ty' op0 v))) (fun r > 497 477 Obj.magic (Errors.OK { Types.fst = tr; Types.snd = r }))))) … … 505 485 Monad.m_bind0 (Monad.max_def Errors.res0) 506 486 (Obj.magic 507 (Errors.opt_to_res (Errors.msg failedOp)487 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp) 508 488 (FrontEndOps.eval_binop m ty1 ty2 ty' op0 v1 v2))) 509 489 (fun r > … … 517 497 Monad.m_bind0 (Monad.max_def Errors.res0) 518 498 (Obj.magic 519 (Errors.opt_to_res (Errors.msg failedLoad)499 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad) 520 500 (FrontEndMem.loadv ty m v))) (fun r > 521 501 Obj.magic (Errors.OK { Types.fst = tr; Types.snd = r }))))) … … 544 524 (Events.eapp (Events.echarge l) tr); Types.snd = r }))))) __ 545 525 546 (** val badState : String.string **)547 let badState = "bad state"548 (*failwith "AXIOM TO BE REALIZED"*)549 550 526 (** val k_exit : 551 527 Nat.nat > cont > Cminor_syntax.internal_function > env > cont … … 553 529 let rec k_exit n k f en = 554 530 (match k with 555  Kend > (fun _ > Errors.Error (Errors.msg badState))531  Kend > (fun _ > Errors.Error (Errors.msg ErrorMessages.BadState)) 556 532  Kseq (x, k') > (fun _ > k_exit n k' f en) 557 533  Kblock k' > … … 596 572  Cminor_syntax.St_label (l', s') > 597 573 (fun _ > 598 match Identifiers.identifier_eq Cminor_syntax.label l l' with574 match Identifiers.identifier_eq PreIdentifiers.Label l l' with 599 575  Types.Inl _ > Types.Some { Types.fst = s'; Types.snd = k } 600 576  Types.Inr _ > find_label l s' k f en) … … 611 587  Types.Some sk > (fun _ > sk)) __ 612 588 613 (** val wrongNumberOfParameters : String.string **)614 let wrongNumberOfParameters = "wrong number of parameters"615 (*failwith "AXIOM TO BE REALIZED"*)616 617 589 (** val bind_params : 618 590 Values.val0 List.list > (AST.ident, AST.typ) Types.prod List.list > env … … 622 594  List.Nil > 623 595 (match ids with 624  List.Nil > Errors.OK (Identifiers.empty_map AST.symbolTag) 625  List.Cons (x, x0) > Errors.Error (Errors.msg wrongNumberOfParameters)) 596  List.Nil > Errors.OK (Identifiers.empty_map PreIdentifiers.SymbolTag) 597  List.Cons (x, x0) > 598 Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters)) 626 599  List.Cons (v, vt) > 627 600 (match ids with 628  List.Nil > Errors.Error (Errors.msg wrongNumberOfParameters) 601  List.Nil > 602 Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters) 629 603  List.Cons (idh, idt) > 630 604 let { Types.fst = id; Types.snd = ty } = idh in … … 633 607 (Obj.magic (bind_params vt idt)) (fun en > 634 608 Obj.magic (Errors.OK 635 (Identifiers.add AST.symbolTag (Types.pi1 en) idh.Types.fst v))))) 609 (Identifiers.add PreIdentifiers.SymbolTag (Types.pi1 en) 610 idh.Types.fst v))))) 636 611 637 612 (** val init_locals : … … 639 614 let init_locals = 640 615 List.foldr (fun idty en > 641 Identifiers.add AST.symbolTag en idty.Types.fst Values.Vundef)616 Identifiers.add PreIdentifiers.SymbolTag en idty.Types.fst Values.Vundef) 642 617 643 618 (** val trace_map_inv : … … 657 632 Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr'); 658 633 Types.snd = (List.Cons (h', t')) })))))) __ 659 660 (** val failedStore : String.string **)661 let failedStore = "failed store"662 (*failwith "AXIOM TO BE REALIZED"*)663 664 (** val badFunctionValue : String.string **)665 let badFunctionValue = "bad function value"666 (*failwith "AXIOM TO BE REALIZED"*)667 668 (** val returnMismatch : String.string **)669 let returnMismatch = "return mismatch"670 (*failwith "AXIOM TO BE REALIZED"*)671 634 672 635 (** val eval_step : … … 703 666 (Monad.m_bind2 (Monad.max_def Errors.res0) 704 667 (Obj.magic (eval_expr ge x e1 en sp m)) (fun tr v > 705 let en' = Identifiers.update_present AST.symbolTag en id v in 668 let en' = 669 Identifiers.update_present PreIdentifiers.SymbolTag en id v 670 in 706 671 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr; 707 672 Types.snd = (State (f, Cminor_syntax.St_skip, en', m, sp, k, … … 717 682 Monad.m_bind0 (Monad.max_def Errors.res0) 718 683 (Obj.magic 719 (Errors.opt_to_res (Errors.msg failedStore)684 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore) 720 685 (FrontEndMem.storev ty m vdst v))) (fun m' > 721 686 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = … … 729 694 Monad.m_bind0 (Monad.max_def Errors.res0) 730 695 (Obj.magic 731 (Errors.opt_to_res (Errors.msg badFunctionValue) 696 (Errors.opt_to_res 697 (Errors.msg ErrorMessages.BadFunctionValue) 732 698 (Globalenvs.find_funct ge vf))) (fun fd > 733 699 Monad.m_bind2 (Monad.max_def Errors.res0) … … 800 766 (let { Types.fst = m'; Types.snd = sp } = 801 767 GenMem.alloc m (Z.z_of_nat Nat.O) 802 (Z.z_of_nat f.Cminor_syntax.f_stacksize) AST.XData768 (Z.z_of_nat f.Cminor_syntax.f_stacksize) 803 769 in 804 770 Obj.magic … … 835 801  SStop > 836 802 (match result with 837  Types.None > Errors.Error (Errors.msg returnMismatch) 803  Types.None > 804 Errors.Error (Errors.msg ErrorMessages.ReturnMismatch) 838 805  Types.Some v > 839 806 (match v with 840  Values.Vundef > Errors.Error (Errors.msg returnMismatch) 807  Values.Vundef > 808 Errors.Error (Errors.msg ErrorMessages.ReturnMismatch) 841 809  Values.Vint (sz, r) > 842 810 (match sz with 843  AST.I8 > (fun x > Errors.Error (Errors.msg returnMismatch)) 811  AST.I8 > 812 (fun x > Errors.Error 813 (Errors.msg ErrorMessages.ReturnMismatch)) 844 814  AST.I16 > 845 (fun x > Errors.Error (Errors.msg returnMismatch)) 815 (fun x > Errors.Error 816 (Errors.msg ErrorMessages.ReturnMismatch)) 846 817  AST.I32 > 847 818 (fun r5 > … … 850 821 { Types.fst = Events.e0; Types.snd = (Finalstate r5) }))) 851 822 r 852  Values.Vnull > Errors.Error (Errors.msg returnMismatch) 853  Values.Vptr x > Errors.Error (Errors.msg returnMismatch))) 823  Values.Vnull > 824 Errors.Error (Errors.msg ErrorMessages.ReturnMismatch) 825  Values.Vptr x > 826 Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))) 854 827  Scall (dst, f, sp, en, k, st') > 855 828 (match result with … … 861 834 Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip, en, 862 835 m, sp, k, st')) }) 863  Types.Some x > Errors.Error (Errors.msg returnMismatch)) 836  Types.Some x > 837 Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)) 864 838  Types.Some v > 865 839 (match dst with 866 840  Types.None > 867 (fun _ > Errors.Error (Errors.msg returnMismatch)) 841 (fun _ > Errors.Error 842 (Errors.msg ErrorMessages.ReturnMismatch)) 868 843  Types.Some idty > 869 844 (fun _ > … … 871 846 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = 872 847 Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip, 873 (Identifiers.update_present AST.symbolTag en848 (Identifiers.update_present PreIdentifiers.SymbolTag en 874 849 idty.Types.fst v), m, sp, k, st')) }))) __)) 875  Finalstate r > IOMonad.err_to_io (Errors.Error (Errors.msg badState)) 850  Finalstate r > 851 IOMonad.err_to_io (Errors.Error (Errors.msg ErrorMessages.BadState)) 876 852 877 853 (** val is_final0 : state0 > Integers.int Types.option **) … … 886 862 { SmallstepExec.is_final = (fun x > Obj.magic is_final0); 887 863 SmallstepExec.step = (Obj.magic eval_step) } 888 889 (** val mainMissing : String.string **)890 let mainMissing = "main missing"891 (*failwith "AXIOM TO BE REALIZED"*)892 864 893 865 (** val make_global0 : Cminor_syntax.cminor_program > genv **) … … 904 876 Monad.m_bind0 (Monad.max_def Errors.res0) 905 877 (Obj.magic 906 (Errors.opt_to_res (Errors.msg mainMissing)878 (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing) 907 879 (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b > 908 880 Monad.m_bind0 (Monad.max_def Errors.res0) 909 881 (Obj.magic 910 (Errors.opt_to_res (Errors.msg mainMissing)882 (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing) 911 883 (Globalenvs.find_funct_ptr ge b))) (fun f > 912 884 Obj.magic (Errors.OK (Callstate (f, List.Nil, m, SStop))))))) … … 933 905 Monad.m_bind0 (Monad.max_def Errors.res0) 934 906 (Obj.magic 935 (Errors.opt_to_res (Errors.msg mainMissing)907 (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing) 936 908 (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b > 937 909 Monad.m_bind0 (Monad.max_def Errors.res0) 938 910 (Obj.magic 939 (Errors.opt_to_res (Errors.msg mainMissing)911 (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing) 940 912 (Globalenvs.find_funct_ptr ge b))) (fun f > 941 913 Obj.magic (Errors.OK (Callstate (f, List.Nil, m, SStop)))))))
Note: See TracChangeset
for help on using the changeset viewer.