source: src/Clight/toCminor.ma @ 2593

include "Clight/ClassifyOp.ma".
include "basics/lists/list.ma".
include "Clight/fresh.ma".

(* Identify local variables that must be allocated memory. *)
(* These are the variables whose addresses are taken. *)
let rec gather_mem_vars_expr (e:expr) : identifier_set SymbolTag ≝
match e with
[ Expr ed ty ⇒
    match ed with
    [ Ederef e1 ⇒ gather_mem_vars_expr e1
    | Eaddrof e1 ⇒ gather_mem_vars_addr e1
    | Eunop _ e1 ⇒ gather_mem_vars_expr e1
    | Ebinop _ e1 e2 ⇒ gather_mem_vars_expr e1 ∪
                       gather_mem_vars_expr e2
    | Ecast _ e1 ⇒ gather_mem_vars_expr e1
    | Econdition e1 e2 e3 ⇒ gather_mem_vars_expr e1 ∪
                            gather_mem_vars_expr e2 ∪
                            gather_mem_vars_expr e3
    | Eandbool e1 e2 ⇒ gather_mem_vars_expr e1 ∪
                       gather_mem_vars_expr e2
    | Eorbool e1 e2 ⇒ gather_mem_vars_expr e1 ∪
                      gather_mem_vars_expr e2
    | Efield e1 _ ⇒ gather_mem_vars_expr e1
    | Ecost _ e1 ⇒ gather_mem_vars_expr e1
    | _ ⇒ ∅
    ]
]
and gather_mem_vars_addr (e:expr) : identifier_set SymbolTag ≝
match e with
[ Expr ed ty ⇒
    match ed with
    [ Evar x ⇒ { (x) }
    | Ederef e1 ⇒ gather_mem_vars_expr e1
    | Efield e1 _ ⇒ gather_mem_vars_addr e1
    | _ ⇒ ∅ (* not an lvalue *)
    ]
].

let rec gather_mem_vars_stmt (s:statement) : identifier_set SymbolTag ≝
match s with
[ Sskip ⇒ ∅
| Sassign e1 e2 ⇒ gather_mem_vars_expr e1 ∪
                  gather_mem_vars_expr e2
| Scall oe1 e2 es ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ] ∪
                    gather_mem_vars_expr e2 ∪
                    (foldl ?? (λs,e. s ∪ gather_mem_vars_expr e) ∅ es)
| Ssequence s1 s2 ⇒ gather_mem_vars_stmt s1 ∪
                    gather_mem_vars_stmt s2
| Sifthenelse e1 s1 s2 ⇒ gather_mem_vars_expr e1 ∪
                         gather_mem_vars_stmt s1 ∪
                         gather_mem_vars_stmt s2
| Swhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
                 gather_mem_vars_stmt s1
| Sdowhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
                   gather_mem_vars_stmt s1
| Sfor s1 e1 s2 s3 ⇒ gather_mem_vars_stmt s1 ∪
                     gather_mem_vars_expr e1 ∪
                     gather_mem_vars_stmt s2 ∪
                     gather_mem_vars_stmt s3
| Sbreak ⇒ ∅
| Scontinue ⇒ ∅
| Sreturn oe1 ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ]
| Sswitch e1 ls ⇒ gather_mem_vars_expr e1 ∪
                  gather_mem_vars_ls ls
| Slabel _ s1 ⇒ gather_mem_vars_stmt s1
| Sgoto _ ⇒ ∅
| Scost _ s1 ⇒ gather_mem_vars_stmt s1
]
and gather_mem_vars_ls (ls:labeled_statements) on ls : identifier_set SymbolTag ≝
match ls with
[ LSdefault s1 ⇒ gather_mem_vars_stmt s1
| LScase _ _ s1 ls1 ⇒ gather_mem_vars_stmt s1 ∪
                      gather_mem_vars_ls ls1
].

(* Defines where a variable should be allocated. *)
inductive var_type : Type[0] ≝
| Global : region → var_type  (* A global, allocated statically in a given region (which one ???)  *)
| Stack  : nat → var_type     (* On the stack, at a given height *) 
| Local  : var_type           (* Locally (hopefully, in a register) *)
.

(* A map associating each variable identifier to its allocation mode and its type. *)
definition var_types ≝ identifier_map SymbolTag (var_type × type).

axiom UndeclaredIdentifier : String.

definition lookup' ≝
λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id).

(* Assert that an identifier is a local variable with the given typ. *)
definition local_id : var_types → ident → typ → Prop ≝
λvars,id,t. match lookup' vars id with [ OK vt ⇒ match (\fst vt) with [ Global _ ⇒ False | _ ⇒ t = typ_of_type (\snd vt) ] | _ ⇒ False ].

(* Note that the semantics allows locals to shadow globals.
   Parameters start out as locals, but get stack allocated if their address
   is taken.  We will add code to store them if that's the case.
 *)

(* Some kind of data is never allocated in registers, even if it fits, typically structured data. *)
definition always_alloc : type → bool ≝
λt. match t with
[ Tarray _ _ ⇒ true
| Tstruct _ _ ⇒ true
| Tunion _ _ ⇒ true
| _ ⇒ false
].

(* This builds a [var_types] map characterizing the allocation mode, of variables,
 * and it returns a stack usage for the function (in bytes, according to [sizeof]) *)
definition characterise_vars : list (ident×region×type) → function → var_types × nat ≝
λglobals, f.
  (* globals are added into a map, with var_type Global, region π_2(idrt) and type π_3(idrt) *)
  let m ≝ foldr ?? (λidrt,m. add ?? m (\fst (\fst idrt)) 〈Global (\snd (\fst idrt)), \snd idrt〉) (empty_map ??) globals in
  (* variables whose addr is taken in the body of the function are gathered in [mem_vars] *)
  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
  (* iterate on the parameters and local variables of the function, with a tuple (map, stack_high) as an accumulator *)
  let 〈m,stacksize〉 ≝ foldr ?? (λv,ms.
    let 〈m,stack_high〉 ≝ ms in 
    let 〈id,ty〉 ≝ v in         
    let 〈c,stack_high〉 ≝
      (* if the (local, parameter) variable is of a compound type OR if its adress is taken, we allocate it on the stack. *)
      if always_alloc ty ∨ id ∈ mem_vars then 
        〈Stack stack_high,stack_high + sizeof ty〉
      else 
        〈Local, stack_high〉 
    in
      〈add ?? m id 〈c, ty〉, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in
  〈m,stacksize〉.

(* A local variable id' status is not modified by the removal of a global variable id : id' is still local *)
lemma local_id_add_global : ∀vars,id,r,t,id',t'.
  local_id (add ?? vars id 〈Global r, t〉) id' t' → local_id vars id' t'.
#var #id #r #t #id' #t'
whd in ⊢ (% → ?); whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?);
cases (identifier_eq ? id id')
[ #E >E >lookup_add_hit whd in ⊢ (% → ?); *
| #NE >lookup_add_miss /2/
] qed.

(* If I add a variable id ≠ id', then id' is still local *)
lemma local_id_add_miss : ∀vars,id,vt,id',t'.
  id ≠ id' → local_id (add ?? vars id vt) id' t' → local_id vars id' t'.
#vars #id #vt #id' #t' #NE
whd in ⊢ (% → %);
whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ]);
>lookup_add_miss
[ #H @H | /2/ ]
qed.

(* After characterise_vars, a variable in the resulting map is either a global or a "local"(register or stack allocated) *)
lemma characterise_vars_src : ∀gl,f,vars,n.
  characterise_vars gl f = 〈vars,n〉 →
  ∀id. present ?? vars id → 
   (∃r,ty. lookup' vars id = OK ? 〈Global r,ty〉 ∧ Exists ? (λx.x = 〈〈id,r〉,ty〉) gl) ∨
   ∃t.local_id vars id t.
#globals #f
whd in ⊢ (∀_.∀_.??%? → ?);
elim (fn_params f @ fn_vars f)
[ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #H %1
  elim globals in H ⊢ %;
  [ normalize * #H cases (H (refl ??))
  | * * #id #rg #ty #tl #IH #H
    cases (identifier_eq ? i id)
    [ #E <E %{rg} %{ty} % [ whd in ⊢ (??%?); >lookup_add_hit // | %1 // ]
    | #NE cases (IH ?)
      [ #rg' * #ty' * #H1 #H2 %{rg'} %{ty'} %
        [ whd in ⊢ (??%?); >lookup_add_miss  [ @H1 | @NE ]
        | %2 @H2
        ]
      | whd in H ⊢ %; >lookup_add_miss in H; //
      ]
    ]
  ]
| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i
  #H >(contract_pair var_types nat ?) in E;
  whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
  cases (always_alloc ty ∨ id ∈ ?) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
  #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
  cases (identifier_eq ? i id)
  [ 1,3: #E' <E' in EQ2:%; #EQ2 %2 %{(typ_of_type ty)}
         destruct (EQ2) whd whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]);
         >lookup_add_hit @refl
  | *: #NE cases (IH m0 n0 ? i ?)
    [ 1,5: * #rg' * #ty' * #H1 #H2 %1 %{rg'} %{ty'} % //
           destruct (EQ2) whd in ⊢ (??%?); >lookup_add_miss try @NE @H1
    | 2,6: * #t #H1 %2 %{t} destruct (EQ2) whd whd in ⊢ (match % with [_ ⇒ ?|_ ⇒ ?]);
           >lookup_add_miss //
    | 3,7: <EQ @refl
    | *: destruct (EQ2) whd in H; >lookup_add_miss in H; //
    ]
  ]
] qed.

