From Velus Require Import Common.
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 Omega.
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 CESyn : CESYNTAX Op).

Equations

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

  Implicit Type eqn: 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
      }.

Program

  Definition global := list node.

  Implicit Type G: global.

  Definition find_node (f : ident) : global -> option node :=
    List.find (fun n=> ident_eqb n.(n_name) f).


  Lemma find_node_name:
    forall G f n,
      find_node f G = Some n ->
      n.(n_name) = f.

  Lemma find_node_other:
    forall f node G node',
      node.(n_name) <> f ->
      (find_node f (node::G) = Some node'
       <-> find_node f G = Some node').

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

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

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

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

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

  Definition gather_mem_eq (eq: equation): list ident :=
    match eq with
    | EqDef _ _ _
    | EqApp _ _ _ _ _ => []
    | EqFby x _ _ _ => [x]
    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.


  Lemma In_gather_mems_cons:
    forall eq eqs x,
      In x (gather_mems (eq :: eqs))
      <-> (In x (gather_mem_eq eq) \/ In x (gather_mems eqs)).

  Lemma In_gather_insts_cons:
    forall eq eqs x,
      InMembers x (gather_insts (eq :: eqs))
      <-> (InMembers x (gather_inst_eq eq) \/ InMembers x (gather_insts eqs)).

  Lemma In_gather_mems_dec:
    forall x eqs,
      { In x (gather_mems eqs) } + { ~In x (gather_mems eqs) }.

  Lemma In_gather_insts_dec:
    forall i eqs,
      { InMembers i (gather_insts eqs) } + { ~InMembers i (gather_insts eqs) }.

End NLSYNTAX.

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