Module SimplLocalsDummy

Require Import FSets.
Require FSetAVL.
Require Import Coqlib.
Require Import Ordered.
Require Import Errors.
Require Import AST.
Require Import Ctypes.
Require Import Cop.
Require Import Clight.

Open Scope error_monad_scope.
Open Scope string_scope.


Definition make_cast (a: expr) (tto: type) : expr :=
  Ecast a tto.

Fixpoint store_params (params: list (ident * type))
                      (s: statement): statement :=
  match params with
  | nil => s
  | (id, ty) :: params' =>
    Ssequence (Sassign (Evar id ty) (Etempvar id ty))
              (store_params params' s)
  end.


Definition transf_function (f: function) : res function :=
  assertion (list_disjoint_dec ident_eq (var_names f.(fn_params)) (var_names f.(fn_temps)));
    let body' := f.(fn_body) in
  OK {| fn_return := f.(fn_return);
        fn_callconv := f.(fn_callconv);
        fn_params := f.(fn_params);
        fn_vars := (f.(fn_params) ++ f.(fn_vars));
        fn_temps := f.(fn_temps);
        fn_body := store_params f.(fn_params) body' |}.


Definition transf_fundef (fd: fundef) : res fundef :=
  match fd with
  | Internal f => do tf <- transf_function f; OK (Internal tf)
  | External ef targs tres cconv => OK (External ef targs tres cconv)
  end.

Definition transf_program (p: program) : res program :=
  AST.transform_partial_program transf_fundef p.