source: src/Clight/toCminor.ma

Last change on this file was 3054, checked in by campbell, 7 years ago

Put missing typ check in; adjust proof because I did it a little
differently to Ilias.

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