(* A local variable in a function is either a parameter or a "local" (:=register or stack alloc'd) 
 * variable, with the right type *)
lemma characterise_vars_all : ∀l,f,vars,n.
  characterise_vars l f = 〈vars,n〉 →
  ∀i,t. local_id vars i t →
        Exists ? (λx.\fst x = i ∧ typ_of_type (\snd x) = t) (fn_params f @ fn_vars f).
#globals #f
whd in ⊢ (∀_.∀_.??%? → ?);
elim (fn_params f @ fn_vars f)
[ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #t #H @False_ind
  elim globals in H;
  [ normalize //
  | * * #id #rg #t #tl #IH whd in ⊢ (?%?? → ?); #H @IH @(local_id_add_global … H)
  ]
| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i #t

  #H >(contract_pair var_types nat ?) in E;
  whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
  cases (always_alloc ty ∨ id ∈ ?) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
  #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2

  cases (identifier_eq ? id i)
  [ 1,3: #E' >E' in EQ2:%; #EQ2 % %
    [ 1,3: @refl
    | *: destruct (EQ2) change with (add ?????) in H:(?%??);
      whd in H; whd in H:(match % with [_ ⇒ ?|_ ⇒ ?]); >lookup_add_hit in H;
      whd in ⊢ (% → ?); #E'' >E'' @refl
    ]
  | *: #NE %2 @(IH m0 n0)
    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])); >contract_pair @EQ
    | 2,4: destruct (EQ2) @(local_id_add_miss … H) @NE
    ]
  ]
] qed.

(* The map generated by characterise_vars is "correct" wrt the fresh ident generator of tag [u],
   i.e. by generating fresh idents with u, we risk no collision with the idents in the map domain. *)
lemma characterise_vars_fresh : ∀gl,f,vars,n,u.
  characterise_vars gl f = 〈vars,n〉 →              (* If we generate a map ... *)
  globals_fresh_for_univ ? gl u →                  (* and the globals are out of the idents generated by u *)
  fn_fresh_for_univ f u →                          (* and the variables of the function f are cool with u too ... *)
  fresh_map_for_univ … vars u.                     (* then there won't be collisions between the map and idents made from u *)
#gl #f #vars #n #u #CH #GL #FN
#id #H
cases (characterise_vars_src … CH … H)
[ * #rg * #ty * #H1 #H2
  cases (Exists_All … H2 GL) * * #id' #rg' #ty' * #E #H destruct //
| * #t #H lapply (characterise_vars_all … CH id t H) #EX
  cases (Exists_All … EX FN) * #id' #ty' * * #E1 #E2 #H' -H destruct //
] qed.

include "Cminor/syntax.ma".
include "common/Errors.ma".

alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)".

axiom BadlyTypedAccess : String.
axiom BadLvalue : String.
axiom MissingField : String.

(* type_should_eq enforces that two types are equal and eliminates this equality by
   transporting P ty1 to P ty2. If ty1 != ty2, then Error *)
definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
λty1,ty2,P,p.
  do E ← assert_type_eq ty1 ty2;
  OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p).
  
(* associated reasoning principle *)
lemma type_should_eq_inversion : 
  ∀ty1,ty2,P,f,res.
    type_should_eq ty1 ty2 P f = OK ? res →
    ty1 = ty2 ∧ f ≃ res.
#ty1 #ty2 #P #f #res normalize
cases (type_eq_dec ty1 ty2) normalize nodelta
[ 2: #Hneq #Habsurd destruct ]
#Heq #Heq2 @conj try assumption
destruct (Heq2) cases Heq normalize nodelta
@eq_to_jmeq @refl
qed.  

(* same gig for regions *)
definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
* * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
qed.

(* same gig for AST typs *)
definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2) ≝
λty1,ty2,P,p.
  match typ_eq ty1 ty2 with
  [ inl E ⇒ OK ? (p⌈P ty1 ↦ P ty2⌉)
  | inr _ ⇒ Error ? (msg TypeMismatch)
  ].
destruct %
qed.

(* associated reasoning principle *)
lemma typ_should_eq_inversion : 
  ∀ty1,ty2,P,a,x. 
    typ_should_eq ty1 ty2 P a = OK ? x → 
    ty1 = ty2 ∧ a ≃ x.
* [ #sz #sg ] * [ 1,3: #sz2 #sg2 ]
[ 4: #P #a #x normalize #H destruct (H) @conj try @refl @refl_jmeq
| 3: cases sz cases sg #P #A #x normalize #H destruct
| 2: cases sz2 cases sg2 #P #a #x normalize #H destruct ] 
cases sz cases sz2 cases sg cases sg2
#P #a #x #H normalize in H:(??%?); destruct (H)
try @conj try @refl try @refl_jmeq
qed.

alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)".
alias id "CMunop" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.ind(1,0,0)".

(* XXX: For some reason matita refuses to pick the right one unless forced. *)
alias id "CMnotbool" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.con(0,3,0)".

(* Translates a Clight unary operation into a Cminor one, while checking
 * that the domain and codomain types are consistent. *)
definition translate_unop : ∀t,t':typ. CLunop → res (CMunop t t') ≝
λt,t'.λop:CLunop.
  match op with
  [ Onotbool ⇒
      match t return λt. res (CMunop t t') with
      [ ASTint sz sg ⇒
          match t' return λt'. res (CMunop ? t') with 
          [ ASTint sz' sg' ⇒ OK ? (CMnotbool ????)
          | _ ⇒ Error ? (msg TypeMismatch)
          ]
      | ASTptr ⇒
          match t' return λt'. res (CMunop ? t') with 
          [ ASTint sz' sg' ⇒ OK ? (CMnotbool ????)
          | _ ⇒ Error ? (msg TypeMismatch)
          ]
      | _ ⇒ Error ? (msg TypeMismatch)
      ]
  | Onotint ⇒
      match t' return λt'. res (CMunop t t') with
      [ ASTint sz sg ⇒ typ_should_eq ?? (λt. CMunop t (ASTint ??)) (Onotint sz sg)
      | _ ⇒ Error ? (msg TypeMismatch)
      ]
  | Oneg ⇒
      match t' return λt'. res (CMunop t t') with
      [ ASTint sz sg ⇒ typ_should_eq ?? (λt.CMunop t (ASTint ??)) (Onegint sz sg)
    (*  | ASTfloat sz ⇒ typ_should_eq ?? (λt.CMunop t (ASTfloat sz)) (Onegf sz) *)
      | _ ⇒ Error ? (msg TypeMismatch)
      ]
  ]. @I qed.

(* Translates a Clight addition into a Cminor one. Four cases to consider :
  - integer/integer add
  - fp/fp add
  - pointer/integer
  - integer/pointer.
  Consistency of the type is enforced by explicit checks.
*)

(* First, how to get rid of a abstract-away pointer or array type *)
definition fix_ptr_type : ∀ty,n. expr (typ_of_type (ptr_type ty n)) → expr ASTptr ≝
λty,n,e. e⌈expr (typ_of_type (ptr_type ty n)) ↦ expr ASTptr⌉.
cases n //
qed.

definition translate_add ≝
λty1,ty2,ty'.
let ty1' ≝ typ_of_type ty1 in
let ty2' ≝ typ_of_type ty2 in
match classify_add ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
[ add_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oadd ??) e1 e2)
(* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *)
| add_case_pi n ty sz sg ⇒
    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddpi I16) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
| add_case_ip n sz sg ty ⇒
    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddip I16) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))) (fix_ptr_type … e2))
| add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch)
].


(* XXX Clight pointer/int subtraction uses neg_shift_pointer_n, which boils down to (sub32 lhs (mul32 (const32 sizeof_ty) (sext32/zext32 rhs))),
 * whereas Cminor uses neg_shift_pointer, which translates into (sub32 lhs (sext32 rhs)). We have to translate the multiplication as actual
 * Cminor code, yielding something like (sub32 lhs (sext32 (mulXX (constXX sizeof_ty) (sextXX/zextXX rhs)))). In the original translate_sub,
 * XX=16, which we can't prove equivalent in general. Moreover, Osubpi expects a /signed/ integer argument, whereas Clight does not care and
 * casesplits on the sign to select either a zero extension or a sign extension. 
 * λ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))))))
      corresponding cl value: Some ? (Vptr (shift_pointer_n ? ptr1 (sizeof ty) sg n2))  =
      mk_offset (sub32 lhs (mult32 (const32 (sizeof ty)) (sext32/zext32 rhs)))

      cminor
      mk_offset (sub32 lhs (sext32 )) 
 *)
definition translate_sub ≝
λty1,ty2,ty'.
let ty1' ≝ typ_of_type ty1 in
let ty2' ≝ typ_of_type ty2 in
match classify_sub ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
[ sub_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osub ??) e1 e2)
(* XXX could optimise cast as above *)
| sub_case_pi n ty sz sg ⇒
    (* XXX This is so ugly. *)
    λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I32) (fix_ptr_type … e1)
                                                    (Op1 ?? (Ocastint ?? I32 Signed) (Op2 ??? (Omul I16 sg) (Op1 ?? (Ocastint ??? sg) e2)
                                                                                     (Cst ? (Ointconst I16 sg (repr I16 (sizeof ty)))))))
(* XXX check in detail? *)
| sub_case_pp n1 n2 ty1 ty2 ⇒ 
    λe1,e2. match ty' return λty'. res (CMexpr (typ_of_type ty')) with
    [ Tint sz sg ⇒ 
      (* XXX we make the constant unsigned to match CL semantics. We also use 32 bits, still for CL semantics. Documented in Csem.ma@sem_sub *)
      (* 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)))))) *)
         OK ? (Op1 ?? (Ocastint I32 Unsigned sz sg) (Op2 ??? (Odivu I32) (Op2 ??? (Osubpp I32) (fix_ptr_type … e1) (fix_ptr_type ?? e2)) (Cst ? (Ointconst I32 Unsigned (repr ? (sizeof ty1))))))
    | _ ⇒ Error ? (msg TypeMismatch)
    ]
| sub_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
].

definition translate_mul ≝
λty1,ty2,ty'.
let ty1' ≝ typ_of_type ty1 in
let ty2' ≝ typ_of_type ty2 in
match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
[ aop_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omul …) e1 e2)
(* | aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omulf …) e1 e2) *)
| aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
].

definition translate_div ≝
λty1,ty2,ty'.
let ty1' ≝ typ_of_type ty1 in
let ty2' ≝ typ_of_type ty2 in
match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
[ aop_case_ii sz sg ⇒
    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
    [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivu …) e1 e2)
    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odiv …) e1 e2)
    ]
(* | aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivf …) e1 e2) *)
| aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
].

definition translate_mod ≝
λty1,ty2,ty'.
let ty1' ≝ typ_of_type ty1 in
let ty2' ≝ typ_of_type ty2 in
match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
[ aop_case_ii sz sg ⇒
    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
    [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omodu …) e1 e2)
    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omod …) e1 e2)
    ]
