Changeset 1626 for src/RTLabs

Timestamp:

Dec 19, 2011, 2:48:33 PM (9 years ago)

Author:

campbell

Message:

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

File:

• src/RTLabs/syntax.ma (modified) (4 diffs)

src/RTLabs/syntax.ma

@@ -13 +13 @@
 | St_cost : costlabel → label → statement
 | St_const : register → constant → label → statement
-| St_op1 : ∀t,t'. unary_operation t t' → register → register → label → statement (* destination source *)
+| St_op1 : ∀t,t'. unary_operation t' t → register → register → label → statement (* destination source *)
 | St_op2 : binary_operation → register → register → register → label → statement (* destination source1 source2 *)
 | St_load : memory_chunk → register → register → label → statement
@@ -25 +25 @@
 | St_return : statement
 .
+
+definition env_has : list (register × typ) → register → typ → Prop ≝
+λl,r,t. Exists ? (λx. 〈r,t〉 = x) l.
+
+definition statement_typed : list (register × typ) → statement → Prop ≝
+λe,s. match s with
+[ St_op1 t t' _ r r' _ ⇒ env_has e r t ∧ env_has e r' t'
+| _ ⇒ True
+].
 
 definition labels_P : (label → Prop) → statement → Prop ≝
@@ -52 +61 @@
 λg,s. labels_P (present ?? g) s.
 
+definition forall_nodes : ∀A.∀P:A → Prop. graph A → Prop ≝
+λA,P,g. ∀l,n. lookup ?? g l = Some ? n → P n.
+
 definition graph_closed : graph statement → Prop ≝
-λg. ∀l,s. lookup ?? g l = Some ? s → labels_present g s.
+  λg. forall_nodes ? (labels_present g) g.
+definition graph_typed : list (register × typ) → graph statement → Prop ≝
+  λe. forall_nodes ? (statement_typed e).
 
 record internal_function : Type[0] ≝
@@ -64 +78 @@
 ; f_graph     : graph statement
 ; f_closed    : graph_closed f_graph
+; f_typed     : graph_typed (f_locals @ f_params) f_graph
 ; f_entry     : Σl:label. present ?? f_graph l
 ; f_exit      : Σl:label. present ?? f_graph l