Module StcIsLast

From Velus Require Import Common.
From Velus Require Import Operators.
From Velus Require Import CoreExpr.CESyntax.
From Velus Require Import Stc.StcSyntax.
From Velus Require Import Clocks.

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

Module Type STCISLAST
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import CESyn : CESYNTAX Op)
       (Import Syn : STCSYNTAX Ids Op CESyn).

  Inductive Is_last_in_tc: ident -> trconstr -> Prop :=
    LastTcNext:
      forall x ck e,
        Is_last_in_tc x (TcNext x ck e).

  Definition Is_last_in (x: ident) (tcs: list trconstr) : Prop :=
    Exists (Is_last_in_tc x) tcs.

  Lemma not_Is_last_in_cons:
    forall x tc tcs,
      ~ Is_last_in x (tc :: tcs) <-> ~ Is_last_in_tc x tc /\ ~ Is_last_in x tcs.

Proof.

    split; intros HH.
    - split; intro; apply HH; unfold Is_last_in; intuition.
    - destruct HH; inversion_clear 1; intuition.
  Qed.

  Lemma lasts_of_In:
    forall tcs x,
      Is_last_in x tcs <-> In x (lasts_of tcs).

Proof.

    induction tcs as [|[]]; simpl.
    - now setoid_rewrite Exists_nil.
    - setoid_rewrite <-IHtcs; split; try right; auto.
      inversion_clear 1 as [?? Last|]; try inv Last; auto.
    - setoid_rewrite <-IHtcs; split.
      + inversion_clear 1 as [?? Last|]; try inv Last; auto.
      + intros [E|?].
        * subst; left; constructor.
        * right; auto.
    - setoid_rewrite <-IHtcs; split; try right; auto.
      inversion_clear 1 as [?? Last|]; try inv Last; auto.
    - setoid_rewrite <-IHtcs; split; try right; auto.
      inversion_clear 1 as [?? Last|]; try inv Last; auto.
  Qed.

  Definition is_last_in_tc_b (x: ident) (tc: trconstr) : bool :=
    match tc with
    | TcNext y ck e => ident_eqb x y
    | _ => false
    end.

  Definition is_last_in_b (x: ident) (tcs: list trconstr) : bool :=
    existsb (is_last_in_tc_b x) tcs.

  Fact Is_last_in_tc_reflect:
    forall x tc,
      Is_last_in_tc x tc <-> is_last_in_tc_b x tc = true.

Proof.

    destruct tc; simpl; split;
      try discriminate; try now inversion 1.
    - inversion_clear 1; apply ident_eqb_refl.
    - rewrite ident_eqb_eq; intro; subst; constructor.
  Qed.

  Corollary Is_last_in_reflect:
    forall x tcs,
      Is_last_in x tcs <-> is_last_in_b x tcs = true.

Proof.

    setoid_rewrite existsb_exists; setoid_rewrite Exists_exists.
    split; intros (?&?& Last); apply Is_last_in_tc_reflect in Last; eauto.
  Qed.

  Lemma Is_last_in_dec:
    forall x tcs,
      { Is_last_in x tcs } + { ~ Is_last_in x tcs }.

Proof.

    intros;
      eapply Bool.reflect_dec, Bool.iff_reflect, Is_last_in_reflect.
  Qed.

End STCISLAST.

Module StcIsLastFun
       (Ids : IDS)
       (Op : OPERATORS)
       (CESyn : CESYNTAX Op)
       (Syn : STCSYNTAX Ids Op CESyn)
<: STCISLAST Ids Op CESyn Syn.
  Include STCISLAST Ids Op CESyn Syn.
End StcIsLastFun.