Changeset 1626 for src/RTLabs
- Timestamp:
- Dec 19, 2011, 2:48:33 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/syntax.ma
r1369 r1626 13 13 | St_cost : costlabel → label → statement 14 14 | 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 *) 16 16 | St_op2 : binary_operation → register → register → register → label → statement (* destination source1 source2 *) 17 17 | St_load : memory_chunk → register → register → label → statement … … 25 25 | St_return : statement 26 26 . 27 28 definition env_has : list (register × typ) → register → typ → Prop ≝ 29 λl,r,t. Exists ? (λx. 〈r,t〉 = x) l. 30 31 definition 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 ]. 27 36 28 37 definition labels_P : (label → Prop) → statement → Prop ≝ … … 52 61 λg,s. labels_P (present ?? g) s. 53 62 63 definition forall_nodes : ∀A.∀P:A → Prop. graph A → Prop ≝ 64 λA,P,g. ∀l,n. lookup ?? g l = Some ? n → P n. 65 54 66 definition 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. 68 definition graph_typed : list (register × typ) → graph statement → Prop ≝ 69 λe. forall_nodes ? (statement_typed e). 56 70 57 71 record internal_function : Type[0] ≝ … … 64 78 ; f_graph : graph statement 65 79 ; f_closed : graph_closed f_graph 80 ; f_typed : graph_typed (f_locals @ f_params) f_graph 66 81 ; f_entry : Σl:label. present ?? f_graph l 67 82 ; f_exit : Σl:label. present ?? f_graph l
Note: See TracChangeset
for help on using the changeset viewer.