Module NLClocking

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.NormLast.NormLast.

Module Type NLCLOCKING
       (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 NL : NORMLAST Ids Op OpAux Cks Senv Syn).

  Import Fresh Notations Facts Tactics.

Phase 1

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

    Variable sub : Env.t ident.

    Lemma init_exp_clockof : forall e,
        clockof (init_exp sub e) = clockof e.

    Corollary init_exp_clocksof : forall es,
        clocksof (map (init_exp sub) es) = clocksof es.

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

    Corollary init_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 (init_exp sub) es)).

    Variable Γ Γ' : static_env.

    Hypothesis Hck : forall x ck, HasClock Γ x ck -> HasClock Γ' x ck.
    Hypothesis Hvar : forall x y ck, Env.find x sub = Some y -> HasClock Γ x ck -> HasClock Γ' y ck.
    Hypothesis Hlast : forall x, Env.find x sub = None -> IsLast Γ x -> IsLast Γ' x.

    Lemma init_exp_wc : forall e,
        wc_exp G Γ e ->
        wc_exp G Γ' (init_exp sub e).

    Lemma init_equation_wc : forall eq,
        wc_equation G Γ eq ->
        wc_equation G Γ' (init_equation sub eq).

    Lemma init_block_wc : forall blk,
        unnested_block blk ->
        wc_block G Γ blk ->
        wc_block G Γ' (init_block sub blk).

  End init_block.

  Lemma init_top_block_wc {PSyn prefs} (G: @global PSyn prefs) : forall ins outs blk outs' blk' st st',
      unnested outs blk ->
      NoDupMembers (ins ++ senv_of_decls outs) ->
      NoDupLocals (map fst (ins ++ senv_of_decls outs)) blk ->
      Forall (fun '(x, (_, ck, _, _)) => wc_clock (idck (ins ++ senv_of_decls outs)) ck) outs ->
      wc_block G (ins ++ senv_of_decls outs) blk ->
      init_top_block outs blk st = (outs', blk', st') ->
      wc_block G (ins ++ senv_of_decls outs') blk'.

Phase 2

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

    Variable sub : Env.t ident.

    Lemma rename_exp_clockof : forall e,
        clockof (rename_exp sub e) = clockof e.

    Corollary rename_exp_clocksof : forall es,
        clocksof (map (rename_exp sub) es) = clocksof es.

    Lemma rename_exp_nclockof : forall e,
        nclockof (rename_exp sub e) = nclockof e.

    Corollary rename_exp_nclocksof : forall es,
        nclocksof (map (rename_exp sub) es) = nclocksof es.

    Variable Γ Γ' : static_env.

    Hypothesis Hty : forall x ck, HasClock Γ x ck -> HasClock Γ' x ck.
    Hypothesis Hvar : forall x y ck, Env.find x sub = Some y -> HasClock Γ x ck -> HasClock Γ' y ck.
    Hypothesis Hlast : forall x, Env.find x sub = None -> IsLast Γ x -> IsLast Γ' x.
    Hypothesis Hnlast : forall x y, Env.find x sub = Some y -> IsLast Γ x -> IsLast Γ' y.

    Lemma rename_exp_wc : forall e,
        wc_exp G Γ e ->
        wc_exp G Γ' (rename_exp sub e).

    Lemma rename_block_wc : forall blk,
        unnested_block blk ->
        wc_block G Γ blk ->
        Forall (wc_block G Γ') (rename_block sub blk).

  End rename_block.

  Lemma output_top_block_wc {PSyn prefs} (G: @global PSyn prefs) : forall ins outs blk blk' st st',
      unnested outs blk ->
      NoDupMembers (ins ++ senv_of_decls outs) ->
      NoDupLocals (map fst (ins ++ senv_of_decls outs)) blk ->
      Forall (fun '(x, (_, ck, _, _)) => wc_clock (idck (ins ++ senv_of_decls outs)) ck) outs ->
      wc_block G (ins ++ senv_of_decls outs) blk ->
      output_top_block outs blk st = (blk', st') ->
      wc_block G (ins ++ senv_of_decls (remove_lasts outs)) blk'.

Phase 3

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

    Variable sub : Env.t ident.

    Variable Γ Γ' : static_env.

    Hypothesis Hty : forall x ck, HasClock Γ x ck -> HasClock Γ' x ck.
    Hypothesis Hvar : forall x y ck, Env.find x sub = Some y -> HasClock Γ x ck -> HasClock Γ' y ck.
    Hypothesis Hlast : forall x, Env.find x sub = None -> IsLast Γ x -> IsLast Γ' x.
    Hypothesis Hnlast : forall x y, Env.find x sub = Some y -> IsLast Γ x -> IsLast Γ' y.

    Lemma unnest_block_wc : forall blk,
        unnested_block blk ->
        wc_block G Γ blk ->
        wc_block G Γ' (unnest_block sub blk).
  End unnest_block.

  Lemma unnest_top_block_wc {PSyn prefs} (G: @global PSyn prefs) : forall ins outs blk blk' st st',
      unnested outs blk ->
      NoDupMembers (senv_of_ins ins ++ senv_of_decls outs) ->
      NoDupLocals (map fst (senv_of_ins ins ++ senv_of_decls outs)) blk ->
      wc_block G (senv_of_ins ins ++ senv_of_decls outs) blk ->
      unnest_top_block blk st = (blk', st') ->
      wc_block G (senv_of_ins ins ++ senv_of_decls outs) blk'.

  Lemma normlast_top_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 (remove_lasts outs) in
      unnested outs blk ->
      (exists ls : list ident, LastsDefined blk ls /\ Permutation.Permutation ls (lasts_of_decls outs)) ->
      NoDupMembers Γ ->
      NoDupLocals (map fst Γ) blk ->
      Forall (AtomOrGensym norm1_prefs) (map fst ins ++ map fst outs) ->
      GoodLocals norm1_prefs blk ->
      Forall (fun '(x, (_, ck, _, _)) => wc_clock (idck Γ) ck) outs ->
      wc_block G Γ blk ->
      normlast_top_block outs blk st = (blk', st') ->
      wc_block G Γ' blk'.


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

  Theorem normlast_global_wc : forall G,
      wc_global G ->
      wc_global (normlast_global G).


End NLCLOCKING.

Module NLClockingFun
       (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)
       (NL : NORMLAST Ids Op OpAux Cks Senv Syn)
       <: NLCLOCKING Ids Op OpAux Cks Senv Syn Clo NL.
  Include NLCLOCKING Ids Op OpAux Cks Senv Syn Clo NL.
End NLClockingFun.