Module CC

From Coq Require Import List Permutation.
Import List.ListNotations.
Open Scope list_scope.

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

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

Module Type EXT_CC
  (Ids : IDS)
  (Op : OPERATORS)
  (OpAux : OPERATORS_AUX Ids Op)
  (Cks : CLOCKS Ids Op OpAux)
  (CESyn : CESYNTAX Ids Op OpAux Cks)
  (Syn : STCSYNTAX Ids Op OpAux Cks CESyn).

  Parameter cutting_points : list ident -> list ident -> list Syn.trconstr -> list ident.

End EXT_CC.

Module Type CC
  (Import Ids : IDS)
  (Import Op : OPERATORS)
  (OpAux : OPERATORS_AUX Ids Op)
  (Import Cks : CLOCKS Ids Op OpAux)
  (Import CESyn : CESYNTAX Ids Op OpAux Cks)
  (Import Syn : STCSYNTAX Ids Op OpAux Cks CESyn)
  (ECC : EXT_CC Ids Op OpAux Cks CESyn Syn).

  Module Fresh := Fresh.Fresh(Ids).
  Import Fresh Notations Facts Tactics.
  Local Open Scope fresh_monad_scope.

  Section rename.
    Definition rename_var sub x :=
      or_default x (Env.find x sub).

    Variable subl subn : Env.t ident.

    Fixpoint rename_clock (ck : clock) :=
      match ck with
      | Cbase => Cbase
      | Con ck x (ty, k) => Con (rename_clock ck) (rename_var subn x) (ty, k)
      end.

    Fixpoint rename_exp (e : exp) :=
      match e with
      | Econst _ | Eenum _ _ => e
      | Evar x ty => Evar (rename_var subn x) ty
      | Elast x ty => match Env.find x subl with
                     | Some xl => Evar xl ty
                     | None => Elast x ty
                     end
      | Ewhen e (x, ty) k => Ewhen (rename_exp e) (x, ty) k
      | Eunop op e1 ty => Eunop op (rename_exp e1) ty
      | Ebinop op e1 e2 ty => Ebinop op (rename_exp e1) (rename_exp e2) ty
      end.

    Fixpoint rename_cexp (e : cexp) :=
      match e with
      | Emerge (x, tx) es ty => Emerge (x, tx) (map rename_cexp es) ty
      | Ecase e es d => Ecase (rename_exp e) (map (option_map rename_cexp) es) (rename_cexp d)
      | Eexp e => Eexp (rename_exp e)
      end.

    Definition rename_rhs (e : rhs) :=
      match e with
      | Eextcall f es ty => Eextcall f (map rename_exp es) ty
      | Ecexp e => Ecexp (rename_cexp e)
      end.
  End rename.

  Definition rename_trconstr subl subn (tc : trconstr) :=
    match tc with
    | TcDef ck x rhs => TcDef ck x (rename_rhs subl subn rhs)
    | TcReset _ _ => tc
    | TcUpdate ck ckrs (UpdLast x e) =>
        TcUpdate ck ckrs (UpdLast x (rename_cexp subl subn e))
    | TcUpdate ck ckrs (UpdNext x e) =>
        TcUpdate ck ckrs (UpdNext x (rename_exp subl subn e))
    | TcUpdate ck ckrs (UpdInst i xs f es) =>
        TcUpdate ck ckrs (UpdInst i xs f (map (rename_exp subl (@Env.empty _)) es))
    end.


  Definition FreshAnn A := Fresh stc A (type * clock).

  Definition cut_cycles_tcs (lasts nexts: list (ident * (const * type * clock))) tcs : FreshAnn (list trconstr) :=
    do nlasts <- fresh_idents (map (fun '(x, (_, ty, ck)) => (x, (ty, ck))) lasts);
    let subl := Env.from_list (map fst nlasts) in
    let eqlasts := map (fun '(x, lx, (ty, ck)) => TcDef ck lx (Ecexp (Eexp (Elast x ty)))) nlasts in
    do nnexts <- fresh_idents (map (fun '(x, (_, ty, ck)) => (x, (ty, ck))) nexts);
    let subn := Env.from_list (map fst nnexts) in
    let eqnexts := map (fun '(x, lx, (ty, ck)) => TcDef ck lx (Ecexp (Eexp (Evar x ty)))) nnexts in

    ret (eqlasts++eqnexts++map (rename_trconstr subl subn) tcs).

Properties

  Section rename_typeof.
    Lemma rename_exp_typeof subl subn : forall e,
        typeof (rename_exp subl subn e) = typeof e.

    Lemma rename_cexp_typeofc subl subn : forall ce,
        typeofc (rename_cexp subl subn ce) = typeofc ce.

    Lemma rename_rhs_typeofr subl subn : forall e,
        typeofr (rename_rhs subl subn e) = typeofr e.
  End rename_typeof.

Variables, Last, Next Definitions

  Lemma fresh_idents_vars_perm : forall xs xs' st st',
      @fresh_idents stc (type * clock) xs st = (xs', st') ->
      Permutation (st_ids st') (map (fun '(_, lx, _) => lx) xs' ++ st_ids st).

  Lemma cut_cycles_tcs_variables : forall lasts nexts tcs tcs' st',
      cut_cycles_tcs lasts nexts tcs init_st = (tcs', st') ->
      Permutation (variables tcs') (variables tcs ++ st_ids st').

  Lemma cut_cycles_tcs_lasts_of : forall lasts nexts tcs tcs' st',
      cut_cycles_tcs lasts nexts tcs init_st = (tcs', st') ->
      lasts_of tcs' = lasts_of tcs.

  Lemma cut_cycles_tcs_nexts_of : forall lasts nexts tcs tcs' st',
      cut_cycles_tcs lasts nexts tcs init_st = (tcs', st') ->
      nexts_of tcs' = nexts_of tcs.

  Lemma cut_cycles_tcs_state_resets_of : forall lasts nexts tcs tcs' st',
      cut_cycles_tcs lasts nexts tcs init_st = (tcs', st') ->
      state_resets_of tcs' = state_resets_of tcs.

  Lemma cut_cycles_tcs_insts_of : forall lasts nexts tcs tcs' st',
      cut_cycles_tcs lasts nexts tcs init_st = (tcs', st') ->
      insts_of tcs' = insts_of tcs.

  Lemma cut_cycles_tcs_inst_resets_of : forall lasts nexts tcs tcs' st',
      cut_cycles_tcs lasts nexts tcs init_st = (tcs', st') ->
      inst_resets_of tcs' = inst_resets_of tcs.

AtomOrGensym / NoDup

  Fact AtomOrGensym_add : forall x,
      AtomOrGensym (PSP.of_list lustre_prefs) x ->
      AtomOrGensym (PSP.of_list gensym_prefs) x.

  Lemma stc_not_in_lustre_prefs :
    ~PS.In stc (PSP.of_list lustre_prefs).

  Program Definition cut_cycles_system (b: @system (PSP.of_list lustre_prefs)) : @system (PSP.of_list gensym_prefs) :=
    let tocut := ECC.cutting_points (map fst b.(s_lasts)) (map fst b.(s_nexts)) b.(s_tcs) in
    let tocut := PSP.of_list tocut in
    let res := cut_cycles_tcs
                 (filter (fun x => PS.mem (fst x) tocut) b.(s_lasts))
                 (filter (fun x => PS.mem (fst x) tocut) b.(s_nexts))
                 b.(s_tcs) init_st in
    let cnexts := filter (fun x => PS.mem (fst x) tocut) b.(s_nexts) in
    {|
      s_name := b.(s_name);
      s_subs := b.(s_subs);
      s_in := b.(s_in);
      s_vars := b.(s_vars)++st_anns (snd res);
      s_lasts := b.(s_lasts);
      s_nexts := b.(s_nexts);
      s_out := b.(s_out);
      s_tcs := fst res;

      s_ingt0 := b.(s_ingt0);
      s_nodup_states_subs := b.(s_nodup_states_subs);
    |}.

  Definition cut_cycles P : program :=
    Program P.(types) P.(externs) (map cut_cycles_system P.(systems)).

  Lemma cut_cycles_map_name : forall P,
      map s_name (map cut_cycles_system P) = map s_name P.

  Lemma cut_cycles_find_system :
    forall P P' f s,
      find_system f P = Some (s, P') ->
      find_system f (cut_cycles P) = Some (cut_cycles_system s, cut_cycles P').

  Lemma cut_cycles_find_system' :
    forall P f s P',
      find_system f (cut_cycles P) = Some (s, P') ->
      exists s' P'',
        find_system f P = Some (s', P'')
        /\ s = cut_cycles_system s'
        /\ P' = cut_cycles P''.


  Lemma fresh_idents_In_anns2 {prefs A} : forall xs1 xs2 xs1' xs2' st0 st1 st2,
      @fresh_idents prefs A xs1 st0 = (xs1', st1) ->
      @fresh_idents prefs A xs2 st1 = (xs2', st2) ->
      Forall (fun '(_, lx, ann) => In (lx, ann) (st_anns st2)) (xs1' ++ xs2').

  Lemma fresh_idents_In_anns2' {prefs A} : forall xs1 xs2 xs1' xs2' st1 st2,
      @fresh_idents prefs A xs1 init_st = (xs1', st1) ->
      @fresh_idents prefs A xs2 st1 = (xs2', st2) ->
      Forall (fun '(lx, ann) => exists x, In (x, ann) (xs1 ++ xs2)) (st_anns st2).

End CC.

Module CCFun
  (Ids : IDS)
  (Op : OPERATORS)
  (OpAux : OPERATORS_AUX Ids Op)
  (Cks : CLOCKS Ids Op OpAux)
  (CESyn : CESYNTAX Ids Op OpAux Cks)
  (Syn : STCSYNTAX Ids Op OpAux Cks CESyn)
  (ECC : EXT_CC Ids Op OpAux Cks CESyn Syn)
  <: CC Ids Op OpAux Cks CESyn Syn ECC.
  Include CC Ids Op OpAux Cks CESyn Syn ECC.
End CCFun.