(* no float case *)
| _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
].

definition translate_shr ≝
λty1,ty2,ty'.
let ty1' ≝ typ_of_type ty1 in
let ty2' ≝ typ_of_type ty2 in
match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
[ aop_case_ii sz sg ⇒
    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
    [ Unsigned ⇒ λe1,e2.  typ_should_eq ??? (Op2 ??? (Oshru …) e1 e2)
    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oshr …) e1 e2)
    ]
(* no float case *)
| _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
].

definition complete_cmp : ∀ty'. CMexpr (ASTint I8 Unsigned) → res (CMexpr (typ_of_type ty')) ≝
λty',e.
match ty' return λty'. res (CMexpr (typ_of_type ty')) with
[ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I8 Unsigned sz sg) e)
| _ ⇒ Error ? (msg TypeMismatch)
]. 
 
definition translate_cmp ≝
λc,ty1,ty2,ty'.
let ty1' ≝ typ_of_type ty1 in
let ty2' ≝ typ_of_type ty2 in
match classify_cmp ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
[ cmp_case_ii sz sg ⇒
    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
    [ Unsigned ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpu … c) e1 e2)
    | Signed ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmp … c) e1 e2)
    ]
| cmp_case_pp n ty ⇒
    λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpp … c) (fix_ptr_type … e1) (fix_ptr_type … e2))
(* | cmp_case_ff sz ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpf … c) e1 e2) *)
| cmp_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
].

definition translate_misc_aop ≝
λty1,ty2,ty',op.
let ty1' ≝ typ_of_type ty1 in
let ty2' ≝ typ_of_type ty2 in
match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
[ aop_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ?? (ASTint sz sg) (op sz sg) e1 e2)
| _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
].

definition translate_binop : binary_operation → type → CMexpr ? → type → CMexpr ? → type → res (CMexpr ?) ≝
λop,ty1,e1,ty2,e2,ty.
let ty' ≝ typ_of_type ty in
match op with
[ Oadd ⇒ translate_add ty1 ty2 ty e1 e2
| Osub ⇒ translate_sub ty1 ty2 ty e1 e2
| Omul ⇒ translate_mul ty1 ty2 ty e1 e2
| Omod ⇒ translate_mod ty1 ty2 ty e1 e2
| Odiv ⇒ translate_div ty1 ty2 ty e1 e2
| Oand ⇒ translate_misc_aop ty1 ty2 ty Oand e1 e2
| Oor  ⇒ translate_misc_aop ty1 ty2 ty Oor e1 e2
| Oxor ⇒ translate_misc_aop ty1 ty2 ty Oxor e1 e2
| Oshl ⇒ translate_misc_aop ty1 ty2 ty Oshl e1 e2
(*| Oshr ⇒ translate_misc_aop ty1 ty2 ty Oshr e1 e2 *)
| Oshr ⇒ translate_shr ty1 ty2 ty e1 e2  (* split on signed/unsigned *)
| Oeq ⇒ translate_cmp Ceq ty1 ty2 ty e1 e2
| One ⇒ translate_cmp Cne ty1 ty2 ty e1 e2
| Olt ⇒ translate_cmp Clt ty1 ty2 ty e1 e2
| Ogt ⇒ translate_cmp Cgt ty1 ty2 ty e1 e2
| Ole ⇒ translate_cmp Cle ty1 ty2 ty e1 e2
| Oge ⇒ translate_cmp Cge ty1 ty2 ty e1 e2
].

lemma typ_equals : ∀t1,t2. ∀P:∀t. expr t → Prop. ∀v1,v2.
  typ_should_eq t1 t2 expr v1 = OK ? v2 →
  P t1 v1 →
  P t2 v2.
#t1 #t2 #P #v1 #v2
whd in ⊢ (??%? → ?); cases (typ_eq t1 t2)
[ #E destruct #E whd in E:(??%?); destruct //
| #NE #E normalize in E; destruct
] qed.

lemma unfix_ptr_type : ∀ty,n,e.∀P:∀t. expr t → Prop.
  P (typ_of_type (ptr_type ty n)) e →
  P ASTptr (fix_ptr_type ty n e).
#ty * [ 2: #n ] #e #P #H @H
qed.

(* Recall that [expr_vars], defined in Cminor/Syntax.ma, asserts a predicate on 
  all the variables of a program. [translate_binop_vars], given
  a predicate verified for all variables of subexprs e1 and e2, produces
  a proof that all variables of [translate_binop op _ e1 _ e2 _] satisfy this
  predicate. *)

lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e.
  expr_vars ? e1 P →
  expr_vars ? e2 P →
  translate_binop op ty1 e1 ty2 e2 ty = OK ? e →
  expr_vars ? e P.
#P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
whd in ⊢ (??%? → ?);
[ inversion (classify_add ty1 ty2) in ⊢ ?;
  [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4 -E3 change with (typ_should_eq ???? = OK ??) in E4;
    @(typ_equals … E4) % //
(*  | #sz #E1 #E2 #E3 destruct >E3 #E4
    @(typ_equals … E4) % // *)
  | #n #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
    @(typ_equals … E4) -E4 -E3 % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)| % // ]
  | #n #sz #sg #ty0 #E1 #E2 #E3 destruct >E3 #E4
    @(typ_equals … E4) % [ 2: @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2) | 1: % // ]
  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
  ]
  
| inversion (classify_sub ty1 ty2) in ⊢ ?;
  [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4
    @(typ_equals … E4) % //
(*  | #sz #E1 #E2 #E3 destruct >E3 #E4
    @(typ_equals … E4) % // *)
  | #n #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
    @(typ_equals … E4) % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)| % // ]
  | #n1 #n2 #ty1' #ty2' #E1 #E2 #E3 destruct >E3
    whd in ⊢ (??%? → ?); cases ty in e ⊢ %;
    [ 2: #sz #sg #e #E4 | 3: #ty #e #E4 | 4: #ty' #n' #e #E4
    | *: normalize #X1 #X2 try #X3 try #X4 destruct
    ] whd in E4:(??%?); destruct % // %
    [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1) | @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2) ]
  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
  ]
| 3,4,5,6,7,8,9,10: inversion (classify_aop ty1 ty2) in ⊢ ?;
  (* Note that some cases require a split on signedness of integer type. *)
  [ 1,3,5,7,9,11,13,15: #sz * #E1 #E2 #E3 destruct >E3 #E4
    @(typ_equals … E4) % //
  | 2,4,6,8,10,12,14,16,18: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
  ]
| *: inversion (classify_cmp ty1 ty2) in ⊢ ?;
  [ 1,4,7,10,13,16: #sz * #E1 #E2 #E3 destruct >E3
  | 2,5,8,11,14,17: #n #ty' #E1 #E2 #E3 destruct >E3
  | *: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); @⊥ destruct
  ] whd in ⊢ (??%? → ?); cases ty in e ⊢ %; normalize nodelta
  try (normalize #X1 #X2 try #X3 try #X4 try #X5 destruct #FAIL)
  #sz #sg #e #E4
  whd in E4:(??%?); destruct % try @H1 try @H2
  try  @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)
  try  @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2)
] qed.  

(* We'll need to implement proper translation of pointers if we really do memory
   spaces. 
(* This function performs leibniz-style subst if r1 = r2, and fails otherwise. *)
definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝
λr1,r2,P.
  match r1 return λx.P x → res (P r2) with
  [ Any ⇒   match r2 return λx.P Any → res (P x) with [ Any ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
  | Data ⇒  match r2 return λx.P Data → res (P x) with [ Data ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
  | IData ⇒ match r2 return λx.P IData → res (P x) with [ IData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
  | PData ⇒ match r2 return λx.P PData → res (P x) with [ PData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
  | XData ⇒ match r2 return λx.P XData → res (P x) with [ XData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
  | Code ⇒  match r2 return λx.P Code → res (P x) with [ Code ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
  ].

(* Simple application of [check_region] to translate between terms. *)
definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝
λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
*)
axiom FIXME : String.

(* Given a source and target type, translate an expession of type source to type target *)
definition 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) ≝
λP,ty1,ty2.
match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with
[ Tint sz1 sg1 ⇒ λe.
    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint ? sg1 sz2 ?) e)
  (*  | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu ?? | _ ⇒ Ofloatofint ??]) e)*)
    | Tpointer _ ⇒ OK ? (Op1 ?? (Optrofint ??) e)
    | Tarray _ _ ⇒ OK ? (Op1 ?? (Optrofint ??) e)
    | _ ⇒ Error ? (msg TypeMismatch)
    ]
(* | Tfloat sz1 ⇒ λe.
    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat ? sz2 | _ ⇒ Ointoffloat ? sz2 ]) e, ?»
    | Tfloat sz2 ⇒ Error ? (msg FIXME) (* OK ? «Op1 ?? (Oid ?) e, ?» (* FIXME *) *)
    | _ ⇒ Error ? (msg TypeMismatch)
    ] *)
| Tpointer _ ⇒ λe. (* will need changed for memory regions *)
    match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with
    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2 ?) e, ?»
    | Tarray _ _ ⇒ (*translate_ptr ? r1 r2 e*) OK ? e
    | Tpointer _ ⇒ OK ? e
    | _ ⇒ Error ? (msg TypeMismatch)
    ]
| Tarray _ _ ⇒ λe. (* will need changed for memory regions *)
    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
    [ Tint sz2 sg2 ⇒ OK ? «Op1 ASTptr (ASTint sz2 sg2) (Ointofptr sz2 ?) e, ?»
    | Tarray _ _ ⇒ OK ? e
    | Tpointer _ ⇒ OK ? e
    | _ ⇒ Error ? (msg TypeMismatch)
    ]
| _ ⇒ λ_. Error ? (msg TypeMismatch)
]. whd normalize nodelta @pi2 
qed.

definition cm_zero ≝ λsz,sg. Cst ? (Ointconst sz sg (zero ?)).
definition cm_one  ≝ λsz,sg. Cst ? (Ointconst sz sg (repr sz 1)).

(* Translate Clight exprs into Cminor ones.
  Arguments :
  - vars:var_types, an environment mapping each variable to a couple (allocation mode, type)
  - e:expr, the expression to be converted
  Result : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars))
  that is, either
  . an error
  . an expression e', matching the type of e, such that e' respect the property that all variables
    in it are not global. In effect, [translate_expr] will replace global variables by constant symbols.
