Changeset 1626 for src/RTLabs/syntax.ma


Ignore:
Timestamp:
Dec 19, 2011, 2:48:33 PM (8 years ago)
Author:
campbell
Message:

Add extra type safety in front end. NB: critical freshness parts
axiomatised for now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/syntax.ma

    r1369 r1626  
    1313| St_cost : costlabel → label → statement
    1414| St_const : register → constant → label → statement
    15 | St_op1 : ∀t,t'. unary_operation t t' → register → register → label → statement (* destination source *)
     15| St_op1 : ∀t,t'. unary_operation t' t → register → register → label → statement (* destination source *)
    1616| St_op2 : binary_operation → register → register → register → label → statement (* destination source1 source2 *)
    1717| St_load : memory_chunk → register → register → label → statement
     
    2525| St_return : statement
    2626.
     27
     28definition env_has : list (register × typ) → register → typ → Prop ≝
     29λl,r,t. Exists ? (λx. 〈r,t〉 = x) l.
     30
     31definition statement_typed : list (register × typ) → statement → Prop ≝
     32λe,s. match s with
     33[ St_op1 t t' _ r r' _ ⇒ env_has e r t ∧ env_has e r' t'
     34| _ ⇒ True
     35].
    2736
    2837definition labels_P : (label → Prop) → statement → Prop ≝
     
    5261λg,s. labels_P (present ?? g) s.
    5362
     63definition forall_nodes : ∀A.∀P:A → Prop. graph A → Prop ≝
     64λA,P,g. ∀l,n. lookup ?? g l = Some ? n → P n.
     65
    5466definition graph_closed : graph statement → Prop ≝
    55 λg. ∀l,s. lookup ?? g l = Some ? s → labels_present g s.
     67  λg. forall_nodes ? (labels_present g) g.
     68definition graph_typed : list (register × typ) → graph statement → Prop ≝
     69  λe. forall_nodes ? (statement_typed e).
    5670
    5771record internal_function : Type[0] ≝
     
    6478; f_graph     : graph statement
    6579; f_closed    : graph_closed f_graph
     80; f_typed     : graph_typed (f_locals @ f_params) f_graph
    6681; f_entry     : Σl:label. present ?? f_graph l
    6782; f_exit      : Σl:label. present ?? f_graph l
Note: See TracChangeset for help on using the changeset viewer.