source: src/Clight/toCminor.ma @ 2572

Last change on this file since 2572 was 2572, checked in by garnier, 7 years ago

Progress on toCminorCorrectness.

File size: 75.8 KB
Line 
1include "Clight/ClassifyOp.ma".
2include "basics/lists/list.ma".
3include "Clight/fresh.ma".
4
5(* Identify local variables that must be allocated memory. *)
6(* These are the variables whose addresses are taken. *)
7let rec gather_mem_vars_expr (e:expr) : identifier_set SymbolTag ≝
8match e with
9[ Expr ed ty ⇒
10    match ed with
11    [ Ederef e1 ⇒ gather_mem_vars_expr e1
12    | Eaddrof e1 ⇒ gather_mem_vars_addr e1
13    | Eunop _ e1 ⇒ gather_mem_vars_expr e1
14    | Ebinop _ e1 e2 ⇒ gather_mem_vars_expr e1 ∪
15                       gather_mem_vars_expr e2
16    | Ecast _ e1 ⇒ gather_mem_vars_expr e1
17    | Econdition e1 e2 e3 ⇒ gather_mem_vars_expr e1 ∪
18                            gather_mem_vars_expr e2 ∪
19                            gather_mem_vars_expr e3
20    | Eandbool e1 e2 ⇒ gather_mem_vars_expr e1 ∪
21                       gather_mem_vars_expr e2
22    | Eorbool e1 e2 ⇒ gather_mem_vars_expr e1 ∪
23                      gather_mem_vars_expr e2
24    | Efield e1 _ ⇒ gather_mem_vars_expr e1
25    | Ecost _ e1 ⇒ gather_mem_vars_expr e1
26    | _ ⇒ ∅
27    ]
28]
29and gather_mem_vars_addr (e:expr) : identifier_set SymbolTag ≝
30match e with
31[ Expr ed ty ⇒
32    match ed with
33    [ Evar x ⇒ { (x) }
34    | Ederef e1 ⇒ gather_mem_vars_expr e1
35    | Efield e1 _ ⇒ gather_mem_vars_addr e1
36    | _ ⇒ ∅ (* not an lvalue *)
37    ]
38].
39
40let rec gather_mem_vars_stmt (s:statement) : identifier_set SymbolTag ≝
41match s with
42[ Sskip ⇒ ∅
43| Sassign e1 e2 ⇒ gather_mem_vars_expr e1 ∪
44                  gather_mem_vars_expr e2
45| Scall oe1 e2 es ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ] ∪
46                    gather_mem_vars_expr e2 ∪
47                    (foldl ?? (λs,e. s ∪ gather_mem_vars_expr e) ∅ es)
48| Ssequence s1 s2 ⇒ gather_mem_vars_stmt s1 ∪
49                    gather_mem_vars_stmt s2
50| Sifthenelse e1 s1 s2 ⇒ gather_mem_vars_expr e1 ∪
51                         gather_mem_vars_stmt s1 ∪
52                         gather_mem_vars_stmt s2
53| Swhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
54                 gather_mem_vars_stmt s1
55| Sdowhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
56                   gather_mem_vars_stmt s1
57| Sfor s1 e1 s2 s3 ⇒ gather_mem_vars_stmt s1 ∪
58                     gather_mem_vars_expr e1 ∪
59                     gather_mem_vars_stmt s2 ∪
60                     gather_mem_vars_stmt s3
61| Sbreak ⇒ ∅
62| Scontinue ⇒ ∅
63| Sreturn oe1 ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ]
64| Sswitch e1 ls ⇒ gather_mem_vars_expr e1 ∪
65                  gather_mem_vars_ls ls
66| Slabel _ s1 ⇒ gather_mem_vars_stmt s1
67| Sgoto _ ⇒ ∅
68| Scost _ s1 ⇒ gather_mem_vars_stmt s1
69]
70and gather_mem_vars_ls (ls:labeled_statements) on ls : identifier_set SymbolTag ≝
71match ls with
72[ LSdefault s1 ⇒ gather_mem_vars_stmt s1
73| LScase _ _ s1 ls1 ⇒ gather_mem_vars_stmt s1 ∪
74                      gather_mem_vars_ls ls1
75].
76
77(* Defines where a variable should be allocated. *)
78inductive var_type : Type[0] ≝
79| Global : region → var_type  (* A global, allocated statically in a given region (which one ???)  *)
80| Stack  : nat → var_type     (* On the stack, at a given height *)
81| Local  : var_type           (* Locally (hopefully, in a register) *)
82.
83
84(* A map associating each variable identifier to its allocation mode and its type. *)
85definition var_types ≝ identifier_map SymbolTag (var_type × type).
86
87axiom UndeclaredIdentifier : String.
88
89definition lookup' ≝
90λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id).
91
92(* Assert that an identifier is a local variable with the given typ. *)
93definition local_id : var_types → ident → typ → Prop ≝
94λvars,id,t. match lookup' vars id with [ OK vt ⇒ match (\fst vt) with [ Global _ ⇒ False | _ ⇒ t = typ_of_type (\snd vt) ] | _ ⇒ False ].
95
96(* Note that the semantics allows locals to shadow globals.
97   Parameters start out as locals, but get stack allocated if their address
98   is taken.  We will add code to store them if that's the case.
99 *)
100
101(* Some kind of data is never allocated in registers, even if it fits, typically structured data. *)
102definition always_alloc : type → bool ≝
103λt. match t with
104[ Tarray _ _ ⇒ true
105| Tstruct _ _ ⇒ true
106| Tunion _ _ ⇒ true
107| _ ⇒ false
108].
109
110(* This builds a [var_types] map characterizing the allocation mode, of variables,
111 * and it returns a stack usage for the function (in bytes, according to [sizeof]) *)
112definition characterise_vars : list (ident×region×type) → function → var_types × nat ≝
113λglobals, f.
114  (* globals are added into a map, with var_type Global, region π_2(idrt) and type π_3(idrt) *)
115  let m ≝ foldr ?? (λidrt,m. add ?? m (\fst (\fst idrt)) 〈Global (\snd (\fst idrt)), \snd idrt〉) (empty_map ??) globals in
116  (* variables whose addr is taken in the body of the function are gathered in [mem_vars] *)
117  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
118  (* iterate on the parameters and local variables of the function, with a tuple (map, stack_high) as an accumulator *)
119  let 〈m,stacksize〉 ≝ foldr ?? (λv,ms.
120    let 〈m,stack_high〉 ≝ ms in
121    let 〈id,ty〉 ≝ v in         
122    let 〈c,stack_high〉 ≝
123      (* if the (local, parameter) variable is of a compound type OR if its adress is taken, we allocate it on the stack. *)
124      if always_alloc ty ∨ id ∈ mem_vars then
125        〈Stack stack_high,stack_high + sizeof ty〉
126      else
127        〈Local, stack_high〉
128    in
129      〈add ?? m id 〈c, ty〉, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in
130  〈m,stacksize〉.
131
132(* A local variable id' status is not modified by the removal of a global variable id : id' is still local *)
133lemma local_id_add_global : ∀vars,id,r,t,id',t'.
134  local_id (add ?? vars id 〈Global r, t〉) id' t' → local_id vars id' t'.
135#var #id #r #t #id' #t'
136whd in ⊢ (% → ?); whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?);
137cases (identifier_eq ? id id')
138[ #E >E >lookup_add_hit whd in ⊢ (% → ?); *
139| #NE >lookup_add_miss /2/
140] qed.
141
142(* If I add a variable id ≠ id', then id' is still local *)
143lemma local_id_add_miss : ∀vars,id,vt,id',t'.
144  id ≠ id' → local_id (add ?? vars id vt) id' t' → local_id vars id' t'.
145#vars #id #vt #id' #t' #NE
146whd in ⊢ (% → %);
147whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ]);
148>lookup_add_miss
149[ #H @H | /2/ ]
150qed.
151
152(* After characterise_vars, a variable in the resulting map is either a global or a "local"(register or stack allocated) *)
153lemma characterise_vars_src : ∀gl,f,vars,n.
154  characterise_vars gl f = 〈vars,n〉 →
155  ∀id. present ?? vars id →
156   (∃r,ty. lookup' vars id = OK ? 〈Global r,ty〉 ∧ Exists ? (λx.x = 〈〈id,r〉,ty〉) gl) ∨
157   ∃t.local_id vars id t.
158#globals #f
159whd in ⊢ (∀_.∀_.??%? → ?);
160elim (fn_params f @ fn_vars f)
161[ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #H %1
162  elim globals in H ⊢ %;
163  [ normalize * #H cases (H (refl ??))
164  | * * #id #rg #ty #tl #IH #H
165    cases (identifier_eq ? i id)
166    [ #E <E %{rg} %{ty} % [ whd in ⊢ (??%?); >lookup_add_hit // | %1 // ]
167    | #NE cases (IH ?)
168      [ #rg' * #ty' * #H1 #H2 %{rg'} %{ty'} %
169        [ whd in ⊢ (??%?); >lookup_add_miss  [ @H1 | @NE ]
170        | %2 @H2
171        ]
172      | whd in H ⊢ %; >lookup_add_miss in H; //
173      ]
174    ]
175  ]
176| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i
177  #H >(contract_pair var_types nat ?) in E;
178  whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
179  cases (always_alloc ty ∨ id ∈ ?) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
180  #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
181  cases (identifier_eq ? i id)
182  [ 1,3: #E' <E' in EQ2:%; #EQ2 %2 %{(typ_of_type ty)}
183         destruct (EQ2) whd whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]);
184         >lookup_add_hit @refl
185  | *: #NE cases (IH m0 n0 ? i ?)
186    [ 1,5: * #rg' * #ty' * #H1 #H2 %1 %{rg'} %{ty'} % //
187           destruct (EQ2) whd in ⊢ (??%?); >lookup_add_miss try @NE @H1
188    | 2,6: * #t #H1 %2 %{t} destruct (EQ2) whd whd in ⊢ (match % with [_ ⇒ ?|_ ⇒ ?]);
189           >lookup_add_miss //
190    | 3,7: <EQ @refl
191    | *: destruct (EQ2) whd in H; >lookup_add_miss in H; //
192    ]
193  ]
194] qed.
195
196(* A local variable in a function is either a parameter or a "local" (:=register or stack alloc'd)
197 * variable, with the right type *)
198lemma characterise_vars_all : ∀l,f,vars,n.
199  characterise_vars l f = 〈vars,n〉 →
200  ∀i,t. local_id vars i t →
201        Exists ? (λx.\fst x = i ∧ typ_of_type (\snd x) = t) (fn_params f @ fn_vars f).
202#globals #f
203whd in ⊢ (∀_.∀_.??%? → ?);
204elim (fn_params f @ fn_vars f)
205[ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #t #H @False_ind
206  elim globals in H;
207  [ normalize //
208  | * * #id #rg #t #tl #IH whd in ⊢ (?%?? → ?); #H @IH @(local_id_add_global … H)
209  ]
210| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i #t
211
212  #H >(contract_pair var_types nat ?) in E;
213  whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
214  cases (always_alloc ty ∨ id ∈ ?) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
215  #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
216
217  cases (identifier_eq ? id i)
218  [ 1,3: #E' >E' in EQ2:%; #EQ2 % %
219    [ 1,3: @refl
220    | *: destruct (EQ2) change with (add ?????) in H:(?%??);
221      whd in H; whd in H:(match % with [_ ⇒ ?|_ ⇒ ?]); >lookup_add_hit in H;
222      whd in ⊢ (% → ?); #E'' >E'' @refl
223    ]
224  | *: #NE %2 @(IH m0 n0)
225    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])); >contract_pair @EQ
226    | 2,4: destruct (EQ2) @(local_id_add_miss … H) @NE
227    ]
228  ]
229] qed.
230
231(* The map generated by characterise_vars is "correct" wrt the fresh ident generator of tag [u],
232   i.e. by generating fresh idents with u, we risk no collision with the idents in the map domain. *)
233lemma characterise_vars_fresh : ∀gl,f,vars,n,u.
234  characterise_vars gl f = 〈vars,n〉 →              (* If we generate a map ... *)
235  globals_fresh_for_univ ? gl u →                  (* and the globals are out of the idents generated by u *)
236  fn_fresh_for_univ f u →                          (* and the variables of the function f are cool with u too ... *)
237  fresh_map_for_univ … vars u.                     (* then there won't be collisions between the map and idents made from u *)
238#gl #f #vars #n #u #CH #GL #FN
239#id #H
240cases (characterise_vars_src … CH … H)
241[ * #rg * #ty * #H1 #H2
242  cases (Exists_All … H2 GL) * * #id' #rg' #ty' * #E #H destruct //
243| * #t #H lapply (characterise_vars_all … CH id t H) #EX
244  cases (Exists_All … EX FN) * #id' #ty' * * #E1 #E2 #H' -H destruct //
245] qed.
246
247include "Cminor/syntax.ma".
248include "common/Errors.ma".
249
250alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)".
251
252axiom BadlyTypedAccess : String.
253axiom BadLvalue : String.
254axiom MissingField : String.
255
256(* type_should_eq enforces that two types are equal and eliminates this equality by
257   transporting P ty1 to P ty2. If ty1 != ty2, then Error *)
258definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
259λty1,ty2,P,p.
260  do E ← assert_type_eq ty1 ty2;
261  OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p). 
262
263(* same gig for regions *)
264definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
265* * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
266qed.
267
268(* same gig for AST typs *)
269definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2) ≝
270λty1,ty2,P,p.
271  match typ_eq ty1 ty2 with
272  [ inl E ⇒ OK ? (p⌈P ty1 ↦ P ty2⌉)
273  | inr _ ⇒ Error ? (msg TypeMismatch)
274  ].
275destruct %
276qed.
277
278alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)".
279alias id "CMunop" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.ind(1,0,0)".
280
281(* XXX: For some reason matita refuses to pick the right one unless forced. *)
282alias id "CMnotbool" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.con(0,3,0)".
283
284(* Translates a Clight unary operation into a Cminor one, while checking
285 * that the domain and codomain types are consistent. *)
286definition translate_unop : ∀t,t':typ. CLunop → res (CMunop t t') ≝
287λt,t'.λop:CLunop.
288  match op with
289  [ Onotbool ⇒
290      match t return λt. res (CMunop t t') with
291      [ ASTint sz sg ⇒
292          match t' return λt'. res (CMunop ? t') with
293          [ ASTint sz' sg' ⇒ OK ? (CMnotbool ????)
294          | _ ⇒ Error ? (msg TypeMismatch)
295          ]
296      | ASTptr ⇒
297          match t' return λt'. res (CMunop ? t') with
298          [ ASTint sz' sg' ⇒ OK ? (CMnotbool ????)
299          | _ ⇒ Error ? (msg TypeMismatch)
300          ]
301      | _ ⇒ Error ? (msg TypeMismatch)
302      ]
303  | Onotint ⇒
304      match t' return λt'. res (CMunop t t') with
305      [ ASTint sz sg ⇒ typ_should_eq ?? (λt. CMunop t (ASTint ??)) (Onotint sz sg)
306      | _ ⇒ Error ? (msg TypeMismatch)
307      ]
308  | Oneg ⇒
309      match t' return λt'. res (CMunop t t') with
310      [ ASTint sz sg ⇒ typ_should_eq ?? (λt.CMunop t (ASTint ??)) (Onegint sz sg)
311    (*  | ASTfloat sz ⇒ typ_should_eq ?? (λt.CMunop t (ASTfloat sz)) (Onegf sz) *)
312      | _ ⇒ Error ? (msg TypeMismatch)
313      ]
314  ]. @I qed.
315
316(* Translates a Clight addition into a Cminor one. Four cases to consider :
317  - integer/integer add
318  - fp/fp add
319  - pointer/integer
320  - integer/pointer.
321  Consistency of the type is enforced by explicit checks.
322*)
323
324(* First, how to get rid of a abstract-away pointer or array type *)
325definition fix_ptr_type : ∀ty,n. expr (typ_of_type (ptr_type ty n)) → expr ASTptr ≝
326λty,n,e. e⌈expr (typ_of_type (ptr_type ty n)) ↦ expr ASTptr⌉.
327cases n //
328qed.
329
330definition translate_add ≝
331λty1,ty2,ty'.
332let ty1' ≝ typ_of_type ty1 in
333let ty2' ≝ typ_of_type ty2 in
334match classify_add ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
335[ add_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oadd ??) e1 e2)
336(* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *)
337| add_case_pi n ty sz sg ⇒
338    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
339| add_case_ip n sz sg ty ⇒
340    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16) (fix_ptr_type … e2) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
341| add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch)
342].
343
344definition translate_sub ≝
345λty1,ty2,ty'.
346let ty1' ≝ typ_of_type ty1 in
347let ty2' ≝ typ_of_type ty2 in
348match classify_sub ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
349[ sub_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osub ??) e1 e2)
350(* XXX could optimise cast as above *)
351| sub_case_pi n ty sz sg ⇒
352    λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I16) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
353(* XXX check in detail? *)
354| sub_case_pp n1 n2 ty1 ty2 ⇒
355    λe1,e2. match ty' return λty'. res (CMexpr (typ_of_type ty')) with
356    [ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I16 Signed sz sg) (Op2 ??? (Odiv I16) (Op2 ??? (Osubpp I16) (fix_ptr_type … e1) (fix_ptr_type ?? e2)) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty2))))))
357    | _ ⇒ Error ? (msg TypeMismatch)
358    ]
359| sub_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
360].
361
362definition translate_mul ≝
363λty1,ty2,ty'.
364let ty1' ≝ typ_of_type ty1 in
365let ty2' ≝ typ_of_type ty2 in
366match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
367[ aop_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omul …) e1 e2)
368(* | aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omulf …) e1 e2) *)
369| aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
370].
371
372definition translate_div ≝
373λty1,ty2,ty'.
374let ty1' ≝ typ_of_type ty1 in
375let ty2' ≝ typ_of_type ty2 in
376match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
377[ aop_case_ii sz sg ⇒
378    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
379    [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivu …) e1 e2)
380    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odiv …) e1 e2)
381    ]
382(* | aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivf …) e1 e2) *)
383| aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
384].
385
386definition translate_mod ≝
387λty1,ty2,ty'.
388let ty1' ≝ typ_of_type ty1 in
389let ty2' ≝ typ_of_type ty2 in
390match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
391[ aop_case_ii sz sg ⇒
392    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
393    [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omodu …) e1 e2)
394    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omod …) e1 e2)
395    ]
396(* no float case *)
397| _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
398].
399
400definition translate_shr ≝
401λty1,ty2,ty'.
402let ty1' ≝ typ_of_type ty1 in
403let ty2' ≝ typ_of_type ty2 in
404match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
405[ aop_case_ii sz sg ⇒
406    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
407    [ Unsigned ⇒ λe1,e2.  typ_should_eq ??? (Op2 ??? (Oshru …) e1 e2)
408    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oshr …) e1 e2)
409    ]
410(* no float case *)
411| _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
412].
413
414definition complete_cmp : ∀ty'. CMexpr (ASTint I8 Unsigned) → res (CMexpr (typ_of_type ty')) ≝
415λty',e.
416match ty' return λty'. res (CMexpr (typ_of_type ty')) with
417[ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I8 Unsigned sz sg) e)
418| _ ⇒ Error ? (msg TypeMismatch)
419].
420 
421definition translate_cmp ≝
422λc,ty1,ty2,ty'.
423let ty1' ≝ typ_of_type ty1 in
424let ty2' ≝ typ_of_type ty2 in
425match classify_cmp ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
426[ cmp_case_ii sz sg ⇒
427    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
428    [ Unsigned ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpu … c) e1 e2)
429    | Signed ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmp … c) e1 e2)
430    ]
431| cmp_case_pp n ty ⇒
432    λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpp … c) (fix_ptr_type … e1) (fix_ptr_type … e2))
433(* | cmp_case_ff sz ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpf … c) e1 e2) *)
434| cmp_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
435].
436
437definition translate_misc_aop ≝
438λty1,ty2,ty',op.
439let ty1' ≝ typ_of_type ty1 in
440let ty2' ≝ typ_of_type ty2 in
441match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
442[ aop_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ?? (ASTint sz sg) (op sz sg) e1 e2)
443| _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
444].
445
446definition translate_binop : binary_operation → type → CMexpr ? → type → CMexpr ? → type → res (CMexpr ?) ≝
447λop,ty1,e1,ty2,e2,ty.
448let ty' ≝ typ_of_type ty in
449match op with
450[ Oadd ⇒ translate_add ty1 ty2 ty e1 e2
451| Osub ⇒ translate_sub ty1 ty2 ty e1 e2
452| Omul ⇒ translate_mul ty1 ty2 ty e1 e2
453| Omod ⇒ translate_mod ty1 ty2 ty e1 e2
454| Odiv ⇒ translate_div ty1 ty2 ty e1 e2
455| Oand ⇒ translate_misc_aop ty1 ty2 ty Oand e1 e2
456| Oor  ⇒ translate_misc_aop ty1 ty2 ty Oor e1 e2
457| Oxor ⇒ translate_misc_aop ty1 ty2 ty Oxor e1 e2
458| Oshl ⇒ translate_misc_aop ty1 ty2 ty Oshl e1 e2
459(*| Oshr ⇒ translate_misc_aop ty1 ty2 ty Oshr e1 e2 *)
460| Oshr ⇒ translate_shr ty1 ty2 ty e1 e2  (* split on signed/unsigned *)
461| Oeq ⇒ translate_cmp Ceq ty1 ty2 ty e1 e2
462| One ⇒ translate_cmp Cne ty1 ty2 ty e1 e2
463| Olt ⇒ translate_cmp Clt ty1 ty2 ty e1 e2
464| Ogt ⇒ translate_cmp Cgt ty1 ty2 ty e1 e2
465| Ole ⇒ translate_cmp Cle ty1 ty2 ty e1 e2
466| Oge ⇒ translate_cmp Cge ty1 ty2 ty e1 e2
467].
468
469lemma typ_equals : ∀t1,t2. ∀P:∀t. expr t → Prop. ∀v1,v2.
470  typ_should_eq t1 t2 expr v1 = OK ? v2 →
471  P t1 v1 →
472  P t2 v2.
473#t1 #t2 #P #v1 #v2
474whd in ⊢ (??%? → ?); cases (typ_eq t1 t2)
475[ #E destruct #E whd in E:(??%?); destruct //
476| #NE #E normalize in E; destruct
477] qed.
478
479lemma unfix_ptr_type : ∀ty,n,e.∀P:∀t. expr t → Prop.
480  P (typ_of_type (ptr_type ty n)) e →
481  P ASTptr (fix_ptr_type ty n e).
482#ty * [ 2: #n ] #e #P #H @H
483qed.
484
485(* Recall that [expr_vars], defined in Cminor/Syntax.ma, asserts a predicate on
486  all the variables of a program. [translate_binop_vars], given
487  a predicate verified for all variables of subexprs e1 and e2, produces
488  a proof that all variables of [translate_binop op _ e1 _ e2 _] satisfy this
489  predicate. *)
490
491lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e.
492  expr_vars ? e1 P →
493  expr_vars ? e2 P →
494  translate_binop op ty1 e1 ty2 e2 ty = OK ? e →
495  expr_vars ? e P.
496#P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
497whd in ⊢ (??%? → ?);
498[ inversion (classify_add ty1 ty2) in ⊢ ?;
499  [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4 -E3 change with (typ_should_eq ???? = OK ??) in E4;
500    @(typ_equals … E4) % //
501(*  | #sz #E1 #E2 #E3 destruct >E3 #E4
502    @(typ_equals … E4) % // *)
503  | #n #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
504    @(typ_equals … E4) -E4 -E3 % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)| % // ]
505  | #n #sz #sg #ty0 #E1 #E2 #E3 destruct >E3 #E4
506    @(typ_equals … E4) % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2)| % // ]
507  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
508  ]
509 
510| inversion (classify_sub ty1 ty2) in ⊢ ?;
511  [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4
512    @(typ_equals … E4) % //
513(*  | #sz #E1 #E2 #E3 destruct >E3 #E4
514    @(typ_equals … E4) % // *)
515  | #n #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
516    @(typ_equals … E4) % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)| % // ]
517  | #n1 #n2 #ty1' #ty2' #E1 #E2 #E3 destruct >E3
518    whd in ⊢ (??%? → ?); cases ty in e ⊢ %;
519    [ 2: #sz #sg #e #E4 | 3: #ty #e #E4 | 4: #ty' #n' #e #E4
520    | *: normalize #X1 #X2 try #X3 try #X4 destruct
521    ] whd in E4:(??%?); destruct % // %
522    [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1) | @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2) ]
523  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
524  ]
525| 3,4,5,6,7,8,9,10: inversion (classify_aop ty1 ty2) in ⊢ ?;
526  (* Note that some cases require a split on signedness of integer type. *)
527  [ 1,3,5,7,9,11,13,15: #sz * #E1 #E2 #E3 destruct >E3 #E4
528    @(typ_equals … E4) % //
529  | 2,4,6,8,10,12,14,16,18: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
530  ]
531| *: inversion (classify_cmp ty1 ty2) in ⊢ ?;
532  [ 1,4,7,10,13,16: #sz * #E1 #E2 #E3 destruct >E3
533  | 2,5,8,11,14,17: #n #ty' #E1 #E2 #E3 destruct >E3
534  | *: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); @⊥ destruct
535  ] whd in ⊢ (??%? → ?); cases ty in e ⊢ %; normalize nodelta
536  try (normalize #X1 #X2 try #X3 try #X4 try #X5 destruct #FAIL)
537  #sz #sg #e #E4
538  whd in E4:(??%?); destruct % try @H1 try @H2
539  try  @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)
540  try  @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2)
541] qed. 
542
543(* We'll need to implement proper translation of pointers if we really do memory
544   spaces.
545(* This function performs leibniz-style subst if r1 = r2, and fails otherwise. *)
546definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝
547λr1,r2,P.
548  match r1 return λx.P x → res (P r2) with
549  [ Any ⇒   match r2 return λx.P Any → res (P x) with [ Any ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
550  | Data ⇒  match r2 return λx.P Data → res (P x) with [ Data ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
551  | IData ⇒ match r2 return λx.P IData → res (P x) with [ IData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
552  | PData ⇒ match r2 return λx.P PData → res (P x) with [ PData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
553  | XData ⇒ match r2 return λx.P XData → res (P x) with [ XData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
554  | Code ⇒  match r2 return λx.P Code → res (P x) with [ Code ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
555  ].
556
557(* Simple application of [check_region] to translate between terms. *)
558definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝
559λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
560*)
561axiom FIXME : String.
562
563(* Given a source and target type, translate an expession of type source to type target *)
564definition translate_cast : ∀P. ∀ty1:type.∀ty2:type. (Σe:CMexpr (typ_of_type ty1). expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝
565λP,ty1,ty2.
566match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with
567[ Tint sz1 sg1 ⇒ λe.
568    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
569    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint ? sg1 sz2 ?) e)
570  (*  | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu ?? | _ ⇒ Ofloatofint ??]) e)*)
571    | Tpointer _ ⇒ OK ? (Op1 ?? (Optrofint ??) e)
572    | Tarray _ _ ⇒ OK ? (Op1 ?? (Optrofint ??) e)
573    | _ ⇒ Error ? (msg TypeMismatch)
574    ]
575(* | Tfloat sz1 ⇒ λe.
576    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
577    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat ? sz2 | _ ⇒ Ointoffloat ? sz2 ]) e, ?»
578    | Tfloat sz2 ⇒ Error ? (msg FIXME) (* OK ? «Op1 ?? (Oid ?) e, ?» (* FIXME *) *)
579    | _ ⇒ Error ? (msg TypeMismatch)
580    ] *)
581| Tpointer _ ⇒ λe. (* will need changed for memory regions *)
582    match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with
583    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2 ?) e, ?»
584    | Tarray _ _ ⇒ (*translate_ptr ? r1 r2 e*) OK ? e
585    | Tpointer _ ⇒ OK ? e
586    | _ ⇒ Error ? (msg TypeMismatch)
587    ]
588| Tarray _ _ ⇒ λe. (* will need changed for memory regions *)
589    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
590    [ Tint sz2 sg2 ⇒ OK ? «Op1 ASTptr (ASTint sz2 sg2) (Ointofptr sz2 ?) e, ?»
591    | Tarray _ _ ⇒ OK ? e
592    | Tpointer _ ⇒ OK ? e
593    | _ ⇒ Error ? (msg TypeMismatch)
594    ]
595| _ ⇒ λ_. Error ? (msg TypeMismatch)
596]. whd normalize nodelta @pi2
597qed.
598
599(* Translate Clight exprs into Cminor ones.
600  Arguments :
601  - vars:var_types, an environment mapping each variable to a couple (allocation mode, type)
602  - e:expr, the expression to be converted
603  Result : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars))
604  that is, either
605  . an error
606  . an expression e', matching the type of e, such that e' respect the property that all variables
607    in it are not global. In effect, [translate_expr] will replace global variables by constant symbols.
608*)
609let rec translate_expr (vars:var_types) (e:expr) on e : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) ≝
610match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with
611[ Expr ed ty ⇒
612  match ed with
613  [ Econst_int sz i ⇒
614      match ty return λty. res (Σe':CMexpr (typ_of_type ty).  expr_vars ? e' (local_id vars)) with
615      [ Tint sz' sg ⇒ intsize_eq_elim' sz sz' (λsz,sz'. res (Σe':CMexpr (typ_of_type (Tint sz' sg)). expr_vars ? e' (local_id vars)))
616                        (OK ? «Cst ? (Ointconst sz sg i), ?»)
617                        (Error ? (msg TypeMismatch))
618      | _ ⇒ Error ? (msg TypeMismatch)
619      ]
620 (* | Econst_float f ⇒
621      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
622      [ Tfloat sz ⇒ OK ? «Cst ? (Ofloatconst sz f), ?»
623      | _ ⇒ Error ? (msg TypeMismatch)
624      ] *)
625  | Evar id ⇒
626      (* E is an equality proof of the shape "lookup' vars id = Ok <c,t>" *) 
627      do 〈c,t〉 as E ← lookup' vars id;
628      match c return λx. (c = x) → res (Σe':CMexpr ?. ?) with
629      [ Global r ⇒ λHeq_c.
630          (* We are accessing a global variable in an expression. Its Cminor counterpart also depends on
631             its access mode:
632             - By_value q, where q is a memory chunk specification (whitch should match the type of the global)
633             - By_reference, and we only take the adress of the variable
634             - By_nothing : error
635           *)
636          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
637          [ By_value t ⇒ OK ? «Mem t (Cst ? (Oaddrsymbol id 0)), ?» (* Mem is "load" in compcert *)
638          | By_reference ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
639          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
640          ]
641      | Stack n ⇒ λHeq_c.
642          (* We have decided that the variable should be allocated on the stack,
643           * because its adress was taken somewhere or becauste it's a structured data. *)
644          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
645          [ By_value t ⇒ OK ? «Mem t (Cst ? (Oaddrstack n)), ?»
646          | By_reference ⇒ (*match r return λr. res (Σe':CMexpr (ASTptr r). ?) with
647                             [ Any ⇒*) OK ? «Cst ? (Oaddrstack n), ?» (*
648                             | _ ⇒ Error  ? [MSG BadlyTypedAccess; CTX ? id]
649                             ]*)
650          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
651          ]
652          (* This is a local variable. Keep it as an identifier in the Cminor code, ensuring that the type of the original expr and of ty match. *)
653      | Local ⇒ λHeq_c. type_should_eq t ty (λt.Σe':CMexpr (typ_of_type t).expr_vars (typ_of_type t) e' (local_id vars))  («Id (typ_of_type t) id, ?»)
654      ] (refl ? c)
655  | Ederef e1 ⇒
656      do e1' ← translate_expr vars e1;
657      (* According to the way the data pointed to by e1 is accessed, the generated Cminor code will vary.
658        - if e1 is a kind of int* ptr, then we load ("Mem") the ptr returned by e1
659        - if e1 is a struct* or a function ptr, then we acess by reference, in which case we :
660           1) check the consistency of the regions in the type of e1 and in the access mode of its type
661           2) return directly the converted CMinor expression "as is" (TODO : what is the strange notation with the ceil function and the mapsto ?)
662      *)
663      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
664      [ ASTptr ⇒ λe1'.
665          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
666          [ By_value t ⇒ OK ? «Mem t (pi1 … e1'), ?»
667          | By_reference ⇒ OK ? e1'
668          | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
669          ]
670      | _ ⇒ λ_. Error ? (msg TypeMismatch)
671      ] e1'             
672  | Eaddrof e1 ⇒
673      do e1' ← translate_addr vars e1;
674      match typ_of_type ty return λx.res (Σz:CMexpr x.?) with
675      [ ASTptr ⇒ OK ? e1'
676(*          match e1' with
677          [ mk_DPair r1 e1' ⇒ region_should_eq r1 r ? e1'
678          ]*)
679      | _ ⇒ Error ? (msg TypeMismatch)
680      ]
681  | Eunop op e1 ⇒
682     match op
683      return λx. (op = x) → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars))
684      with
685      [ Onotbool ⇒ λHop.
686        match typ_of_type ty
687        return λy. (typ_of_type ty = y) → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars))
688        with
689        [ ASTint sz sg ⇒  λHtyp_of_type.
690          match sz
691          return λz. (sz = z) → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars))
692          with
693          [ I32 ⇒ λHsz.
694            do op' ← translate_unop (typ_of_type (typeof e1)) (typ_of_type ty) op;
695            do e1' ← translate_expr vars e1;
696            OK ? «Op1 ?? op' e1', ?»
697          | _ ⇒ λHsz.
698            Error ? (msg TypeMismatch)
699          ] (refl ? sz)
700        | _ ⇒ λHtyp_of_type.
701          Error ? (msg TypeMismatch)
702        ] (refl ? (typ_of_type ty))       
703      | _ ⇒ λHop.
704        do op' ← translate_unop (typ_of_type (typeof e1)) (typ_of_type ty) op;
705        do e1' ← translate_expr vars e1;
706        OK ? «Op1 ?? op' e1', ?»
707      ] (refl ? op)
708  | Ebinop op e1 e2 ⇒
709      do e1' ← translate_expr vars e1;
710      do e2' ← translate_expr vars e2;
711      do e' as E ← translate_binop op (typeof e1) e1' (typeof e2) e2' ty;
712      OK ? «e', ?»
713  | Ecast ty1 e1 ⇒
714      do e1' ← translate_expr vars e1;
715      do e' ← translate_cast ? (typeof e1) ty1 e1';
716      do e' ← typ_should_eq (typ_of_type ty1) (typ_of_type ty) ? e';
717      OK ? e'
718  | Econdition e1 e2 e3 ⇒
719      do e1' ← translate_expr vars e1;
720      do e2' ← translate_expr vars e2;
721      do e2' ← typ_should_eq (typ_of_type (typeof e2)) (typ_of_type ty) ? e2';
722      do e3' ← translate_expr vars e3;
723      do e3' ← typ_should_eq (typ_of_type (typeof e3)) (typ_of_type ty) ? e3';
724      match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → res ? with
725      [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' e3', ?»
726      | _ ⇒ λ_.Error ? (msg TypeMismatch)
727      ] e1'
728  | Eandbool e1 e2 ⇒
729      do e1' ← translate_expr vars e1;
730      do e2' ← translate_expr vars e2;
731      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
732      [ Tint sz sg ⇒
733          do e2' ← type_should_eq ? (Tint sz sg) (λx.Σe:CMexpr (typ_of_type x).?) e2';
734          match typ_of_type (typeof e1)
735          return λx.
736            (Σe:CMexpr x. expr_vars ? e (local_id vars)) → (res ?)
737          with
738          [ ASTint sz1 _ ⇒ λe1'.
739            OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz sg (zero ?))), ?»
740          | _ ⇒ λ_. Error ? (msg TypeMismatch)
741          ] e1'
742      | _ ⇒ Error ? (msg TypeMismatch)
743      ]
744(*  | Eandbool e1 e2 ⇒
745      do e1' ← translate_expr vars e1;
746      do e2' ← translate_expr vars e2;
747      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
748      [ Tint sz sg ⇒
749        match sz
750        return λsz'. (sz = sz') → res (Σe':CMexpr (typ_of_type ?). ?)
751        with
752        [ I32 ⇒ λHsz_eq.
753          do e2' ← type_should_eq ? (Tint I32 sg) (λx.Σe:CMexpr (typ_of_type x).?) e2';
754          match typ_of_type (typeof e1)
755          return λx.
756            (Σe:CMexpr x. expr_vars ? e (local_id vars)) → (res ?)
757          with
758          [ ASTint sz1 _ ⇒ λe1'.
759            OK ? «Cond ??? e1' e2' (Cst ? (Ointconst I32 sg (zero ?))), ?»
760          | _ ⇒ λ_. Error ? (msg TypeMismatch)
761          ] e1'
762        | _ ⇒ λ_. Error ? (msg TypeMismatch)
763        ] (refl ? sz)
764      | _ ⇒ Error ? (msg TypeMismatch)
765      ]*)
766  | Eorbool e1 e2 ⇒
767      do e1' ← translate_expr vars e1;
768      do e2' ← translate_expr vars e2;
769      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
770      [ Tint sz sg ⇒
771        do e2' ← type_should_eq ? (Tint sz sg) (λx.Σe:CMexpr (typ_of_type x).?) e2';
772        match typ_of_type (typeof e1)
773        return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with
774        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz sg (repr ? 1))) e2', ?»
775        | _ ⇒ λ_. Error ? (msg TypeMismatch)
776        ] e1'
777      | _ ⇒ Error ? (msg TypeMismatch)
778      ]     
779  | Esizeof ty1 ⇒
780      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
781      [ Tint sz sg ⇒ OK ? «Cst ? (Ointconst sz sg (repr ? (sizeof ty1))), ?»
782      | _ ⇒ Error ? (msg TypeMismatch)
783      ]     
784  | Efield e1 id ⇒
785      match typeof e1 with
786      [ Tstruct _ fl ⇒
787          do e1' ← translate_addr vars e1;
788(*          match e1' with
789          [ mk_DPair r e1' ⇒*)
790            do off ← field_offset id fl;
791            match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
792            [ By_value t ⇒
793                OK ? «Mem t (Op2 ? (ASTint I16 Signed (* XXX efficiency? *)) ?
794                                   (Oaddp …) e1' (Cst ? (Ointconst I16 Signed (repr ? off)))),?»
795            | By_reference ⇒
796(*                do e1' ← region_should_eq r r' ? e1';*)
797                OK ? «Op2 ASTptr (ASTint I16 Signed (* XXX efficiency? *)) ASTptr
798                        (Oaddp …) e1' (Cst ? (Ointconst I16 Signed (repr ? off))),?»
799            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
800            ]
801      | Tunion _ _ ⇒
802          do e1' ← translate_addr vars e1;
803            match access_mode ty return λt.λ_. res (Σz:CMexpr t.?) with
804            [ By_value t ⇒ OK ? «Mem t e1', ?»
805            | By_reference ⇒ OK ? e1'
806            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
807            ]
808      | _ ⇒ Error ? (msg BadlyTypedAccess)
809      ]           
810  | Ecost l e1 ⇒
811      do e1' ← translate_expr vars e1;
812      do e' ← OK ? «Ecost ? l e1',?»;
813      typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e'     
814  ]
815]
816
817(* Translate addr takes an expression e1, and returns a Cminor code computing the address of the result of [e1].   *)
818and translate_addr (vars:var_types) (e:expr) on e : res ((*𝚺r.*) Σe':CMexpr ASTptr. expr_vars ? e' (local_id vars)) ≝
819match e with
820[ Expr ed _ ⇒
821  match ed with
822  [ Evar id ⇒
823      do 〈c,t〉 ← lookup' vars id;
824      match c return λ_. res (Σz:CMexpr ASTptr.?) with
825      [ Global r ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
826      | Stack n ⇒ OK ? «Cst ? (Oaddrstack n), ?»
827      | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *)
828      ]
829  | Ederef e1 ⇒
830      do e1' ← translate_expr vars e1;
831      match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (Σz:CMexpr ASTptr. expr_vars ? z (local_id vars)) with
832      [ ASTptr ⇒ λe1'.OK ? e1'
833      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
834      ] e1'
835  | Efield e1 id ⇒
836      match typeof e1 with
837      [ Tstruct _ fl ⇒
838          do e1' ← translate_addr vars e1;
839          do off ← field_offset id fl;
840(*          match e1' with
841          [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?)*)
842             OK ? «Op2 ASTptr (ASTint I16 Signed (* FIXME inefficient?*)) ASTptr
843                   (Oaddp I16) e1' (Cst ? (Ointconst I16 Signed (repr ? off))), ?»
844      | Tunion _ _ ⇒ translate_addr vars e1
845      | _ ⇒ Error ? (msg BadlyTypedAccess)
846      ]
847  | _ ⇒ Error ? (msg BadLvalue)
848  ]
849].
850whd try @I
851[ >E whd >Heq_c @refl
852| 2,3: @pi2
853| cases e1' //
854| cases e1' //
855| @(translate_binop_vars … E) @pi2
856| % [ % ] @pi2
857| % [ % @pi2 ] whd @I
858| % [ % [ @pi2 | @I ] | @pi2 ]
859| % [ @pi2 | @I ]
860| % [ @pi2 | @I ]
861| @pi2
862| @pi2
863| % [ @pi2 | @I ]
864] qed.
865
866(* We provide a function to work out how to do an assignment to an lvalue
867   expression.  It is used for both Clight assignments and Clight function call
868   destinations, but doesn't take the value to be assigned so that we can use
869   it to form a single St_store when possible (and avoid introducing an
870   unnecessary temporary variable and assignment).
871   *)
872inductive destination (vars:var_types) : Type[0] ≝
873| IdDest : ∀id,ty. local_id vars id (typ_of_type ty) → destination vars
874| MemDest : (Σe:CMexpr ASTptr.expr_vars ? e (local_id vars)) → destination vars.
875
876(* Let a source Clight expression be assign(e1, e2). First of all, observe that [e1] is a
877  /Clight/ expression, not converted by translate_expr. We thus have to do part of the work
878  of [translate_expr] in this function. [translate_dest] will convert e1
879   into a proper destination for an assignement operation. We proceed by case analysis on e1.
880   - if e1 is a variable [id], then we proceed by case analysis on its allocation mode:
881      - if [id] is allocated locally (in a register), then id becomes directly
882        the target for the assignement, as (IdDest vars id t H), where t is the type
883        of id, and H asserts that id is indeed a local variable.
884      - if [id] is a global variable stored in region [r], then we perform [translate_expr]'s
885        job and return an adress, given as a constant symbol corresponding to [id], with
886        region r and memory chunk specified by the access mode of the rhs type ty2 of [e2].
887      - same thing for stack-allocated variables, except that we don't specify any region.
888   - if e1 is not a variable, we use [translate_addr] to generate a Cminor expression computing
889    the adres of e1
890*)
891definition translate_dest ≝
892λvars,e1.
893  match e1 with
894  [ Expr ed1 ty1 ⇒
895      match ed1 with
896      [ Evar id ⇒
897          do 〈c,t〉 as E ← lookup' vars id;
898          match c return λx.? → ? with
899          [ Local ⇒ λE. OK ? (IdDest vars id t ?)
900          | Global r ⇒ λE. OK ? (MemDest ? (Cst ? (Oaddrsymbol id 0)))
901          | Stack n ⇒ λE. OK ? (MemDest ? (Cst ? (Oaddrstack n)))
902          ] E
903      | _ ⇒
904          do e1' ← translate_addr vars e1;
905          OK ? (MemDest ? e1')
906      ]
907  ].
908whd // >E @refl
909qed.
910
911(* [lenv] is the type of maps from Clight labels to Cminor labels. *)
912definition lenv ≝ identifier_map SymbolTag (identifier Label).
913
914axiom MissingLabel : String.
915
916(* Find the Cminor label corresponding to [l] or fail. *)
917definition lookup_label ≝
918λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).
919
920(* True iff the Cminor label [l] is in the codomain of [lbls] *)
921definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup_label lbls l' = OK ? l.
922
923(* True iff The Clight label [l] is in the domain of [lbls] *)
924definition label_in_domain ≝ λlbls:lenv. λl. present ?? lbls l.
925
926let rec fresh_list_for_univ (l:list (identifier Label)) (u:universe Label) ≝
927match l with
928[ nil ⇒ True
929| cons elt tl ⇒ fresh_for_univ ? elt u ∧ fresh_list_for_univ tl u].
930
931record labgen : Type[0] ≝ {
932  labuniverse   : universe Label;
933  label_genlist    : list (identifier Label);
934  genlist_is_fresh : fresh_list_for_univ label_genlist labuniverse
935}.
936
937lemma fresh_list_stays_fresh : ∀l,tmp,u,u'. fresh_list_for_univ l u → 〈tmp,u'〉=fresh Label u → fresh_list_for_univ l u'.
938#l elim l
939[ 1: normalize //
940| 2: #hd #tl #Hind #tmp #u #u' #HA #HB
941  whd
942  @conj
943  [ 1: whd in HA ⊢ ?;
944    elim HA #HAleft #HAright
945    @(fresh_remains_fresh ? hd tmp u u') assumption
946  | 2: whd in HA ⊢ ?;
947    elim HA #HAleft #HAright   
948    @Hind //
949  ]
950]
951qed.
952
953definition In ≝ λelttype.λelt.λl.Exists elttype (λx.x=elt) l.   
954
955definition generate_fresh_label :
956 ∀ul. Σlul:(identifier Label × labgen).
957               (And (∀lab. In ? lab (label_genlist ul) → In ? lab (label_genlist (snd … lul)))
958                   (In ? (fst … lul) (label_genlist (snd … lul)))) ≝
959λul.
960let 〈tmp,u〉 as E ≝ fresh ? (labuniverse ul) in
961 «〈tmp, mk_labgen u (tmp::(label_genlist ul)) ?〉, ?».
962[ 1: normalize @conj
963  [ 1: @(fresh_is_fresh ? tmp u (labuniverse ul) ?) assumption
964  | 2: @fresh_list_stays_fresh // ]
965| @conj /2/
966]
967qed.
968
969let rec labels_defined (s:statement) : list ident ≝
970match s with
971[ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2
972| Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2
973| Swhile _ s ⇒ labels_defined s
974| Sdowhile _ s ⇒ labels_defined s
975| Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
976| Sswitch _ ls ⇒ labels_defined_switch ls
977| Slabel l s ⇒ l::(labels_defined s)
978| Scost _ s ⇒ labels_defined s
979| _ ⇒ [ ]
980]
981and labels_defined_switch (ls:labeled_statements) : list ident ≝
982match ls with
983[ LSdefault s ⇒ labels_defined s
984| LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls
985].
986
987definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s).
988
989(* For each label l in s, there exists a matching label l' = lenv(l) defined in s' *)
990definition labels_translated : lenv → statement → stmt → Prop ≝
991λlbls,s,s'.  ∀l.
992  (Exists ? (λl'.l' = l) (labels_defined s)) →
993  ∃l'. lookup_label lbls l = (OK ? l') ∧ ldefined s' l'.
994
995
996(* Invariant on statements, holds during conversion to Cminor *)
997definition stmt_inv ≝  λvars. stmt_P (stmt_vars (local_id vars)).
998
999definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝
1000λA,B,f,oa.
1001match oa with
1002[ None ⇒ OK ? (None ?)
1003| Some a ⇒ do b ← f a; OK ? (Some ? b)
1004].
1005
1006definition translate_expr_sigma : ∀vars:var_types. expr → res (Σe:(𝚺t:typ.CMexpr t). match e with [ mk_DPair t e ⇒ expr_vars t e (local_id vars) ]) ≝
1007λv,e.
1008  do e' ← translate_expr v e;
1009  OK (Σe:(𝚺t:typ.CMexpr t).?) «❬?, e'❭, ?».
1010whd @pi2
1011qed.
1012
1013(* Add the list of typed variables tmpenv to the environment [var_types] with
1014   the allocation mode Local. *)
1015definition add_tmps : var_types → list (ident × type) → var_types ≝
1016λvs,tmpenv.
1017  foldr ?? (λidty,vs. add ?? vs (\fst idty) 〈Local, \snd idty〉) vs tmpenv.
1018
1019record tmpgen (vars:var_types) : Type[0] ≝ {
1020  tmp_universe : universe SymbolTag;
1021  tmp_env : list (ident × type);
1022  tmp_ok : fresh_map_for_univ … (add_tmps vars tmp_env) tmp_universe;
1023  tmp_preserved :
1024    ∀id,ty. local_id vars id ty → local_id (add_tmps vars tmp_env) id ty
1025}.
1026
1027definition alloc_tmp : ∀vars. type → tmpgen vars → ident × (tmpgen vars) ≝
1028λvars,ty,g.
1029  let 〈tmp,u〉 as E ≝ fresh ? (tmp_universe ? g) in
1030  〈tmp, mk_tmpgen ? u (〈tmp, ty〉::(tmp_env ? g)) ??〉.
1031[ #id #ty'
1032  whd in ⊢ (? → ?%??);
1033  whd in ⊢ (% → %);
1034  whd in ⊢ (? → match % with [_ ⇒ ? | _ ⇒ ?]); #H
1035  >lookup_add_miss
1036  [ @(tmp_preserved … g) @H
1037  | @(fresh_distinct … E) @(tmp_ok … g)
1038    lapply (tmp_preserved … g id ty' H)
1039    whd in ⊢ (% → %);
1040    whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?);
1041    cases (lookup ??? id)
1042    [ * | #x #_ % #E destruct ]
1043  ]
1044| @fresh_map_add
1045  [ @(fresh_map_preserved … E) @(tmp_ok … g)
1046  | @(fresh_is_fresh … E)
1047  ]
1048] qed.
1049
1050
1051lemma lookup_label_hit : ∀lbls,l,l'.
1052  lookup_label lbls l = OK ? l' →
1053  lpresent lbls l'.
1054#lbls #l #l' #E whd %{l} @E
1055qed.
1056
1057(* TODO: is this really needed now? *)
1058
1059definition tmps_preserved : ∀vars:var_types. tmpgen vars → tmpgen vars → Prop ≝
1060λvars,u1,u2.
1061  ∀id,ty. local_id (add_tmps vars (tmp_env … u1)) id ty → local_id (add_tmps vars (tmp_env … u2)) id ty.
1062
1063lemma alloc_tmp_preserves : ∀vars,tmp,u,u',q.
1064  〈tmp,u'〉 = alloc_tmp ? q u → tmps_preserved vars u u'.
1065#vars #tmp * #u1 #e1 #F1 #P1 * #u2 #e2 #F2 #P2 #q
1066whd in ⊢ (???% → ?); generalize in ⊢ (???(?%) → ?);
1067cases (fresh SymbolTag u1) in ⊢ (??%? → ???(match % with [ _ ⇒ ? ]?) → ?);
1068#tmp' #u' #E1 #E2 whd in E2:(???%); destruct
1069#id #ty #H whd in ⊢ (?%??); whd in H ⊢ %;
1070whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ];
1071>lookup_add_miss // @(fresh_distinct … E1) @F1
1072whd in H:(match % with [_ ⇒ ?|_ ⇒ ?]) ⊢ %;
1073cases (lookup ??? id) in H ⊢ %;
1074[ * | #x #_ % #E destruct ]
1075qed.
1076
1077lemma add_tmps_oblivious : ∀vars,s,u.
1078  stmt_inv vars s → stmt_inv (add_tmps vars (tmp_env vars u)) s.
1079#vars #s #u #H
1080@(stmt_P_mp … H)
1081#s' #H1 @(stmt_vars_mp … H1) #id #t #H @(tmp_preserved ? u ?? H)
1082qed.
1083
1084lemma local_id_fresh_tmp : ∀vars,tmp,u,ty,u0.
1085  〈tmp,u〉 = alloc_tmp vars ty u0 → local_id (add_tmps vars (tmp_env … u)) tmp (typ_of_type ty).
1086#vars #tmp #u #ty #u0
1087whd in ⊢ (???% → ?); generalize in ⊢ (???(?%) → ?);
1088cases (fresh SymbolTag (tmp_universe vars u0)) in ⊢ (??%? → ???(match % with [_⇒?]?) → ?);
1089* #tmp' #u' #e #E whd in E:(???%);
1090destruct
1091whd in ⊢ (?%??); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit
1092@refl
1093qed.
1094
1095
1096let rec mklabels (ul:labgen) : (identifier Label) × (identifier Label) × labgen ≝
1097  match generate_fresh_label ul with
1098  [ mk_Sig res1 H1 ⇒
1099     let 〈entry_label, ul1〉 as E1 ≝ res1 in
1100     match generate_fresh_label ul1 with
1101     [ mk_Sig res2 H2 ⇒
1102        let 〈exit_label, ul2〉 as E2 ≝ res2 in
1103        〈entry_label, exit_label, ul2〉
1104     ]
1105  ].
1106
1107(* When converting loops into gotos, and in order to eliminate blocks, we have
1108 * to convert continues and breaks into goto's, too. We add some "flags" in
1109 * in argument to [translate_statement], meaning that the next encountered break
1110 * or continue has to be converted into a goto to some contained label.
1111 * ConvertTo l1 l2 means "convert continue to goto l1 and convert break to goto l2".
1112 *)
1113inductive convert_flag : Type[0] ≝
1114| DoNotConvert : convert_flag
1115| ConvertTo    : identifier Label → identifier Label → convert_flag. (* continue, break *)
1116
1117let rec labels_of_flag (flag : convert_flag) : list (identifier Label) ≝
1118match flag with
1119[ DoNotConvert ⇒ [ ]
1120| ConvertTo continue break ⇒ continue :: break :: [ ]
1121].
1122
1123(* For a top-level expression, [label-wf] collapses to "all labels are properly declared" *)
1124definition label_wf ≝
1125λ (s : statement) .λ (s' : stmt) .λ (lbls : lenv). λ (flag : convert_flag).
1126    stmt_P (λs1. stmt_labels (λl.ldefined s' l ∨ lpresent lbls l ∨ In ? l (labels_of_flag flag)) s1) s'.
1127
1128definition return_ok : option typ → stmt → Prop ≝
1129λot.
1130stmt_P (λs.
1131  match s with [ St_return oe ⇒
1132    match oe with [ Some e ⇒ Some ? (dpi1 … e) = ot | None ⇒ None ? = ot ]
1133  | _ ⇒ True ]).
1134
1135(* trans_inv is the invariant which is enforced during the translation from Clight to Cminor.
1136  The involved arguments are the following:
1137  . vars:var_types, an environment mapping variables to their types and allocation modes
1138  . lbls:lenv, a mapping from old (Clight) to fresh and new (Cminor) labels,
1139  . s:statement, a Clight statement,
1140  . uv, a fresh variable generator (containing itself some invariants)
1141  . flag, wich maps "break" and "continue" to "gotos"
1142  . su', a couple of a Cminor statement and fresh variable generator.
1143*)
1144definition trans_inv : ∀vars:var_types . ∀lbls:lenv . statement → tmpgen vars → convert_flag → option typ → ((tmpgen vars) × labgen × stmt) → Prop ≝
1145λvars,lbls,s,uv,flag,rettyp,su'.
1146  let 〈uv', ul', s'〉 ≝ su' in
1147  stmt_inv (add_tmps vars (tmp_env … uv')) s' ∧   (* remaining variables in s' are local*)
1148  labels_translated lbls s s' ∧                   (* all the labels in s are transformed in label of s' using [lbls] as a map *)
1149  tmps_preserved vars uv uv' ∧                    (* the variables generated are local and grows in a monotonic fashion *)
1150  return_ok rettyp s' ∧                           (* return statements have correct typ *)
1151  label_wf s s' lbls flag.                        (* labels are "properly" declared, as defined in [ŀabel_wf].*)
1152
1153axiom ReturnMismatch : String.
1154
1155let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (rettyp:option typ) (s:statement) on s
1156  : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) ≝
1157match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) with
1158[ Sskip ⇒ OK ? «〈uv, ul, St_skip〉, ?»
1159| Sassign e1 e2 ⇒
1160    do e2' ← translate_expr vars e2;  (* rhs *)
1161    do dest ← translate_dest vars e1; (* e1 *)
1162    match dest with
1163    [ IdDest id ty p ⇒
1164       (* Don't compare the Clight types, or we'll have to deal with
1165          array/pointer punning. *)
1166       do e2' ← typ_should_eq (typ_of_type (typeof e2)) (typ_of_type ty) ? e2';
1167       OK ? «〈uv, ul, St_assign ? id e2'〉, ?»
1168    | MemDest e1' ⇒
1169       OK ? «〈uv, ul, St_store ? e1' e2'〉, ?»
1170    ]
1171| Scall ret ef args ⇒
1172    do ef' ← translate_expr vars ef;
1173    do ef' ← typ_should_eq (typ_of_type (typeof ef)) ASTptr ? ef';
1174    do args' ← mmap_sigma ??? (translate_expr_sigma vars) args;
1175    match ret with
1176    [ None ⇒ OK ? «〈uv, ul, St_call (None ?) ef' args'〉, ?»
1177    | Some e1 ⇒
1178        do dest ← translate_dest vars e1;
1179        match dest with
1180        [ IdDest id ty p ⇒ OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?»
1181        | MemDest e1' ⇒
1182            let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in
1183            OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) e1' (Id ? tmp))〉, ?»
1184        ]
1185    ]
1186| Ssequence s1 s2 ⇒
1187    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
1188    do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag rettyp s2;
1189    OK ? «〈fgens2, St_seq s1' s2'〉, ?»
1190| Sifthenelse e1 s1 s2 ⇒
1191    do e1' ← translate_expr vars e1;
1192    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → res ? with
1193    [ ASTint _ _ ⇒ λe1'.
1194         do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
1195         do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag rettyp s2;
1196        OK ? «〈fgens2, St_ifthenelse ?? e1' s1' s2'〉, ?»
1197    | _ ⇒ λ_.Error ? (msg TypeMismatch)
1198    ] e1'
1199(* Performing loop conversions while keeping good cost labelling properties is
1200   a little tricky.  In principle we should have a cost label in each branch,
1201   but the behaviour of the next stage means that we can put in Cminor skips and
1202   goto labels before the cost label. *)
1203| Swhile e1 s1 ⇒
1204    do e1' ← translate_expr vars e1;
1205    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → res ? with
1206    [ ASTint _ _ ⇒ λe1'.         
1207        let 〈labels, ul1〉 as E1 ≝ mklabels ul in
1208        let 〈entry, exit〉 as E2 ≝ labels in
1209        do «fgens2, s1',H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) rettyp s1;
1210        let converted_loop ≝
1211          St_label entry
1212          (St_seq
1213            (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) St_skip)
1214            (St_label exit St_skip))
1215        in         
1216          OK ? «〈fgens2, converted_loop〉, ?»
1217    | _ ⇒ λ_.Error ? (msg TypeMismatch)
1218    ] e1'
1219| Sdowhile e1 s1 ⇒
1220    do e1' ← translate_expr vars e1;
1221    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → res ? with
1222    [ ASTint _ _ ⇒ λe1'.
1223        let 〈labels, ul1〉 as E1 ≝ mklabels ul in
1224        let 〈condexpr, exit〉 as E2 ≝ labels in
1225        let 〈body, ul2〉 ≝ generate_fresh_label … ul1 in
1226        do «fgens2, s1', H1» ← translate_statement vars uv ul2 lbls (ConvertTo condexpr exit) rettyp s1;
1227        (* This is particularly carefully implemented, we need to reach the
1228           cost label in s1' or the cost label after the loop (if they are
1229           present) after the ifthenelse, and we're only allowed skips and
1230           goto labels in between.  So we structure it like a while with a goto
1231           into the middle (the CFG will be essentially the same, anyway.) *)
1232        let converted_loop ≝
1233        St_seq
1234          (St_seq
1235            (St_goto body)
1236            (St_label condexpr
1237              (St_ifthenelse ?? e1'
1238                (St_label body
1239                  (St_seq
1240                    s1'
1241                    (St_goto condexpr)))
1242                St_skip)))
1243          (St_label exit St_skip)
1244        in
1245        OK ? «〈fgens2, converted_loop〉, ?»
1246    | _ ⇒ λ_.Error ? (msg TypeMismatch)
1247    ] e1'
1248| Sfor s1 e1 s2 s3 ⇒
1249    do e1' ← translate_expr vars e1;
1250    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → res ? with
1251    [ ASTint _ _ ⇒ λe1'.
1252        let 〈labels, ul1〉 as E ≝ mklabels ul in
1253        let 〈continue, exit〉 as E2 ≝ labels in
1254        let 〈entry, ul2〉 ≝ generate_fresh_label … ul1 in
1255        do «fgens2, s1', H1» ← translate_statement vars uv ul2 lbls flag rettyp s1;
1256        (* The choice of flag is arbitrary - Clight's semantics give no meaning
1257           to continue or break in s2 because in C it must be an expression. *)
1258        do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) lbls flag rettyp s2;
1259        do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) lbls (ConvertTo continue exit) rettyp s3;
1260        let converted_loop ≝
1261          St_seq
1262            s1'
1263            (St_label entry
1264              (St_seq
1265                (St_ifthenelse ?? e1' (St_seq s3' (St_label continue (St_seq s2' (St_goto entry)))) St_skip)
1266                (St_label exit St_skip)
1267            ))
1268        in
1269          OK ? «〈fgens4, converted_loop〉, ?»
1270    | _ ⇒ λ_.Error ? (msg TypeMismatch)
1271    ] e1'
1272| Sbreak ⇒
1273   match flag return λf.flag = f → ? with
1274   [ DoNotConvert ⇒ λEflag.
1275     Error ? (msg FIXME)
1276   | ConvertTo continue_label break_label ⇒ λEflag.
1277     OK ? «〈uv, ul, St_goto break_label〉, ?»
1278   ] (refl ? flag)
1279| Scontinue ⇒
1280  match flag return λf.flag = f → ? with
1281  [ DoNotConvert ⇒ λEflag.
1282    Error ? (msg FIXME)
1283  | ConvertTo continue_label break_label ⇒ λEflag.
1284    OK ? «〈uv, ul, St_goto continue_label〉, ?»
1285  ] (refl ? flag)
1286| Sreturn ret ⇒
1287    match ret with
1288    [ None ⇒
1289        match rettyp return λx.res (Σy.trans_inv … x y) with
1290        [ None ⇒ OK ? «〈uv, ul, St_return (None ?)〉, ?»
1291        | _ ⇒ Error ? (msg ReturnMismatch)
1292        ]
1293    | Some e1 ⇒
1294        match rettyp return λx.res (Σy.trans_inv … x y) with
1295        [ Some rty ⇒
1296            do e1' ← translate_expr vars e1;
1297            do e1' ← typ_should_eq (typ_of_type (typeof e1)) rty ? e1';
1298            OK ? «〈uv, ul, St_return (Some ? (mk_DPair … e1'))〉, ?»
1299        | _ ⇒ Error ? (msg ReturnMismatch)
1300        ]
1301    ]
1302| Sswitch e1 ls ⇒ Error ? (msg FIXME)
1303| Slabel l s1 ⇒
1304    do l' as E ← lookup_label lbls l;
1305    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
1306    OK ? «〈fgens1, St_label l' s1'〉, ?»
1307| Sgoto l ⇒
1308    do l' as E ← lookup_label lbls l;
1309    OK ? «〈uv, ul, St_goto l'〉, ?»
1310| Scost l s1 ⇒
1311    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
1312    OK ? «〈fgens1, St_cost l s1'〉, ?»
1313].
1314try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
1315try (@I)
1316try (#l #H elim H)
1317try (#size #sign #H assumption)
1318try (#H1 try #H2 assumption)
1319[ 1,5: @(tmp_preserved … p) ]
1320[ 1,3: elim e2' | 2,9,23: elim e1' | 4,7,13: elim ef' ]
1321[ 1,2,3,4,5,6,7,8 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
1322[ 1: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
1323             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
1324             | 3: elim args' // ]
1325| 7: (* we should be able to merge this case with the previous ... *)
1326     @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
1327             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
1328             | 3: elim args' // ]
1329| 2: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp)
1330| 3:  @(All_mp (𝚺 t:typ.expr t) (λe. match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars)]))
1331       [ 1: #a #Ha elim a in Ha ⊢ ?; #ta #a #Ha whd @(expr_vars_mp ?? (local_id vars))
1332       [ 1: #i0 #t0 #H0 @(tmp_preserved vars uv1 i0 t0 H0)
1333       | 2: assumption ]
1334       | 2: elim args' // ]
1335| 4: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) ]
1336[ 1: #size #sign | 2: ]
1337[ 1,2: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ]
1338try @refl (* Does (at least) the return_ok cases *)
1339try @(match fgens1 return λx.x=fgens1 → ? with
1340     [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1))
1341try @(match fgens2 return λx.x=fgens2 → ? with
1342     [ mk_Prod uv2 ul2 ⇒ λHfgens2.? ] (refl ? fgens2))
1343try @(match fgens3 return λx.x=fgens3 → ? with
1344     [ mk_Prod uv3 ul3 ⇒ λHfgens3.? ] (refl ? fgens3))
1345try @(match fgens4 return λx.x=fgens4 → ? with
1346     [ mk_Prod uv4 ul4 ⇒ λHfgens4.? ] (refl ? fgens4))
1347whd in H1 H2 H3 ⊢ ?; destruct whd nodelta in H1 H2 H3;
1348try (elim H1 -H1 * * * #Hstmt_inv1 #Hlabels_tr1 #Htmps_pres1 #Hret1)
1349try (elim H2 -H2 * * * #Hstmt_inv2 #Hlabels_tr2 #Htmps_pres2 #Hret2)
1350try (elim H3 -H3 * * * #Hstmt_inv3 #Hlabels_tr3 #Htmps_pres3 #Hret3)
1351[ 1,2: #Hind1 #Hind2 | 3,4,8,10: #Hind | 5: #Hind1 #Hind2 #Hind3 ]
1352try @conj try @conj try @conj try @conj try @conj try @conj try (whd @I) try assumption
1353[ 1,7: @(stmt_P_mp … Hstmt_inv1) #e #Hvars @(stmt_vars_mp … Hvars) #i #t #Hlocal @(Htmps_pres2 … Hlocal)
1354| 2: #l #H cases (Exists_append ???? H) #Hcase
1355         [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
1356           [ 1: @(proj1 ?? Hlabel)
1357           | 2: normalize @Exists_append_l @(proj2 … Hlabel) ]
1358         | 2: elim (Hlabels_tr2 l Hcase) #label #Hlabel @(ex_intro … label) @conj
1359           [ 1: @(proj1 ?? Hlabel)
1360           | 2: normalize @Exists_append_r @(proj2 … Hlabel) ]
1361         ]
1362| 3,9: #id #ty #H @(Htmps_pres2 … (Htmps_pres1 id ty H)) ]
1363[ 1: @(stmt_P_mp … Hind2) | 2: @(stmt_P_mp … Hind1) ]
1364[ 1,2: #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1365     #l * try * [ 1,4: #H %1 %1 normalize in H ⊢ %; try (@Exists_append_l @H); try (@Exists_append_r @H)
1366                | 2,5: #H %1 %2 assumption
1367                | 3,6: #H %2 assumption ]
1368(* if/then/else *)
1369| 3: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
1370| 4: whd #l #H
1371       cases (Exists_append ???? H) #Hcase
1372         [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
1373           [ 1: @(proj1 ?? Hlabel)
1374           | 2: normalize @Exists_append_l @(proj2 … Hlabel) ]
1375         | 2: elim (Hlabels_tr2 l Hcase) #label #Hlabel @(ex_intro … label) @conj
1376           [ 1: @(proj1 ?? Hlabel)
1377           | 2: normalize @Exists_append_r @(proj2 … Hlabel) ]
1378         ]
1379]                 
1380[ 1: 1: @(stmt_P_mp … Hind2) | 2: @(stmt_P_mp … Hind1) ]
1381[ 1,2: #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1382     #l * try * [ 1,4: #H %1 %1 normalize in H ⊢ %; try (@Exists_append_l @H); try (@Exists_append_r @H)
1383                | 2,5: #H %1 %2 assumption
1384                | 3,6: #H %2 assumption ] ]
1385try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I try assumption
1386[ 1,7,19: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
1387| 2,8: whd #l #H normalize in H;
1388       elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label)
1389       @conj
1390       [ 1,3: @(proj1 … Hlabel)
1391       | 2,4: whd @or_intror normalize in ⊢ (???%);
1392              [ @Exists_append_l @Exists_append_l @Exists_append_l | %2 @Exists_append_l @Exists_append_l @Exists_append_l ]
1393              @(proj2 … Hlabel) ]
1394| whd %1 %1 normalize /2/
1395| 4,12: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1396   #l * try * [ 1,5: #H %1 %1 normalize %2 [ 2: %2 ] @Exists_append_l @Exists_append_l try @Exists_append_l @H
1397              | 2,6: #H %1 %2 assumption
1398              | 3,7: #H <H %1 %1 normalize /2/
1399              | 4,8: #H normalize in H; elim H [ 1,3: #E <E %1 %1 normalize %2 [2: %2]
1400                                                 @Exists_append_r normalize /2/
1401                                               | 2,4: * ]
1402              ]
1403| normalize %1 %1 %1 //
1404| 6,11: normalize %1 %1 %2 [ @Exists_append_r normalize /2/ | %1 % ]
1405| whd %1 %1 normalize %2 %1 %
1406| 10,13: normalize %1 %1 %1 %
1407| normalize %1 %1 %2 %2 /2/
1408| whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
1409               | 2: #H elim (Hlabels_tr1 label H)
1410                    #lab * #Hlookup #Hdef @(ex_intro … lab) @conj
1411                    [ 1: // | 2: whd %2 assumption ]
1412               ]
1413| normalize %1 %1 %1 %
1414| @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1415  #l * try * [ 1: #H %1 %1 normalize %2 @H
1416             | 2: #H %1 %2 assumption
1417             | 3: #H %2 assumption ]
1418| @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
1419  #H @(Htmps_pres3 … (Htmps_pres2 … H))
1420| @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
1421  #H @(Htmps_pres3 … H)
1422| % //
1423| whd #l #H normalize in H;
1424  cases (Exists_append … H) #Hcase
1425  [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
1426    [ 1: @(proj1 … Hlabel)
1427    | 2: normalize @Exists_append_l @(proj2 … Hlabel)
1428    ]
1429  | 2: cases (Exists_append … Hcase) #Hcase2
1430    [ 1: elim (Hlabels_tr2 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
1431      [ 1: @(proj1 … Hlabel)
1432      | 2: normalize >append_nil >append_nil >append_cons
1433           @Exists_append_r @Exists_append_l @Exists_append_r %2
1434           @(proj2 … Hlabel)
1435      ]
1436    | 2: elim (Hlabels_tr3 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
1437      [ 1: @(proj1 … Hlabel)
1438      | 2: normalize >append_nil >append_nil >append_cons
1439         @Exists_append_r @Exists_append_l @Exists_append_l
1440         @(proj2 … Hlabel)
1441      ]
1442    ]
1443  ]
1444| #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
1445| @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1446   #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H
1447              | 2: #H %1 %2 assumption
1448              | 3: #H %2 assumption ]
1449| whd %1 %1 normalize /2/
1450| @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1451   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
1452                   @Exists_append_r @Exists_append_l @Exists_append_l
1453                   @Exists_append_l assumption
1454              | 2: #H %1 %2 assumption
1455              | 3: #H <H %1 %1 normalize
1456                   @Exists_append_r %2 @Exists_append_l @Exists_append_l
1457                   @Exists_append_r %1 %
1458              | 4: * [ 1: #Eq <Eq %1 %1 whd normalize
1459                       @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r
1460                       @Exists_append_r whd %1 //
1461                     | 2: * ]
1462              ]
1463| % %1 normalize @Exists_append_r %2 @Exists_append_l @Exists_append_l
1464  @Exists_append_r % %
1465| @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1466   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
1467                   @Exists_append_r @Exists_append_l @Exists_append_l                   
1468                   @Exists_append_r %2 @Exists_append_l assumption
1469              | 2: #H %1 %2 assumption
1470              | 3: /2/
1471              ]
1472| whd %1 %1 normalize /2/
1473| whd %1 %1 normalize
1474  @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r
1475  whd %1 //
1476| normalize %2 /3/
1477| normalize /4/
1478| whd %1 %2 whd @(ex_intro … l) @E
1479] qed.
1480
1481axiom ParamGlobalMixup : String.
1482
1483(* params and statement aren't real parameters, they're just there for giving the invariant. *)
1484definition alloc_params :
1485 ∀vars:var_types.∀lbls,statement,uv,flag,rettyp. list (ident×type) → (Σsu:(tmpgen vars)×labgen×stmt. trans_inv vars lbls statement uv flag rettyp su)
1486   → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag rettyp su) ≝   
1487λvars,lbls,statement,uv,ul,rettyp,params,s. foldl ?? (λsu,it.
1488  let 〈id,ty〉 ≝ it in
1489  do «result,Is» ← su;
1490  let 〈fgens1, s〉 as Eresult ≝ result in
1491  do 〈t,ty'〉 as E ← lookup' vars id;
1492  match t return λx.? → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv ul rettyp su) with
1493  [ Local ⇒ λE. OK (Σs:(tmpgen vars)×labgen×stmt.?) «result,Is»
1494  | Stack n ⇒ λE.
1495      OK ? «〈fgens1, St_seq (St_store ? (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?»
1496  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
1497  ] E) (OK ? s) params.
1498whd
1499@(match fgens1 return λx.x=fgens1 → ? with
1500  [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1))
1501whd in Is ⊢ %; destruct whd in Is;
1502try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I
1503elim Is * * * #Hincl #Hstmt_inv #Hlab_tr #Hret #Htmp_pr try assumption
1504@(expr_vars_mp … (tmp_preserved … uv1)) whd >E @refl
1505qed.
1506
1507axiom DuplicateLabel : String.
1508
1509definition lenv_list_inv : lenv → lenv → list ident → Prop ≝
1510λlbls0,lbls,ls.
1511 ∀l,l'. lookup_label lbls l = OK ? l' →
1512 Exists ? (λl'. l' = l) ls ∨ lookup_label lbls0 l = OK ? l'.
1513
1514lemma lookup_label_add : ∀lbls,l,l'.
1515  lookup_label (add … lbls l l') l = OK ? l'.
1516#lbls #l #l' whd in ⊢ (??%?); >lookup_add_hit @refl
1517qed.
1518
1519lemma lookup_label_miss : ∀lbls,l,l',l0.
1520  l0 ≠ l →
1521  lookup_label (add … lbls l l') l0 = lookup_label lbls l0.
1522#lbls #l #l' #l0 #NE
1523whd in ⊢ (??%%);
1524>lookup_add_miss
1525[ @refl | @NE ]
1526qed.
1527
1528let rec populate_lenv (ls:list ident) (ul:labgen) (lbls:lenv): res ((Σlbls':lenv. lenv_list_inv lbls lbls' ls) × labgen) ≝
1529match ls return λls.res ((Σlbls':lenv. lenv_list_inv lbls lbls' ls) × labgen) with
1530[ nil ⇒ OK ? 〈«lbls, ?», ul〉
1531| cons l t ⇒
1532  match lookup_label lbls l return λlook. lookup_label lbls l = look → ? with
1533  [ OK _    ⇒ λ_.Error ? (msg DuplicateLabel)
1534  | Error _ ⇒ λLOOK.
1535    match generate_fresh_label … ul with
1536    [ mk_Sig ret H ⇒
1537       do 〈packed_lbls, ul1〉 ← populate_lenv t (snd ?? ret) (add … lbls l (fst ?? ret));
1538       match packed_lbls with
1539       [ mk_Sig lbls' Hinv ⇒ OK ? 〈«lbls', ?», ul1〉 ]
1540    ]
1541  ] (refl ? (lookup_label lbls l))
1542].
1543[ 1: whd #l #l' #Hlookup %2 assumption
1544| 2: whd in Hinv; whd #cl_lab #cm_lab #Hlookup
1545     @(eq_identifier_elim … l cl_lab)
1546     [ 1: #Heq %1 >Heq whd %1 //
1547     | 2: #Hneq cases (Hinv cl_lab cm_lab Hlookup)
1548           [ 1: #H %1 %2 @H
1549           | 2: #LOOK' %2 >lookup_label_miss in LOOK'; /2/ #H @H ]
1550     ]
1551]
1552qed.
1553
1554definition build_label_env :
1555   ∀body:statement. res ((Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) × labgen) ≝
1556λbody.
1557  let initial_labgen ≝ mk_labgen (new_universe ?) (nil ?) ?  in
1558  do 〈label_map, u〉 ← populate_lenv (labels_defined body) initial_labgen (empty_map ??);
1559  let lbls ≝ pi1 ?? label_map in
1560  let H    ≝ pi2 ?? label_map in
1561  OK ? 〈«lbls, ?», u〉.
1562[ 1: #l #l' #E cases (H l l' E) //
1563     whd in ⊢ (??%? → ?); #H destruct
1564| 2: whd @I ]
1565qed.
1566
1567lemma local_id_split : ∀vars,tmpgen,i,t.
1568  local_id (add_tmps vars (tmp_env vars tmpgen)) i t →
1569  local_id vars i t ∨ Exists ? (λx. \fst x = i ∧ typ_of_type (\snd x) = t) (tmp_env … tmpgen).
1570#vars #tmpgen #i #t
1571whd in ⊢ (?%?? → ?);
1572elim (tmp_env vars tmpgen)
1573[ #H %1 @H
1574| * #id #ty #tl #IH
1575  cases (identifier_eq ? i id)
1576  [ #E >E #H %2 whd %1 % [ @refl | whd in H; whd in H:(match % with [_⇒?|_⇒?]); >lookup_add_hit in H; #E1 >E1 @refl ]
1577  | #NE #H cases (IH ?)
1578    [ #H' %1 @H'
1579    | #H' %2 %2 @H'
1580    | whd in H; whd in H:(match % with [ _ ⇒ ? | _ ⇒ ? ]);
1581      >lookup_add_miss in H; [ #H @H | @NE ]
1582    ]
1583  ]
1584] qed.
1585
1586lemma Exists_squeeze : ∀A,P,l1,l2,l3.
1587  Exists A P (l1@l3) → Exists A P (l1@l2@l3).
1588#A #P #l1 #l2 #l3 #EX
1589cases (Exists_append … EX)
1590[ #EX1 @Exists_append_l @EX1
1591| #EX3 @Exists_append_r @Exists_append_r @EX3
1592] qed.
1593
1594(* This lemma allows to merge two stmt_P in one. Used in the following parts to merge an invariant on variables
1595   and an invariant on labels. *)
1596lemma stmt_P_conj : ∀ (P1:stmt → Prop). ∀ (P2:stmt → Prop). ∀ s. stmt_P P1 s → stmt_P P2 s → stmt_P (λs.P1 s ∧ P2 s) s.
1597#P1 #P2 #s elim s
1598normalize /6 by proj1, proj2, conj/
1599qed.
1600
1601definition translate_function :
1602  ∀tmpuniverse:universe SymbolTag.
1603  ∀globals:list (ident×region×type).
1604  ∀f:function.
1605    globals_fresh_for_univ ? globals tmpuniverse →
1606    fn_fresh_for_univ f tmpuniverse →
1607  res internal_function ≝
1608λtmpuniverse, globals, f, Fglobals, Ffn.
1609  do 〈env_pack, ul〉 ← build_label_env (fn_body f);
1610    match env_pack with
1611    [ mk_Sig lbls Ilbls ⇒
1612      let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in
1613      let uv ≝ mk_tmpgen vartypes tmpuniverse [ ] ?? in
1614      do s0 ← translate_statement vartypes uv ul lbls DoNotConvert (opttyp_of_type (fn_return f)) (fn_body f);
1615      do «fgens, s1, Is» ← alloc_params vartypes lbls ? uv DoNotConvert (opttyp_of_type (fn_return f)) (fn_params f) s0;
1616      let params ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f) in
1617      let vars ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? (fst ?? fgens) @ fn_vars f) in
1618      do D ← check_distinct_env ?? (params @ vars);
1619      OK ? (mk_internal_function
1620        (opttyp_of_type (fn_return f))
1621        params
1622        vars
1623        D
1624        stacksize
1625        s1 ?)
1626  ].
1627[ 1: #i #t #Hloc whd @Hloc
1628| 2: whd #id #Hpresent normalize in Hpresent:(???%?); whd in Hpresent;
1629      @(characterise_vars_fresh … (sym_eq … E)) //
1630| 3: @(match fgens return λx.x=fgens → ? with
1631     [ mk_Prod uv' ul' ⇒ λHfgens.? ] (refl ? fgens))
1632     whd in Is; <Hfgens in Is; #Is whd in Is ⊢ %;
1633     elim Is * * * #Hstmt_inv #Hlab_trans #Htmps_pres #Hreturn #Hlabel_wf
1634     (* merge Hlabel_wf with Hstmt_inv and eliminate right away *)
1635     @(stmt_P_mp … (stmt_P_conj … (stmt_P_conj … Hstmt_inv Hlabel_wf) Hreturn))
1636     #s * * #Hstmt_vars #Hstmt_labels #Hstmt_return %
1637     [ 1: (* prove that variables are either parameters or locals *)
1638        @(stmt_vars_mp … Hstmt_vars) #i #t #H
1639        (* Case analysis: (i, t) is either in vartypes, or in (tmp_env vartypes uv) *)
1640        cases (local_id_split … H)
1641        [ 1: #H' >map_append
1642          @Exists_map [ 1: #x @(And (\fst x = i) (typ_of_type (\snd x) = t))  (* * #id #ty @(〈id, typ_of_type ty〉=〈i, t〉)*)
1643                      | 2: whd @Exists_squeeze @(characterise_vars_all globals f ?? (sym_eq ??? E) i t H')
1644                      | 3: * #id #ty * #E1 #E2 <E1 <E2 @refl
1645                      ]
1646        | 2: #EX @Exists_append_r whd in ⊢ (???%); <map_append @Exists_append_l
1647          @Exists_map [ 1: #x @(And (\fst x = i) (typ_of_type (\snd x) = t))
1648                      | 2: <Hfgens @EX
1649                      | 3: * #id #ty * #E1 #E2 <E1 <E2 % @refl
1650                      ]
1651        ]
1652     | 2: (* prove that labels are properly declared. *)
1653          @(stmt_labels_mp … Hstmt_labels) #l * *
1654          [ 1: #H assumption
1655          | 2: * #cl_label #Hlookup lapply (Ilbls cl_label l Hlookup) #Hdefined
1656                cases (Hlab_trans … Hdefined) #lx * #LOOKUPx >LOOKUPx in Hlookup; #Ex destruct (Ex)
1657                #H @H
1658          ]
1659     | cases s in Hstmt_return; // * normalize [2: * #t #e ]
1660       cases (fn_return f) normalize #A try #B try #C try #D try #E destruct //
1661    ]
1662] qed.   
1663
1664definition translate_fundef :
1665  ∀tmpuniverse:universe SymbolTag.
1666  ∀globals:list (ident×region×type).
1667    globals_fresh_for_univ ? globals tmpuniverse →
1668  ∀f:clight_fundef.
1669    fd_fresh_for_univ f tmpuniverse →
1670  res (fundef internal_function) ≝
1671λtmpuniverse,globals,Fglobals,f.
1672match f return λf. fd_fresh_for_univ f ? → ? with
1673[ CL_Internal fn ⇒ λFf. do fn' ← translate_function tmpuniverse globals fn Fglobals Ff; OK ? (Internal ? fn')
1674| CL_External fn argtys retty ⇒ λ_. OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
1675].
1676
1677let rec map_partial_All (A,B:Type[0]) (P:A → Prop) (f:∀a:A. P a → res B)
1678  (l:list A) (H:All A P l) on l : res (list B) ≝
1679match l return λl. All A P l → ? with
1680[ nil ⇒ λ_. OK (list B) (nil B)
1681| cons hd tl ⇒ λH.
1682    do b_hd ← f hd (proj1 … H);
1683    do b_tl ← map_partial_All A B P f tl (proj2 … H);
1684      OK (list B) (cons B b_hd b_tl)
1685] H.
1686
1687definition clight_to_cminor : clight_program → res Cminor_program ≝
1688λp.
1689  let tmpuniverse ≝ universe_for_program p in
1690  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
1691  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
1692  let globals ≝ fun_globals @ var_globals in
1693  do fns ← map_partial_All ??? (λx,H. do f ← translate_fundef tmpuniverse globals ? (\snd x) H; OK ? 〈\fst x, f〉) (prog_funct ?? p) ?;
1694    OK ? (mk_program ??
1695      (map ?? (λv. 〈\fst v, \fst (\snd v)〉) (prog_vars ?? p))
1696      fns
1697      (prog_main ?? p)).
1698cases (prog_fresh p) * #H1 #H2 #H3
1699[ @(All_mp … H1) #x * //
1700| @All_append
1701  [ elim (prog_funct ?? p) in H1 ⊢ %; // * #id #fd #tl #IH * * #Hhd1 #Hhd2 #Htl % // @IH @Htl
1702  | whd in H3; elim (prog_vars ?? p) in H3 ⊢ %; // #hd #tl #IH * #Hhd #Htl % /2/
1703  ]
1704] qed.
1705
1706(* It'd be nice to go back to some generic thing like
1707
1708 transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)).
1709
1710   rather than the messier definition above.
1711*)
Note: See TracBrowser for help on using the repository browser.