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

Require Import Omega.

From Velus Require Import Common.
From Velus Require Import Operators Environment.
From Velus Require Import Clocks.
From Velus Require Import CoindStreams IndexedStreams.
From Velus Require Import CoindIndexed.
From Velus Require Import Lustre.LSyntax Lustre.LOrdered Lustre.LTyping Lustre.LClocking Lustre.LCausality Lustre.LSemantics Lustre.LClockSemantics.
From Velus Require Import Lustre.Normalization.Fresh Lustre.Normalization.Normalization.
From Velus Require Import Lustre.Normalization.NTyping Lustre.Normalization.NClocking.
From Velus Require Import Lustre.Normalization.NCausality.

Correctness of the Normalization

Module Type CORRECTNESS
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Op)
       (Import CStr : COINDSTREAMS Op OpAux)
       (IStr : INDEXEDSTREAMS Op OpAux)
       (Import Syn : LSYNTAX Ids Op)
       (LCA : LCAUSALITY Ids Op Syn)
       (Import Ty : LTYPING Ids Op Syn)
       (Import Cl : LCLOCKING Ids Op Syn)
       (Import Ord : LORDERED Ids Op Syn)
       (Import Sem : LSEMANTICS Ids Op OpAux Syn Ord CStr)
       (LCS : LCLOCKSEMANTICS Ids Op OpAux Syn Cl LCA Ord CStr IStr Sem)
       (Import Norm : NORMALIZATION Ids Op OpAux Syn LCA).

  Import Fresh Tactics Unnesting.
  Module Import Typing := NTypingFun Ids Op OpAux Syn LCA Ty Norm.
  Module Import Clocking := NClockingFun Ids Op OpAux Syn LCA Cl Norm.
  Module Import Causality := NCausalityFun Ids Op OpAux Syn LCA Cl Norm.
  Import List.

  CoFixpoint default_stream : Stream OpAux.value :=
    absent ⋅ default_stream.

  Fact unnest_exp_sem_length : forall G vars e is_control es' eqs' st st',
      wt_exp G (vars++Typing.st_tys st) e ->
      unnest_exp G is_control e st = (es', eqs', st') ->
      Forall (fun e => forall v H b,
                  sem_exp G H b e v ->
                  length v = 1) es'.


  Import Permutation.

  Fact fresh_ident_refines {B V} : forall vars H H' a id (v : V) (st st' : fresh_st B) reu,
      st_valid_reuse st (PSP.of_list vars) reu ->
      Env.dom H (vars++st_ids st) ->
      fresh_ident norm1 a st = (id, st') ->
      H' = Env.add id v H ->
      Env.refines eq H H'.

  Fact idents_for_anns_NoDupMembers : forall anns ids st st' aft reu,
      st_valid_reuse st aft reu ->
      idents_for_anns anns st = (ids, st') ->
      NoDupMembers ids.

  Fact idents_for_anns_nIn : forall anns ids st st' aft reu,
      st_valid_reuse st aft reu ->
      idents_for_anns anns st = (ids, st') ->
      Forall (fun id => ~In id (st_ids st)) (map fst ids).

  Fact idents_for_anns_dom {V} : forall vars H H' anns ids (vs : list V) st st' reu,
      length vs = length ids ->
      st_valid_reuse st (PSP.of_list vars) reu ->
      Env.dom H (vars++st_ids st) ->
      idents_for_anns anns st = (ids, st') ->
      H' = Env.adds (map fst ids) vs H ->
      Env.dom H' (vars++st_ids st').

  Fact idents_for_anns_refines {V} : forall vars H H' anns ids (vs : list V) st st' reu,
      length vs = length ids ->
      st_valid_reuse st (PSP.of_list vars) reu ->
      Env.dom H (vars++st_ids st) ->
      idents_for_anns anns st = (ids, st') ->
      H' = Env.adds (map fst ids) vs H ->
      Env.refines eq H H'.

  Fact idents_for_anns'_NoDupMembers : forall anns ids st st' aft reusable,
      NoDup (map fst (Syn.anon_streams anns) ++ PS.elements reusable) ->
      st_valid_reuse st aft (ps_adds (map fst (Syn.anon_streams anns)) reusable) ->
      idents_for_anns' anns st = (ids, st') ->
      NoDupMembers ids.

  Fact idents_for_anns'_nIn : forall anns ids st st' aft reusable,
      NoDup (map fst (Syn.anon_streams anns) ++ PS.elements reusable) ->
      st_valid_reuse st aft (ps_adds (map fst (Syn.anon_streams anns)) reusable) ->
      idents_for_anns' anns st = (ids, st') ->
      Forall (fun id => ~In id (st_ids st)) (map fst ids).

  Fact idents_for_anns'_nIn' : forall anns ids st st' aft reusable,
      NoDup (map fst (Syn.anon_streams anns) ++ PS.elements reusable) ->
      st_valid_reuse st aft (ps_adds (map fst (Syn.anon_streams anns)) reusable) ->
      idents_for_anns' anns st = (ids, st') ->
      Forall (fun id => ~In id (PSP.to_list aft++st_ids st)) (map fst ids).

  Fact idents_for_anns'_dom {V} : forall vars H H' anns ids (vs : list V) st st' reu,
      length vs = length ids ->
      st_valid_reuse st (PSP.of_list vars) reu ->
      Env.dom H (vars++st_ids st) ->
      idents_for_anns' anns st = (ids, st') ->
      H' = Env.adds (map fst ids) vs H ->
      Env.dom H' (vars++st_ids st').

  Fact reuse_ident_refines {B V} : forall vars H H' a id (v : V) (st st' : fresh_st B) reusable,
      ~PS.In id reusable ->
      st_valid_reuse st (PSP.of_list vars) (PS.add id reusable) ->
      Env.dom H (vars++st_ids st) ->
      reuse_ident id a st = (tt, st') ->
      H' = Env.add id v H ->
      Env.refines eq H H'.

  Fact idents_for_anns'_refines {V} : forall vars H H' anns ids (vs : list V) st st' reusable,
      length vs = length ids ->
      NoDup (map fst (Syn.anon_streams anns) ++ PS.elements reusable) ->
      st_valid_reuse st (PSP.of_list vars) (ps_adds (map fst (Syn.anon_streams anns)) reusable) ->
      Env.dom H (vars++st_ids st) ->
      idents_for_anns' anns st = (ids, st') ->
      H' = Env.adds (map fst ids) vs H ->
      Env.refines eq H H'.

  Fact fresh_ident_dom {B V} : forall pref vars H H' a id (v : V) (st st' : fresh_st B),
      Env.dom H (vars++st_ids st) ->
      fresh_ident pref a st = (id, st') ->
      H' = Env.add id v H ->
      Env.dom H' (vars++st_ids st').

  Fact reuse_ident_dom {B V} : forall vars H H' a id (v : V) (st st' : fresh_st B),
      Env.dom H (vars++st_ids st) ->
      reuse_ident id a st = (tt, st') ->
      H' = Env.add id v H ->
      Env.dom H' (vars++st_ids st').

