include "Clight/Csyntax.ma".
include "Clight/TypeComparison.ma".
include "utilities/lists.ma".
include "utilities/deppair.ma".

(* Identify local variables that must be allocated memory. *)

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
].

inductive var_type : Type[0] ≝
| Global : region → var_type
| Stack  : nat → var_type
| Local  : var_type
.

definition var_types ≝ identifier_map SymbolTag var_type.

axiom UndeclaredIdentifier : String.

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

definition local_id : var_types → ident → Prop ≝
λvars,id. match lookup' vars id with [ OK t ⇒ match t with [ Global _ ⇒ False | _ ⇒ True ] | _ ⇒ 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.
 *)

definition always_alloc : type → bool ≝
λt. match t with
[ Tarray _ _ _ ⇒ true
| Tstruct _ _ ⇒ true
| Tunion _ _ ⇒ true
| _ ⇒ false
].

definition characterise_vars : list (ident×region) → function → var_types × nat ≝
λglobals, f.
  let m ≝ foldr ?? (λidr,m. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
  let 〈m,stacksize〉 ≝ foldr ?? (λv,ms.
    let 〈m,stack_high〉 ≝ ms in
    let 〈id,ty〉 ≝ v in
    let 〈c,stack_high〉 ≝ if always_alloc ty ∨ mem_set ? mem_vars id
                           then 〈Stack stack_high,stack_high + sizeof ty〉
                           else 〈Local, stack_high〉 in
      〈add ?? m id c, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in
  〈m,stacksize〉.

lemma local_id_add_global : ∀vars,id,r,id'.
  local_id (add ?? vars id (Global r)) id' → local_id vars id'.
#var #id #r #id'
whd in ⊢ (% → ?) whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?)
cases (identifier_eq ? id id')
[ #E >E >lookup_add_hit whd in ⊢ (% → ?) *
| #NE >lookup_add_miss // @eq_identifier_elim // #E >E in NE * /2/
] qed.

lemma local_id_add_miss : ∀vars,id,t,id'.
  id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'.
#vars #id #t #id' #NE
whd in ⊢ (% → %)
whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ])
>lookup_add_miss
[ #H @H | @eq_identifier_elim // #E >E in NE * /2/ ]
qed.

lemma characterise_vars_all : ∀l,f,vars,n.
  characterise_vars l f = 〈vars,n〉 →
  ∀i. local_id vars i →
      Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f).
#globals #f
whd in ⊢ (∀_.∀_.??%? → ?)
elim (fn_params f @ fn_vars f)
[ #vars #n whd in ⊢ (??%? → ?) #E destruct #i #H @False_ind
  elim globals in H
  [ normalize //
  | * #id #rg #t #IH whd in ⊢ (?%? → ?) #H @IH @(local_id_add_global ???? H)
  ]
| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?) #E #i
  cases (identifier_eq ? id i)
  [ #E' <E' #H % @refl
  | #NE #H whd %2 >(contract_pair var_types nat ?) in E;
    whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
    cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
    #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
    @(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.

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.


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).

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

definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
* [ #sz1 #sg1 | #r1 | #sz1 ]
* [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
| *; #P #p @(region_should_eq r1 ?? p)
| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
] 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)".

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 r ⇒
          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.

definition translate_add ≝
λty1,e1,ty2,e2,ty'.
let ty1' ≝ typ_of_type ty1 in
let ty2' ≝ typ_of_type ty2 in
match classify_add ty1 ty2 with
[ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2)
| add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2)
(* XXX using the integer size for e2 as the offset's size isn't right, because
   if e2 produces an 8bit value then the true offset might overflow *)
| add_case_pi ty ⇒
    match ty2' with
    [ ASTint sz2 _ ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst sz2 (repr ? (sizeof ty))))))
    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
    ]
| add_case_ip ty ⇒
    match ty1' with
    [ ASTint sz1 _ ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst sz1 (repr ? (sizeof ty))))))
    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
    ]
| add_default ⇒ Error ? (msg TypeMismatch)
].

