Changeset 175 for C-semantics/Events.ma


Ignore:
Timestamp:
Oct 13, 2010, 12:19:22 PM (10 years ago)
Author:
campbell
Message:

Add cost labels, with the semantics that the label is added to the
event trace.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Events.ma

    r3 r175  
    2424include "datatypes/list.ma".
    2525include "extralib.ma".
     26include "CostLabel.ma".
    2627
    2728(* * The observable behaviour of programs is stated in terms of
     
    4041  | EVfloat: float -> eventval.
    4142
    42 nrecord event : Type := {
    43   ev_name: ident;
    44   ev_args: list eventval;
    45   ev_res: eventval
    46 }.
     43ninductive event : Type ≝
     44  | EVcost: costlabel → event
     45  | EVextcall: ∀ev_name: ident. ∀ev_args: list eventval. ∀ev_res: eventval. event.
    4746
    4847(* * The dynamic semantics for programs collect traces of events.
     
    5352ndefinition E0 : trace := nil ?.
    5453
     54ndefinition Echarge : costlabel → trace ≝
     55λlabel. EVcost label :: (nil ?).
     56
    5557ndefinition Eextcall : ident → list eventval → eventval → trace ≝
    5658             λname: ident. λargs: list eventval. λres: eventval.
    57   mk_event name args res :: (nil ?).
     59  EVextcall name args res :: (nil ?).
    5860
    5961ndefinition Eapp : trace → trace → trace ≝ λt1,t2. t1 @ t2.
Note: See TracChangeset for help on using the changeset viewer.