Module Cshmannotgen

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.
Import Annotations.

Open Local Scope string_scope.
Open Local Scope error_monad_scope.

Definition dummy_annotation: list ablock := nil.

Fixpoint transl_expr (e: Csharpminor.expr) (n: ident): res (ident * Csharpminorannot.expr) :=
  match e with
    | Csharpminor.Econst c =>
      OK (n, Econst c)
    | Csharpminor.Evar v => OK (n, Evar v)
    | Csharpminor.Eaddrof a => OK (n, Eaddrof a)
    | Csharpminor.Eunop op a =>
      do (n, a) <- transl_expr a n;
      OK (n, Eunop op a)
    | Csharpminor.Ebinop op a1 a2 =>
      do (n, a1) <- transl_expr a1 n;
      do (n, a2) <- transl_expr a2 n;
      OK (n, Ebinop op a1 a2)
    | Csharpminor.Eload kappa a =>
      do (n, a) <- transl_expr a n;
      OK (Psucc n, Eload (n, dummy_annotation) kappa a)
  end.

Fixpoint transl_exprlist (el: list Csharpminor.expr) (n: ident): res (ident * list Csharpminorannot.expr) :=
  match el with
    | nil => OK (n, nil)
    | e::el => do (n, e) <- transl_expr e n;
              do (n, el) <- transl_exprlist el n;
              OK (n, e::el)
  end.

Fixpoint transl_statement (s: Csharpminor.stmt) (n: ident): res (ident * Csharpminorannot.stmt) :=
  match s with
    | Csharpminor.Sskip => OK (n, Sskip)
    | Csharpminor.Sset a b =>
      do (n, b) <- transl_expr b n;
      OK (n, Sset a b)
    | Csharpminor.Sstore kappa a1 a2 =>
      do (n, a1) <- transl_expr a1 n;
      do (n, a2) <- transl_expr a2 n;
      OK (Psucc n, Sstore (n, dummy_annotation) kappa a1 a2)
    | Csharpminor.Scall optid sig a al =>
      do (n, a) <- transl_expr a n;
      do (n, al) <- transl_exprlist al n;
      OK (n, Scall optid sig a al)
    | Csharpminor.Sbuiltin optid ef al =>
      do (n, al) <- transl_exprlist al n;
      OK (n, Sbuiltin optid ef al)
    | Csharpminor.Sseq s1 s2 =>
      do (n, s1) <- transl_statement s1 n;
      do (n, s2) <- transl_statement s2 n;
      OK (n, Sseq s1 s2)
    | Csharpminor.Sifthenelse a s1 s2 =>
      do (n, a) <- transl_expr a n;
      do (n, s1) <- transl_statement s1 n;
      do (n, s2) <- transl_statement s2 n;
      OK (n, Sifthenelse a s1 s2)
    | Csharpminor.Sloop s =>
      do (n, s) <- transl_statement s n;
      OK (n, Sloop s)
    | Csharpminor.Sblock s =>
      do (n, s) <- transl_statement s n;
      OK (n, Sblock s)
    | Csharpminor.Sexit a =>
      OK (n, Sexit a)
    | Csharpminor.Sswitch b a ls =>
      do (n, a) <- transl_expr a n;
      do (n, ls) <- transl_lstatement ls n;
      OK (n, Sswitch b a ls)
    | Csharpminor.Sreturn None => OK (n, Sreturn None)
    | Csharpminor.Sreturn (Some a) =>
      do (n, a) <- transl_expr a n;
      OK (n, Sreturn (Some a))
    | Csharpminor.Slabel lbl s =>
      do (n, s) <- transl_statement s n;
      OK (n, Slabel lbl s)
    | Csharpminor.Sgoto lbl =>
      OK (n, Sgoto lbl)
  end
with transl_lstatement (ls: Csharpminor.lbl_stmt) (n: ident): res (ident * lbl_stmt) :=
       match ls with
         | Csharpminor.LSnil => OK (n, LSnil)
         | Csharpminor.LScons lbl s ls =>
           do (n, s) <- transl_statement s n;
           do (n, ls) <- transl_lstatement ls n;
           OK (n, LScons lbl s ls)
       end.

Definition transl_function (f: Csharpminor.function) (n: ident): res (ident * function) :=
  do (n, body) <- transl_statement f.(Csharpminor.fn_body) n;
  OK (n, mkfunction f.(Csharpminor.fn_sig) f.(Csharpminor.fn_params) f.(Csharpminor.fn_vars) f.(Csharpminor.fn_temps) body).

Definition transl_fundef (fd: Csharpminor.fundef) (n: ident): res (ident * fundef) :=
  match fd with
    | AST.Internal f =>
      do (n, tf) <- transl_function f n;
      OK (n, AST.Internal tf)
    | AST.External ef =>
      OK (n, AST.External ef)
  end.

Fixpoint transl_globdefs (l : list (ident * globdef Csharpminor.fundef unit)) (n: ident) :=
  match l with
    | nil => OK nil
    | (id, Gfun f)::l =>
      do (n, f) <- transl_fundef f n;
      do l <- transl_globdefs l n;
      OK ((id, Gfun f)::l)
    | (id, Gvar v)::l =>
      do l <- transl_globdefs l n;
      OK ((id, Gvar v)::l)
  end.

Definition transl_program (p: Csharpminor.program): res program :=
  do tprog_defs <- transl_globdefs p.(prog_defs) 1%positive;
  if list_norepet_dec peq (List.map fst tprog_defs) then
    OK {| prog_defs := tprog_defs;
          prog_public := p.(prog_public);
          prog_main := p.(prog_main)
       |}
  else Error (msg "prog_def_names are repeat").