Changeset 24 for Csemantics/CexecIO.ma
 Timestamp:
 Aug 27, 2010, 1:21:50 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/CexecIO.ma
r20 r24 3 3 4 4 include "extralib.ma". 5 include "IOMonad.ma". 5 6 6 7 (* Some experimental definitions for an executable semantics. *) … … 611 612 (* IO monad *) 612 613 613 ninductive IO (T:Type) : Type ≝ 614  Interact : ident → list eventval → (eventval → IO T) → IO T 615  Value : T → IO T 616  Wrong : IO T. 617 618 nlet rec bindIO (T,T':Type) (v:IO T) (f:T → IO T') on v : IO T' ≝ 619 match v with 620 [ Interact fn args k ⇒ (Interact ? fn args (λres. bindIO T T' (k res) f)) 621  Value v' ⇒ (f v') 622  Wrong ⇒ Wrong T' 623 ]. 624 625 nlet rec bindIO2 (T1,T2,T':Type) (v:IO (T1×T2)) (f:T1 → T2 → IO T') on v : IO T' ≝ 626 match v with 627 [ Interact fn args k ⇒ (Interact ? fn args (λres. bindIO2 T1 T2 T' (k res) f)) 628  Value v' ⇒ match v' with [ mk_pair v1 v2 ⇒ f v1 v2 ] 629  Wrong ⇒ Wrong T' 630 ]. 631 632 ndefinition do_io : ident → list eventval → IO eventval ≝ 633 λfn,args. Interact eventval fn args (λres. Value eventval res). 634 635 ndefinition ret: ∀T. T → (IO T) ≝ 636 λT,x.(Value T x). 637 638 ndefinition err_to_io : ∀T. res T → IO T ≝ 639 λT,v. match v with [ OK v' ⇒ Value T v'  Error ⇒ Wrong T ]. 640 (*ncoercion err_to_io : ∀A.∀c:res A.IO A ≝ err_to_io on _c:res ? to IO ?.*) 641 ndefinition err_to_io_sig : ∀T.∀P:T → Prop. res (sigma T P) → IO (sigma T P) ≝ 642 λT,P,v. match v with [ OK v' ⇒ Value (sigma T P) v'  Error ⇒ Wrong (sigma T P) ]. 643 ncoercion err_to_io_sig : ∀A.∀P:A → Prop.∀c:res (sigma A P).IO (sigma A P) ≝ err_to_io_sig on _c:res ? to IO ?. 644 645 646 (* If the original definitions are vague enough, do I need to do this? *) 647 notation "! ident v ← e;: e'" right associative with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}. 648 notation "! 〈ident v1, ident v2〉 ← e;: e'" right associative with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}. 649 interpretation "IO monad bind" 'bindIO e f = (bindIO ? ? e f). 650 interpretation "IO monad pair bind" 'bindIO2 e f = (bindIO2 ??? e f). 651 (**) 652 nlet rec P_io (A:Type) (P:A → CProp[0]) (v:IO A) on v : CProp[0] ≝ 653 match v return λ_.CProp[0] with 654 [ Wrong ⇒ True 655  Value z ⇒ P z 656  Interact fn args k ⇒ ∀v'.P_io A P (k v') 657 ]. 658 659 ndefinition P_to_P_option_io : ∀A:Type[0].∀P:A → CProp[0].option (IO A) → CProp[0] ≝ 660 λA,P,a.match a with 661 [ None ⇒ False 662  Some y ⇒ P_io A P y 663 ]. 664 665 nlet rec io_inject_0 (A:Type) (P:A → Prop) (a:IO A) (p:P_io A P a) on a : IO (sigma A P) ≝ 666 (match a return λa'.a=a' → ? with 667 [ Wrong ⇒ λ_. Wrong ? 668  Value c ⇒ λe2. Value ? (sig_intro A P c ?) 669  Interact fn args k ⇒ λe2. Interact ? fn args (λv. io_inject_0 A P (k v) ?) 670 ]) (refl ? a). 671 (* XXX: odd, can't do both cases at once. *) 672 ##[ nrewrite > e2 in p; nwhd in ⊢ (% → ?); //; 673 ## nrewrite > e2 in p; nwhd in ⊢ (% → ?); //; 674 ##] nqed. 675 676 ndefinition io_inject : ∀A.∀P:A → Prop.∀a:option (IO A).∀p:P_to_P_option_io A P a.IO (sigma A P) ≝ 677 λA.λP:A → Prop.λa:option (IO A).λp:P_to_P_option_io A P a. 678 (match a return λa'.a=a' → IO (sigma A P) with 679 [ None ⇒ λe1.? 680  Some b ⇒ λe1. io_inject_0 A P b ? 681 ]) (refl ? a). 682 ##[ nrewrite > e1 in p; nnormalize; *; 683 ## nrewrite > e1 in p; nnormalize; // 684 ##] nqed. 685 686 nlet rec io_eject (A:Type) (P: A → Prop) (a:IO (sigma A P)) on a : IO A ≝ 687 match a with 688 [ Wrong ⇒ Wrong ? 689  Value b ⇒ match b with [ sig_intro w p ⇒ Value ? w] 690  Interact fn args k ⇒ Interact ? fn args (λv. io_eject A P (k v)) 691 ]. 692 693 ncoercion io_inject : 694 ∀A.∀P:A → Prop.∀a.∀p:P_to_P_option_io ? P a.IO (sigma A P) ≝ io_inject 695 on a:option (IO ?) to IO (sigma ? ?). 696 ncoercion io_eject : ∀A.∀P:A → Prop.∀c:IO (sigma A P).IO A ≝ io_eject 697 on _c:IO (sigma ? ?) to IO ?. 698 699 ndefinition opt_to_io : ∀T.option T → IO T ≝ 700 λT,v. match v with [ None ⇒ Wrong T  Some v' ⇒ Value T v' ]. 701 ncoercion opt_to_io : ∀T.∀v:option T. IO T ≝ opt_to_io on _v:option ? to IO ?. 702 703 nlemma sig_bindIO_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:IO (sigma A P). ∀f:sigma A P → IO B. 704 (∀v:A. ∀p:P v. P_io ? P' (f (sig_intro A P v p))) → 705 P_io ? P' (bindIO (sigma A P) B e f). 706 #A B P P' e f; nelim e; 707 ##[ #fn args k IH; #IH'; nwhd; #res; napply IH; //; 708 ## #v0; nelim v0; #v Hv IH; nwhd; napply IH; 709 ## //; 710 ##] nqed. 711 712 nlemma sig_bindIO2_OK: ∀A,B,C. ∀P:(A×B) → Prop. ∀P':C → Prop. ∀e:IO (sigma (A×B) P). ∀f: A → B → IO C. 713 (∀vA:A.∀vB:B. ∀p:P 〈vA,vB〉. P_io ? P' (f vA vB)) → 714 P_io ? P' (bindIO2 A B C e f). 715 #A B C P P' e f; nelim e; 716 ##[ #fn args k IH; #IH'; nwhd; #res; napply IH; napply IH'; 717 ## #v0; nelim v0; #v; nelim v; #vA vB Hv IH; napply IH; //; 718 ## //; 719 ##] nqed. 720 721 nlemma opt_bindIO_OK: ∀A,B. ∀P:B → Prop. ∀e:option A. ∀f: A → IO B. 722 (∀v:A. e = Some A v → P_io ? P (f v)) → 723 P_io ? P (bindIO A B e f). 724 #A B P e; nelim e; //; #v f H; napply H; //; 725 nqed. 726 727 nlemma bindIO_OK: ∀A,B. ∀P:B → Prop. ∀e:IO A. ∀f: A → IO B. 728 (∀v:A. P_io ? P (f v)) → 729 P_io ? P (bindIO A B e f). 730 #A B P e; nelim e; 731 ##[ #fn args k IH; #f H; nwhd; #res; napply IH; //; 732 ## #v f H; napply H; 733 ## //; 734 ##] nqed. 735 (* 736 nlemma bind_assoc_r: ∀A,B,C,e,f,g. 737 bindIO B C (bindIO A B e f) g = bindIO A C e (λx.bindIO B C (f x) g). 738 #A B C e f g; nelim e; 739 ##[ #fn args k IH; nwhd in ⊢ (???%); 740 nnormalize; 741 *) 742 743 nlemma extract_subset_pair_io: ∀A,B,C,P. ∀e:{e:A×B  P e}. ∀Q:A→B→IO C. ∀R:C→Prop. 744 (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → P_io ? R (Q a b)) → 745 P_io ? R (match eject ?? e with [ mk_pair a b ⇒ Q a b ]). 746 #A B C P e Q R; ncases e; #e'; ncases e'; nnormalize; 747 ##[ *; 748 ## #e''; ncases e''; #a b Pab H; nnormalize; /2/; 749 ##] nqed. 614 (* Interactions are function calls that return a value and do not change 615 the rest of the Clight program's state. *) 616 ndefinition io ≝ mk_interaction (ident × (list eventval)) eventval. 617 618 ndefinition do_io : ident → list eventval → IO io eventval ≝ 619 λfn,args. Interact io eventval 〈fn,args〉 (λres. Value io eventval res). 620 621 ndefinition ret: ∀T. T → (IO io T) ≝ 622 λT,x.(Value io T x). 623 624 (* Checking types of values given to / received from an external function call. *) 750 625 751 626 ndefinition check_eventval : ∀ev:eventval. ∀ty:typ. res (Σv:val. eventval_match ev ty v) ≝ … … 784 659 (* execution *) 785 660 786 nlet rec exec_step (ge:genv) (st:state) on st : (IO (Σr:trace × state. step ge st (\fst r) (\snd r))) ≝661 nlet rec exec_step (ge:genv) (st:state) on st : (IO io (Σr:trace × state. step ge st (\fst r) (\snd r))) ≝ 787 662 match st with 788 663 [ State f s k e m ⇒ … … 820 695 match fn_return f with 821 696 [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉) 822  _ ⇒ Some ? (Wrong ? )697  _ ⇒ Some ? (Wrong ??) 823 698 ] 824 699  Kcall _ _ _ _ ⇒ 825 700 match fn_return f with 826 701 [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉) 827  _ ⇒ Some ? (Wrong ? )702  _ ⇒ Some ? (Wrong ??) 828 703 ] 829 704  Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉) … … 838 713  Kfor3 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉) 839 714  Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉) 840  _ ⇒ Some ? (Wrong ? )715  _ ⇒ Some ? (Wrong ??) 841 716 ] 842 717  Scontinue ⇒ … … 853 728  Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉) 854 729  Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉) 855  _ ⇒ Some ? (Wrong ? )730  _ ⇒ Some ? (Wrong ??) 856 731 ] 857 732  Sbreak ⇒ … … 862 737  Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉) 863 738  Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉) 864  _ ⇒ Some ? (Wrong ? )739  _ ⇒ Some ? (Wrong ??) 865 740 ] 866 741  Sifthenelse a s1 s2 ⇒ Some ? ( … … 886 761 [ None ⇒ match fn_return f with 887 762 [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉) 888  _ ⇒ Some ? (Wrong ? )763  _ ⇒ Some ? (Wrong ??) 889 764 ] 890 765  Some a ⇒ Some ? ( … … 896 771 ! v ← exec_expr ge e m a;: 897 772 match v with [ Vint n ⇒ ret ? 〈E0, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉 898  _ ⇒ Wrong ? ])773  _ ⇒ Wrong ?? ]) 899 774  Slabel lbl s' ⇒ Some ? (ret ? 〈E0, State f s' k e m〉) 900 775  Sgoto lbl ⇒ 901 776 match find_label lbl (fn_body f) (call_cont k) with 902 777 [ Some sk' ⇒ match sk' with [ mk_pair s' k' ⇒ Some ? (ret ? 〈E0, State f s' k' e m〉) ] 903  None ⇒ Some ? (Wrong ? )778  None ⇒ Some ? (Wrong ??) 904 779 ] 905 780 ] … … 924 799 match res with 925 800 [ Vundef ⇒ Some ? (ret ? 〈E0, (State f Sskip k' e m)〉) 926  _ ⇒ Some ? (Wrong ? )801  _ ⇒ Some ? (Wrong ??) 927 802 ] 928 803  Some r' ⇒ … … 934 809 ] 935 810 ] 936  _ ⇒ Some ? (Wrong ? )811  _ ⇒ Some ? (Wrong ??) 937 812 ] 938 813 ]. nwhd; //; … … 1008 883 nqed. 1009 884 1010 nlet rec make_initial_state (p:program) : IO (Σs:state. initial_state p s) ≝885 nlet rec make_initial_state (p:program) : IO io (Σs:state. initial_state p s) ≝ 1011 886 let ge ≝ globalenv Genv ?? p in 1012 887 let m0 ≝ init_mem Genv ?? p in … … 1040 915 1041 916 nlet rec exec_steps (n:nat) (ge:genv) (s:state) : 1042 IO (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝917 IO io (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝ 1043 918 match is_final_state s with 1044 919 [ inl _ ⇒ Some ? (ret ? 〈E0, s〉)
Note: See TracChangeset
for help on using the changeset viewer.