Changeset 3035


Ignore:
Timestamp:
Mar 29, 2013, 3:21:49 PM (4 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/semantics.ma

    r3014 r3035  
    3434     λ_.mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) …
    3535  | lin_pass ⇒
    36      λ_.mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ?
     36     λ_.mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics)
    3737  | assembly_pass ⇒
    3838     λprog. let 〈code,sigma,policy〉 ≝ prog in
    3939      mk_preclassified_system_pass … (ASM_preclassified_system code sigma policy) …
    4040  | object_code_pass ⇒
    41      λprog. mk_preclassified_system_pass ? (OC_preclassified_system prog) …
     41     λprog. mk_preclassified_system_pass (OC_preclassified_system prog) …
    4242  ].
    4343%
     
    4949
    5050 λpass,prog,n,print_pass,print_event,print_error,print_exit.
    51  let pcs ≝ preclassified_system_of_pass pass prog in
     51 let res ≝
     52  let pcs ≝ preclassified_system_of_pass pass prog in
    5253  let prog ≝ prog⌈syntax_of_pass pass ↦ ?⌉ in
    5354  let g ≝ make_global … pcs prog in
    54   match make_initial_state … pcs prog with
    55   [ Error msg ⇒ print_error msg
    56   | OK s0 ⇒
    57      let i ≝ print_pass pass in
    58      let 〈trace,res〉 ≝ observe_all_in_measurable n (pcs_to_cs pcs …) print_event [ ] s0 in
    59      match res with
     55  ! s0 ← make_initial_state … pcs prog ;
     56  let i ≝ print_pass pass in
     57  let 〈trace,res〉 ≝ observe_all_in_measurable n (pcs_to_cs pcs …) print_event [ ] s0 in
     58    res
     59 in
     60    match res with
    6061     [ OK n ⇒ print_exit n
    61      | Error msg ⇒ print_error msg ]].
     62     | Error msg ⇒ print_error msg ]
     63.
    6264@pcs_ok
    6365qed.
Note: See TracChangeset for help on using the changeset viewer.