From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.
From Coq Require Import Sorting.Permutation.
From Coq Require Import Setoid.
From Coq Require Import Morphisms.
From Coq Require Import Logic.FunctionalExtensionality.

From Coq Require Import FSets.FMapPositive.
From Velus Require Import Common.
From Velus Require Import CommonProgram.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import FunctionalEnvironment.
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 CoreExpr.CESemantics.

The NLustre semantics

Module Type NLINDEXEDSEMANTICS
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Ids Op)
       (Import Cks : CLOCKS Ids Op OpAux)
       (Import CESyn : CESYNTAX Ids Op OpAux Cks)
       (Import Syn : NLSYNTAX Ids Op OpAux Cks CESyn)
       (Import Str : INDEXEDSTREAMS Ids Op OpAux Cks)
       (Import Ord : NLORDERED Ids Op OpAux Cks CESyn Syn)
       (Import CESem : CESEMANTICS Ids Op OpAux Cks CESyn Str).

  Fixpoint hold (v0: value) (xs: stream svalue) (n: nat) : value :=
    match n with
    | 0 => v0
    | S m => match xs m with
            | absent => hold v0 xs m
            | present hv => hv
            end
    end.

  Definition fby (v0: value) (xs: stream svalue) : stream svalue :=
    fun n =>
      match xs n with
      | absent => absent
      | _ => present (hold v0 xs n)
      end.

  Fixpoint doreset (xs: stream svalue) (rs: stream bool) (n : nat) : bool :=
    if rs n then true
    else match n with
         | 0 => false
         | S m => match xs m with
                 | absent => doreset xs rs m
                 | present _ => false
                 end
         end.

  Definition reset (v0: value) (xs: stream svalue) (rs: stream bool) : stream svalue :=
    fun n =>
      match xs n with
      | absent => absent
      | present x => if (doreset xs rs n) then present v0 else present x
      end.

  Lemma reset_spec : forall v0 xs rs v n,
      reset v0 xs rs n = v <->
      (xs n = absent /\ v = absent) \/
      (exists x, xs n = present x /\ doreset xs rs n = false /\ v = present x) \/
      (exists x, xs n = present x /\ doreset xs rs n = true /\ v = present v0).

  Fact lt_S_inv : forall n m,
      n < S m ->
      (n < m \/ n = m).

  Lemma doreset_spec : forall xs rs n,
      doreset xs rs n = true <->
      rs n = true \/
      (exists m, m < n /\ rs m = true /\
            forall k, m <= k -> k < n -> xs k = absent).

  Fact doreset_shift : forall xs rs xs' rs' ,
      (forall k, xs' (S k) = xs k) ->
      (forall k, rs' (S k) = rs k) ->
      ((exists x, xs' 0 = present x) \/ rs' 0 = false) ->
      forall n, doreset xs' rs' (S n) = doreset xs rs n.

  Lemma reset_shift : forall v0 xs rs xs' rs' ,
      (forall k, xs' (S k) = xs k) ->
      (forall k, rs' (S k) = rs k) ->
      ((exists x, xs' 0 = present x) \/ rs' 0 = false) ->
      forall n, reset v0 xs' rs' (S n) = reset v0 xs rs n.

  Fact doreset_shift' : forall xs rs xs' rs' k x n,
      (forall k, xs' (S k) = xs k) ->
      (forall k, rs' (S k) = rs k) ->
      k < n -> xs k = present x ->
      doreset xs' rs' (S n) = doreset xs rs n.

  Lemma reset_shift' : forall n v0 xs rs xs' rs' k x,
      (forall k, xs' (S k) = xs k) ->
      (forall k, rs' (S k) = rs k) ->
      k < n -> xs k = present x ->
      reset v0 xs' rs' (S n) = reset v0 xs rs n.

  Definition bools_of (vs: stream svalue) (rs: stream bool) :=
    forall n, (vs n = absent /\ rs n = false) \/
         (vs n = present (Venum true_tag) /\ rs n = true) \/
         (vs n = present (Venum false_tag) /\ rs n = false).

  Lemma bools_of_det : forall vs rs rs',
      bools_of vs rs ->
      bools_of vs rs' ->
      rs' = rs.

  Definition bools_ofs (vs : list vstream) (rs : cstream) :=
    exists rss, Forall2 bools_of vs rss /\
           (forall n, rs n = existsb (fun rs => rs n) rss).

  Global Instance bools_ofs_SameElements_Proper:
    Proper (SameElements eq ==> eq ==> Basics.impl)
           bools_ofs.

  Lemma bools_ofs_det : forall vss rs rs',
      bools_ofs vss rs ->
      bools_ofs vss rs' ->
      rs' = rs.

  Lemma bools_ofs_svalue_to_bool:
    forall ys rs n,
      bools_ofs ys rs ->
      Forall (fun y => exists r, svalue_to_bool (y n) = Some r) ys.

  Lemma bools_ofs_svalue_to_bool_true:
    forall ys rs n,
    bools_ofs ys rs ->
    rs n = true <-> Exists (fun y => svalue_to_bool (y n) = Some true) ys.

  Lemma bools_ofs_svalue_to_bool_false:
    forall ys rs n,
    bools_ofs ys rs ->
    rs n = false <-> Forall (fun y => svalue_to_bool (y n) = Some false) ys.

Another formulation for the resetable fby. For the sem -> msem proof, it is simpler to have the fby and reset integrated

  Fixpoint holdreset (v0 : value) (xs : stream svalue) (rs : stream bool) (n : nat) :=
    match n with
    | 0 => v0
    | S m => match rs m, xs m with
            | true, absent => v0
            | false, absent => holdreset v0 xs rs m
            | _, present hv => hv
            end
      end.

  Definition fbyreset (v0: value) (xs: stream svalue) (rs : stream bool) : stream svalue :=
    fun n =>
      match rs n, xs n with
      | _, absent => absent
      | true, _ => present v0
      | false, _ => present (holdreset v0 xs rs n)
      end.

  Lemma reset_fby_fbyreset : forall v0 xs rs,
      reset v0 (fby v0 xs) rs ≈ fbyreset v0 xs rs.

  Definition var_history (H: history) := fun n => (var_env (H n)).

  Section NodeSemantics.

    Variable G: global.

    Inductive sem_equation: stream bool -> history -> equation -> Prop :=
    | SEqDef:
        forall bk H x xs ck ce,
          sem_var H (Var x) xs ->
          sem_arhs bk H ck ce xs ->
          sem_equation bk H (EqDef x ck ce)
    | SEqApp:
        forall bk H x ck f arg xrs ys rs ls xs,
          sem_exps bk H arg ls ->
          sem_vars H x xs ->
          sem_clock bk (var_history H) ck (clock_of ls) ->
          Forall2 (fun '(x, _) => sem_var H (Var x)) xrs ys ->
          bools_ofs ys rs ->
          (forall k, sem_node f (mask k rs ls) (mask k rs xs)) ->
          sem_equation bk H (EqApp x ck f arg xrs)
    | SEqFby:
        forall bk H x ls xs c0 ck le xrs ys rs,
          sem_aexp bk H ck le ls ->
          sem_var H (Var x) xs ->
          Forall2 (fun '(x, _) => sem_var H (Var x)) xrs ys ->
          bools_ofs ys rs ->
          xs = reset (sem_const c0) (fby (sem_const c0) ls) rs ->
          sem_equation bk H (EqFby x ck c0 le xrs)
    | SEqLast:
        forall bk H x ty ck c0 xrs xs ys rs,
          sem_var H (Var x) xs ->
          sem_clocked_var bk H (Var x) ck ->
          Forall2 (fun '(x, _) => sem_var H (Var x)) xrs ys ->
          bools_ofs ys rs ->
          sem_var H (Last x) (reset (sem_const c0) (fby (sem_const c0) xs) rs) ->
          sem_equation bk H (EqLast x ty ck c0 xrs)

    with sem_node: ident -> stream (list svalue) -> stream (list svalue) -> Prop :=
         | SNode:
             forall bk H f xss yss n,
               bk = clock_of xss ->
               find_node f G = Some n ->
               sem_vars H (map fst n.(n_in)) xss ->
               sem_vars H (map fst n.(n_out)) yss ->
               sem_clocked_vars bk H (map (fun '(x, (_, ck)) => (x, (ck, false))) n.(n_in)) ->
               Forall (sem_equation bk H) n.(n_eqs) ->
               sem_node f xss yss.


  End NodeSemantics.

  Global Hint Constructors sem_equation : nlsem.

Induction principle for sem_node and sem_equation

  Section sem_node_mult.
    Variable G: global.

    Variable P_equation: stream bool -> history -> equation -> Prop.
    Variable P_node: ident -> stream (list svalue) -> stream (list svalue) -> Prop.

    Hypothesis EqDefCase:
      forall bk H x xs ck ce,
        sem_var H (Var x) xs ->
        sem_arhs bk H ck ce xs ->
        P_equation bk H (EqDef x ck ce).

    Hypothesis EqAppCase:
      forall bk H x ck f arg xrs ys rs ls xs,
        sem_exps bk H arg ls ->
        sem_vars H x xs ->
        sem_clock bk (var_history H) ck (clock_of ls) ->
        Forall2 (fun '(x, _) => sem_var H (Var x)) xrs ys ->
        bools_ofs ys rs ->
        (forall k, sem_node G f (mask k rs ls) (mask k rs xs)
              /\ P_node f (mask k rs ls) (mask k rs xs)) ->
        P_equation bk H (EqApp x ck f arg xrs).

    Hypothesis EqFbyCase:
      forall bk H x ls xs c0 ck le xrs ys rs,
        sem_aexp bk H ck le ls ->
        sem_var H (Var x) xs ->
        Forall2 (fun '(x, _) => sem_var H (Var x)) xrs ys ->
        bools_ofs ys rs ->
        xs = reset (sem_const c0) (fby (sem_const c0) ls) rs ->
        P_equation bk H (EqFby x ck c0 le xrs).

    Hypothesis EqLastCase:
      forall bk H x ty ck c0 xrs xs ys rs,
        sem_var H (Var x) xs ->
        sem_clocked_var bk H (Var x) ck ->
        Forall2 (fun '(x, _) => sem_var H (Var x)) xrs ys ->
        bools_ofs ys rs ->
        sem_var H (Last x) (reset (sem_const c0) (fby (sem_const c0) xs) rs) ->
        P_equation bk H (EqLast x ty ck c0 xrs).

    Hypothesis NodeCase:
      forall bk H f xss yss n,
        bk = clock_of xss ->
        find_node f G = Some n ->
        sem_vars H (map fst n.(n_in)) xss ->
        sem_vars H (map fst n.(n_out)) yss ->
        sem_clocked_vars bk H (map (fun '(x, (_, ck)) => (x, (ck, false))) n.(n_in)) ->
        Forall (sem_equation G bk H) n.(n_eqs) ->
        Forall (P_equation bk H) n.(n_eqs) ->
        P_node f xss yss.

    Fixpoint sem_equation_mult
            (b: stream bool) (H: history) (e: equation)
            (Sem: sem_equation G b H e) {struct Sem}
      : P_equation b H e
    with sem_node_mult
           (f: ident) (xss oss: stream (list svalue))
           (Sem: sem_node G f xss oss) {struct Sem}
         : P_node f xss oss.

    Combined Scheme sem_node_equation_reset_ind from
             sem_node_mult, sem_equation_mult.

  End sem_node_mult.

  Lemma hold_abs:
    forall n c xs,
      xs n = absent ->
      hold c xs n = hold c xs (S n).

  Lemma hold_pres:
    forall v n c xs,
      xs n = present v ->
      v = hold c xs (S n).

  Lemma sem_node_wf:
    forall G f xss yss,
      sem_node G f xss yss ->
      wf_streams xss /\ wf_streams yss.

Properties of the global environment

  Lemma sem_node_cons:
    forall node G enums externs f xs ys,
      Ordered_nodes (Global enums externs (node::G))
      -> sem_node (Global enums externs (node::G)) f xs ys
      -> node.(n_name) <> f
      -> sem_node (Global enums externs G) f xs ys.

  Lemma sem_node_cons':
    forall node G enums externs f xs ys,
      Ordered_nodes (Global enums externs (node::G))
      -> sem_node (Global enums externs G) f xs ys
      -> node.(n_name) <> f
      -> sem_node (Global enums externs (node::G)) f xs ys.

  Lemma sem_equation_global_tl:
    forall bk nd G H eq enums externs,
      Ordered_nodes (Global enums externs (nd::G)) ->
      ~ Is_node_in_eq nd.(n_name) eq ->
      sem_equation (Global enums externs (nd::G)) bk H eq ->
      sem_equation (Global enums externs G) bk H eq.

  Lemma Forall_sem_equation_global_tl:
    forall bk nd G H eqs enums externs,
      Ordered_nodes (Global enums externs (nd::G))
      -> ~ Is_node_in nd.(n_name) eqs
      -> Forall (sem_equation (Global enums externs (nd::G)) bk H) eqs
      -> Forall (sem_equation (Global enums externs G) bk H) eqs.

  Lemma sem_equation_global_tl':
    forall bk nd G H eq enums externs,
      Ordered_nodes (Global enums externs (nd::G)) ->
      ~ Is_node_in_eq nd.(n_name) eq ->
      sem_equation (Global enums externs G) bk H eq ->
      sem_equation (Global enums externs (nd::G)) bk H eq.

  Lemma Forall_sem_equation_global_tl':
    forall bk nd G H eqs enums externs,
      Ordered_nodes (Global enums externs (nd::G))
      -> ~ Is_node_in nd.(n_name) eqs
      -> Forall (sem_equation (Global enums externs G) bk H) eqs
      -> Forall (sem_equation (Global enums externs (nd::G)) bk H) eqs.

  Lemma sem_equations_permutation:
    forall eqs eqs' G bk H,
      Forall (sem_equation G bk H) eqs ->
      Permutation eqs eqs' ->
      Forall (sem_equation G bk H) eqs'.


  Add Parametric Morphism G: (sem_equation G)
      with signature eq_str ==> eq ==> eq ==> Basics.impl
        as sem_equation_eq_str.

  Add Parametric Morphism G f: (sem_node G f)
      with signature eq_str ==> eq_str ==> Basics.impl
        as sem_node_eq_str.

End NLINDEXEDSEMANTICS.

Module NLIndexedSemanticsFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Cks : CLOCKS Ids Op OpAux)
       (CESyn : CESYNTAX Ids Op OpAux Cks)
       (Syn : NLSYNTAX Ids Op OpAux Cks CESyn)
       (Str : INDEXEDSTREAMS Ids Op OpAux Cks)
       (Ord : NLORDERED Ids Op OpAux Cks CESyn Syn)
       (CESem : CESEMANTICS Ids Op OpAux Cks CESyn Str)
<: NLINDEXEDSEMANTICS Ids Op OpAux Cks CESyn Syn Str Ord CESem.
  Include NLINDEXEDSEMANTICS Ids Op OpAux Cks CESyn Syn Str Ord CESem.
End NLIndexedSemanticsFun.