definition translate_sub ≝
λty1,e1,ty2,e2,ty'.
let ty1' ≝ typ_of_type ty1 in
let ty2' ≝ typ_of_type ty2 in
match classify_sub ty1 ty2 with
[ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2)
| sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2)
(* XXX choosing offset sizes? *)
| sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
| sub_case_pp ty ⇒ 
    match ty' with (* XXX overflow *)
    [ ASTint sz _ ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' (Osubpp sz) e1 e2) (Cst ? (Ointconst sz (repr ? (sizeof ty)))))
    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
    ]
| sub_default ⇒ Error ? (msg TypeMismatch)
].

definition translate_mul ≝
λty1,e1,ty2,e2,ty'.
let ty1' ≝ typ_of_type ty1 in
let ty2' ≝ typ_of_type ty2 in
match classify_mul ty1 ty2 with
[ mul_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omul e1 e2)
| mul_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Omulf e1 e2)
| mul_default ⇒ Error ? (msg TypeMismatch)
].

definition translate_div ≝
λty1,e1,ty2,e2,ty'.
let ty1' ≝ typ_of_type ty1 in
let ty2' ≝ typ_of_type ty2 in
match classify_div ty1 ty2 with
[ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2)
| div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2)
| div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2)
| div_default ⇒ Error ? (msg TypeMismatch)
].

definition translate_mod ≝
λty1,e1,ty2,e2,ty'.
let ty1' ≝ typ_of_type ty1 in
let ty2' ≝ typ_of_type ty2 in
match classify_mod ty1 ty2 with
[ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2)
| mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2)
| mod_default ⇒ Error ? (msg TypeMismatch)
].

definition translate_shr ≝
λty1,e1,ty2,e2,ty'.
let ty1' ≝ typ_of_type ty1 in
let ty2' ≝ typ_of_type ty2 in
match classify_shr ty1 ty2 with
[ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2)
| shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2)
| shr_default ⇒ Error ? (msg TypeMismatch)
].

definition translate_cmp ≝
λc,ty1,e1,ty2,e2,ty'.
let ty1' ≝ typ_of_type ty1 in
let ty2' ≝ typ_of_type ty2 in
match classify_cmp ty1 ty2 with
[ cmp_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpu c) e1 e2)
| cmp_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmp c) e1 e2)
| cmp_case_pp ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpp c) e1 e2)
| cmp_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpf c) e1 e2)
| cmp_default ⇒ 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 e1 ty2 e2 ty'
| Osub ⇒ translate_sub ty1 e1 ty2 e2 ty'
| Omul ⇒ translate_mul ty1 e1 ty2 e2 ty'
| Omod ⇒ translate_mod ty1 e1 ty2 e2 ty'
| Odiv ⇒ translate_div ty1 e1 ty2 e2 ty'
| Oand ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oand e1 e2)
| Oor  ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oor e1 e2)
| Oxor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oxor e1 e2)
| Oshl ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oshl e1 e2)
| Oshr ⇒ translate_shr ty1 e1 ty2 e2 ty'
| Oeq ⇒ translate_cmp Ceq ty1 e1 ty2 e2 ty'
| One ⇒ translate_cmp Cne ty1 e1 ty2 e2 ty'
| Olt ⇒ translate_cmp Clt ty1 e1 ty2 e2 ty'
| Ogt ⇒ translate_cmp Cgt ty1 e1 ty2 e2 ty'
| Ole ⇒ translate_cmp Cle ty1 e1 ty2 e2 ty'
| Oge ⇒ translate_cmp Cge ty1 e1 ty2 e2 ty'
].

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 ⊢ (??%? → ?)
[ cases (classify_add ty1 ty2)
  [ 3,4: #z ] whd in ⊢ (??%? → ?)
  [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    whd in c:(??%?); destruct % [ @H1 | % // @H2 ]
  | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    whd in c:(??%?); destruct % [ @H2 | % // @H1 ]
  | *: #E destruct (E) % try @H1 @H2
  ]
| cases (classify_sub ty1 ty2)
  [ 3,4: #z] whd in ⊢ (??%? → ?)
  [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I
  | *: #E destruct (E) % try @H1 try @H2 % // @H2
  ]
| cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct
    % try @H1 @H2
| cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct
    % try @H1 @H2
| cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct
    % try @H1 @H2
| 6,7,8,9: #E destruct % try @H1 @H2
| cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
| 11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
] qed.

(* We'll need to implement proper translation of pointers if we really do memory
   spaces. *)
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) ]
  ].

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.

definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. 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 r _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e)
    | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) 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 r1 _ ⇒ λ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 r2 _ _ ⇒ translate_ptr ? r1 r2 e
    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
    | _ ⇒ Error ? (msg TypeMismatch)
    ]
