source: src/Clight/toCminor.ma @ 1872

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

Make binary operations in Cminor/RTLabs properly typed.
A few extra bits and pieces that help:
Separate out Clight operation classification to its own file.
Use dependently typed classification to refine the types.
Fix bug in cast simplification.
Remove memory_chunk in favour of the low-level typ, as this now contains
exactly the right amount of information (unlike in CompCert?).
Make Cminor/RTLabs comparisons produce an 8-bit result (and cast if
necessary).

File size: 73.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
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 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 ∨ mem_set ? mem_vars id 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 ∨ mem_set ?? 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 ∨ mem_set ?? 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* [ #sz1 #sg1 | #r1 | #sz1 ]
271* [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
272[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
273  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
274| *; #P #p @(region_should_eq r1 ?? p)
275| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
276] qed.
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 r ⇒
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 : ∀r,ty,n. expr (typ_of_type (ptr_type r ty n)) → expr (ASTptr r) ≝
326λr,ty,n,e. e⌈expr (typ_of_type (ptr_type r ty n)) ↦ expr (ASTptr r)⌉.
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| add_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddf sz) e1 e2)
337(* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *)
338| add_case_pi n r ty sz sg ⇒
339    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16 r) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
340| add_case_ip n sz sg r ty ⇒
341    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16 r) (fix_ptr_type … e2) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
342| add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch)
343].
344
345
346definition translate_sub ≝
347λty1,ty2,ty'.
348let ty1' ≝ typ_of_type ty1 in
349let ty2' ≝ typ_of_type ty2 in
350match classify_sub ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
351[ sub_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osub ??) e1 e2)
352| sub_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osubf sz) e1 e2)
353(* XXX could optimise cast as above *)
354| sub_case_pi n r ty sz sg ⇒
355    λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I16 r) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
356(* XXX check in detail? *)
357| sub_case_pp n1 n2 r1 ty1 r2 ty2 ⇒
358    λe1,e2. match ty' return λty'. res (CMexpr (typ_of_type ty')) with
359    [ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I16 Signed sz sg) (Op2 ??? (Odiv I16) (Op2 ??? (Osubpp I16 r1 r2) (fix_ptr_type … e1) (fix_ptr_type ??? e2)) (Cst ? (Ointconst I16 (repr ? (sizeof ty2))))))
360    | _ ⇒ Error ? (msg TypeMismatch)
361    ]
362| sub_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
363].
364
365definition translate_mul ≝
366λty1,ty2,ty'.
367let ty1' ≝ typ_of_type ty1 in
368let ty2' ≝ typ_of_type ty2 in
369match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
370[ aop_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omul …) e1 e2)
371| aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omulf …) e1 e2)
372| aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
373].
374
375definition translate_div ≝
376λty1,ty2,ty'.
377let ty1' ≝ typ_of_type ty1 in
378let ty2' ≝ typ_of_type ty2 in
379match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
380[ aop_case_ii sz sg ⇒
381    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
382    [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivu …) e1 e2)
383    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odiv …) e1 e2)
384    ]
385| aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivf …) e1 e2)
386| aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
387].
388
389definition translate_mod ≝
390λty1,ty2,ty'.
391let ty1' ≝ typ_of_type ty1 in
392let ty2' ≝ typ_of_type ty2 in
393match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
394[ aop_case_ii sz sg ⇒
395    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
396    [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omodu …) e1 e2)
397    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omod …) e1 e2)
398    ]
399(* no float case *)
400| _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
401].
402
403definition translate_shr ≝
404λty1,ty2,ty'.
405let ty1' ≝ typ_of_type ty1 in
406let ty2' ≝ typ_of_type ty2 in
407match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
408[ aop_case_ii sz sg ⇒
409    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
410    [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omodu …) e1 e2)
411    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omod …) e1 e2)
412    ]
413(* no float case *)
414| _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
415].
416
417definition complete_cmp : ∀ty'. CMexpr (ASTint I8 Unsigned) → res (CMexpr (typ_of_type ty')) ≝
418λty',e.
419match ty' return λty'. res (CMexpr (typ_of_type ty')) with
420[ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I8 Unsigned sz sg) e)
421| _ ⇒ Error ? (msg TypeMismatch)
422].
423
424definition translate_cmp ≝
425λc,ty1,ty2,ty'.
426let ty1' ≝ typ_of_type ty1 in
427let ty2' ≝ typ_of_type ty2 in
428match classify_cmp ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
429[ cmp_case_ii sz sg ⇒
430    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
431    [ Unsigned ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpu … c) e1 e2)
432    | Signed ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmp … c) e1 e2)
433    ]
434| cmp_case_pp n r ty ⇒
435    λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpp … c) (fix_ptr_type … e1) (fix_ptr_type … e2))
436| cmp_case_ff sz ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpf … c) e1 e2)
437| cmp_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
438].
439
440definition translate_misc_aop ≝
441λty1,ty2,ty',op.
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 ⇒ λe1,e2. typ_should_eq ??? (Op2 ?? (ASTint sz sg) (op sz sg) e1 e2)
446| _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
447].
448
449definition translate_binop : binary_operation → type → CMexpr ? → type → CMexpr ? → type → res (CMexpr ?) ≝
450λop,ty1,e1,ty2,e2,ty.
451let ty' ≝ typ_of_type ty in
452match op with
453[ Oadd ⇒ translate_add ty1 ty2 ty e1 e2
454| Osub ⇒ translate_sub ty1 ty2 ty e1 e2
455| Omul ⇒ translate_mul ty1 ty2 ty e1 e2
456| Omod ⇒ translate_mod ty1 ty2 ty e1 e2
457| Odiv ⇒ translate_div ty1 ty2 ty e1 e2
458| Oand ⇒ translate_misc_aop ty1 ty2 ty Oand e1 e2
459| Oor  ⇒ translate_misc_aop ty1 ty2 ty Oor e1 e2
460| Oxor ⇒ translate_misc_aop ty1 ty2 ty Oxor e1 e2
461| Oshl ⇒ translate_misc_aop ty1 ty2 ty Oshl e1 e2
462| Oshr ⇒ translate_shr ty1 ty2 ty e1 e2
463| Oeq ⇒ translate_cmp Ceq ty1 ty2 ty e1 e2
464| One ⇒ translate_cmp Cne ty1 ty2 ty e1 e2
465| Olt ⇒ translate_cmp Clt ty1 ty2 ty e1 e2
466| Ogt ⇒ translate_cmp Cgt ty1 ty2 ty e1 e2
467| Ole ⇒ translate_cmp Cle ty1 ty2 ty e1 e2
468| Oge ⇒ translate_cmp Cge ty1 ty2 ty e1 e2
469].
470
471lemma typ_equals : ∀t1,t2. ∀P:∀t. expr t → Prop. ∀v1,v2.
472  typ_should_eq t1 t2 expr v1 = OK ? v2 →
473  P t1 v1 →
474  P t2 v2.
475* [ * * | * | * ]
476* try * try *
477#P #v1 #v2 #E whd in E:(??%?); destruct
478#H @H
479qed.
480
481lemma unfix_ptr_type : ∀r,ty,n,e.∀P:∀t. expr t → Prop.
482  P (typ_of_type (ptr_type r ty n)) e →
483  P (ASTptr r) (fix_ptr_type r ty n e).
484#r #ty * [ 2: #n ] #e #P #H @H
485qed.
486
487(* Recall that [expr_vars], defined in Cminor/Syntax.ma, asserts a predicate on
488  all the variables of a program. [translate_binop_vars], given
489  a predicate verified for all variables of subexprs e1 and e2, produces
490  a proof that all variables of [translate_binop op _ e1 _ e2 _] satisfy this
491  predicate. *)
492
493lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e.
494  expr_vars ? e1 P →
495  expr_vars ? e2 P →
496  translate_binop op ty1 e1 ty2 e2 ty = OK ? e →
497  expr_vars ? e P.
498#P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
499whd in ⊢ (??%? → ?);
500[ inversion (classify_add ty1 ty2) in ⊢ ?;
501  [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4 -E3 change with (typ_should_eq ???? = OK ??) in E4;
502    @(typ_equals … E4) % //
503  | #sz #E1 #E2 #E3 destruct >E3 #E4
504    @(typ_equals … E4) % //
505  | #n #r #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
506    @(typ_equals … E4) -E4 -E3 % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)| % // ]
507  | #n #sz #sg #r #ty0 #E1 #E2 #E3 destruct >E3 #E4
508    @(typ_equals … E4) % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2)| % // ]
509  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
510  ]
511| inversion (classify_sub ty1 ty2) in ⊢ ?;
512  [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4
513    @(typ_equals … E4) % //
514  | #sz #E1 #E2 #E3 destruct >E3 #E4
515    @(typ_equals … E4) % //
516  | #n #r #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
517    @(typ_equals … E4) % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)| % // ]
518  | #n1 #n2 #r1 #ty1' #r2 #ty2' #E1 #E2 #E3 destruct >E3
519    whd in ⊢ (??%? → ?); cases ty in e ⊢ %;
520    [ 2: #sz #sg #e #E4 | 4: #r #ty #e #E4 | 5: #r #ty' #n' #e #E4
521    | *: normalize #X1 #X2 try #X3 try #X4 destruct
522    ] whd in E4:(??%?); destruct % // %
523    [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1) | @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2) ]
524  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
525  ]
526| 3,4,5,6,7,8,9,10: inversion (classify_aop ty1 ty2) in ⊢ ?;
527  (* Note that some cases require a split on signedness of integer type. *)
528  [ 1,4,7,10,13,16,19,22: #sz * #E1 #E2 #E3 destruct >E3 #E4
529    @(typ_equals … E4) % //
530  | 2,5: #sz #E1 #E2 #E3 destruct >E3 #E4
531    @(typ_equals … E4) % //
532  | 8,11,14,17,20,23: #sz #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
533  | 3,6,9,12,15,18,21,24: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
534  ]
535| 11,12,13,14,15,16: inversion (classify_cmp ty1 ty2) in ⊢ ?;
536  [ 1,5,9,13,17,21: #sz * #E1 #E2 #E3 destruct >E3
537  | 2,6,10,14,18,22: #n #r #ty' #E1 #E2 #E3 destruct >E3
538  | 3,7,11,15,19,23: #sz #E1 #E2 #E3 destruct >E3
539  | *: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); @⊥ destruct
540  ] whd in ⊢ (??%? → ?); cases ty in e ⊢ %;
541  try (normalize #X1 #X2 try #X3 try #X4 try #X5 destruct #FAIL)
542  #sz #sg #e #E4
543  whd in E4:(??%?); destruct %
544  [ 25,27,29,31,33,35: @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)
545  | 26,28,30,32,34,36: @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2)
546  | *: //
547  ]
548] qed.
549
550
551(* We'll need to implement proper translation of pointers if we really do memory
552   spaces. *)
553(* This function performs leibniz-style subst if r1 = r2, and fails otherwise. *)
554definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝
555λr1,r2,P.
556  match r1 return λx.P x → res (P r2) with
557  [ Any ⇒   match r2 return λx.P Any → res (P x) with [ Any ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
558  | Data ⇒  match r2 return λx.P Data → res (P x) with [ Data ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
559  | IData ⇒ match r2 return λx.P IData → res (P x) with [ IData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
560  | PData ⇒ match r2 return λx.P PData → res (P x) with [ PData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
561  | XData ⇒ match r2 return λx.P XData → res (P x) with [ XData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
562  | Code ⇒  match r2 return λx.P Code → res (P x) with [ Code ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
563  ].
564
565(* Simple application of [check_region] to translate between terms. *)
566definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝
567λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
568
569axiom FIXME : String.
570
571(* Given a source and target type, translate an expession of type source to type target *)
572definition 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) ≝
573λP,ty1,ty2.
574match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with
575[ Tint sz1 sg1 ⇒ λe.
576    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
577    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint ? sg1 sz2 ?) e)
578    | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu ?? | _ ⇒ Ofloatofint ??]) e)
579    | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e)
580    | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e)
581    | _ ⇒ Error ? (msg TypeMismatch)
582    ]
583| Tfloat sz1 ⇒ λe.
584    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
585    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat ? sz2 | _ ⇒ Ointoffloat ? sz2 ]) e, ?»
586    | Tfloat sz2 ⇒ Error ? (msg FIXME) (* OK ? «Op1 ?? (Oid ?) e, ?» (* FIXME *) *)
587    | _ ⇒ Error ? (msg TypeMismatch)
588    ]
589| Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
590    match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with
591    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2 ??) e, ?»
592    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
593    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
594    | _ ⇒ Error ? (msg TypeMismatch)
595    ]
596| Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
597    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
598    [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2 ??) e, ?»
599    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
600    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
601    | _ ⇒ Error ? (msg TypeMismatch)
602    ]
603| _ ⇒ λ_. Error ? (msg TypeMismatch)
604]. whd normalize nodelta @pi2
605qed.
606
607(* Translate Clight exprs into Cminor ones.
608  Arguments :
609  - vars:var_types, an environment mapping each variable to a couple (allocation mode, type)
610  - e:expr, the expression to be converted
611  Result : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars))
612  that is, either
613  . an error
614  . an expression e', matching the type of e, such that e' respect the property that all variables
615    in it are not global. In effect, [translate_expr] will replace global variables by constant symbols.
616*)
617let rec translate_expr (vars:var_types) (e:expr) on e : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) ≝
618match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with
619[ Expr ed ty ⇒
620  match ed with
621  [ Econst_int sz i ⇒ OK ? «Cst ? (Ointconst sz i), ?»
622  | Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?»
623  | Evar id ⇒
624      do 〈c,t〉 as E ← lookup' vars id; (* E is an equality proof of the shape "lookup' vars id = Ok <c,t>" *)
625      match c return λx.? = ? → res (Σe':CMexpr ?. ?) with
626      [ Global r ⇒ λ_.
627          (* We are accessing a global variable in an expression. Its Cminor counterpart also depends on
628             its access mode:
629             - By_value q, where q is a memory chunk specification (whitch should match the type of the global)
630             - By_reference, and we only take the adress of the variable
631             - By_nothing : error
632           *)
633          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
634          [ By_value t ⇒ OK ? «Mem t r (Cst ? (Oaddrsymbol id 0)), ?» (* Mem is "load" in compcert *)
635          | By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
636          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
637          ]
638      | Stack n ⇒ λE.
639          (* We have decided that the variable should be allocated on the stack,
640           * because its adress was taken somewhere or becauste it's a structured data. *)
641          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
642          [ By_value t ⇒ OK ? «Mem t Any (Cst ? (Oaddrstack n)), ?»
643          | By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?»
644          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
645          ]
646          (* 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. *)
647      | Local ⇒ λE. 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, ?»)
648      ] E
649  | Ederef e1 ⇒
650      do e1' ← translate_expr vars e1;
651      (* According to the way the data pointed to by e1 is accessed, the generated Cminor code will vary.
652        - if e1 is a kind of int* ptr, then we load ("Mem") the ptr returned by e1
653        - if e1 is a struct* or a function ptr, then we acess by reference, in which case we :
654           1) check the consistency of the regions in the type of e1 and in the access mode of its type
655           2) return directly the converted CMinor expression "as is" (TODO : what is the strange notation with the ceil function and the mapsto ?)
656      *)
657      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
658      [ ASTptr r ⇒ λe1'.
659          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
660          [ By_value t ⇒ OK ? «Mem t ? (pi1 … e1'), ?»
661          | By_reference r' ⇒ region_should_eq r r' ? e1'
662          | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
663          ]
664      | _ ⇒ λ_. Error ? (msg TypeMismatch)
665      ] e1'
666  | Eaddrof e1 ⇒
667      do e1' ← translate_addr vars e1;
668      match typ_of_type ty return λx.res (Σz:CMexpr x.?) with
669      [ ASTptr r ⇒
670          match e1' with
671          [ mk_DPair r1 e1' ⇒ region_should_eq r1 r ? e1'
672          ]
673      | _ ⇒ Error ? (msg TypeMismatch)
674      ]
675  | Eunop op e1 ⇒
676      do op' ← translate_unop (typ_of_type (typeof e1)) (typ_of_type ty) op;
677      do e1' ← translate_expr vars e1;
678      OK ? «Op1 ?? op' e1', ?»
679  | Ebinop op e1 e2 ⇒
680      do e1' ← translate_expr vars e1;
681      do e2' ← translate_expr vars e2;
682      do e' as E ← translate_binop op (typeof e1) e1' (typeof e2) e2' ty;
683      OK ? «e', ?»
684  | Ecast ty1 e1 ⇒
685      do e1' ← translate_expr vars e1;
686      do e' ← translate_cast ? (typeof e1) ty1 e1';
687      do e' ← typ_should_eq (typ_of_type ty1) (typ_of_type ty) ? e';
688      OK ? e'
689  | Econdition e1 e2 e3 ⇒
690      do e1' ← translate_expr vars e1;
691      do e2' ← translate_expr vars e2;
692      do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
693      do e3' ← translate_expr vars e3;
694      do e3' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e3';
695      match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → ? with
696      [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' e3', ?»
697      | _ ⇒ λ_.Error ? (msg TypeMismatch)
698      ] e1'
699  | Eandbool e1 e2 ⇒
700      do e1' ← translate_expr vars e1;
701      do e2' ← translate_expr vars e2;
702      match ty with
703      [ Tint sz _ ⇒
704        do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
705        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with
706        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))), ?»
707        | _ ⇒ λ_.Error ? (msg TypeMismatch)
708        ] e1'
709      | _ ⇒ Error ? (msg TypeMismatch)
710      ]
711  | Eorbool e1 e2 ⇒
712      do e1' ← translate_expr vars e1;
713      do e2' ← translate_expr vars e2;
714      match ty with
715      [ Tint sz _ ⇒
716        do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
717        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with
718        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2', ?»
719        | _ ⇒ λ_.Error ? (msg TypeMismatch)
720        ] e1'
721      | _ ⇒ Error ? (msg TypeMismatch)
722      ]
723  | Esizeof ty1 ⇒
724      match ty with
725      [ Tint sz _ ⇒ OK ? «Cst ? (Ointconst sz (repr ? (sizeof ty1))), ?»
726      | _ ⇒ Error ? (msg TypeMismatch)
727      ]
728  | Efield e1 id ⇒
729      match typeof e1 with
730      [ Tstruct _ fl ⇒
731          do e1' ← translate_addr vars e1;
732          match e1' with
733          [ mk_DPair r e1' ⇒
734            do off ← field_offset id fl;
735            match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
736            [ By_value t ⇒
737                OK ? «Mem t r (Op2 ? (ASTint I16 Signed (* XXX efficiency? *)) ?
738                                   (Oaddp …) e1' (Cst ? (Ointconst I16 (repr ? off)))),?»
739            | By_reference r' ⇒
740                do e1' ← region_should_eq r r' ? e1';
741                OK ? «Op2 (ASTptr r') (ASTint I16 Signed (* XXX efficiency? *)) (ASTptr r')
742                        (Oaddp …) e1' (Cst ? (Ointconst I16 (repr ? off))),?»
743            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
744            ]
745          ]
746      | Tunion _ _ ⇒
747          do e1' ← translate_addr vars e1;
748          match e1' with
749          [ mk_DPair r e1' ⇒
750            match access_mode ty return λt.λ_. res (Σz:CMexpr t.?) with
751            [ By_value t ⇒ OK ? «Mem t ? e1', ?»
752            | By_reference r' ⇒ region_should_eq r r' ? e1'
753            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
754            ]
755          ]
756      | _ ⇒ Error ? (msg BadlyTypedAccess)
757      ]
758  | Ecost l e1 ⇒
759      do e1' ← translate_expr vars e1;
760      do e' ← OK ? «Ecost ? l e1',?»;
761      typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e'
762  ]
763]
764
765(* Translate addr takes an expression e1, and returns a Cminor code computing the address of the result of [e1].   *)
766and translate_addr (vars:var_types) (e:expr) on e : res (𝚺r. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝
767match e with
768[ Expr ed _ ⇒
769  match ed with
770  [ Evar id ⇒
771      do 〈c,t〉 ← lookup' vars id;
772      match c return λ_. res (𝚺r.Σz:CMexpr (ASTptr r).?) with
773      [ Global r ⇒ OK ? ❬r, «Cst ? (Oaddrsymbol id 0), ?»❭
774      | Stack n ⇒ OK ? ❬Any, «Cst ? (Oaddrstack n), ?»❭
775      | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *)
776      ]
777  | Ederef e1 ⇒
778      do e1' ← translate_expr vars e1;
779      match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (𝚺r. Σz:CMexpr (ASTptr r). ?) with
780      [ ASTptr r ⇒ λe1'.OK ? ❬r, e1'❭
781      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
782      ] e1'
783  | Efield e1 id ⇒
784      match typeof e1 with
785      [ Tstruct _ fl ⇒
786          do e1' ← translate_addr vars e1;
787          do off ← field_offset id fl;
788          match e1' with
789          [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?)
790             (❬r, «Op2 (ASTptr r) (ASTint I16 Signed (* FIXME inefficient?*)) (ASTptr r)
791                     (Oaddp I16 r) e1'' (Cst ? (Ointconst I16 (repr ? off))), ?» ❭)
792          ]
793      | Tunion _ _ ⇒ translate_addr vars e1
794      | _ ⇒ Error ? (msg BadlyTypedAccess)
795      ]
796  | _ ⇒ Error ? (msg BadLvalue)
797  ]
798].
799whd try @I
800[ >E whd @refl
801| 2,3: @pi2
802| @(translate_binop_vars … E) @pi2
803| % [ % ] @pi2
804| % [ % @pi2 ] whd @I
805| % [ % [ @pi2 | @I ] | @pi2 ]
806| % [ @pi2 | @I ]
807| % [ @pi2 | @I ]
808| @pi2
809| @pi2
810| % [ @pi2 | @I ]
811] qed.
812
813(* We provide a function to work out how to do an assignment to an lvalue
814   expression.  It is used for both Clight assignments and Clight function call
815   destinations, but doesn't take the value to be assigned so that we can use
816   it to form a single St_store when possible (and avoid introducing an
817   unnecessary temporary variable and assignment).
818   *)
819inductive destination (vars:var_types) : Type[0] ≝
820| IdDest : ∀id,ty. local_id vars id (typ_of_type ty) → destination vars
821| MemDest : ∀r:region. (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.
822
823(* Let a source Clight expression be assign(e1, e2). First of all, observe that [e1] is a
824  /Clight/ expression, not converted by translate_expr. We thus have to do part of the work
825  of [translate_expr] in this function. [translate_dest] will convert e1
826   into a proper destination for an assignement operation. We proceed by case analysis on e1.
827   - if e1 is a variable [id], then we proceed by case analysis on its allocation mode:
828      - if [id] is allocated locally (in a register), then id becomes directly
829        the target for the assignement, as (IdDest vars id t H), where t is the type
830        of id, and H asserts that id is indeed a local variable.
831      - if [id] is a global variable stored in region [r], then we perform [translate_expr]'s
832        job and return an adress, given as a constant symbol corresponding to [id], with
833        region r and memory chunk specified by the access mode of the rhs type ty2 of [e2].
834      - same thing for stack-allocated variables, except that we don't specify any region.
835   - if e1 is not a variable, we use [translate_addr] to generate a Cminor expression computing
836    the adres of e1
837*)
838definition translate_dest ≝
839λvars,e1.
840  match e1 with
841  [ Expr ed1 ty1 ⇒
842      match ed1 with
843      [ Evar id ⇒
844          do 〈c,t〉 as E ← lookup' vars id;
845          match c return λx.? → ? with
846          [ Local ⇒ λE. OK ? (IdDest vars id t ?)
847          | Global r ⇒ λE. OK ? (MemDest ? r (Cst ? (Oaddrsymbol id 0)))
848          | Stack n ⇒ λE. OK ? (MemDest ? Any (Cst ? (Oaddrstack n)))
849          ] E
850      | _ ⇒
851          do e1' ← translate_addr vars e1;
852          match e1' with [ mk_DPair r e1' ⇒ OK ? (MemDest ? r e1') ]
853      ]
854  ].
855whd // >E @refl
856qed.
857
858(* [lenv] is the type of maps from Clight labels to Cminor labels. *)
859definition lenv ≝ identifier_map SymbolTag (identifier Label).
860
861axiom MissingLabel : String.
862
863(* Find the Cminor label corresponding to [l] or fail. *)
864definition lookup_label ≝
865λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).
866
867(* True iff the Cminor label [l] is in the codomain of [lbls] *)
868definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup_label lbls l' = OK ? l.
869
870(* True iff The Clight label [l] is in the domain of [lbls] *)
871definition label_in_domain ≝ λlbls:lenv. λl. present ?? lbls l.
872
873let rec fresh_list_for_univ (l:list (identifier Label)) (u:universe Label) ≝
874match l with
875[ nil ⇒ True
876| cons elt tl ⇒ fresh_for_univ ? elt u ∧ fresh_list_for_univ tl u].
877
878record labgen : Type[0] ≝ {
879  labuniverse   : universe Label;
880  label_genlist    : list (identifier Label);
881  genlist_is_fresh : fresh_list_for_univ label_genlist labuniverse
882}.
883
884lemma 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'.
885#l elim l
886[ 1: normalize //
887| 2: #hd #tl #Hind #tmp #u #u' #HA #HB
888  whd
889  @conj
890  [ 1: whd in HA ⊢ ?;
891    elim HA #HAleft #HAright
892    @(fresh_remains_fresh ? hd tmp u u') assumption
893  | 2: whd in HA ⊢ ?;
894    elim HA #HAleft #HAright   
895    @Hind //
896  ]
897]
898qed.
899
900definition In ≝ λelttype.λelt.λl.Exists elttype (λx.x=elt) l.   
901
902definition generate_fresh_label :
903 ∀ul. Σlul:(identifier Label × labgen).
904               (And (∀lab. In ? lab (label_genlist ul) → In ? lab (label_genlist (snd … lul)))
905                   (In ? (fst … lul) (label_genlist (snd … lul)))) ≝
906λul.
907let 〈tmp,u〉 as E ≝ fresh ? (labuniverse ul) in
908 «〈tmp, mk_labgen u (tmp::(label_genlist ul)) ?〉, ?».
909[ 1: normalize @conj
910  [ 1: @(fresh_is_fresh ? tmp u (labuniverse ul) ?) assumption
911  | 2: @fresh_list_stays_fresh // ]
912| @conj /2/
913]
914qed.
915
916let rec labels_defined (s:statement) : list ident ≝
917match s with
918[ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2
919| Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2
920| Swhile _ s ⇒ labels_defined s
921| Sdowhile _ s ⇒ labels_defined s
922| Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
923| Sswitch _ ls ⇒ labels_defined_switch ls
924| Slabel l s ⇒ l::(labels_defined s)
925| Scost _ s ⇒ labels_defined s
926| _ ⇒ [ ]
927]
928and labels_defined_switch (ls:labeled_statements) : list ident ≝
929match ls with
930[ LSdefault s ⇒ labels_defined s
931| LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls
932].
933
934definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s).
935
936(* For each label l in s, there exists a matching label l' = lenv(l) defined in s' *)
937definition labels_translated : lenv → statement → stmt → Prop ≝
938λlbls,s,s'.  ∀l.
939  (Exists ? (λl'.l' = l) (labels_defined s)) →
940  ∃l'. lookup_label lbls l = (OK ? l') ∧ ldefined s' l'.
941
942
943(* Invariant on statements, holds during conversion to Cminor *)
944definition stmt_inv ≝  λvars. stmt_P (stmt_vars (local_id vars)).
945
946(* I (Ilias) decided to inline the following definition, to make explicit the data constructed.
947 * This was needed to prove some stuff in translate_statement at some point, but it might be
948 * useless now. If needed, I can revert this change.  *)
949definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt. stmt_inv vars s) ≝
950λvars,e1,e2.
951do e2' ← translate_expr vars e2;
952do dest ← translate_dest vars e1;
953match dest with
954[ IdDest id ty p ⇒
955    do e2' ← type_should_eq (typeof e2) ty ? e2';
956    OK ? «St_assign ? id e2', ?»
957| MemDest r e1' ⇒ OK ? «St_store ? r e1' e2', ?»
958].
959% try (//)  try (elim e2' //) elim e1' //
960qed.
961
962definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝
963λA,B,f,oa.
964match oa with
965[ None ⇒ OK ? (None ?)
966| Some a ⇒ do b ← f a; OK ? (Some ? b)
967].
968
969definition 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) ]) ≝
970λv,e.
971  do e' ← translate_expr v e;
972  OK (Σe:(𝚺t:typ.CMexpr t).?) «❬?, e'❭, ?».
973whd @pi2
974qed.
975
976(* Add the list of typed variables tmpenv to the environment [var_types] with
977   the allocation mode Local. *)
978definition add_tmps : var_types → list (ident × type) → var_types ≝
979λvs,tmpenv.
980  foldr ?? (λidty,vs. add ?? vs (\fst idty) 〈Local, \snd idty〉) vs tmpenv.
981
982record tmpgen (vars:var_types) : Type[0] ≝ {
983  tmp_universe : universe SymbolTag;
984  tmp_env : list (ident × type);
985  tmp_ok : fresh_map_for_univ … (add_tmps vars tmp_env) tmp_universe;
986  tmp_preserved :
987    ∀id,ty. local_id vars id ty → local_id (add_tmps vars tmp_env) id ty
988}.
989
990definition alloc_tmp : ∀vars. type → tmpgen vars → ident × (tmpgen vars) ≝
991λvars,ty,g.
992  let 〈tmp,u〉 as E ≝ fresh ? (tmp_universe ? g) in
993  〈tmp, mk_tmpgen ? u (〈tmp, ty〉::(tmp_env ? g)) ??〉.
994[ #id #ty'
995  whd in ⊢ (? → ?%??);
996  whd in ⊢ (% → %);
997  whd in ⊢ (? → match % with [_ ⇒ ? | _ ⇒ ?]); #H
998  >lookup_add_miss
999  [ @(tmp_preserved … g) @H
1000  | @(fresh_distinct … E) @(tmp_ok … g)
1001    lapply (tmp_preserved … g id ty' H)
1002    whd in ⊢ (% → %);
1003    whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?);
1004    cases (lookup ??? id)
1005    [ * | #x #_ % #E destruct ]
1006  ]
1007| @fresh_map_add
1008  [ @(fresh_map_preserved … E) @(tmp_ok … g)
1009  | @(fresh_is_fresh … E)
1010  ]
1011] qed.
1012
1013
1014lemma lookup_label_hit : ∀lbls,l,l'.
1015  lookup_label lbls l = OK ? l' →
1016  lpresent lbls l'.
1017#lbls #l #l' #E whd %{l} @E
1018qed.
1019
1020(* TODO: is this really needed now? *)
1021
1022definition tmps_preserved : ∀vars:var_types. tmpgen vars → tmpgen vars → Prop ≝
1023λvars,u1,u2.
1024  ∀id,ty. local_id (add_tmps vars (tmp_env … u1)) id ty → local_id (add_tmps vars (tmp_env … u2)) id ty.
1025
1026lemma alloc_tmp_preserves : ∀vars,tmp,u,u',q.
1027  〈tmp,u'〉 = alloc_tmp ? q u → tmps_preserved vars u u'.
1028#vars #tmp * #u1 #e1 #F1 #P1 * #u2 #e2 #F2 #P2 #q
1029whd in ⊢ (???% → ?); generalize in ⊢ (???(?%) → ?);
1030cases (fresh SymbolTag u1) in ⊢ (??%? → ???(match % with [ _ ⇒ ? ]?) → ?);
1031#tmp' #u' #E1 #E2 whd in E2:(???%); destruct
1032#id #ty #H whd in ⊢ (?%??); whd in H ⊢ %;
1033whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ];
1034>lookup_add_miss // @(fresh_distinct … E1) @F1
1035whd in H:(match % with [_ ⇒ ?|_ ⇒ ?]) ⊢ %;
1036cases (lookup ??? id) in H ⊢ %;
1037[ * | #x #_ % #E destruct ]
1038qed.
1039
1040lemma add_tmps_oblivious : ∀vars,s,u.
1041  stmt_inv vars s → stmt_inv (add_tmps vars (tmp_env vars u)) s.
1042#vars #s #u #H
1043@(stmt_P_mp … H)
1044#s' #H1 @(stmt_vars_mp … H1) #id #t #H @(tmp_preserved ? u ?? H)
1045qed.
1046
1047lemma local_id_fresh_tmp : ∀vars,tmp,u,ty,u0.
1048  〈tmp,u〉 = alloc_tmp vars ty u0 → local_id (add_tmps vars (tmp_env … u)) tmp (typ_of_type ty).
1049#vars #tmp #u #ty #u0
1050whd in ⊢ (???% → ?); generalize in ⊢ (???(?%) → ?);
1051cases (fresh SymbolTag (tmp_universe vars u0)) in ⊢ (??%? → ???(match % with [_⇒?]?) → ?);
1052* #tmp' #u' #e #E whd in E:(???%);
1053destruct
1054whd in ⊢ (?%??); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit
1055@refl
1056qed.
1057
1058
1059let rec mklabels (ul:labgen) : (identifier Label) × (identifier Label) × labgen ≝
1060  match generate_fresh_label ul with
1061  [ mk_Sig res1 H1 ⇒
1062     let 〈entry_label, ul1〉 as E1 ≝ res1 in
1063     match generate_fresh_label ul1 with
1064     [ mk_Sig res2 H2 ⇒
1065        let 〈exit_label, ul2〉 as E2 ≝ res2 in
1066        〈entry_label, exit_label, ul2〉
1067     ]
1068  ].
1069
1070(* When converting loops into gotos, and in order to eliminate blocks, we have
1071 * to convert continues and breaks into goto's, too. We add some "flags" in
1072 * in argument to [translate_statement], meaning that the next encountered break
1073 * or continue has to be converted into a goto to some contained label.
1074 * ConvertTo l1 l2 means "convert continue to goto l1 and convert break to goto l2".
1075 *)
1076inductive convert_flag : Type[0] ≝
1077| DoNotConvert : convert_flag
1078| ConvertTo    : identifier Label → identifier Label → convert_flag. (* continue, break *)
1079
1080let rec labels_of_flag (flag : convert_flag) : list (identifier Label) ≝
1081match flag with
1082[ DoNotConvert ⇒ [ ]
1083| ConvertTo continue break ⇒ continue :: break :: [ ]
1084].
1085
1086(* For a top-level expression, [label-wf] collapses to "all labels are properly declared" *)
1087definition label_wf ≝
1088λ (s : statement) .λ (s' : stmt) .λ (lbls : lenv). λ (flag : convert_flag).
1089    stmt_P (λs1. stmt_labels (λl.ldefined s' l ∨ lpresent lbls l ∨ In ? l (labels_of_flag flag)) s1) s'.
1090
1091(* trans_inv is the invariant which is enforced during the translation from Clight to Cminor.
1092  The involved arguments are the following:
1093  . vars:var_types, an environment mapping variables to their types and allocation modes
1094  . lbls:lenv, a mapping from old (Clight) to fresh and new (Cminor) labels,
1095  . s:statement, a Clight statement,
1096  . uv, a fresh variable generator (containing itself some invariants)
1097  . flag, wich maps "break" and "continue" to "gotos"
1098  . su', a couple of a Cminor statement and fresh variable generator.
1099*)
1100definition trans_inv : ∀vars:var_types . ∀lbls:lenv . statement → tmpgen vars → convert_flag → ((tmpgen vars) × labgen × stmt) → Prop ≝
1101λvars,lbls,s,uv,flag,su'.
1102  let 〈uv', ul', s'〉 ≝ su' in
1103  stmt_inv (add_tmps vars (tmp_env … uv')) s' ∧   (* remaining variables in s' are local*)
1104  labels_translated lbls s s' ∧                   (* all the labels in s are transformed in label of s' using [lbls] as a map *)
1105  tmps_preserved vars uv uv' ∧                    (* the variables generated are local and grows in a monotonic fashion *)
1106  label_wf s s' lbls flag.                        (* labels are "properly" declared, as defined in [ŀabel_wf].*)
1107                                 
1108let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (s:statement) on s
1109  : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag su) ≝
1110match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag su) with
1111[ Sskip ⇒ OK ? «〈uv, ul, St_skip〉, ?»
1112| Sassign e1 e2 ⇒
1113    do e2' ← translate_expr vars e2;  (* rhs *)
1114    do dest ← translate_dest vars e1; (* e1 *)
1115    match dest with
1116    [ IdDest id ty p ⇒
1117       do e2' ← type_should_eq (typeof e2) ty ? e2';
1118       OK ? «〈uv, ul, St_assign ? id e2'〉, ?»
1119    | MemDest r e1' ⇒
1120       OK ? «〈uv, ul, St_store ? r e1' e2'〉, ?»
1121    ]
1122| Scall ret ef args ⇒
1123    do ef' ← translate_expr vars ef;
1124    do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef';
1125    do args' ← mmap_sigma ??? (translate_expr_sigma vars) args;
1126    match ret with
1127    [ None ⇒ OK ? «〈uv, ul, St_call (None ?) ef' args'〉, ?»
1128    | Some e1 ⇒
1129        do dest ← translate_dest vars e1;
1130        match dest with
1131        [ IdDest id ty p ⇒ OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?»
1132        | MemDest r e1' ⇒
1133            let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in
1134            OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r e1' (Id ? tmp))〉, ?»
1135        ]
1136    ]
1137| Ssequence s1 s2 ⇒
1138    do «fgens1, s1', H1» ← translate_statement vars uv ul «lbls,?» flag s1;
1139    do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) «lbls,?» flag s2;
1140    OK ? «〈fgens2, St_seq s1' s2'〉, ?»
1141| Sifthenelse e1 s1 s2 ⇒
1142    do e1' ← translate_expr vars e1;
1143    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
1144    [ ASTint _ _ ⇒ λe1'.
1145         do «fgens1, s1', H1» ← translate_statement vars uv ul «lbls,?» flag s1;
1146         do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) «lbls,?» flag s2;
1147        OK ? «〈fgens2, St_ifthenelse ?? e1' s1' s2'〉, ?»
1148    | _ ⇒ λ_.Error ? (msg TypeMismatch)
1149    ] e1'
1150| Swhile e1 s1 ⇒
1151    do e1' ← translate_expr vars e1;
1152    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
1153    [ ASTint _ _ ⇒ λe1'.         
1154         (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
1155         match mklabels ul with
1156         [ mk_Sig result Hmklabels =>
1157              let 〈labels, ul1〉 as E1 ≝ result in
1158              let 〈entry, exit〉 as E2 ≝ labels in
1159              do «fgens2, s1',H1» ← translate_statement vars uv ul1 «lbls,?» (ConvertTo entry exit) s1;
1160              let converted_loop ≝
1161               St_label entry
1162               (St_seq
1163                 (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) St_skip)
1164                 (St_label exit St_skip))
1165              in         
1166              OK ? «〈fgens2, converted_loop〉, ?»
1167         ]
1168    | _ ⇒ λ_.Error ? (msg TypeMismatch)
1169    ] e1'
1170| Sdowhile e1 s1 ⇒
1171    do e1' ← translate_expr vars e1;
1172    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
1173    [ ASTint _ _ ⇒ λe1'.
1174         match mklabels ul with
1175         [ mk_Sig result Hmklabels ⇒
1176              let 〈labels, ul1〉 as E1 ≝ result in
1177              let 〈entry, exit〉 as E2 ≝ labels in             
1178              do «fgens2, s1', H1» ← translate_statement vars uv ul1 «lbls,?» (ConvertTo entry exit) s1;
1179              let converted_loop ≝
1180               St_label entry
1181                 (St_seq
1182                   (St_seq
1183                     s1'
1184                     (St_ifthenelse ?? e1' (St_goto entry) St_skip)
1185                   )
1186                   (St_label exit St_skip))
1187              in
1188              (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
1189              OK ? «〈fgens2, converted_loop〉, ?»
1190         ]
1191    | _ ⇒ λ_.Error ? (msg TypeMismatch)
1192    ] e1'
1193| Sfor s1 e1 s2 s3 ⇒
1194    do e1' ← translate_expr vars e1;
1195    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
1196    [ ASTint _ _ ⇒ λe1'.
1197         match mklabels ul with
1198         [ mk_Sig result Hmklabels ⇒
1199              let 〈labels, ul1〉 as E ≝ result in
1200              let 〈entry, exit〉 as E2 ≝ labels in                           
1201              do «fgens2, s1', H1» ← translate_statement vars uv ul1 «lbls,?» flag s1;
1202              do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) «lbls, ?» (ConvertTo entry exit) s2;
1203              do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) «lbls, ?» (ConvertTo entry exit) s3;
1204              (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
1205              let converted_loop ≝
1206                St_seq
1207                 s1'
1208                 (St_label entry
1209                   (St_seq
1210                     (St_ifthenelse ?? e1' (St_seq s3' (St_seq s2' (St_goto entry))) St_skip)
1211                     (St_label exit St_skip)
1212                    ))
1213              in
1214             OK ? «〈fgens4, converted_loop〉, ?»
1215        ]
1216    | _ ⇒ λ_.Error ? (msg TypeMismatch)
1217    ] e1'
1218| Sbreak ⇒
1219   match flag return λf.flag = f → ? with
1220   [ DoNotConvert ⇒ λEflag.
1221     Error ? (msg FIXME)
1222   | ConvertTo continue_label break_label ⇒ λEflag.
1223     OK ? «〈uv, ul, St_goto break_label〉, ?»
1224   ] (refl ? flag)
1225| Scontinue ⇒
1226  match flag return λf.flag = f → ? with
1227  [ DoNotConvert ⇒ λEflag.
1228    Error ? (msg FIXME)
1229  | ConvertTo continue_label break_label ⇒ λEflag.
1230    OK ? «〈uv, ul, St_goto continue_label〉, ?»
1231  ] (refl ? flag)
1232| Sreturn ret ⇒
1233    match ret with
1234    [ None ⇒ OK ? «〈uv, ul, St_return (None ?)〉, ?»
1235    | Some e1 ⇒
1236        do e1' ← translate_expr vars e1;
1237        OK ? «〈uv, ul, St_return (Some ? (mk_DPair … e1'))〉, ?»
1238    ]
1239| Sswitch e1 ls ⇒ Error ? (msg FIXME)
1240| Slabel l s1 ⇒
1241    do l' as E ← lookup_label lbls l;
1242    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;
1243    OK ? «〈fgens1, St_label l' s1'〉, ?»
1244| Sgoto l ⇒
1245    do l' as E ← lookup_label lbls l;
1246    OK ? «〈uv, ul, St_goto l'〉, ?»
1247| Scost l s1 ⇒
1248    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;
1249    OK ? «〈fgens1, St_cost l s1'〉, ?»
1250].
1251try @conj try @conj try @conj try @conj try @conj try @conj try @conj
1252try (@I)
1253try (#l #H elim H)
1254try (#size #sign #H assumption)
1255try (#region #H assumption)
1256[ 1,5: @(tmp_preserved … p) ]
1257[ 1,3: elim e2' | 2,9: elim e1' | 4,7,14: elim ef' ]
1258[ 1,2,3,4,5,6,7 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
1259[ 1: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
1260             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
1261             | 3: elim args' // ]
1262| 8: (* we should be able to merge this case with the previous ... *)
1263     @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
1264             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
1265             | 3: elim args' // ]
1266| 2: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp)
1267| 3:  @(All_mp (𝚺 t:typ.expr t) (λe. match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars)]))
1268       [ 1: #a #Ha elim a in Ha ⊢ ?; #ta #a #Ha whd @(expr_vars_mp ?? (local_id vars))
1269       [ 1: #i0 #t0 #H0 @(tmp_preserved vars uv1 i0 t0 H0)
1270       | 2: assumption ]
1271       | 2: elim args' // ]
1272| 4: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) ]
1273[ 1: #size #sign | 2: #reg | 3: #fsize ]
1274[ 1,2,3: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ]
1275try @(match fgens1 return λx.x=fgens1 → ? with
1276     [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1))
1277try @(match fgens2 return λx.x=fgens2 → ? with
1278     [ mk_Prod uv2 ul2 ⇒ λHfgens2.? ] (refl ? fgens2))
1279try @(match fgens3 return λx.x=fgens3 → ? with
1280     [ mk_Prod uv3 ul3 ⇒ λHfgens3.? ] (refl ? fgens3))
1281try @(match fgens4 return λx.x=fgens4 → ? with
1282     [ mk_Prod uv4 ul4 ⇒ λHfgens4.? ] (refl ? fgens4))
1283whd in H1 H2 H3 ⊢ ?; destruct whd nodelta in H1 H2 H3;
1284try (elim H1 -H1 * * #Hstmt_inv1 #Hlabels_tr1 #Htmps_pres1)
1285try (elim H2 -H2 * * #Hstmt_inv2 #Hlabels_tr2 #Htmps_pres2)
1286try (elim H3 -H3 * * #Hstmt_inv3 #Hlabels_tr3 #Htmps_pres3)
1287[ 1,2: #Hind1 #Hind2 | 3,4,9,11: #Hind | 5: #Hind1 #Hind2 #Hind3 ]
1288try @conj try @conj try @conj try @conj try @conj try (whd @I) try assumption
1289[ 1,7: @(stmt_P_mp … Hstmt_inv1) #e #Hvars @(stmt_vars_mp … Hvars) #i #t #Hlocal @(Htmps_pres2 … Hlocal)
1290| 2: #l #H cases (Exists_append ???? H) #Hcase
1291         [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
1292           [ 1: @(proj1 ?? Hlabel)
1293           | 2: normalize @Exists_append_l @(proj2 … Hlabel) ]
1294         | 2: elim (Hlabels_tr2 l Hcase) #label #Hlabel @(ex_intro … label) @conj
1295           [ 1: @(proj1 ?? Hlabel)
1296           | 2: normalize @Exists_append_r @(proj2 … Hlabel) ]
1297         ]
1298| 3,9: #id #ty #H @(Htmps_pres2 … (Htmps_pres1 id ty H)) ]
1299[ 1: @(stmt_P_mp … Hind2) | 2: @(stmt_P_mp … Hind1) ]
1300[ 1,2: #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1301     #l * try * [ 1,4: #H %1 %1 normalize in H ⊢ %; try (@Exists_append_l @H); try (@Exists_append_r @H)
1302                | 2,5: #H %1 %2 assumption
1303                | 3,6: #H %2 assumption ]
1304(* if/then/else *)
1305| 3: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
1306| 4: whd #l #H
1307       cases (Exists_append ???? H) #Hcase
1308         [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
1309           [ 1: @(proj1 ?? Hlabel)
1310           | 2: normalize @Exists_append_l @(proj2 … Hlabel) ]
1311         | 2: elim (Hlabels_tr2 l Hcase) #label #Hlabel @(ex_intro … label) @conj
1312           [ 1: @(proj1 ?? Hlabel)
1313           | 2: normalize @Exists_append_r @(proj2 … Hlabel) ]
1314         ]
1315]                 
1316[ 1: 1: @(stmt_P_mp … Hind2) | 2: @(stmt_P_mp … Hind1) ]
1317[ 1,2: #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1318     #l * try * [ 1,4: #H %1 %1 normalize in H ⊢ %; try (@Exists_append_l @H); try (@Exists_append_r @H)
1319                | 2,5: #H %1 %2 assumption
1320                | 3,6: #H %2 assumption ] ]
1321try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I
1322[ 1,9,19,32: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
1323| 2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) //
1324| 3,10: whd #l #H normalize in H;
1325         elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label)
1326         @conj
1327         [ 1,3: @(proj1 … Hlabel)
1328         | 2,4: whd @or_intror normalize @Exists_append_l @Exists_append_l try @Exists_append_l
1329              @(proj2 … Hlabel) ]
1330| 30: whd %2 %2 whd /2/
1331| 31: whd %2 whd /2/
1332| 4,16: whd %1 %1 normalize /2/
1333| 5,12: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1334   #l * try * [ 1,5: #H %1 %1 normalize %2 @Exists_append_l @Exists_append_l try @Exists_append_l @H
1335              | 2,6: #H %1 %2 assumption
1336              | 3,7: #H <H %1 %1 normalize /2/
1337              | 4,8: #H normalize in H; elim H [ 1,3: #E <E %1 %1 normalize %2
1338                                                 @Exists_append_r normalize /2/
1339                                               | 2,4: * ]
1340              ]
1341| 6: normalize %1 %1 %1 //                                                                                   
1342| 7,14: normalize %1 %1 %2 @Exists_append_r normalize /2/
1343| 11,13: whd %1 %1 normalize /2/
1344| 15: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
1345                   | 2: #H elim (Hlabels_tr1 label H)
1346                         #lab * #Hlookup #Hdef @(ex_intro … lab) @conj
1347                         [ 1: // | 2: whd %2 assumption ]
1348                   ]
1349| 17: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1350   #l * try * [ 1: #H %1 %1 normalize %2 @H
1351              | 2: #H %1 %2 assumption
1352              | 3: #H %2 assumption ]
1353| 18: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
1354   #H @(Htmps_pres3 … (Htmps_pres2 … H))
1355| 20: @(stmt_P_mp … Hstmt_inv3) //
1356| 21: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
1357   #H @(Htmps_pres3 … H)
1358| 22: whd #l #H normalize in H;
1359      cases (Exists_append … H) #Hcase
1360      [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
1361        [ 1: @(proj1 … Hlabel)
1362        | 2: normalize @Exists_append_l @(proj2 … Hlabel)
1363        ]
1364      | 2: cases (Exists_append … Hcase) #Hcase2
1365        [ 1: elim (Hlabels_tr2 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
1366          [ 1: @(proj1 … Hlabel)
1367          | 2: normalize >append_nil >append_nil >append_cons
1368               @Exists_append_r @Exists_append_l @Exists_append_r
1369               @(proj2 … Hlabel)
1370          ]
1371        | 2: elim (Hlabels_tr3 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
1372          [ 1: @(proj1 … Hlabel)
1373          | 2: normalize >append_nil >append_nil >append_cons
1374             @Exists_append_r @Exists_append_l @Exists_append_l
1375             @(proj2 … Hlabel)
1376          ]
1377        ]
1378      ]
1379| 23: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
1380| 24: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1381   #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H
1382              | 2: #H %1 %2 assumption
1383              | 3: #H %2 assumption ]
1384| 25: whd %1 %1 normalize /2/
1385| 26: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1386   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
1387                   @Exists_append_r @Exists_append_l @Exists_append_l
1388                   @Exists_append_l assumption
1389              | 2: #H %1 %2 assumption
1390              | 3: #H <H %1 %1 normalize
1391                   @Exists_append_r whd %1 //
1392              | 4: * [ 1: #H <H %1 %1 normalize
1393                       @Exists_append_r @(Exists_add ?? (nil ?))
1394                       @Exists_append_r @Exists_append_r
1395                       whd %1 //
1396                     | 2: * ]
1397              ]
1398| 27: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1399   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
1400                   @Exists_append_r @Exists_append_l @Exists_append_l                   
1401                   @Exists_append_r @Exists_append_l assumption
1402              | 2: #H %1 %2 assumption
1403              | 3: #H <H %1 %1 normalize
1404                   @Exists_append_r whd %1 //
1405              | 4: * [ 1: #Eq <Eq %1 %1 whd normalize
1406                       @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r
1407                       @Exists_append_r whd %1 //
1408                     | 2: * ]
1409              ]
1410| 28: whd %1 %1 normalize /2/
1411| 29: whd %1 %1 normalize
1412      @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r
1413      whd %1 //
1414| 33: whd %1 %2 whd @(ex_intro … l) @E
1415] qed.
1416
1417axiom ParamGlobalMixup : String.
1418
1419(* params and statement aren't real parameters, they're just there for giving the invariant. *)
1420definition alloc_params :
1421 ∀vars:var_types.∀lbls,statement,uv,flag. list (ident×type) → (Σsu:(tmpgen vars)×labgen×stmt. trans_inv vars lbls statement uv flag su)
1422   → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag su) ≝   
1423λvars,lbls,statement,uv,ul,params,s. foldl ?? (λsu,it.
1424  let 〈id,ty〉 ≝ it in
1425  do «result,Is» ← su;
1426  let 〈fgens1, s〉 as Eresult ≝ result in
1427  do 〈t,ty'〉 as E ← lookup' vars id;
1428  match t return λx.? → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv ul su) with
1429  [ Local ⇒ λE. OK (Σs:(tmpgen vars)×labgen×stmt.?) «result,Is»
1430  | Stack n ⇒ λE.
1431      OK ? «〈fgens1, St_seq (St_store ? Any (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?»
1432  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
1433  ] E) (OK ? s) params.
1434whd
1435@(match fgens1 return λx.x=fgens1 → ? with
1436  [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1))
1437whd in Is ⊢ %; destruct whd in Is;
1438try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I
1439elim Is * * #Hincl #Hstmt_inv #Hlab_tr #Htmp_pr try assumption
1440@(expr_vars_mp … (tmp_preserved … uv1)) whd >E @refl
1441qed.
1442
1443axiom DuplicateLabel : String.
1444
1445definition lenv_list_inv : lenv → lenv → list ident → Prop ≝
1446λlbls0,lbls,ls.
1447 ∀l,l'. lookup_label lbls l = OK ? l' →
1448 Exists ? (λl'. l' = l) ls ∨ lookup_label lbls0 l = OK ? l'.
1449
1450lemma lookup_label_add : ∀lbls,l,l'.
1451  lookup_label (add … lbls l l') l = OK ? l'.
1452#lbls #l #l' whd in ⊢ (??%?); >lookup_add_hit @refl
1453qed.
1454
1455lemma lookup_label_miss : ∀lbls,l,l',l0.
1456  l0 ≠ l →
1457  lookup_label (add … lbls l l') l0 = lookup_label lbls l0.
1458#lbls #l #l' #l0 #NE
1459whd in ⊢ (??%%);
1460>lookup_add_miss
1461[ @refl | @NE ]
1462qed.
1463
1464let rec populate_lenv (ls:list ident) (ul:labgen) (lbls:lenv): res ((Σlbls':lenv. lenv_list_inv lbls lbls' ls) × labgen) ≝
1465match ls return λls.res ((Σlbls':lenv. lenv_list_inv lbls lbls' ls) × labgen) with
1466[ nil ⇒ OK ? 〈«lbls, ?», ul〉
1467| cons l t ⇒
1468  match lookup_label lbls l return λlook. lookup_label lbls l = look → ? with
1469  [ OK _    ⇒ λ_.Error ? (msg DuplicateLabel)
1470  | Error _ ⇒ λLOOK.
1471    match generate_fresh_label … ul with
1472    [ mk_Sig ret H ⇒
1473       do 〈packed_lbls, ul1〉 ← populate_lenv t (snd ?? ret) (add … lbls l (fst ?? ret));
1474       match packed_lbls with
1475       [ mk_Sig lbls' Hinv ⇒ OK ? 〈«lbls', ?», ul1〉 ]
1476    ]
1477  ] (refl ? (lookup_label lbls l))
1478].
1479[ 1: whd #l #l' #Hlookup %2 assumption
1480| 2: whd in Hinv; whd #cl_lab #cm_lab #Hlookup
1481     @(eq_identifier_elim … l cl_lab)
1482     [ 1: #Heq %1 >Heq whd %1 //
1483     | 2: #Hneq cases (Hinv cl_lab cm_lab Hlookup)
1484           [ 1: #H %1 %2 @H
1485           | 2: #LOOK' %2 >lookup_label_miss in LOOK'; /2/ #H @H ]
1486     ]
1487]
1488qed.
1489
1490definition build_label_env :
1491   ∀body:statement. res ((Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) × labgen) ≝
1492λbody.
1493  let initial_labgen ≝ mk_labgen (new_universe ?) (nil ?) ?  in
1494  do 〈label_map, u〉 ← populate_lenv (labels_defined body) initial_labgen (empty_map ??);
1495  let lbls ≝ pi1 ?? label_map in
1496  let H    ≝ pi2 ?? label_map in
1497  OK ? 〈«lbls, ?», u〉.
1498[ 1: #l #l' #E cases (H l l' E) //
1499     whd in ⊢ (??%? → ?); #H destruct
1500| 2: whd @I ]
1501qed.
1502
1503lemma local_id_split : ∀vars,tmpgen,i,t.
1504  local_id (add_tmps vars (tmp_env vars tmpgen)) i t →
1505  local_id vars i t ∨ Exists ? (λx. \fst x = i ∧ typ_of_type (\snd x) = t) (tmp_env … tmpgen).
1506#vars #tmpgen #i #t
1507whd in ⊢ (?%?? → ?);
1508elim (tmp_env vars tmpgen)
1509[ #H %1 @H
1510| * #id #ty #tl #IH
1511  cases (identifier_eq ? i id)
1512  [ #E >E #H %2 whd %1 % [ @refl | whd in H; whd in H:(match % with [_⇒?|_⇒?]); >lookup_add_hit in H; #E1 >E1 @refl ]
1513  | #NE #H cases (IH ?)
1514    [ #H' %1 @H'
1515    | #H' %2 %2 @H'
1516    | whd in H; whd in H:(match % with [ _ ⇒ ? | _ ⇒ ? ]);
1517      >lookup_add_miss in H; [ #H @H | @NE ]
1518    ]
1519  ]
1520] qed.
1521
1522lemma Exists_squeeze : ∀A,P,l1,l2,l3.
1523  Exists A P (l1@l3) → Exists A P (l1@l2@l3).
1524#A #P #l1 #l2 #l3 #EX
1525cases (Exists_append … EX)
1526[ #EX1 @Exists_append_l @EX1
1527| #EX3 @Exists_append_r @Exists_append_r @EX3
1528] qed.
1529
1530(* This lemma allows to merge two stmt_P in one. Used in the following parts to merge an invariant on variables
1531   and an invariant on labels. *)
1532lemma 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.
1533#P1 #P2 #s elim s
1534normalize try @conj try @conj try /3/
1535[ #z0 #s #Hind1 #Hind2 * * #HA #HB #HC * * #HD #HE #HF try @conj try @conj try @conj try /2/
1536| #H5 #H6 #H7 #H8 #H9 #H10 #H11 * * #H15 #H16 #H17 * * #H20 #H21 #H22
1537  try @conj try @conj try @conj try /2/
1538| 3,4: #H24 #H25 * #H29 #H30 * #H33 #H34 try @conj try @conj try @conj try /2/
1539| 5,6: #H36 #H37 #H38 * #H42 #H43 * #H46 #H47 try @conj try @conj try @conj try /2/ ]
1540qed.
1541
1542definition translate_function :
1543  ∀tmpuniverse:universe SymbolTag.
1544  ∀globals:list (ident×region×type).
1545  ∀f:function.
1546    globals_fresh_for_univ ? globals tmpuniverse →
1547    fn_fresh_for_univ f tmpuniverse →
1548  res internal_function ≝
1549λtmpuniverse, globals, f, Fglobals, Ffn.
1550  do 〈env_pack, ul〉 ← build_label_env (fn_body f);
1551    match env_pack with
1552    [ mk_Sig lbls Ilbls ⇒
1553      let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in
1554      let uv ≝ mk_tmpgen vartypes tmpuniverse [ ] ?? in
1555      do s0 ← translate_statement vartypes uv ul lbls DoNotConvert (fn_body f);
1556      do «fgens, s1, Is» ← alloc_params vartypes lbls ? uv DoNotConvert (fn_params f) s0;
1557      let params ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f) in
1558      let vars ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? (fst ?? fgens) @ fn_vars f) in
1559      do D ← check_distinct_env ?? (params @ vars);
1560      OK ? (mk_internal_function
1561        (opttyp_of_type (fn_return f))
1562        params
1563        vars
1564        D
1565        stacksize
1566        s1 ?)
1567  ].
1568[ 1: #i #t #Hloc whd @Hloc
1569| 2: whd #id #Hpresent normalize in Hpresent:(???%?); whd in Hpresent;
1570      @(characterise_vars_fresh … (sym_eq … E)) //
1571| 3: @(match fgens return λx.x=fgens → ? with
1572     [ mk_Prod uv' ul' ⇒ λHfgens.? ] (refl ? fgens))
1573     whd in Is; <Hfgens in Is; #Is whd in Is ⊢ %;
1574     elim Is * * #Hstmt_inv #Hlab_trans #Htmps_pres #Hlabel_wf
1575     (* merge Hlabel_wf with Hstmt_inv and eliminate right away *)
1576     @(stmt_P_mp … (stmt_P_conj … Hstmt_inv Hlabel_wf))
1577     #s * #Hstmt_vars #Hstmt_labels @conj
1578     [ 1: (* prove that variables are either parameters or locals *)
1579        @(stmt_vars_mp … Hstmt_vars) #i #t #H
1580        (* Case analysis: (i, t) is either in vartypes, or in (tmp_env vartypes uv) *)
1581        cases (local_id_split … H)
1582        [ 1: #H' >map_append
1583          @Exists_map [ 1: #x @(And (\fst x = i) (typ_of_type (\snd x) = t))  (* * #id #ty @(〈id, typ_of_type ty〉=〈i, t〉)*)
1584                      | 2: whd @Exists_squeeze @(characterise_vars_all globals f ?? (sym_eq ??? E) i t H')
1585                      | 3: * #id #ty * #E1 #E2 <E1 <E2 @refl
1586                      ]
1587        | 2: #EX @Exists_append_r whd in ⊢ (???%); <map_append @Exists_append_l
1588          @Exists_map [ 1: #x @(And (\fst x = i) (typ_of_type (\snd x) = t))
1589                      | 2: <Hfgens @EX
1590                      | 3: * #id #ty * #E1 #E2 <E1 <E2 % @refl
1591                      ]
1592        ]
1593     | 2: (* prove that labels are properly declared. *)
1594          @(stmt_labels_mp … Hstmt_labels) #l * *
1595          [ 1: #H assumption
1596          | 2: * #cl_label #Hlookup lapply (Ilbls cl_label l Hlookup) #Hdefined
1597                cases (Hlab_trans … Hdefined) #lx * #LOOKUPx >LOOKUPx in Hlookup; #Ex destruct (Ex)
1598                #H @H
1599          ]
1600    ]
1601] qed.   
1602
1603definition translate_fundef :
1604  ∀tmpuniverse:universe SymbolTag.
1605  ∀globals:list (ident×region×type).
1606    globals_fresh_for_univ ? globals tmpuniverse →
1607  ∀f:clight_fundef.
1608    fd_fresh_for_univ f tmpuniverse →
1609  res (fundef internal_function) ≝
1610λtmpuniverse,globals,Fglobals,f.
1611match f return λf. fd_fresh_for_univ f ? → ? with
1612[ CL_Internal fn ⇒ λFf. do fn' ← translate_function tmpuniverse globals fn Fglobals Ff; OK ? (Internal ? fn')
1613| CL_External fn argtys retty ⇒ λ_. OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
1614].
1615
1616(* TODO: move universe generation to higher level once we do runtime function
1617   generation.  Cheating a bit - we only need the new identifiers to be fresh
1618   for individual functions. *)
1619
1620let rec map_partial_All (A,B:Type[0]) (P:A → Prop) (f:∀a:A. P a → res B)
1621  (l:list A) (H:All A P l) on l : res (list B) ≝
1622match l return λl. All A P l → ? with
1623[ nil ⇒ λ_. OK (list B) (nil B)
1624| cons hd tl ⇒ λH.
1625    do b_hd ← f hd (proj1 … H);
1626    do b_tl ← map_partial_All A B P f tl (proj2 … H);
1627      OK (list B) (cons B b_hd b_tl)
1628] H.
1629
1630definition clight_to_cminor : clight_program → res Cminor_program ≝
1631λp.
1632  let tmpuniverse ≝ universe_for_program p in
1633  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
1634  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
1635  let globals ≝ fun_globals @ var_globals in
1636  do fns ← map_partial_All ??? (λx,H. do f ← translate_fundef tmpuniverse globals ? (\snd x) H; OK ? 〈\fst x, f〉) (prog_funct ?? p) ?;
1637    OK ? (mk_program ??
1638      (map ?? (λv. 〈\fst v, \fst (\snd v)〉) (prog_vars ?? p))
1639      fns
1640      (prog_main ?? p)).
1641cases (prog_fresh p) * #H1 #H2 #H3
1642[ @(All_mp … H1) #x * //
1643| @All_append
1644  [ elim (prog_funct ?? p) in H1 ⊢ %; // * #id #fd #tl #IH * * #Hhd1 #Hhd2 #Htl % // @IH @Htl
1645  | whd in H3; elim (prog_vars ?? p) in H3 ⊢ %; // #hd #tl #IH * #Hhd #Htl % /2/
1646  ]
1647] qed.
1648
1649(* It'd be nice to go back to some generic thing like
1650
1651 transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)).
1652
1653   rather than the messier definition above.
1654*)
Note: See TracBrowser for help on using the repository browser.