*)
let rec translate_expr (vars:var_types) (e:expr) on e : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) ≝
match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with
[ Expr ed ty ⇒
  match ed with
  [ Econst_int sz i ⇒
      match ty return λty. res (Σe':CMexpr (typ_of_type ty).  expr_vars ? e' (local_id vars)) with
      [ 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)))
                        (OK ? «Cst ? (Ointconst sz sg i), ?»)
                        (Error ? (msg TypeMismatch))
      | _ ⇒ Error ? (msg TypeMismatch)
      ]
 (* | Econst_float f ⇒
      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
      [ Tfloat sz ⇒ OK ? «Cst ? (Ofloatconst sz f), ?»
      | _ ⇒ Error ? (msg TypeMismatch)
      ] *)
  | Evar id ⇒
      (* E is an equality proof of the shape "lookup' vars id = Ok <c,t>" *)  
      do 〈c,t〉 as E ← lookup' vars id;
      match c return λx. (c = x) → res (Σe':CMexpr ?. ?) with
      [ Global r ⇒ λHeq_c.
          (* We are accessing a global variable in an expression. Its Cminor counterpart also depends on
             its access mode:
             - By_value q, where q is a memory chunk specification (whitch should match the type of the global)
             - By_reference, and we only take the adress of the variable
             - By_nothing : error 
           *)
          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
          [ By_value t ⇒ OK ? «Mem t (Cst ? (Oaddrsymbol id 0)), ?» (* Mem is "load" in compcert *)
          | By_reference ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
          ]
      | Stack n ⇒ λHeq_c.
          (* We have decided that the variable should be allocated on the stack, 
           * because its adress was taken somewhere or becauste it's a structured data. *)
          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
          [ By_value t ⇒ OK ? «Mem t (Cst ? (Oaddrstack n)), ?»
          | By_reference ⇒ (*match r return λr. res (Σe':CMexpr (ASTptr r). ?) with
                             [ Any ⇒*) OK ? «Cst ? (Oaddrstack n), ?» (*
                             | _ ⇒ Error  ? [MSG BadlyTypedAccess; CTX ? id]
                             ]*)
          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
          ]
          (* 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. *)
      | Local ⇒ λHeq_c. type_should_eq t ty (λt.Σe':CMexpr (typ_of_type t).expr_vars (typ_of_type t) e' (local_id vars))  («Id (typ_of_type t) id, ?»)
      ] (refl ? c)
  | Ederef e1 ⇒
      do e1' ← translate_expr vars e1;
      (* According to the way the data pointed to by e1 is accessed, the generated Cminor code will vary.
        - if e1 is a kind of int* ptr, then we load ("Mem") the ptr returned by e1
        - if e1 is a struct* or a function ptr, then we acess by reference, in which case we :
           1) check the consistency of the regions in the type of e1 and in the access mode of its type
           2) return directly the converted CMinor expression "as is" (TODO : what is the strange notation with the ceil function and the mapsto ?)
      *)
      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
      [ ASTptr ⇒ λe1'.
          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
          [ By_value t ⇒ OK ? «Mem t (pi1 … e1'), ?»
          | By_reference ⇒ OK ? e1'
          | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
          ]
      | _ ⇒ λ_. Error ? (msg TypeMismatch)
      ] e1'              
  | Eaddrof e1 ⇒
      do e1' ← translate_addr vars e1;
      match typ_of_type ty return λx.res (Σz:CMexpr x.?) with 
      [ ASTptr ⇒ OK ? e1'
(*          match e1' with
          [ mk_DPair r1 e1' ⇒ region_should_eq r1 r ? e1'
          ]*)
      | _ ⇒ Error ? (msg TypeMismatch)
      ]
  | Eunop op e1 ⇒
     match op
      return λx. (op = x) → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars))
      with
      [ Onotbool ⇒ λHop.
        match typ_of_type ty 
        return λy. (typ_of_type ty = y) → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars))
        with
        [ ASTint sz sg ⇒  λHtyp_of_type.
          match sz
          return λz. (sz = z) → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars))
          with
          [ I32 ⇒ λHsz.
            do op' ← translate_unop (typ_of_type (typeof e1)) (typ_of_type ty) op;
            do e1' ← translate_expr vars e1;
            OK ? «Op1 ?? op' e1', ?»
          | _ ⇒ λHsz.
            Error ? (msg TypeMismatch)
          ] (refl ? sz)
        | _ ⇒ λHtyp_of_type.
          Error ? (msg TypeMismatch)
        ] (refl ? (typ_of_type ty))        
      | _ ⇒ λHop.
        do op' ← translate_unop (typ_of_type (typeof e1)) (typ_of_type ty) op;
        do e1' ← translate_expr vars e1;
        OK ? «Op1 ?? op' e1', ?»
      ] (refl ? op)
  | Ebinop op e1 e2 ⇒
      do e1' ← translate_expr vars e1;
      do e2' ← translate_expr vars e2;
      do e' as E ← translate_binop op (typeof e1) e1' (typeof e2) e2' ty;
      OK ? «e', ?»
  | Ecast ty1 e1 ⇒
      do e1' ← translate_expr vars e1;
      do e' ← translate_cast ? (typeof e1) ty1 e1';
      do e' ← typ_should_eq (typ_of_type ty1) (typ_of_type ty) ? e';
      OK ? e'
  | Econdition e1 e2 e3 ⇒
      do e1' ← translate_expr vars e1;
      do e2' ← translate_expr vars e2;
      do e2' ← typ_should_eq (typ_of_type (typeof e2)) (typ_of_type ty) ? e2';
      do e3' ← translate_expr vars e3;
      do e3' ← typ_should_eq (typ_of_type (typeof e3)) (typ_of_type ty) ? e3';
      match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → res ? with
      [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' e3', ?»
      | _ ⇒ λ_.Error ? (msg TypeMismatch)
      ] e1'
  | Eandbool e1 e2 ⇒
      do e1' ← translate_expr vars e1;
      do e2' ← translate_expr vars e2;
      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
      [ Tint sz sg ⇒
          do e2' ← type_should_eq ? (Tint sz sg) (λx.Σe:CMexpr (typ_of_type x).?) e2';
          match typ_of_type (typeof e1) 
          return λx.
            (Σe:CMexpr x. expr_vars ? e (local_id vars)) → (res ?) 
          with
          [ ASTint sz1 _ ⇒ λe1'.
            (* Producing a nested comparison to match CL. *)
            OK ? «Cond ??? e1' (Cond ??? e2' (cm_one sz sg) (cm_zero sz sg)) (cm_zero sz sg), ?»
          | _ ⇒ λ_. Error ? (msg TypeMismatch)
          ] e1'
      | _ ⇒ Error ? (msg TypeMismatch)
      ]
  | Eorbool e1 e2 ⇒
      do e1' ← translate_expr vars e1;
      do e2' ← translate_expr vars e2;
      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
      [ Tint sz sg ⇒
        do e2' ← type_should_eq ? (Tint sz sg) (λx.Σe:CMexpr (typ_of_type x).?) e2';
        match typ_of_type (typeof e1) 
        return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with
        [ ASTint _ _ ⇒ λe1'.
          OK ? «Cond ??? e1' (cm_one sz sg) (Cond ??? e2' (cm_one sz sg) (cm_zero sz sg)), ?»
        | _ ⇒ λ_. Error ? (msg TypeMismatch)
        ] e1'
      | _ ⇒ Error ? (msg TypeMismatch)
      ]      
  | Esizeof ty1 ⇒
      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
      [ Tint sz sg ⇒ OK ? «Cst ? (Ointconst sz sg (repr ? (sizeof ty1))), ?»
      | _ ⇒ Error ? (msg TypeMismatch)
      ]      
  | Efield e1 id ⇒
      match typeof e1 with
      [ Tstruct _ fl ⇒
          do e1' ← translate_addr vars e1;
(*          match e1' with
          [ mk_DPair r e1' ⇒*)
            do off ← field_offset id fl;
            match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
            [ By_value t ⇒
                OK ? «Mem t (Op2 ? (ASTint I16 Signed (* XXX efficiency? *)) ?
                                   (Oaddpi …) e1' (Cst ? (Ointconst I16 Signed (repr ? off)))),?»
            | By_reference ⇒
(*                do e1' ← region_should_eq r r' ? e1';*)
                OK ? «Op2 ASTptr (ASTint I16 Signed (* XXX efficiency? *)) ASTptr
                        (Oaddpi …) e1' (Cst ? (Ointconst I16 Signed (repr ? off))),?»
            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
            ]
      | Tunion _ _ ⇒
          do e1' ← translate_addr vars e1;
            match access_mode ty return λt.λ_. res (Σz:CMexpr t.?) with
            [ By_value t ⇒ OK ? «Mem t e1', ?»
            | By_reference ⇒ OK ? e1'
            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
            ]
      | _ ⇒ Error ? (msg BadlyTypedAccess)
      ]            
  | Ecost l e1 ⇒
      do e1' ← translate_expr vars e1;
      do e' ← OK ? «Ecost ? l e1',?»;
      typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e'      
  ]
] 

(* Translate addr takes an expression e1, and returns a Cminor code computing the address of the result of [e1].   *)
and translate_addr (vars:var_types) (e:expr) on e : res ((*𝚺r.*) Σe':CMexpr ASTptr. expr_vars ? e' (local_id vars)) ≝
match e with
[ Expr ed _ ⇒
  match ed with
  [ Evar id ⇒
      do 〈c,t〉 ← lookup' vars id;
      match c return λ_. res (Σz:CMexpr ASTptr.?) with
      [ Global r ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
      | Stack n ⇒ OK ? «Cst ? (Oaddrstack n), ?»
      | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *)
      ]
  | Ederef e1 ⇒
      do e1' ← translate_expr vars e1;
      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
      [ ASTptr ⇒ λe1'.OK ? e1'
      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
      ] e1'
  | Efield e1 id ⇒
      match typeof e1 with
      [ Tstruct _ fl ⇒
          do e1' ← translate_addr vars e1;
          do off ← field_offset id fl;
(*          match e1' with
          [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?)*)
             OK ? «Op2 ASTptr (ASTint I16 Signed (* FIXME inefficient?*)) ASTptr
                   (Oaddpi I16) e1' (Cst ? (Ointconst I16 Signed (repr ? off))), ?»
      | Tunion _ _ ⇒ translate_addr vars e1
      | _ ⇒ Error ? (msg BadlyTypedAccess)
      ]
  | _ ⇒ Error ? (msg BadLvalue)
  ]
].
whd try @I
[ >E whd >Heq_c @refl
| 2,3: @pi2
| cases e1' //
| cases e1' //
| @(translate_binop_vars … E) @pi2
| % [ % ] @pi2
| % [ % try @pi2 whd @conj try @conj try // @pi2 ] whd @I
| % [ % [ @pi2 | @I ] | % try @conj try // @pi2 ]
| % [ @pi2 | @I ]
| % [ @pi2 | @I ]
| @pi2
| @pi2
| % [ @pi2 | @I ]
] qed.

(* We provide a function to work out how to do an assignment to an lvalue
   expression.  It is used for both Clight assignments and Clight function call
   destinations, but doesn't take the value to be assigned so that we can use
   it to form a single St_store when possible (and avoid introducing an
   unnecessary temporary variable and assignment).
   *)
inductive destination (vars:var_types) : Type[0] ≝
| IdDest : ∀id,ty. local_id vars id (typ_of_type ty) → destination vars
| MemDest : (Σe:CMexpr ASTptr.expr_vars ? e (local_id vars)) → destination vars.

(* Let a source Clight expression be assign(e1, e2). First of all, observe that [e1] is a
  /Clight/ expression, not converted by translate_expr. We thus have to do part of the work
  of [translate_expr] in this function. [translate_dest] will convert e1
   into a proper destination for an assignement operation. We proceed by case analysis on e1.
   - if e1 is a variable [id], then we proceed by case analysis on its allocation mode:
      - if [id] is allocated locally (in a register), then id becomes directly
        the target for the assignement, as (IdDest vars id t H), where t is the type
        of id, and H asserts that id is indeed a local variable.
      - if [id] is a global variable stored in region [r], then we perform [translate_expr]'s 
        job and return an adress, given as a constant symbol corresponding to [id], with
        region r and memory chunk specified by the access mode of the rhs type ty2 of [e2].
      - same thing for stack-allocated variables, except that we don't specify any region.
   - if e1 is not a variable, we use [translate_addr] to generate a Cminor expression computing
    the adres of e1
*)
definition translate_dest ≝
λvars,e1.
  match e1 with
  [ Expr ed1 ty1 ⇒
      match ed1 with
      [ Evar id ⇒
          do 〈c,t〉 as E ← lookup' vars id;
          match c return λx.? → ? with
          [ Local ⇒ λE. OK ? (IdDest vars id t ?)
          | Global r ⇒ λE. OK ? (MemDest ? (Cst ? (Oaddrsymbol id 0)))
          | Stack n ⇒ λE. OK ? (MemDest ? (Cst ? (Oaddrstack n)))
          ] E
      | _ ⇒
          do e1' ← translate_addr vars e1;
          OK ? (MemDest ? e1')
      ]
  ].
whd // >E @refl
qed.

(* [lenv] is the type of maps from Clight labels to Cminor labels. *)
definition lenv ≝ identifier_map SymbolTag (identifier Label).

axiom MissingLabel : String.

(* Find the Cminor label corresponding to [l] or fail. *)
definition lookup_label ≝
λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).

(* True iff the Cminor label [l] is in the codomain of [lbls] *)
definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup_label lbls l' = OK ? l.

(* True iff The Clight label [l] is in the domain of [lbls] *)
definition label_in_domain ≝ λlbls:lenv. λl. present ?? lbls l.

let rec fresh_list_for_univ (l:list (identifier Label)) (u:universe Label) ≝
match l with
[ nil ⇒ True
| cons elt tl ⇒ fresh_for_univ ? elt u ∧ fresh_list_for_univ tl u].

record labgen : Type[0] ≝ {
  labuniverse   : universe Label;
  label_genlist    : list (identifier Label);
  genlist_is_fresh : fresh_list_for_univ label_genlist labuniverse
}.

lemma 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'.
#l elim l
[ 1: normalize // 
| 2: #hd #tl #Hind #tmp #u #u' #HA #HB
  whd
  @conj
  [ 1: whd in HA ⊢ ?;
    elim HA #HAleft #HAright
    @(fresh_remains_fresh ? hd tmp u u') assumption
  | 2: whd in HA ⊢ ?;
    elim HA #HAleft #HAright    
    @Hind //
  ]
]
qed. 

definition In ≝ λelttype.λelt.λl.Exists elttype (λx.x=elt) l.   

definition generate_fresh_label :
 ∀ul. Σlul:(identifier Label × labgen).
               (And (∀lab. In ? lab (label_genlist ul) → In ? lab (label_genlist (snd … lul)))
                   (In ? (fst … lul) (label_genlist (snd … lul)))) ≝
λul.
let 〈tmp,u〉 as E ≝ fresh ? (labuniverse ul) in
 «〈tmp, mk_labgen u (tmp::(label_genlist ul)) ?〉, ?».
[ 1: normalize @conj 
  [ 1: @(fresh_is_fresh ? tmp u (labuniverse ul) ?) assumption
  | 2: @fresh_list_stays_fresh // ]
| @conj /2/
]
qed.

let rec labels_defined (s:statement) : list ident ≝
match s with
[ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2
| Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2
| Swhile _ s ⇒ labels_defined s
| Sdowhile _ s ⇒ labels_defined s
| Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
| Sswitch _ ls ⇒ labels_defined_switch ls
| Slabel l s ⇒ l::(labels_defined s)
| Scost _ s ⇒ labels_defined s
| _ ⇒ [ ]
]
and labels_defined_switch (ls:labeled_statements) : list ident ≝
match ls with
[ LSdefault s ⇒ labels_defined s
| LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls
].

definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s).

(* For each label l in s, there exists a matching label l' = lenv(l) defined in s' *)
definition labels_translated : lenv → statement → stmt → Prop ≝
λlbls,s,s'.  ∀l.
  (Exists ? (λl'.l' = l) (labels_defined s)) →
  ∃l'. lookup_label lbls l = (OK ? l') ∧ ldefined s' l'.


(* Invariant on statements, holds during conversion to Cminor *)
definition stmt_inv ≝  λvars. stmt_P (stmt_vars (local_id vars)).

definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝
λA,B,f,oa.
match oa with
[ None ⇒ OK ? (None ?)
| Some a ⇒ do b ← f a; OK ? (Some ? b)
].

definition 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) ]) ≝
λv,e.
  do e' ← translate_expr v e;
  OK (Σe:(𝚺t:typ.CMexpr t).?) «❬?, e'❭, ?».
