source: Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma @ 1097

Last change on this file since 1097 was 1097, checked in by campbell, 9 years ago

Checkpoint labels work on branch again.

File size: 5.3 KB
RevLine 
[751]1
2include "common/FrontEndOps.ma".
3include "common/CostLabel.ma".
[1087]4include "utilities/lists.ma".
5include "utilities/option.ma".
[751]6
[1087]7definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
8λtag,A,m,i. lookup … m i ≠ None ?.
9
[880]10(* TODO: consider making the typing stricter. *)
[751]11
[880]12inductive expr : typ → Type[0] ≝
13| Id : ∀t. ident → expr t
14| Cst : ∀t. constant → expr t
15| Op1 : ∀t,t'. unary_operation → expr t → expr t'
16| Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
[881]17| Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
[880]18| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
19| Ecost : ∀t. costlabel → expr t → expr t.
20
[1087]21(* Assert a predicate on every variable or parameter identifier. *)
22let rec expr_vars (t:typ) (e:expr t) (P:ident → Prop) on e : Prop ≝
23match e with
24[ Id _ i ⇒ P i
25| Cst _ _ ⇒ True
26| Op1 _ _ _ e ⇒ expr_vars ? e P
27| Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
28| Mem _ _ _ e ⇒ expr_vars ? e P
29| Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
30| Ecost _ _ e ⇒ expr_vars ? e P
31].
32
33lemma expr_vars_mp : ∀t,e,P,Q.
34  (∀i. P i → Q i) → expr_vars t e P → expr_vars t e Q.
35#t0 #e elim e normalize /3/
36[ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2
37  % /3/
38| #sz #sg #t #e1 #e2 #e3 #IH1 #IH2 #IH3 #P #Q #H * * /5/
39] qed.
40
[1096]41axiom Label : String.
42
[751]43inductive stmt : Type[0] ≝
44| St_skip : stmt
[880]45| St_assign : ∀t. ident → expr t → stmt
[881]46| St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
[816]47(* ident for returned value, expression to identify fn, args. *)
[880]48| St_call : option ident → expr (ASTptr Code) → list (Σt. expr t) → stmt
49| St_tailcall : expr (ASTptr Code) → list (Σt. expr t) → stmt
[751]50| St_seq : stmt → stmt → stmt
[880]51| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
[751]52| St_loop : stmt → stmt
53| St_block : stmt → stmt
54| St_exit : nat → stmt
55(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
[961]56| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
[880]57| St_return : option (Σt. expr t) → stmt
[1096]58| St_label : identifier Label → stmt → stmt
59| St_goto : identifier Label → stmt
[751]60| St_cost : costlabel → stmt → stmt.
61
[1096]62let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝
63match s with
64[ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
65| St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
66| St_loop s' ⇒ P s ∧ stmt_P P s'
67| St_block s' ⇒ P s ∧ stmt_P P s'
68| St_label _ s' ⇒ P s ∧ stmt_P P s'
69| St_cost _ s' ⇒ P s ∧ stmt_P P s'
70| _ ⇒ P s
71].
72
73lemma stmt_P_P : ∀P,s. stmt_P P s → P s.
74#P * normalize /2/
75[ #s1 #s2 * * /2/
76| #sz #sg #e #s1 #s2 * * /2/
77| 3,4: #s * /2/
78| 5,6: #i #s normalize * /2/
79] qed.
80
[1087]81(* Assert a predicate on every variable or parameter identifier. *)
[1096]82definition stmt_vars : (ident → Prop) → stmt → Prop ≝
83λP,s.
[1087]84match s with
[1096]85[ St_assign _ i e ⇒ P i ∧ expr_vars ? e P
[1087]86| St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
87| St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P i ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es
88| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es
[1096]89| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
[1087]90| St_switch _ _ e _ _ ⇒ expr_vars ? e P
91| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ dp _ e ⇒ expr_vars ? e P ] ]
[1096]92| _ ⇒ True
[1087]93].
94
[1096]95definition stmt_labels : (identifier Label → Prop) → stmt → Prop ≝
96λP,s.
97match s with
98[ St_label l _ ⇒ P l
99| St_goto l ⇒ P l
100| _ ⇒ True
101].
102
103lemma stmt_P_mp : ∀P,Q. (∀s. P s → Q s) → ∀s. stmt_P P s → stmt_P Q s.
104#P #Q #H #s elim s /2/
105[ #s1 #s2 #H1 #H2 normalize * * /4/
106| #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
107| #s #H * /5/
108| #s #H * /5/
109| #l #s #H * /5/
110| #l #s #H * /5/
111] qed.
112
113lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars P s → stmt_vars Q s.
[1087]114#P #Q #H #s elim s normalize
115[ //
116| #t #id #e * /4/
117| #t #r #q #e1 #e2 * /4/
118| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ]
119| #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ]
120| #s1 #s2 #H1 #H2 * /3/
[1096]121| #sz #sg #e #s1 #s2 #H1 #H2 /5/
[1087]122| 8,9: #s #H1 #H2 /2/
123| //
124| /5/
125| * normalize [ // | *; normalize /3/ ]
126| /2/
127| //
128| /2/
129] qed.
130
[1097]131lemma stmt_labels_mp : ∀P,Q. (∀l. P l → Q l) → ∀s. stmt_labels P s → stmt_labels Q s.
132#P #Q #H #s elim s normalize /2/ qed.
133
[1096]134(* Get labels from a Cminor statement. *)
135let rec labels_of (s:stmt) : list (identifier Label) ≝
136match s with
137[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
138| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
139| St_loop s ⇒ labels_of s
140| St_block s ⇒ labels_of s
141| St_label l s ⇒ l::(labels_of s)
142| St_cost _ s ⇒ labels_of s
143| _ ⇒ [ ]
144].
145
[751]146record internal_function : Type[0] ≝
[886]147{ f_return    : option typ
148; f_params    : list (ident × typ)
149; f_vars      : list (ident × typ)
[751]150; f_stacksize : nat
151; f_body      : stmt
[1096]152; f_inv       : stmt_P (λs.stmt_vars (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) s ∧
153                           stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
[751]154}.
155
156definition Cminor_program ≝ program (fundef internal_function) unit.
Note: See TracBrowser for help on using the repository browser.