Module LClockedSemantics

From Coq Require Import Streams.
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 FSets.FMapPositive.
From Velus Require Import Common.
From Velus Require Import CommonList.
From Velus Require Import FunctionalEnvironment.
From Velus Require Import Operators.
From Velus Require Import CoindStreams IndexedStreams.
From Velus Require Import CoindIndexed.
From Velus Require Import Clocks.
From Velus Require Import Lustre.StaticEnv.
From Velus Require Import Lustre.LSyntax Lustre.LClocking Lustre.LOrdered.
From Velus Require Import Lustre.LSemantics.

Module Type LCLOCKEDSEMANTICS
       (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 Clo : LCLOCKING Ids Op OpAux Cks Senv Syn)
       (Import Lord : LORDERED Ids Op OpAux Cks Senv Syn)
       (Import CStr : COINDSTREAMS Ids Op OpAux Cks)
       (Import Sem : LSEMANTICS Ids Op OpAux Cks Senv Syn Lord CStr).

  Import CStr.
  Module IStr := IndexedStreamsFun Ids Op OpAux Cks.
  Module Import CIStr := CoindIndexedFun Ids Op OpAux Cks CStr IStr.

  Lemma history_tl_same_find {K} : forall (H H' : @history K) vars,
      Forall (fun x => orel (EqSt (A:=svalue)) (H x) (H' x)) vars ->
      Forall (fun x => orel (EqSt (A:=svalue)) ((history_tl H) x) ((history_tl H') x)) vars.

  Import List.

  Lemma sem_clock_same_find : forall H H' vars ck bs bs',
      wc_clock vars ck ->
      Forall (fun x => orel (EqSt (A:=svalue)) (H' x) (H x)) (map fst vars) ->
      sem_clock H bs ck bs' ->
      sem_clock H' bs ck bs'.

Clocked semantics

  Section ClockedSemantics.
    Definition sc_vars Γ H bs :=
      (forall x ck xs, HasClock Γ x ck -> sem_var H (Var x) xs -> sem_clock (var_history H) bs ck (abstract_clock xs))
      /\ (forall x ck xs, HasClock Γ x ck -> IsLast Γ x -> sem_var H (Last x) xs -> sem_clock (var_history H) bs ck (abstract_clock xs)).

    Definition clocked_node H bs (env : static_env) :=
      dom H env /\ sc_vars env H bs.

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

    Section sem_scope.

      Context {A : Type}.

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

      Inductive sem_scope_ck : Sem.history -> Stream bool -> (scope A) -> Prop :=
      | Sscope : forall Hi Hi' bs locs blks,
          dom Hi' (senv_of_decls locs) ->

          Forall (sem_last_decl sem_exp Hi Hi' bs) locs ->

          sc_vars (senv_of_decls locs) (Hi + Hi') bs ->

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

    Section sem_branch.
      Context {A : Type}.

      Variable sem_block : A -> Prop.

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

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

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

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

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

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

    | Sbinop:
        forall H b e1 e2 op ty1 ty2 s1 s2 o ann,
          sem_exp_ck H b e1 [s1] ->
          sem_exp_ck H b e2 [s2] ->
          typeof e1 = [ty1] ->
          typeof e2 = [ty2] ->
          lift2 op ty1 ty2 s1 s2 o ->
          sem_exp_ck 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_ck H b) es ss ->
        liftn (fun ss => sem_extern f tyins ss tyout) (concat ss) vs ->
        sem_exp_ck H b (Eextcall f es (tyout, ck)) [vs]

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

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

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

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

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

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

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

    with sem_equation_ck: Sem.history -> Stream bool -> equation -> Prop :=
      Seq:
        forall H b xs es ss,
          Forall2 (sem_exp_ck H b) es ss ->
          Forall2 (fun x => sem_var H (Var x)) xs (concat ss) ->
          sem_equation_ck H b (xs, es)

    with sem_transitions_ck : Sem.history -> Stream bool -> list (exp * (enumtag * bool)) -> (enumtag * bool) -> Stream (synchronous (enumtag * bool)) -> Prop :=
    | Stransdef : forall H bs default stres,
        stres ≡ const_stres bs default ->
        sem_transitions_ck H bs [] default stres
    | Strans : forall H bs e C r trans default vs bs' stres1 stres,
        sem_exp_ck H bs e [vs] ->
        bools_of vs bs' ->
        sem_transitions_ck H bs trans default stres1 ->
        stres ≡ choose_first (const_stres bs' (C, r)) stres1 ->
        sem_transitions_ck H bs ((e, (C, r))::trans) default stres

    with sem_block_ck: Sem.history -> Stream bool -> block -> Prop :=
    | Sbeq:
      forall H b eq,
        sem_equation_ck H b eq ->
        sem_block_ck H b (Beq eq)

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

    | Sswitch:
      forall Hi b ec branches sc,
        sem_exp_ck 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) b sc in
                           sem_branch_ck (Forall (sem_block_ck Hi' bi)) (snd blks)) branches ->
        sem_block_ck Hi b (Bswitch ec branches)

    | SautoWeak:
      forall H bs ini oth states ck bs' stres0 stres1 stres,
        sem_clock (var_history H) bs ck bs' ->
        sem_transitions_ck H bs' (List.map (fun '(e, t) => (e, (t, false))) ini) (oth, false) stres0 ->
        fby stres0 stres1 stres ->
        Forall (fun state =>
                  let tag := fst (fst state) in
                  forall k, exists Hik, select_hist tag k stres H Hik
                              /\ let bik := fselectb tag k stres bs in
                                sem_branch_ck
                                  (fun blks =>
                                     sem_scope_ck sem_exp_ck
                                       (fun Hi' blks =>
                                          Forall (sem_block_ck Hi' bik) (fst blks)
                                          /\ sem_transitions_ck Hi' bik (snd blks) (tag, false) (fselect absent tag k stres stres1)
                                       ) Hik bik (snd blks)) (snd state)
               ) states ->
        sem_block_ck H bs (Bauto Weak ck (ini, oth) states)

    | SautoStrong:
      forall H bs ini states ck bs' stres stres1,
        sem_clock (var_history H) bs ck bs' ->
        fby (const_stres bs' (ini, false)) stres1 stres ->
        Forall (fun state =>
                  let tag := fst (fst state) in
                  forall k, exists Hik, select_hist tag k stres H Hik
                              /\ let bik := fselectb tag k stres bs in
                                sem_branch_ck
                                  (fun blks =>
                                     sem_transitions_ck Hik bik (fst blks) (tag, false) (fselect absent tag k stres stres1)
                                  ) (snd state)
               ) states ->
        Forall (fun state =>
                  let tag := fst (fst state) in
                  forall k, exists Hik, select_hist tag k stres1 H Hik
                              /\ let bik := fselectb tag k stres1 bs in
                                sem_branch_ck
                                  (fun blks =>
                                     sem_scope_ck sem_exp_ck
                                       (fun Hi' blks => Forall (sem_block_ck Hi' bik) (fst blks)
                                       ) Hik bik (snd blks)) (snd state)
               ) states ->
        sem_block_ck H bs (Bauto Strong ck ([], ini) states)

    | Slocal:
      forall Hi bs scope,
        sem_scope_ck sem_exp_ck (fun Hi' => Forall (sem_block_ck Hi' bs)) Hi bs scope ->
        sem_block_ck Hi bs (Blocal scope)

    with sem_node_ck: ident -> list (Stream svalue) -> list (Stream svalue) -> Prop :=
      Snode:
        forall f ss os n H,
          find_node f G = Some n ->
          Forall2 (fun x => sem_var H (Var x)) (List.map fst n.(n_in)) ss ->
          Forall2 (fun x => sem_var H (Var x)) (List.map fst n.(n_out)) os ->
          let bs := clocks_of ss in
          Forall (sem_last_decl sem_exp_ck (FEnv.empty _) H bs) n.(n_out) ->
          sem_block_ck H bs n.(n_block) ->
          clocked_node H bs (senv_of_ins n.(n_in) ++ senv_of_decls n.(n_out)) ->
          sem_node_ck f ss os.

  End ClockedSemantics.

  Global Hint Constructors sem_exp_ck sem_equation_ck sem_scope_ck sem_branch_ck sem_block_ck : lcsem.

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

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

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

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

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


  Section sem_exp_ind2.
    Context {prefs PSyn} (G: @global prefs PSyn).

    Variable P_exp : Sem.history -> Stream bool -> exp -> list (Stream svalue) -> Prop.
    Variable P_equation : Sem.history -> Stream bool -> equation -> Prop.
    Variable P_transitions : Sem.history -> Stream bool -> list (exp * (enumtag * bool)) -> (enumtag * bool) -> Stream (synchronous (enumtag * bool)) -> Prop.
    Variable P_block : Sem.history -> Stream bool -> block -> Prop.
    Variable P_node : ident -> list (Stream svalue) -> list (Stream svalue) -> Prop.

    Hypothesis ConstCase:
      forall H b c cs,
        cs ≡ const b c ->
        P_exp H b (Econst c) [cs].

    Hypothesis EnumCase:
      forall H b k ty es,
        es ≡ enum b k ->
        P_exp H b (Eenum k ty) [es].

    Hypothesis VarCase:
      forall H b x s ann,
        sem_var H (Var x) s ->
        P_exp H b (Evar x ann) [s].

    Hypothesis LastCase:
      forall H b x s ann,
        sem_var H (Last x) s ->
        P_exp H b (Elast x ann) [s].

    Hypothesis UnopCase:
      forall H b e op ty s o ann,
        sem_exp_ck G H b e [s] ->
        P_exp H b e [s] ->
        typeof e = [ty] ->
        lift1 op ty s o ->
        P_exp H b (Eunop op e ann) [o].

    Hypothesis BinopCase:
      forall H b e1 e2 op ty1 ty2 s1 s2 o ann,
        sem_exp_ck G H b e1 [s1] ->
        P_exp H b e1 [s1] ->
        sem_exp_ck G H b e2 [s2] ->
        P_exp H b e2 [s2] ->
        typeof e1 = [ty1] ->
        typeof e2 = [ty2] ->
        lift2 op ty1 ty2 s1 s2 o ->
        P_exp H b (Ebinop op e1 e2 ann) [o].

    Hypothesis ExtcallCase:
      forall H b f es tyout ck tyins ss vs,
        Forall2 (fun cty ty => cty = Tprimitive ty) (typesof es) tyins ->
        Forall2 (sem_exp_ck G H b) es ss ->
        Forall2 (P_exp H b) es ss ->
        liftn (fun ss => sem_extern f tyins ss tyout) (concat ss) vs ->
        P_exp H b (Eextcall f es (tyout, ck)) [vs].

    Hypothesis FbyCase:
      forall H b e0s es anns s0ss sss os,
        Forall2 (sem_exp_ck G H b) e0s s0ss ->
        Forall2 (P_exp H b) e0s s0ss ->
        Forall2 (sem_exp_ck G H b) es sss ->
        Forall2 (P_exp H b) es sss ->
        Forall3 fby (concat s0ss) (concat sss) os ->
        P_exp H b (Efby e0s es anns) os.

    Hypothesis ArrowCase:
      forall H b e0s es anns s0ss sss os,
        Forall2 (sem_exp_ck G H b) e0s s0ss ->
        Forall2 (P_exp H b) e0s s0ss ->
        Forall2 (sem_exp_ck G H b) es sss ->
        Forall2 (P_exp H b) es sss ->
        Forall3 arrow (concat s0ss) (concat sss) os ->
        P_exp H b (Earrow e0s es anns) os.

    Hypothesis WhenCase:
      forall H b x tx s k es lann ss os,
        Forall2 (sem_exp_ck G H b) es ss ->
        Forall2 (P_exp H b) es ss ->
        sem_var H (Var x) s ->
        Forall2 (fun s' => when k s' s) (concat ss) os ->
        P_exp H b (Ewhen es (x, tx) k lann) os.

    Hypothesis MergeCase:
      forall H b x tx s es lann vs os,
        sem_var H (Var x) s ->
        Forall2Brs (sem_exp_ck G H b) es vs ->
        Forall2Brs (P_exp H b) es vs ->
        Forall2 (merge s) vs os ->
        P_exp H b (Emerge (x, tx) es lann) os.

    Hypothesis CaseTotalCase:
      forall H b e s es tys ck vs os,
        sem_exp_ck G H b e [s] ->
        P_exp H b e [s] ->
        Forall2Brs (sem_exp_ck G H b) es vs ->
        Forall2Brs (P_exp H b) es vs ->
        Forall3 (case s) vs (List.map (fun _ => None) tys) os ->
        P_exp H b (Ecase e es None (tys, ck)) os.

    Hypothesis CaseDefaultCase:
      forall H b e s es d lann vs vd os,
        sem_exp_ck G H b e [s] ->
        P_exp H b e [s] ->
        wt_streams [s] (typeof e) ->
        Forall2Brs (sem_exp_ck G H b) es vs ->
        Forall2Brs (P_exp H b) es vs ->
        Forall2 (sem_exp_ck G H b) d vd ->
        Forall2 (P_exp H b) d vd ->
        Forall3 (case s) vs (List.map Some (concat vd)) os ->
        P_exp H b (Ecase e es (Some d) lann) os.

    Hypothesis AppCase:
      forall H b f es er lann ss os sr bs,
        Forall2 (sem_exp_ck G H b) es ss ->
        Forall2 (P_exp H b) es ss ->
        Forall2 (fun e r => sem_exp_ck G H b e [r]) er sr ->
        Forall2 (fun e r => P_exp H b e [r]) er sr ->
        bools_ofs sr bs ->
        (forall k, sem_node_ck G f (List.map (maskv k bs) (concat ss)) (List.map (maskv k bs) os)
              /\ P_node f (List.map (maskv k bs) (concat ss)) (List.map (maskv k bs) os)) ->
        P_exp H b (Eapp f es er lann) os.

    Hypothesis Equation:
      forall H b xs es ss,
        Forall2 (sem_exp_ck G H b) es ss ->
        Forall2 (P_exp H b) es ss ->
        Forall2 (fun x => sem_var H (Var x)) xs (concat ss) ->
        P_equation H b (xs, es).

    Hypothesis BeqCase:
      forall H b eq,
        sem_equation_ck G H b eq ->
        P_equation H b eq ->
        P_block H b (Beq eq).

    Hypothesis BresetCase:
      forall H b blocks er sr r,
        sem_exp_ck G H b er [sr] ->
        P_exp H b er [sr] ->
        bools_of sr r ->
        (forall k, Forall (sem_block_ck G (mask_hist k r H) (maskb k r b)) blocks /\
                Forall (P_block (mask_hist k r H) (maskb k r b)) blocks) ->
        P_block H b (Breset blocks er).

    Hypothesis BswitchCase:
      forall Hi b ec branches sc,
        sem_exp_ck G Hi b ec [sc] ->
        P_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) b sc in
                                  sem_branch_ck (fun blks => Forall (sem_block_ck G Hi' bi) blks
                                                       /\ Forall (P_block Hi' bi) blks
                                    ) (snd blks)) branches ->
        P_block Hi b (Bswitch ec branches).

    Hypothesis TransDefCase:
      forall Hi bs default stres,
        stres ≡ const_stres bs default ->
        P_transitions Hi bs [] default stres.

    Hypothesis TransCase:
      forall Hi bs e C r trans default vs bs' stres1 stres,
        sem_exp_ck G Hi bs e [vs] ->
        P_exp Hi bs e [vs] ->
        bools_of vs bs' ->
        sem_transitions_ck G Hi bs trans default stres1 ->
        P_transitions Hi bs trans default stres1 ->
        stres ≡ choose_first (const_stres bs' (C, r)) stres1 ->
        P_transitions Hi bs ((e, (C, r))::trans) default stres.

    Hypothesis BautoWeakCase:
      forall Hi bs ini oth states ck bs' stres0 stres1 stres,
        sem_clock (var_history Hi) bs ck bs' ->
        sem_transitions_ck G Hi bs' (List.map (fun '(e, t) => (e, (t, false))) ini) (oth, false) stres0 ->
        P_transitions Hi bs' (List.map (fun '(e, t) => (e, (t, false))) ini) (oth, false) stres0 ->
        fby stres0 stres1 stres ->
        Forall (fun '((tag, _), br) =>
                  forall k, exists Hik,
                    select_hist tag k stres Hi Hik
                    /\ let bik := fselectb tag k stres bs in
                      sem_branch_ck
                        (fun '(_, scope) =>
                           sem_scope_ck
                             (fun Hi' bik e vs => sem_exp_ck G Hi' bik e vs /\ P_exp Hi' bik e vs)
                             (fun Hi' blks => Forall (sem_block_ck G Hi' bik) (fst blks)
                                           /\ Forall (P_block Hi' bik) (fst blks)
                                           /\ sem_transitions_ck G Hi' bik (snd blks) (tag, false) (fselect absent tag k stres stres1)
                                           /\ P_transitions Hi' bik (snd blks) (tag, false) (fselect absent tag k stres stres1)
                             ) Hik bik scope)
                        br) states ->
        P_block Hi bs (Bauto Weak ck (ini, oth) states).

    Hypothesis BautoStrongCase:
      forall Hi bs ini states ck bs' stres0 stres1,
        sem_clock (var_history Hi) bs ck bs' ->
        fby (const_stres bs' (ini, false)) stres1 stres0 ->
        Forall (fun '((tag, _), br) =>
                  forall k, exists Hik, select_hist tag k stres0 Hi Hik
                              /\ let bik := fselectb tag k stres0 bs in
                                sem_branch_ck
                                  (fun '(unl, _) =>
                                     sem_transitions_ck G Hik bik unl (tag, false) (fselect absent tag k stres0 stres1)
                                     /\ P_transitions Hik bik unl (tag, false) (fselect absent tag k stres0 stres1)
                                  ) br
          ) states ->
        Forall (fun '((tag, _), br) =>
                  forall k, exists Hik,
                    select_hist tag k stres1 Hi Hik
                    /\ let bik := fselectb tag k stres1 bs in
                      sem_branch_ck
                        (fun '(_, scope) =>
                           sem_scope_ck
                             (fun Hi' bik e vs => sem_exp_ck G Hi' bik e vs /\ P_exp Hi' bik e vs)
                             (fun Hi' blks => Forall (sem_block_ck G Hi' bik) (fst blks)
                                           /\ Forall (P_block Hi' bik) (fst blks)
                             ) Hik bik scope)
                        br) states ->
        P_block Hi bs (Bauto Strong ck ([], ini) states).

    Hypothesis BlocalCase:
      forall Hi bs scope,
        sem_scope_ck (fun Hi' bs e vs => sem_exp_ck G Hi' bs e vs /\ P_exp Hi' bs e vs)
          (fun Hi' blks => Forall (sem_block_ck G Hi' bs) blks /\ Forall (P_block Hi' bs) blks)
          Hi bs scope ->
        P_block Hi bs (Blocal scope).

    Hypothesis Node:
      forall f ss os n H,
        find_node f G = Some n ->
        Forall2 (fun x => sem_var H (Var x)) (List.map fst n.(n_in)) ss ->
        Forall2 (fun x => sem_var H (Var x)) (List.map fst n.(n_out)) os ->
        let bs := clocks_of ss in
        Forall (sem_last_decl (fun Hi' bs e vs => sem_exp_ck G Hi' bs e vs /\ P_exp Hi' bs e vs) (FEnv.empty _) H bs) n.(n_out) ->
        sem_block_ck G H bs n.(n_block) ->
        P_block H bs n.(n_block) ->
        clocked_node H bs (senv_of_ins n.(n_in) ++ senv_of_decls n.(n_out)) ->
        P_node f ss os.

    Local Ltac SolveForall :=
      match goal with
      | H: Forall ?P1 ?l |- Forall ?P2 ?l =>
          induction H; eauto
      | H: Forall2 ?P1 ?l1 ?l2 |- Forall2 ?P2 ?l1 ?l2 =>
          induction H; eauto
      | _ => idtac
      end.

    Fixpoint sem_exp_ck_ind2
      (H: Sem.history) (b: Stream bool) (e: exp) (ss: list (Stream svalue))
      (Sem: sem_exp_ck G H b e ss)
      {struct Sem}
      : P_exp H b e ss
    with sem_equation_ck_ind2
           (H: Sem.history) (b: Stream bool) (e: equation)
           (Sem: sem_equation_ck G H b e)
           {struct Sem}
      : P_equation H b e
    with sem_transitions_ind2
           (H: Sem.history) (b: Stream bool) trans default stres
           (Sem: sem_transitions_ck G H b trans default stres)
           {struct Sem}
      : P_transitions H b trans default stres
    with sem_block_ck_ind2
           (H: Sem.history) (b: Stream bool) (d: block)
           (Sem: sem_block_ck G H b d)
           {struct Sem}
      : P_block H b d
    with sem_node_ck_ind2
           (f: ident) (ss os: list (Stream svalue))
           (Sem: sem_node_ck G f ss os)
           {struct Sem}
      : P_node f ss os.

  End sem_exp_ind2.

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

  Section sem_refines.
    Context {PSyn prefs} (G: @global PSyn prefs).

    Fact sem_exp_refines : forall b e H H' v,
        H ⊑ H' ->
        sem_exp_ck G H b e v ->
        sem_exp_ck G H' b e v.

    Fact sem_equation_refines : forall H H' b equ,
        H ⊑ H' ->
        sem_equation_ck G H b equ ->
        sem_equation_ck G H' b equ.

    Fact sc_vars_refines : forall Γ H H' b,
        H ⊑ H' ->
        (forall x, IsVar Γ x -> FEnv.In (Var x) H' -> FEnv.In (Var x) H) ->
        (forall x, IsLast Γ x -> FEnv.In (Last x) H' -> FEnv.In (Last x) H) ->
        sc_vars Γ H b ->
        sc_vars Γ H' b.

    Fact sem_transitions_refines : forall H H' b trans default stres,
        H ⊑ H' ->
        sem_transitions_ck G H b trans default stres ->
        sem_transitions_ck G H' b trans default stres.

    Lemma sem_scope_refines {A} P_sem : forall locs (blk: A) H H' bs,
        H ⊑ H' ->
        sem_scope_ck (sem_exp_ck G) P_sem H bs (Scope locs blk) ->
        (forall H H',
            H ⊑ H' ->
            P_sem H blk ->
            P_sem H' blk) ->
        sem_scope_ck (sem_exp_ck G) P_sem H' bs (Scope locs blk).

    Lemma sem_block_refines : forall blk H H' bs,
        H ⊑ H' ->
        sem_block_ck G H bs blk ->
        sem_block_ck G H' bs blk.

    Corollary sem_scope_refines1 : forall locs blk H H' bs,
        H ⊑ H' ->
        sem_scope_ck (sem_exp_ck G)
          (fun Hi => Forall (sem_block_ck G Hi bs)) H bs (Scope locs blk) ->
        sem_scope_ck (sem_exp_ck G)
          (fun Hi => Forall (sem_block_ck G Hi bs)) H' bs (Scope locs blk).

    Corollary sem_scope_refines2 : forall locs blk def stres H H' bs,
        H ⊑ H' ->
        sem_scope_ck (sem_exp_ck G)
          (fun Hi blks => Forall (sem_block_ck G Hi bs) (fst blks)
                       /\ sem_transitions_ck G Hi bs (snd blks) def stres) H bs (Scope locs blk) ->
        sem_scope_ck (sem_exp_ck G)
          (fun Hi blks => Forall (sem_block_ck G Hi bs) (fst blks)
                       /\ sem_transitions_ck G Hi bs (snd blks) def stres) H' bs (Scope locs blk).

    Corollary sem_scope_refines3 {T} : forall locs (blk: _ * T) H H' bs,
        H ⊑ H' ->
        sem_scope_ck (sem_exp_ck G)
          (fun Hi blks => Forall (sem_block_ck G Hi bs) (fst blks)) H bs (Scope locs blk) ->
        sem_scope_ck (sem_exp_ck G)
          (fun Hi blks => Forall (sem_block_ck G Hi bs) (fst blks)) H' bs (Scope locs blk).

  End sem_refines.

  Local Hint Constructors Sem.sem_exp Sem.sem_equation Sem.sem_block : lcsem.

  Lemma sc_vars_app : forall Γ1 Γ2 Hi bs,
      (forall x, InMembers x Γ1 -> ~InMembers x Γ2) ->
      sc_vars Γ1 Hi bs ->
      sc_vars Γ2 Hi bs ->
      sc_vars (Γ1 ++ Γ2) Hi bs.

  Lemma sc_vars_incl : forall Γ1 Γ2 Hi bs,
      incl Γ2 Γ1 ->
      sc_vars Γ1 Hi bs ->
      sc_vars Γ2 Hi bs.

  Lemma local_hist_sc_vars : forall (Γ Γ': static_env) locs H H' bs,
      incl (map fst Γ') (map fst Γ) ->
      (forall x, InMembers x locs -> ~IsVar Γ x) ->
      dom_ub H Γ ->
      dom H' (@senv_of_decls exp locs) ->
      sc_vars Γ' H bs ->
      sc_vars (senv_of_decls locs) (H + H') bs ->
      sc_vars (Γ' ++ senv_of_decls locs) (H + H') bs.


  Local Hint Constructors sem_exp : lcsem.

  Add Parametric Morphism : sc_vars
      with signature @Permutation _ ==> history_equiv ==> @EqSt bool ==> Basics.impl
        as sc_vars_morph.

  Add Parametric Morphism : clocked_node
      with signature eq ==> @EqSt _ ==> eq ==> Basics.impl
        as clocked_node_morph.

  Local Hint Resolve clocked_node_morph_Proper : lcsem.

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

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

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

  Fact sem_scope_ck_morph {A} P_blk1 (P_blk2: _ -> _ -> Prop) {PSyn prefs} (G: @global PSyn prefs) :
    forall Hi1 Hi2 bs1 bs2 locs (blks: A),
      sem_scope_ck (sem_exp_ck G) P_blk1 Hi1 bs1 (Scope locs blks) ->
      history_equiv Hi1 Hi2 ->
      bs1 ≡ bs2 ->
      (forall Hi1 Hi2, history_equiv Hi1 Hi2 -> P_blk1 Hi1 blks -> P_blk2 Hi2 blks) ->
      sem_scope_ck (sem_exp_ck G) P_blk2 Hi2 bs2 (Scope locs blks).

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

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

  Section sem_restrict.
    Context {PSyn prefs} (G: @global PSyn prefs).

    Hypothesis HwcG : wc_global G.

    Fact sem_exp_restrict : forall Γ H b e vs,
        wx_exp Γ e ->
        sem_exp_ck G H b e vs ->
        sem_exp_ck G (restrict H Γ) b e vs.

    Lemma sem_equation_restrict : forall Γ H b eq,
        wx_equation Γ eq ->
        sem_equation_ck G H b eq ->
        sem_equation_ck G (restrict H Γ) b eq.

    Fact sc_vars_restrict : forall locs Γ H bs,
        incl (map fst locs) (map fst Γ) ->
        Forall (wc_clock (idck Γ)) (map snd (idck locs)) ->
        sc_vars locs H bs ->
        sc_vars locs (restrict H Γ) bs.

    Fact sem_transitions_restrict : forall Γ H b trans default stres,
        Forall (fun '(e, _) => wx_exp Γ e) trans ->
        sem_transitions_ck G H b trans default stres ->
        sem_transitions_ck G (restrict H Γ) b trans default stres.

    Lemma sem_scope_restrict {A} (P_wc: _ -> _ -> Prop) (sem_block : _ -> _ -> Prop) :
      forall Γ Hi bs locs (blks : A),
        wc_env (idck Γ) ->
        wc_scope P_wc G Γ (Scope locs blks) ->
        sem_scope_ck (sem_exp_ck G) sem_block Hi bs (Scope locs blks) ->
        (forall Γ Hi Hi',
            wc_env (idck Γ) ->
            P_wc Γ blks ->
            sem_block Hi blks ->
            FEnv.Equiv (@EqSt _) Hi' (restrict Hi Γ) ->
            sem_block Hi' blks) ->
        sem_scope_ck (sem_exp_ck G) sem_block (restrict Hi Γ) bs (Scope locs blks).

    Lemma sem_block_restrict : forall blk Γ H b,
        wc_env (idck Γ) ->
        wc_block G Γ blk ->
        sem_block_ck G H b blk ->
        sem_block_ck G (restrict H Γ) b blk.

    Corollary sem_scope_restrict2 : forall locs blk def stres Γ H bs,
        wc_env (idck Γ) ->
        wc_scope (fun Γ blks => Forall (wc_block G Γ) (fst blks)
                             /\ Forall (fun '(e, (_, _)) => wc_exp G Γ e /\ clockof e = [Cbase]) (snd blks))
                 G Γ (Scope locs blk) ->
        sem_scope_ck (sem_exp_ck G)
                     (fun Hi blks => Forall (sem_block_ck G Hi bs) (fst blks)
                                  /\ sem_transitions_ck G Hi bs (snd blks) def stres) H bs (Scope locs blk) ->
        sem_scope_ck (sem_exp_ck G)
                     (fun Hi blks => Forall (sem_block_ck G Hi bs) (fst blks)
                                  /\ sem_transitions_ck G Hi bs (snd blks) def stres)
                     (restrict H Γ) bs (Scope locs blk).

    Corollary sem_scope_restrict3 : forall locs (blk: _ * list transition) Γ H bs,
        wc_env (idck Γ) ->
        wc_scope (fun Γ blks => Forall (wc_block G Γ) (fst blks)
                             /\ Forall (fun '(e, (_, _)) => wc_exp G Γ e /\ clockof e = [Cbase]) (snd blks))
                 G Γ (Scope locs blk) ->
        sem_scope_ck (sem_exp_ck G)
                     (fun Hi blks => Forall (sem_block_ck G Hi bs) (fst blks)) H bs (Scope locs blk) ->
        sem_scope_ck (sem_exp_ck G)
                     (fun Hi blks => Forall (sem_block_ck G Hi bs) (fst blks))
                     (restrict H Γ) bs (Scope locs blk).

  End sem_restrict.

Properties of the global environment

  Ltac sem_cons :=
    match goal with
    | H:sem_scope_ck _ _ _ _ _ |- sem_scope_ck _ _ _ _ _ =>
        inv H; destruct_conjs; econstructor; eauto
    | H:sem_branch_ck _ _ |- _ => inv H; destruct_conjs
    | |- sem_branch_ck _ _ => econstructor; eauto
    | _ => Sem.sem_cons
    end.

  Definition exp_ck_cons1 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) H bs e ss :=
    ~ Is_node_in_exp nd.(n_name) e -> sem_exp_ck (Global typs exts nds) H bs e ss.
  Definition equation_ck_cons1 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) H bs equ :=
    ~ Is_node_in_eq nd.(n_name) equ -> sem_equation_ck (Global typs exts nds) H bs equ.
  Definition transitions_ck_cons1 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) H bs trans default stres :=
    ~ List.Exists (fun '(e, _) => Is_node_in_exp nd.(n_name) e) trans -> sem_transitions_ck (Global typs exts nds) H bs trans default stres.
  Definition block_ck_cons1 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) H bs blk :=
    ~ Is_node_in_block nd.(n_name) blk -> sem_block_ck (Global typs exts nds) H bs blk.
  Definition node_ck_cons1 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) f xs ys :=
    nd.(n_name) <> f -> sem_node_ck (Global typs exts nds) f xs ys.
  Global Hint Unfold exp_ck_cons1 equation_ck_cons1 transitions_ck_cons1 block_ck_cons1 node_ck_cons1 : lsem.

  Lemma sem_exp_ck_cons1 {PSyn prefs} :
    forall typs exts (nd : @node PSyn prefs) nds Hi bs e ss,
      Ordered_nodes (Global typs exts (nd::nds)) ->
      sem_exp_ck (Global typs exts (nd::nds)) Hi bs e ss ->
      exp_ck_cons1 typs exts nd nds Hi bs e ss.

  Lemma sem_block_ck_cons1 {PSyn prefs} :
    forall typs exts (nd : @node PSyn prefs) nds Hi bs blk,
      Ordered_nodes (Global typs exts (nd::nds)) ->
      sem_block_ck (Global typs exts (nd::nds)) Hi bs blk ->
      block_ck_cons1 typs exts nd nds Hi bs blk.

  Lemma sem_node_ck_cons1 {PSyn prefs} :
    forall typs exts (nd : @node PSyn prefs) nds f xs ys,
      Ordered_nodes (Global typs exts (nd::nds)) ->
      sem_node_ck (Global typs exts (nd::nds)) f xs ys ->
      node_ck_cons1 typs exts nd nds f xs ys.

  Corollary sem_node_ck_cons1' {PSyn prefs} : forall typs exts (n nd: @node PSyn prefs) nds Hi bs,
      Ordered_nodes (Global typs exts (nd::nds)) ->
      ~Is_node_in nd.(n_name) n ->
      sem_block_ck (Global typs exts (nd::nds)) Hi bs (n_block n) ->
      Forall (sem_last_decl (sem_exp_ck (Global typs exts (nd::nds))) (FEnv.empty (Stream svalue)) Hi bs) (n_out n) ->
      sem_block_ck (Global typs exts nds) Hi bs (n_block n)
      /\ Forall (sem_last_decl (sem_exp_ck (Global typs exts nds)) (FEnv.empty (Stream svalue)) Hi bs) (n_out n).

  Definition exp_ck_cons2 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) H bs e ss :=
    ~ Is_node_in_exp nd.(n_name) e -> sem_exp_ck (Global typs exts (nd::nds)) H bs e ss.
  Definition equation_ck_cons2 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) H bs equ :=
    ~ Is_node_in_eq nd.(n_name) equ -> sem_equation_ck (Global typs exts (nd::nds)) H bs equ.
  Definition transitions_ck_cons2 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) H bs trans default stres :=
    ~ List.Exists (fun '(e, _) => Is_node_in_exp nd.(n_name) e) trans -> sem_transitions_ck (Global typs exts (nd::nds)) H bs trans default stres.
  Definition block_ck_cons2 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) H bs blk :=
    ~ Is_node_in_block nd.(n_name) blk -> sem_block_ck (Global typs exts (nd::nds)) H bs blk.
  Definition node_ck_cons2 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) f xs ys :=
    nd.(n_name) <> f -> sem_node_ck (Global typs exts (nd::nds)) f xs ys.
  Global Hint Unfold exp_ck_cons2 equation_ck_cons2 transitions_ck_cons2 block_ck_cons2 node_ck_cons2 : lsem.

  Lemma sem_exp_ck_cons2 {PSyn prefs} :
    forall typs exts (nd : @node PSyn prefs) nds Hi bs e ss,
      Ordered_nodes (Global typs exts (nd::nds)) ->
      sem_exp_ck (Global typs exts nds) Hi bs e ss ->
      exp_ck_cons2 typs exts nd nds Hi bs e ss.

  Lemma sem_block_ck_cons2 {PSyn prefs} :
    forall typs exts (nd : @node PSyn prefs) nds Hi bs blk,
      Ordered_nodes (Global typs exts (nd::nds)) ->
      sem_block_ck (Global typs exts nds) Hi bs blk ->
      block_ck_cons2 typs exts nd nds Hi bs blk.

  Lemma sem_node_ck_cons2 {PSyn prefs} :
    forall typs exts (nd : @node PSyn prefs) nds f xs ys,
      Ordered_nodes (Global typs exts (nd::nds)) ->
      sem_node_ck (Global typs exts nds) f xs ys ->
      node_ck_cons2 typs exts nd nds f xs ys.

  Lemma sem_node_ck_cons_iff {PSyn prefs} :
    forall (n : @node PSyn prefs) nds types externs f xs ys,
      Ordered_nodes (Global types externs (n::nds)) ->
      n_name n <> f ->
      sem_node_ck (Global types externs nds) f xs ys <->
      sem_node_ck (Global types externs (n::nds)) f xs ys.


  Lemma sc_when :
    forall H b x ty k ck xs ys rs,
      sem_var H x xs ->
      sem_clock H b ck (abstract_clock ys) ->
      when k ys xs rs ->
      sem_clock H b (Con ck x (ty, k)) (abstract_clock rs).

  Lemma sc_merge :
    forall H b ck x tx xs vs ss,
      vs <> [] ->
      sem_var H x xs ->
      Forall (fun vs => sem_clock H b (Con ck x (tx, (fst vs))) (abstract_clock (snd vs))) vs ->
      merge xs vs ss ->
      sem_clock H b ck (abstract_clock ss).

  Global Hint Constructors Is_free_in_clock : clocks lcsem.

  Lemma sc_parent :
    forall H b ck lck ss,
      Forall2 (sem_clock H b) lck (map abstract_clock ss) ->
      In ck lck ->
      Forall (fun ck' => ck' = ck \/ clock_parent ck ck') lck ->
      sem_clock H b ck (clocks_of ss).

  Lemma wc_env_free_in_clock :
    forall x i ck vars,
      wc_env vars ->
      In (x, ck) vars ->
      Is_free_in_clock i ck ->
      exists ick, In (i, ick) vars.

  Fact sc_has_base {PSyn prefs} : forall H b bck sub (n : @node PSyn prefs) ncks ss,
      wc_env (map (fun '(x, (_, ck, _)) => (x, ck)) (n_in n)) ->
      Forall2 (fun nck => sem_clock H b (stripname nck)) ncks (map abstract_clock ss) ->
      Forall2 (WellInstantiated bck sub) (map (fun '(x, (_, ck, _)) => (x, ck)) (n_in n)) ncks ->
      sem_clock H b bck (clocks_of ss).

  Lemma sc_inst_mask:
    forall H' b b' ck ck' bck sub cks rs,
      instck bck sub ck = Some ck' ->
      sem_clock H' b' bck b ->
      (forall k, exists H, sem_clock H (maskb k rs b) ck (maskb k rs cks) /\
                 (forall x x',
                     Is_free_in_clock x ck ->
                     sub x = Some x' ->
                     orel (fun v1 v2 => EqSt v1 (maskv k rs v2)) (H x) (H' x'))) ->
      sem_clock H' b' ck' cks.

  Lemma sc_inst_unmask:
    forall H H' b b' ck ck' bck sub cks k rs,
      instck bck sub ck = Some ck' ->
      sem_clock H' b' ck' cks ->
      sem_clock H' b' bck b ->
      (forall x x',
          Is_free_in_clock x ck ->
          sub x = Some x' ->
          orel (fun v1 v2 => EqSt v1 (maskv k rs v2)) (H x) (H' x')) ->
      sem_clock H (maskb k rs b) ck (maskb k rs cks).

  Lemma inst_in_eqst_mask:
    forall H Hi xs ys vs i ck bck sub k rs,
      In (i, ck) xs ->
      Forall2 (WellInstantiated bck sub) xs ys ->
      Forall2 (sem_var Hi) (map fst xs) (map (maskv k rs) vs) ->
      Forall2 (fun '(_, o) s => LiftO True (fun x => sem_var H x s) o) ys vs ->
      forall i',
        sub i = Some i' ->
        orel (fun v1 v2 => v1 ≡ maskv k rs v2) (Hi i) (H i').

  Corollary sc_inside_mask {PSyn prefs} :
    forall H Hi b es ss0 bck sub (n : @node PSyn prefs) k rs,
      Forall2 (fun '(_, o) (s : Stream svalue) => LiftO True (fun x1 : ident => sem_var H (Var x1) s) o) (nclocksof es) (concat ss0) ->
      wc_env (map (fun '(x, (_, ck, _)) => (x, ck)) (n_in n)) ->
      Forall2 (sem_clock (var_history H) b) (clocksof es) (map abstract_clock (concat ss0)) ->
      Forall2 (WellInstantiated bck sub) (map (fun '(x, (_, ck, _)) => (x, ck)) (n_in n)) (nclocksof es) ->
      Forall2 (fun x => sem_var Hi (Var x)) (idents (n_in n)) (map (maskv k rs) (concat ss0)) ->
      Forall2 (fun xc => sem_clock (var_history Hi) (clocks_of (map (maskv k rs) (concat ss0))) (snd xc))
              (map (fun '(x, (_, ck, _)) => (x, ck)) (n_in n)) (map abstract_clock (map (maskv k rs) (concat ss0))).

  Definition def_stream b := enum b 0.

  Lemma sc_outside_mask {PSyn1 PSyn2 prefs1 prefs2} :
    forall (G : @global PSyn1 prefs1) H es b Γ ncks ss0 ss bck sub (n : @node PSyn2 prefs2) rs,
      Forall (wc_exp G Γ) es ->
      Forall2 (fun '(_, o1) s => LiftO True (fun x0 : ident => sem_var H (Var x0) s) o1) (nclocksof es) (concat ss0) ->
      Forall2 (fun '(_, o) s => LiftO True (fun x0 => sem_var H (Var x0) s) o) ncks ss ->
      wc_env (map (fun '(x, (_, ck, _)) => (x, ck)) (n_in n)) ->
      wc_env (map (fun '(x, (_, ck, _)) => (x, ck)) (n_in n) ++ map (fun '(x, (_, ck, _, _)) => (x, ck)) (n_out n)) ->
      Forall2 (sem_clock (var_history H) b) (clocksof es) (map abstract_clock (concat ss0)) ->
      Forall2 (WellInstantiated bck sub) (map (fun '(x, (_, ck, _)) => (x, ck)) (n_in n)) (nclocksof es) ->
      Forall2 (WellInstantiated bck sub) (map (fun '(x, (_, ck, _, _)) => (x, ck)) (n_out n)) ncks ->
      (forall k, exists Hi,
            Forall2 (fun xc => sem_clock (var_history Hi) (clocks_of (map (maskv k rs) (concat ss0))) (snd xc))
                    (map (fun '(x, (_, ck, _, _)) => (x, ck)) (n_out n)) (map abstract_clock (map (maskv k rs) ss)) /\
            Forall2 (fun x => sem_var Hi (Var x)) (map fst (n_in n)) (map (maskv k rs) (concat ss0)) /\
            Forall2 (fun x => sem_var Hi (Var x)) (map fst (n_out n)) (map (maskv k rs) ss)) ->
      Forall2 (sem_clock (var_history H) b) (map fst ncks) (map abstract_clock ss).

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

  Lemma sc_vars_subclock Γ Γ' : forall Hi bs bs' ck,
      sem_clock (var_history Hi) bs ck bs' ->
      (forall x ck', HasClock Γ' x ck' -> HasClock Γ x ck /\ ck' = Cbase) ->
      (forall x, IsLast Γ' x -> IsLast Γ x) ->
      sc_vars Γ Hi bs ->
      sc_vars Γ' Hi bs'.

more `mask` properties

  Lemma history_mask_count : forall r H n,
      FEnv.Equiv eq (CIStr.tr_history (mask_hist (count r) # n r H) n) (CIStr.tr_history H n).

  Corollary sem_var_instant_mask_hist_count: forall H n r x v,
      IStr.sem_var_instant (CIStr.tr_history H n) x v <->
        IStr.sem_var_instant (CIStr.tr_history (mask_hist ((count r) # n) r H) n) x v.

  Lemma sem_clock_mask : forall H bs ck bs' k r,
      sem_clock H bs ck bs' ->
      sem_clock (mask_hist k r H) (maskb k r bs) ck (maskb k r bs').

  Lemma sem_clock_unmask : forall H bs ck bs' r,
      (forall k, sem_clock (mask_hist k r H) (maskb k r bs) ck (maskb k r bs')) ->
      sem_clock H bs ck bs'.

  Lemma sc_vars_mask : forall Γ H b r k,
      sc_vars Γ H b ->
      sc_vars Γ (mask_hist k r H) (maskb k r b).

  Lemma sc_vars_unmask : forall Γ H b r,
      (forall k, sc_vars Γ (mask_hist k r H) (maskb k r b)) ->
      sc_vars Γ H b.

  Lemma sem_clock_filter : forall Hi Hi' bs ck k sc,
      sem_clock Hi bs ck (abstract_clock sc) ->
      sem_clock Hi' (fwhenb k bs sc) Cbase (fwhenb k (abstract_clock sc) sc).

  Lemma sc_vars_when : forall Γ Γ' Hi Hi' bs ck e sc,
      sc_vars Γ Hi bs ->
      sem_clock (var_history Hi) bs ck (abstract_clock sc) ->
      (forall x ck', HasClock Γ' x ck' -> HasClock Γ x ck /\ ck' = Cbase) ->
      (forall x, IsLast Γ' x -> IsLast Γ x) ->
      when_hist e Hi sc Hi' ->
      sc_vars Γ' Hi' (fwhenb e bs sc).

  Lemma sem_clock_select : forall Hi Hi' bs ck e k sc,
      sem_clock Hi bs ck (abstract_clock sc) ->
      sem_clock Hi' (fselectb e k sc bs) Cbase (fselectb e k sc (abstract_clock sc)).

  Lemma sc_vars_select : forall Γ Γ' Hi Hi' bs ck e k sc,
      sc_vars Γ Hi bs ->
      sem_clock (var_history Hi) bs ck (abstract_clock sc) ->
      (forall x ck', HasClock Γ' x ck' -> HasClock Γ x ck /\ ck' = Cbase) ->
      (forall x, IsLast Γ' x -> IsLast Γ x) ->
      select_hist e k sc Hi Hi' ->
      sc_vars Γ' Hi' (fselectb e k sc bs).

  Lemma sc_vars_slower_hist : forall Γ H b,
      sc_vars Γ H b ->
      dom_ub H Γ ->
      slower_hist H b.

Alignment of streams produced by expressions

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


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

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

    Lemma sem_exp_sem_var : forall H b e vs,
        wl_exp G e ->
        sem_exp_ck G H b e vs ->
        Forall2 (fun '(_, o) s => LiftO True (fun x : ident => sem_var H (Var x) s) o) (nclockof e) vs.

    Corollary sem_exps_sem_var : forall H b es vs,
        Forall (wl_exp G) es ->
        Forall2 (sem_exp_ck G H b) es vs ->
        Forall2 (fun '(_, o) s => LiftO True (fun x : ident => sem_var H (Var x) s) o) (nclocksof es) (concat vs).

  End props.

  Lemma sc_outside_mask' {PSyn prefs} :
    forall (G: @global PSyn prefs) f n H b Γ ncks es rs ss vs bck sub,
      wc_global G ->
      find_node f G = Some n ->
      Forall (wc_exp G Γ) es ->
      Forall2 (sem_exp_ck G H b) es ss ->
      (forall k, sem_node_ck G f (map (maskv k rs) (concat ss)) (map (maskv k rs) vs)) ->
      Forall2 (fun '(_, o) (s : Stream svalue) => LiftO True (fun x0 : ident => sem_var H (Var x0) s) o) ncks vs ->
      Forall2 (sem_clock (var_history H) b) (clocksof es) (map abstract_clock (concat ss)) ->
      Forall2 (WellInstantiated bck sub) (map (fun '(x, (_, ck, _)) => (x, ck)) (n_in n)) (nclocksof es) ->
      Forall2 (WellInstantiated bck sub) (map (fun '(x, (_, ck, _, _)) => (x, ck)) (n_out n)) ncks ->
      Forall2 (sem_clock (var_history H) b) (map fst ncks) (map abstract_clock vs).

  Fact sc_exps' {PSyn prefs} : forall (G : @global PSyn prefs) H b Γ es ss,
      Forall
         (fun e => forall vs,
              wc_exp G Γ e ->
              sem_exp_ck G H b e vs ->
              Forall2 (sem_clock (var_history H) b) (clockof e) (map abstract_clock vs)) es ->

      Forall (wc_exp G Γ) es ->
      Forall2 (sem_exp_ck G H b) es ss ->
      Forall2 (sem_clock (var_history H) b) (clocksof es) (map abstract_clock (concat ss)).

  Lemma Forall2Brs_sc_exp1 {PSyn prefs} (G: @global PSyn prefs) : forall H b Γ ck x tx es vs,
    Forall (fun es =>
              Forall (fun e => forall vs,
                          wc_exp G Γ e ->
                          sem_exp_ck G H b e vs ->
                          Forall2 (sem_clock (var_history H) b) (clockof e) (map abstract_clock vs)) (snd es)) es ->
    Forall (fun es => Forall (wc_exp G Γ) (snd es)) es ->
    Forall (fun '(i, es) => Forall (eq (Con ck x (tx, i))) (clocksof es)) es ->
    Forall2Brs (sem_exp_ck G H b) es vs ->
    Forall (Forall (fun '(i, v) => sem_clock (var_history H) b (Con ck x (tx, i)) (abstract_clock v))) vs.

  Lemma sc_exp {PSyn prefs} (G: @global PSyn prefs) : forall Γ H b e vs,
      wc_global G ->
      sc_vars Γ H b ->
      wc_exp G Γ e ->
      sem_exp_ck G H b e vs ->
      Forall2 (sem_clock (var_history H) b) (clockof e) (map abstract_clock vs).

  Corollary sc_exps {PSyn prefs} (G: @global PSyn prefs) : forall Γ H b es vss,
      wc_global G ->
      sc_vars Γ H b ->

      Forall (wc_exp G Γ) es ->
      Forall2 (sem_exp_ck G H b) es vss ->
      Forall2 (sem_clock (var_history H) b) (clocksof es) (map abstract_clock (concat vss)).

  Corollary sc_exps2 {PSyn prefs} (G: @global PSyn prefs) : forall Γ H b es vss,
      wc_global G ->
      sc_vars Γ H b ->

      Forall (wc_exp G Γ) es ->
      Forall2 (fun e v => sem_exp_ck G H b e [v]) es vss ->
      Forall2 (sem_clock (var_history H) b) (clocksof es) (map abstract_clock vss).

  Fact const_stres_ac {A} : forall bs (x : A),
      abstract_clock (const_stres bs x) ≡ bs.

  Fact choose_first_ac {A} : forall bs xs ys,
      slower xs bs ->
      abstract_clock ys ≡ bs ->
      @abstract_clock A (choose_first xs ys) ≡ bs.

  Lemma sc_transitions {PSyn prefs} (G: @global PSyn prefs) Γ : forall Hi bs' trans def stres,
      wc_global G ->
      sc_vars Γ Hi bs' ->

      Forall (fun '(e, _) => wc_exp G Γ e /\ clockof e = [Cbase]) trans ->
      sem_transitions_ck G Hi bs' trans def stres ->
      abstract_clock stres ≡ bs'.

  Fact wc_global_Ordered_nodes {PSyn prefs} : forall (G: @global PSyn prefs),
      wc_global G ->
      Ordered_nodes G.

Another version of semantic inclusion

  Section sem_ref.
    Context {PSyn1 PSyn2 : list decl -> block -> Prop}.
    Context {pref1 pref2 : PS.t}.

    Definition node_sem_refines (G : @global PSyn1 pref1) (G' : @global PSyn2 pref2) f : Prop :=
      forall ins outs, sem_node_ck G f ins outs -> sem_node_ck G' f ins outs.

    Definition global_sem_refines (G : @global PSyn1 pref1) (G' : @global PSyn2 pref2) : Prop :=
      forall f, node_sem_refines G G' f.

    Hint Constructors sem_exp_ck : core.

    Fact sem_ref_sem_exp : forall G G' H b e vs,
        global_sem_refines G G' ->
        sem_exp_ck G H b e vs ->
        sem_exp_ck G' H b e vs.

    Fact sem_ref_sem_equation : forall G G' H b eq,
        global_sem_refines G G' ->
        sem_equation_ck G H b eq ->
        sem_equation_ck G' H b eq.

    Fact sem_ref_sem_transitions : forall G G' H b trans def stres,
        global_sem_refines G G' ->
        sem_transitions_ck G H b trans def stres ->
        sem_transitions_ck G' H b trans def stres.

    Fact sem_ref_sem_block : forall G G' blk H b,
        global_sem_refines G G' ->
        sem_block_ck G H b blk ->
        sem_block_ck G' H b blk.

    Fact global_sem_ref_nil : forall enms1 enms2 exts1 exts2,
      global_sem_refines (Global enms1 exts1 []) (Global enms2 exts2 []).

    Fact global_sem_ref_cons : forall enms1 enms2 exts1 exts2 nds nds' n n' f,
        Ordered_nodes (Global enms1 exts1 (n::nds)) ->
        Ordered_nodes (Global enms2 exts2 (n'::nds')) ->
        n_name n = f ->
        n_name n' = f ->
        global_sem_refines (Global enms1 exts1 nds) (Global enms2 exts2 nds') ->
        node_sem_refines (Global enms1 exts1 (n::nds)) (Global enms2 exts2 (n'::nds')) f ->
        global_sem_refines (Global enms1 exts1 (n::nds)) (Global enms2 exts2 (n'::nds')).

  End sem_ref.

Execution of a node with absent inputs

  Lemma sem_var_instant_absent: forall H x v,
      IStr.sem_var_instant H x v ->
      IStr.sem_var_instant (FEnv.map (fun _ => absent) H) x absent.
  Global Hint Resolve sem_var_instant_absent : lcsem.

  Lemma sem_clock_false: forall H ck b b',
      IStr.sem_clock b H ck b' ->
      IStr.sem_clock (fun _ => false) (fun n => FEnv.map (fun _ => absent) (H n)) ck (fun _ => false).

  Section sem_node_absent.
    Context {PSyn : list decl -> block -> Prop}.
    Context {prefs : PS.t}.

    Import List.

    Lemma Forall2_sem_exp_absent: forall (f : list (Stream svalue) -> list (Stream svalue)) (G : @global PSyn prefs) H b es ss,
        Forall2 (fun e vs => sem_exp_ck G H b e (f vs)) es ss ->
        Forall2 (sem_exp_ck G H b) es (map f ss).
    Hint Resolve Forall2_sem_exp_absent : lcsem.

    Lemma sem_var_absent {K}: forall (H: @FEnv.t K _) x v,
        sem_var H x v ->
        sem_var (FEnv.map (fun _ => Streams.const absent) H) x (Streams.const absent).
    Hint Resolve sem_var_absent : lcsem.

    Lemma sem_var_absent_inv {K} : forall (H: @FEnv.t K _) x v,
        sem_var (FEnv.map (fun _ => Streams.const absent) H) x v ->
        exists v', sem_var H x v' /\ v ≡ Streams.const absent.

    Lemma sem_clock_absent: forall H bs ck bs',
        sem_clock H bs ck bs' ->
        sem_clock (FEnv.map (fun _ => Streams.const absent) H) (Streams.const false) ck (Streams.const false).

    Lemma clocks_of_false: forall ss,
      clocks_of (map (fun _ : Stream svalue => Streams.const absent) ss) ≡ Streams.const false.

    Lemma fby_absent {A}:
      @fby A (Streams.const absent) (Streams.const absent) (Streams.const absent).

    Lemma arrow_absent:
      arrow (Streams.const absent) (Streams.const absent) (Streams.const absent).

    Fact clocked_node_absent: forall H bs vars,
        clocked_node H bs vars ->
        clocked_node (FEnv.map (fun _ => Streams.const absent) H) (Streams.const false) vars.

    Fact sem_scope_absent {A} P_exp1 P_blk1 (P_exp2: _ -> _ -> _ -> _ -> Prop) (P_blk2: _ -> _ -> Prop) :
      forall locs (blks: A) Hi bs,
        sem_scope_ck P_exp1 P_blk1 Hi bs (Scope locs blks) ->
        (forall Hi1 Hi2 e vs,
            P_exp1 Hi1 bs e vs ->
            FEnv.Equiv (@EqSt _) Hi2 (FEnv.map (fun _ => Streams.const absent) Hi1) ->
            P_exp2 Hi2 (Streams.const false) e (map (fun _ => Streams.const absent) vs)) ->
        (forall Hi1 Hi2,
            P_blk1 Hi1 blks ->
            FEnv.Equiv (@EqSt _) Hi2 (FEnv.map (fun _ => Streams.const absent) Hi1) ->
            P_blk2 Hi2 blks) ->
        sem_scope_ck P_exp2 P_blk2
                     (FEnv.map (fun _ => Streams.const absent) Hi) (Streams.const false) (Scope locs blks).

    Lemma sem_block_absent:
      forall (G : @global PSyn prefs) H bs bck,
        sem_block_ck G H bs bck ->
        sem_block_ck G (FEnv.map (fun _ => Streams.const absent) H) (Streams.const false) bck.

  End sem_node_absent.


  Lemma sem_clock_when_const : forall H bs bs' bs'' cs ck id x tx c,
      sem_clock H bs ck bs' ->
      sem_clock H bs (Con ck id (tx, x)) bs'' ->
      sem_var H id cs ->
      when x (const bs' c) cs (const bs'' c).

  Lemma sem_clock_when_enum : forall H bs bs' bs'' cs ck id x tx c,
      sem_clock H bs ck bs' ->
      sem_clock H bs (Con ck id (tx, x)) bs'' ->
      sem_var H id cs ->
      when x (enum bs' c) cs (enum bs'' c).

End LCLOCKEDSEMANTICS.

Module LClockedSemanticsFun
       (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)
       (Clo : LCLOCKING Ids Op OpAux Cks Senv Syn)
       (Lord : LORDERED Ids Op OpAux Cks Senv Syn)
       (CStr : COINDSTREAMS Ids Op OpAux Cks)
       (Sem : LSEMANTICS Ids Op OpAux Cks Senv Syn Lord CStr)
<: LCLOCKEDSEMANTICS Ids Op OpAux Cks Senv Syn Clo Lord CStr Sem.
  Include LCLOCKEDSEMANTICS Ids Op OpAux Cks Senv Syn Clo Lord CStr Sem.
End LClockedSemanticsFun.