Module DLClocking

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

From Velus Require Import Common.
From Velus Require Import Operators Environment.
From Velus Require Import Clocks.
From Velus Require Import Lustre.StaticEnv.
From Velus Require Import Lustre.LSyntax Lustre.LClocking.
From Velus Require Import Lustre.DeLast.DeLast.

Module Type DLCLOCKING
       (Import Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Import Cks : CLOCKS Ids Op OpAux)
       (Import Senv : STATICENV Ids Op OpAux Cks)
       (Import Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Import Clo : LCLOCKING Ids Op OpAux Cks Senv Syn)
       (Import DL : DELAST Ids Op OpAux Cks Senv Syn).

  Section rename.
    Context {PSyn : list decl -> block -> Prop}.
    Context {prefs : PS.t}.
    Variable G : @global PSyn prefs.

    Variable sub : Env.t ident.

    Section rename_in_exp.
      Variable Γ Γ' : static_env.

      Hypothesis Hvar : forall x ty, HasClock Γ x ty -> HasClock Γ' x ty.
      Hypothesis Hlast : forall x ty, HasClock Γ x ty -> IsLast Γ x -> HasClock Γ' (rename_in_var sub x) ty.

      Lemma rename_in_exp_clockof : forall e,
          clockof (rename_in_exp sub e) = clockof e.

      Corollary rename_in_exp_clocksof : forall es,
          clocksof (map (rename_in_exp sub) es) = clocksof es.

      Lemma rename_in_exp_nclockof : forall sub e,
          Forall2 (fun '(ck1, o1) '(ck2, o2) => ck1 = ck2 /\ LiftO True (fun id1 => o2 = Some id1) o1)
                  (nclockof e) (nclockof (rename_in_exp sub e)).

      Corollary rename_in_exp_nclocksof : forall sub es,
          Forall2 (fun '(ck1, o1) '(ck2, o2) => ck1 = ck2 /\ LiftO True (fun id1 => o2 = Some id1) o1)
                  (nclocksof es) (nclocksof (map (rename_in_exp sub) es)).

      Lemma rename_in_exp_wc : forall e,
          wc_exp G Γ e ->
          wc_exp G Γ' (rename_in_exp sub e).

      Lemma rename_in_equation_wc : forall eq,
          wc_equation G Γ eq ->
          wc_equation G Γ' (rename_in_equation sub eq).

    End rename_in_exp.

  End rename.

  Import Fresh Facts Tactics.

  Fact delast_scope_wc {A} P_nd P_wc1 (P_wc2: _ -> _ -> Prop) f_dl f_add {PSyn prefs} (G: @global PSyn prefs) :
    forall locs (blk: A) sub Γ Γty Γ' s' st st',
      (forall x ty, HasClock Γ x ty -> HasClock Γ' x ty) ->
      (forall x ty, HasClock Γ x ty -> IsLast Γ x -> HasClock Γ' (rename_in_var sub x) ty) ->
      incl (map fst Γ) Γty ->
      (forall x, Env.In x sub -> In x Γty) ->
      NoDupScope P_nd Γty (Scope locs blk) ->
      wc_scope P_wc1 G Γ (Scope locs blk) ->
      delast_scope f_dl f_add sub (Scope locs blk) st = (s', st') ->
      (forall Γ Γty Γ' sub blk' st st',
          (forall x ty, HasClock Γ x ty -> HasClock Γ' x ty) ->
          (forall x ty, HasClock Γ x ty -> IsLast Γ x -> HasClock Γ' (rename_in_var sub x) ty) ->
          incl (map fst Γ) Γty ->
          (forall x, Env.In x sub -> In x Γty) ->
          P_nd Γty blk ->
          P_wc1 Γ blk ->
          f_dl sub blk st = (blk', st') ->
          P_wc2 Γ' blk') ->
      (forall Γ blks1 blks2,
          Forall (wc_block G Γ) blks1 ->
          P_wc2 Γ blks2 ->
          P_wc2 Γ (f_add blks1 blks2)) ->
      wc_scope P_wc2 G Γ' s'.

  Lemma delast_block_wc {PSyn prefs} (G: @global PSyn prefs) : forall blk sub Γ Γty Γ' blk' st st',
      (forall x ck, HasClock Γ x ck -> HasClock Γ' x ck) ->
      (forall x ck, HasClock Γ x ck -> IsLast Γ x -> HasClock Γ' (rename_in_var sub x) ck) ->
      incl (map fst Γ) Γty ->
      (forall x, Env.In x sub -> In x Γty) ->
      NoDupLocals Γty blk ->
      wc_block G Γ blk ->
      delast_block sub blk st = (blk', st') ->
      wc_block G Γ' blk'.

  Lemma delast_outs_and_block_wc {PSyn prefs} (G: @global PSyn prefs) : forall ins outs blk blk' st st',
      let Γ := senv_of_ins ins ++ senv_of_decls outs in
      let Γ' := senv_of_ins ins ++ @senv_of_decls exp (map (fun xtc => (fst xtc, (fst (fst (fst (snd xtc))), snd (fst (fst (snd xtc))), 1%positive, None))) outs) in
      NoDupMembers Γ ->
      NoDupLocals (map fst Γ) blk ->
      wc_env (map (fun '(x, (_, ck, _)) => (x, ck)) ins ++ map (fun '(x, (_, ck, _, _)) => (x, ck)) outs) ->
      Forall (fun '(_, (_, ck, _, o)) => LiftO True (fun '(e, _) => wc_exp G Γ e /\ clockof e = [ck]) o) outs ->
      wc_block G Γ blk ->
      delast_outs_and_block outs blk st = (blk', st') ->
      wc_block G Γ' blk'.


  Lemma delast_node_wc : forall G1 G2 (n : @node _ _),
      global_iface_incl G1 G2 ->
      wc_node G1 n ->
      wc_node G2 (delast_node n).

  Theorem delast_global_wc : forall G,
      wc_global G ->
      wc_global (delast_global G).

End DLCLOCKING.

Module DLClockingFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Cks : CLOCKS Ids Op OpAux)
       (Senv : STATICENV Ids Op OpAux Cks)
       (Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Clo : LCLOCKING Ids Op OpAux Cks Senv Syn)
       (DL : DELAST Ids Op OpAux Cks Senv Syn)
       <: DLCLOCKING Ids Op OpAux Cks Senv Syn Clo DL.
  Include DLCLOCKING Ids Op OpAux Cks Senv Syn Clo DL.
End DLClockingFun.