Changeset 208 for Csemantics
 Timestamp:
 Nov 1, 2010, 11:10:46 AM (10 years ago)
 Location:
 Csemantics
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/CexecIO.ma
r189 r208 622 622 match s with 623 623 [ Sassign a1 a2 ⇒ Some ? ( 624 ! 〈l,tr1〉 ← exec_lvalue ge e m a1; :625 ! 〈v2,tr2〉 ← exec_expr ge e m a2; :626 ! m' ← store_value_of_type' (typeof a1) m l v2; :624 ! 〈l,tr1〉 ← exec_lvalue ge e m a1; 625 ! 〈v2,tr2〉 ← exec_expr ge e m a2; 626 ! m' ← store_value_of_type' (typeof a1) m l v2; 627 627 ret ? 〈tr1⧺tr2, State f Sskip k e m'〉) 628 628  Scall lhs a al ⇒ Some ? ( 629 ! 〈vf,tr2〉 ← exec_expr ge e m a; :630 ! 〈vargs,tr3〉 ← exec_exprlist ge e m al; :631 ! fd ← find_funct ? ? ge vf; :632 ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (typeof a)); :629 ! 〈vf,tr2〉 ← exec_expr ge e m a; 630 ! 〈vargs,tr3〉 ← exec_exprlist ge e m al; 631 ! fd ← find_funct ? ? ge vf; 632 ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (typeof a)); 633 633 (* 634 634 ! k' ← match lhs with 635 635 [ None ⇒ ret ? (Kcall (None ?) f e k) 636 636  Some lhs' ⇒ 637 ! locofs ← exec_lvalue ge e m lhs'; :637 ! locofs ← exec_lvalue ge e m lhs'; 638 638 ret ? (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k) 639 ]; :639 ]; 640 640 ret ? 〈E0, Callstate fd vargs k' m〉) 641 641 *) … … 643 643 [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉 644 644  Some lhs' ⇒ 645 ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs'; :645 ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs'; 646 646 ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉 647 647 ]) … … 662 662  Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉) 663 663  Kdowhile a s' k' ⇒ Some ? ( 664 ! 〈v,tr〉 ← exec_expr ge e m a; :665 ! b ← bool_of_val_3 v (typeof a); :664 ! 〈v,tr〉 ← exec_expr ge e m a; 665 ! b ← bool_of_val_3 v (typeof a); 666 666 match b with 667 667 [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉 … … 678 678  Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉) 679 679  Kdowhile a s' k' ⇒ Some ? ( 680 ! 〈v,tr〉 ← exec_expr ge e m a; :681 ! b ← bool_of_val_3 v (typeof a); :680 ! 〈v,tr〉 ← exec_expr ge e m a; 681 ! b ← bool_of_val_3 v (typeof a); 682 682 match b with 683 683 [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉 … … 698 698 ] 699 699  Sifthenelse a s1 s2 ⇒ Some ? ( 700 ! 〈v,tr〉 ← exec_expr ge e m a; :701 ! b ← bool_of_val_3 v (typeof a); :700 ! 〈v,tr〉 ← exec_expr ge e m a; 701 ! b ← bool_of_val_3 v (typeof a); 702 702 ret ? 〈tr, State f (if b then s1 else s2) k e m〉) 703 703  Swhile a s' ⇒ Some ? ( 704 ! 〈v,tr〉 ← exec_expr ge e m a; :705 ! b ← bool_of_val_3 v (typeof a); :704 ! 〈v,tr〉 ← exec_expr ge e m a; 705 ! b ← bool_of_val_3 v (typeof a); 706 706 ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m 707 707 else State f Sskip k e m〉) … … 710 710 match is_Sskip a1 with 711 711 [ inl _ ⇒ Some ? ( 712 ! 〈v,tr〉 ← exec_expr ge e m a2; :713 ! b ← bool_of_val_3 v (typeof a2); :712 ! 〈v,tr〉 ← exec_expr ge e m a2; 713 ! b ← bool_of_val_3 v (typeof a2); 714 714 ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉) 715 715  inr _ ⇒ Some ? (ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉) … … 722 722 ] 723 723  Some a ⇒ Some ? ( 724 ! u ← is_not_void (fn_return f); :725 ! 〈v,tr〉 ← exec_expr ge e m a; :724 ! u ← is_not_void (fn_return f); 725 ! 〈v,tr〉 ← exec_expr ge e m a; 726 726 ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉) 727 727 ] 728 728  Sswitch a sl ⇒ Some ? ( 729 ! 〈v,tr〉 ← exec_expr ge e m a; :729 ! 〈v,tr〉 ← exec_expr ge e m a; 730 730 match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉 731 731  _ ⇒ Wrong ??? ]) … … 742 742 [ Internal f ⇒ Some ? ( 743 743 match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒ 744 ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs; :744 ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs; 745 745 ret ? 〈E0, State f (fn_body f) k e m2〉 746 746 ]) 747 747  External f argtys retty ⇒ Some ? ( 748 ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys); :749 ! evres ← do_io f evargs; :750 ! vres ← check_eventval evres (proj_sig_res (signature_of_type argtys retty)); :748 ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys); 749 ! evres ← do_io f evargs; 750 ! vres ← check_eventval evres (proj_sig_res (signature_of_type argtys retty)); 751 751 ret ? 〈(Eextcall f evargs evres), Returnstate vres k m〉) 752 752 ] … … 763 763 match r' with [ mk_pair l ty ⇒ 764 764 Some ? ( 765 ! m' ← store_value_of_type' ty m l res; :765 ! m' ← store_value_of_type' ty m l res; 766 766 ret ? 〈E0, (State f Sskip k' e m')〉) 767 767 ] … … 846 846 let m0 ≝ init_mem Genv ?? p in 847 847 Some ? ( 848 ! 〈sp,b〉 ← find_symbol ? ? ge (prog_main ?? p); :849 ! u ← opt_to_io … (match ms_eq_dec sp Code with [ inl _ ⇒ Some ? something  inr _ ⇒ None ? ]); :850 ! f ← find_funct_ptr ? ? ge b; :848 ! 〈sp,b〉 ← find_symbol ? ? ge (prog_main ?? p); 849 ! u ← opt_to_io … (match ms_eq_dec sp Code with [ inl _ ⇒ Some ? something  inr _ ⇒ None ? ]); 850 ! f ← find_funct_ptr ? ? ge b; 851 851 ret ? (Callstate f (nil ?) Kstop m0)). 852 852 nwhd; … … 884 884 [ O ⇒ Some ? (ret ? 〈E0, s〉) 885 885  S n' ⇒ Some ? ( 886 ! 〈t,s'〉 ← exec_step ge s; :886 ! 〈t,s'〉 ← exec_step ge s; 887 887 (* ! 〈t,s'〉 ← match s with 888 888 [ State f s k e m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (State f s k e (mk_mem c n p)) ] 889 889  Callstate fd args k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Callstate fd args k (mk_mem c n p)) ] 890 890  Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Returnstate r k (mk_mem c n p)) ] 891 ] ; :*)891 ] ;*) 892 892 ! 〈t',s''〉 ← match s' with 893 893 [ State f s k e m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (State f s k e (mk_mem c n p)) ] 894 894  Callstate fd args k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Callstate fd args k (mk_mem c n p)) ] 895 895  Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Returnstate r k (mk_mem c n p)) ] 896 ] ; :897 (* ! 〈t',s''〉 ← exec_steps n' ge s'; :*)896 ] ; 897 (* ! 〈t',s''〉 ← exec_steps n' ge s';*) 898 898 ret ? 〈t ⧺ t',s''〉) 899 899 ] … … 915 915 [ O ⇒ OK ? 〈E0, s〉 916 916  S n' ⇒ 917 〈t,s'〉 ← exec_step ge s; :918 〈t',s''〉 ← exec_steps_without_proof n' ge s'; :917 〈t,s'〉 ← exec_step ge s; 918 〈t',s''〉 ← exec_steps_without_proof n' ge s'; 919 919 OK ? 〈t ⧺ t',s''〉 920 920 ] … … 940 940 941 941 ndefinition exec_inf : program → execution ≝ 942 λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; :ret ? 〈E0,sig_eject ?? s〉).943 942 λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,sig_eject ?? s〉). 943 
Csemantics/IOMonad.ma
r189 r208 33 33 34 34 (* If the original definitions are vague enough, do I need to do this? *) 35 notation > "! ident v ← e; :e'" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.36 notation > "! ident v : ty ← e; :e'" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.37 notation < "vbox(! \nbsp ident v ← e; :e')" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.38 notation < "vbox(! \nbsp ident v : ty ← e; :e')" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.39 notation > "! 〈ident v1, ident v2〉 ← e; :e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.40 notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e; :e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.41 notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e; :e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.42 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; : e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty2}.λ${ident v2} : ${ty2}.${e'})}.35 notation > "! ident v ← e; e'" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}. 36 notation > "! ident v : ty ← e; e'" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}. 37 notation < "vbox(! \nbsp ident v ← e; break e')" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}. 38 notation < "vbox(! \nbsp ident v : ty ← e; break e')" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}. 39 notation > "! 〈ident v1, ident v2〉 ← e; e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}. 40 notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e; e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}. 41 notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}. 42 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}. 43 43 interpretation "IO monad bind" 'bindIO e f = (bindIO ???? e f). 44 44 interpretation "IO monad pair bind" 'bindIO2 e f = (bindIO2 ????? e f).
Note: See TracChangeset
for help on using the changeset viewer.