Conservation of sem_exp

  Fact unnest_reset_sem : forall G vars b e H v e' eqs' st st' reusable,
      LiftO True (fun e => forall e' eqs' st',
                   unnest_exp G true e st = ([e'], eqs', st') ->
                   exists H',
                     Env.refines eq H H' /\
                     st_valid_reuse st' (PSP.of_list vars) reusable /\
                     Env.dom H' (vars++st_ids st') /\
                     sem_exp G H' b e' [v] /\ Forall (sem_equation G H' b) eqs') e ->
      LiftO True (wl_exp G) e ->
      LiftO True (fun e => numstreams e = 1) e ->
      LiftO True (fun e => sem_exp G H b e [v]) e ->
      st_valid_reuse st (PSP.of_list vars) (ps_adds (match e with None => [] | Some e => map fst (fresh_in e) end) reusable) ->
      Env.dom H (vars++st_ids st) ->
      unnest_reset (unnest_exp G true) e st = (e', eqs', st') ->
      (exists H',
          Env.refines eq H H' /\
          st_valid_reuse st' (PSP.of_list vars) reusable /\
          Env.dom H' (vars++st_ids st') /\
          LiftO True (fun e' => sem_exp G H' b e' [v]) e' /\
          Forall (sem_equation G H' b) eqs').

  Ltac solve_incl :=
    repeat unfold idty; repeat unfold idck;
    match goal with
    | H : wt_nclock ?l1 ?ck |- wt_nclock ?l2 ?ck =>
      eapply wt_nclock_incl; [| eauto]
    | H : wc_clock ?l1 ?ck |- wc_clock ?l2 ?ck =>
      eapply wc_clock_incl; [| eauto]
    | H : wt_exp ?G ?l1 ?e |- wt_exp ?G ?l2 ?e =>
      eapply wt_exp_incl; [| eauto]
    | H : wc_exp ?G ?l1 ?e |- wc_exp ?G ?l2 ?e =>
      eapply wc_exp_incl; [| eauto]
    | H : wt_equation ?G ?l1 ?eq |- wt_equation ?G ?l2 ?eq =>
      eapply wt_equation_incl; [| eauto]
    | H : wc_equation ?G ?l1 ?eq |- wc_equation ?G ?l2 ?eq =>
      eapply wc_equation_incl; [| eauto]
    | |- incl ?l1 ?l1 => reflexivity
    | |- incl (map ?f ?l1) (map ?f ?l2) => eapply incl_map
    | |- incl ?l1 (?l1 ++ ?l2) =>
      eapply incl_appl; reflexivity
    | |- incl (?l1 ++ ?l2) (?l1 ++ ?l3) =>
      eapply incl_app
    | |- incl ?l1 (?l2 ++ ?l3) =>
      eapply incl_appr
    | |- incl ?l1 (?a::?l2) =>
      eapply incl_tl
    | |- incl (st_anns ?st1) (st_anns _) =>
      eapply st_follows_incl; repeat solve_st_follows
    | |- incl (st_tys ?st1) (st_tys _) =>
      eapply st_follows_tys_incl; repeat solve_st_follows
    | |- incl (st_clocks ?st1) (st_clocks _) =>
      eapply st_follows_clocks_incl; repeat solve_st_follows
    end; auto.

  Fact In_fresh_in_NoDup : forall e es vars,
      In e es ->
      NoDup (map fst (fresh_ins es) ++ vars) ->
      NoDup (map fst (fresh_in e) ++ vars).
  Hint Resolve In_fresh_in_NoDup.

  Fact unnest_arrow_sem : forall G H bs e0s es anns s0s ss os,
      length e0s = length anns ->
      length es = length anns ->
      Forall2 (fun e s => sem_exp G H bs e [s]) e0s s0s ->
      Forall2 (fun e s => sem_exp G H bs e [s]) es ss ->
      Forall3 arrow s0s ss os ->
      Forall2 (fun e s => sem_exp G H bs e [s]) (unnest_arrow e0s es anns) os.

  Fact unnest_fby_sem : forall G H bs e0s es anns s0s ss os,
      length e0s = length anns ->
      length es = length anns ->
      Forall2 (fun e s => sem_exp G H bs e [s]) e0s s0s ->
      Forall2 (fun e s => sem_exp G H bs e [s]) es ss ->
      Forall3 fby s0s ss os ->
      Forall2 (fun e s => sem_exp G H bs e [s]) (unnest_fby e0s es anns) os.

  Fact unnest_when_sem : forall G H bs es tys ckid b ck s ss os,
      length es = length tys ->
      Forall2 (fun e s => sem_exp G H bs e [s]) es ss ->
      sem_var H ckid s ->
      Forall2 (fun s' => when b s' s) ss os ->
      Forall2 (fun e s => sem_exp G H bs e [s]) (unnest_when ckid b es tys ck) os.

  Fact unnest_merge_sem : forall G H bs ets efs tys ckid ck s ts fs os,
      length ets = length tys ->
      length efs = length tys ->
      Forall2 (fun e s => sem_exp G H bs e [s]) ets ts ->
      Forall2 (fun e s => sem_exp G H bs e [s]) efs fs ->
      sem_var H ckid s ->
      Forall3 (merge s) ts fs os ->
      Forall2 (fun e s => sem_exp G H bs e [s]) (unnest_merge ckid ets efs tys ck) os.

  Fact unnest_ite_sem : forall G H bs e ets efs tys ck s ts fs os,
      length ets = length tys ->
      length efs = length tys ->
      sem_exp G H bs e [s] ->
      Forall2 (fun e s => sem_exp G H bs e [s]) ets ts ->
      Forall2 (fun e s => sem_exp G H bs e [s]) efs fs ->
      Forall3 (ite s) ts fs os ->
      Forall2 (fun e s => sem_exp G H bs e [s]) (unnest_ite e ets efs tys ck) os.

  Fact sem_var_adds : forall H xs vs,
      length xs = length vs ->
      NoDup xs ->
      Forall2 (sem_var (Env.adds xs vs H)) xs vs.

  Fact map_bind2_sem : forall G vars b is_control es H vs es' eqs' st st' reusable,
      NoDup (map fst (fresh_ins es)++PS.elements reusable) ->
      Forall (wl_exp G) es ->
      Forall2 (sem_exp G H b) es vs ->
      st_valid_reuse st (PSP.of_list vars) (ps_adds (map fst (fresh_ins es)) reusable) ->
      Env.dom H (vars++st_ids st) ->
      Forall2 (fun e v => forall H es' eqs' st st' reusable,
                   NoDup (map fst (fresh_in e)++PS.elements reusable) ->
                   wl_exp G e ->
                   sem_exp G H b e v ->
                   st_valid_reuse st (PSP.of_list vars) (ps_adds (map fst (fresh_in e)) reusable) ->
                   Env.dom H (vars++st_ids st) ->
                   unnest_exp G is_control e st = (es', eqs', st') ->
                   (exists H',
                       Env.refines eq H H' /\
                       st_valid_reuse st' (PSP.of_list vars) reusable /\
                       Env.dom H' (vars++st_ids st') /\
                       Forall2 (fun e v => sem_exp G H' b e [v]) es' v /\
                       Forall (sem_equation G H' b) eqs')) es vs ->
      map_bind2 (unnest_exp G is_control) es st = (es', eqs', st') ->
      (exists H',
          Env.refines eq H H' /\
          st_valid_reuse st' (PSP.of_list vars) reusable /\
          Env.dom H' (vars++st_ids st') /\
          Forall2 (fun es vs => Forall2 (fun e v => sem_exp G H' b e [v]) es vs) es' vs /\
          Forall (sem_equation G H' b) (concat eqs')).

  Lemma unnest_noops_exp_sem : forall G vars b ck e H v e' eqs' st st' reusable,
      st_valid_reuse st (PSP.of_list vars) reusable ->
      Env.dom H (vars++st_ids st) ->
      sem_exp G H b e [v] ->
      unnest_noops_exp ck e st = (e', eqs', st') ->
      (exists H',
          Env.refines eq H H' /\
          st_valid_reuse st' (PSP.of_list vars) reusable /\
          Env.dom H' (vars++st_ids st') /\
          sem_exp G H' b e' [v] /\
          Forall (sem_equation G H' b) eqs').

  Lemma unnest_noops_exps_sem : forall G vars b cks es H vs es' eqs' st st' reusable,
      length es = length cks ->
      st_valid_reuse st (PSP.of_list vars) reusable ->
      Env.dom H (vars++st_ids st) ->
      Forall2 (fun e v => sem_exp G H b e [v]) es vs ->
      unnest_noops_exps cks es st = (es', eqs', st') ->
      (exists H',
          Env.refines eq H H' /\
          st_valid_reuse st' (PSP.of_list vars) reusable /\
          Env.dom H' (vars++st_ids st') /\
          Forall2 (fun e v => sem_exp G H' b e [v]) es' vs /\
          Forall (sem_equation G H' b) eqs').

  Hint Constructors sem_exp.
  Fact unnest_exp_sem : forall G vars b e H vs is_control es' eqs' st st' reusable,
      NoDup (map fst (fresh_in e) ++ PS.elements reusable) ->
      wl_exp G e ->
      sem_exp G H b e vs ->
      st_valid_reuse st (PSP.of_list vars) (ps_adds (map fst (fresh_in e)) reusable) ->
      Env.dom H (vars++st_ids st) ->
      unnest_exp G is_control e st = (es', eqs', st') ->
      (exists H',
          Env.refines eq H H' /\
          st_valid_reuse st' (PSP.of_list vars) reusable /\
          Env.dom H' (vars++st_ids st') /\
          Forall2 (fun e v => sem_exp G H' b e [v]) es' vs /\
          Forall (sem_equation G H' b) eqs').

  Corollary unnest_exps_sem : forall G vars b es H vs es' eqs' st st' reusable,
      NoDup (map fst (fresh_ins es) ++ PS.elements reusable) ->
      Forall (wl_exp G) es ->
      Forall2 (sem_exp G H b) es vs ->
      st_valid_reuse st (PSP.of_list vars) (ps_adds (map fst (fresh_ins es)) reusable) ->
      Env.dom H (vars++st_ids st) ->
      map_bind2 (unnest_exp G false) es st = (es', eqs', st') ->
      (exists H',
          Env.refines eq H H' /\
          st_valid_reuse st' (PSP.of_list vars) reusable /\
          Env.dom H' (vars++st_ids st') /\
          Forall2
            (fun (es : list exp) (vs : list (Stream OpAux.value)) =>
             Forall2 (fun e v => sem_exp G H' b e [v]) es vs) es' vs /\
          Forall (sem_equation G H' b) (concat eqs')).

  Fact unnest_rhs_sem : forall G vars b e H vs es' eqs' st st' reusable,
      NoDup (map fst (anon_in e) ++ PS.elements reusable) ->
      wl_exp G e ->
      sem_exp G H b e vs ->
      st_valid_reuse st (PSP.of_list vars) (ps_adds (map fst (anon_in e)) reusable) ->
      Env.dom H (vars++st_ids st) ->
      unnest_rhs G e st = (es', eqs', st') ->
      (exists H',
          Env.refines eq H H' /\
          st_valid_reuse st' (PSP.of_list vars) reusable /\
          Env.dom H' (vars++st_ids st') /\
          (Forall2 (fun e v => sem_exp G H' b e [v]) es' vs \/
           exists e', (es' = [e'] /\ sem_exp G H' b e' vs)) /\
          Forall (sem_equation G H' b) eqs').

  Corollary map_bind2_unnest_rhs_sem : forall G vars b es H vs es' eqs' st st' reusable,
      NoDup (map fst (anon_ins es) ++ PS.elements reusable) ->
      Forall (wl_exp G) es ->
      Forall2 (sem_exp G H b) es vs ->
      st_valid_reuse st (PSP.of_list vars) (ps_adds (map fst (anon_ins es)) reusable) ->
      Env.dom H (vars++st_ids st) ->
      map_bind2 (unnest_rhs G) es st = (es', eqs', st') ->
      (exists H',
          Env.refines eq H H' /\
          st_valid_reuse st' (PSP.of_list vars) reusable /\
          Env.dom H' (vars++st_ids st') /\
          Forall2 (fun es' vs =>
                     Forall2 (fun e v => sem_exp G H' b e [v]) es' vs \/
                     exists e', (es' = [e'] /\ sem_exp G H' b e' vs)) es' vs /\
          Forall (sem_equation G H' b) (concat eqs')).

  Corollary unnest_rhss_sem : forall G vars b es H vs es' eqs' st st' reusable,
      NoDup (map fst (anon_ins es) ++ PS.elements reusable) ->
      Forall (wt_exp G (vars++st_tys st)) es ->
      Forall2 (sem_exp G H b) es vs ->
      st_valid_reuse st (PSP.of_list (map fst vars)) (ps_adds (map fst (anon_ins es)) reusable) ->
      Env.dom H (map fst vars++st_ids st) ->
      unnest_rhss G es st = (es', eqs', st') ->
      (exists H',
          Env.refines eq H H' /\
          st_valid_reuse st' (PSP.of_list (map fst vars)) reusable /\
          Env.dom H' (map fst vars++st_ids st') /\
          Forall (fun '(e, v) => sem_exp G H' b e v)
                 (combine_for_numstreams es' (concat vs)) /\
          Forall (sem_equation G H' b) eqs').

  Fact combine_for_numstreams_length {V} : forall es (vs : list V),
      length (combine_for_numstreams es vs) = length es.

  Fact combine_for_numstreams_fst_split {V} : forall es (vs : list V),
      fst (split (combine_for_numstreams es vs)) = es.

  Fact combine_for_numstreams_numstreams {V} : forall es (vs : list V),
      length vs = length (annots es) ->
      Forall (fun '(e, v) => numstreams e = length v) (combine_for_numstreams es vs).

  Fact combine_for_numstreams_nth_2 {V1 V2} : forall es (v1s : list V1) (v2s : list V2) n n0 e v1 v2 d1 d2 de1 de2,
      length v1s = length (annots es) ->
      length v2s = length (annots es) ->
      n < length es ->
      n0 < length v1 ->
      nth n (combine_for_numstreams es v1s) de1 = (e, v1) ->
      nth n (combine_for_numstreams es v2s) de2 = (e, v2) ->
      exists n',
        (n' < length v1s /\
         nth n' v1s d1 = nth n0 v1 d1 /\
         nth n' v2s d2 = nth n0 v2 d2).

  Fact unnest_equation_sem : forall G vars H b equ eqs' st st' reusable,
      NoDup (map fst (anon_in_eq equ) ++ PS.elements reusable) ->
      wt_equation G (vars++st_tys st) equ ->
      sem_equation G H b equ ->
      st_valid_reuse st (PSP.of_list (map fst vars)) (ps_adds (map fst (anon_in_eq equ)) reusable) ->
      Env.dom H (map fst vars++st_ids st) ->
      unnest_equation G equ st = (eqs', st') ->
      (exists H', Env.refines eq H H' /\
             st_valid_reuse st' (PSP.of_list (map fst vars)) reusable /\
             Env.dom H' (map fst vars++st_ids st') /\
             Forall (sem_equation G H' b) eqs').

  Corollary unnest_equations_sem : forall G vars b eqs H eqs' st st' reusable,
      NoDup (map fst (anon_in_eqs eqs) ++ PS.elements reusable) ->
      Forall (wt_equation G (vars ++ st_tys st)) eqs ->
      Forall (sem_equation G H b) eqs ->
      st_valid_reuse st (PSP.of_list (map fst vars)) (ps_adds (map fst (anon_in_eqs eqs)) reusable) ->
      Env.dom H (map fst vars++st_ids st) ->
      unnest_equations G eqs st = (eqs', st') ->
      (exists H', Env.refines eq H H' /\
             Forall (sem_equation G H' b) eqs').

Preservation of sem_node

  Fact unnest_node_sem_equation : forall G H n Hwl Hpref ins,
      wt_node G n ->
      Env.dom H (idents (n_in n ++ n_vars n ++ n_out n)) ->
      Forall2 (sem_var H) (idents (n_in n)) ins ->
      Forall (sem_equation G H (clocks_of ins)) (n_eqs n) ->
      exists H', Env.refines eq H H' /\
            Forall (sem_equation G H' (clocks_of ins)) (n_eqs (unnest_node G n Hwl Hpref)).

  Lemma unnest_node_eq : forall G G' f n Hwl Hpref ins outs,
      Forall2 (fun n n' => n_name n = n_name n') G G' ->
      global_iface_eq G G' ->
      global_sem_refines G G' ->
      wt_global (n::G) ->
      wc_global (n::G) ->
      Ordered_nodes (n::G) ->
      Ordered_nodes ((unnest_node G n Hwl Hpref)::G') ->
      sem_node (n::G) f ins outs ->
      sem_node ((unnest_node G n Hwl Hpref)::G') f ins outs.

  Fact unnest_global_names' : forall G Hwl Hpref,
      Forall2 (fun n n' => n_name n = n_name n') G (unnest_global G Hwl Hpref).

  Fact wt_global_Ordered_nodes : forall G,
      wt_global G ->
      Ordered_nodes G.
  Hint Resolve wt_global_Ordered_nodes.

  Lemma unnest_global_refines : forall G Hwl Hpref,
      wt_global G ->
      wc_global G ->
      global_sem_refines G (unnest_global G Hwl Hpref).

  Corollary unnest_global_sem : forall G Hwl Hprefs f ins outs,
      wt_global G ->
      wc_global G ->
      sem_node G f ins outs ->
      sem_node (unnest_global G Hwl Hprefs) f ins outs.

  Corollary unnest_global_sem_clock_inputs : forall G Hwl Hprefs f ins,
      LCS.sem_clock_inputs G f ins ->
      LCS.sem_clock_inputs (unnest_global G Hwl Hprefs) f ins.

Preservation of the semantics through the second pass

Manipulation of initialization streams

  CoFixpoint const_val (b : Stream bool) (v : Op.val) : Stream value :=
    (if Streams.hd b then present v else absent) ⋅ (const_val (Streams.tl b) v).

  Fact const_val_Cons : forall b bs v,
      const_val (b ⋅ bs) v =
      (if b then present v else absent) ⋅ (const_val bs v).

  Fact const_val_const : forall b c,
      const b c ≡ const_val b (Op.sem_const c).

  Lemma sfby_const : forall bs v,
      sfby v (const_val bs v) ≡ (const_val bs v).

  Lemma ite_false : forall bs xs ys,
      aligned xs bs ->
      aligned ys bs ->
      ite (const_val bs false_val) xs ys ys.

  Lemma sfby_fby1 : forall bs v y ys,
      aligned ys bs ->
      fby1 y (const_val bs v) ys (sfby y ys).

  Lemma sfby_fby1' : forall y y0s ys zs,
      fby1 y y0s ys zs ->
      zs ≡ (sfby y ys).

  Lemma sfby_fby : forall b v y,
      aligned y b ->
      fby (const_val b v) y (sfby v y).

  Definition init_stream bs :=
    sfby true_val (const bs false_const).

  Instance init_stream_Proper:
    Proper (@EqSt bool ==> @EqSt value) init_stream.

  Lemma fby_ite : forall bs v y0s ys zs,
      (aligned y0s bs \/ aligned ys bs \/ aligned zs bs) ->
      fby y0s ys zs ->
      ite (sfby true_val (const_val bs false_val)) y0s (sfby v ys) zs.

  Corollary fby_init_stream_ite : forall bs v y0s ys zs,
      (aligned y0s bs \/ aligned ys bs \/ aligned zs bs) ->
      fby y0s ys zs ->
      ite (init_stream bs) y0s (sfby v ys) zs.

  Lemma arrow_ite : forall bs y0s ys zs,
      (aligned y0s bs \/ aligned ys bs \/ aligned zs bs) ->
      arrow y0s ys zs ->
      ite (sfby true_val (const_val bs false_val)) y0s ys zs.

  Corollary arrow_init_stream_ite : forall bs y0s ys zs,
      (aligned y0s bs \/ aligned ys bs \/ aligned zs bs) ->
      arrow y0s ys zs ->
      ite (init_stream bs) y0s ys zs.

  Lemma ac_sfby : forall c vs,
      abstract_clock (sfby c vs) ≡ abstract_clock vs.

  Lemma init_stream_ac : forall bs,
      abstract_clock (init_stream bs) ≡ bs.

Additional stuff

  Definition st_vars (st : fresh_st (type * clock * bool)) : list (ident * (type * clock)) :=
    idty (st_anns st).

  Fact st_ids_st_vars : forall st,
      st_ids st = map fst (st_vars st).

  Fact st_tys'_st_vars : forall st,
      st_tys' st = idty (st_vars st).

  Fact st_clocks'_st_vars : forall st,
      st_clocks' st = idck (st_vars st).

  Fact st_follows_vars_incl : forall st st',
      st_follows st st' ->
      incl (st_vars st) (st_vars st').

  Import NormFby.

  Fact st_valid_after_NoDupMembers : forall st vars,
      NoDupMembers vars ->
      st_valid_after st (PSP.of_list (map fst vars)) ->
      NoDupMembers (vars++st_vars st).

  Fact fresh_ident_refines' {B V} : forall vars H H' a id (v : V) (st st' : fresh_st B),
      st_valid_after st (PSP.of_list vars) ->
      Env.dom H (vars++st_ids st) ->
      fresh_ident norm2 a st = (id, st') ->
      H' = Env.add id v H ->
      Env.refines eq H H'.

Relation between state and history

  Definition init_eqs_valids bs H (st : fresh_st (Op.type * clock * bool)) :=
    Forall (fun '(id, ck) =>
              (exists bs', sem_clock H bs ck bs' /\
                      sem_var H id (init_stream bs'))) (st_inits st).

  Definition hist_st (vars : list (ident * clock)) b H st :=
    Env.dom H (map fst vars++st_ids st) /\
    init_eqs_valids b H st /\
    LCS.sc_var_inv' (vars++st_clocks' st) H b.

  Fact fresh_ident_init_eqs : forall vars b ty ck id v H st st',
      st_valid_after st (PSP.of_list vars) ->
      Env.dom H (vars ++ st_ids st) ->
      fresh_ident norm2 ((ty, ck), false) st = (id, st') ->
      init_eqs_valids b H st ->
      init_eqs_valids b (Env.add id v H) st'.

  Fact fresh_ident_hist_st : forall vars b ty ck id v H st st',
      st_valid_after st (PSP.of_list (map fst vars)) ->
      sem_clock H b ck (abstract_clock v) ->
      fresh_ident norm2 ((ty, ck), false) st = (id, st') ->
      hist_st vars b H st ->
      hist_st vars b (Env.add id v H) st'.

  Module Import CIStr := CoindIndexedFun Op OpAux CStr IStr.

  Fact sem_clock_when : forall H bs bs' bs'' cs ck id ckb c,
      sem_clock H bs ck bs' ->
      sem_clock H bs (Con ck id ckb) bs'' ->
      sem_var H id cs ->
      when ckb (const bs' c) cs (const bs'' c).

  Lemma add_whens_sem_exp : forall G H b ck ty b' c,
      sem_clock H b ck b' ->
      sem_exp G H b (add_whens (Econst c) ty ck) [const b' c].

  Fact init_var_for_clock_sem : forall G vars bs H ck bs' x eqs' st st',
      sem_clock H bs ck bs' ->
      st_valid_after st (PSP.of_list (map fst vars)) ->
      hist_st vars bs H st ->
      init_var_for_clock ck st = (x, eqs', st') ->
      (exists H',
          Env.refines eq H H' /\
          st_valid_after st' (PSP.of_list (map fst vars)) /\
          hist_st vars bs H' st' /\
          sem_var H' x (init_stream bs') /\
          Forall (sem_equation G H' bs) eqs').

  Hint Constructors LCS.sem_exp_anon.
  Lemma normalized_lexp_sem_sem_anon : forall G H b e vs,
      normalized_lexp e ->
      sem_exp G H b e vs ->
      LCS.sem_exp_anon G H b e vs.

  Lemma normalized_cexp_sem_sem_anon : forall G H b e vs,
      normalized_cexp e ->
      sem_exp G H b e vs ->
      LCS.sem_exp_anon G H b e vs.

  Lemma unnested_equation_sem_sem_anon : forall G env H b equ,
      unnested_equation G equ ->
      wc_equation G env equ ->
      sem_equation G H b equ ->
      LCS.sem_equation_anon G H b equ.

  Corollary normalized_equation_sem_sem_anon : forall G env H b equ out,
      normalized_equation G out equ ->
      wc_equation G env equ ->
      sem_equation G H b equ ->
      LCS.sem_equation_anon G H b equ.

  Lemma sc_lexp : forall G H bs env e s ck,
      wc_global G ->
      LCS.sc_nodes G ->
      NoDupMembers env ->
      wc_env (idck env) ->
      LCS.sc_var_inv' (idck env) H bs ->
      normalized_lexp e ->
      clockof e = [ck] ->
      wt_exp G (idty env) e ->
      wc_exp G (idck env) e ->
      sem_exp G H bs e [s] ->
      sem_clock H bs ck (abstract_clock s).

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

  Fact fby_iteexp_sem : forall G vars bs H e0 e ty nck y0 y z e' eqs' st st',
      wc_global G ->
      LCS.sc_nodes G ->
      NoDupMembers vars ->
      wc_env (idck vars++st_clocks' st) ->
      normalized_lexp e0 ->
      clockof e0 = [fst nck] ->
      wt_exp G (idty vars++st_tys' st) e0 ->
      wc_exp G (idck vars++st_clocks' st) e0 ->
      sem_exp G H bs e0 [y0] ->
      sem_exp G H bs e [y] ->
      fby y0 y z ->
      st_valid_after st (PSP.of_list (map fst vars)) ->
      hist_st (idck vars) bs H st ->
      fby_iteexp e0 e (ty, nck) st = (e', eqs', st') ->
      (exists H',
          Env.refines eq H H' /\
          st_valid_after st' (PSP.of_list (map fst vars)) /\
          hist_st (idck vars) bs H' st' /\
          sem_exp G H' bs e' [z] /\
          Forall (sem_equation G H' bs) eqs').

  Fact arrow_iteexp_sem : forall G vars bs H e0 e ty nck y0 y z e' eqs' st st',
      wc_global G ->
      LCS.sc_nodes G ->
      NoDupMembers vars ->
      wc_env (idck vars++st_clocks' st) ->
      normalized_lexp e0 ->
      clockof e0 = [fst nck] ->
      wt_exp G (idty vars++st_tys' st) e0 ->
      wc_exp G (idck vars++st_clocks' st) e0 ->
      sem_exp G H bs e0 [y0] ->
      sem_exp G H bs e [y] ->
      arrow y0 y z ->
      st_valid_after st (PSP.of_list (map fst vars)) ->
      hist_st (idck vars) bs H st ->
      arrow_iteexp e0 e (ty, nck) st = (e', eqs', st') ->
      (exists H',
          Env.refines eq H H' /\
          st_valid_after st' (PSP.of_list (map fst vars)) /\
          hist_st (idck vars) bs H' st' /\
          sem_exp G H' bs e' [z] /\
          Forall (sem_equation G H' bs) eqs').

  Fact fby_equation_sc_exp : forall G H vars bs e0 ck s0s ss vs,
      wc_global G ->
      LCS.sc_nodes G ->
      NoDupMembers vars ->
      wc_env (idck vars) ->
      normalized_lexp e0 ->
      wt_exp G (idty vars) e0 ->
      wc_exp G (idck vars) e0 ->
      clockof e0 = [ck] ->
      sem_exp G H bs e0 [s0s] ->
      fby s0s ss vs ->
      LCS.sc_var_inv' (idck vars) H bs ->
      sem_clock H bs ck (abstract_clock vs).

  Fact fby_equation_sem : forall G vars bs H to_cut equ eqs' st st',
      wc_global G ->
      LCS.sc_nodes G ->
      NoDupMembers vars ->
      wc_env (idck vars++st_clocks' st) ->
      unnested_equation G equ ->
      wt_equation G (idty vars++st_tys' st) equ ->
      wc_equation G (idck vars++st_clocks' st) equ ->
      sem_equation G H bs equ ->
      st_valid_after st (PSP.of_list (map fst vars)) ->
      hist_st (idck vars) bs H st ->
      fby_equation to_cut equ st = (eqs', st') ->
      (exists H',
          Env.refines eq H H' /\
          st_valid_after st' (PSP.of_list (map fst vars)) /\
          hist_st (idck vars) bs H' st' /\
          Forall (sem_equation G H' bs) eqs').

  Fact fby_equations_sem : forall G vars bs to_cut eqs eqs' H st st',
      wc_global G ->
      LCS.sc_nodes G ->
      NoDupMembers vars ->
      wc_env (idck vars++st_clocks' st) ->
      Forall (unnested_equation G) eqs ->
      Forall (wt_equation G (idty vars++st_tys' st)) eqs ->
      Forall (wc_equation G (idck vars++st_clocks' st)) eqs ->
      Forall (sem_equation G H bs) eqs ->
      st_valid_after st (PSP.of_list (map fst vars)) ->
      hist_st (idck vars) bs H st ->
      fby_equations to_cut eqs st = (eqs', st') ->
      (exists H',
          Env.refines eq H H' /\
          Forall (sem_equation G H' bs) eqs').

  Fact init_st_hist_st : forall b H n,
      Env.dom H (idents (n_in n++n_vars n++n_out n)) ->
      LCS.sc_var_inv' (idck (n_in n++n_vars n++n_out n)) H b ->
      hist_st (idck (n_in n++n_vars n++n_out n)) b H init_st.

  Fact normfby_node_sem_equation : forall G H to_cut n Hwl Hpref ins,
      wc_global G ->
      LCS.sc_nodes G ->
      unnested_node G n ->
      wt_node G n ->
      wc_node G n ->
      LCA.node_causal n ->
      Env.dom H (map fst (n_in n ++ n_vars n ++ n_out n)) ->
      Forall2 (sem_var H) (idents (n_in n)) ins ->
      Forall2 (fun xc => sem_clock H (clocks_of ins) (snd xc)) (idck (n_in n)) (map abstract_clock ins) ->
      Forall (sem_equation G H (clocks_of ins)) (n_eqs n) ->
      exists H' : Env.t (Stream value),
        Env.refines eq H H' /\ Forall (sem_equation G H' (clocks_of ins)) (n_eqs (normfby_node G to_cut n Hwl Hpref)).

  Lemma normfby_node_eq : forall G G' f n Hwl Hpref ins outs to_cut,
      Forall2 (fun n n' => n_name n = n_name n') G G' ->
      global_iface_eq G G' ->
      LCS.global_sc_refines G G' ->
      wt_global (n::G) ->
      wc_global (n::G) ->
      wt_global G' ->
      wc_global G' ->
      Ordered_nodes (n::G) ->
      Ordered_nodes ((normfby_node G to_cut n Hwl Hpref)::G') ->
      Forall LCA.node_causal (n::G) ->
      Forall LCA.node_causal G' ->
      sem_node (n::G) f ins outs ->
      LCS.sem_clock_inputs (n::G) f ins ->
      sem_node ((normfby_node G to_cut n Hwl Hpref)::G') f ins outs.

  Fact iface_eq_sem_clocks_input : forall G G' f ins,
      global_iface_eq G G' ->
      LCS.sem_clock_inputs G f ins ->
      LCS.sem_clock_inputs G' f ins.

  Fact normfby_global_names' : forall G Hwl Hprefs,
      Forall2 (fun n n' => n_name n = n_name n') G (normfby_global G Hwl Hprefs).

  Lemma normfby_global_refines : forall G Hunt Hprefs,
      wt_global G ->
      wc_global G ->
      Forall LCA.node_causal G ->
      LCS.global_sc_refines G (normfby_global G Hunt Hprefs).

  Corollary normfby_global_sem : forall G Hunt Hprefs f ins outs,
      wt_global G ->
      wc_global G ->
      Ordered_nodes G ->
      Forall LCA.node_causal G ->
      sem_node G f ins outs ->
      LCS.sem_clock_inputs G f ins ->
      sem_node (normfby_global G Hunt Hprefs) f ins outs.

  Corollary normfby_global_sem_clock_inputs : forall G Hwl Hprefs f ins,
      LCS.sem_clock_inputs G f ins ->
      LCS.sem_clock_inputs (normfby_global G Hwl Hprefs) f ins.

Conclusion

  Theorem normalize_global_sem : forall G Hwl Hprefs G' f ins outs,
      wt_global G ->
      wc_global G ->
      sem_node G f ins outs ->
      LCS.sem_clock_inputs G f ins ->
      normalize_global G Hwl Hprefs = Errors.OK G' ->
      sem_node G' f ins outs.

  Corollary normalize_global_sem_clock_inputs : forall G G' Hwl Hprefs f ins,
      LCS.sem_clock_inputs G f ins ->
      normalize_global G Hwl Hprefs = Errors.OK G' ->
      LCS.sem_clock_inputs G' f ins.

In addition : normalization only produces causal programs

  Lemma normalize_global_causal : forall G G' Hwl Hprefs,
      wc_global G ->
      normalize_global G Hwl Hprefs = Errors.OK G' ->
      Forall LCA.node_causal G'.

End CORRECTNESS.

Module CorrectnessFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Op)
       (CStr : COINDSTREAMS Op OpAux)
       (IStr : INDEXEDSTREAMS Op OpAux)
       (Syn : LSYNTAX Ids Op)
       (LCA : LCAUSALITY Ids Op Syn)
       (Ty : LTYPING Ids Op Syn)
       (Clo : LCLOCKING Ids Op Syn)
       (Lord : LORDERED Ids Op Syn)
       (Sem : LSEMANTICS Ids Op OpAux Syn Lord CStr)
       (LClockSem : LCLOCKSEMANTICS Ids Op OpAux Syn Clo LCA Lord CStr IStr Sem)
       (Norm : NORMALIZATION Ids Op OpAux Syn LCA)
       <: CORRECTNESS Ids Op OpAux CStr IStr Syn LCA Ty Clo Lord Sem LClockSem Norm.
  Include CORRECTNESS Ids Op OpAux CStr IStr Syn LCA Ty Clo Lord Sem LClockSem Norm.
End CorrectnessFun.