Changeset 208


Ignore:
Timestamp:
Nov 1, 2010, 11:10:46 AM (9 years ago)
Author:
campbell
Message:

Fix up IO monad syntax.

Location:
C-semantics
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r189 r208  
    622622  match s with
    623623  [ 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;
    627627    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉)
    628628  | 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));
    633633(*
    634634    ! k' ← match lhs with
    635635         [ None ⇒ ret ? (Kcall (None ?) f e k)
    636636         | Some lhs' ⇒
    637            ! locofs ← exec_lvalue ge e m lhs';:
     637           ! locofs ← exec_lvalue ge e m lhs';
    638638           ret ? (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k)
    639          ];:
     639         ];
    640640    ret ? 〈E0, Callstate fd vargs k' m〉)
    641641*)
     
    643643         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
    644644         | Some lhs' ⇒
    645            ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs';:
     645           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs';
    646646           ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
    647647         ])
     
    662662      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
    663663      | 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);
    666666          match b with
    667667          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
     
    678678      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
    679679      | 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);
    682682          match b with
    683683          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
     
    698698      ]
    699699  | 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);
    702702      ret ? 〈tr, State f (if b then s1 else s2) k e m〉)
    703703  | 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);
    706706      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
    707707                      else State f Sskip k e m〉)
     
    710710      match is_Sskip a1 with
    711711      [ 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);
    714714          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉)
    715715      | inr _ ⇒ Some ? (ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉)
     
    722722      ]
    723723    | 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;
    726726        ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉)
    727727    ]
    728728  | Sswitch a sl ⇒ Some ? (
    729       ! 〈v,tr〉 ← exec_expr ge e m a;:
     729      ! 〈v,tr〉 ← exec_expr ge e m a;
    730730      match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
    731731                   | _ ⇒ Wrong ??? ])
     
    742742  [ Internal f ⇒ Some ? (
    743743    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;
    745745      ret ? 〈E0, State f (fn_body f) k e m2〉
    746746    ])
    747747  | 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));
    751751      ret ? 〈(Eextcall f evargs evres), Returnstate vres k m〉)
    752752  ]
     
    763763      match r' with [ mk_pair l ty ⇒
    764764        Some ? (
    765           ! m' ← store_value_of_type' ty m l res;:
     765          ! m' ← store_value_of_type' ty m l res;
    766766          ret ? 〈E0, (State f Sskip k' e m')〉)
    767767      ]
     
    846846  let m0 ≝ init_mem Genv ?? p in
    847847  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;
    851851    ret ? (Callstate f (nil ?) Kstop m0)).
    852852nwhd;
     
    884884  [ O ⇒ Some ? (ret ? 〈E0, s〉)
    885885  | S n' ⇒ Some ? (
    886       ! 〈t,s'〉 ← exec_step ge s;:
     886      ! 〈t,s'〉 ← exec_step ge s;
    887887(*      ! 〈t,s'〉 ← match s with
    888888                 [ 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)) ]
    889889                 | 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)) ]
    890890                 | 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                 ] ;*)
    892892      ! 〈t',s''〉 ← match s' with
    893893                 [ 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)) ]
    894894                 | 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)) ]
    895895                 | 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';*)
    898898      ret ? 〈t ⧺ t',s''〉)
    899899  ]
     
    915915  [ O ⇒ OK ? 〈E0, s〉
    916916  | 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';
    919919      OK ? 〈t ⧺ t',s''〉
    920920  ]
     
    940940
    941941ndefinition 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
  • C-semantics/IOMonad.ma

    r189 r208  
    3333
    3434(* 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'})}.
     35notation > "! ident v ← e; e'" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
     36notation > "! ident v : ty ← e; e'" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.
     37notation < "vbox(! \nbsp ident v ← e; break e')" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
     38notation < "vbox(! \nbsp ident v : ty ← e; break e')" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.
     39notation > "! 〈ident v1, ident v2〉 ← e; e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
     40notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e; e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
     41notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
     42notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
    4343interpretation "IO monad bind" 'bindIO e f = (bindIO ???? e f).
    4444interpretation "IO monad pair bind" 'bindIO2 e f = (bindIO2 ????? e f).
Note: See TracChangeset for help on using the changeset viewer.