Changeset 1316 for src/RTLabs/syntax.ma


Ignore:
Timestamp:
Oct 7, 2011, 12:26:39 PM (8 years ago)
Author:
campbell
Message:

Merge in id-lookup-branch to trunk.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src

  • src/RTLabs/syntax.ma

    r1307 r1316  
    2626.
    2727
     28definition labels_P : (label → Prop) → statement → Prop ≝
     29λP,s. match s with
     30[ St_skip l ⇒ P l
     31| St_cost _ l ⇒ P l
     32| St_const _ _ l ⇒ P l
     33| St_op1 _ _ _ l ⇒ P l
     34| St_op2 _ _ _ _ l ⇒ P l
     35| St_load _ _ _ l ⇒ P l
     36| St_store _ _ _ l ⇒ P l
     37| St_call_id _ _ _ l ⇒ P l
     38| St_call_ptr _ _ _ l ⇒ P l
     39| St_tailcall_id _ _ ⇒ True
     40| St_tailcall_ptr _ _ ⇒ True
     41| St_cond _ l1 l2 ⇒ P l1 ∧ P l2
     42| St_jumptable _ ls ⇒ All ? P ls
     43| St_return ⇒ True
     44].
     45
     46lemma labels_P_mp : ∀P,Q. (∀l. P l → Q l) → ∀s.labels_P P s → labels_P Q s.
     47#P #Q #H * /3/
     48#r #l #l' * /3/
     49qed.
     50
     51definition labels_present : graph statement → statement → Prop ≝
     52λg,s. labels_P (present ?? g) s.
     53
     54definition graph_closed : graph statement → Prop ≝
     55λg. ∀l,s. lookup ?? g l = Some ? s → labels_present g s.
     56
    2857record internal_function : Type[0] ≝
    2958{ f_labgen    : universe LabelTag
     
    3463; f_stacksize : nat
    3564; f_graph     : graph statement
    36 ; f_entry     : Σl:label. lookup ?? f_graph l ≠ None ?
    37 ; f_exit      : Σl:label. lookup ?? f_graph l ≠ None ?
     65; f_closed    : graph_closed f_graph
     66; f_entry     : Σl:label. present ?? f_graph l
     67; f_exit      : Σl:label. present ?? f_graph l
    3868}.
    3969
Note: See TracChangeset for help on using the changeset viewer.