| Tarray r1 _ _ ⇒ λ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 r1) (ASTint sz2 sg2) (Ointofptr sz2 ??) e, ?»
    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
    | _ ⇒ Error ? (msg TypeMismatch)
    ]
| _ ⇒ λ_. Error ? (msg TypeMismatch)
]. whd @use_sig qed.

lemma access_mode_typ : ∀ty,r. access_mode ty = By_reference r → typ_of_type ty = ASTptr r.
*
[ 5: #r #ty #n #r' normalize #E destruct @refl
| 6: #args #ret #r normalize #E destruct @refl
| *: normalize #a #b try #c try #d destruct
  [ cases a in d; normalize; cases b; normalize #E destruct
  | cases a in c; normalize #E destruct
  ]
] qed.

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 ⇒ OK ? «Cst ? (Ointconst sz i), ?»
  | Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?»
  | Evar id ⇒
      do c as E ← lookup' vars id;
      match c return λx.? = ? → res (Σe':CMexpr ?. ?) with
      [ Global r ⇒ λ_.
          match access_mode ty with
          [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?»
          | By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
          ]
      | Stack n ⇒ λE.
          match access_mode ty with
          [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?»
          | By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?»
          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
          ]
      | Local ⇒ λE. OK ? «Id ? id, ?»
      ] E
  | 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)) → ? with
      [ ASTptr r ⇒ λe1'.
          match access_mode ty return λx.? → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with
          [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (eject … e1'), ?»
          | By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1';
                                  OK ? e1'⌈Σe':CMexpr ?. expr_vars ? e' (local_id vars) ↦ Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)⌉
          | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
          ] (access_mode_typ ty)
      | _ ⇒ λ_. 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 r ⇒
          match e1' with
          [ dp r1 e1' ⇒ region_should_eq r1 r ? e1'
          ]
      | _ ⇒ Error ? (msg TypeMismatch)
      ]
  | Eunop op e1 ⇒
      do op' ← translate_unop (typ_of_type (typeof e1)) (typ_of_type ty) op;
      do e1' ← translate_expr vars e1;
      OK ? «Op1 ?? op' e1', ?»
  | 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' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
      do e3' ← translate_expr vars e3;
      do e3' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e3';
      match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → ? 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 with
      [ Tint sz _ ⇒
        do e2' ← type_should_eq ? ty (λ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' e2' (Cst ? (Ointconst sz (zero ?))), ?»
        | _ ⇒ λ_.Error ? (msg TypeMismatch)
        ] e1'
      | _ ⇒ Error ? (msg TypeMismatch)
      ]
  | Eorbool e1 e2 ⇒
      do e1' ← translate_expr vars e1;
      do e2' ← translate_expr vars e2;
      match ty with
      [ Tint sz _ ⇒
        do e2' ← type_should_eq ? ty (λ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)) → ? with
        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2', ?»
        | _ ⇒ λ_.Error ? (msg TypeMismatch)
        ] e1'
      | _ ⇒ Error ? (msg TypeMismatch)
      ]
  | Esizeof ty1 ⇒
      match ty with
      [ Tint sz _ ⇒ OK ? «Cst ? (Ointconst sz (repr ? (sizeof ty1))), ?»
      | _ ⇒ Error ? (msg TypeMismatch)
      ]
  | Efield e1 id ⇒
      match typeof e1 with
      [ Tstruct _ fl ⇒
          do e1' ← translate_addr vars e1;
          match e1' with
          [ dp r e1' ⇒
            do off ← field_offset id fl;
            match access_mode ty with
            [ By_value q ⇒ OK ? «Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))),?»
            | By_reference _ ⇒ OK ? «Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))),?»
            | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
            ]
          ]
      | Tunion _ _ ⇒
          do e1' ← translate_addr vars e1;
          match e1' with
          [ dp r e1' ⇒
            match access_mode ty return λx. access_mode ty = x → res ? with
            [ By_value q ⇒ λ_. OK ? «Mem ?? q e1', ?»
            | By_reference r' ⇒  λE. do e1' ← region_should_eq r r' ? e1';
                                OK ? e1'⌈Σz:CMexpr (ASTptr r').? ↦ Σz:CMexpr (typ_of_type ty).?⌉
            | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
            ] (refl ? (access_mode ty))
          ]
      | _ ⇒ 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'
  ]
] and translate_addr (vars:var_types) (e:expr) on e : res (Σr. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝
match e with
[ Expr ed _ ⇒
  match ed with
  [ Evar id ⇒
      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
      match c return λ_. res (Σr.Σz:CMexpr (ASTptr r).?) with
      [ Global r ⇒ OK ? «r, «Cst ? (Oaddrsymbol id 0), ?»»
      | Stack n ⇒ OK ? «Any, «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 (Σr. Σz:CMexpr (ASTptr r). ?) with
      [ ASTptr r ⇒ λe1'.OK ? «r, 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
          [ dp r e1'' ⇒ OK (Σr:region.Σe:CMexpr (ASTptr r).?) («r, «Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1'' (Cst ? (Ointconst I32 (repr ? off))), ?» »)
          ]
      | Tunion _ _ ⇒ translate_addr vars e1
      | _ ⇒ Error ? (msg BadlyTypedAccess)
      ]
  | _ ⇒ Error ? (msg BadLvalue)
  ]
].
whd try @I
[ >E @I
| >(E ? (refl ??)) @refl
| 3,4: @use_sig
| @(translate_binop_vars … E) @use_sig
| % [ % ] @use_sig
| % [ % @use_sig ] whd @I
| % [ % [ @use_sig | @I ] | @use_sig ]
| % [ @use_sig | @I ]
| % [ @use_sig | @I ]
| >(access_mode_typ … E) @refl
| @use_sig
| @use_sig
| % [ @use_sig | @I ]
] qed.

inductive destination (vars:var_types) : Type[0] ≝
| IdDest : ∀id:ident. local_id vars id → destination vars
| MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.

definition translate_dest ≝
λvars,e1,ty2.
    do q ← match access_mode ty2 with
           [ By_value q ⇒ OK ? q
           | By_reference r ⇒ OK ? (Mpointer r)
           | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
           ];
    match e1 with
    [ Expr ed1 ty1 ⇒
        match ed1 with
        [ Evar id ⇒
            do c as E ← lookup' vars id;
            match c return λx.? → ? with
            [ Local ⇒ λE. OK ? (IdDest vars id ?)
            | Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0)))
            | Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n)))
            ] E
        | _ ⇒
            do e1' ← translate_addr vars e1;
            match e1' with [ dp r e1' ⇒ OK ? (MemDest ? r q e1') ]
        ]
    ].
