Module NoDup

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

From Velus Require Import Common.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import NLustre.NLSyntax.
From Velus Require Import CoreExpr.CESyntax.
From Velus Require Import NLustre.IsVariable.
From Velus Require Import NLustre.IsDefined.
From Velus Require Import NLustre.Memories.

No duplication of variables



Module Type NODUP
       (Ids : IDS)
       (Op : OPERATORS)
       (Import CESyn : CESYNTAX Op)
       (Import Syn : NLSYNTAX Ids Op CESyn)
       (Import Mem : MEMORIES Ids Op CESyn Syn)
       (Import IsD : ISDEFINED Ids Op CESyn Syn Mem)
       (Import IsV : ISVARIABLE Ids Op CESyn Syn Mem IsD).

  Inductive NoDup_defs : list equation -> Prop :=
  | NDDNil: NoDup_defs nil
  | NDDEqDef:
      forall x ck e eqs,
        NoDup_defs eqs ->
        ~Is_defined_in x eqs ->
        NoDup_defs (EqDef x ck e :: eqs)
  | NDDEqApp:
      forall xs ck f e r eqs,
        NoDup_defs eqs ->
        (forall x, In x xs -> ~Is_defined_in x eqs) ->
        NoDup_defs (EqApp xs ck f e r :: eqs)
  | NDDEqFby:
      forall x ck v e eqs,
        NoDup_defs eqs ->
        ~Is_defined_in x eqs ->
        NoDup_defs (EqFby x ck v e :: eqs).

Properties


  Lemma NoDup_defs_cons:
    forall eq eqs,
      NoDup_defs (eq :: eqs) -> NoDup_defs eqs.
Proof.
    intros eq eqs Hndd.
    destruct eq; inversion_clear Hndd; assumption.
  Qed.

  Lemma not_Is_variable_in_memories:
    forall x eqs,
      PS.In x (memories eqs)
      -> NoDup_defs eqs
      -> ~Is_variable_in x eqs.
Proof.
    intros x eqs Hinm Hndd Hvar.

    induction eqs as [ | eq eqs IHeqs ].
    - inv Hvar.
    - assert (NoDup_defs eqs)
        by now eapply NoDup_defs_cons; eauto.

      unfold memories in *; simpl in *.
      destruct eq; simpl in *;
      match goal with
      | _ : context[ EqFby _ _ _ _ ] |- _ =>
        idtac
      | _ =>
        (* Case: eq ~ EqApp or eq ~ EqDef *)
        (assert (Is_defined_in x eqs)
          by now apply Is_defined_in_memories);
        (assert (Is_variable_in x eqs)
          by now inv Hvar; auto; exfalso; inv Hndd;
            match goal with
            | H: Is_variable_in_eq ?x (EqDef ?i _ _) |- _ => inv H
            | H: Is_variable_in_eq ?x (EqApp ?i _ _ _ _) |- _ => inv H
            end; firstorder);
        now apply IHeqs
      end.
      (* Case: eq ~ EqFby *)
      rewrite In_fold_left_memory_eq in Hinm.
      destruct Hinm.
      * assert (Is_defined_in x eqs)
          by now apply Is_defined_in_memories.
        assert (Is_variable_in x eqs)
          by now inv Hvar; auto; exfalso; inv Hndd;
            match goal with
            | H: Is_variable_in_eq ?x (EqFby ?i _ _ _) |- _ => inv H
            end.
        now apply IHeqs.
      * assert (x = i) as ->.
        {
          rewrite PSF.add_iff in H0.
          destruct H0; auto.
          exfalso; eapply not_In_empty; eauto.
        }

        assert (~ Is_variable_in i eqs)
          by now apply not_Is_defined_in_not_Is_variable_in;
          inv Hndd.

        assert (~ Is_variable_in_eq i (EqFby i c c0 e))
          by now intro His_var; inv His_var.

        now inv Hvar.
  Qed.

  Lemma NoDup_defs_NoDup_vars_defined:
    forall eqs,
      NoDup (vars_defined eqs) ->
      NoDup_defs eqs.
Proof.
    unfold vars_defined.
    induction eqs as [|eq eqs].
    - auto using NoDup_defs.
    - simpl. intro Hnodup.
      apply NoDup_app'_iff in Hnodup.
      destruct Hnodup as (Hnd1 & Hnd2 & Hni).
      apply IHeqs in Hnd2.
      destruct eq.
      + constructor; auto.
        simpl in *.
        intro Hdef.
        inv Hni. apply H1.
        now apply Is_defined_in_vars_defined.
      + constructor; auto.
        intros x Hin Hdef.
        simpl in *.
        eapply Forall_forall in Hin; eauto.
        apply Hin.
        now apply Is_defined_in_vars_defined.
      + constructor; auto.
        simpl in *.
        intro Hdef.
        inv Hni. apply H1.
        now apply Is_defined_in_vars_defined.
  Qed.

  Lemma NoDup_defs_node:
    forall n,
      NoDup_defs n.(n_eqs).
Proof.
    intro; apply NoDup_defs_NoDup_vars_defined, NoDup_var_defined_n_eqs.
  Qed.

End NODUP.

Module NoDupFun
       (Ids : IDS)
       (Op : OPERATORS)
       (CESyn : CESYNTAX Op)
       (Syn : NLSYNTAX Ids Op CESyn)
       (Mem : MEMORIES Ids Op CESyn Syn)
       (IsD : ISDEFINED Ids Op CESyn Syn Mem)
       (IsV : ISVARIABLE Ids Op CESyn Syn Mem IsD)
       <: NODUP Ids Op CESyn Syn Mem IsD IsV.

  Include NODUP Ids Op CESyn Syn Mem IsD IsV.

End NoDupFun.