Changeset 3035 for src/semantics.ma

Timestamp:

Mar 29, 2013, 3:21:49 PM (8 years ago)

Author:

mckinna

Message:

Tweak: tidied up ?/\ldots
Conceptual: better monadic threading of Error before final handling by print_exit/print_error: res should be implemented by ML-level raise/try_with.

File:

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

src/semantics.ma

@@ -34 +34 @@
      λ_.mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) …
   | lin_pass ⇒
-     λ_.mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ?
+     λ_.mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) …
   | assembly_pass ⇒
      λprog. let 〈code,sigma,policy〉 ≝ prog in
       mk_preclassified_system_pass … (ASM_preclassified_system code sigma policy) …
   | object_code_pass ⇒
-     λprog. mk_preclassified_system_pass ? (OC_preclassified_system prog) …
+     λprog. mk_preclassified_system_pass … (OC_preclassified_system prog) …
   ].
 %
@@ -49 +49 @@
 ≝
  λpass,prog,n,print_pass,print_event,print_error,print_exit.
- let pcs ≝ preclassified_system_of_pass pass prog in
+ let res ≝ 
+  let pcs ≝ preclassified_system_of_pass pass prog in
   let prog ≝ prog⌈syntax_of_pass pass ↦ ?⌉ in
   let g ≝ make_global … pcs prog in
-  match make_initial_state … pcs prog with
-  [ Error msg ⇒ print_error msg
-  | OK s0 ⇒
-     let i ≝ print_pass pass in
-     let 〈trace,res〉 ≝ observe_all_in_measurable n (pcs_to_cs pcs …) print_event [ ] s0 in
-     match res with
+  ! s0 ← make_initial_state … pcs prog ; 
+  let i ≝ print_pass pass in
+  let 〈trace,res〉 ≝ observe_all_in_measurable n (pcs_to_cs pcs …) print_event [ ] s0 in
+    res
+ in 
+    match res with
      [ OK n ⇒ print_exit n
-     | Error msg ⇒ print_error msg ]].
+     | Error msg ⇒ print_error msg ]
+.
 @pcs_ok
 qed.