whd // >E @I
qed.

definition lenv ≝ identifier_map SymbolTag (identifier Label).

axiom MissingLabel : String.

definition lookup_label ≝
λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).

definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup_label lbls l' = OK ? l.

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).

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'.

definition stmt_inv ≝
λvars. λlbls:lenv.
  stmt_P (λs.stmt_vars (local_id vars) s ∧ stmt_labels (lpresent lbls) s).

definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.∀ls. stmt_inv vars ls s) ≝
λvars,e1,e2.
do e2' ← translate_expr vars e2;
do dest ← translate_dest vars e1 (typeof e2);
match dest with
[ IdDest id p ⇒ OK ? «St_assign ? id e2', ?»
| MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?»
].
#ls whd %
[ % // @use_sig
| @I
| % @use_sig
| @I
] qed.

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 [ dp 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 @use_sig
qed.

record tmpgen : Type[0] ≝ {
  tmp_universe : universe SymbolTag;
  tmp_env : list (ident × typ)
}.

definition alloc_tmp : memory_chunk → tmpgen → ident × tmpgen ≝
λc,g.
  let 〈tmp,u〉 ≝ fresh ? (tmp_universe g) in
  〈tmp, mk_tmpgen u (〈tmp, typ_of_memory_chunk c〉::(tmp_env g))〉.

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

definition add_tmps : var_types → tmpgen → var_types ≝
λvs,g.
  foldr ?? (λidty,vs. add ?? vs (\fst idty) Local) vs (tmp_env g).

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

lemma alloc_tmp_preserves : ∀tmp,u,u',vars,q.
  〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'.
#tmp #g #g' #vars #q
whd in ⊢ (???% → ?)
generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?)
* #tmp' #u whd in ⊢ (???% → ?) #E
destruct
#id #H
whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]
cases (identifier_eq ? id tmp')
[ #E1 >E1 >lookup_add_hit @I
| * #NE >lookup_add_miss [ @H | @eq_identifier_elim // #E1 cases (NE E1)
] qed.

definition trans_inv : var_types → lenv → statement → tmpgen → (stmt×tmpgen) → Prop ≝
λvars,lbls,s,u,su'.
  let 〈s',u'〉 ≝ su' in
  stmt_inv (add_tmps vars u') lbls s' ∧
  labels_translated lbls s s' ∧
  tmps_preserved vars u u'.

lemma trans_inv_stmt_inv : ∀vars,lbls,s,u,su.
  trans_inv vars lbls s u su → stmt_inv (add_tmps vars (\snd su)) lbls (\fst su).
#var #lbls #s #u * #s' #u' * * #H1 #H2 #H3 @H1
qed.

lemma trans_inv_labels : ∀vars,lbls,s,u,su.
  trans_inv vars lbls s u su → labels_translated lbls s (\fst su).
#vars #lbls #s #u * #s' #u' * * #_ #H #_ @H
qed.

lemma local_id_add_local_oblivious : ∀vars,id,id'.
  local_id vars id → local_id (add ?? vars id' Local) id.
#vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
cases (identifier_eq ? id id')
[ #E >E >lookup_add_hit @I
| * #NE >lookup_add_miss [ @H | @eq_identifier_elim // #E cases (NE E)
] qed.

lemma local_id_add_tmps_oblivious : ∀vars,id,u.
  local_id vars id → local_id (add_tmps vars u) id.
#vars #id * #u #l #H elim l
[ //
| * #id' #ty #tl @local_id_add_local_oblivious
] qed.

lemma add_tmps_oblivious : ∀vars,lbls,s,u.
  stmt_inv vars lbls s → stmt_inv (add_tmps vars u) lbls s.
#vars #lbls #s #u #H
@(stmt_P_mp … H)
#s' * #H1 #H2 %
[ @(stmt_vars_mp … H1)
  #id @local_id_add_tmps_oblivious
| @H2
] qed.

lemma local_id_fresh_tmp : ∀tmp,u,q,u0,vars.
  〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp.
#tmp #u #q #u0 #vars
whd in ⊢ (???% → ?)
generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?)
* #tmp' #u' whd in ⊢ (???% → ?) #E
destruct
whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ] >lookup_add_hit
@I
qed.

let rec translate_statement (vars:var_types) (lbls:lenv) (u:tmpgen) (s:statement) on s : res (Σsu:stmt×tmpgen.trans_inv vars lbls s u su) ≝
match s return λs.res (Σsu:stmt×tmpgen.trans_inv vars lbls s u su) with
[ Sskip ⇒ OK ? «〈St_skip, u〉, ?»
| Sassign e1 e2 ⇒
    do s' ← translate_assign vars e1 e2;
    OK ? «〈eject ?? s', u〉, ?»
| Scall ret ef args ⇒
    do ef' ← translate_expr vars ef;
    do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef';
    do args' ← mmap_sigma … (translate_expr_sigma vars) args;
    match ret with
    [ None ⇒ OK ? «〈St_call (None ?) ef' args', u〉, ?»
    | Some e1 ⇒
        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
        match dest with
        [ IdDest id p ⇒ OK ? «〈St_call (Some ? id) ef' args', u〉, ?»
        | MemDest r q e1' ⇒
            let 〈tmp, u〉 as Etmp ≝ alloc_tmp q u in
            OK ? «〈St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), u〉, ?»
        ]
    ]
| Ssequence s1 s2 ⇒
     do «s1', u1, H1» ← translate_statement vars lbls u s1;
     do «s2', u2, H2» ← translate_statement vars lbls u1 s2;
    OK ? «〈St_seq s1' s2', u2〉, ?»
| Sifthenelse e1 s1 s2 ⇒
    do e1' ← translate_expr vars e1;
    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    [ ASTint _ _ ⇒ λe1'.
         do «s1', u, H1» ← translate_statement vars lbls u s1;
         do «s2', u, H2» ← translate_statement vars lbls u s2;
        OK ? «〈St_ifthenelse ?? e1' s1' s2', u〉, ?»
    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    ] e1'
| Swhile e1 s1 ⇒
    do e1' ← translate_expr vars e1;
    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    [ ASTint _ _ ⇒ λe1'.
         do «s1', u, H1» ← translate_statement vars lbls u s1;
        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
        OK ? «〈St_block
               (St_loop
                 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), u〉, ?»
    | _ ⇒ λ_.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 ?) → ? with
    [ ASTint _ _ ⇒ λe1'.
         do «s1',u, H1» ← translate_statement vars lbls u s1;
        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
        OK ? «〈St_block
               (St_loop
                 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), u〉, ?»
    | _ ⇒ λ_.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 ?) → ? with
    [ ASTint _ _ ⇒ λe1'.
         do «s1', u, H1» ← translate_statement vars lbls u s1;
         do «s2', u, H2» ← translate_statement vars lbls u s2;
         do «s3', u, H3» ← translate_statement vars lbls u s3;
        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
        OK ? «〈St_seq s1'
             (St_block
               (St_loop
                 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), u〉, ?»
    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    ] e1'
| Sbreak ⇒ OK ? «〈St_exit 1, u〉, ?»
| Scontinue ⇒ OK ? «〈St_exit 0, u〉, ?»
| Sreturn ret ⇒
    match ret with
    [ None ⇒ OK ? «〈St_return (None ?), u〉, ?»
    | Some e1 ⇒
        do e1' ← translate_expr vars e1;
        OK ? «〈St_return (Some ? (dp … e1')), u〉, ?»
    ]
| Sswitch e1 ls ⇒ Error ? (msg FIXME)
| Slabel l s1 ⇒
    do l' as E ← lookup_label lbls l;
     do «s1', u, H1» ← translate_statement vars lbls u s1;
    OK ? «〈St_label l' s1', u〉, ?»
| Sgoto l ⇒
    do l' as E ← lookup_label lbls l;
    OK ? «〈St_goto l', u〉, ?»
| Scost l s1 ⇒
     do «s1', u, H1» ← translate_statement vars lbls u s1;
    OK ? «〈St_cost l s1', u〉, ?»
].
try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
try @I
try (#l #H @(match H in False with [ ]))
try (#id #H @H)
[ @add_tmps_oblivious @(use_sig ?? s')
| @local_id_add_tmps_oblivious @p
]
try (@use_sig' #x @expr_vars_mp #i @local_id_add_tmps_oblivious)
[ 1,3,6: @use_sig' #x @All_mp * #ty #e @expr_vars_mp #i @local_id_add_tmps_oblivious
| 2,4: @(local_id_fresh_tmp … Etmp)
| @(alloc_tmp_preserves … Etmp)
| 7,11: @(stmt_P_mp … (π1 (π1 H1))) #s * #H3 #H4 % [ 1,3: @(stmt_vars_mp … H3) cases H2 #_ #H @H | *: @H4 ]
| 8,12: @(trans_inv_stmt_inv … H2)
| 9,13: #l #H cases (Exists_append … H)
  [ 1,3: #H3 cases H1 * #S1 #L1 #T1 cases (L1 l H3) #l' * #E1 #D1
    %{l'} % [ 1,3: @E1 | *: @Exists_append_l @D1 ]
  | *: #H3 cases H2 * #S2 #L2 #T2 cases (L2 l H3) #l' * #E2 #D2
    %{l'} % [ 1,3: @E2 | *: @Exists_append_r @D2 ]
  ]
| 10,14: cases H2 #_ #TP2 #id #L @TP2 cases H1 #_ #TP1 @TP1 @L
| 15,18: @(π1 (π1 H1))
| 16,19: cases H1 * #_ #L1 #_ #l #H cases (L1 l H) #l' * #E1 #D1
  %{l'} % [ 1,3: @E1 | *: @Exists_append_l @D1 ]
| 17,20: @(π2 H1)
(* Sfor *)
| @(stmt_P_mp … (π1 (π1 H1))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #H @(π2 H3) @(π2 H2) @H | @H5 ]
| @(π1 (π1 H3))
| @(stmt_P_mp … (π1 (π1 H2))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #H @(π2 H3) @H | @H5 ]
| #l #H cases (Exists_append … H)
  [ #EX1 cases H1 * #S1 #L1 #_ cases (L1 l EX1) #l' * #E1 #D1
    %{l'} % [ @E1 | @Exists_append_l @D1 ]
  | #EX cases (Exists_append … EX)
    [ #EX2 cases H2 * #S2 #L2 #_ cases (L2 l EX2) #l' * #E2 #D2
      %{l'} % [ @E2 | @Exists_append_r @Exists_append_l @Exists_append_r @D2 ]
    | #EX3 cases H3 * #S3 #L3 #_ cases (L3 l EX3) #l' * #E3 #D3
      %{l'} % [ @E3 | @Exists_append_r @Exists_append_l @Exists_append_l @D3 ]
    ]
  ]
| #id #H @(π2 H3) @(π2 H2) @(π2 H1) @H
(* Slabel *)
| %{l} @E
| @(π1 (π1 H1))
| #l'' * [ #E <E %{l'} % // %1 @refl | #EX cases (π2 (π1 H1) l'' EX) #l4 * #LK #LD %{l4} % // %2 @LD ]
| @(π2 H1)
(* Sgoto *)
| %{l} @E
| @(π1 (π1 H1))
(* Scost *)
| @(π2 (π1 H1))
| @(π2 H1)
] qed.


axiom ParamGlobalMixup : String.

(* ls and s0 aren't real parameters, they're just there for giving the invariant. *)
definition alloc_params : ∀vars:var_types.∀ls,s0,u. list (ident×type) → (Σsu:stmt×tmpgen. trans_inv vars ls s0 u su) → res (Σsu:stmt×tmpgen.trans_inv vars ls s0 u su) ≝
λvars,ls,s0,u,params,s. foldl ?? (λsu,it.
  let 〈id,ty〉 ≝ it in
   do «s,u, Is» ← su;
  do t as E ← lookup' vars id;
  match t return λx.? → ? with
  [ Local ⇒ λE. OK (Σs:stmt×tmpgen.?) «〈s,u〉,Is»
  | Stack n ⇒ λE.
      do q ← match access_mode ty with
      [ By_value q ⇒ OK ? q
      | By_reference r ⇒ OK ? (Mpointer r)
      | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
      ];
      OK ? «〈St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s, u〉, ?»
  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
  ] E) (OK ? s) params.
try @conj try @conj try @conj try @conj try @conj try @conj
try @I
[ @(expr_vars_mp … (λid. local_id_add_tmps_oblivious vars id u)) whd >E @I
| @(π1 (π1 Is))
| @(π2 (π1 Is))
| @(π2 Is)
] qed.

(*
lemma local_id_add_local : ∀vars,id,id'.
  local_id vars id →
  local_id (add ?? vars id' Local) id.
#vars #id #id' #H
whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ?] cases (identifier_eq ? id id')
[ #E < E >lookup_add_hit //
| #NE >lookup_add_miss // @eq_identifier_elim // #E cases NE >E /2/
] 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 | @(eq_identifier_elim ?? l0 l)
  [ #E cases (NE E)
  | #_ @I
  ]
]
qed.  

let rec populate_lenv (ls:list ident) (lbls:lenv) (u:universe ?) : res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) ≝
match ls return λls. res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) with
[ nil ⇒ OK ? «lbls, ?»
| cons l t ⇒
    match lookup_label lbls l return λx.lookup_label lbls l = x → ? with
    [ OK _ ⇒ λ_. Error ? (msg DuplicateLabel)
    | Error _ ⇒ λLOOK.
        let 〈l',u1〉 ≝ fresh … u in
        do lbls1 ← populate_lenv t (add … lbls l l') u1;
        OK ? «eject … lbls1, ?»
    ] (refl ? (lookup_label lbls l))
].
[ #l #l' #H %2 @H
| cases lbls1 #lbls' #I whd in ⊢ (??%?)
  #l1 #l1' #E1 @(eq_identifier_elim … l l1)
  [ #E %1 %1 @E
  | #NE cases (I l1 l1' E1)
    [ #H %1 %2 @H
    | #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)) ≝
λbody.
  do «lbls, H» ← populate_lenv (labels_defined body) (empty_map ??) (new_universe ?);
  OK ? «lbls, ?».
#l #l' #E cases (H l l' E) //
whd in ⊢ (??%? → ?) #H destruct
qed.

lemma local_id_split : ∀vars,tmpgen,i.
  local_id (add_tmps vars tmpgen) i →
  local_id vars i ∨ Exists ? (λx.\fst x = i) (tmp_env tmpgen).
#vars #tmpgen #i
whd in ⊢ (?%? → ?)
elim (tmp_env tmpgen)
[ #H %1 @H
| * #id #ty #tl #IH
  cases (identifier_eq ? i id)
  [ #E >E #H %2 whd %1 @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 | @eq_identifier_elim // #E cases (NE E) ]
    ]
  ]
] 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.

definition translate_function : universe SymbolTag → list (ident×region) → function → res internal_function ≝
λtmpuniverse, globals, f.
  do «lbls, Ilbls» ← build_label_env (fn_body f);
  let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in
  let tmp ≝ mk_tmpgen tmpuniverse [ ] in
  do s ← translate_statement vartypes lbls tmp (fn_body f);
   do «s,tmp, Is» ← alloc_params vartypes lbls ?? (fn_params f) s;
  OK ? (mk_internal_function
    (opttyp_of_type (fn_return f))
    (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
    ((tmp_env tmp)@(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
    stacksize
    s ?).
cases Is * #S #L #TP
@(stmt_P_mp ???? S)
#s1 * #H1 #H2 %
[ @(stmt_vars_mp … H1)
  #i #H
  cases (local_id_split … H)
  [ #H' @Exists_squeeze >map_append
    @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i) @H'
                | skip
                | * #id #ty #E1 <E1 @refl
                ]
  | #EX @Exists_append_r @Exists_append_l @EX
  ]
| @(stmt_labels_mp … H2)
  #l * #l' #LOOKUP
  lapply (Ilbls l' l LOOKUP) #DEFINED
  cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP #Ex destruct (Ex)
  #H @H
] qed.

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

(* TODO: move universe generation to higher level once we do runtime function
   generation.  Cheating a bit - we only need the new identifiers to be fresh
   for individual functions. *)
include "Clight/fresh.ma".

definition clight_to_cminor : clight_program → res Cminor_program ≝
λp.
  let tmpuniverse ≝ universe_for_program p in
  let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
  let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in
  let globals ≝ fun_globals @ var_globals in
  transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)).