include "Clight/Csyntax.ma".
include "Clight/TypeComparison.ma".
include "utilities/lists.ma".
(*
let rec mem_vars_expr (mem_vars:identifier_set SymbolTag) (e:expr) on e : Prop ≝
match e with
[ Expr ed ty ⇒
    match ed with
    [ Ederef e1 ⇒ mem_vars_expr mem_vars e1
    | Eaddrof e1 ⇒ mem_vars_addr mem_vars e1
    | Eunop _ e1 ⇒ mem_vars_expr mem_vars e1
    | Ebinop _ e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧
                       mem_vars_expr mem_vars e2
    | Ecast _ e1 ⇒ mem_vars_expr mem_vars e1
    | Econdition e1 e2 e3 ⇒ mem_vars_expr mem_vars e1 ∧
                            mem_vars_expr mem_vars e2 ∧
                            mem_vars_expr mem_vars e3
    | Eandbool e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧
                       mem_vars_expr mem_vars e2
    | Eorbool e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧
                      mem_vars_expr mem_vars e2
    | Efield e1 _ ⇒ mem_vars_expr mem_vars e1
    | Ecost _ e1 ⇒ mem_vars_expr mem_vars e1
    | _ ⇒ True
    ]
]
and mem_vars_addr (mem_vars:identifier_set SymbolTag) (e:expr) on e : Prop ≝
match e with
[ Expr ed ty ⇒
    match ed with
    [ Evar x ⇒ mem_set ? mem_vars x = true
    | Ederef e1 ⇒ mem_vars_expr mem_vars e1
    | Efield e1 _ ⇒ mem_vars_addr mem_vars e1
    | _ ⇒ False (* not an lvalue *)
    ]
].

let rec mem_vars_stmt (mem_vars:identifier_set SymbolTag) (s:statement) on s : Prop ≝
match s with
[ Sskip ⇒ True
| Sassign e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧
                  mem_vars_expr mem_vars e2
| Scall oe1 e2 es ⇒ match oe1 with [ None ⇒ True | Some e1 ⇒ mem_vars_expr mem_vars e1 ] ∧
                    mem_vars_expr mem_vars e2 ∧
                    All ? (mem_vars_expr mem_vars) es
| Ssequence s1 s2 ⇒ mem_vars_stmt mem_vars s1 ∧
                    mem_vars_stmt mem_vars s2
| Sifthenelse e1 s1 s2 ⇒ mem_vars_expr mem_vars e1 ∧
                         mem_vars_stmt mem_vars s1 ∧
                         mem_vars_stmt mem_vars s2
| Swhile e1 s1 ⇒ mem_vars_expr mem_vars e1 ∧
                 mem_vars_stmt mem_vars s1
| Sdowhile e1 s1 ⇒ mem_vars_expr mem_vars e1 ∧
                   mem_vars_stmt mem_vars s1
| Sfor s1 e1 s2 s3 ⇒ mem_vars_stmt mem_vars s1 ∧
                     mem_vars_expr mem_vars e1 ∧
                     mem_vars_stmt mem_vars s2 ∧
                     mem_vars_stmt mem_vars s3
| Sbreak ⇒ True
| Scontinue ⇒ True
| Sreturn oe1 ⇒ match oe1 with [ None ⇒ True | Some e1 ⇒ mem_vars_expr mem_vars e1 ]
| Sswitch e1 ls ⇒ mem_vars_expr mem_vars e1 ∧
                  mem_vars_ls mem_vars ls
| Slabel _ s1 ⇒ mem_vars_stmt mem_vars s1
| Sgoto _ ⇒ True
| Scost _ s1 ⇒ mem_vars_stmt mem_vars s1
]
and mem_vars_ls (mem_vars:identifier_set SymbolTag) (ls:labeled_statements) on ls : Prop ≝
match ls with
[ LSdefault s1 ⇒ mem_vars_stmt mem_vars s1
| LScase _ s1 ls1 ⇒ mem_vars_stmt mem_vars s1 ∧
                    mem_vars_ls mem_vars ls1
].
*)

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.

(* 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 ≝ foldl ?? (λm,idr. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
  let m ≝ foldl ?? (λm,v. add ?? m (\fst v) Local) m (fn_params f) in
  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
  let 〈m,stacksize〉 ≝ foldl ?? (λms,v.
    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〉.


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

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

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

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,6,0)".

definition translate_unop : type → CLunop → res CMunop ≝
λty.λop:CLunop.
  match op with
  [ Onotbool ⇒ OK ? CMnotbool
  | Onotint ⇒ OK ? Onotint
  | Oneg ⇒
      match ty with
      [ Tint _ _ ⇒ OK ? Onegint
      | Tfloat _ ⇒ OK ? Onegf
      | _ ⇒ Error ? (msg TypeMismatch)
      ]
  ].

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


(* 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 : ∀r1,r2. CMexpr (ASTptr r1) → res (CMexpr (ASTptr r2)) ≝
λr1,r2,e. check_region r1 r2 ? e.

definition translate_cast : type → ∀ty2:type. CMexpr ? → res (CMexpr (typ_of_type ty2)) ≝
λty1,ty2.
match ty1 return λx.CMexpr (typ_of_type x) → ? with
[ Tint sz1 sg1 ⇒ λe.
    match ty2 return λx.res (CMexpr (typ_of_type x)) 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 (CMexpr (typ_of_type x)) with
    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2 | _ ⇒ Ointoffloat sz2 ]) e)
    | Tfloat sz2 ⇒ OK ? (Op1 ?? Oid e) (* FIXME *)
    | _ ⇒ Error ? (msg TypeMismatch)
    ]
| Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
    match ty2 return λx.res (CMexpr (typ_of_type x)) 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 (CMexpr (typ_of_type x)) 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)
].

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.


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 (CMexpr (typ_of_type (typeof e))) ≝
match e return λe. res (CMexpr (typ_of_type (typeof e))) 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 ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
      match c 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 ⇒
          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 ⇒ OK ? (Id ? id)
      ]
  | Ederef e1 ⇒
      do e1' ← translate_expr vars e1;
      match typ_of_type (typeof e1) return λx.CMexpr x → ? with
      [ ASTptr r ⇒ λe1'.
          match access_mode ty return λx.access_mode ty = x → res (CMexpr (typ_of_type ty)) with
          [ By_value q ⇒ λ_.OK ? (Mem (typ_of_type ty) ? q e1')
          | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈CMexpr (ASTptr r') ↦ CMexpr (typ_of_type ty)⌉
          | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
          ] (refl ? (access_mode ty))
      | _ ⇒ λ_. Error ? (msg TypeMismatch)
      ] e1'
  | Eaddrof e1 ⇒
      do e1' ← translate_addr vars e1;
      match typ_of_type ty return λx.res (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 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;
      translate_binop op (typeof e1) e1' (typeof e2) e2' ty
  | Ecast ty1 e1 ⇒
      do e1' ← translate_expr vars e1;
      do e' ← translate_cast (typeof e1) ty1 e1';
      typ_should_eq ? (typ_of_type ty) ? e'
  | Econdition e1 e2 e3 ⇒
      do e1' ← translate_expr vars e1;
      do e2' ← translate_expr vars e2;
      do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
      do e3' ← translate_expr vars e3;
      do e3' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e3';
      match typ_of_type (typeof e1) return λx.CMexpr x → ? 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.CMexpr (typ_of_type x)) e2';
        match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) 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.CMexpr (typ_of_type x)) e2';
        match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) 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 ⇒
      do e' ← 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 (CMexpr (typ_of_type ty)) with
            [ By_value q ⇒ λ_. OK ? (Mem ?? q e1')
            | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈res (CMexpr (ASTptr r')) ↦ res (CMexpr (typ_of_type ty))⌉
            | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
            ] (refl ? (access_mode ty))
          ]
      | _ ⇒ Error ? (msg BadlyTypedAccess)
      ];
      typ_should_eq ? (typ_of_type ty) ? e'
  | Ecost l e1 ⇒
      do e1' ← translate_expr vars e1;
      do e' ← OK ? (Ecost ? l e1');
      typ_should_eq ? (typ_of_type ty) ? e'
  ]
] and translate_addr (vars:var_types) (e:expr) on e : res (Σr.CMexpr (ASTptr r)) ≝
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.CMexpr (ASTptr r)) with
      [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id 0)))
      | Stack n ⇒ OK ? (dp ?? 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. CMexpr x → res (Σr. CMexpr (ASTptr r)) with
      [ ASTptr r ⇒ λe1'.OK ? (dp ?? 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 ? (dp ?? 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)
  ]
].
>(access_mode_typ … E) @refl
qed.

inductive destination : Type[0] ≝
| IdDest : ident → destination
| MemDest : ∀r:region. memory_chunk → CMexpr (ASTptr r) → destination.

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 ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
            match c with
            [ Local ⇒ OK ? (IdDest id)
            | Global r ⇒ OK ? (MemDest r q (Cst ? (Oaddrsymbol id 0)))
            | Stack n ⇒ OK ? (MemDest Any q (Cst ? (Oaddrstack n)))
            ]
        | _ ⇒
            do e1' ← translate_addr vars e1;
            match e1' with [ dp r e1' ⇒ OK ? (MemDest r q e1') ]
        ]
    ].
