From Velus Require Import Common.
From Velus Require Import Environment.
From Velus Require Import Operators.
From Velus Require Import Clocks.

From Velus Require Import CoreExpr.CESyntax.
From Velus Require Import Stc.StcSyntax.

From Velus Require Import Obc.ObcSyntax.

From Coq Require Import List.
Import List.ListNotations.
From Coq Require Import Morphisms.

Open Scope list.

Translation

Module Type TRANSLATION
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Op)
       (Import CESyn : CESYNTAX Op)
       (Import SynStc : STCSYNTAX Ids Op CESyn)
       (Import SynObc : OBCSYNTAX Ids Op OpAux).

  Section Translate.

    Variable memories : PS.t.
    Variable clkvars : Env.t clock.

    Definition tovar (xt: ident * type) : exp :=
      let (x, ty) := xt in
      if PS.mem x memories then State x ty else Var x ty.

    Definition bool_var (x: ident) : exp := tovar (x, bool_type).

    Fixpoint Control (ck: clock) (s: stmt) : stmt :=
      match ck with
      | Cbase => s
      | Con ck x true => Control ck (Ifte (bool_var x) s Skip)
      | Con ck x false => Control ck (Ifte (bool_var x) Skip s)
      end.

    Fixpoint translate_exp (e: CESyn.exp) : exp :=
      match e with
      | Econst c => Const c
      | Evar x ty => tovar (x, ty)
      | Ewhen e c x => translate_exp e
      | Eunop op e ty => Unop op (translate_exp e) ty
      | Ebinop op e1 e2 ty => Binop op (translate_exp e1) (translate_exp e2) ty
      end.

    Fixpoint translate_cexp (x: ident) (e: cexp) : stmt :=
      match e with
      | Emerge y t f =>
        Ifte (bool_var y) (translate_cexp x t) (translate_cexp x f)
      | Eite b t f =>
        Ifte (translate_exp b) (translate_cexp x t) (translate_cexp x f)
      | Eexp l =>
        Assign x (translate_exp l)
      end.

    Definition var_on_base_clock (ck: clock) (x: ident) : bool :=
      negb (PS.mem x memories)
           && match Env.find x clkvars with
              | Some ck' => clock_eq ck ck'
              | None => false
              end.

    Definition translate_arg (ck: clock) (e : CESyn.exp) : exp :=
      match e with
      | Evar x ty =>
        if var_on_base_clock ck x
        then Valid x ty
        else translate_exp e
      | _ => translate_exp e
      end.

    Definition translate_tc (tc: trconstr) : stmt :=
      match tc with
      | TcDef x ck ce =>
        Control ck (translate_cexp x ce)
      | TcNext x ck le =>
        Control ck (AssignSt x (translate_exp le))
      | TcCall s xs ck rst f es =>
        Control ck (Call xs f s step (map (translate_arg ck) es))
      | TcReset s ck f =>
        Control ck (Call [] f s reset [])
      end.


    Definition translate_tcs (tcs: list trconstr) : stmt :=
      fold_left (fun i tc => Comp (translate_tc tc) i) tcs Skip.

  End Translate.

  Program Definition step_method (s: system) : method :=
    let memids := map fst s.(s_lasts) in
    let mems := ps_from_list memids in
    let clkvars := Env.adds_with snd s.(s_out)
                    (Env.adds_with snd s.(s_vars)
                      (Env.from_list_with snd s.(s_in)))
    in
    {| m_name := step;
       m_in := idty s.(s_in);
       m_vars := idty s.(s_vars);
       m_out := idty s.(s_out);
       m_body := translate_tcs mems clkvars s.(s_tcs)
    |}.

  Definition reset_mems (mems: list (ident * (const * clock))) : stmt :=
    fold_left (fun s xc => Comp s (AssignSt (fst xc) (Const (fst (snd xc))))) mems Skip.

  Definition reset_insts (insts: list (ident * ident)) : stmt :=
    fold_left (fun s xf => Comp s (Call [] (snd xf) (fst xf) reset [])) insts Skip.

  Definition translate_reset (b: system) : stmt :=
    Comp (reset_mems b.(s_lasts)) (reset_insts b.(s_subs)).

  Hint Constructors NoDupMembers.

  Program Definition reset_method (b: system) : method :=
    {| m_name := reset;
       m_in := [];
       m_vars := [];
       m_out := [];
       m_body := translate_reset b
    |}.

  Program Definition translate_system (b: system) : class :=
    {| c_name := b.(s_name);
       c_mems := map (fun xc => (fst xc, type_const (fst (snd xc)))) b.(s_lasts);
       c_objs := b.(s_subs);
       c_methods := [ step_method b; reset_method b ]
    |}.

  Definition translate (P: SynStc.program) : program :=
    map translate_system P.

  Lemma exists_step_method:
    forall s,
      find_method step (translate_system s).(c_methods) = Some (step_method s).

  Lemma exists_reset_method:
    forall s,
      find_method reset (translate_system s).(c_methods)
      = Some (reset_method s).

  Lemma find_method_stepm_out:
    forall s stepm,
      find_method step (translate_system s).(c_methods) = Some stepm ->
      stepm.(m_out) = idty s.(s_out).

  Lemma find_method_stepm_in:
    forall s stepm,
      find_method step (translate_system s).(c_methods) = Some stepm ->
      stepm.(m_in) = idty s.(s_in).

  Lemma find_class_translate:
    forall f P cls P',
      find_class f (translate P) = Some (cls, P') ->
      exists s P',
        find_system f P = Some (s, P')
        /\ cls = translate_system s.

  Lemma find_system_translate:
    forall f P s P',
      find_system f P = Some (s, P') ->
      exists cls prog',
        find_class f (translate P) = Some (cls, prog')
        /\ cls = translate_system s
        /\ prog' = translate P'.

  Lemma typeof_correct:
    forall mems e,
      typeof (translate_exp mems e) = CESyn.typeof e.

  Corollary typeof_arg_correct:
    forall mems clkvars ck e,
      typeof (translate_arg mems clkvars ck e) = CESyn.typeof e.

End TRANSLATION.

Module TranslationFun
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Op)
       (Import CESyn : CESYNTAX Op)
       (Import SynStc : STCSYNTAX Ids Op CESyn)
       (Import SynObc : OBCSYNTAX Ids Op OpAux)
       <: TRANSLATION Ids Op OpAux CESyn SynStc SynObc.
  Include TRANSLATION Ids Op OpAux CESyn SynStc SynObc.
End TranslationFun.