From Velus Require Import Common.
From Velus Require Import CommonProgram.
From Velus Require Import Operators.
From Velus Require Import CoreExpr.CESyntax.
From Velus Require Import Clocks.
From Coq Require Import PArith.
From Coq Require Import Sorting.Permutation.

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

The NLustre dataflow language

Module Type NLSYNTAX
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Ids Op)
       (Import Cks : CLOCKS Ids Op OpAux)
       (Import CESyn : CESYNTAX Ids Op OpAux Cks).

Equations

  Inductive equation : Type :=
  | EqDef : ident -> clock -> rhs -> equation
  | EqApp : list ident -> clock -> ident -> list exp -> list (ident * clock) -> equation
  | EqFby : ident -> clock -> const -> exp -> list (ident * clock) -> equation.

Node

  Definition var_defined (eq: equation) : list ident :=
    match eq with
    | EqDef x _ _ => [x]
    | EqApp x _ _ _ _ => x
    | EqFby x _ _ _ _ => [x]
    end.

  Definition vars_defined (eqs: list equation) : list ident :=
    flat_map var_defined eqs.

  Definition is_fby (eq: equation) : bool :=
    match eq with
    | EqFby _ _ _ _ _ => true
    | _ => false
    end.

  Definition is_app (eq: equation) : bool :=
    match eq with
    | EqApp _ _ _ _ _ => true
    | _ => false
    end.

  Definition is_def (eq: equation) : bool :=
    match eq with
    | EqDef _ _ _ => true
    | _ => false
    end.

  Record node : Type :=
    mk_node {
        n_name : ident;
        n_in : list (ident * (type * clock));
        n_out : list (ident * (type * clock));
        n_vars : list (ident * (type * clock));
        n_eqs : list equation;

        n_ingt0 : 0 < length n_in;
        n_outgt0 : 0 < length n_out;
        n_defd : Permutation (vars_defined n_eqs)
                               (map fst (n_vars ++ n_out));
        n_vout : forall out, In out (map fst n_out) ->
                          ~ In out (vars_defined (filter is_fby n_eqs));
        n_nodup : NoDupMembers (n_in ++ n_vars ++ n_out);
        n_good : Forall (AtomOrGensym (PSP.of_list gensym_prefs)) (map fst (n_in ++ n_vars ++ n_out)) /\ atom n_name
      }.

  Global Instance node_unit: ProgramUnit node :=
    { name := n_name; }.

Program

  Record global := Global {
                       types : list type;
                       externs : list (ident * (list ctype * ctype));
                       nodes : list node
                     }.

  Global Program Instance global_program: Program node global :=
    { units := nodes;
      update := fun g => Global g.(types) g.(externs) }.

  Definition find_node (f: ident) (G: global) :=
    option_map fst (find_unit f G).

Structural properties

  Lemma find_node_now:
    forall f n G enums externs,
      n.(n_name) = f ->
      find_node f (Global enums externs (n::G)) = Some n.

Proof.

    intros * Heq; subst.
    unfold find_node, find_unit; simpl.
    destruct (ident_eq_dec _ _); simpl; congruence.
  Qed.

  Lemma find_node_other:
    forall f node G enums externs,
      node.(n_name) <> f ->
      find_node f (Global enums externs (node::G)) = find_node f (Global enums externs G).

