source: src/Clight/toCminor.ma @ 2468

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

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

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