Changeset 2186 for src/joint/Traces.ma


Ignore:
Timestamp:
Jul 16, 2012, 4:59:09 PM (8 years ago)
Author:
tranquil
Message:

updated joint semantics

File:
1 moved

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r1976 r2186  
    11include "joint/semantics_paolo.ma".
    2 include "common/StructuredTraces.ma".
    32
    4 definition stmt_classifier :
    5   ∀p : params.∀globals.
    6     (ext_step p → status_class) →
    7     (ext_fin_stmt p → status_class) →
    8     joint_statement p globals → status_class
    9   ≝ λp,globals,ext_step_classifier,ext_fin_step_classifier,s.
    10   match s with
    11   [ sequential stp _ ⇒
    12     match stp with
    13     [ COND _ _ ⇒ cl_jump
    14     | extension ext_s ⇒ ext_step_classifier ext_s
    15     | CALL_ID _ _ _ ⇒ cl_call (* Paolo : this does not take into account external calls! *)
    16     | _ ⇒ cl_other
    17     ]
    18   | final stp ⇒
    19     match stp with
    20     [ RETURN ⇒ cl_return
    21     | extension_fin ext_s ⇒ ext_fin_step_classifier ext_s
    22     | _ ⇒ cl_other
    23     ]
    24   ].
     3record evaluation_params : Type[1] ≝
     4 { globals: list ident
     5 ; sparams:> sem_params
     6 ; exit: cpointer
     7 ; ev_genv: genv globals sparams
     8 ; io_env : state sparams → ∀o:io_out.res (io_in o)
     9 } .
     10
     11(*record classifier_params : Type[1] ≝
     12  { cl_pars :> evaluation_parameters
     13  ; cl_ext_step : ext_step cl_pars → status_class
     14  ; cl_ext_fin_stmt : ext_fin_stmt cl_pars → status_class
     15  }.*)
     16
    2517
    2618definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
     
    3022]
    3123qed.
    32  
     24
     25let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
     26  match c with
     27  [ Value x ⇒ OK … x
     28  | Interact o f ⇒
     29    ! i ← env o ;
     30    io_evaluate O I X env (f i)
     31  | Wrong e ⇒ Error … e
     32  ].
     33
     34definition cost_label_of_stmt :
     35  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
     36  λp,s.match s with
     37  [ sequential s _ ⇒
     38    match s with
     39    [ step_seq s ⇒
     40      match s with
     41      [ COST_LABEL lbl ⇒ Some ? lbl
     42      | _ ⇒ None ?
     43      ]
     44    | _ ⇒ None ?
     45    ]
     46  | _ ⇒ None ?
     47  ].
     48
    3349definition joint_abstract_status :
    34  ∀p : evaluation_parameters.
    35  (ext_step p → status_class) →
    36  (ext_fin_stmt p → status_class) →
    37  abstract_status ≝
    38  λp,ext_step_cl,ext_fin_step_cl.
     50 ∀p : evaluation_params.
     51 abstract_status ≝
     52 λp.
    3953 mk_abstract_status
    4054   (* as_status ≝ *) (state_pc p)
    41    (* as_execute ≝ *) (λs1,s2.eval_state … p (genv2 p) s1 = return s2)
     55   (* as_execute ≝ *)
     56    (λs1,s2.io_evaluate … (io_env p s1) (eval_state … p (ev_genv p) s1) = return s2)
    4257   (* as_pc ≝ *) cpointerDeq
    4358   (* as_pc_of ≝ *) (pc …)
    4459   (* as_classifier ≝ *)
    45     (λs,cl.∃stmt.fetch_statement ? p … (genv2 p) (pc … s) = return stmt ∧
    46      stmt_classifier … ext_step_cl ext_fin_step_cl stmt = cl)
     60    (λs,cl.∃stmt.fetch_statement ? p … (ev_genv p) (pc … s) = return stmt ∧
     61     stmt_classifier … stmt = cl)
    4762   (* as_label_of_pc ≝ *)
    4863    (λpc.
    49       match fetch_statement ? p … (genv2 p) pc with
    50       [ OK stmt ⇒
    51         match stmt with
    52         [ sequential s _ ⇒
    53           match s with
    54           [ COST_LABEL l ⇒ Some ? l
    55           | _ ⇒ None ?
    56           ]
    57         | _ ⇒ None ?
    58         ]
     64      match fetch_statement ? p … (ev_genv p) pc with
     65      [ OK stmt ⇒ cost_label_of_stmt … stmt
    5966      | _ ⇒ None ?
    6067      ])
    6168   (* as_after_return ≝ *)
    62     (λs1,s2. (* Paolo: considering sequential calls, tailcalls are out of the picture for now *)
    63       ∃stp,nxt.fetch_statement ? p … (genv2 p) (pc … s1) = return (sequential ?? stp nxt) ∧
     69    (λs1,s2.
     70      (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *)
     71      ∃stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return (sequential ?? stp nxt) ∧
    6472      succ_pc p p (pc … s1) nxt = return pc … s2)
    65    (* as_final ≝ *) (λs.is_final (globals ?) p (genv2 p) (exit p) s ≠ None ?).
     73   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?).
Note: See TracChangeset for help on using the changeset viewer.