Proof.

    unfold find_node, option_map; intros ??? enums externs Hneq.
    erewrite find_unit_other with (p' := Global enums externs G);
      simpl; eauto; try reflexivity.
    unfold equiv_program; reflexivity.
  Qed.

  Lemma find_node_In:
    forall G f n,
      find_node f G = Some n ->
      n.(n_name) = f /\ In n G.(nodes).

Proof.

    unfold find_node, option_map; intros * Find.
    apply option_map_inv in Find as ((?&?) & Find & E); inv E.
    apply find_unit_In in Find; auto.
  Qed.

  Lemma find_node_Exists:
    forall f enums externs G,
      find_node f (Global enums externs G) <> None <-> List.Exists (fun n=> f = n.(n_name)) G.

Proof.

    unfold find_node; intros.
    rewrite option_map_None.
    rewrite find_unit_Exists; reflexivity.
  Qed.

  Lemma find_node_split:
    forall f G node,
      find_node f G = Some node ->
      exists bG aG,
        G.(nodes) = bG ++ node :: aG.

Proof.

    unfold find_node; intros * Find.
    apply option_map_inv in Find as ((?&?) & Find & E); inv E.
    apply find_unit_spec in Find as (?& us & E &?).
    unfold units, global_program in *.
    rewrite E; eauto.
  Qed.

  Lemma Forall_not_find_node_None:
    forall G f enums externs,
      Forall (fun n => ~(f = n.(n_name))) G <-> find_node f (Global enums externs G) = None.

Proof.

    unfold find_node; intros.
    rewrite option_map_None, find_unit_None; reflexivity.
  Qed.

  Lemma is_filtered_eqs:
    forall eqs,
      Permutation
        (filter is_def eqs ++ filter is_app eqs ++ filter is_fby eqs)
        eqs.

Proof.

    induction eqs as [|eq eqs]; auto.
    destruct eq; simpl.
    - now apply Permutation_cons.
    - rewrite <-Permutation_cons_app.
      apply Permutation_cons; reflexivity.
      now symmetry.
    - symmetry.
      rewrite <-Permutation_app_assoc.
      apply Permutation_cons_app.
      rewrite Permutation_app_assoc.
      now symmetry.
  Qed.

  Lemma is_filtered_vars_defined:
    forall eqs,
      Permutation
        (vars_defined (filter is_def eqs) ++ vars_defined (filter is_app eqs) ++ vars_defined (filter is_fby eqs))
        (vars_defined eqs).

Proof.

    simpl.
    induction eqs as [|[] eqs]; simpl; auto.
    - rewrite Permutation_app_comm, 2 Permutation_app_assoc.
      apply Permutation_app_head.
      rewrite <-Permutation_app_assoc, Permutation_app_comm; auto.
    - symmetry.
      rewrite <-Permutation_app_assoc.
      apply Permutation_cons_app.
      symmetry.
      rewrite Permutation_app_assoc; auto.
  Qed.

  Lemma NoDup_var_defined_n_eqs:
    forall n,
      NoDup (vars_defined n.(n_eqs)).

Proof.

    intro n.
    rewrite n.(n_defd).
    apply fst_NoDupMembers.
    apply (NoDupMembers_app_r _ _ n.(n_nodup)).
  Qed.

Lemma n_eqsgt0:
forall n, 0 < length n.(n_eqs).

Proof.

    intro.
    pose proof (n_defd n) as Defd.
    pose proof (n_outgt0 n) as Out.
    unfold vars_defined in Defd.
    apply Permutation_length in Defd.
    rewrite flat_map_length, map_length, app_length in Defd.
    destruct (n_eqs n); simpl in *; lia.
  Qed.

  Definition gather_mem_eq (eq: equation): list (ident * type) :=
    match eq with
    | EqDef _ _ _
    | EqApp _ _ _ _ _ => []
    | EqFby x _ _ e _ => [(x, typeof e)]
    end.

  Definition gather_inst_eq (eq: equation): list (ident * ident) :=
    match eq with
    | EqDef _ _ _
    | EqFby _ _ _ _ _ => []
    | EqApp i _ f _ _ =>
      match i with
      | [] => []
      | i :: _ => [(i,f)]
      end
    end.

  Definition gather_app_vars_eq (eq: equation): list ident :=
    match eq with
    | EqDef _ _ _
    | EqFby _ _ _ _ _ => []
    | EqApp xs _ _ _ _ => tl xs
    end.

  Definition gather_mems := flat_map gather_mem_eq.
  Definition gather_insts := flat_map gather_inst_eq.
  Definition gather_app_vars := flat_map gather_app_vars_eq.

Basic syntactical properties

  Lemma node_in_not_nil:
    forall n,
      n.(n_in) <> [].

Proof.

    intros n E; pose proof (n_ingt0 n) as H.
    rewrite E in H; simpl in H; lia.
  Qed.

  Lemma node_out_not_nil:
    forall n,
      n.(n_out) <> [].

Proof.

    intros n E; pose proof (n_outgt0 n) as H.
    rewrite E in H; simpl in H; lia.
  Qed.

  Lemma InMembers_gather_mems_In_vars_defined:
    forall eqs x,
      InMembers x (gather_mems eqs) -> In x (vars_defined eqs).

Proof.

    induction eqs as [|[]]; simpl; auto; intros * Hin.
    - apply in_app; auto.
    - intuition.
  Qed.

  Lemma n_nodup_gather_mems:
    forall n,
      NoDup (gather_mems (n_eqs n)).

Proof.

    intro.
    pose proof (NoDup_var_defined_n_eqs n) as Hnodup.
    unfold gather_mems, vars_defined in *.
    induction (n_eqs n) as [|[]]; simpl in *; intros; auto.
    - constructor.
    - inv Hnodup; auto.
    - rewrite Permutation_app_comm in Hnodup; apply NoDup_app_weaken in Hnodup; auto.
    - inv Hnodup; constructor; auto.
      apply NotInMembers_NotIn; auto.
      intros Hin; apply InMembers_gather_mems_In_vars_defined in Hin; contradiction.
  Qed.

Interface equivalence between nodes

Section interface_eq.

Nodes are equivalent if their interface are equivalent, that is if they have the same identifier and the same input/output types

    Definition node_iface_eq (n1 n2 : node) :=
      n1.(n_name) = n2.(n_name) /\
      n1.(n_in) = n2.(n_in) /\
      n1.(n_out) = n2.(n_out).

Globals are equivalent if they contain equivalent nodes

    Definition global_iface_eq (G1 G2 : global) : Prop :=
      types G1 = types G2
      /\ externs G1 = externs G2
      /\ forall f, orel2 node_iface_eq (find_node f G1) (find_node f G2).

    Lemma global_iface_eq_nil : forall enums externs,
        global_iface_eq (Global enums externs []) (Global enums externs []).

Proof.

      unfold global_iface_eq, find_node.
      repeat split; auto.
      intros *; simpl. constructor.
    Qed.

    Lemma global_iface_eq_cons : forall enums externs nds nds' n n',
        global_iface_eq (Global enums externs nds) (Global enums externs nds') ->
        n.(n_name) = n'.(n_name) ->
        n.(n_in) = n'.(n_in) ->
        n.(n_out) = n'.(n_out) ->
        global_iface_eq (Global enums externs (n::nds)) (Global enums externs (n'::nds')).

Proof.

      intros * (?&Heq1&Heq2) Hname Hin Hout.
      repeat split; auto. intros ?.
      destruct (Pos.eq_dec (n_name n) f); subst.
      - simpl. repeat rewrite find_node_now; auto.
        repeat constructor; auto.
      - repeat rewrite find_node_other; auto.
        congruence.
    Qed.

    Lemma global_iface_eq_find : forall G G' f n,
        global_iface_eq G G' ->
        find_node f G = Some n ->
        exists n', (find_node f G' = Some n' /\
               node_iface_eq n n').

Proof.

      intros G G' f n (_&_&Hglob) Hfind.
      specialize (Hglob f).
      inv Hglob; try congruence.
      rewrite Hfind in H. inv H.
      exists sy. auto.
    Qed.

End interface_eq.

Global Instance node_iface_eq_refl : Reflexive node_iface_eq.

Proof.

intros n. repeat split.
Qed.

Global Instance node_iface_eq_sym : Symmetric node_iface_eq.

Proof.

    intros ?? (?&?&?).
    constructor; auto.
  Qed.

Global Instance node_iface_eq_trans : Transitive node_iface_eq.

Proof.

    intros n1 n2 n3 H12 H23.
    destruct H12 as [? [? ?]].
    destruct H23 as [? [? ?]].
    repeat split; etransitivity; eauto.
  Qed.

Global Instance global_eq_refl : Reflexive global_iface_eq.

Proof.

    intros G. repeat split; intros; try reflexivity.
    destruct (find_node f G); constructor.
    apply node_iface_eq_refl.
  Qed.

Global Instance global_iface_eq_sym : Symmetric global_iface_eq.

Proof.

    intros ?? (?&?&?).
    repeat split; auto.
    intros f. specialize (H1 f).
    inv H1; constructor; auto.
    apply node_iface_eq_sym; auto.
  Qed.

Fact global_iface_eq_trans : Transitive global_iface_eq.

Proof.

    intros n1 n2 n3 (?&?&H12) (?&?&H23).
    repeat split; try congruence.
    intros f. specialize (H12 f). specialize (H23 f).
    inv H12; inv H23; try congruence; constructor.
    rewrite <-H4 in H6. inv H6.
    eapply node_iface_eq_trans; eauto.
  Qed.

End NLSYNTAX.

Module NLSyntaxFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Cks : CLOCKS Ids Op OpAux)
       (CESyn : CESYNTAX Ids Op OpAux Cks)
       <: NLSYNTAX Ids Op OpAux Cks CESyn.
  Include NLSYNTAX Ids Op OpAux Cks CESyn.
End NLSyntaxFun.