source: src/Cminor/syntax.ma @ 1369

Last change on this file since 1369 was 1369, checked in by campbell, 8 years ago

Put type information into front-end unary ops.
Slight change to semantics: booleans produced by Onotbool can be any given
integer size.

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