From Velus Require Import Common.
From Velus Require Import Environment.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import Lustre.LSyntax.
From Velus Require Import CoreExpr.CESyntax.
From Velus Require Import NLustre.NLSyntax.
From Velus Require Import Transcription.Tr Transcription.TrOrdered.

From Velus Require Import Lustre.LTyping.
From Velus Require Import Lustre.LClocking.
From Velus Require Import Lustre.LOrdered.
From Velus Require Import Lustre.LCausality.
From Velus Require Import Lustre.LSemantics Lustre.LClockSemantics.
From Velus Require Import Lustre.Normalization.Normalization.
From Velus Require Import Lustre.Normalization.Correctness.
From Velus Require Import NLustre.NLOrdered.
From Velus Require Import NLustre.NLCoindSemantics.

From Velus Require Import CoindStreams IndexedStreams.

From Coq Require Import String.

From Coq Require Import List.
Import List.ListNotations.
From Coq Require Import Permutation.
From Coq Require Import Omega.
From Coq Require Import Setoid.
From Coq Require Import Morphisms.

Open Scope list.

From compcert Require Import common.Errors.
Open Scope error_monad_scope.

From Coq Require Import Classes.EquivDec.

Semantics Preservation Proof for Transcription

Module Type CORRECTNESS
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux: OPERATORS_AUX Op)
       (L : LSYNTAX Ids Op)
       (Import CE : CESYNTAX Op)
       (NL : NLSYNTAX Ids Op CE)
       (Import TR : TR Ids Op OpAux L CE NL)
       (LT : LTYPING Ids Op L)
       (LC : LCLOCKING Ids Op L)
       (LCA : LCAUSALITY Ids Op L)
       (Ord : NLORDERED Ids Op CE NL)
       (Lord : LORDERED Ids Op L)
       (Import Str : COINDSTREAMS Op OpAux)
       (IStr : INDEXEDSTREAMS Op OpAux)
       (LS : LSEMANTICS Ids Op OpAux L Lord Str)
       (LCS : LCLOCKSEMANTICS Ids Op OpAux L LC LCA Lord Str IStr LS)
       (LN : NORMALIZATION Ids Op OpAux L LCA)
       (NLSC : NLCOINDSEMANTICS Ids Op OpAux CE NL Str Ord).

  Lemma sem_const_step :
    forall G H b e e' v s,
      to_constant e = OK e' ->
      LS.sem_exp G H b e [v ⋅ s] ->
      LS.sem_exp G (history_tl H) (Streams.tl b) e [s].

  Lemma sem_lexp_step :
    forall G H b e e' v s,
      to_lexp e = OK e' ->
      LS.sem_exp G H b e [v ⋅ s] ->
      LS.sem_exp G (history_tl H) (Streams.tl b) e [s].

  Lemma sem_cexp_step :
    forall G H b e e' v s,
      to_cexp e = OK e' ->
      LS.sem_exp G H b e [v ⋅ s] ->
      LS.sem_exp G (history_tl H) (Streams.tl b) e [s].

  Lemma ty_lexp :
    forall G env e e',
      LT.wt_exp G env e ->
      to_lexp e = OK e' ->
      L.typeof e = [CE.typeof e'].

  Lemma sem_exp_lexp :
    forall G G' env H b e e' s,
      LT.wt_exp G' env e ->
      to_lexp e = OK e' ->
      LS.sem_exp G H b e [s] ->
      NLSC.sem_exp H b e' s.

  Lemma sem_lexp_single :
    forall e e' G H b ss,
      to_lexp e = OK e' ->
      LS.sem_exp G H b e ss ->
      exists s, ss = [s].

  Lemma sem_exps_lexps :
    forall G H b tenv es les ss,
      mmap to_lexp es = OK les ->
      Forall (LT.wt_exp G tenv) es ->
      Forall2 (LS.sem_exp G H b) es ss ->
      Forall2 (NLSC.sem_exp H b) les (concat ss).

  Lemma sem_exp_cexp :
    forall G G' env H b e e' s,
      LT.wt_exp G' env e ->
      to_cexp e = OK e' ->
      LS.sem_exp G H b e [s] ->
      NLSC.sem_cexp H b e' s.

  Lemma sem_lexp_step2: forall H b e v s,
      NLSC.sem_exp H b e (v ⋅ s) ->
      NLSC.sem_exp (history_tl H) (Streams.tl b) e s.

  Lemma sem_cexp_step2: forall H b e v s,
      NLSC.sem_cexp H b e (v ⋅ s) ->
      NLSC.sem_cexp (history_tl H) (Streams.tl b) e s.

  Lemma fby_const:
    forall b c xs ys rs,
      LS.fby xs ys rs ->
      xs ≡ const b c ->
      b ≡ abstract_clock rs ->
      rs ≡ sfby (sem_const c) ys.

  Lemma sem_const_exp:
    forall G H b e c c' xs,
      to_constant e = OK c ->
      LS.sem_exp G H b e [present c' ⋅ xs] ->
      c' = sem_const c.

  Lemma fby_const_when :
    forall G H bk x i ck e b c s cs css xs ys,
      sem_var H x xs ->
      sem_clock H bk (Con ck i b) (abstract_clock xs) ->
      LS.fby css ys xs ->
      to_constant e = OK c ->
      LS.sem_exp G H bk e [cs] ->
      when b cs s css ->
      xs ≡ sfby (sem_const c) ys.

  Lemma var_fby_const :
    forall G H b c a env cenv ck ckx x e0 e1 cs xs ys,
      LS.sem_exp G H b e0 [cs] ->
      sem_var H x xs ->
      LS.fby cs ys xs ->
      find_clock env x = OK ck ->
      LC.wc_exp G cenv (L.Efby [e0] [e1] a) ->
      [ckx] = map L.clock_of_nclock a ->
      In (x, ckx) cenv ->
      envs_eq env cenv ->
      to_constant e0 = OK c ->
      sem_clock H b ck (abstract_clock xs) ->
      sem_var H x (sfby (sem_const c) ys).

  Lemma sem_exp_caexp :
    forall G H b env e e' s ck,
      LT.wt_exp G env e ->
      to_cexp e = OK e' ->
      LS.sem_exp G H b e [s] ->
      sem_clock H b ck (abstract_clock s) ->
      NLSC.sem_caexp H b ck e' s.

  Lemma sem_lexp_laexp :
    forall H b e s ck,
      NLSC.sem_exp H b e s ->
      sem_clock H b ck (abstract_clock s) ->
      NLSC.sem_aexp H b ck e s.

  Module NCor := CorrectnessFun Ids Op OpAux Str IStr L LCA LT LC Lord LS LCS LN.

  Lemma sc_cexp : forall G env H b e vs,
      LC.wc_global G ->
      LCS.sc_nodes G ->
      NoDupMembers env ->
      LCS.sc_var_inv' env H b ->
      LN.Unnesting.normalized_cexp e ->
      LC.wc_exp G env e ->
      LS.sem_exp G H b e vs ->
      Forall2 (sem_clock H b) (L.clockof e) (map abstract_clock vs).

  Corollary sc_lexps : forall G env H b es vs,
      LC.wc_global G ->
      LCS.sc_nodes G ->
      NoDupMembers env ->
      LCS.sc_var_inv' env H b ->
      Forall LN.Unnesting.normalized_lexp es ->
      Forall (LC.wc_exp G env) es ->
      Forall2 (LS.sem_exp G H b) es vs ->
      Forall2 (sem_clock H b) (L.clocksof es) (map abstract_clock (concat vs)).

  Hint Resolve envs_eq_find'.

  Lemma sem_toeq :
    forall cenv out G H P env envo eq eq' b,
      LN.NormFby.normalized_equation G out eq ->
      LT.wt_equation G (idty cenv) eq ->
      LC.wc_equation G (idck cenv) eq ->
      LC.wc_global G ->
      LCS.sc_nodes G ->
      NoDupMembers cenv ->
      envs_eq env (idck cenv) ->
      (forall f xs ys,
          LS.sem_node G f xs ys ->
          LCS.sem_clock_inputs G f xs ->
          NLSC.sem_node P f xs ys) ->
      LCS.sc_var_inv' (idck cenv) H b ->
      to_equation env envo eq = OK eq' ->
      LS.sem_equation G H b eq ->
      NLSC.sem_equation P H b eq'.

  Lemma sem_toeqs' :
    forall cenv out G H P env envo eqs eqs' b,
      Forall (LN.NormFby.normalized_equation G out) eqs ->
      Forall (LT.wt_equation G (idty cenv)) eqs ->
      Forall (LC.wc_equation G (idck cenv)) eqs ->
      LC.wc_global G ->
      LCS.sc_nodes G ->
      NoDupMembers cenv ->
      envs_eq env (idck cenv) ->
      (forall f xs ys,
          LS.sem_node G f xs ys ->
          LCS.sem_clock_inputs G f xs ->
          NLSC.sem_node P f xs ys) ->
      LCS.sc_var_inv' (idck cenv) H b ->
      mmap (to_equation env envo) eqs = OK eqs' ->
      Forall (LS.sem_equation G H b) eqs ->
      Forall (NLSC.sem_equation P H b) eqs'.

  Lemma sem_toeqs :
    forall G n H P env envo eqs' ins,
      LN.NormFby.normalized_node G n ->
      Forall (LT.wt_equation G (idty (L.n_in n ++ L.n_vars n ++ L.n_out n))) (L.n_eqs n) ->
      Forall (LC.wc_equation G (idck (L.n_in n ++ L.n_vars n ++ L.n_out n))) (L.n_eqs n) ->
      LCA.node_causal n ->
      Lord.Ordered_nodes G ->
      LT.wt_global G ->
      LC.wc_global G ->
      LCS.sc_nodes G ->
      envs_eq env (idck (L.n_in n ++ L.n_vars n ++ L.n_out n)) ->
      (forall f xs ys,
          LS.sem_node G f xs ys ->
          LCS.sem_clock_inputs G f xs ->
          NLSC.sem_node P f xs ys) ->
      LC.wc_node G n ->
      Forall2 (sem_var H) (L.idents (L.n_in n)) ins ->
      LCS.sem_clock_inputs (n :: G) (L.n_name n) ins ->
      mmap (to_equation env envo) (L.n_eqs n) = OK eqs' ->
      Forall (LS.sem_equation G H (clocks_of ins)) (L.n_eqs n) ->
      Forall (NLSC.sem_equation P H (clocks_of ins)) eqs'.

  Lemma inputs_clocked_vars :
    forall n G H f ins,
      LCS.sem_clock_inputs (n :: G) f ins ->
      L.n_name n = f ->
      wc_env (idck (L.n_in n)) ->
      Forall2 (sem_var H) (L.idents (L.n_in n)) ins ->
      NLSC.sem_clocked_vars H (clocks_of ins) (idck (L.n_in n)).

  Module Import TrOrdered := TrOrderedFun Ids Op OpAux L Lord CE NL Ord TR.

  Theorem sem_l_nl :
    forall G P Hprefs f ins outs,
      LN.NormFby.normalized_global G ->
      Lord.Ordered_nodes G ->
      Forall LCA.node_causal G ->
      LT.wt_global G ->
      LC.wc_global G ->
      to_global G Hprefs = OK P ->
      LS.sem_node G f ins outs ->
      LCS.sem_clock_inputs G f ins ->
      NLSC.sem_node P f ins outs.

End CORRECTNESS.

Module CorrectnessFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Op)
       (L : LSYNTAX Ids Op)
       (CE : CESYNTAX Op)
       (NL : NLSYNTAX Ids Op CE)
       (TR : TR Ids Op OpAux L CE NL)
       (LT : LTYPING Ids Op L)
       (LC : LCLOCKING Ids Op L)
       (LCA : LCAUSALITY Ids Op L)
       (Ord : NLORDERED Ids Op CE NL)
       (Lord : LORDERED Ids Op L)
       (Str : COINDSTREAMS Op OpAux)
       (IStr : INDEXEDSTREAMS Op OpAux)
       (LS : LSEMANTICS Ids Op OpAux L Lord Str)
       (LCS : LCLOCKSEMANTICS Ids Op OpAux L LC LCA Lord Str IStr LS)
       (LN : NORMALIZATION Ids Op OpAux L LCA)
       (NLSC : NLCOINDSEMANTICS Ids Op OpAux CE NL Str Ord)
<: CORRECTNESS Ids Op OpAux L CE NL TR LT LC LCA Ord Lord Str IStr LS LCS LN NLSC.
  Include CORRECTNESS Ids Op OpAux L CE NL TR LT LC LCA Ord Lord Str IStr LS LCS LN NLSC.
End CorrectnessFun.