include "Clight/Csyntax.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 : 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 → function → var_types × nat ≝
λglobals, f.
  let m ≝ foldl ?? (λm,id. add ?? m id Global) (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_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.
axiom TypeMismatch : 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 ≝
λe1,ty1,e2,ty2.
match classify_add ty1 ty2 with
[ add_case_ii ⇒ OK ? (Op2 Oadd e1 e2)
| add_case_ff ⇒ OK ? (Op2 Oaddf e1 e2)
| add_case_pi ty ⇒ OK ? (Op2 Oaddp e1 (Op2 Omul e2 (Cst (Ointconst (repr (sizeof ty))))))
| add_case_ip ty ⇒ OK ? (Op2 Oaddp e2 (Op2 Omul e1 (Cst (Ointconst (repr (sizeof ty))))))
| add_default ⇒ Error ? (msg TypeMismatch)
].

definition translate_sub ≝
λe1,ty1,e2,ty2.
match classify_sub ty1 ty2 with
[ sub_case_ii ⇒ OK ? (Op2 Osub e1 e2)
| sub_case_ff ⇒ OK ? (Op2 Osubf e1 e2)
| sub_case_pi ty ⇒ OK ? (Op2 Osubpi e1 (Op2 Omul e2 (Cst (Ointconst (repr (sizeof ty))))))
| sub_case_pp ty ⇒ OK ? (Op2 Odivu (Op2 Osubpp e1 e2) (Cst (Ointconst (repr (sizeof ty)))))
| sub_default ⇒ Error ? (msg TypeMismatch)
].

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

definition translate_div ≝
λe1,ty1,e2,ty2.
match classify_div ty1 ty2 with
[ div_case_I32unsi ⇒ OK ? (Op2 Odivu e1 e2) (* FIXME: should be 8 bit only *)
| div_case_ii ⇒ OK ? (Op2 Odiv e1 e2)
| div_case_ff ⇒ OK ? (Op2 Odivf e1 e2)
| div_default ⇒ Error ? (msg TypeMismatch)
].

definition translate_mod ≝
λe1,ty1,e2,ty2.
match classify_mod ty1 ty2 with
[ mod_case_I32unsi ⇒ OK ? (Op2 Omodu e1 e2) (* FIXME: should be 8 bit only *)
| mod_case_ii ⇒ OK ? (Op2 Omod e1 e2)
| mod_default ⇒ Error ? (msg TypeMismatch)
].

definition translate_shr ≝
λe1,ty1,e2,ty2.
match classify_shr ty1 ty2 with
[ shr_case_I32unsi ⇒ OK ? (Op2 Oshru e1 e2) (* FIXME: should be 8 bit only *)
| shr_case_ii ⇒ OK ? (Op2 Oshr e1 e2)
| shr_default ⇒ Error ? (msg TypeMismatch)
].

definition translate_cmp ≝
λc,e1,ty1,e2,ty2.
match classify_cmp ty1 ty2 with
[ cmp_case_I32unsi ⇒ OK ? (Op2 (Ocmpu c) e1 e2)
| cmp_case_ii ⇒ OK ? (Op2 (Ocmp c) e1 e2)
| cmp_case_pp ⇒ OK ? (Op2 (Ocmpp c) e1 e2)
| cmp_case_ff ⇒ OK ? (Op2 (Ocmpf c) e1 e2)
| cmp_default ⇒ Error ? (msg TypeMismatch)
].

definition translate_binop : binary_operation → CMexpr → type → CMexpr → type → res CMexpr ≝
λop,e1,ty1,e2,ty2.
match op with
[ Oadd ⇒ translate_add e1 ty1 e2 ty2
| Osub ⇒ translate_sub e1 ty1 e2 ty2
| Omul ⇒ translate_mul e1 ty1 e2 ty2
| Omod ⇒ translate_mod e1 ty1 e2 ty2
| Odiv ⇒ translate_div e1 ty1 e2 ty2
| Oand ⇒ OK ? (Op2 Oand e1 e2)
| Oor  ⇒ OK ? (Op2 Oor e1 e2)
| Oxor ⇒ OK ? (Op2 Oxor e1 e2)
| Oshl ⇒ OK ? (Op2 Oshl e1 e2)
| Oshr ⇒ translate_shr e1 ty1 e2 ty2
| Oeq ⇒ translate_cmp Ceq e1 ty1 e2 ty2
| One ⇒ translate_cmp Cne e1 ty1 e2 ty2
| Olt ⇒ translate_cmp Clt e1 ty1 e2 ty2
| Ogt ⇒ translate_cmp Cgt e1 ty1 e2 ty2
| Ole ⇒ translate_cmp Cle e1 ty1 e2 ty2
| Oge ⇒ translate_cmp Cge e1 ty1 e2 ty2
].

definition translate_cast : type → type → CMexpr → res CMexpr ≝
λty1,ty2,e.
match ty1 with
[ Tint sz1 sg1 ⇒
    match ty2 with
    [ Tint sz2 sg2 ⇒ OK ? e (* FIXME: do we need to do zero/sign ext?  Ought to be 8 bit anyway... *)
    | 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 ⇒
    match ty2 with
    [ Tint sz2 sg2 ⇒ OK ? (Op1 (match sg2 with [ Unsigned ⇒ Ointuoffloat | _ ⇒ Ointoffloat]) e)
    | Tfloat sz2 ⇒ OK ? e
    | _ ⇒ Error ? (msg TypeMismatch)
    ]
| Tpointer _ _ ⇒ (* will need changed for memory regions *)
    match ty2 with
    [ Tint sz2 sg2 ⇒ OK ? (Op1 Ointofptr e)
    | Tarray _ _ _ ⇒ OK ? e
    | Tpointer _ _ ⇒ OK ? e
    | _ ⇒ Error ? (msg TypeMismatch)
    ]
| Tarray _ _ _ ⇒ (* will need changed for memory regions *)
    match ty2 with
    [ Tint sz2 sg2 ⇒ OK ? (Op1 Ointofptr e)
    | Tarray _ _ _ ⇒ OK ? e
    | Tpointer _ _ ⇒ OK ? e
    | _ ⇒ Error ? (msg TypeMismatch)
    ]
| _ ⇒ Error ? (msg TypeMismatch)
].

let rec translate_expr (vars:var_types) (e:expr) on e : res CMexpr ≝
match e with
[ Expr ed ty ⇒
  match ed with
  [ Econst_int i ⇒ OK ? (Cst (Ointconst 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 ⇒
          match access_mode ty with
          [ By_value q ⇒ OK ? (Mem q (Cst (Oaddrsymbol id zero)))
          | By_reference _ ⇒ OK ? (Cst (Oaddrsymbol id zero))
          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
          ]
      | Stack n ⇒
          match access_mode ty with
          [ By_value q ⇒ OK ? (Mem q (Cst (Oaddrstack (repr n))))
          | By_reference _ ⇒ OK ? (Cst (Oaddrstack (repr n)))
          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
          ]
      | Local ⇒ OK ? (Id id)
      ]
  | Ederef e1 ⇒
      do e1' ← translate_expr vars e1;
      match access_mode ty with
      [ By_value q ⇒ OK ? (Mem q e1')
      | By_reference _ ⇒ OK ? e1'
      | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
      ]
  | Eaddrof e1 ⇒ translate_addr vars e1
  | 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 e1' (typeof e1) e2' (typeof e2)
  | Ecast ty1 e1 ⇒
      do e1' ← translate_expr vars e1;
      translate_cast ty ty1 e1'
  | Econdition e1 e2 e3 ⇒
      do e1' ← translate_expr vars e1;
      do e2' ← translate_expr vars e2;
      do e3' ← translate_expr vars e3;
      OK ? (Cond e1' e2' e3')
  | Eandbool e1 e2 ⇒
      do e1' ← translate_expr vars e1;
      do e2' ← translate_expr vars e2;
      OK ? (Cond e1' e2' (Cst (Ointconst zero)))
  | Eorbool e1 e2 ⇒
      do e1' ← translate_expr vars e1;
      do e2' ← translate_expr vars e2;
      OK ? (Cond e1' (Cst (Ointconst one)) e2')
  | Esizeof ty1 ⇒ OK ? (Cst (Ointconst (repr (sizeof ty1))))
  | Efield e1 id ⇒
      match typeof e1 with
      [ Tstruct _ fl ⇒
          do e1' ← translate_addr vars e1;
          do off ← field_offset id fl;
          match access_mode ty with
          [ By_value q ⇒ OK ? (Mem q (Op2 Oaddp e1' (Cst (Ointconst (repr off)))))
          | By_reference _ ⇒ OK ? (Op2 Oaddp e1' (Cst (Ointconst (repr off))))
          | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
          ]
      | Tunion _ _ ⇒
          do e1' ← translate_addr vars e1;
          match access_mode ty with
          [ By_value q ⇒ OK ? (Mem q e1')
          | By_reference _ ⇒ OK ? e1'
          | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
          ]
      | _ ⇒ Error ? (msg BadlyTypedAccess)
      ]
  | Ecost l e1 ⇒
      do e1' ← translate_expr vars e1;
      OK ? (Ecost l e1')
  ]
] and translate_addr (vars:var_types) (e:expr) on e : res CMexpr ≝
match e with
[ Expr ed _ ⇒
  match ed with
  [ Evar id ⇒
      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
      match c with
      [ Global ⇒ OK ? (Cst (Oaddrsymbol id zero))
      | Stack n ⇒ OK ? (Cst (Oaddrstack (repr n)))
      | Local ⇒ Error ? (msg BadlyTypedAccess) (* TODO: could rule out? *)
      ]
  | Ederef e1 ⇒ translate_expr vars e1
  | Efield e1 id ⇒
      match typeof e1 with
      [ Tstruct _ fl ⇒
          do e1' ← translate_addr vars e1;
          do off ← field_offset id fl;
          OK ? (Op2 Oaddp e1' (Cst (Ointconst (repr off))))
      | Tunion _ _ ⇒ translate_addr vars e1
      | _ ⇒ Error ? (msg BadlyTypedAccess)
      ]
  | _ ⇒ Error ? (msg BadLvalue)
  ]
].

inductive destination : Type[0] ≝
| IdDest : ident → destination
| MemDest : memory_chunk → CMexpr → 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 ⇒ OK ? (MemDest q (Cst (Oaddrsymbol id zero)))
            | Stack n ⇒ OK ? (MemDest q (Cst (Oaddrstack (repr n))))
            ]
        | _ ⇒
            do e1' ← translate_addr vars e1;
            OK ? (MemDest 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 q e1' ⇒ OK ? (St_store 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)
].

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 args' ← mmap … (translate_expr 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 q e1' ⇒
            let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp | _ ⇒ tmp ] in
            OK ? (St_seq (St_call (Some ? tmp) ef' args') (St_store 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;
    do s1' ← translate_statement vars tmp tmpp s1;
    do s2' ← translate_statement vars tmp tmpp s2;
    OK ? (St_ifthenelse e1' s1' s2')
| Swhile e1 s1 ⇒
    do e1' ← translate_expr vars 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))))
| Sdowhile e1 s1 ⇒
    do e1' ← translate_expr vars 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)))))
| Sfor s1 e1 s2 s3 ⇒
    do e1' ← translate_expr vars 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)))))
| Sbreak ⇒ OK ? (St_exit 1)
| Scontinue ⇒ OK ? (St_exit 0)
| Sreturn ret ⇒
    do ret' ← m_option_map ?? (translate_expr vars) ret;
    OK ? (St_return ret')
| 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')
].


definition is_pointer : type → bool ≝
λty.
  match ty with
  [ Tpointer _ _ ⇒ true
  | Tfunction _ _ ⇒ true
  | _ ⇒ false
  ].

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

definition translate_function : list ident → function → res internal_function ≝
λglobals, f.
  let 〈vartypes, stacksize〉 ≝ characterise_vars globals f in
  let tmp ≝ bigid1 in (* FIXME *)
  let tmpp ≝ bigid2 in (* FIXME *)
  let p_ptrs ≝ filter ? (λx. is_pointer (\snd x)) (fn_params f) in
  let v_ptrs ≝ (filter ? (λx. is_pointer (\snd x)) (fn_vars f)) in
  do s ← translate_statement vartypes tmp tmpp (fn_body f);
  OK ? (mk_internal_function
    (signature_of_type (type_of_params (fn_params f)) (fn_return f))
    (map ?? (fst ??) (fn_params f))
    (tmp::tmpp::(map ?? (fst ??) (fn_vars f)))
    (tmpp::(map ?? (fst ??) p_ptrs) @ (map ?? (fst ??) v_ptrs))
    stacksize
    s).

definition translate_fundef : list ident → 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 globals ≝ (prog_funct_names ?? p)@(prog_var_names ?? p) in
  transform_partial_program2 ???? (translate_fundef globals) (λ_. OK ? it) p.