Changeset 1214 for src/joint

Timestamp:

Sep 15, 2011, 2:27:50 PM (9 years ago)

Author:

sacerdot

Message:

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

File:

• src/joint/semantics.ma (modified) (2 diffs)

src/joint/semantics.ma

@@ -156 +156 @@
   let sp ≝ sub sp (val_of_memory_chunk chunk) in
   let st ≝ set_sp … (address_of_val sp) st in
-  (*CSC: no monadic notation here *)
-  bind ?? (opt_to_res ? (msg FailedStore) (loadv chunk (m … st) sp))
-   (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).*)
+  do v ← opt_to_res ? (msg FailedStore) (loadv chunk (m … st) sp);
+  do v ← Byte_of_val v;
+  OK ? 〈st,v〉).*)
 
 definition save_ra : ∀p. state p → label → res (state p) ≝
  λp,st,l.
   let 〈addrl,addrh〉 ≝ address_of_label … (m … st) l in
-  (* No monadic notation here *)
-  bind ?? (push … st addrl) (λst.push … st addrh).
+  do st ← push … st addrl;
+  push … st addrh.
 
 definition fetch_ra : ∀p.state p → res (state p × address) ≝
  λp,st.
-  (* No monadic notation here *)
-  bind ?? (pop … st) (λres. let 〈st,addrh〉 ≝ res in
-  bind ?? (pop … st) (λres. let 〈st,addrl〉 ≝ res in
-   OK ? 〈st, 〈addrl,addrh〉〉)).
+  do 〈st,addrh〉 ← pop … st;
+  do 〈st,addrl〉 ← pop … st;
+  OK ? 〈st, 〈addrl,addrh〉〉.
 
 axiom MissingSymbol : String.
@@ -289 +288 @@
 qed.
 
-definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option ((*CSC: why not res*) int) ≝
-  λglobals: list ident.
-  λp.
-  λexit.
-  λregistersno.
-  λst.
- (* CSC: monadic notation missing here *)
-  match fetch_statement … st with
-  [ Error _ ⇒ None ?
-  | OK s ⇒ 
-    match s with
-      [ joint_st_return ⇒
-        match fetch_ra … st with
-         [ Error _ ⇒ None ?
-         | OK st_l ⇒
-           let 〈st,l〉 ≝ st_l in
-           if eq_address l exit then
-             (* CSC: monadic notation missing here *)
-             match fetch_result globals p st registersno with
-             [ Error _ ⇒ None ?
-             | OK val ⇒
-                match val with
-                 [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
-                 | _ ⇒ None ?]]
-           else
-            None ? ]
-      | _ ⇒ None ? ]].
+definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option int ≝
+  λglobals,p,exit,registersno,st. res_to_opt … (
+  do s ← fetch_statement … st;
+  match s with
+   [ joint_st_return ⇒
+      do 〈st,l〉 ← fetch_ra … st;
+      if eq_address l exit then
+       do val ← fetch_result globals p st registersno;
+       match val with
+        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. OK ? i) (Error ? [])
+        | _ ⇒ Error ? []]
+      else
+       Error ? []
+   | _ ⇒ Error ? []]).
 
 definition joint_exec: ∀globals:list ident. sem_params2 globals → address → nat → execstep io_out io_in ≝