Changeset 2442


Ignore:
Timestamp:
Nov 7, 2012, 6:12:20 PM (7 years ago)
Author:
piccolo
Message:

Traces repaired. (By Paolo)
Statement of lineariseProof in place.

Location:
src/joint
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2422 r2442  
    3838
    3939axiom ExternalMain : String.
    40 check save_frame
    4140
    4241definition make_initial_state :
     
    7675  | Init bl _ _ _ ⇒
    7776    match symbol_for_block … (ev_genv p) (mk_block Code bl) with
    78     [ Some f ⇒ cl_call f
     77    [ Some f ⇒ cl_call
    7978    | None ⇒ cl_other (* we don't care, as call will fail anyway *)
    8079    ]
     
    149148   (* as_pc ≝ *) cpointerDeq
    150149   (* as_pc_of ≝ *) (pc …)
    151    (* as_classifier ≝ *)
    152     (λs,cl.∃fn,stmt.
    153       fetch_statement ? p … (ev_genv p) (pc … s) = return 〈fn,stmt〉 ∧
    154       match stmt with
    155       [ sequential stp nxt ⇒
    156         ∃flow,s'.
    157         io_evaluate … (io_env p s) (eval_step … (ev_genv p) fn s stp) = return 〈flow, s'〉 ∧
    158         step_flow_classifier … flow = cl
    159       | final stp ⇒
    160         ∃flow.io_evaluate … (io_env p s) (eval_fin_step_pc … (ev_genv p) fn s stp) = return flow ∧
    161         fin_step_flow_classifier … flow = cl
     150   (* as_classify ≝ *)
     151    (λs.
     152      match (
     153        ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) ;
     154        match stmt with
     155        [ sequential stp nxt ⇒
     156          ! 〈flow, s'〉  ← io_evaluate … (io_env p s) (eval_step … (ev_genv p) fn s stp) ;
     157          return step_flow_classifier … flow
     158        | final stp ⇒
     159          ! flow ← io_evaluate … (io_env p s) (eval_fin_step_pc … (ev_genv p) fn s stp) ;
     160          return fin_step_flow_classifier … flow
     161        ]) with
     162      [ OK c ⇒ c
     163      | Error _ ⇒ cl_other
    162164      ])
    163165   (* as_label_of_pc ≝ *)
     
    172174      ∃fn,stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return 〈fn,sequential ?? stp nxt〉 ∧
    173175      succ_pc p p (pc … s1) nxt = return pc … s2)
    174    (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?).
     176   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?)
     177   (* as_call_ident_≝ *) ?. cases daemon (* TODO *) qed.
Note: See TracChangeset for help on using the changeset viewer.