From Velus Require Import Common.
From Velus Require Import FunctionalEnvironment.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import Lustre.StaticEnv.
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.LSemantics Lustre.LClockedSemantics.
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 Velus Require Import CoindToIndexed IndexedToCoind CoindIndexed.

From Velus Require Import CoreExpr.CESemantics.
From Velus Require Import CoreExpr.CEInterpreter.
From Velus Require Import NLustre.NLIndexedSemantics.
From Velus Require Import NLCoindToIndexed NLIndexedToCoind.

From Coq Require Import String.

From Coq Require Import List.
Import List.ListNotations.
From Coq Require Import Permutation.
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.

From Coq Require Import Classical_Prop.

Semantics Preservation Proof for Transcription

Module Type CORRECTNESS
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux: OPERATORS_AUX Ids Op)
       (Import Cks : CLOCKS Ids Op OpAux)
       (Import Senv : STATICENV Ids Op OpAux Cks)
       (L : LSYNTAX Ids Op OpAux Cks Senv)
       (Import CE : CESYNTAX Ids Op OpAux Cks)
       (NL : NLSYNTAX Ids Op OpAux Cks CE)
       (Import TR : TR Ids Op OpAux Cks Senv L CE NL)
       (LT : LTYPING Ids Op OpAux Cks Senv L)
       (LC : LCLOCKING Ids Op OpAux Cks Senv L)
       (Ord : NLORDERED Ids Op OpAux Cks CE NL)
       (Lord : LORDERED Ids Op OpAux Cks Senv L)
       (Import Str : COINDSTREAMS Ids Op OpAux Cks)
       (LS : LSEMANTICS Ids Op OpAux Cks Senv L Lord Str)
       (Import LCS : LCLOCKEDSEMANTICS Ids Op OpAux Cks Senv L LC Lord Str LS)
       (LN : NORMALIZATION Ids Op OpAux Cks Senv L)
       (NLSC : NLCOINDSEMANTICS Ids Op OpAux Cks CE NL Str Ord).

  Lemma sem_lexp_step {PSyn prefs} :
    forall (G: @L.global PSyn prefs) H b e e' s,
      to_lexp e = OK e' ->
      LCS.sem_exp_ck G H b e s ->
      LCS.sem_exp_ck G (history_tl H) (Streams.tl b) e (map (@Streams.tl _) s).

  Lemma sem_cexp_step {PSyn prefs} :
    forall (G: @L.global PSyn prefs) H b e e' s,
      to_cexp e = OK e' ->
      LCS.sem_exp_ck G H b e s ->
      LCS.sem_exp_ck G (history_tl H) (Streams.tl b) e (map (@Streams.tl _) s).

  Lemma ty_lexp {PSyn prefs} :
    forall (G: @L.global PSyn prefs) env e e',
      LT.wt_exp G env e ->
      to_lexp e = OK e' ->
      L.typeof e = [CE.typeof e'].

  Lemma sem_exp_lexp {PSyn prefs} :
    forall (G : @L.global PSyn prefs) env H b e e' s,
      LT.wt_exp G env e ->
      to_lexp e = OK e' ->
      LCS.sem_exp_ck G H b e [s] ->
      NLSC.sem_exp (LS.var_history H) b e' s.

  Lemma sem_lexp_single {PSyn prefs} :
    forall e e' G H b ss,
      to_lexp e = OK e' ->
      LCS.sem_exp_ck (G: @L.global PSyn prefs) H b e ss ->
      exists s, ss = [s].

  Lemma sem_exps_lexps {PSyn prefs} :
    forall (G: @L.global PSyn prefs) H b tenv es les ss,
      mmap to_lexp es = OK les ->
      Forall (LT.wt_exp G tenv) es ->
      Forall2 (LCS.sem_exp_ck G H b) es ss ->
      Forall2 (NLSC.sem_exp (LS.var_history H) b) les (concat ss).

  Lemma sem_exp_controls {PSyn prefs} (G: @L.global PSyn prefs) env0 : forall H b es es' vs,
    Forall (fun es =>
              Forall (fun e => forall e' s,
                          LT.wt_exp G env0 e ->
                          to_cexp e = OK e' ->
                          LCS.sem_exp_ck G H b e [s] ->
                          NLSC.sem_cexp (LS.var_history H) b e' s)
                     (snd es)) es ->
    Forall (fun es => Forall (LT.wt_exp G env0) (snd es)) es ->
    LS.Forall2Brs (LCS.sem_exp_ck G H b) es [vs] ->
    mmap
      (fun pat =>
         match pat with
         | (i, []) => Error (msg "control expression not normalized")
         | (i, [e]) => do ce <- to_cexp e; OK (i, ce)
         | (i, e :: _ :: _) => Error (msg "control expression not normalized")
         end) es = OK es' ->
    Forall2 (NLSC.sem_cexp (LS.var_history H) b) (map snd es') (map snd vs).

  Lemma merge_Permutation : forall c vs vs' s,
      Permutation vs vs' ->
      merge c vs s ->
      merge c vs' s.

  Lemma case_Permutation : forall c vs vs' vd s,
      Permutation vs vs' ->
      case c vs vd s ->
      case c vs' vd s.

  Lemma case_complete : forall tx tn c vs vs' vd s,
      wt_streams [c] [Tenum tx tn] ->
      map fst vs' = seq 0 (length tn) ->
      (forall i v, In (i, v) vs' <-> In (i, v) vs \/ (i < length vs' /\ ~InMembers i vs /\ v = vd)) ->
      case c vs (Some vd) s ->
      case c vs' None s.

  Lemma Forall2_Permutation_1_fst {A B C} : forall (P : (A * B) -> (A * C) -> Prop) l1 l1' l2,
      Permutation l1 l1' ->
      Forall2 P l1 l2 ->
      map fst l1 = map fst l2 ->
      exists l2', Permutation l2 l2' /\ Forall2 P l1' l2' /\ map fst l1' = map fst l2'.

  Fixpoint complete_sem (s : list enumtag) (brs : list (enumtag * Stream svalue)) (d : Stream svalue) : list (enumtag * Stream svalue) :=
    match s with
    | [] => brs
    | k::s =>
      match brs with
      | [] => (k, d)::(complete_sem s brs d)
      | (tag, e)::tl => if (tag =? k) then (tag, e)::(complete_sem s tl d)
                      else (k, d)::(complete_sem s brs d)
      end
    end.

  Lemma complete_sem_fst : forall n es d,
      NoDupMembers es ->
      Sorted.StronglySorted le (map fst es) ->
      incl (map fst es) (seq 0 n) ->
      map fst (complete_sem (seq 0 n) es d) = (seq 0 n).

  Corollary complete_sem_length : forall n ys d,
      NoDupMembers ys ->
      Sorted.StronglySorted le (map fst ys) ->
      incl (map fst ys) (seq 0 n) ->
      length (complete_sem (seq 0 n) ys d) = n.

  Lemma complete_branches_sem H b : forall n es d ys vd,
      map fst ys = map fst es ->
      Forall2 (fun e y => NLSC.sem_cexp H b (snd e) (snd y)) es ys ->
      NLSC.sem_cexp H b d vd ->
      Forall2 (fun oe => NLSC.sem_cexp H b (or_default d oe)) (map snd (complete_branches (seq 0 n) es)) (map snd (complete_sem (seq 0 n) ys vd)).

  Lemma complete_sem_In : forall n ys d i v,
      NoDupMembers ys ->
      Sorted.StronglySorted le (map fst ys) ->
      incl (map fst ys) (seq 0 n) ->
      In (i, v) (complete_sem (seq 0 n) ys d) <-> In (i, v) ys \/ (In i (seq 0 n) /\ ~InMembers i ys /\ v = d).

  Lemma sem_exp_cexp {PSyn prefs} :
    forall (G: @L.global PSyn prefs) env H b e e' s,
      LT.wt_exp G env e ->
      to_cexp e = OK e' ->
      LCS.sem_exp_ck G H b e [s] ->
      NLSC.sem_cexp (LS.var_history 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.

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

  Lemma reset_or_not_reset : forall n r,
      (forall m, m <= n -> r # m = false) \/
      (exists m, m <= n /\ r # m = true).

  Lemma fby1_reset1_fby:
    forall n r x0 v0 x y,
      (forall m, m <= n -> r # m = false) ->
      LS.fby1 v0 (NCor.const_val (abstract_clock (mask' absent 0 0 r x)) x0) (mask' absent 0 0 r x) (mask' absent 0 0 r y) ->
      y # n = (NLSC.reset1 x0 (sfby v0 x) r false) # n.

  Lemma reset1_fby_reset : forall n v0 v xs rs,
      (exists m, m <= n /\ rs # m = true) ->
      (NLSC.reset1 v0 (sfby v xs) rs false) # n = (NLSC.reset1 v0 (sfby v0 xs) rs false) # n.

  Corollary fby_reset_fby:
    forall r x0 x y,
      (forall k, LS.fby (NCor.const_val (abstract_clock (maskv k r x)) x0) (maskv k r x) (maskv k r y)) ->
      y ≡ NLSC.reset x0 (sfby x0 x) r.

  Fact sem_clock_ac : forall H bs bs' ck x ty k xs vs ys,
      sem_var H x vs ->
      sem_clock H bs (Con ck x (ty, k)) bs' ->
      when k xs vs ys ->
      bs' ≡ abstract_clock ys.

  Fact sem_clock_inv : forall H bs ck x ty k xs vs ys,
      sem_var H x vs ->
      sem_clock H bs (Con ck x (ty, k)) (abstract_clock ys) ->
      when k xs vs ys ->
      sem_clock H bs ck (abstract_clock xs).

  Fact sem_clock_const : forall H ck x s ty k bs bs' bs'' c xs ys,
    sem_var H x s ->
    sem_clock H bs ck bs' ->
    sem_clock H bs (Con ck x (ty, k)) bs'' ->
    when k xs s ys ->
    xs ≡ (NCor.const_val bs' c) ->
    ys ≡ (NCor.const_val bs'' c).

  Lemma to_constant_sem {PSyn prefs} :
    forall (G: @L.global PSyn prefs) cenv H b e ck b' c cs,
      L.clockof e = [ck] ->
      LC.wc_exp G cenv e ->
      to_constant e = OK c ->
      LCS.sem_exp_ck G H b e [cs] ->
      sem_clock (LS.var_history H) b ck b' ->
      cs ≡ (NCor.const_val b' (sem_const c)).

  Module CES := CESemanticsFun Ids Op OpAux Cks CE IStr.
  Module CEI := CEInterpreterFun Ids Op OpAux Cks CE IStr CES.
  Module ICStr := IndexedToCoindFun Ids Op OpAux Cks IStr Str.
  Module CIStr' := CoindToIndexedFun Ids Op OpAux Cks Str IStr.
  Module Import ConvStr := CoindIndexedFun Ids Op OpAux Cks Str IStr.
  Module NLSI := NLIndexedSemanticsFun Ids Op OpAux Cks CE NL IStr Ord CES.
  Module NICStr := NLIndexedToCoindFun Ids Op OpAux Cks CE NL IStr Str ICStr Ord CES NLSI CEI NLSC.
  Module NCIStr := NLCoindToIndexedFun Ids Op OpAux Cks CE NL IStr Str CIStr' Ord CES NLSI NLSC.

  Lemma sem_rhs_arhs : forall H b ck e s,
      NLSC.sem_rhs H b e s ->
      sem_clock H b ck (abstract_clock s) ->
      NLSC.sem_arhs H b ck e s.

  Corollary sem_exp_arhs {PSyn prefs} :
    forall (G: @L.global PSyn prefs) H b env e e' s ck,
      LT.wt_exp G env e ->
      to_cexp e = OK e' ->
      LCS.sem_exp_ck G H b e [s] ->
      sem_clock (LS.var_history H) b ck (abstract_clock s) ->
      NLSC.sem_arhs (LS.var_history H) b ck (Ecexp 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.

  Lemma Forall2_forall' {A B} : forall (P : nat -> A -> B -> Prop) xs ys,
    (forall k, Forall2 (P k) xs ys) <-> Forall2 (fun x y => forall k, (P k x y)) xs ys.

  Lemma Forall_Forall2 {A B} : forall (P : A -> B -> Prop) xs,
      Forall (fun x => exists y, P x y) xs ->
      exists ys, Forall2 P xs ys.

  Lemma sem_lexp_mask: forall r H b e v,
      (forall k, NLSC.sem_exp (mask_hist k r H) (maskb k r b) e (maskv k r v)) ->
      NLSC.sem_exp H b e v.

  Corollary sem_lexps_mask: forall r H b es vs,
      (forall k, Forall2 (fun e v => NLSC.sem_exp (mask_hist k r H) (maskb k r b) e (maskv k r v)) es vs) ->
      Forall2 (NLSC.sem_exp H b) es vs.

  Lemma sem_aexp_mask: forall r H b ck e v,
      (forall k, NLSC.sem_aexp (mask_hist k r H) (maskb k r b) ck e (maskv k r v)) ->
      NLSC.sem_aexp H b ck e v.

  Lemma sem_arhs_mask: forall r H b ck e v,
      (forall k, NLSC.sem_arhs (mask_hist k r H) (maskb k r b) ck e (maskv k r v)) ->
      NLSC.sem_arhs H b ck e v.

  Lemma sem_toeq_normalized {PSyn prefs} :
    forall (G: @L.global PSyn prefs) P cenv x e ck e' r H b,
      LC.wc_global G ->
      LCS.sc_vars cenv H b ->
      LN.Unnesting.normalized_cexp e ->
      LT.wt_exp G cenv e ->
      LC.wc_exp G cenv e ->
      L.clockof e = [ck] ->
      to_cexp e = OK e' ->
      (forall k, LCS.sem_equation_ck G (mask_hist k r H) (maskb k r b) ([x], [e])) ->
      NLSC.sem_equation P (LS.var_history H) b (NL.EqDef x ck (Ecexp e')).

  Lemma sem_lexp_mask_inv: forall r k H b e v,
      NLSC.sem_exp (mask_hist k r H) (maskb k r b) e v ->
      exists v', v ≡ maskv k r v'.

  Lemma sem_normalized_lexp_mask_inv {PSyn prefs}: forall (G: @L.global PSyn prefs) r k H b e v,
      LN.Unnesting.normalized_lexp e ->
      LCS.sem_exp_ck G (mask_hist k r H) (maskb k r b) e v ->
      exists v', EqSts v [maskv k r v'].

  Corollary sem_laexp_mask_inv: forall r k H b e ck v,
      NLSC.sem_aexp (mask_hist k r H) (maskb k r b) ck e v ->
      exists v', v ≡ maskv k r v'.

  Lemma sem_normalized_lexp_det {PSyn prefs} : forall (G: @L.global PSyn prefs) H b e vs1 vs2,
      LN.Unnesting.normalized_lexp e ->
      LCS.sem_exp_ck G H b e vs1 ->
      LCS.sem_exp_ck G H b e vs2 ->
      EqSts vs1 vs2.

  Lemma disj_str_maskb : forall k r rs,
      maskb k r (disj_str rs) ≡ disj_str (map (maskb k r) rs).

  Lemma disj_str_comm : forall r1 r2,
      disj_str [r1;r2] ≡ disj_str [r2;r1].

  Lemma count_ex_dec : forall r k,
      (exists n, (count r) # n = k) \/ (forall n, (count r) # n <> k).

  Lemma count_neq_0_or_lt : forall r k,
      (forall n, (count r) # n <> k) ->
      (k = 0 /\ r # 0 = true) \/
      (forall n, (count r) # n < k).

  Lemma count_disj_count : forall k r1 r2,
      exists k1 k2, forall n, (count (disj_str [r1;r2])) # n = k <->
                    ((count (maskb k2 r2 r1)) # n = k1 /\ (count r2) # n = k2).

  Lemma mask_disj : forall k r1 r2,
      exists k1 k2,
        forall A (absent: A) xs, mask absent k (disj_str [r1;r2]) xs ≡
                            mask absent k1 (maskb k2 r2 r1) (mask absent k2 r2 xs).

  Corollary mask_disj' {K} : forall k r1 r2,
      exists k1 k2,
        (forall xs, maskv k (disj_str [r1;r2]) xs ≡ maskv k1 (maskb k2 r2 r1) (maskv k2 r2 xs)) /\
        (forall bs, maskb k (disj_str [r1;r2]) bs ≡ maskb k1 (maskb k2 r2 r1) (maskb k2 r2 bs)) /\
        (forall (H: @history K), FEnv.Equiv (@EqSt _) (mask_hist k (disj_str [r1;r2]) H) (mask_hist k1 (maskb k2 r2 r1) (mask_hist k2 r2 H))).

  Lemma sem_toeq {PSyn prefs} :
    forall cenv out (G: @L.global PSyn prefs) H P env envo xr rs r eq eq' b,
      LN.NormFby.normalized_equation G out eq ->
      LT.wt_equation G cenv eq ->
      LC.wc_equation G cenv eq ->
      LC.wc_global G ->
      envs_eq env (idck cenv) ->
      (forall f xs ys,
          LCS.sem_node_ck G f xs ys ->
          NLSC.sem_node P f xs ys) ->
      LCS.sc_vars cenv H b ->
      Forall (fun xr => In xr (idck cenv)) xr ->
      to_equation env envo xr eq = OK eq' ->
      Forall2 (sem_var H) (map (fun '(x, _) => LS.Var x) xr) rs ->
      bools_ofs rs r ->
      (forall k, LCS.sem_equation_ck G (mask_hist k r H) (maskb k r b) eq) ->
      NLSC.sem_equation P (LS.var_history H) b eq'.

  Lemma sem_blocktoeq {PSyn prefs} :
    forall cenv out (G: @L.global PSyn prefs) H P env envo bck xr rs r eqs' b,
      LN.NormFby.normalized_block G out bck ->
      LT.wt_block G cenv bck ->
      LC.wc_block G cenv bck ->
      LC.wc_global G ->
      envs_eq env (idck cenv) ->
      (forall f xs ys,
          LCS.sem_node_ck G f xs ys ->
          NLSC.sem_node P f xs ys) ->
      LCS.sc_vars cenv H b ->
      Forall (fun xr0 => In xr0 (idck cenv)) xr ->
      block_to_equation env envo xr bck = OK eqs' ->
      Forall2 (sem_var H) (map (fun '(x, _) => LS.Var x) xr) rs ->
      bools_ofs rs r ->
      (forall k, LCS.sem_block_ck G (mask_hist k r H) (maskb k r b) bck) ->
      NLSC.sem_equation P (LS.var_history H) b eqs'.

  Lemma sem_blockstoeqs {PSyn prefs} :
    forall cenv out (G: @L.global PSyn prefs) H P env envo bcks eqs' b,
      Forall (LN.NormFby.normalized_block G out) bcks ->
      Forall (LT.wt_block G cenv) bcks ->
      Forall (LC.wc_block G cenv) bcks ->
      LC.wc_global G ->
      envs_eq env (idck cenv) ->
      (forall f xs ys,
          LCS.sem_node_ck G f xs ys ->
          NLSC.sem_node P f xs ys) ->
      LCS.sc_vars cenv H b ->
      mmap (block_to_equation env envo []) bcks = OK eqs' ->
      Forall (LCS.sem_block_ck G H b) bcks ->
      Forall (NLSC.sem_equation P (LS.var_history H) b) eqs'.

  Lemma inputs_clocked_vars {PSyn prefs} :
    forall (n: @L.node PSyn prefs) H ins,
      Forall2 (fun x => sem_var H (LS.Var x)) (L.idents (L.n_in n)) ins ->
      LCS.sc_vars (senv_of_ins (L.n_in n) ++ senv_of_decls (L.n_out n)) H (clocks_of ins) ->
      NLSC.sem_clocked_vars (LS.var_history H) (clocks_of ins) (Common.idck (Common.idty (L.n_in n))).

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

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

End CORRECTNESS.

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