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

From Coq Require Import Sorting.Permutation.
From Coq Require Import Morphisms.
From Coq Require Import Program.Tactics.
From Coq Require Import Omega.

From Coq Require Import FSets.FMapPositive.
From Velus Require Import Common.
From Velus Require Import Environment.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import CoreExpr.CESyntax.
From Velus Require Import NLustre.NLSyntax.
From Velus Require Import NLustre.NLOrdered.
From Velus Require Import IndexedStreams.
From Velus Require Import CoindStreams.
From Velus Require Import CoindToIndexed.

From Velus Require Import CoreExpr.CESemantics.
From Velus Require Import NLustre.NLIndexedSemantics.
From Velus Require Import NLustre.NLCoindSemantics.

From Coq Require Import Setoid.

Module Type NLCOINDTOINDEXED
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Op)
       (Import CESyn : CESYNTAX Op)
       (Import Syn : NLSYNTAX Ids Op CESyn)
       (Import IStr : INDEXEDSTREAMS Op OpAux)
       (Import CStr : COINDSTREAMS Op OpAux)
       (Import CIStr : COINDTOINDEXED Op OpAux CStr IStr)
       (Import Ord : NLORDERED Ids Op CESyn Syn)
       (CESem : CESEMANTICS Ids Op OpAux CESyn IStr)
       (Indexed : NLINDEXEDSEMANTICS Ids Op OpAux CESyn Syn IStr Ord CESem)
       (CoInd : NLCOINDSEMANTICS Ids Op OpAux CESyn Syn CStr Ord).

  Section Global.

    Variable G : global.

SEMANTICS CORRESPONDENCE

Variables

    Corollary sem_vars_impl:
      forall H xs xss,
      Forall2 (sem_var H) xs xss ->
      CESem.sem_vars (tr_history H) xs (tr_Streams xss).

Proof.

Hint Resolve sem_vars_impl.

Semantics of exps

State the correspondence for exp. Goes by induction on the coinductive semantics of exp.

    Hint Constructors CESem.sem_exp_instant.
    Lemma sem_exp_impl:
      forall H b e es,
        CoInd.sem_exp H b e es ->
        CESem.sem_exp (tr_Stream b) (tr_history H) e (tr_Stream es).

Proof.

    Hint Resolve sem_exp_impl.

    Corollary sem_exps_impl:
      forall H b es ess,
        Forall2 (CoInd.sem_exp H b) es ess ->
        CESem.sem_exps (tr_Stream b) (tr_history H) es (tr_Streams ess).

Proof.

Hint Resolve sem_exps_impl.

Give an indexed specification for annotated exp, using the previous lemma.

    Lemma sem_aexp_index:
      forall n H b ck le es,
        CoInd.sem_aexp H b ck le es ->
        (sem_clock_instant (tr_Stream b n)
                                   (tr_history H n) ck false
         /\ CESem.sem_exp_instant
             (tr_Stream b n) (tr_history H n) le absent
         /\ tr_Stream es n = absent)
        \/
        (exists e,
            sem_clock_instant (tr_Stream b n)
                                      (tr_history H n) ck true
            /\ CESem.sem_exp_instant
                (tr_Stream b n) (tr_history H n) le (present e)
            /\ tr_Stream es n = present e).

Proof.

We deduce from the previous lemma the correspondence for annotated exp.

    Corollary sem_aexp_impl:
      forall H b e es ck,
        CoInd.sem_aexp H b ck e es ->
        CESem.sem_aexp (tr_Stream b) (tr_history H) ck e (tr_Stream es).

Proof.

Hint Resolve sem_aexp_impl.

fby is not a predicate but a function, so we directly state the correspondence.

    Lemma fby_impl:
      forall c xs,
      tr_Stream (sfby c xs) ≈ Indexed.fby c (tr_Stream xs).

Proof.

Semantics of cexps

State the correspondence for cexp. Goes by induction on the coinductive semantics of cexp.

    Hint Constructors CESem.sem_cexp_instant.
    Lemma sem_cexp_impl:
      forall H b e es,
        CoInd.sem_cexp H b e es ->
        CESem.sem_cexp (tr_Stream b) (tr_history H) e (tr_Stream es).

Proof.

Hint Resolve sem_cexp_impl.

Give an indexed specification for annotated cexp, using the previous lemma.

    Lemma sem_caexp_index:
      forall n H b ck le es,
        CoInd.sem_caexp H b ck le es ->
        (sem_clock_instant (tr_Stream b n)
                                   (tr_history H n) ck false
         /\ CESem.sem_cexp_instant
             (tr_Stream b n) (tr_history H n) le absent
         /\ tr_Stream es n = absent)
        \/
        (exists e,
            sem_clock_instant (tr_Stream b n)
                                      (tr_history H n) ck true
            /\ CESem.sem_cexp_instant
                (tr_Stream b n) (tr_history H n) le (present e)
            /\ tr_Stream es n = present e).