whd @pi2
qed.

(* Add the list of typed variables tmpenv to the environment [var_types] with
   the allocation mode Local. *)
definition add_tmps : var_types → list (ident × type) → var_types ≝
λvs,tmpenv.
  foldr ?? (λidty,vs. add ?? vs (\fst idty) 〈Local, \snd idty〉) vs tmpenv.

record tmpgen (vars:var_types) : Type[0] ≝ {
  tmp_universe : universe SymbolTag;
  tmp_env : list (ident × type);
  tmp_ok : fresh_map_for_univ … (add_tmps vars tmp_env) tmp_universe;
  tmp_preserved :
    ∀id,ty. local_id vars id ty → local_id (add_tmps vars tmp_env) id ty
}.

definition alloc_tmp : ∀vars. type → tmpgen vars → ident × (tmpgen vars) ≝
λvars,ty,g.
  let 〈tmp,u〉 as E ≝ fresh ? (tmp_universe ? g) in
  〈tmp, mk_tmpgen ? u (〈tmp, ty〉::(tmp_env ? g)) ??〉.
[ #id #ty'
  whd in ⊢ (? → ?%??);
  whd in ⊢ (% → %);
  whd in ⊢ (? → match % with [_ ⇒ ? | _ ⇒ ?]); #H
  >lookup_add_miss
  [ @(tmp_preserved … g) @H
  | @(fresh_distinct … E) @(tmp_ok … g)
    lapply (tmp_preserved … g id ty' H)
    whd in ⊢ (% → %);
    whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?);
    cases (lookup ??? id)
    [ * | #x #_ % #E destruct ]
  ]
| @fresh_map_add
  [ @(fresh_map_preserved … E) @(tmp_ok … g)
  | @(fresh_is_fresh … E)
  ]
] qed.


lemma lookup_label_hit : ∀lbls,l,l'.
  lookup_label lbls l = OK ? l' →
  lpresent lbls l'.
#lbls #l #l' #E whd %{l} @E
qed.

(* TODO: is this really needed now? *)

definition tmps_preserved : ∀vars:var_types. tmpgen vars → tmpgen vars → Prop ≝
λvars,u1,u2.
  ∀id,ty. local_id (add_tmps vars (tmp_env … u1)) id ty → local_id (add_tmps vars (tmp_env … u2)) id ty.

lemma alloc_tmp_preserves : ∀vars,tmp,u,u',q.
  〈tmp,u'〉 = alloc_tmp ? q u → tmps_preserved vars u u'.
#vars #tmp * #u1 #e1 #F1 #P1 * #u2 #e2 #F2 #P2 #q
whd in ⊢ (???% → ?); generalize in ⊢ (???(?%) → ?);
cases (fresh SymbolTag u1) in ⊢ (??%? → ???(match % with [ _ ⇒ ? ]?) → ?);
#tmp' #u' #E1 #E2 whd in E2:(???%); destruct
#id #ty #H whd in ⊢ (?%??); whd in H ⊢ %;
whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ];
>lookup_add_miss // @(fresh_distinct … E1) @F1
whd in H:(match % with [_ ⇒ ?|_ ⇒ ?]) ⊢ %;
cases (lookup ??? id) in H ⊢ %;
[ * | #x #_ % #E destruct ]
qed.

lemma add_tmps_oblivious : ∀vars,s,u.
  stmt_inv vars s → stmt_inv (add_tmps vars (tmp_env vars u)) s.
#vars #s #u #H
@(stmt_P_mp … H)
#s' #H1 @(stmt_vars_mp … H1) #id #t #H @(tmp_preserved ? u ?? H)
qed.

lemma local_id_fresh_tmp : ∀vars,tmp,u,ty,u0.
  〈tmp,u〉 = alloc_tmp vars ty u0 → local_id (add_tmps vars (tmp_env … u)) tmp (typ_of_type ty).
#vars #tmp #u #ty #u0
whd in ⊢ (???% → ?); generalize in ⊢ (???(?%) → ?);
cases (fresh SymbolTag (tmp_universe vars u0)) in ⊢ (??%? → ???(match % with [_⇒?]?) → ?);
* #tmp' #u' #e #E whd in E:(???%);
destruct
whd in ⊢ (?%??); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit
@refl
qed.


let rec mklabels (ul:labgen) : (identifier Label) × (identifier Label) × labgen ≝
  match generate_fresh_label ul with
  [ mk_Sig res1 H1 ⇒
     let 〈entry_label, ul1〉 as E1 ≝ res1 in
     match generate_fresh_label ul1 with
     [ mk_Sig res2 H2 ⇒
        let 〈exit_label, ul2〉 as E2 ≝ res2 in
        〈entry_label, exit_label, ul2〉
     ]
  ].

(* When converting loops into gotos, and in order to eliminate blocks, we have
 * to convert continues and breaks into goto's, too. We add some "flags" in
 * in argument to [translate_statement], meaning that the next encountered break
 * or continue has to be converted into a goto to some contained label. 
 * ConvertTo l1 l2 means "convert continue to goto l1 and convert break to goto l2".
 *)
inductive convert_flag : Type[0] ≝
| DoNotConvert : convert_flag
| ConvertTo    : identifier Label → identifier Label → convert_flag. (* continue, break *)

let rec labels_of_flag (flag : convert_flag) : list (identifier Label) ≝
match flag with
[ DoNotConvert ⇒ [ ]
| ConvertTo continue break ⇒ continue :: break :: [ ]
].

(* For a top-level expression, [label-wf] collapses to "all labels are properly declared" *)
definition label_wf ≝
λ (s : statement) .λ (s' : stmt) .λ (lbls : lenv). λ (flag : convert_flag).
    stmt_P (λs1. stmt_labels (λl.ldefined s' l ∨ lpresent lbls l ∨ In ? l (labels_of_flag flag)) s1) s'.

definition return_ok : option typ → stmt → Prop ≝
λot.
stmt_P (λs.
  match s with [ St_return oe ⇒
    match oe with [ Some e ⇒ Some ? (dpi1 … e) = ot | None ⇒ None ? = ot ]
  | _ ⇒ True ]).

(* trans_inv is the invariant which is enforced during the translation from Clight to Cminor.
  The involved arguments are the following:
  . vars:var_types, an environment mapping variables to their types and allocation modes
  . lbls:lenv, a mapping from old (Clight) to fresh and new (Cminor) labels,
  . s:statement, a Clight statement,
  . uv, a fresh variable generator (containing itself some invariants)
  . flag, wich maps "break" and "continue" to "gotos"
  . su', a couple of a Cminor statement and fresh variable generator.
*)
definition trans_inv : ∀vars:var_types . ∀lbls:lenv . statement → tmpgen vars → convert_flag → option typ → ((tmpgen vars) × labgen × stmt) → Prop ≝
λvars,lbls,s,uv,flag,rettyp,su'. 
  let 〈uv', ul', s'〉 ≝ su' in
  stmt_inv (add_tmps vars (tmp_env … uv')) s' ∧   (* remaining variables in s' are local*)
  labels_translated lbls s s' ∧                   (* all the labels in s are transformed in label of s' using [lbls] as a map *)
  tmps_preserved vars uv uv' ∧                    (* the variables generated are local and grows in a monotonic fashion *)
  return_ok rettyp s' ∧                           (* return statements have correct typ *)
  label_wf s s' lbls flag.                        (* labels are "properly" declared, as defined in [ŀabel_wf].*) 

axiom ReturnMismatch : String.

let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (rettyp:option typ) (s:statement) on s 
  : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) ≝
match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) with
[ Sskip ⇒ OK ? «〈uv, ul, St_skip〉, ?»
| Sassign e1 e2 ⇒
    do e2' ← translate_expr vars e2;  (* rhs *)
    do dest ← translate_dest vars e1; (* e1 *)
    match dest with
    [ IdDest id ty p ⇒
       (* Don't compare the Clight types, or we'll have to deal with
          array/pointer punning. *)
       do e2' ← typ_should_eq (typ_of_type (typeof e2)) (typ_of_type ty) ? e2';
       OK ? «〈uv, ul, St_assign ? id e2'〉, ?»
    | MemDest e1' ⇒ 
       OK ? «〈uv, ul, St_store ? e1' e2'〉, ?»
    ]
| Scall ret ef args ⇒
    do ef' ← translate_expr vars ef;
    do ef' ← typ_should_eq (typ_of_type (typeof ef)) ASTptr ? ef';
    do args' ← mmap_sigma ??? (translate_expr_sigma vars) args;
    match ret with
    [ None ⇒ OK ? «〈uv, ul, St_call (None ?) ef' args'〉, ?»
    | Some e1 ⇒
        do dest ← translate_dest vars e1;
        match dest with
        [ IdDest id ty p ⇒ OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?»
        | MemDest e1' ⇒
            let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in
            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))〉, ?»
        ]
    ]
| Ssequence s1 s2 ⇒
    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
    do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag rettyp s2;
    OK ? «〈fgens2, St_seq s1' s2'〉, ?»
| Sifthenelse e1 s1 s2 ⇒
    do e1' ← translate_expr vars e1;
    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → res ? with
    [ ASTint _ _ ⇒ λe1'.
         do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
         do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag rettyp s2;
        OK ? «〈fgens2, St_ifthenelse ?? e1' s1' s2'〉, ?»
    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    ] e1'
(* Performing loop conversions while keeping good cost labelling properties is
   a little tricky.  In principle we should have a cost label in each branch,
   but the behaviour of the next stage means that we can put in Cminor skips and
   goto labels before the cost label. *)
| Swhile e1 s1 ⇒
    do e1' ← translate_expr vars e1;
    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → res ? with
    [ ASTint _ _ ⇒ λe1'.         
        let 〈labels, ul1〉 as E1 ≝ mklabels ul in
        let 〈entry, exit〉 as E2 ≝ labels in
        do «fgens2, s1',H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) rettyp s1;
        let converted_loop ≝
          St_label entry
          (St_seq
            (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) St_skip)
            (St_label exit St_skip))
        in         
          OK ? «〈fgens2, converted_loop〉, ?»
    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    ] e1'
| Sdowhile e1 s1 ⇒
    do e1' ← translate_expr vars e1;
    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → res ? with
    [ ASTint _ _ ⇒ λe1'.
        let 〈labels, ul1〉 as E1 ≝ mklabels ul in
        let 〈condexpr, exit〉 as E2 ≝ labels in
        let 〈body, ul2〉 ≝ generate_fresh_label … ul1 in
        do «fgens2, s1', H1» ← translate_statement vars uv ul2 lbls (ConvertTo condexpr exit) rettyp s1;
        (* This is particularly carefully implemented, we need to reach the
           cost label in s1' or the cost label after the loop (if they are
           present) after the ifthenelse, and we're only allowed skips and
           goto labels in between.  So we structure it like a while with a goto
           into the middle (the CFG will be essentially the same, anyway.) *)
        let converted_loop ≝
        St_seq
          (St_seq
            (St_goto body)
            (St_label condexpr
              (St_ifthenelse ?? e1'
                (St_label body
                  (St_seq
                    s1'
                    (St_goto condexpr)))
                St_skip)))
          (St_label exit St_skip)
        in
        OK ? «〈fgens2, converted_loop〉, ?»
    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    ] e1'
| Sfor s1 e1 s2 s3 ⇒
    do e1' ← translate_expr vars e1;
    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → res ? with
    [ ASTint _ _ ⇒ λe1'.
        let 〈labels, ul1〉 as E ≝ mklabels ul in
        let 〈continue, exit〉 as E2 ≝ labels in
        let 〈entry, ul2〉 ≝ generate_fresh_label … ul1 in
        do «fgens2, s1', H1» ← translate_statement vars uv ul2 lbls flag rettyp s1;
        (* The choice of flag is arbitrary - Clight's semantics give no meaning
           to continue or break in s2 because in C it must be an expression. *)
        do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) lbls flag rettyp s2;
        do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) lbls (ConvertTo continue exit) rettyp s3;
        let converted_loop ≝
          St_seq
            s1'
            (St_label entry
              (St_seq
                (St_ifthenelse ?? e1' (St_seq s3' (St_label continue (St_seq s2' (St_goto entry)))) St_skip)
                (St_label exit St_skip)
            ))
        in 
          OK ? «〈fgens4, converted_loop〉, ?»
    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    ] e1'
| Sbreak ⇒
   match flag return λf.flag = f → ? with
   [ DoNotConvert ⇒ λEflag.
     Error ? (msg FIXME) 
   | ConvertTo continue_label break_label ⇒ λEflag.
     OK ? «〈uv, ul, St_goto break_label〉, ?» 
   ] (refl ? flag)
| Scontinue ⇒ 
  match flag return λf.flag = f → ? with
  [ DoNotConvert ⇒ λEflag.
    Error ? (msg FIXME) 
  | ConvertTo continue_label break_label ⇒ λEflag.
    OK ? «〈uv, ul, St_goto continue_label〉, ?»
  ] (refl ? flag) 
| Sreturn ret ⇒
    match ret with
    [ None ⇒ 
        match rettyp return λx.res (Σy.trans_inv … x y) with
        [ None ⇒ OK ? «〈uv, ul, St_return (None ?)〉, ?»
        | _ ⇒ Error ? (msg ReturnMismatch)
        ]
    | Some e1 ⇒
        match rettyp return λx.res (Σy.trans_inv … x y) with
        [ Some rty ⇒
            do e1' ← translate_expr vars e1;
            do e1' ← typ_should_eq (typ_of_type (typeof e1)) rty ? e1';
            OK ? «〈uv, ul, St_return (Some ? (mk_DPair … e1'))〉, ?»
        | _ ⇒ Error ? (msg ReturnMismatch)
        ]
    ]
| Sswitch e1 ls ⇒ Error ? (msg FIXME)
| Slabel l s1 ⇒
    do l' as E ← lookup_label lbls l;
    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
    OK ? «〈fgens1, St_label l' s1'〉, ?»
| Sgoto l ⇒
    do l' as E ← lookup_label lbls l;
    OK ? «〈uv, ul, St_goto l'〉, ?»
| Scost l s1 ⇒
    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
    OK ? «〈fgens1, St_cost l s1'〉, ?»
].
try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
try (@I)
try (#l #H elim H)
try (#size #sign #H assumption)
try (#H1 try #H2 assumption)
[ 1,5: @(tmp_preserved … p) ]
[ 1,3: elim e2' | 2,9,23: elim e1' | 4,7,13: elim ef' ]
[ 1,2,3,4,5,6,7,8 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
[ 1: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
             | 3: elim args' // ] 
| 7: (* we should be able to merge this case with the previous ... *)
     @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
             | 3: elim args' // ]
| 2: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp)
| 3:  @(All_mp (𝚺 t:typ.expr t) (λe. match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars)]))
       [ 1: #a #Ha elim a in Ha ⊢ ?; #ta #a #Ha whd @(expr_vars_mp ?? (local_id vars))
       [ 1: #i0 #t0 #H0 @(tmp_preserved vars uv1 i0 t0 H0)
       | 2: assumption ]
       | 2: elim args' // ]
| 4: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) ]
[ 1: #size #sign | 2: ]
[ 1,2: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ]
try @refl (* Does (at least) the return_ok cases *)
try @(match fgens1 return λx.x=fgens1 → ? with
     [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1))
try @(match fgens2 return λx.x=fgens2 → ? with
     [ mk_Prod uv2 ul2 ⇒ λHfgens2.? ] (refl ? fgens2))
try @(match fgens3 return λx.x=fgens3 → ? with
     [ mk_Prod uv3 ul3 ⇒ λHfgens3.? ] (refl ? fgens3))
try @(match fgens4 return λx.x=fgens4 → ? with
     [ mk_Prod uv4 ul4 ⇒ λHfgens4.? ] (refl ? fgens4))
whd in H1 H2 H3 ⊢ ?; destruct whd nodelta in H1 H2 H3;
try (elim H1 -H1 * * * #Hstmt_inv1 #Hlabels_tr1 #Htmps_pres1 #Hret1)
try (elim H2 -H2 * * * #Hstmt_inv2 #Hlabels_tr2 #Htmps_pres2 #Hret2)
try (elim H3 -H3 * * * #Hstmt_inv3 #Hlabels_tr3 #Htmps_pres3 #Hret3)
[ 1,2: #Hind1 #Hind2 | 3,4,8,10: #Hind | 5: #Hind1 #Hind2 #Hind3 ]
try @conj try @conj try @conj try @conj try @conj try @conj try (whd @I) try assumption
[ 1,7: @(stmt_P_mp … Hstmt_inv1) #e #Hvars @(stmt_vars_mp … Hvars) #i #t #Hlocal @(Htmps_pres2 … Hlocal)
| 2: #l #H cases (Exists_append ???? H) #Hcase
         [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
           [ 1: @(proj1 ?? Hlabel)
           | 2: normalize @Exists_append_l @(proj2 … Hlabel) ]
         | 2: elim (Hlabels_tr2 l Hcase) #label #Hlabel @(ex_intro … label) @conj
           [ 1: @(proj1 ?? Hlabel)
           | 2: normalize @Exists_append_r @(proj2 … Hlabel) ]
         ]
| 3,9: #id #ty #H @(Htmps_pres2 … (Htmps_pres1 id ty H)) ]
[ 1: @(stmt_P_mp … Hind2) | 2: @(stmt_P_mp … Hind1) ]
[ 1,2: #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     #l * try * [ 1,4: #H %1 %1 normalize in H ⊢ %; try (@Exists_append_l @H); try (@Exists_append_r @H)
                | 2,5: #H %1 %2 assumption
                | 3,6: #H %2 assumption ]
(* if/then/else *)
| 3: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
| 4: whd #l #H
       cases (Exists_append ???? H) #Hcase
         [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
           [ 1: @(proj1 ?? Hlabel)
           | 2: normalize @Exists_append_l @(proj2 … Hlabel) ]
         | 2: elim (Hlabels_tr2 l Hcase) #label #Hlabel @(ex_intro … label) @conj
           [ 1: @(proj1 ?? Hlabel)
           | 2: normalize @Exists_append_r @(proj2 … Hlabel) ]
         ]
]                  
[ 1: 1: @(stmt_P_mp … Hind2) | 2: @(stmt_P_mp … Hind1) ]
[ 1,2: #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     #l * try * [ 1,4: #H %1 %1 normalize in H ⊢ %; try (@Exists_append_l @H); try (@Exists_append_r @H)
                | 2,5: #H %1 %2 assumption
                | 3,6: #H %2 assumption ] ]
try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I try assumption
[ 1,7,19: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
| 2,8: whd #l #H normalize in H;
       elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label)
       @conj
       [ 1,3: @(proj1 … Hlabel)
       | 2,4: whd @or_intror normalize in ⊢ (???%);
              [ @Exists_append_l @Exists_append_l @Exists_append_l | %2 @Exists_append_l @Exists_append_l @Exists_append_l ]
              @(proj2 … Hlabel) ]
| whd %1 %1 normalize /2/
| 4,12: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
   #l * try * [ 1,5: #H %1 %1 normalize %2 [ 2: %2 ] @Exists_append_l @Exists_append_l try @Exists_append_l @H
              | 2,6: #H %1 %2 assumption
              | 3,7: #H <H %1 %1 normalize /2/
              | 4,8: #H normalize in H; elim H [ 1,3: #E <E %1 %1 normalize %2 [2: %2]
                                                 @Exists_append_r normalize /2/
                                               | 2,4: * ]
              ]
| normalize %1 %1 %1 //
| 6,11: normalize %1 %1 %2 [ @Exists_append_r normalize /2/ | %1 % ] 
| whd %1 %1 normalize %2 %1 %
| 10,13: normalize %1 %1 %1 %
| normalize %1 %1 %2 %2 /2/
| whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
               | 2: #H elim (Hlabels_tr1 label H)
                    #lab * #Hlookup #Hdef @(ex_intro … lab) @conj
                    [ 1: // | 2: whd %2 assumption ]
               ]
| normalize %1 %1 %1 %
| @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
  #l * try * [ 1: #H %1 %1 normalize %2 @H
             | 2: #H %1 %2 assumption
             | 3: #H %2 assumption ]
| @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
  #H @(Htmps_pres3 … (Htmps_pres2 … H))
| @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
  #H @(Htmps_pres3 … H)
| % //
| whd #l #H normalize in H;
  cases (Exists_append … H) #Hcase
  [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
    [ 1: @(proj1 … Hlabel)
    | 2: normalize @Exists_append_l @(proj2 … Hlabel)
    ]
  | 2: cases (Exists_append … Hcase) #Hcase2
    [ 1: elim (Hlabels_tr2 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
      [ 1: @(proj1 … Hlabel)
      | 2: normalize >append_nil >append_nil >append_cons
           @Exists_append_r @Exists_append_l @Exists_append_r %2
           @(proj2 … Hlabel)
      ]
    | 2: elim (Hlabels_tr3 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
      [ 1: @(proj1 … Hlabel)
      | 2: normalize >append_nil >append_nil >append_cons
         @Exists_append_r @Exists_append_l @Exists_append_l
         @(proj2 … Hlabel)
      ]
    ]
  ]
| #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
| @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
   #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H
              | 2: #H %1 %2 assumption
              | 3: #H %2 assumption ]
| whd %1 %1 normalize /2/
| @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
                   @Exists_append_r @Exists_append_l @Exists_append_l 
                   @Exists_append_l assumption
              | 2: #H %1 %2 assumption
              | 3: #H <H %1 %1 normalize
                   @Exists_append_r %2 @Exists_append_l @Exists_append_l
                   @Exists_append_r %1 %
              | 4: * [ 1: #Eq <Eq %1 %1 whd normalize
                       @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r
                       @Exists_append_r whd %1 //
                     | 2: * ]
              ]
| % %1 normalize @Exists_append_r %2 @Exists_append_l @Exists_append_l
  @Exists_append_r % %
| @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
                   @Exists_append_r @Exists_append_l @Exists_append_l                    
                   @Exists_append_r %2 @Exists_append_l assumption
              | 2: #H %1 %2 assumption
              | 3: /2/
              ]
| whd %1 %1 normalize /2/
| whd %1 %1 normalize
  @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r 
  whd %1 //
| normalize %2 /3/
| normalize /4/
| whd %1 %2 whd @(ex_intro … l) @E
] qed.

axiom ParamGlobalMixup : String.

(* params and statement aren't real parameters, they're just there for giving the invariant. *)
definition alloc_params :
 ∀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) 
   → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag rettyp su) ≝   
λvars,lbls,statement,uv,ul,rettyp,params,s. foldl ?? (λsu,it.
  let 〈id,ty〉 ≝ it in
  do «result,Is» ← su;
  let 〈fgens1, s〉 as Eresult ≝ result in
  do 〈t,ty'〉 as E ← lookup' vars id;
  match t return λx.? → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv ul rettyp su) with
  [ Local ⇒ λE. OK (Σs:(tmpgen vars)×labgen×stmt.?) «result,Is»
  | Stack n ⇒ λE.
      OK ? «〈fgens1, St_seq (St_store ? (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?»
  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
  ] E) (OK ? s) params.
whd
@(match fgens1 return λx.x=fgens1 → ? with
  [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1))
whd in Is ⊢ %; destruct whd in Is;
try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I
elim Is * * * #Hincl #Hstmt_inv #Hlab_tr #Hret #Htmp_pr try assumption
@(expr_vars_mp … (tmp_preserved … uv1)) whd >E @refl
qed.

axiom DuplicateLabel : String.

definition lenv_list_inv : lenv → lenv → list ident → Prop ≝
λlbls0,lbls,ls.
 ∀l,l'. lookup_label lbls l = OK ? l' →
 Exists ? (λl'. l' = l) ls ∨ lookup_label lbls0 l = OK ? l'.

lemma lookup_label_add : ∀lbls,l,l'.
  lookup_label (add … lbls l l') l = OK ? l'.
#lbls #l #l' whd in ⊢ (??%?); >lookup_add_hit @refl
qed.

lemma lookup_label_miss : ∀lbls,l,l',l0.
  l0 ≠ l →
  lookup_label (add … lbls l l') l0 = lookup_label lbls l0.
#lbls #l #l' #l0 #NE
whd in ⊢ (??%%);
>lookup_add_miss
[ @refl | @NE ]
qed.

let rec populate_lenv (ls:list ident) (ul:labgen) (lbls:lenv): res ((Σlbls':lenv. lenv_list_inv lbls lbls' ls) × labgen) ≝
match ls return λls.res ((Σlbls':lenv. lenv_list_inv lbls lbls' ls) × labgen) with
[ nil ⇒ OK ? 〈«lbls, ?», ul〉
| cons l t ⇒
  match lookup_label lbls l return λlook. lookup_label lbls l = look → ? with
  [ OK _    ⇒ λ_.Error ? (msg DuplicateLabel)
  | Error _ ⇒ λLOOK.
    match generate_fresh_label … ul with
    [ mk_Sig ret H ⇒ 
       do 〈packed_lbls, ul1〉 ← populate_lenv t (snd ?? ret) (add … lbls l (fst ?? ret));
       match packed_lbls with
       [ mk_Sig lbls' Hinv ⇒ OK ? 〈«lbls', ?», ul1〉 ]
    ]
  ] (refl ? (lookup_label lbls l))
].
[ 1: whd #l #l' #Hlookup %2 assumption
| 2: whd in Hinv; whd #cl_lab #cm_lab #Hlookup
     @(eq_identifier_elim … l cl_lab)
     [ 1: #Heq %1 >Heq whd %1 //
     | 2: #Hneq cases (Hinv cl_lab cm_lab Hlookup)
           [ 1: #H %1 %2 @H
           | 2: #LOOK' %2 >lookup_label_miss in LOOK'; /2/ #H @H ]
     ]
]
qed.

definition build_label_env : 
   ∀body:statement. res ((Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) × labgen) ≝
λbody.
  let initial_labgen ≝ mk_labgen (new_universe ?) (nil ?) ?  in
  do 〈label_map, u〉 ← populate_lenv (labels_defined body) initial_labgen (empty_map ??);
  let lbls ≝ pi1 ?? label_map in
  let H    ≝ pi2 ?? label_map in
  OK ? 〈«lbls, ?», u〉.
[ 1: #l #l' #E cases (H l l' E) //
     whd in ⊢ (??%? → ?); #H destruct
| 2: whd @I ]
qed.

lemma local_id_split : ∀vars,tmpgen,i,t.
  local_id (add_tmps vars (tmp_env vars tmpgen)) i t →
  local_id vars i t ∨ Exists ? (λx. \fst x = i ∧ typ_of_type (\snd x) = t) (tmp_env … tmpgen).
#vars #tmpgen #i #t
whd in ⊢ (?%?? → ?);
elim (tmp_env vars tmpgen)
[ #H %1 @H
| * #id #ty #tl #IH
  cases (identifier_eq ? i id)
  [ #E >E #H %2 whd %1 % [ @refl | whd in H; whd in H:(match % with [_⇒?|_⇒?]); >lookup_add_hit in H; #E1 >E1 @refl ]
  | #NE #H cases (IH ?)
    [ #H' %1 @H'
    | #H' %2 %2 @H'
    | whd in H; whd in H:(match % with [ _ ⇒ ? | _ ⇒ ? ]);
      >lookup_add_miss in H; [ #H @H | @NE ]
    ]
  ]
] qed.

lemma Exists_squeeze : ∀A,P,l1,l2,l3.
  Exists A P (l1@l3) → Exists A P (l1@l2@l3).
#A #P #l1 #l2 #l3 #EX
cases (Exists_append … EX)
[ #EX1 @Exists_append_l @EX1
| #EX3 @Exists_append_r @Exists_append_r @EX3
] qed.

(* This lemma allows to merge two stmt_P in one. Used in the following parts to merge an invariant on variables
   and an invariant on labels. *)
lemma 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.
#P1 #P2 #s elim s
normalize /6 by proj1, proj2, conj/
qed.

definition translate_function :
  ∀tmpuniverse:universe SymbolTag.
  ∀globals:list (ident×region×type).
  ∀f:function.
    globals_fresh_for_univ ? globals tmpuniverse →
    fn_fresh_for_univ f tmpuniverse →
  res internal_function ≝
λtmpuniverse, globals, f, Fglobals, Ffn.
  do 〈env_pack, ul〉 ← build_label_env (fn_body f);
    match env_pack with
    [ mk_Sig lbls Ilbls ⇒
      let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in
      let uv ≝ mk_tmpgen vartypes tmpuniverse [ ] ?? in
      do s0 ← translate_statement vartypes uv ul lbls DoNotConvert (opttyp_of_type (fn_return f)) (fn_body f);
      do «fgens, s1, Is» ← alloc_params vartypes lbls ? uv DoNotConvert (opttyp_of_type (fn_return f)) (fn_params f) s0;
      let params ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f) in
      let vars ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? (fst ?? fgens) @ fn_vars f) in
      do D ← check_distinct_env ?? (params @ vars);
      OK ? (mk_internal_function
        (opttyp_of_type (fn_return f))
        params
        vars
        D
        stacksize
        s1 ?)
  ].
[ 1: #i #t #Hloc whd @Hloc
| 2: whd #id #Hpresent normalize in Hpresent:(???%?); whd in Hpresent;
      @(characterise_vars_fresh … (sym_eq … E)) //
| 3: @(match fgens return λx.x=fgens → ? with
     [ mk_Prod uv' ul' ⇒ λHfgens.? ] (refl ? fgens))
     whd in Is; <Hfgens in Is; #Is whd in Is ⊢ %;
     elim Is * * * #Hstmt_inv #Hlab_trans #Htmps_pres #Hreturn #Hlabel_wf
     (* merge Hlabel_wf with Hstmt_inv and eliminate right away *)
     @(stmt_P_mp … (stmt_P_conj … (stmt_P_conj … Hstmt_inv Hlabel_wf) Hreturn))
     #s * * #Hstmt_vars #Hstmt_labels #Hstmt_return %
     [ 1: (* prove that variables are either parameters or locals *)
        @(stmt_vars_mp … Hstmt_vars) #i #t #H
        (* Case analysis: (i, t) is either in vartypes, or in (tmp_env vartypes uv) *)
        cases (local_id_split … H)
        [ 1: #H' >map_append
          @Exists_map [ 1: #x @(And (\fst x = i) (typ_of_type (\snd x) = t))  (* * #id #ty @(〈id, typ_of_type ty〉=〈i, t〉)*)
                      | 2: whd @Exists_squeeze @(characterise_vars_all globals f ?? (sym_eq ??? E) i t H')
                      | 3: * #id #ty * #E1 #E2 <E1 <E2 @refl
                      ]
        | 2: #EX @Exists_append_r whd in ⊢ (???%); <map_append @Exists_append_l 
          @Exists_map [ 1: #x @(And (\fst x = i) (typ_of_type (\snd x) = t))
                      | 2: <Hfgens @EX
                      | 3: * #id #ty * #E1 #E2 <E1 <E2 % @refl
                      ]
        ]
     | 2: (* prove that labels are properly declared. *) 
          @(stmt_labels_mp … Hstmt_labels) #l * *
          [ 1: #H assumption
          | 2: * #cl_label #Hlookup lapply (Ilbls cl_label l Hlookup) #Hdefined
                cases (Hlab_trans … Hdefined) #lx * #LOOKUPx >LOOKUPx in Hlookup; #Ex destruct (Ex)
                #H @H
          ]
     | cases s in Hstmt_return; // * normalize [2: * #t #e ]
       cases (fn_return f) normalize #A try #B try #C try #D try #E destruct //
    ]
] qed.    

definition translate_fundef :
  ∀tmpuniverse:universe SymbolTag.
  ∀globals:list (ident×region×type).
    globals_fresh_for_univ ? globals tmpuniverse →
  ∀f:clight_fundef.
    fd_fresh_for_univ f tmpuniverse →
  res (fundef internal_function) ≝
λtmpuniverse,globals,Fglobals,f.
match f return λf. fd_fresh_for_univ f ? → ? with
[ CL_Internal fn ⇒ λFf. do fn' ← translate_function tmpuniverse globals fn Fglobals Ff; OK ? (Internal ? fn')
| CL_External fn argtys retty ⇒ λ_. OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
].

let rec map_partial_All (A,B:Type[0]) (P:A → Prop) (f:∀a:A. P a → res B)
  (l:list A) (H:All A P l) on l : res (list B) ≝
match l return λl. All A P l → ? with
[ nil ⇒ λ_. OK (list B) (nil B)
| cons hd tl ⇒ λH.
    do b_hd ← f hd (proj1 … H);
    do b_tl ← map_partial_All A B P f tl (proj2 … H);
      OK (list B) (cons B b_hd b_tl)
] H.

definition clight_to_cminor : clight_program → res Cminor_program ≝
λp.
  let tmpuniverse ≝ universe_for_program p in
  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
  let globals ≝ fun_globals @ var_globals in
  do fns ← map_partial_All ??? (λx,H. do f ← translate_fundef tmpuniverse globals ? (\snd x) H; OK ? 〈\fst x, f〉) (prog_funct ?? p) ?;
    OK ? (mk_program ??
      (map ?? (λv. 〈\fst v, \fst (\snd v)〉) (prog_vars ?? p))
      fns
      (prog_main ?? p)).
cases (prog_fresh p) * #H1 #H2 #H3
[ @(All_mp … H1) #x * //
| @All_append
  [ elim (prog_funct ?? p) in H1 ⊢ %; // * #id #fd #tl #IH * * #Hhd1 #Hhd2 #Htl % // @IH @Htl
  | whd in H3; elim (prog_vars ?? p) in H3 ⊢ %; // #hd #tl #IH * #Hhd #Htl % /2/
  ]
] qed.

(* It'd be nice to go back to some generic thing like

 transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)).

   rather than the messier definition above.
*)