(*
definition translate_assign ≝
λvars,e1,e2.
    do e2' ← translate_expr vars e2;
    do q ← match access_mode (typeof e2) 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 ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
            match c with
            [ Local ⇒ OK ? (St_assign id e2')
            | Global ⇒ OK ? (St_store q (Cst (Oaddrsymbol id zero)) e2')
            | Stack n ⇒ OK ? (St_store q (Cst (Oaddrstack (repr n))) e2')
            ]
        | _ ⇒
            do e1' ← translate_addr vars e1;
            OK ? (St_store q e1' e2')
        ]
    ].
*)
definition translate_assign ≝
λvars,e1,e2.
do e2' ← translate_expr vars e2;
do dest ← translate_dest vars e1 (typeof e2);
match dest with
[ IdDest id ⇒ OK ? (St_assign ? id e2')
| MemDest r q e1' ⇒ OK ? (St_store ? r q e1' e2')
].

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 : var_types → expr → res (Σt:typ.CMexpr t) ≝
λv,e.
  do e' ← translate_expr v e;
  OK ? (dp ? (λt:typ.CMexpr t) ? e').

axiom FIXME : String.

let rec translate_statement (vars:var_types) (tmp:ident) (tmpp:ident) (s:statement) on s : res stmt ≝
match s with
[ Sskip ⇒ OK ? St_skip
| Sassign e1 e2 ⇒ translate_assign vars e1 e2
| Scall ret ef args ⇒
    do ef' ← translate_expr vars ef;
    do ef' ← typ_should_eq ? (ASTptr Code) ? ef';
    do args' ← mmap … (translate_expr_sigma vars) args;
    match ret with
    [ None ⇒ OK ? (St_call (None ?) ef' args')
    | 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 ⇒ OK ? (St_call (Some ? id) ef' args')
        | MemDest r q e1' ⇒
            let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp | _ ⇒ tmp ] in
            OK ? (St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)))
        ]
    ]
| Ssequence s1 s2 ⇒
    do s1' ← translate_statement vars tmp tmpp s1;
    do s2' ← translate_statement vars tmp tmpp s2;
    OK ? (St_seq s1' s2')
| Sifthenelse e1 s1 s2 ⇒
    do e1' ← translate_expr vars e1;
    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
    [ ASTint _ _ ⇒ λe1'.
        do s1' ← translate_statement vars tmp tmpp s1;
        do s2' ← translate_statement vars tmp tmpp s2;
        OK ? (St_ifthenelse ?? e1' s1' s2')
    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    ] e1'
| Swhile e1 s1 ⇒
    do e1' ← translate_expr vars e1;
    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
    [ ASTint _ _ ⇒ λe1'.
        do s1' ← translate_statement vars tmp tmpp 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))))
    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    ] e1'
| Sdowhile e1 s1 ⇒
    do e1' ← translate_expr vars e1;
    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
    [ ASTint _ _ ⇒ λe1'.
        do s1' ← translate_statement vars tmp tmpp 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)))))
    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    ] e1'
| Sfor s1 e1 s2 s3 ⇒
    do e1' ← translate_expr vars e1;
    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
    [ ASTint _ _ ⇒ λe1'.
        do s1' ← translate_statement vars tmp tmpp s1;
        do s2' ← translate_statement vars tmp tmpp s2;
        do s3' ← translate_statement vars tmp tmpp 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)))))
    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    ] e1'
| Sbreak ⇒ OK ? (St_exit 1)
| Scontinue ⇒ OK ? (St_exit 0)
| Sreturn ret ⇒
    match ret with
    [ None ⇒ OK ? (St_return (None ?))
    | Some e1 ⇒
        do e1' ← translate_expr vars e1;
        OK ? (St_return (Some ? (dp … e1')))
    ]
| Sswitch e1 ls ⇒ Error ? (msg FIXME)
| Slabel l s1 ⇒
    do s1' ← translate_statement vars tmp tmpp s1;
    OK ? (St_label l s1')
| Sgoto l ⇒ OK ? (St_goto l)
| Scost l s1 ⇒
    do s1' ← translate_statement vars tmp tmpp s1;
    OK ? (St_cost l s1')
].

axiom ParamGlobalMixup : String.

definition alloc_params : var_types → list (ident×type) → stmt → res stmt ≝
λvars,params,s. foldl ?? (λs,it.
  let 〈id,ty〉 ≝ it in
  do s ← s;
  do t ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
  match t with
  [ Local ⇒ OK ? s
  | Stack n ⇒
      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)
  | Global _ ⇒ Error ? [MSG ParamGlobalMixup; CTX ? id]
  ]) (OK ? s) params.

definition bigid1 ≝ an_identifier SymbolTag [[
false;true;false;false;
false;false;false;false;
false;false;false;false;
false;false;false;false]].
definition bigid2 ≝ an_identifier SymbolTag [[
false;true;false;false;
false;false;false;false;
false;false;false;false;
false;false;false;true]].

(* FIXME: the temporary handling is nonsense, I'm afraid. *)
definition translate_function : list (ident×region) → function → res internal_function ≝
λglobals, f.
  let 〈vartypes, stacksize〉 ≝ characterise_vars globals f in
  let tmp ≝ bigid1 in (* FIXME *)
  let tmpp ≝ bigid2 in (* FIXME *)
  do s ← translate_statement vartypes tmp tmpp (fn_body f);
  do s ← alloc_params vartypes (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,ASTint I32 Unsigned〉::〈tmpp,ASTptr Any〉::(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
    stacksize
    s).

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

definition clight_to_cminor : clight_program → res Cminor_program ≝
λp.
  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 ???? (translate_fundef globals) (λi. OK ? (\fst i)) p.