Proof.

We deduce from the previous lemma the correspondence for annotated cexp.

    Corollary sem_caexp_impl:
      forall H b e es ck,
        CoInd.sem_caexp H b ck e es ->
        CESem.sem_caexp (tr_Stream b) (tr_history H) ck e (tr_Stream es).

Proof.

Hint Resolve sem_caexp_impl.

RESET CORRESPONDENCE

We state the correspondence for bools_of.

    Lemma bools_of_impl:
      forall xs rs,
        CStr.bools_of xs rs ->
        CESem.bools_of (tr_Stream xs) (tr_Stream rs).

Proof.

Properties about count and mask

When a reset occurs initially, the count at n is the count at n forgetting the first instant, plus one if no reset occurs at n when shifting.

    Lemma count_true_shift:
      forall n r,
        IStr.count (tr_Stream (true ⋅ r)) n
        = if tr_Stream r n
          then IStr.count (tr_Stream r) n
          else S (IStr.count (tr_Stream r) n).

Proof.

When no reset occurs initially, the count at n is the count at n forgetting the first instant, minus one if a reset occurs at n when shifting.

    Lemma count_false_shift:
      forall n r,
        IStr.count (tr_Stream (false ⋅ r)) n
        = if tr_Stream r n
          then IStr.count (tr_Stream r) n - 1
          else IStr.count (tr_Stream r) n.

Proof.

State the correspondence for count.

    Lemma count_impl:
      forall r,
        tr_Stream (CStr.count r) ≈ IStr.count (tr_Stream r).

Proof.

State the correspondence for mask.

    Lemma mask_impl:
      forall k r xss,
        tr_Streams (List.map (CStr.mask k r) xss)
        ≈ IStr.mask k (tr_Stream r) (tr_Streams xss).

Proof.

FINAL LEMMAS

Correspondence for clocks_of, used to give a base clock for node applications.

    Lemma tr_clocks_of:
      forall xss,
        CESem.clock_of (tr_Streams xss) ≈ tr_Stream (CStr.clocks_of xss).

Proof.

Hint Resolve tr_clocks_of.

Give an indexed specification for Streams synchronization.

    Lemma aligned_index:
      forall xs bs,
        aligned xs bs ->
        forall n, tr_Stream bs n = true <-> tr_Stream xs n <> absent.

Proof.

    Lemma sem_clocked_var_impl:
      forall H b x ck xs,
        sem_var H x xs ->
        CoInd.sem_clocked_var H b x ck ->
        CESem.sem_clocked_var (tr_Stream b) (tr_history H) x ck.

Proof.

    Lemma sem_clocked_vars_impl:
      forall H b xcs xss,
        Forall2 (sem_var H) (List.map fst xcs) xss ->
        CoInd.sem_clocked_vars H b xcs ->
        CESem.sem_clocked_vars (tr_Stream b) (tr_history H) xcs.

Proof.

Hint Resolve sem_clocked_vars_impl.

The final theorem stating the correspondence for nodes applications. We have to use a custom mutually recursive induction scheme sem_node_mult.

    Hint Constructors Indexed.sem_equation.
    Theorem implies:
      forall f xss yss,
        CoInd.sem_node G f xss yss ->
        Indexed.sem_node G f (tr_Streams xss) (tr_Streams yss).

Proof.

  End Global.

End NLCOINDTOINDEXED.

Module NLCoindToIndexedFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Op)
       (CESyn : CESYNTAX Op)
       (Syn : NLSYNTAX Ids Op CESyn)
       (IStr : INDEXEDSTREAMS Op OpAux)
       (CStr : COINDSTREAMS Op OpAux)
       (CIStr : COINDTOINDEXED Op OpAux CStr IStr)
       (Ord : NLORDERED Ids Op CESyn Syn)
       (CESem : CESEMANTICS Ids Op OpAux CESyn IStr)
       (Indexed : NLINDEXEDSEMANTICS Ids Op OpAux CESyn Syn IStr Ord CESem)
       (CoInd : NLCOINDSEMANTICS Ids Op OpAux CESyn Syn CStr Ord)
<: NLCOINDTOINDEXED Ids Op OpAux CESyn Syn IStr CStr CIStr Ord CESem Indexed CoInd.
  Include NLCOINDTOINDEXED Ids Op OpAux CESyn Syn IStr CStr CIStr Ord CESem Indexed CoInd.
End NLCoindToIndexedFun.