source: src/Cminor/Cminor_syntax.ma

Last change on this file was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 5.7 KB
Line 
1
2include "common/FrontEndOps.ma".
3include "common/CostLabel.ma".
4include "basics/lists/list.ma".
5
6inductive expr : typ → Type[0] ≝
7| Id : ∀t. ident → expr t
8| Cst : ∀t. constant t → expr t
9| Op1 : ∀t,t'. unary_operation t t' → expr t → expr t'
10| Op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → expr t1 → expr t2 → expr t'
11| Mem : ∀t. expr ASTptr → expr t
12| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
13| Ecost : ∀t. costlabel → expr t → expr t.
14
15(* Assert a predicate on every variable or parameter identifier. *)
16let rec expr_vars (t:typ) (e:expr t) (P:ident → typ → Prop) on e : Prop ≝
17match e with
18[ Id t i ⇒ P i t
19| Cst _ _ ⇒ True
20| Op1 _ _ _ e ⇒ expr_vars ? e P
21| Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
22| Mem _ e ⇒ expr_vars ? e P
23| Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
24| Ecost _ _ e ⇒ expr_vars ? e P
25].
26
27lemma expr_vars_mp : ∀t,e,P,Q.
28  (∀i,t. P i t → Q i t) → expr_vars t e P → expr_vars t e Q.
29#t0 #e elim e normalize /3/
30[ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2
31  % /3/
32| #sz #sg #t #e1 #e2 #e3 #IH1 #IH2 #IH3 #P #Q #H * * /5/
33] qed.
34
35inductive stmt : Type[0] ≝
36| St_skip : stmt
37| St_assign : ∀t. ident → expr t → stmt
38| St_store : ∀t. expr ASTptr → expr t → stmt
39(* ident for returned value, expression to identify fn, args. *)
40| St_call : option (ident × typ) → expr ASTptr → list (𝚺t. expr t) → stmt
41(* We don't use these at the moment, and they're getting in the way.
42| St_tailcall : expr ASTptr → list (𝚺t. expr t) → stmt
43*)
44| St_seq : stmt → stmt → stmt
45| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
46| St_return : option (𝚺t. expr t) → stmt
47| St_label : identifier Label → stmt → stmt
48| St_goto : identifier Label → stmt
49| St_cost : costlabel → stmt → stmt.
50
51(* Apply a predicate to every statement.  Be careful with grouping so that the
52   local application is the first conjunct, and substatements the second. *)
53
54let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝
55match s with
56[ St_seq s1 s2 ⇒ P s ∧ (stmt_P P s1 ∧ stmt_P P s2)
57| St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ (stmt_P P s1 ∧ stmt_P P s2)
58| St_label _ s' ⇒ P s ∧ stmt_P P s'
59| St_cost _ s' ⇒ P s ∧ stmt_P P s'
60| _ ⇒ P s ∧ True
61].
62
63lemma stmt_P_P : ∀P,s. stmt_P P s → P s.
64#P * normalize * /3 by proj1/
65qed.
66
67(* Assert a predicate on every variable or parameter identifier. *)
68definition stmt_vars : (ident → typ → Prop) → stmt → Prop ≝
69λP,s.
70match s with
71[ St_assign t i e ⇒ P i t ∧ expr_vars ? e P
72| St_store _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
73| St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P (\fst i) (\snd i) ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
74(*
75| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
76*)
77| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
78| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ mk_DPair _ e ⇒ expr_vars ? e P ] ]
79| _ ⇒ True
80].
81
82definition stmt_labels : (identifier Label → Prop) → stmt → Prop ≝
83λP,s.
84match s with
85[ St_label l _ ⇒ P l
86| St_goto l ⇒ P l
87| _ ⇒ True
88].
89
90lemma stmt_P_mp : ∀P,Q. (∀s. P s → Q s) → ∀s. stmt_P P s → stmt_P Q s.
91#P #Q #H #s elim s /6 by proj1, proj2, conj/
92qed.
93
94lemma stmt_vars_mp : ∀P,Q. (∀i,t. P i t → Q i t) → ∀s. stmt_vars P s → stmt_vars Q s.
95#P #Q #H #s elim s normalize
96[ //
97| #t #id #e * /4/
98| #t #e1 #e2 * /4/
99| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ]
100(*
101| #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ]
102*)
103| #s1 #s2 #H1 #H2 * /3/
104| #sz #sg #e #s1 #s2 #H1 #H2 /5/
105| * normalize [ // | *; normalize /3/ ]
106| /2/
107| //
108| /2/
109] qed.
110
111lemma stmt_labels_mp : ∀P,Q. (∀l. P l → Q l) → ∀s. stmt_labels P s → stmt_labels Q s.
112#P #Q #H #s elim s normalize /2/ qed.
113
114(* Get labels from a Cminor statement. *)
115let rec labels_of (s:stmt) : list (identifier Label) ≝
116match s with
117[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
118| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
119| St_label l s ⇒ l::(labels_of s)
120| St_cost _ s ⇒ labels_of s
121| _ ⇒ [ ]
122].
123
124inductive rettyp_match : option typ → option (𝚺t.expr t) → Prop ≝
125| rettyp_none : rettyp_match (None ?) (None ?)
126| rettyp_some : ∀t,e. rettyp_match (Some ? t) (Some ? ❬t,e❭).
127
128record cminor_stmt_inv (env:list (ident × typ)) (labels:list (identifier Label)) (rettyp:option typ) (s:stmt) : Prop ≝ {
129  cm_inv_var : stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) env) s;
130  cm_inv_labels : stmt_labels (λl.Exists ? (λl'.l' = l) labels) s;
131  cm_inv_return : match s with [ St_return oe ⇒ rettyp_match rettyp oe
132                               | _ ⇒ True ]
133}.
134
135record internal_function : Type[0] ≝
136{ f_return    : option typ
137; f_params    : list (ident × typ)
138; f_vars      : list (ident × typ)
139; f_distinct  : distinct_env … (f_params @ f_vars)
140; f_stacksize : nat
141; f_body      : stmt
142     (* Ensure that variables appear in the params and vars list with the
143        correct typ; and that all goto labels used are declared. *)
144; f_inv       : stmt_P (cminor_stmt_inv (f_params @ f_vars) (labels_of f_body) f_return) f_body
145}.
146
147(* We define two closely related versions of Cminor, the first with the original
148   initialisation data for global variables, and the second where the code is
149   responsible for initialisation and we only give the size of each variable. *)
150
151definition Cminor_program ≝ program (λ_.fundef internal_function) (list init_data).
152
153definition Cminor_noinit_program ≝ program (λ_.fundef internal_function) nat.
Note: See TracBrowser for help on using the repository browser.