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

From Velus Require Import Common Environment.
From Velus Require Import CommonTyping.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import Lustre.StaticEnv.
From Velus Require Import Lustre.LSyntax.
From Velus Require Fresh.
From Velus Require Import Lustre.Normalization.Unnesting.
From Velus Require Import Lustre.SubClock.SubClock.

Putting FBYs into normalized form

Module Type NORMFBY
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import 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 Unt : UNNESTING Ids Op OpAux Cks Senv Syn).

  Import Fresh Fresh.Notations Facts Tactics.
  Local Open Scope fresh_monad_scope.

  Module Import SC := SubClockFun Ids Op OpAux Cks Senv Syn.

  Open Scope bool_scope.

  Lemma norm2_not_in_norm1_prefs :
    ~PS.In norm2 norm1_prefs.

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

  Definition init_var_for_clock (ck : clock) : FreshAnn (ident * list equation) :=
    fun st => let (x, st') := fresh_ident None ((OpAux.bool_velus_type, ck)) st in
           ((x, [([x], [Efby [add_whens (Eenum 1 bool_velus_type) bool_velus_type ck]
                             [add_whens (Eenum 0 bool_velus_type) bool_velus_type ck]
                             [(bool_velus_type, ck)]])]), st').

  Fixpoint is_constant (e : exp) : bool :=
    match e with
    | Econst _ | Eenum _ _ => true
    | Ewhen [e] _ _ ([ty], _) => is_constant e
    | _ => false
    end.

  Definition init_type (ty : type) :=
    match ty with
    | Tprimitive cty => Econst (init_ctype cty)
    | Tenum _ _ => Eenum 0 ty
    end.

  Definition fby_iteexp (e0 : exp) (e : exp) (ann : ann) : FreshAnn (exp * list equation) :=
    let '(ty, ck) := ann in
    do (initid, eqs) <- init_var_for_clock ck;
    do px <- fresh_ident None (ty, ck);
    ret (Ecase (Evar initid (bool_velus_type, ck))
               [(1, [e0]); (0, [Evar px (ty, ck)])] None ([ty], ck),
         ([px], [Efby [add_whens (init_type ty) ty ck] [e] [ann]])::eqs).

  Definition arrow_iteexp (e0 : exp) (e : exp) (ann : ann) : FreshAnn (exp * list equation) :=
    let '(ty, ck) := ann in
    do (initid, eqs) <- init_var_for_clock ck;
    ret (Ecase (Evar initid (bool_velus_type, ck)) [(1, [e0]); (0, [e])] None
              ([ty], ck), eqs).

  Definition normfby_equation (to_cut : PS.t) (eq : equation) : FreshAnn (list equation) :=
    match eq with
    | ([x], [Efby [e0] [e] [ann]]) =>
      let '(ty, ck) := ann in
      if is_constant e0 then
        if PS.mem x to_cut then
          do x' <- fresh_ident None (ty, ck);
          ret [([x], [Evar x' ann]); ([x'], [Efby [e0] [e] [ann]])]
        else ret [eq]
      else
        do (fby, eqs) <- fby_iteexp e0 e ann; ret (([x], [fby])::eqs)
    | ([x], [Earrow [e0] [e] [ann]]) =>
      do (ite, eqs) <- arrow_iteexp e0 e ann;
      ret (([x], [ite])::eqs)
    | _ => ret [eq]
    end.

  Fixpoint normfby_block (to_cut : PS.t) (d : block) : FreshAnn (list block) :=
    match d with
    | Beq eq =>
      do eq' <- normfby_equation to_cut eq;
      ret (map Beq eq')
    | Breset [d] (Evar x (ty, ckr)) =>
      do blocks' <- normfby_block to_cut d;
      ret (map (fun d => Breset [d] (Evar x (ty, ckr))) blocks')
    | _ => ret [d]
    end.

  Definition normfby_blocks (to_cut : PS.t) (blocks : list block) : FreshAnn (list block) :=
    do blocks' <- mmap (normfby_block to_cut) blocks;
    ret (concat blocks').


  Local Ltac destruct_to_singl l :=
    destruct l; [|destruct l]; auto.

  Fact normfby_equation_spec : forall to_cut xs es,
      (exists x e0 e ann,
          xs = [x] /\
          es = [Efby [e0] [e] [ann]] /\
          is_constant e0 = true /\
          normfby_equation to_cut (xs, es) =
          (let '(ty, ck) := ann in
           if PS.mem x to_cut then
             do x' <- fresh_ident None (ty, ck);
             ret [([x], [Evar x' ann]); ([x'], es)]
           else ret [(xs, es)]))
      \/ (exists x e0 e ann,
          xs = [x] /\
          es = [Efby [e0] [e] [ann]] /\
          is_constant e0 = false /\
          normfby_equation to_cut (xs, es) =
          (do (fby, eqs) <- fby_iteexp e0 e ann;
           ret (([x], [fby])::eqs)))
      \/ (exists x e0 e ann,
            xs = [x] /\
            es = [Earrow [e0] [e] [ann]] /\
            normfby_equation to_cut (xs, es) =
            (do (ite, eqs) <- arrow_iteexp e0 e ann;
             ret (([x], [ite])::eqs)))
      \/ normfby_equation to_cut (xs, es) = (ret [(xs, es)]).

  Ltac inv_normfby_equation Hfby to_cut eq :=
    let Hspec := fresh "Hspec" in
    let Hconst := fresh "Hconst" in
    let Hr := fresh "Hr" in
    destruct eq as [xs es];
    specialize (normfby_equation_spec to_cut xs es) as
        [(?&?&?&?&?&?&Hconst&Hspec)|[(?&?&?&?&?&?&Hconst&Hspec)|[(?&?&?&?&?&?&Hspec)|Hspec]]];
    subst; rewrite Hspec in Hfby; clear Hspec; repeat inv_bind; auto.

Preservation of st_follows

  Fact init_var_for_clock_st_follows : forall ck res st st',
      init_var_for_clock ck st = (res, st') ->
      st_follows st st'.
  Global Hint Resolve init_var_for_clock_st_follows : norm.

  Fact fby_iteexp_st_follows : forall e0 e ann res st st',
      fby_iteexp e0 e ann st = (res, st') ->
      st_follows st st'.
  Global Hint Resolve fby_iteexp_st_follows : norm.

  Fact arrow_iteexp_st_follows : forall e0 e ann res st st',
      arrow_iteexp e0 e ann st = (res, st') ->
      st_follows st st'.
  Global Hint Resolve arrow_iteexp_st_follows : norm.

  Fact normfby_equation_st_follows : forall to_cut eq eqs' st st',
      normfby_equation to_cut eq st = (eqs', st') ->
      st_follows st st'.
  Global Hint Resolve normfby_equation_st_follows : norm.

  Fact normfby_block_st_follows : forall to_cut d blocks' st st',
      normfby_block to_cut d st = (blocks', st') ->
      st_follows st st'.
  Global Hint Resolve normfby_block_st_follows : norm.

The variables generated are a permutation of the ones contained in the state

  Fact init_var_for_clock_vars_perm : forall ck id eqs st st',
      init_var_for_clock ck st = ((id, eqs), st') ->
      Permutation (flat_map fst eqs++st_ids st) (st_ids st').

  Fact fby_iteexp_vars_perm : forall e0 e ann e' eqs' st st',
      fby_iteexp e0 e ann st = (e', eqs', st') ->
      Permutation (flat_map fst eqs'++st_ids st) (st_ids st').

  Fact arrow_iteexp_vars_perm : forall e0 e ann e' eqs' st st',
      arrow_iteexp e0 e ann st = (e', eqs', st') ->
      Permutation (flat_map fst eqs'++st_ids st) (st_ids st').

  Fact normfby_equation_vars_perm : forall to_cut eq eqs' st st',
      normfby_equation to_cut eq st = (eqs', st') ->
      Permutation (flat_map fst eqs'++st_ids st) (fst eq++st_ids st').

  Lemma normfby_block_vars_perm : forall G blk blks' xs st st',
      VarsDefinedComp blk xs ->
      normfby_block G blk st = (blks', st') ->
      exists ys, Forall2 VarsDefinedComp blks' ys /\ Permutation (concat ys ++ st_ids st) (xs ++ st_ids st').

  Corollary normfby_blocks_vars_perm : forall G blks blks' xs st st',
      Forall2 VarsDefinedComp blks xs ->
      normfby_blocks G blks st = (blks', st') ->
      exists ys, Forall2 VarsDefinedComp blks' ys /\ Permutation (concat ys ++ st_ids st) (concat xs ++ st_ids st').

Additional props

  Fact init_var_for_clock_In : forall ck id eqs' st st',
      init_var_for_clock ck st = (id, eqs', st') ->
      In (id, (bool_velus_type, ck)) (st_anns st').

Specification of a normalized node

  Inductive normalized_constant : exp -> Prop :=
  | constant_Econst : forall c,
      normalized_constant (Econst c)
  | constant_Eenum : forall k ty,
      normalized_constant (Eenum k ty)
  | constant_Ewhen : forall e x b ty cl,
      normalized_constant e ->
      normalized_constant (Ewhen [e] x b ([ty], cl)).

  Inductive normalized_equation {PSyn prefs} (G : @global PSyn prefs) : PS.t -> equation -> Prop :=
  | normalized_eq_Eapp : forall out xs f n es er lann,
      Forall normalized_lexp es ->
      find_node f G = Some n ->
      Forall2 noops_exp (map (fun '(_, (_, ck, _)) => ck) n.(n_in)) es ->
      Forall (fun e => exists x ann, e = Evar x ann) er ->
      normalized_equation G out (xs, [Eapp f es er lann])
  | normalized_eq_Efby : forall out x e0 e ann,
      ~PS.In x out ->
      normalized_constant e0 ->
      normalized_lexp e ->
      normalized_equation G out ([x], [Efby [e0] [e] [ann]])
  | normalized_eq_Eextcall : forall out x f es ann,
      Forall normalized_lexp es ->
      normalized_equation G out ([x], [Eextcall f es ann])
  | normalized_eq_cexp : forall out x e,
      normalized_cexp e ->
      normalized_equation G out ([x], [e]).

  Inductive normalized_block {PSyn prefs} (G : @global PSyn prefs) : PS.t -> block -> Prop :=
  | normalized_Beq : forall out eq,
      normalized_equation G out eq ->
      normalized_block G out (Beq eq)
  | normalized_Breset : forall out block x ann,
      normalized_block G out block ->
      normalized_block G out (Breset [block] (Evar x ann)).

  Inductive normalized_node {PSyn1 PSyn2 prefs1 prefs2} (G : @global PSyn1 prefs1) : (@node PSyn2 prefs2) -> Prop :=
  | normalized_Node : forall n locs blks,
      n_block n = Blocal (Scope locs blks) ->
      Forall (fun '(_, (_, _, _, o)) => o = None) locs ->
      Forall (normalized_block G (ps_from_list (List.map fst (n_out n)))) blks ->
      normalized_node G n.

  Definition normalized_global {PSyn prefs} : @global PSyn prefs -> Prop :=
    wt_program normalized_node.

  Global Hint Constructors normalized_constant normalized_equation normalized_block : norm.

normalized_node implies unnested_node

  Fact constant_normalized_lexp : forall e,
      normalized_constant e ->
      normalized_lexp e.

  Fact normalized_eq_unnested_eq {PSyn prefs} : forall (G : @global PSyn prefs) to_cut eq,
      normalized_equation G to_cut eq ->
      unnested_equation G eq.

  Fact normalized_block_unnested_block {PSyn prefs} : forall (G : @global PSyn prefs) to_cut block,
      normalized_block G to_cut block ->
      unnested_block G block.

  Fact normalized_node_unnested_node {PSyn1 PSyn2 prefs1 prefs2} : forall (G : @global PSyn1 prefs1) (n : @node PSyn2 prefs2),
      normalized_node G n ->
      unnested_node G n.

  Fact normalized_global_unnested_global {PSyn prefs} : forall (G : @global PSyn prefs),
      normalized_global G ->
      unnested_global G.

equations and expressions are normalized

  Fact add_whens_is_constant : forall ty ck e,
      normalized_constant e ->
      normalized_constant (add_whens e ty ck).

  Fact add_whens_normalized_lexp : forall ty ck e,
      normalized_lexp e ->
      normalized_lexp (add_whens e ty ck).

  Fact is_constant_normalized_constant : forall e,
      is_constant e = true <->
      normalized_constant e.

  Fact init_var_for_clock_normalized_eq {PSyn prefs} : forall (G : @global PSyn prefs) ck id eqs' out st st',
      PS.For_all (AtomOrGensym norm1_prefs) out ->
      init_var_for_clock ck st = (id, eqs', st') ->
      Forall (normalized_equation G out) eqs'.

  Fact normfby_equation_normalized_eq {PSyn prefs} : forall (G : @global PSyn prefs) out to_cut eq eqs' st st',
      PS.For_all (AtomOrGensym norm1_prefs) out ->
      unnested_equation G eq ->
      PS.Subset out to_cut ->
      normfby_equation to_cut eq st = (eqs', st') ->
      Forall (normalized_equation G out) eqs'.

  Fact normfby_block_normalized_block {PSyn prefs} : forall (G : @global PSyn prefs) out to_cut d blocks' st st',
      PS.For_all (AtomOrGensym norm1_prefs) out ->
      unnested_block G d ->
      PS.Subset out to_cut ->
      normfby_block to_cut d st = (blocks', st') ->
      Forall (normalized_block G out) blocks'.

  Corollary normfby_blocks_normalized_block {PSyn prefs} : forall (G : @global PSyn prefs) out to_cut blocks blocks' st st',
      PS.For_all (AtomOrGensym norm1_prefs) out ->
      Forall (unnested_block G) blocks ->
      PS.Subset out to_cut ->
      normfby_blocks to_cut blocks st = (blocks', st') ->
      Forall (normalized_block G out) blocks'.

  Lemma normfby_block_GoodLocals to_cut : forall prefs blk blk' st st',
      GoodLocals prefs blk ->
      normfby_block to_cut blk st = (blk', st') ->
      Forall (GoodLocals prefs) blk'.

  Corollary normfby_blocks_GoodLocals to_cut : forall prefs blks blks' st st',
      Forall (GoodLocals prefs) blks ->
      normfby_blocks to_cut blks st = (blks', st') ->
      Forall (GoodLocals prefs) blks'.

  Lemma normfby_block_NoDupLocals G env : forall blk blks' st st',
      NoDupLocals env blk ->
      normfby_block G blk st = (blks', st') ->
      Forall (NoDupLocals env) blks'.

  Corollary normfby_blocks_NoDupLocals G env : forall blks blks' st st',
      Forall (NoDupLocals env) blks ->
      normfby_blocks G blks st = (blks', st') ->
      Forall (NoDupLocals env) blks'.

nolocal

  Lemma normfby_block_nolocal : forall to_cut blk blks' st st',
      nolocal_block blk ->
      normfby_block to_cut blk st = (blks', st') ->
      Forall nolocal_block blks'.

  Corollary normfby_blocks_nolocal : forall to_cut blks blks' st st',
      Forall nolocal_block blks ->
      normfby_blocks to_cut blks st = (blks', st') ->
      Forall nolocal_block blks'.

Cut next cycles Cycles of the form x = 0 fby y; y = 0 fby x; leads to a non schedulable program in STC: next x := y; next y := x; because a register cannot be used after it is updated. The solution is to cut this cycle: x = 0 fby y; y' = 0 fby x; y = y'; which can be scheduled to y = y'; next y' := x; next x := y; The function `cut_next_cycles` tries to calculate a small set of identifiers that need to be cut for the program to be schedulable. It exploits the unnested form of the program.

  Fixpoint free_vars_lexp (e : exp) : PS.t :=
    match e with
    | Econst _ | Eenum _ _ => PS.empty
    | Evar x _ => PS.singleton x
    | Eunop _ e1 _ => free_vars_lexp e1
    | Ebinop _ e1 e2 _ => PS.union (free_vars_lexp e1) (free_vars_lexp e2)
    | Ewhen [e] (x, _) _ _ => PS.add x (free_vars_lexp e)
    | _ => PS.empty
    end.

  Fixpoint next_dep (blk : block) : option (ident * PS.t) :=
    match blk with
    | Beq ([x], [Efby _ [e] _]) => Some (x, free_vars_lexp e)
    | Breset [blk] _ => next_dep blk
    | _ => None
    end.

  Definition cut_next_dep (deps : Env.t PS.t) (to_cut : PS.t) (blk : block) : (Env.t PS.t * PS.t) :=
    match next_dep blk with
    | None => (deps, to_cut)
    | Some (x, used) =>
        let used_trans := PS.fold (fun x s => match Env.find x deps with
                                           | Some s' => PS.union s s'
                                           | None => s
                                           end) used used in
        if PS.mem x used_trans
        then (deps, PS.add x to_cut)
        else (Env.add x used_trans deps, to_cut)
    end.

  Definition cut_next_cycles (blks : list block) : PS.t :=
    snd (fold_left (fun '(deps, to_cut) => cut_next_dep deps to_cut) blks (Env.empty _, PS.empty)).

Normalization of a full node

  Program Definition normfby_node (n : @node nolocal norm1_prefs) : @node nolocal norm2_prefs :=
    {| n_name := n_name n;
       n_hasstate := n_hasstate n;
       n_in := n_in n;
       n_out := n_out n;
       n_block := match (n_block n) with
                  | Blocal (Scope vars blks) =>
                    let res := normfby_blocks (PS.union (ps_from_list (map fst (n_out n))) (cut_next_cycles blks)) blks init_st in
                    let nvars := st_anns (snd res) in
                    Blocal (Scope (vars++map (fun xtc => (fst xtc, ((fst (snd xtc)), snd (snd xtc), xH, None))) nvars) (fst res))
                  | blk => blk
                  end;
       n_ingt0 := n_ingt0 n;
       n_outgt0 := n_outgt0 n;
    |}.

  Global Program Instance normfby_node_transform_unit: TransformUnit node node :=
    { transform_unit := normfby_node }.

  Global Program Instance normfby_global_without_units : TransformProgramWithoutUnits (@global nolocal norm1_prefs) (@global nolocal norm2_prefs) :=
    { transform_program_without_units := fun g => Global g.(types) g.(externs) [] }.

  Definition normfby_global : @global nolocal norm1_prefs -> @global nolocal norm2_prefs := transform_units.

normfby_global produces an equivalent global

  Fact normfby_global_eq : forall G,
      global_iface_eq G (normfby_global G).

  Fact normfby_nodes_names {PSyn prefs} : forall (a : @node PSyn prefs) nds,
      Forall (fun n => (n_name a <> n_name n)%type) nds ->
      Forall (fun n => (n_name a <> n_name n)%type) (map normfby_node nds).

er normalization, a global is normalized

  Fact normfby_node_normalized_node {PSyn prefs} : forall (G : @global PSyn prefs) n,
      unnested_node G n ->
      normalized_node G (normfby_node n).

  Fact normfby_global_normalized_global : forall G,
      unnested_global G ->
      normalized_global (normfby_global G).
End NORMFBY.

Module NormFbyFun
       (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)
       (Unt : UNNESTING Ids Op OpAux Cks Senv Syn)
       <: NORMFBY Ids Op OpAux Cks Senv Syn Unt.
  Include NORMFBY Ids Op OpAux Cks Senv Syn Unt.
End NormFbyFun.