Module Cshmstackgen

Require Import Coqlib.
Require Import Maps.
Require Import Errors.
Require Import Integers.
Require Import Floats.
Require Import AST.
Require Import Ctypes.
Require Import Cop.
Require Import Csharpminorannot.
Require Import Cminorgen.
Require Import Annotations.


Local Open Scope error_monad_scope.

Definition var_addr (cenv: compilenv) (sp id: ident): expr :=
  match PTree.get id cenv with
  | Some ofs => Ebinop Cminor.Oadd (Eaddrof sp) (Econst (Ointconst (Int.repr ofs)))
  | None => Eaddrof id
  end.

Fixpoint transl_expr (cenv: compilenv) (sp: ident) (e: expr): res expr :=
  match e with
  | Evar id => OK (Evar id)
  | Eaddrof id => OK (var_addr cenv sp id)
  | Econst cst => OK (Econst cst)
  | Eunop op e1 => do te1 <- transl_expr cenv sp e1;
                  OK (Eunop op te1)
  | Ebinop op e1 e2 => do te1 <- transl_expr cenv sp e1;
                      do te2 <- transl_expr cenv sp e2;
                      OK (Ebinop op te1 te2)
  | Eload (n, nil) kappa e => do te <- transl_expr cenv sp e;
                  OK (Eload (n, nil) kappa te)
  | Eload (n, _) _ _ => Error (msg "Cshmstackgen: non-empty annotation in load")
  end.

Fixpoint transl_exprlist (cenv: compilenv) (sp: ident) (el: list expr): res (list expr) :=
  match el with
  | nil => OK nil
  | e1::e2 => do te1 <- transl_expr cenv sp e1;
             do te2 <- transl_exprlist cenv sp e2;
             OK (te1::te2)
  end.

Fixpoint transl_stmt (cenv: compilenv) (sp: ident) (s: stmt): res stmt :=
  match s with
  | Sskip => OK Sskip
  | Sset id e => do te <- transl_expr cenv sp e;
                OK (Sset id te)
  | Sstore (n, nil) kappa e1 e2 => do te1 <- transl_expr cenv sp e1;
                            do te2 <- transl_expr cenv sp e2;
                            OK (Sstore (n, nil) kappa te1 te2)
  | Sstore (n, _) _ _ _ => Error (msg "Cshmstackgen: non-empty annot in store")
  | Scall optid sig e el => do te <- transl_expr cenv sp e;
                           do tel <- transl_exprlist cenv sp el;
                           OK (Scall optid sig te tel)
  | Sbuiltin optid ef el => do tel <- transl_exprlist cenv sp el;
                           OK (Sbuiltin optid ef tel)
  | Sseq s1 s2 => do ts1 <- transl_stmt cenv sp s1;
                 do ts2 <- transl_stmt cenv sp s2;
                 OK (Sseq ts1 ts2)
  | Sifthenelse e s1 s2 => do te <- transl_expr cenv sp e;
                          do ts1 <- transl_stmt cenv sp s1;
                          do ts2 <- transl_stmt cenv sp s2;
                          OK (Sifthenelse te ts1 ts2)
  | Sloop s => do ts <- transl_stmt cenv sp s;
              OK (Sloop ts)
  | Sblock s => do ts <- transl_stmt cenv sp s;
               OK (Sblock ts)
  | Sexit n => OK (Sexit n)
  | Sswitch is_long e ls => do te <- transl_expr cenv sp e;
                           do tls <- transl_lstmt cenv sp ls;
                           OK (Sswitch is_long te tls)
  | Sreturn None => OK (Sreturn None)
  | Sreturn (Some e) => do te <- transl_expr cenv sp e;
                       OK (Sreturn (Some te))
  | Slabel lbl s => do ts <- transl_stmt cenv sp s;
                   OK (Slabel lbl ts)
  | Sgoto lbl => OK (Sgoto lbl)
  end
with transl_lstmt (cenv: compilenv) (sp: ident) (ls: lbl_stmt): res lbl_stmt :=
       match ls with
       | LSnil => OK LSnil
       | LScons lbl s ls => do ts <- transl_stmt cenv sp s;
                           do tls <- transl_lstmt cenv sp ls;
                           OK (LScons lbl ts tls)
       end.

Definition sp_of (sp: ident) (f: function): ident :=
  List.fold_left (fun acc x => if plt acc x then x else acc) (List.map fst f.(fn_vars)) sp.

Definition transl_function (sp: ident) (f: function): res function :=
  let (cenv, stacksize) := build_compilenv f in
  if zle stacksize Int.max_unsigned
  then do tbody <- transl_stmt cenv (sp_of sp f) f.(fn_body);
       OK (mkfunction f.(fn_sig) f.(fn_params) ((sp_of sp f, stacksize)::nil) f.(fn_temps) tbody)
  else Error (msg "Cshmstackgen: too many local variables").

Definition transl_fundef (sp: ident) (fd : fundef): res fundef :=
  AST.transf_partial_fundef (transl_function sp) fd.

Definition sp_of_prog (p: program): ident :=
  Psucc (List.fold_left (fun acc x => if plt acc x then x else acc) (List.map fst p.(prog_defs)) xH).

Definition transl_program (p: program): res program :=
  AST.transform_partial_program (transl_fundef (sp_of_prog p)) p.