Changeset 1214


Ignore:
Timestamp:
Sep 15, 2011, 2:27:50 PM (8 years ago)
Author:
sacerdot
Message:

res_to_opt function added to common/Errors and used in joint/semantics to make
the code look nicer

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r1125 r1214  
    238238#A #m #P #e elim e; /2/;
    239239qed.
     240
     241definition res_to_opt : ∀A:Type[0]. res A → option A ≝
     242 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
  • src/joint/semantics.ma

    r1213 r1214  
    156156  let sp ≝ sub sp (val_of_memory_chunk chunk) in
    157157  let st ≝ set_sp … (address_of_val sp) st in
    158   (*CSC: no monadic notation here *)
    159   bind ?? (opt_to_res ? (msg FailedStore) (loadv chunk (m … st) sp))
    160    (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).*)
     158  do v ← opt_to_res ? (msg FailedStore) (loadv chunk (m … st) sp);
     159  do v ← Byte_of_val v;
     160  OK ? 〈st,v〉).*)
    161161
    162162definition save_ra : ∀p. state p → label → res (state p) ≝
    163163 λp,st,l.
    164164  let 〈addrl,addrh〉 ≝ address_of_label … (m … st) l in
    165   (* No monadic notation here *)
    166   bind ?? (push … st addrl) (λst.push … st addrh).
     165  do st ← push … st addrl;
     166  push … st addrh.
    167167
    168168definition fetch_ra : ∀p.state p → res (state p × address) ≝
    169169 λp,st.
    170   (* No monadic notation here *)
    171   bind ?? (pop … st) (λres. let 〈st,addrh〉 ≝ res in
    172   bind ?? (pop … st) (λres. let 〈st,addrl〉 ≝ res in
    173    OK ? 〈st, 〈addrl,addrh〉〉)).
     170  do 〈st,addrh〉 ← pop … st;
     171  do 〈st,addrl〉 ← pop … st;
     172  OK ? 〈st, 〈addrl,addrh〉〉.
    174173
    175174axiom MissingSymbol : String.
     
    289288qed.
    290289
    291 definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option ((*CSC: why not res*) int) ≝
    292   λglobals: list ident.
    293   λp.
    294   λexit.
    295   λregistersno.
    296   λst.
    297  (* CSC: monadic notation missing here *)
    298   match fetch_statement … st with
    299   [ Error _ ⇒ None ?
    300   | OK s ⇒
    301     match s with
    302       [ joint_st_return ⇒
    303         match fetch_ra … st with
    304          [ Error _ ⇒ None ?
    305          | OK st_l ⇒
    306            let 〈st,l〉 ≝ st_l in
    307            if eq_address l exit then
    308              (* CSC: monadic notation missing here *)
    309              match fetch_result globals p st registersno with
    310              [ Error _ ⇒ None ?
    311              | OK val ⇒
    312                 match val with
    313                  [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
    314                  | _ ⇒ None ?]]
    315            else
    316             None ? ]
    317       | _ ⇒ None ? ]].
     290definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option int ≝
     291  λglobals,p,exit,registersno,st. res_to_opt … (
     292  do s ← fetch_statement … st;
     293  match s with
     294   [ joint_st_return ⇒
     295      do 〈st,l〉 ← fetch_ra … st;
     296      if eq_address l exit then
     297       do val ← fetch_result globals p st registersno;
     298       match val with
     299        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. OK ? i) (Error ? [])
     300        | _ ⇒ Error ? []]
     301      else
     302       Error ? []
     303   | _ ⇒ Error ? []]).
    318304
    319305definition joint_exec: ∀globals:list ident. sem_params2 globals → address → nat → execstep io_out io_in ≝
Note: See TracChangeset for help on using the changeset viewer.