Ignore:
Timestamp:
Feb 9, 2011, 11:49:17 AM (10 years ago)
Author:
campbell
Message:

Port Clight semantics to the new-new matita syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Events.ma

    r478 r487  
    2222(*include "Floats.ma".*)
    2323include "Values.ma".
    24 include "datatypes/list.ma".
     24include "basics/list.ma".
    2525include "extralib.ma".
    2626include "CostLabel.ma".
     
    3737  world. *)
    3838
    39 ninductive eventval: Type :=
     39inductive eventval: Type[0] :=
    4040  | EVint: int -> eventval
    4141  | EVfloat: float -> eventval.
    4242
    43 ninductive event : Type
     43inductive event : Type[0]
    4444  | EVcost: costlabel → event
    4545  | EVextcall: ∀ev_name: ident. ∀ev_args: list eventval. ∀ev_res: eventval. event.
     
    4848  Traces are of two kinds: finite (type [trace]) or infinite (type [traceinf]). *)
    4949
    50 ndefinition trace := list event.
    51 
    52 ndefinition E0 : trace := nil ?.
    53 
    54 ndefinition Echarge : costlabel → trace ≝
     50definition trace := list event.
     51
     52definition E0 : trace := nil ?.
     53
     54definition Echarge : costlabel → trace ≝
    5555λlabel. EVcost label :: (nil ?).
    5656
    57 ndefinition Eextcall : ident → list eventval → eventval → trace ≝
     57definition Eextcall : ident → list eventval → eventval → trace ≝
    5858             λname: ident. λargs: list eventval. λres: eventval.
    5959  EVextcall name args res :: (nil ?).
    6060
    61 ndefinition Eapp : trace → trace → trace ≝ λt1,t2. t1 @ t2.
    62 
    63 ncoinductive traceinf : Type :=
     61definition Eapp : trace → trace → trace ≝ λt1,t2. t1 @ t2.
     62
     63coinductive traceinf : Type[0] :=
    6464  | Econsinf: event -> traceinf -> traceinf.
    6565
    66 nlet rec Eappinf (t: trace) (T: traceinf) on t : traceinf :=
     66let rec Eappinf (t: trace) (T: traceinf) on t : traceinf :=
    6767  match t with
    6868  [ nil => T
     
    8787Infix "***" := Eappinf (at level 60, right associativity).
    8888*)
    89 nlemma E0_left: ∀t. E0 ⧺ t = t.
    90 //; nqed.
    91 
    92 nlemma E0_right: ∀t. t ⧺ E0 = t.
    93 napply append_nil; nqed.
    94 
    95 nlemma Eapp_assoc: ∀t1,t2,t3. (t1 ⧺ t2) ⧺ t3 = t1 ⧺ (t2 ⧺ t3).
    96 napply associative_append; nqed.
    97 
    98 nlemma Eapp_E0_inv: ∀t1,t2. t1 ⧺ t2 = E0 → t1 = E0 ∧ t2 = E0.
    99 napply nil_append_nil_both; nqed.
     89lemma E0_left: ∀t. E0 ⧺ t = t.
     90//; qed.
     91
     92lemma E0_right: ∀t. t ⧺ E0 = t.
     93@append_nil qed.
     94
     95lemma Eapp_assoc: ∀t1,t2,t3. (t1 ⧺ t2) ⧺ t3 = t1 ⧺ (t2 ⧺ t3).
     96@associative_append qed.
     97
     98lemma Eapp_E0_inv: ∀t1,t2. t1 ⧺ t2 = E0 → t1 = E0 ∧ t2 = E0.
     99@nil_append_nil_both qed.
    100100 
    101 nlemma E0_left_inf: ∀T. E0 ⧻ T = T.
    102 //; nqed.
    103 
    104 nlemma Eappinf_assoc: ∀t1,t2,T. (t1 ⧺ t2) ⧻ T = t1 ⧻ (t2 ⧻ T).
    105 #t1; nelim t1; #t2 T; nnormalize; //; nqed.
     101lemma E0_left_inf: ∀T. E0 ⧻ T = T.
     102//; qed.
     103
     104lemma Eappinf_assoc: ∀t1,t2,T. (t1 ⧺ t2) ⧻ T = t1 ⧻ (t2 ⧻ T).
     105#t1 elim t1; #t2 #T normalize; //; qed.
    106106
    107107(*
     
    137137  infinite concatenations of nonempty finite traces. *)
    138138
    139 ncoinductive traceinf': Type
     139coinductive traceinf': Type[0]
    140140  | Econsinf': ∀t: trace. ∀T: traceinf'. t ≠ E0 → traceinf'.
    141141
    142 ndefinition split_traceinf' : ∀t:trace. traceinf' → t ≠ E0 → event × traceinf' ≝
     142definition split_traceinf' : ∀t:trace. traceinf' → t ≠ E0 → event × traceinf' ≝
    143143λt,T.
    144144  match t return λt0.t0 ≠ E0 → ? with
     
    150150     ]) (refl ? t')
    151151  ].
    152 ##[ *; #NE; napply False_rect_Type0; napply NE; napply refl;
    153 ##| @; #E'; nrewrite > E' in E; #E; nwhd in E:(??%%); ndestruct (E);
    154 ##] nqed.
    155 
    156 nlet corec traceinf_of_traceinf' (T': traceinf') : traceinf ≝
     152[ *; #NE @False_rect_Type0 @NE @refl
     153| % #E' >E' in E #E whd in E:(??%%); destruct (E);
     154] qed.
     155
     156let corec traceinf_of_traceinf' (T': traceinf') : traceinf ≝
    157157  match T' with
    158158  [ Econsinf' t T'' NOTEMPTY ⇒
    159       match split_traceinf' t T'' NOTEMPTY with [ mk_pair e tl ⇒
     159      match split_traceinf' t T'' NOTEMPTY with [ pair e tl ⇒
    160160      Econsinf e (traceinf_of_traceinf' tl) ]
    161161  ].
    162162
    163 nremark unroll_traceinf':
     163lemma unroll_traceinf':
    164164  ∀T. T = match T with [ Econsinf' t T' NE ⇒ Econsinf' t T' NE ].
    165 #T; ncases T; //; nqed.
    166 
    167 nremark unroll_traceinf:
     165#T cases T; //; qed.
     166
     167lemma unroll_traceinf:
    168168  ∀T. T = match T with [ Econsinf t T' ⇒ Econsinf t T' ].
    169 #T; ncases T; //;
    170 nqed.
    171 
    172 nlemma traceinf_traceinfp_app:
     169#T cases T #ev #tr @refl (* XXX //; *)
     170qed.
     171
     172lemma traceinf_traceinfp_app:
    173173  ∀t,T,NE.
    174174  traceinf_of_traceinf' (Econsinf' t T NE) = t ⧻ traceinf_of_traceinf' T.
    175 #t; nelim t;
    176 ##[ #T NE; ncases NE; #NE'; napply False_ind; napply NE'; napply refl;
    177 ##| #h t'; ncases t'; ##[ ##2: #h' t''; ##] #IH T NE;
    178     nrewrite > (unroll_traceinf (traceinf_of_traceinf' ?));
    179     nwhd in ⊢ (??%?); //; nrewrite > (IH …); napply refl;
    180 ##] nqed.
     175#t elim t;
     176[ #T #NE cases NE; #NE' @False_ind @NE' @refl
     177| #h #t' cases t'; [ 2: #h' #t'' ] #IH #T #NE
     178    >(unroll_traceinf (traceinf_of_traceinf' ?))
     179    whd in ⊢ (??%?); //; >(IH …) @refl
     180] qed.
    181181
    182182(* <<< *)
     
    187187  from the operating system. *)
    188188
    189 ninductive eventval_match: eventval -> typ -> val -> Prop :=
     189inductive eventval_match: eventval -> typ -> val -> Prop :=
    190190  | ev_match_int:
    191191      ∀i. eventval_match (EVint i) ASTint (Vint i)
     
    193193      ∀f. eventval_match (EVfloat f) ASTfloat (Vfloat f).
    194194
    195 ninductive eventval_list_match: list eventval -> list typ -> list val -> Prop :=
     195inductive eventval_list_match: list eventval -> list typ -> list val -> Prop :=
    196196  | evl_match_nil:
    197197      eventval_list_match (nil ?) (nil ?) (nil ?)
     
    202202      eventval_list_match (ev1::evl) (ty1::tyl) (v1::vl).
    203203
    204 ninductive event_match:
     204inductive event_match:
    205205         external_function -> list val -> trace -> val -> Prop :=
    206206  event_match_intro:
Note: See TracChangeset for help on using the changeset viewer.