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

From Coq Require Import Streams.
From Coq Require Import Sorting.Permutation.
From Coq Require Import Setoid.
From Coq Require Import Morphisms.

From Coq Require Import FSets.FMapPositive.
From Velus Require Import Common.
From Velus Require Import CommonProgram.
From Velus Require Import CommonList.
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 Lustre.LOrdered.
From Velus Require Import CoindStreams.

Lustre semantics

Module Type LSEMANTICS
       (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)
       (Import Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Import Lord : LORDERED Ids Op OpAux Cks Senv Syn)
       (Import Str : COINDSTREAMS Ids Op OpAux Cks).

  CoInductive fby1 {A : Type} : A -> Stream (synchronous A) -> Stream (synchronous A) -> Stream (synchronous A) -> Prop :=
  | Fby1A:
      forall v xs ys rs,
        fby1 v xs ys rs ->
        fby1 v (absent ⋅ xs) (absent ⋅ ys) (absent ⋅ rs)
  | Fby1P:
      forall v w s xs ys rs,
        fby1 s xs ys rs ->
        fby1 v (present w ⋅ xs) (present s ⋅ ys) (present v ⋅ rs).

  CoInductive fby {A : Type} : Stream (synchronous A) -> Stream (synchronous A) -> Stream (synchronous A) -> Prop :=
  | FbyA:
      forall xs ys rs,
        fby xs ys rs ->
        fby (absent ⋅ xs) (absent ⋅ ys) (absent ⋅ rs)
  | FbyP:
      forall x y xs ys rs,
        fby1 y xs ys rs ->
        fby (present x ⋅ xs) (present y ⋅ ys) (present x ⋅ rs).

  CoInductive arrow1: Stream svalue -> Stream svalue -> Stream svalue -> Prop :=
  | Arrow1A: forall xs ys rs,
      arrow1 xs ys rs ->
      arrow1 (absent ⋅ xs) (absent ⋅ ys) (absent ⋅ rs)
  | Arrow1P: forall x y xs ys rs,
      arrow1 xs ys rs ->
      arrow1 (present x ⋅ xs) (present y ⋅ ys) (present y ⋅ rs).

  CoInductive arrow: Stream svalue -> Stream svalue -> Stream svalue -> Prop :=
  | ArrowA: forall xs ys rs,
      arrow xs ys rs ->
      arrow (absent ⋅ xs) (absent ⋅ ys) (absent ⋅ rs)
  | ArrowP: forall x y xs ys rs,
      arrow1 xs ys rs ->
      arrow (present x ⋅ xs) (present y ⋅ ys) (present x ⋅ rs).

  Definition history : Type := (history * history).

  Section NodeSemantics.
    Context {PSyn : block -> Prop}.
    Context {prefs : PS.t}.
    Variable G : @global PSyn prefs.

    Section Forall2Brs.
      Variable P : exp -> list (Stream svalue) -> Prop.

      Inductive Forall2Brs : list (enumtag * list exp) -> list (list (enumtag * Stream svalue)) -> Prop :=
      | F2Tnil : forall vs,
          Forall (fun vs => vs = []) vs ->
          Forall2Brs [] vs
      | F2Tcons : forall c es brs vs1 vs2 vs3,
          Forall2 P es vs1 ->
          Forall2Brs brs vs2 ->
          Forall3 (fun v1 vs2 vs3 => vs3 = (c, v1)::vs2) (concat vs1) vs2 vs3 ->
          Forall2Brs ((c, es)::brs) vs3.

    End Forall2Brs.

    Definition mask_hist k rs H := (mask_hist k rs (fst H), mask_hist k rs (snd H)).
    Definition when_hist e Hi cs Hi' :=
      when_hist e (fst Hi) cs (fst Hi')
      /\ when_hist e (snd Hi) cs (snd Hi').

    Section sem_scope.
      Context {A : Type}.

      Variable sem_exp : history -> exp -> list (Stream svalue) -> Prop.
      Variable sem_block : history -> A -> Prop.

      Inductive sem_scope : history -> Stream bool -> (scope A) -> Prop :=
      | Sscope : forall Hi Hi' Hl Hl' bs locs blks,
          (forall x, FEnv.In x Hi' <-> IsVar (senv_of_locs locs) x) ->
          (forall x, FEnv.In x Hl' <-> IsLast (senv_of_locs locs) x) ->

          (forall x ty ck cx e0 clx,
              In (x, (ty, ck, cx, Some (e0, clx))) locs ->
              exists vs0 vs1 vs,
                sem_exp (Hi + Hi', Hl + Hl') e0 [vs0]
                /\ sem_var Hi' x vs1
                /\ fby vs0 vs1 vs
                /\ sem_var Hl' x vs) ->

          sem_block (Hi + Hi', Hl + Hl') blks ->
          sem_scope (Hi, Hl) bs (Scope locs blks).
    End sem_scope.

    Section sem_branch.
      Context {A : Type}.

      Variable sem_block : A -> Prop.

      Inductive sem_branch : (branch A) -> Prop :=
      | Sbranch : forall caus blks,
          sem_block blks ->
          sem_branch (Branch caus blks).
    End sem_branch.

    Inductive sem_exp
      : history -> Stream bool -> exp -> list (Stream svalue) -> Prop :=
    | Sconst:
      forall H b c cs,
        cs ≡ const b c ->
        sem_exp H b (Econst c) [cs]

    | Senum:
      forall H b k ty es,
        es ≡ enum b k ->
        sem_exp H b (Eenum k ty) [es]

    | Svar:
      forall H b x s ann,
        sem_var (fst H) x s ->
        sem_exp H b (Evar x ann) [s]

    | Slast:
      forall H b x s ann,
        sem_var (snd H) x s ->
        sem_exp H b (Elast x ann) [s]

    | Sunop:
      forall H b e op ty s o ann,
        sem_exp H b e [s] ->
        typeof e = [ty] ->
        lift1 op ty s o ->
        sem_exp H b (Eunop op e ann) [o]

    | Sbinop:
      forall H b e1 e2 op ty1 ty2 s1 s2 o ann,
        sem_exp H b e1 [s1] ->
        sem_exp H b e2 [s2] ->
        typeof e1 = [ty1] ->
        typeof e2 = [ty2] ->
        lift2 op ty1 ty2 s1 s2 o ->
        sem_exp H b (Ebinop op e1 e2 ann) [o]

    | Sextcall:
      forall H b f es tyout ck tyins ss vs,
        Forall2 (fun ty cty => ty = Tprimitive cty) (typesof es) tyins ->
        Forall2 (sem_exp H b) es ss ->
        liftn (fun ss => sem_extern f tyins ss tyout) (concat ss) vs ->
        sem_exp H b (Eextcall f es (tyout, ck)) [vs]

    | Sfby:
      forall H b e0s es anns s0ss sss os,
        Forall2 (sem_exp H b) e0s s0ss ->
        Forall2 (sem_exp H b) es sss ->
        Forall3 fby (concat s0ss) (concat sss) os ->
        sem_exp H b (Efby e0s es anns) os

    | Sarrow:
      forall H b e0s es anns s0ss sss os,
        Forall2 (sem_exp H b) e0s s0ss ->
        Forall2 (sem_exp H b) es sss ->
        Forall3 arrow (concat s0ss) (concat sss) os ->
        sem_exp H b (Earrow e0s es anns) os

    | Swhen:
      forall H b x tx s k es lann ss os,
        Forall2 (sem_exp H b) es ss ->
        sem_var (fst H) x s ->
        Forall2 (fun s' => when k s' s) (concat ss) os ->
        sem_exp H b (Ewhen es (x, tx) k lann) os

    | Smerge:
      forall H b x tx s es lann vs os,
        sem_var (fst H) x s ->
        Forall2Brs (sem_exp H b) es vs ->
        Forall2 (merge s) vs os ->
        sem_exp H b (Emerge (x, tx) es lann) os

    | ScaseTotal:
      forall H b e s es tys ck vs os,
        sem_exp H b e [s] ->
        Forall2Brs (sem_exp H b) es vs ->
        Forall3 (case s) vs (List.map (fun _ => None) tys) os ->
        sem_exp H b (Ecase e es None (tys, ck)) os

    | ScaseDefault:
      forall H b e s es d lann vs vd os,
        sem_exp H b e [s] ->
        wt_streams [s] (typeof e) ->
        Forall2Brs (sem_exp H b) es vs ->
        Forall2 (sem_exp H b) d vd ->
        Forall3 (case s) vs (List.map Some (concat vd)) os ->
        sem_exp H b (Ecase e es (Some d) lann) os

    | Sapp:
      forall H b f es er lann ss os rs bs,
        Forall2 (sem_exp H b) es ss ->
        Forall2 (fun e r => sem_exp H b e [r]) er rs ->
        bools_ofs rs bs ->
        (forall k, sem_node f (List.map (maskv k bs) (concat ss)) (List.map (maskv k bs) os)) ->
        sem_exp H b (Eapp f es er lann) os

    with sem_equation: history -> Stream bool -> equation -> Prop :=
      Seq:
        forall H b xs es ss,
          Forall2 (sem_exp H b) es ss ->
          Forall2 (sem_var (fst H)) xs (concat ss) ->
          sem_equation H b (xs, es)

    with sem_block: history -> Stream bool -> block -> Prop :=
    | Sbeq:
      forall H b eq,
        sem_equation H b eq ->
        sem_block H b (Beq eq)

    | Sreset:
      forall H b blocks er sr r,
        sem_exp H b er [sr] ->
        bools_of sr r ->
        (forall k, Forall (sem_block (mask_hist k r H) (maskb k r b)) blocks) ->
        sem_block H b (Breset blocks er)

    | Sswitch:
      forall Hi b ec branches sc,
        sem_exp Hi b ec [sc] ->
        wt_streams [sc] (typeof ec) ->
        Forall (fun blks =>
                  exists Hi', when_hist (fst blks) Hi sc Hi'
                         /\ let bi := fwhenb (fst blks) sc b in
                           sem_branch (Forall (sem_block Hi' bi)) (snd blks)) branches ->
        sem_block Hi b (Bswitch ec branches)

    | Slocal:
      forall Hi bs scope,
        sem_scope (fun Hi' => sem_exp Hi' bs) (fun Hi' => Forall (sem_block Hi' bs)) Hi bs scope ->
        sem_block Hi bs (Blocal scope)

    with sem_node: ident -> list (Stream svalue) -> list (Stream svalue) -> Prop :=
    | Snode:
      forall f ss os n H b,
          find_node f G = Some n ->
          Forall2 (sem_var H) (idents n.(n_in)) ss ->
          Forall2 (sem_var H) (idents n.(n_out)) os ->
          sem_block (H, FEnv.empty _) b n.(n_block) ->
          b = clocks_of ss ->
          sem_node f ss os.

  End NodeSemantics.

  Ltac inv_exp :=
    match goal with
    | H:sem_exp _ _ _ _ _ |- _ => inv H
    end.

  Ltac inv_scope :=
    match goal with
    | H:sem_scope _ _ _ _ _ |- _ => inv H
    end;
    destruct_conjs; subst.

  Ltac inv_branch :=
    match goal with
    | H:sem_branch _ _ |- _ => inv H
    end;
    destruct_conjs; subst.

  Ltac inv_block :=
    match goal with
    | H:sem_block _ _ _ _ |- _ => inv H
    end.

Properties of Forall2Brs

  Lemma Forall2Brs_impl_In (P1 P2 : _ -> _ -> Prop) : forall es vs,
      (forall x y, List.Exists (fun es => In x (snd es)) es -> P1 x y -> P2 x y) ->
      Forall2Brs P1 es vs ->
      Forall2Brs P2 es vs.

  Lemma Forall2Brs_fst P : forall es vs,
      Forall2Brs P es vs ->
      Forall (fun vs => List.map fst vs = List.map fst es) vs.

  Lemma Forall2Brs_length1 (P : _ -> _ -> Prop) : forall es vs,
      Forall (fun es => Forall (fun e => forall v, P e v -> length v = numstreams e) (snd es)) es ->
      Forall2Brs P es vs ->
      Forall (fun es => length (annots (snd es)) = length vs) es.

  Lemma Forall2Brs_length2 (P : _ -> _ -> Prop) : forall es vs,
      Forall2Brs P es vs ->
      Forall (fun vs => length vs = length es) vs.

  Lemma Forall2Brs_map_1 (P : _ -> _ -> Prop) f : forall es vs,
      Forall2Brs (fun e => P (f e)) es vs <->
      Forall2Brs P (List.map (fun '(i, es) => (i, List.map f es)) es) vs.

  Lemma Forall2Brs_map_2 (P : _ -> _ -> Prop) f : forall es vs,
      Forall2Brs (fun e vs => P e (List.map f vs)) es vs ->
      Forall2Brs P es (List.map (List.map (fun '(i, v) => (i, f v))) vs).

properties of the global environment

  Ltac sem_cons :=
    intros; simpl_Forall; solve_Exists;
    unfold Is_node_in_eq in *;
    match goal with
    | H: Forall2Brs _ ?l1 ?l2 |- Forall2Brs _ ?l1 ?l2 =>
        eapply Forall2Brs_impl_In in H; eauto; intros; sem_cons
    | H: forall _, _ -> _ -> _ -> sem_exp _ _ _ ?e _ |- sem_exp _ _ _ ?e _ => eapply H; eauto
    | H: forall _ _, _ -> _ -> _ -> sem_block _ _ _ ?e |- sem_block _ _ _ ?e => eapply H; eauto
    | H: forall (_ : ident) (xs ys : list (Stream svalue)), _ -> _ -> sem_node _ _ _ _ |- sem_node _ _ _ _ =>
        eapply H; eauto using Is_node_in_exp; econstructor; sem_cons
    | Hname: n_name ?nd <> _, Hfind: find_node _ {| types := _; nodes := ?nd :: _ |} = _ |- _ =>
        rewrite find_node_other in Hfind; auto
    | Hname: n_name ?nd <> _ |- find_node _ {| types := _; nodes := ?nd :: _ |} = _ =>
        rewrite find_node_other; auto
    | Hname: n_name ?nd <> _ |- ~_ => idtac
    | H: ~Is_node_in_exp _ (Eapp _ _ _ _) |- _ <> _ => contradict H; subst; eapply INEapp2
    | H: ~_ |- ~_ => contradict H; try constructor; sem_cons
    | |- _ \/ _ => solve [left;sem_cons|right;sem_cons]
    | |- exists d, Some _ = Some d /\ List.Exists _ d =>
        do 2 esplit; [reflexivity|sem_cons]
    | k: nat,H: forall (_ : nat), _ |- _ => specialize (H k); sem_cons
    | H: Forall2 _ ?xs _ |- Forall2 _ ?xs _ =>
        eapply Forall2_impl_In in H; eauto; intros; sem_cons
    | |- exists _, when_hist _ _ _ _ /\ _ =>
        do 2 esplit; [auto|sem_cons]
    | H: forall _ _ _ _ _ _, In _ _ -> exists _ _ _, _ /\ _ /\ _ /\ _ |- exists _ _ _, _ /\ _ /\ _ /\ _ =>
        edestruct H as (?&?&?&?&?&?&?); eauto;
        do 3 esplit; split; [|split; [|split]]; eauto; sem_cons
    | H:sem_branch _ _ |- _ =>
        inv H; destruct_conjs
    | |- sem_branch _ _ => econstructor; eauto
    | |- Is_node_in_branch _ _ => econstructor; sem_cons
    | H:sem_scope _ _ _ _ _ |- sem_scope _ _ _ _ _ =>
        inv H; destruct_conjs; econstructor; eauto
    | |- Is_node_in_scope _ _ _ => econstructor; sem_cons
    | |- _ /\ _ => split; sem_cons
    | |- exists _ _, _ /\ _ /\ _ =>
        do 2 esplit; split; [|split]; eauto; sem_cons
    | _ => auto
    end.

  Section sem_cons.
    Context {PSyn prefs} (nd : @node PSyn prefs) (nds : list (@node PSyn prefs)).
    Context (typs : list type) (externs : list (ident * (list ctype * ctype))).

    Lemma sem_exp_cons1' :
      forall H bk e vs,
        (forall f xs ys, Is_node_in_exp f e -> sem_node (Global typs externs (nd::nds)) f xs ys -> sem_node (Global typs externs nds) f xs ys) ->
        sem_exp (Global typs externs (nd::nds)) H bk e vs ->
        ~Is_node_in_exp nd.(n_name) e ->
        sem_exp (Global typs externs nds) H bk e vs.

    Lemma sem_block_cons1' :
      forall blk H bk,
        (forall f xs ys, Is_node_in_block f blk -> sem_node (Global typs externs (nd::nds)) f xs ys -> sem_node (Global typs externs nds) f xs ys) ->
        sem_block (Global typs externs (nd::nds)) H bk blk ->
        ~Is_node_in_block nd.(n_name) blk ->
        sem_block (Global typs externs nds) H bk blk.

  End sem_cons.

  Lemma sem_node_cons1 {PSyn prefs} :
    forall (nd : @node PSyn prefs) nds typs externs f xs ys,
      Ordered_nodes (Global typs externs (nd::nds)) ->
      sem_node (Global typs externs (nd::nds)) f xs ys ->
      nd.(n_name) <> f ->
      sem_node (Global typs externs nds) f xs ys.

  Corollary sem_block_cons1 {PSyn prefs} :
    forall (nd : @node PSyn prefs) nds typs externs blk Hi bs,
      Ordered_nodes (Global typs externs (nd::nds)) ->
      sem_block (Global typs externs (nd::nds)) Hi bs blk ->
      ~Is_node_in_block nd.(n_name) blk ->
      sem_block (Global typs externs nds) Hi bs blk.

  Add Parametric Morphism {A} (v : A) : (fby1 v)
      with signature @EqSt _ ==> @EqSt _ ==> @EqSt _ ==> Basics.impl
        as fby1_EqSt.

  Add Parametric Morphism {A} : (@fby A)
      with signature @EqSt _ ==> @EqSt _ ==> @EqSt _ ==> Basics.impl
        as fby_EqSt.

  Add Parametric Morphism : arrow1
      with signature @EqSt _ ==> @EqSt _ ==> @EqSt _ ==> Basics.impl
        as arrow1_EqSt.

  Add Parametric Morphism : arrow
      with signature @EqSt _ ==> @EqSt _ ==> @EqSt _ ==> Basics.impl
        as arrow_EqSt.

  Add Parametric Morphism k : (when k)
      with signature @EqSt svalue ==> @EqSt svalue ==> @EqSt svalue ==> Basics.impl
        as when_EqSt.

  Add Parametric Morphism : const
      with signature @EqSt bool ==> eq ==> @EqSt svalue
        as const_EqSt.

  Add Parametric Morphism : enum
      with signature @EqSt bool ==> eq ==> @EqSt svalue
        as enum_EqSt.

  Add Parametric Morphism : sem_var
      with signature FEnv.Equiv (@EqSt _) ==> eq ==> @EqSt svalue ==> Basics.impl
        as sem_var_EqSt.

  Definition history_equiv (Hi1 Hi2 : history) : Prop :=
    FEnv.Equiv (@EqSt _) (fst Hi1) (fst Hi2) /\ FEnv.Equiv (@EqSt _) (snd Hi1) (snd Hi2).

  Global Instance history_equiv_refl : Reflexive history_equiv.

  Add Parametric Morphism {PSyn prefs} (G : @global PSyn prefs) : (sem_exp G)
      with signature history_equiv ==> @EqSt bool ==> eq ==> @EqSts svalue ==> Basics.impl
        as sem_exp_morph.

  Add Parametric Morphism {PSyn prefs} (G : @global PSyn prefs) : (sem_equation G)
      with signature history_equiv ==> @EqSt bool ==> eq ==> Basics.impl
        as sem_equation_morph.

  Add Parametric Morphism {PSyn prefs} (G : @global PSyn prefs) : (sem_block G)
      with signature history_equiv ==> @EqSt bool ==> eq ==> Basics.impl
        as sem_block_morph.

  Add Parametric Morphism {PSyn prefs} (G : @global PSyn prefs) : (sem_node G)
      with signature eq ==> @EqSts svalue ==> @EqSts svalue ==> Basics.impl
        as sem_node_morph.

  Fact sem_var_In : forall H x vs,
      sem_var H x vs ->
      FEnv.In x H.

  Corollary sem_vars_In : forall H xs vs,
      Forall2 (sem_var H) xs vs ->
      Forall (fun v => FEnv.In v H) xs.

All the defined variables have a semantic

  Ltac inv_scope' := (Syn.inv_scope || inv_scope).
  Ltac inv_branch' := (Syn.inv_branch || inv_branch).
  Ltac inv_block' := (Syn.inv_block || inv_block).

  Lemma sem_block_defined {PSyn prefs} (G: @global PSyn prefs) : forall blk H bs x,
      sem_block G H bs blk ->
      Is_defined_in x blk ->
      FEnv.In x (fst H).

  Corollary Forall_sem_block_defined {PSyn prefs} (G: @global PSyn prefs) : forall blks x H bs,
      Forall (sem_block G H bs) blks ->
      List.Exists (Is_defined_in x) blks ->
      FEnv.In x (fst H).

  Lemma sem_scope_defined {PSyn prefs} (G: @global PSyn prefs) : forall locs blks Hi bs x,
      sem_scope (fun Hi => sem_exp G Hi bs) (fun Hi => Forall (sem_block G Hi bs)) Hi bs (Scope locs blks) ->
      Is_defined_in_scope (List.Exists (Is_defined_in x)) x (Scope locs blks) ->
      FEnv.In x (fst Hi).

  Corollary sem_scope_defined1 {PSyn prefs} (G: @global PSyn prefs) :
    forall locs blks Hi bs Γ xs x,
      sem_scope (fun Hi => sem_exp G Hi bs) (fun Hi => Forall (sem_block G Hi bs)) Hi bs (Scope locs blks) ->
      VarsDefinedScope (fun blks ys => exists xs, Forall2 VarsDefined blks xs /\ Permutation (concat xs) ys) (Scope locs blks) xs ->
      NoDupScope (fun Γ => Forall (NoDupLocals Γ)) Γ (Scope locs blks) ->
      incl xs Γ ->
      In x xs ->
      FEnv.In x (fst Hi).

  Corollary sem_scope_defined2 {A} {PSyn prefs} (G: @global PSyn prefs) :
    forall locs (blks: _ * A) Hi bs Γ xs x,
      sem_scope (fun Hi => sem_exp G Hi bs) (fun Hi blks => Forall (sem_block G Hi bs) (fst blks)) Hi bs (Scope locs blks) ->
      VarsDefinedScope (fun blks ys => exists xs, Forall2 VarsDefined (fst blks) xs /\ Permutation (concat xs) ys) (Scope locs blks) xs ->
      NoDupScope (fun Γ blks => Forall (NoDupLocals Γ) (fst blks)) Γ (Scope locs blks) ->
      incl xs Γ ->
      In x xs ->
      FEnv.In x (fst Hi).

  Lemma sem_branch_defined {PSyn prefs} (G: @global PSyn prefs) : forall caus blks Hi bs x,
      sem_branch (Forall (sem_block G Hi bs)) (Branch caus blks) ->
      Is_defined_in_branch (List.Exists (Is_defined_in x)) (Branch caus blks) ->
      FEnv.In x (fst Hi).

  Corollary sem_branch_defined1 {PSyn prefs} (G: @global PSyn prefs) :
    forall caus blks Hi bs Γ xs x,
      sem_branch (Forall (sem_block G Hi bs)) (Branch caus blks) ->
      VarsDefinedBranch (fun blks ys => exists xs, Forall2 VarsDefined blks xs /\ Permutation (concat xs) ys) (Branch caus blks) xs ->
      NoDupBranch (Forall (NoDupLocals Γ)) (Branch caus blks) ->
      incl xs Γ ->
      In x xs ->
      FEnv.In x (fst Hi).

  Corollary sem_branch_defined2 {A} {PSyn prefs} (G: @global PSyn prefs) :
    forall caus (blks: (A * scope (_ * A))) Hi bs Γ xs x,
      sem_branch
        (fun blks =>
           sem_scope (fun Hi => sem_exp G Hi bs)
             (fun Hi blks => Forall (sem_block G Hi bs) (fst blks)) Hi bs (snd blks))
        (Branch caus blks) ->
      VarsDefinedBranch
        (fun blks => VarsDefinedScope (fun blks ys => exists xs, Forall2 VarsDefined (fst blks) xs /\ Permutation (concat xs) ys) (snd blks))
        (Branch caus blks) xs ->
      NoDupBranch
        (fun blks => NoDupScope (fun Γ blks => Forall (NoDupLocals Γ) (fst blks)) Γ (snd blks))
        (Branch caus blks) ->
      incl xs Γ ->
      In x xs ->
      FEnv.In x (fst Hi).

Preservation of the semantics while refining an environment

  Fact refines_eq_EqSt {A} : forall H H' ,
      FEnv.refines eq H H' ->
      FEnv.refines (@EqSt A) H H'.

  Fact sem_var_refines : forall H H' id v,
      H ⊑ H' ->
      sem_var H id v ->
      sem_var H' id v.

  Lemma sem_var_refines_inv : forall env Hi1 Hi2 x vs,
      List.In x env ->
      FEnv.dom_lb Hi1 env ->
      (forall vs, sem_var Hi1 x vs -> sem_var Hi2 x vs) ->
      sem_var Hi2 x vs ->
      sem_var Hi1 x vs.

  Lemma sem_var_refines' : forall Hi1 Hi2 x vs,
      FEnv.In x Hi1 ->
      Hi1 ⊑ Hi2 ->
      sem_var Hi2 x vs ->
      sem_var Hi1 x vs.

  Corollary sem_var_refines'' : forall env Hi1 Hi2 x vs,
      List.In x env ->
      FEnv.dom_lb Hi1 env ->
      Hi1 ⊑ Hi2 ->
      sem_var Hi2 x vs ->
      sem_var Hi1 x vs.

  Lemma sem_clock_refines : forall H H' ck bs bs',
      H ⊑ H' ->
      sem_clock H bs ck bs' ->
      sem_clock H' bs ck bs'.

  Lemma sem_clock_refines' : forall vars H H' ck bs bs',
      wx_clock vars ck ->
      (forall x vs, IsVar vars x -> sem_var H x vs -> sem_var H' x vs) ->
      sem_clock H bs ck bs' ->
      sem_clock H' bs ck bs'.

  Fact sem_exp_refines {PSyn prefs} : forall (G : @global PSyn prefs) b e H H' Hl v,
      H ⊑ H' ->
      sem_exp G (H, Hl) b e v ->
      sem_exp G (H', Hl) b e v.

  Fact sem_equation_refines {PSyn prefs} : forall (G : @global PSyn prefs) H H' Hl b equ,
      H ⊑ H' ->
      sem_equation G (H, Hl) b equ ->
      sem_equation G (H', Hl) b equ.

  Fact sem_block_refines {PSyn prefs} : forall (G: @global PSyn prefs) d H H' Hl b,
      H ⊑ H' ->
      sem_block G (H, Hl) b d ->
      sem_block G (H', Hl) b d.

  Section props.
    Context {PSyn : block -> Prop}.
    Context {prefs : PS.t}.
    Variable (G : @global PSyn prefs).


    Fact sem_exp_numstreams : forall H b e v,
        wl_exp G e ->
        sem_exp G H b e v ->
        length v = numstreams e.

    Corollary sem_exps_numstreams : forall H b es vs,
        Forall (wl_exp G) es ->
        Forall2 (sem_exp G H b) es vs ->
        length (concat vs) = length (annots es).

    Lemma sem_vars_mask_inv: forall k r H xs vs,
        Forall2 (sem_var (Str.mask_hist k r H)) xs vs ->
        exists vs', Forall2 (sem_var H) xs vs' /\ EqSts vs (List.map (maskv k r) vs').

    Fact sem_block_sem_var : forall blk x Hi bs,
        Is_defined_in x blk ->
        sem_block G Hi bs blk ->
        exists vs, sem_var (fst Hi) x vs.

    Corollary sem_block_dom_lb : forall blk xs Hi Hl bs,
        VarsDefined blk xs ->
        NoDupLocals xs blk ->
        sem_block G (Hi, Hl) bs blk ->
        FEnv.dom_lb Hi xs.

    Corollary Forall_sem_block_dom_lb : forall blks xs ys Hi Hl bs,
        Forall2 VarsDefined blks xs ->
        Forall (NoDupLocals ys) blks ->
        Forall (sem_block G (Hi, Hl) bs) blks ->
        Permutation (concat xs) ys ->
        FEnv.dom_lb Hi ys.

  End props.

Restriction

  Fact sem_var_restrict : forall vars H id v,
      List.In id vars ->
      sem_var H id v ->
      sem_var (FEnv.restrict H vars) id v.

  Fact sem_var_restrict_inv : forall vars H id v,
      sem_var (FEnv.restrict H vars) id v ->
      List.In id vars /\ sem_var H id v.

  Fact sem_clock_restrict : forall vars ck H bs bs',
      wx_clock vars ck ->
      sem_clock H bs ck bs' ->
      sem_clock (FEnv.restrict H (List.map fst vars)) bs ck bs'.

  Fact sem_exp_restrict {PSyn prefs} : forall (G : @global PSyn prefs) Γ H Hl b e vs,
      wx_exp Γ e ->
      sem_exp G (H, Hl) b e vs ->
      sem_exp G (FEnv.restrict H (List.map fst Γ), Hl) b e vs.

  Lemma sem_equation_restrict {PSyn prefs} : forall (G : @global PSyn prefs) Γ H Hl b eq,
      wx_equation Γ eq ->
      sem_equation G (H, Hl) b eq ->
      sem_equation G (FEnv.restrict H (List.map fst Γ), Hl) b eq.

  Lemma sem_scope_restrict {A} (wx_block : _ -> _ -> Prop) (sem_block : _ -> _ -> Prop) {PSyn prefs} (G: @global PSyn prefs) :
    forall Γ Hi Hl bs locs (blks : A),
      (forall Γ Hi Hi' Hl,
          wx_block Γ blks ->
          sem_block (Hi, Hl) blks ->
          FEnv.Equiv (@EqSt _) Hi' (FEnv.restrict Hi (List.map fst Γ)) ->
          sem_block (Hi', Hl) blks) ->
      wx_scope wx_block Γ (Scope locs blks) ->
      sem_scope (fun Hi' => sem_exp G Hi' bs) sem_block (Hi, Hl) bs (Scope locs blks) ->
      sem_scope (fun Hi' => sem_exp G Hi' bs) sem_block (FEnv.restrict Hi (List.map fst Γ), Hl) bs (Scope locs blks).

  Lemma sem_block_restrict {PSyn prefs} : forall (G: @global PSyn prefs) blk Γ H Hl b,
      wx_block Γ blk ->
      sem_block G (H, Hl) b blk ->
      sem_block G (FEnv.restrict H (List.map fst Γ), Hl) b blk.

Alignment

  Lemma ac_fby1 {A} :
    forall xs ys rs,
      @fby A xs ys rs -> abstract_clock xs ≡ abstract_clock rs.

  Lemma ac_fby2 {A} :
    forall xs ys rs,
      @fby A xs ys rs -> abstract_clock ys ≡ abstract_clock rs.

  Lemma fby_aligned {A} : forall bs (xs ys zs: Stream (synchronous A)),
      fby xs ys zs ->
      (aligned xs bs \/ aligned ys bs \/ aligned zs bs) ->
      (aligned xs bs /\ aligned ys bs /\ aligned zs bs).

  Lemma ac_arrow1 : forall xs ys rs,
      arrow xs ys rs -> abstract_clock xs ≡ abstract_clock rs.

  Lemma ac_arrow2 : forall xs ys rs,
      arrow xs ys rs -> abstract_clock ys ≡ abstract_clock rs.

  Lemma arrow_aligned : forall bs xs ys zs,
      arrow xs ys zs ->
      (aligned xs bs \/ aligned ys bs \/ aligned zs bs) ->
      (aligned xs bs /\ aligned ys bs /\ aligned zs bs).

End LSEMANTICS.

Module LSemanticsFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Cks : CLOCKS Ids Op OpAux)
       (Senv : STATICENV Ids Op OpAux Cks)
       (Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Lord : LORDERED Ids Op OpAux Cks Senv Syn)
       (Str : COINDSTREAMS Ids Op OpAux Cks)
<: LSEMANTICS Ids Op OpAux Cks Senv Syn Lord Str.
  Include LSEMANTICS Ids Op OpAux Cks Senv Syn Lord Str.
End LSemanticsFun.