From Coq Require Import List Sorting.Permutation.
Import List.ListNotations.
Open Scope list_scope.
Require Import Omega.

From Coq Require Import Setoid Morphisms.

From Velus Require Import Common Environment.
From Velus Require Import Operators.
From Velus Require Import Lustre.LSyntax.
From Velus Require Lustre.Normalization.Fresh.

Normalization procedure

Module Type UNNESTING
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (OpAux : OPERATORS_AUX Op)
       (Import Syn : LSYNTAX Ids Op).

  Module Fresh := Fresh.Fresh(Ids).
  Export Fresh.
  Import Fresh Notations Facts Tactics.
  Local Open Scope fresh_monad_scope.

Some additional tactics

  Ltac simpl_forall :=
    repeat
      match goal with
      | |- Forall2 _ ?l1 ?l1 => apply Forall2_same
      | H : Forall _ (map _ _) |- _ => rewrite Forall_map in H
      | H : Forall2 _ (map _ _) _ |- _ => rewrite Forall2_map_1 in H
      | H : Forall2 _ _ (map _ _) |- _ => rewrite Forall2_map_2 in H
      | |- Forall _ (map _ _) => rewrite Forall_map
      | |- Forall2 _ (map _ _) _ => rewrite Forall2_map_1
      | |- Forall2 _ _ (map _ _) => rewrite Forall2_map_2
      | |- Forall _ (combine _ _) => eapply Forall2_combine'
      | |- Forall2 _ (combine _ _) _ => eapply Forall3_combine'1
      | H1 : Forall _ ?l, H2 : Forall _ ?l |- _ =>
        eapply Forall_Forall in H1; [|eapply H2]; clear H2
      | H1 : Forall2 _ ?l1 ?l2, H2 : Forall2 _ ?l1 ?l2 |- _ =>
        eapply Forall2_Forall2 in H1; [|eapply H2]; clear H2
      | H1 : Forall3 _ ?l1 ?l2 ?l3, H2 : Forall3 _ ?l1 ?l2 ?l3 |- _ =>
        eapply Forall3_Forall3 in H1; [|eapply H2]; clear H2
      | H : Forall _ ?l1 |- Forall2 _ ?l1 ?l2 =>
        eapply Forall2_ignore2' with (ys:=l2) in H; try congruence
      | H : Forall _ ?l2 |- Forall2 _ ?l1 ?l2 =>
        eapply Forall2_ignore1' with (xs:=l1) in H; try congruence
      | H : Forall2 _ ?l2 ?l3 |- Forall3 _ ?l1 ?l2 ?l3 =>
        eapply Forall3_ignore1' with (xs:=l1) in H; try congruence
      | H : Forall2 _ ?l1 ?l3 |- Forall3 _ ?l1 ?l2 ?l3 =>
        eapply Forall3_ignore2' with (ys:=l2) in H; try congruence
      | H : Forall2 _ ?l1 ?l2 |- Forall3 _ ?l1 ?l2 ?l3 =>
        eapply Forall3_ignore3' with (zs:=l3) in H; try congruence
      | H : Forall _ ?l1 |- Forall3 _ ?l1 ?l2 ?l3 =>
        eapply Forall2_ignore2' with (ys:=l2) in H; try congruence
      | H : Forall _ ?l2 |- Forall3 _ ?l1 ?l2 ?l3 =>
        eapply Forall2_ignore1' with (xs:=l1) in H; try congruence
      | H : Forall _ ?l3 |- Forall3 _ ?l1 ?l2 ?l3 =>
        eapply Forall2_ignore1' with (xs:=l1) in H; try congruence
      end; simpl in *; auto.

  Ltac destruct_conjs :=
    repeat
      match goal with
      | H: _ /\ _ |- _ => destruct H
      | x: _ * _ |- _ => destruct x
      end.

  Ltac solve_forall :=
    simpl_forall;
    match goal with
    | H: Forall _ ?l |- Forall _ ?l =>
      eapply Forall_impl_In; [|eapply H]; clear H; intros; simpl in *
    | H: Forall2 _ ?l1 ?l2 |- Forall2 _ ?l1 ?l2 =>
      eapply Forall2_impl_In; [|eapply H]; clear H; intros; simpl in *
    | H: Forall3 _ ?l1 ?l2 ?l3 |- Forall3 _ ?l1 ?l2 ?l3 =>
      eapply Forall3_impl_In; [|eapply H]; clear H; intros; simpl in *
    | |- Forall _ _ =>
      eapply Forall_forall; intros
    | _ => idtac
    end; destruct_conjs; eauto.

  Ltac simpl_In :=
    match goal with
    | x : ?t1 * ?t2 |- _ =>
      destruct x
    | H : In (?x1, ?x2) (combine ?l1 ?l2) |- _ =>
      specialize (in_combine_l _ _ _ _ H) as ?; apply in_combine_r in H
    | H : In ?x (map ?f ?l) |- _ =>
      rewrite in_map_iff in H; destruct H as [? [? ?]]; subst
    | H : In ?x (idty ?l) |- _ =>
      rewrite In_idty_exists in H; destruct H as (?&?); subst
    | H : In ?x (idck ?l) |- _ =>
      rewrite In_idck_exists in H; destruct H as (?&?); subst
    | |- In ?x (map ?f ?l) => rewrite in_map_iff
    | |- In ?x (idty ?l) => rewrite In_idty_exists
    | |- In ?x (idck ?l) => rewrite In_idck_exists
    end.

  Ltac simpl_list :=
    simpl in *;
    match goal with
    | H : context c [annots ?es] |- _ => unfold annots in H
    | |- context c [annots ?es] => unfold annots
    | H : context c [typesof ?es] |- _ => unfold typesof in H
    | |- context c [typesof ?es] => unfold typesof
    | H : context c [clocksof ?es] |- _ => unfold clocksof in H
    | |- context c [clocksof ?es] => unfold clocksof
    | H : context c [vars_defined ?es] |- _ => unfold vars_defined in H
    | |- context c [vars_defined ?es] => unfold vars_defined
    | H: context c [flat_map ?f ?l] |- _ => rewrite flat_map_concat_map in H
    | |- context c [flat_map ?f ?l] => rewrite flat_map_concat_map
    | H: context c [map ?f (map ?g ?l)] |- _ => rewrite map_map in H
    | |- context c [map ?f (map ?g ?l)] => rewrite map_map
    | H: context c [map ?f (app ?l1 ?l2)] |- _ => rewrite map_app in H
    | |- context c [map ?f (app ?l1 ?l2)] => rewrite map_app
    | H: context c [concat (app ?l1 ?l2)] |- _ => rewrite concat_app in H
    | |- context c [concat (app ?l1 ?l2)] => rewrite concat_app
    | H: context c [idty (?l1 ++ ?l2)] |- _ => rewrite idty_app in H
    | H: context c [idck (?l1 ++ ?l2)] |- _ => rewrite idck_app in H
    | H: context c [app ?l nil] |- _ => rewrite app_nil_r in H
    | |- context c [app ?l nil] => rewrite app_nil_r
    | H: context c [app (app ?l1 ?l2) ?l3] |- _ => rewrite <- app_assoc in H
    | |- context c [app (app ?l1 ?l2) ?l3] => rewrite <- app_assoc
    end.

  Ltac subst_length :=
    match goal with
    | H: length ?x1 = length ?x2 |- context l [length ?x1] =>
      setoid_rewrite H
    | H: length ?x1 = length ?x2, H1: context l [length ?x1] |- _ =>
      setoid_rewrite H in H1
    | H: ?x1 = ?x2 |- context l [length ?x1] =>
      setoid_rewrite H
    | H: ?x1 = ?x2, H1: context l [length ?x1] |- _ =>
      setoid_rewrite H in H1
    end.

  Ltac simpl_length :=
    repeat subst_length;
    (match goal with
     | H : context c [typesof _] |- _ =>
       rewrite typesof_annots in H
     | H : context c [clocksof _] |- _ =>
       rewrite clocksof_annots in H
     | H : _ < Nat.min _ _ |- _ =>
       setoid_rewrite Nat.min_glb_lt_iff in H; destruct H
     | H : context c [Nat.min ?x1 ?x1] |- _ =>
       repeat setoid_rewrite PeanoNat.Nat.min_id in H
     | H : context c [length (combine _ _)] |- _ =>
       setoid_rewrite combine_length in H
     | H : context c [length (map ?l1 ?l2)] |- _ =>
       setoid_rewrite map_length in H
     | |- _ < Nat.min _ _ =>
       apply Nat.min_glb_lt
     | |- context c [Nat.min ?x1 ?x1] =>
       setoid_rewrite PeanoNat.Nat.min_id
     | |- context c [length (combine _ _)] =>
       setoid_rewrite combine_length
     | |- context c [length (map _ _)] =>
       setoid_rewrite map_length
     | |- context c [typesof _] =>
       rewrite typesof_annots
     | |- context c [clocksof _] =>
       rewrite clocksof_annots
     | _ => idtac
     end).

  Ltac solve_length :=
    repeat simpl_length; auto; try congruence.

  Ltac simpl_nth :=
    match goal with
    | H : In ?x _ |- _ =>
      apply In_nth with (d:=x) in H; destruct H as [? [? ?]]
    | H : context c [nth _ (combine _ _) (?x1, ?x2)] |- _ =>
      rewrite (combine_nth _ _ _ x1 x2) in H; [inv H|clear H;try solve_length]
    | H : context c [nth _ (map _ _) _] |- _ =>
      erewrite map_nth' in H; [|clear H; try solve_length]
    | |- context c [nth _ (map _ _) _] =>
      erewrite map_nth'; [| try solve_length]
    end.

  Ltac ndup_simpl :=
    repeat rewrite map_app, <- app_assoc in *.
  Ltac ndup_l H :=
    ndup_simpl;
    rewrite Permutation_swap in H;
    apply NoDup_app_r in H; auto.
  Ltac ndup_r H :=
    ndup_simpl;
    apply NoDup_app_r in H; auto.

  Definition default_ann : ann := (Op.bool_type, (Cbase, None)).

  Definition FreshAnn A := Fresh A (type * clock).

  Definition hd_default (l : list exp) : exp :=
    hd (Econst (init_type bool_type)) l.

  Fixpoint idents_for_anns (anns : list ann) : FreshAnn (list (ident * ann)) :=
    match anns with
    | [] => ret []
    | (ty, (cl, name))::tl => do x <- fresh_ident norm1 (ty, cl);
                            do xs <- idents_for_anns tl;
                            ret ((x, (ty, (cl, name)))::xs)
    end.

  Fact idents_for_anns_values: forall anns ids st st',
      idents_for_anns anns st = (ids, st') ->
      map snd ids = anns.

  Corollary idents_for_anns_length : forall anns idents st st',
      idents_for_anns anns st = (idents, st') ->
      length idents = length anns.
  Hint Resolve idents_for_anns_length.

  Fixpoint idents_for_anns' (anns : list ann) :=
    match anns with
    | [] => ret []
    | (ty, (ck, None))::tl => do x <- fresh_ident norm1 (ty, ck);
                            do xs <- idents_for_anns' tl;
                            ret ((x, (ty, (ck, None)))::xs)
    | (ty, (ck, Some x))::tl => do _ <- reuse_ident x (ty, ck);
                              do xs <- idents_for_anns' tl;
                              ret ((x, (ty, (ck, Some x)))::xs)
    end.

  Fact idents_for_anns'_values: forall anns idents st st',
      idents_for_anns' anns st = (idents, st') ->
      map snd idents = anns.

  Corollary idents_for_anns'_length : forall anns ids st st',
      idents_for_anns' anns st = (ids, st') ->
      length ids = length anns.
  Hint Resolve idents_for_anns'_length.

  Definition unnest_reset k (e : option exp) : FreshAnn (option exp * list equation) :=
    match e with
    | None => ret (None, [])
    | Some e => do (e', eqs1) <- k e;
               match hd_default e' with
               | Evar v ann => ret (Some (Evar v ann), eqs1)
               | e => let '(ty, (ck, _)) := hd (bool_type, (Cbase, None)) (annot e) in
                     do x <- fresh_ident norm1 (ty, ck);
                     ret (Some (Evar x (ty, (ck, Some x))), ([x], [e])::eqs1)
               end
    end.

  Lemma unnest_reset_spec : forall k e es' eqs' st st',
      k e st = ((es', eqs'), st') ->
      (exists v, exists ann, (hd_default es') = Evar v ann /\ unnest_reset k (Some e) st = ((Some (Evar v ann), eqs'), st'))
      \/ exists ty ck o x st'', hd (bool_type, (Cbase, None)) (annot (hd_default es')) = (ty, (ck, o)) /\
                          fresh_ident norm1 (ty, ck) st' = (x, st'') /\
                          unnest_reset k (Some e) st = ((Some (Evar x (ty, (ck, Some x))), ([x], [hd_default es'])::eqs'), st'').

  Ltac unnest_reset_spec :=
    match goal with
    | H:unnest_reset ?k ?e ?st = (?res, ?st') |- _ =>
      let e' := fresh "e" in
      destruct e as [e'|];
      [ let Hk := fresh "Hk" in let Hk' := fresh "Hk" in
                                let Hhd := fresh "Hhd" in
                                let Hfresh := fresh "Hfresh" in
                                let Hnorm' := fresh "Hnorm" in
                                destruct (k e' st) as [[? ?] ?] eqn:Hk;
                                assert (Hk' := Hk);
                                eapply unnest_reset_spec in Hk as [[? [[? [? ?]] [? Hnorm']]]|[? [? [? [? [? [Hhd [Hfresh Hnorm']]]]]]]]; subst;
                                rewrite Hnorm' in H; clear Hnorm'; inv H
      | simpl in H; repeat inv_bind ]
    end.

  Definition unnest_fby (e0s : list exp) (es : list exp) (anns : list ann) :=
    map (fun '((e0, e), a) => Efby [e0] [e] [a]) (combine (combine e0s es) anns).

  Definition unnest_arrow (e0s : list exp) (es : list exp) (anns : list ann) :=
    map (fun '((e0, e), a) => Earrow [e0] [e] [a]) (combine (combine e0s es) anns).

  Definition unnest_when ckid b es tys ck :=
    map (fun '(e, ty) => Ewhen [e] ckid b ([ty], ck)) (combine es tys).

  Definition unnest_merge ckid ets efs tys ck :=
    map (fun '((e1, e2), ty) => Emerge ckid [e1] [e2] ([ty], ck)) (combine (combine ets efs) tys).

  Definition unnest_ite e ets efs tys ck :=
    map (fun '((et, ef), ty) => Eite e [et] [ef] ([ty], ck)) (combine (combine ets efs) tys).

  Hint Unfold unnest_when unnest_merge unnest_ite.

  Corollary unnest_reset_Some : forall k e e' eqs' st st',
      unnest_reset k (Some e) st = (e', eqs', st') ->
      exists e'', e' = Some e''.

  Fixpoint is_noops_exp (ck: clock) (e : exp) : bool :=
    match ck with
    | Cbase => true
    | Con ck' _ _ =>
      match e with
      | Econst _ | Evar _ _ => true
      | Ewhen [e'] _ _ _ => is_noops_exp ck' e'
      | _ => false
      end
    end.

  Definition find_node_incks G (f : ident) : list clock :=
    match find_node f G with
    | Some n => map (fun '(_, (_, ck)) => ck) (n_in n)
    | None => []
    end.

  Definition unnest_noops_exp (cki: clock) (e : exp) : FreshAnn (exp * list equation) :=
    let '(ty, (ck, o)) := hd (bool_type, (Cbase, None)) (annot e) in
    if is_noops_exp cki e then ret (e, [])
    else do x <- fresh_ident norm1 (ty, ck);
         ret (Evar x (ty, (ck, o)), [([x], [e])]).

  Definition unnest_noops_exps (ckis : list clock) (es : list exp) : FreshAnn (list exp * list equation) :=
    do (es', eqs') <- map_bind2 (fun '(cki, e) => unnest_noops_exp cki e) (combine ckis es);
    ret (es', concat eqs').

  Fixpoint unnest_exp G (is_control : bool) (e : exp) {struct e} : FreshAnn (list exp * list equation) :=
    let unnest_exps := fun es => do (es, eqs) <- map_bind2 (unnest_exp G false) es; ret (concat es, concat eqs) in
    let unnest_controls := fun es => do (es, eqs) <- map_bind2 (unnest_exp G true) es; ret (concat es, concat eqs) in
    match e with
    | Econst c => ret ([Econst c], [])
    | Evar v ann => ret ([Evar v ann], [])
    | Eunop op e1 ann =>
      do (e1', eqs) <- unnest_exp G false e1;
      ret ([Eunop op (hd_default e1') ann], eqs)
    | Ebinop op e1 e2 ann =>
      do (e1', eqs1) <- unnest_exp G false e1;
      do (e2', eqs2) <- unnest_exp G false e2;
      ret ([Ebinop op (hd_default e1') (hd_default e2') ann], eqs1++eqs2)
    | Efby e0s es anns =>
      do (e0s', eqs1) <- unnest_exps e0s;
      do (es', eqs2) <- unnest_exps es;
      let fbys := unnest_fby e0s' es' anns in
      do xs <- idents_for_anns anns;
      ret (List.map (fun '(x, ann) => Evar x ann) xs,
           (List.map (fun '((x, _), fby) => ([x], [fby])) (combine xs fbys))++eqs1++eqs2)
    | Earrow e0s es anns =>
      do (e0s', eqs1) <- unnest_exps e0s;
      do (es', eqs2) <- unnest_exps es;
      let arrows := unnest_arrow e0s' es' anns in
      do xs <- idents_for_anns anns;
      ret (List.map (fun '(id, ann) => Evar id ann) xs,
           (combine (List.map (fun '(id, _) => [id]) xs) (List.map (fun e => [e]) arrows))++eqs1++eqs2)
    | Ewhen es ckid b (tys, ck) =>
      do (es', eqs) <- unnest_exps es;
      ret (unnest_when ckid b es' tys ck, eqs)
    | Emerge ckid es1 es2 (tys, cl) =>
      do (es1', eqs1) <- unnest_controls es1;
      do (es2', eqs2) <- unnest_controls es2;
      let merges := unnest_merge ckid es1' es2' tys cl in
      if is_control then
        ret (merges, eqs1++eqs2)
      else
        do xs <- idents_for_anns (List.map (fun ty => (ty, cl)) tys);
        ret (List.map (fun '(id, ann) => Evar id ann) xs,
             (combine (List.map (fun '(id, _) => [id]) xs) (List.map (fun e => [e]) merges))++eqs1++eqs2)
    | Eite e es1 es2 (tys, ck) =>
      do (e', eqs0) <- unnest_exp G false e;
      do (es1', eqs1) <- unnest_controls es1;
      do (es2', eqs2) <- unnest_controls es2;
      let ites := unnest_ite (hd_default e') es1' es2' tys ck in
      if is_control then
        ret (ites, eqs0++eqs1++eqs2)
      else
        do xs <- idents_for_anns (List.map (fun ty => (ty, ck)) tys);
        ret (List.map (fun '(id, ann) => Evar id ann) xs,
             (combine (List.map (fun '(id, _) => [id]) xs) (List.map (fun e => [e]) ites))++eqs0++eqs1++eqs2)
    | Eapp f es er anns =>
      do (es', eqs1) <- unnest_exps es;
      do (es', eqs2) <- unnest_noops_exps (find_node_incks G f) es';
      do (er', eqs3) <- unnest_reset (unnest_exp G true) er;
      do xs <- idents_for_anns' anns;
      ret (List.map (fun '(id, ann) => Evar id ann) xs,
           (List.map fst xs, [Eapp f es' er' (List.map snd xs)])::eqs1++eqs2++eqs3)
    end.

  Definition unnest_exps G (es : list exp) :=
    do (es, eqs) <- map_bind2 (unnest_exp G false) es;
    ret (concat es, concat eqs).

  Definition unnest_rhs G (e : exp) : FreshAnn (list exp * list equation) :=
    match e with
    | Eapp f es er anns =>
      do (es', eqs1) <- unnest_exps G es;
      do (es', eqs2) <- unnest_noops_exps (find_node_incks G f) es';
      do (er', eqs3) <- unnest_reset (unnest_exp G true) er;
      ret ([Eapp f es' er' anns], eqs1++eqs2++eqs3)
    | Efby e0s es anns =>
      do (e0s', eqs1) <- unnest_exps G e0s;
      do (es', eqs2) <- unnest_exps G es;
      let fbys := unnest_fby e0s' es' anns in
      ret (fbys, eqs1++eqs2)
    | Earrow e0s es anns =>
      do (e0s', eqs1) <- unnest_exps G e0s;
      do (es', eqs2) <- unnest_exps G es;
      let arrows := unnest_arrow e0s' es' anns in
      ret (arrows, eqs1++eqs2)
    | _ => unnest_exp G true e
    end.

  Definition unnest_rhss G (es : list exp) :=
    do (es, eqs) <- map_bind2 (unnest_rhs G) es; ret (concat es, concat eqs).

  Fixpoint combine_for_numstreams {B} (es : list exp) (vs : list B) :=
    match es with
    | [] => []
    | hd::tl => let n := numstreams hd in
              (hd, (firstn n vs))::(combine_for_numstreams tl (skipn n vs))
    end.

  Definition split_equation (eq : equation) : list equation :=
    let (xs, es) := eq in
    List.map (fun '(e, xs) => (xs, [e])) (combine_for_numstreams es xs).

  Definition unnest_equation G (e : equation) : FreshAnn (list equation) :=
    let '(xs, es) := e in
    do (es', eqs) <- unnest_rhss G es;
    ret ((split_equation (xs, es'))++eqs).

  Definition unnest_equations G (eqs : list equation) : FreshAnn (list equation) :=
    do eqs <- map_bind (unnest_equation G) eqs;
    ret (concat eqs).

  Definition unnest_equations' G (eq : list equation) (st : fresh_st (type * clock)) :
    { res | unnest_equations G eq st = res }.

Some additional facts

  Fact combine_for_numstreams_In {B} : forall es (xs : list B) e x,
      In (e, x) (combine_for_numstreams es xs) ->
      In e es.

Propagation of the st_valid_after property

  Fact idents_for_anns_st_valid_after : forall anns res st st' aft,
      idents_for_anns anns st = (res, st') ->
      st_valid_after st norm1 aft ->
      st_valid_after st' norm1 aft.
  Hint Resolve idents_for_anns_st_valid_after.

Propagation of the st_valid_reuse property

  Definition elab_prefs := PS.singleton elab.
  Definition st_valid_reuse {B} st aft reusable := @st_valid_reuse B st norm1 aft elab_prefs reusable.
  Hint Unfold st_valid_reuse.

  Fact idents_for_anns_st_valid_reuse : forall anns res st st' aft reusable,
      idents_for_anns anns st = (res, st') ->
      st_valid_reuse st aft reusable ->
      st_valid_reuse st' aft reusable.
  Hint Resolve idents_for_anns_st_valid_reuse.

  Fact idents_for_anns'_st_valid : forall anns res st st' aft reusable,
      NoDup (map fst (anon_streams anns)++PS.elements reusable) ->
      idents_for_anns' anns st = (res, st') ->
      st_valid_reuse st aft (ps_adds (map fst (anon_streams anns)) reusable) ->
      st_valid_reuse st' aft reusable.
  Hint Resolve idents_for_anns'_st_valid.

  Fact unnest_reset_st_valid : forall k e e' eqs' st st' aft reu,
      LiftO True (fun e => forall res st st',
                   k e st = (res, st') ->
                   st_valid_reuse st aft (ps_adds (map fst (fresh_in e)) reu) ->
                   st_valid_reuse st' aft reu) e ->
      unnest_reset k e st = (e', eqs', st') ->
      st_valid_reuse st aft (match e with None => reu | Some e' => ps_adds (map fst (fresh_in e')) reu end) ->
      st_valid_reuse st' aft reu.
  Hint Resolve unnest_reset_st_valid.

  Fact unnest_noops_exp_st_valid : forall e ck e' eqs' st st' aft reu,
      unnest_noops_exp ck e st = (e', eqs', st') ->
      st_valid_reuse st aft reu ->
      st_valid_reuse st' aft reu.

  Fact unnest_noops_exps_st_valid : forall es ckis es' eqs' st st' aft reu,
      unnest_noops_exps ckis es st = (es', eqs', st') ->
      st_valid_reuse st aft reu ->
      st_valid_reuse st' aft reu.

  Fact map_bind2_st_valid_reuse' {B} :
    forall (k : exp -> list (ident * B)) (f : exp -> FreshAnn (list exp * list equation)) es es' eqs' st st' aft reusable,
      Forall (fun e =>
                forall es' eqs' st st' aft reusable,
                  NoDup (map fst (k e)++PS.elements reusable) ->
                  f e st = (es', eqs', st') ->
                  st_valid_reuse st aft (ps_adds (map fst (k e)) reusable) ->
                  st_valid_reuse st' aft reusable) es ->
      NoDup (map fst (concat (map k es))++PS.elements reusable) ->
      map_bind2 f es st = (es', eqs', st') ->
      st_valid_reuse st aft (ps_adds (map fst (concat (map k es))) reusable) ->
      st_valid_reuse st' aft reusable.

  Local Ltac solve_st_valid :=
    match goal with
    | H : map_bind2 _ _ _ = (_, _, ?st) |- st_valid_reuse ?st _ _ =>
      eapply map_bind2_st_valid_reuse' in H; eauto; solve_forall
    | H : unnest_reset _ _ = (_, _, ?st) |- st_valid_reuse ?st _ _ =>
      eapply unnest_reset_st_valid; eauto
    | H : unnest_noops_exps _ _ _ = (_, _, ?st) |- st_valid_reuse ?st _ _ =>
      eapply unnest_noops_exps_st_valid; eauto
    | H : idents_for_anns _ _ = (_, ?st) |- st_valid_reuse ?st _ _ =>
      eapply idents_for_anns_st_valid_reuse; eauto
    | H : idents_for_anns' _ _ = (_, ?st) |- st_valid_reuse ?st _ _ =>
      eapply idents_for_anns'_st_valid; eauto
    end.

  Global Add Parametric Morphism {B} st aft : (@st_valid_reuse B st aft)
      with signature @PS.eq ==> Basics.impl
        as st_valid_reuse_PSeq_Proper.

  Fact unnest_exp_st_valid : forall G e is_control res st st' aft reusable,
      NoDup (map fst (fresh_in e)++PS.elements reusable) ->
      unnest_exp G is_control e st = (res, st') ->
      st_valid_reuse st aft (ps_adds (map fst (fresh_in e)) reusable) ->
      st_valid_reuse st' aft reusable.
  Hint Resolve unnest_exp_st_valid.

  Fact unnest_rhs_st_valid : forall G e res st st' aft reusable,
      NoDup (map fst (anon_in e)++PS.elements reusable) ->
      unnest_rhs G e st = (res, st') ->
      st_valid_reuse st aft (ps_adds (map fst (anon_in e)) reusable) ->
      st_valid_reuse st' aft reusable.
  Hint Resolve unnest_rhs_st_valid.

  Fact unnest_equation_st_valid : forall G e res st st' aft reusable,
      NoDup (map fst (anon_in_eq e)++PS.elements reusable) ->
      unnest_equation G e st = (res, st') ->
      st_valid_reuse st aft (ps_adds (map fst (anon_in_eq e)) reusable) ->
      st_valid_reuse st' aft reusable.
  Hint Resolve unnest_equation_st_valid.

  Fact unnest_equations_st_valid : forall G eqs res st st' aft reusable,
      NoDup (map fst (anon_in_eqs eqs)++PS.elements reusable) ->
      unnest_equations G eqs st = (res, st') ->
      st_valid_reuse st aft (ps_adds (map fst (anon_in_eqs eqs)) reusable) ->
      st_valid_reuse st' aft reusable.

Propagation of the st_follows property

  Fact idents_for_anns_st_follows : forall anns res st st',
      idents_for_anns anns st = (res, st') ->
      st_follows st st'.
  Hint Resolve idents_for_anns_st_follows.

  Corollary idents_for_anns_incl : forall anns ids st st',
      idents_for_anns anns st = (ids, st') ->
      incl (List.map (fun '(id, (ty, (cl, _))) => (id, (ty, cl))) ids) (st_anns st').

  Corollary idents_for_anns_incl_ids : forall anns ids st st',
      idents_for_anns anns st = (ids, st') ->
      incl (List.map fst ids) (st_ids st').

  Fact idents_for_anns'_st_follows : forall anns res st st',
      idents_for_anns' anns st = (res, st') ->
      st_follows st st'.
  Hint Resolve idents_for_anns'_st_follows.

  Corollary idents_for_anns'_incl : forall anns ids st st',
      idents_for_anns' anns st = (ids, st') ->
      incl (List.map (fun '(id, (ty, (cl, _))) => (id, (ty, cl))) ids) (st_anns st').

  Corollary idents_for_anns'_incl_ids : forall anns ids st st',
      idents_for_anns' anns st = (ids, st') ->
      incl (List.map fst ids) (st_ids st').

  Fact unnest_reset_st_follows' : forall k e res st st',
      LiftO True (fun e => forall res st st',
                   k e st = (res, st') ->
                   st_follows st st') e ->
      unnest_reset k e st = (res, st') ->
      st_follows st st'.
  Hint Resolve unnest_reset_st_follows'.

  Lemma unnest_noops_exp_st_follows : forall e ck e' eqs' st st' ,
      unnest_noops_exp ck e st = (e', eqs', st') ->
      st_follows st st'.
  Hint Resolve unnest_noops_exp_st_follows.

  Lemma unnest_noops_exps_st_follows : forall es ckis es' eqs' st st' ,
      unnest_noops_exps ckis es st = (es', eqs', st') ->
      st_follows st st'.
  Hint Resolve unnest_noops_exps_st_follows.

  Local Ltac solve_st_follows' :=
    match goal with
    | |- st_follows ?st ?st =>
      reflexivity
    | H : st_follows ?st1 ?st2 |- st_follows ?st1 _ =>
      etransitivity; [eapply H |]
    | H : fresh_ident _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply fresh_ident_st_follows in H; eauto | ]
    | H : reuse_ident _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply reuse_ident_st_follows in H; eauto | ]
    | H : idents_for_anns _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply idents_for_anns_st_follows in H; eauto | ]
    | H : idents_for_anns' _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply idents_for_anns'_st_follows in H; eauto | ]
    | H : unnest_reset _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_reset_st_follows' in H; eauto | ]
    | H : unnest_noops_exps _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_noops_exps_st_follows in H; eauto | ]
    | H : map_bind2 _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply map_bind2_st_follows in H; eauto; solve_forall | ]
    end.

  Fact unnest_exp_st_follows : forall G e is_control res st st',
      unnest_exp G is_control e st = (res, st') ->
      st_follows st st'.
  Hint Resolve unnest_exp_st_follows.

  Corollary unnest_exps_st_follows : forall G es res st st',
      unnest_exps G es st = (res, st') ->
      st_follows st st'.

  Fact unnest_rhs_st_follows : forall G e res st st',
      unnest_rhs G e st = (res, st') ->
      st_follows st st'.
  Hint Resolve unnest_rhs_st_follows.

  Corollary unnest_rhss_st_follows : forall G es res st st',
      unnest_rhss G es st = (res, st') ->
      st_follows st st'.
  Hint Resolve unnest_rhss_st_follows.

  Fact unnest_equation_st_follows : forall G e res st st',
      unnest_equation G e st = (res, st') ->
      st_follows st st'.
  Hint Resolve unnest_equation_st_follows.

  Fact unnest_equations_st_follows : forall G eqs res st st',
      unnest_equations G eqs st = (res, st') ->
      st_follows st st'.

  Fact unnest_reset_st_follows : forall G b e res st st',
      unnest_reset (unnest_exp G b) e st = (res, st') ->
      st_follows st st'.

Length of unnested expression

  Ltac rewrite_Forall_forall :=
    match goal with
    | H : Forall _ _ |- _ =>
      rewrite Forall_forall in H
    | H : Forall2 _ _ _ |- _ =>
      rewrite Forall2_forall2 in H; destruct H
    | H : Forall3 _ _ _ _ |- _ =>
      rewrite Forall3_forall3 in H; destruct H as [? [? ?]]
    | |- Forall _ _ =>
      rewrite Forall_forall; intros; subst
    | |- Forall2 _ _ _ =>
      rewrite Forall2_forall2; repeat split; auto; intros; subst
    | |- Forall3 _ _ _ _ =>
      rewrite Forall3_forall3; repeat split; auto; intros; subst
    end.

  Fact map_bind2_length : forall G is_control es es' eqs' st st',
      Forall2 (fun e es' => forall eqs' st st',
                   unnest_exp G is_control e st = (es', eqs', st') ->
                   length es' = numstreams e) es es' ->
      map_bind2 (unnest_exp G is_control) es st = (es', eqs', st') ->
      length (concat es') = length (annots es).

  Local Hint Resolve nth_In.
  Fact unnest_exp_length : forall G e is_control es' eqs' st st',
      wl_exp G e ->
      unnest_exp G is_control e st = (es', eqs', st') ->
      length es' = numstreams e.
  Hint Resolve unnest_exp_length.

  Corollary map_bind2_unnest_exp_length : forall G is_control es es' eqs' st st',
      Forall (wl_exp G) es ->
      map_bind2 (unnest_exp G is_control) es st = (es', eqs', st') ->
      length (concat es') = length (annots es).
  Hint Resolve map_bind2_unnest_exp_length.

  Corollary unnest_exps_length : forall G es es' eqs' st st',
      Forall (wl_exp G) es ->
      unnest_exps G es st = (es', eqs', st') ->
      length es' = length (annots es).
  Hint Resolve unnest_exps_length.

  Fact unnest_fby_length : forall e0s es anns,
      length e0s = length anns ->
      length es = length anns ->
      length (unnest_fby e0s es anns) = length anns.

  Fact unnest_arrow_length : forall e0s es anns,
      length e0s = length anns ->
      length es = length anns ->
      length (unnest_arrow e0s es anns) = length anns.


  Fact unnest_merge_length : forall ckid ets efs tys nck,
      length ets = length tys ->
      length efs = length tys ->
      length (unnest_merge ckid ets efs tys nck) = length tys.

  Fact unnest_ite_length : forall e ets efs tys nck,
      length ets = length tys ->
      length efs = length tys ->
      length (unnest_ite e ets efs tys nck) = length tys.

  Fact unnest_rhs_length : forall G e es' eqs' st st',
      wl_exp G e ->
      unnest_rhs G e st = (es', eqs', st') ->
      (length es' = 1 \/ length es' = numstreams e).
  Hint Resolve unnest_rhs_length.

  Fact unnest_exp_numstreams : forall G e is_control es' eqs' st st',
      unnest_exp G is_control e st = (es', eqs', st') ->
      Forall (fun e => numstreams e = 1) es'.

  Corollary map_bind2_unnest_exp_numstreams : forall G es is_control es' eqs' st st',
      map_bind2 (unnest_exp G is_control) es st = (es', eqs', st') ->
      Forall (fun e => numstreams e = 1) (concat es').

  Corollary unnest_exps_numstreams : forall G es es' eqs' st st',
      unnest_exps G es st = (es', eqs', st') ->
      Forall (fun e => numstreams e = 1) es'.

Preservation of annotations

  Definition without_names (vars : list ann) : list (Op.type * clock) :=
    List.map (fun '(ty, (cl, _)) => (ty, cl)) vars.

  Fact without_names_length : forall anns,
      length (without_names anns) = length anns.

  Fact idents_for_anns_annots : forall anns ids st st',
      idents_for_anns anns st = (ids, st') ->
      annots (map (fun '(x, a) => Evar x a) ids) = anns.

  Fact idents_for_anns'_annots : forall anns ids st st',
      idents_for_anns' anns st = (ids, st') ->
      annots (map (fun '(x, a) => Evar x a) ids) = anns.

  Fact unnest_merge_annot : forall ckid ets efs tys ck,
      length ets = length tys ->
      length efs = length tys ->
      Forall2 (fun ty e => annot e = [(ty, ck)]) tys (unnest_merge ckid ets efs tys ck).

  Fact unnest_ite_annot : forall e ets efs tys ck,
      length ets = length tys ->
      length efs = length tys ->
      Forall2 (fun ty e => annot e = [(ty, ck)]) tys (unnest_ite e ets efs tys ck).

  Fact unnest_noops_exps_annots : forall cks es es' eqs' st st',
      length cks = length es ->
      Forall (fun e => numstreams e = 1) es ->
      unnest_noops_exps cks es st = (es', eqs', st') ->
      annots es' = annots es.

  Fact unnest_exp_annot : forall G e is_control es' eqs' st st',
      wl_exp G e ->
      unnest_exp G is_control e st = (es', eqs', st') ->
      annots es' = annot e.

  Corollary unnest_exp_annot_length : forall G e is_control es' eqs' st st',
      wl_exp G e ->
      unnest_exp G is_control e st = (es', eqs', st') ->
      length (annots es') = length (annot e).

  Fact map_bind2_unnest_exp_annots': forall G is_control es es' eqs' st st',
      Forall (wl_exp G) es ->
      map_bind2 (unnest_exp G is_control) es st = (es', eqs', st') ->
      Forall2 (fun es' e => annots es' = annot e) es' es.

  Corollary map_bind2_unnest_exp_annots'' : forall G is_control es es' eqs' st st',
      Forall (wl_exp G) es ->
      map_bind2 (unnest_exp G is_control) es st = (es', eqs', st') ->
      Forall2 (fun e ann => annot e = [ann]) (concat es') (annots es).

  Corollary map_bind2_unnest_exp_annots_length' :
    forall G is_control es es' eqs' st st',
      Forall (wl_exp G) es ->
      map_bind2 (unnest_exp G is_control) es st = (es', eqs', st') ->
      Forall2 (fun es' e => length (annots es') = length (annot e)) es' es.

  Fact map_bind2_unnest_exp_annots :
    forall G is_control es es' eqs' st st',
      Forall (wl_exp G) es ->
      map_bind2 (unnest_exp G is_control) es st = (es', eqs', st') ->
      annots (concat es') = annots es.

  Fact map_bind2_unnest_exp_annots_length :
    forall G is_control es es' eqs' st st',
      Forall (wl_exp G) es ->
      map_bind2 (unnest_exp G is_control) es st = (es', eqs', st') ->
      length (annots (concat es')) = length (annots es).

  Fact unnest_exps_annots : forall G es es' eqs' st st',
      Forall (wl_exp G) es ->
      unnest_exps G es st = (es', eqs', st') ->
      annots es' = annots es.

  Corollary unnest_exps_annots_length : forall G es es' eqs' st st',
      Forall (wl_exp G) es ->
      unnest_exps G es st = (es', eqs', st') ->
      length (annots es') = length (annots es).

  Fact unnest_fby_annot : forall anns e0s es,
      length e0s = length anns ->
      length es = length anns ->
      annots (unnest_fby e0s es anns) = anns.

  Fact unnest_arrow_annot : forall anns e0s es,
      length e0s = length anns ->
      length es = length anns ->
      annots (unnest_arrow e0s es anns) = anns.


  Fact unnest_fby_annot' : forall anns e0s es,
      length e0s = length anns ->
      length es = length anns ->
      Forall2 (fun e a => annot e = [a]) (unnest_fby e0s es anns) anns.

  Fact unnest_arrow_annot' : forall anns e0s es,
      length e0s = length anns ->
      length es = length anns ->
      Forall2 (fun e a => annot e = [a]) (unnest_arrow e0s es anns) anns.


  Fact unnest_rhs_annot : forall G e es' eqs' st st',
      wl_exp G e ->
      unnest_rhs G e st = (es', eqs', st') ->
      annots es' = annot e.

  Corollary unnest_rhs_annot_length : forall G e es' eqs' st st',
      wl_exp G e ->
      unnest_rhs G e st = (es', eqs', st') ->
      length (annots es') = length (annot e).

  Fact unnest_rhss_annots : forall G es es' eqs' st st',
      Forall (wl_exp G) es ->
      unnest_rhss G es st = (es', eqs', st') ->
      annots es' = annots es.

  Corollary unnest_rhss_annots_length : forall G es es' eqs' st st',
      Forall (wl_exp G) es ->
      unnest_rhss G es st = (es', eqs', st') ->
      length (annots es') = length (annots es).

Propagation of the variable permutation property

  Fact idents_for_anns_vars_perm : forall anns ids st st',
      idents_for_anns anns st = (ids, st') ->
      Permutation ((map fst ids)++(st_ids st)) (st_ids st').

  Fact idents_for_anns'_vars_perm : forall anns ids st st',
      idents_for_anns' anns st = (ids, st') ->
      Permutation ((map fst ids)++(st_ids st)) (st_ids st').

  Fact map_bind2_vars_perm {A B} : forall (k : A -> FreshAnn (B * list equation)) es es' eqs' st st',
      map_bind2 k es st = (es', eqs', st') ->
      Forall (fun e => forall es' eqs' st st',
                  k e st = (es', eqs', st') ->
                  Permutation ((vars_defined eqs')++(st_ids st)) (st_ids st')) es ->
      Permutation ((vars_defined (concat eqs'))++(st_ids st)) (st_ids st').

  Fact unnest_noops_exps_vars_perm : forall cks es es' eqs' st st',
      unnest_noops_exps cks es st = (es', eqs', st') ->
      Permutation (vars_defined eqs'++st_ids st) (st_ids st').

  Fact unnest_reset_vars_perm : forall k e es' eqs' st st',
      LiftO True (fun e => forall es' eqs' st st',
                   k e st = ((es', eqs'), st') ->
                   Permutation ((vars_defined eqs')++(st_ids st)) (st_ids st')) e ->
      unnest_reset k e st = ((es', eqs'), st') ->
      Permutation ((vars_defined eqs')++(st_ids st)) (st_ids st').

  Fact unnest_exp_vars_perm : forall G e is_control es' eqs' st st',
      wl_exp G e ->
      unnest_exp G is_control e st = ((es', eqs'), st') ->
      Permutation ((vars_defined eqs')++(st_ids st)) (st_ids st').

  Corollary unnest_exps_vars_perm : forall G es es' eqs' st st',
      Forall (wl_exp G) es ->
      unnest_exps G es st = ((es', eqs'), st') ->
      Permutation ((vars_defined eqs')++(st_ids st)) (st_ids st').

  Fact unnest_rhs_vars_perm : forall G e es' eqs' st st',
      wl_exp G e ->
      unnest_rhs G e st = ((es', eqs'), st') ->
      Permutation ((vars_defined eqs')++(st_ids st)) (st_ids st').

  Corollary unnest_rhss_vars_perm : forall G es es' eqs' st st',
      Forall (wl_exp G) es ->
      unnest_rhss G es st = ((es', eqs'), st') ->
      Permutation ((vars_defined eqs')++(st_ids st)) (st_ids st').

  Fact split_equation_vars_defined : forall xs es,
      length xs = length (annots es) ->
      vars_defined (split_equation (xs, es)) = vars_defined [(xs, es)].

  Corollary split_equations_vars_defined : forall eqs,
      Forall (fun '(xs, es) => length xs = length (annots es)) eqs ->
      vars_defined (flat_map split_equation eqs) = vars_defined eqs.

  Fact unnest_equation_vars_perm : forall G eq eqs' st st',
      wl_equation G eq ->
      unnest_equation G eq st = (eqs', st') ->
      Permutation ((vars_defined eqs')++(st_ids st)) ((vars_defined [eq])++(st_ids st')).

  Corollary unnest_equations_vars_perm : forall G eqs eqs' st st',
      Forall (wl_equation G) eqs ->
      unnest_equations G eqs st = (eqs', st') ->
      Permutation ((vars_defined eqs')++(st_ids st)) ((vars_defined eqs)++(st_ids st')).

Specification of an (almost) normalized node

  Inductive normalized_lexp : exp -> Prop :=
  | unnested_Econst : forall c, normalized_lexp (Econst c)
  | unnested_Evar : forall x ty cl, normalized_lexp (Evar x (ty, cl))
  | unnested_Eunop : forall op e1 ty cl,
      normalized_lexp e1 ->
      normalized_lexp (Eunop op e1 (ty, cl))
  | unnested_Ebinop : forall op e1 e2 ty cl,
      normalized_lexp e1 ->
      normalized_lexp e2 ->
      normalized_lexp (Ebinop op e1 e2 (ty, cl))
  | unnested_Ewhen : forall e x b ty cl,
      normalized_lexp e ->
      normalized_lexp (Ewhen [e] x b ([ty], cl)).

  Fixpoint noops_exp (ck: clock) (e : exp) : Prop :=
    match ck with
    | Cbase => True
    | Con ck' _ _ =>
      match e with
      | Econst _ | Evar _ _ => True
      | Ewhen [e'] _ _ _ => noops_exp ck' e'
      | _ => False
      end
    end.

  Inductive normalized_cexp : exp -> Prop :=
  | unnested_Emerge : forall x et ef ty cl,
      normalized_cexp et ->
      normalized_cexp ef ->
      normalized_cexp (Emerge x [et] [ef] ([ty], cl))
  | unnested_Eite : forall e et ef ty cl,
      normalized_lexp e ->
      normalized_cexp et ->
      normalized_cexp ef ->
      normalized_cexp (Eite e [et] [ef] ([ty], cl))
  | normalized_lexp_cexp : forall e,
      normalized_lexp e ->
      normalized_cexp e.

  Inductive unnested_equation G : equation -> Prop :=
  | unnested_eq_Eapp : forall xs f n es lann,
      Forall normalized_lexp es ->
      find_node f G = Some n ->
      Forall2 noops_exp (map (fun '(_, (_, ck)) => ck) n.(n_in)) es ->
      unnested_equation G (xs, [Eapp f es None lann])
  | unnested_eq_Eapp_reset : forall xs f n es x ty cl lann,
      Forall normalized_lexp es ->
      find_node f G = Some n ->
      Forall2 noops_exp (map (fun '(_, (_, ck)) => ck) n.(n_in)) es ->
      unnested_equation G (xs, [Eapp f es (Some (Evar x (ty, cl))) lann])
  | unnested_eq_Efby : forall x e0 e ann,
      normalized_lexp e0 ->
      normalized_lexp e ->
      unnested_equation G ([x], [Efby [e0] [e] [ann]])
  | unnested_eq_Earrow : forall x e0 e ann,
      normalized_lexp e0 ->
      normalized_lexp e ->
      unnested_equation G ([x], [Earrow [e0] [e] [ann]])
  | unnested_eq_cexp : forall x e,
      normalized_cexp e ->
      unnested_equation G ([x], [e]).

  Definition unnested_node G (n : node) :=
    Forall (unnested_equation G) (n_eqs n).

  Definition unnested_global G := ForallTail (fun n G => unnested_node G n) G.

  Hint Constructors normalized_lexp normalized_cexp unnested_equation.


  Fact normalized_lexp_numstreams : forall e,
      normalized_lexp e ->
      numstreams e = 1.

  Fact normalized_cexp_numstreams : forall e,
      normalized_cexp e ->
      numstreams e = 1.

After normalization, equations and expressions are unnested

  Fact normalized_lexp_hd_default : forall es,
      Forall normalized_lexp es ->
      normalized_lexp (hd_default es).

  Fact normalized_cexp_hd_default : forall es,
      Forall normalized_cexp es ->
      normalized_cexp (hd_default es).

  Fact map_bind2_normalized_lexp' {A A2} :
    forall (k : A -> FreshAnn ((list exp) * A2)) a es' a2s st st',
      map_bind2 k a st = (es', a2s, st') ->
      Forall (fun a => forall es' a2s st st',
                  k a st = (es', a2s, st') ->
                  Forall normalized_lexp es') a ->
      Forall normalized_lexp (concat es').

  Fact map_bind2_normalized_cexp' {A A2} :
    forall (k : A -> FreshAnn ((list exp) * A2)) a es' a2s st st',
      map_bind2 k a st = (es', a2s, st') ->
      Forall (fun a => forall es' a2s st st',
                  k a st = (es', a2s, st') ->
                  Forall normalized_cexp es') a ->
      Forall normalized_cexp (concat es').

  Hint Resolve in_combine_l in_combine_r.
  Hint Resolve normalized_lexp_hd_default normalized_cexp_hd_default.

  Lemma unnest_exp_normalized_lexp : forall G e es' eqs' st st',
      unnest_exp G false e st = (es', eqs', st') ->
      Forall normalized_lexp es'.
  Hint Resolve unnest_exp_normalized_lexp.

  Corollary map_bind2_normalized_lexp : forall G es es' eqs' st st',
      map_bind2 (unnest_exp G false) es st = (es', eqs', st') ->
      Forall normalized_lexp (concat es').
  Hint Resolve map_bind2_normalized_lexp.

  Corollary unnest_exps_normalized_lexp: forall G es es' eqs' st st',
      unnest_exps G es st = (es', eqs', st') ->
      Forall normalized_lexp es'.
  Hint Resolve unnest_exps_normalized_lexp.

  Fact unnest_reset_is_var : forall k e e' eqs' st st',
      unnest_reset k e st = (e', eqs', st') ->
      LiftO True (fun e => exists x ann, e = Evar x ann) e'.

  Fact unnest_reset_unnested_eq : forall G k e e' eqs' st st',
      LiftO True (fun e => forall es' eqs' st st',
                   k e st = (es', eqs', st') ->
                   Forall normalized_cexp es' /\ Forall (unnested_equation G) eqs') e ->
      unnest_reset k e st = (e', eqs', st') ->
      Forall (unnested_equation G) eqs'.

  Fact unnest_merge_normalized_cexp : forall x ets efs tys ck,
      Forall normalized_cexp ets ->
      Forall normalized_cexp efs ->
      Forall normalized_cexp (unnest_merge x ets efs tys ck).

  Fact unnest_ite_normalized_cexp : forall e ets efs tys ck,
      normalized_lexp e ->
      Forall normalized_cexp ets ->
      Forall normalized_cexp efs ->
      Forall normalized_cexp (unnest_ite e ets efs tys ck).

  Lemma unnest_exp_normalized_cexp : forall G e es' eqs' st st',
      unnest_exp G true e st = (es', eqs', st') ->
      Forall normalized_cexp es'.
  Hint Resolve unnest_exp_normalized_cexp.

  Corollary map_bind2_normalized_cexp : forall G es es' eqs' st st',
      map_bind2 (unnest_exp G true) es st = (es', eqs', st') ->
      Forall normalized_cexp (concat es').

  Fact map_bind2_unnested_eq {A A1} :
    forall G (k : A -> FreshAnn (A1 * (list equation))) a a1s eqs' st st',
      map_bind2 k a st = (a1s, eqs', st') ->
      Forall (fun a => forall a1s eqs' st st',
                  k a st = (a1s, eqs', st') ->
                  Forall (unnested_equation G) eqs') a ->
      Forall (unnested_equation G) (concat eqs').

  Lemma is_noops_exp_spec : forall ck e,
      is_noops_exp ck e = true <->
      noops_exp ck e.

  Lemma unnest_noops_exp_noops_exp : forall G es f n es' es'' eqs' eqs'' st st' st'',
      Forall (wl_exp G) es ->
      length (annots es) = length (n_in n) ->
      find_node f G = Some n ->
      map_bind2 (unnest_exp G false) es st = (es', eqs', st') ->
      unnest_noops_exps (find_node_incks G f) (concat es') st' = (es'', eqs'', st'') ->
      Forall normalized_lexp es'' /\
      Forall2 noops_exp (map (fun '(_, (_, ck)) => ck) (n_in n)) es''.

  Lemma unnest_noops_exp_unnested_eq : forall G es f n es' es'' eqs' eqs'' st st' st'',
      Forall (wl_exp G) es ->
      length (annots es) = length (n_in n) ->
      find_node f G = Some n ->
      map_bind2 (unnest_exp G false) es st = (es', eqs', st') ->
      unnest_noops_exps (find_node_incks G f) (concat es') st' = (es'', eqs'', st'') ->
      Forall (unnested_equation G) eqs''.

  Lemma unnest_exp_unnested_eq : forall G e is_control es' eqs' st st',
      wl_exp G e ->
      unnest_exp G is_control e st = (es', eqs', st') ->
      Forall (unnested_equation G) eqs'.
  Local Hint Resolve unnest_exp_unnested_eq.

  Corollary unnest_exps_unnested_eq : forall G es es' eqs' st st',
      Forall (wl_exp G) es ->
      unnest_exps G es st = (es', eqs', st') ->
      Forall (unnested_equation G) eqs'.
  Local Hint Resolve unnest_exps_unnested_eq.

  Inductive unnested_rhs G : exp -> Prop :=
  | unnested_rhs_Eapp : forall f n es lann,
      Forall normalized_lexp es ->
      find_node f G = Some n ->
      Forall2 noops_exp (map (fun '(_, (_, ck)) => ck) (n_in n)) es ->
      unnested_rhs G (Eapp f es None lann)
  | unnested_rhs_Eapp_reset : forall f n es x ty cl lann,
      Forall normalized_lexp es ->
      find_node f G = Some n ->
      Forall2 noops_exp (map (fun '(_, (_, ck)) => ck) (n_in n)) es ->
      unnested_rhs G (Eapp f es (Some (Evar x (ty, cl))) lann)
  | unnested_rhs_Efby : forall e0 e ann,
      normalized_lexp e0 ->
      normalized_lexp e ->
      unnested_rhs G (Efby [e0] [e] [ann])
  | unnested_rhs_Earrow : forall e0 e ann,
      normalized_lexp e0 ->
      normalized_lexp e ->
      unnested_rhs G (Earrow [e0] [e] [ann])
  | unnested_rhs_cexp : forall e,
      normalized_cexp e ->
      unnested_rhs G e.
  Hint Constructors unnested_rhs.

  Fact unnested_equation_unnested_rhs : forall G xs es,
      unnested_equation G (xs, es) ->
      Forall (unnested_rhs G) es.

  Fact unnest_rhs_unnested_rhs : forall G e es' eqs' st st',
      wl_exp G e ->
      unnest_rhs G e st = (es', eqs', st') ->
      Forall (unnested_rhs G) es'.

  Corollary unnest_rhss_unnested_rhs : forall G es es' eqs' st st',
      Forall (wl_exp G) es ->
      unnest_rhss G es st = (es', eqs', st') ->
      Forall (unnested_rhs G) es'.

  Fact unnest_rhs_unnested_eq : forall G e es' eqs' st st',
      wl_exp G e ->
      unnest_rhs G e st = (es', eqs', st') ->
      Forall (unnested_equation G) eqs'.
  Hint Resolve unnest_rhs_unnested_eq.

  Corollary unnest_rhss_unnested_eq : forall G es es' eqs' st st',
      Forall (wl_exp G) es ->
      unnest_rhss G es st = (es', eqs', st') ->
      Forall (unnested_equation G) eqs'.
  Hint Resolve unnest_rhss_unnested_eq.

  Lemma unnest_equation_unnested_eq : forall G eq eqs' st st',
      wl_equation G eq ->
      unnest_equation G eq st = (eqs', st') ->
      Forall (unnested_equation G) eqs'.

  Corollary unnest_equations_unnested_eq : forall G eqs eqs' st st',
      Forall (wl_equation G) eqs ->
      unnest_equations G eqs st = (eqs', st') ->
      Forall (unnested_equation G) eqs'.

No anonymous names in a unnested node

  Fact normalized_lexp_no_fresh : forall e,
      normalized_lexp e ->
      fresh_in e = [].

  Corollary normalized_lexps_no_fresh : forall es,
      Forall normalized_lexp es ->
      fresh_ins es = [].

  Fact normalized_cexp_no_fresh : forall e,
      normalized_cexp e ->
      fresh_in e = [].

  Corollary normalized_cexps_no_fresh : forall es,
      Forall normalized_cexp es ->
      fresh_ins es = [].

  Corollary unnest_exp_no_fresh : forall G e is_control es' eqs' st st',
      unnest_exp G is_control e st = (es', eqs', st') ->
      fresh_ins es' = [].

  Corollary unnest_exps_no_fresh : forall G es es' eqs' st st',
      unnest_exps G es st = (es', eqs', st') ->
      fresh_ins es' = [].

  Fact unnested_equation_no_anon_in_eq : forall G e,
      unnested_equation G e ->
      anon_in_eq e = [].

  Lemma unnested_equations_no_anon : forall G eqs,
      Forall (unnested_equation G) eqs ->
      anon_in_eqs eqs = [].

  Corollary unnest_equations_no_anon : forall G eqs eqs' st st',
      Forall (wl_equation G) eqs ->
      unnest_equations G eqs st = (eqs', st') ->
      anon_in_eqs eqs' = [].

Normalization of a full node

  Import Facts Tactics.

  Lemma norm1_not_in_elab_prefs :
    ~PS.In norm1 elab_prefs.

  Lemma AtomOrGensym_add : forall pref prefs xs,
      Forall (AtomOrGensym prefs) xs ->
      Forall (AtomOrGensym (PS.add pref prefs)) xs.

  Program Definition unnest_node G (n : node)
          (Hwl : wl_node G n)
          (Hpref : n_prefixes n = elab_prefs) : node :=
    let eqs := unnest_equations' G (n_eqs n) init_st in
    let nvars := (st_anns (snd (proj1_sig eqs))) in
    {| n_name := (n_name n);
       n_hasstate := (n_hasstate n);
       n_in := (n_in n);
       n_out := (n_out n);
       n_vars := (n_vars n)++nvars;
       n_prefixes := PS.add norm1 (n_prefixes n);
       n_eqs := fst (proj1_sig eqs);
       n_ingt0 := (n_ingt0 n);
       n_outgt0 := (n_outgt0 n);
    |}.

  Fixpoint unnest_global (G : global) :
    wl_global G ->
    Forall (fun n => n_prefixes n = elab_prefs) G ->
    global.

unnest_global produces a global with the correct prefixes

  Lemma unnest_global_prefixes : forall G G' Hwl Hprefs,
      unnest_global G Hwl Hprefs = G' ->
      Forall (fun n => n_prefixes n = PS.add norm1 elab_prefs) G'.

unnest_global produces an equivalent global

  Fact unnest_global_eq : forall G Hwt Hprefs,
      global_iface_eq G (unnest_global G Hwt Hprefs).

  Fact unnest_global_names : forall a G Hwt Hprefs,
      Forall (fun n => (n_name a <> n_name n)%type) G ->
      Forall (fun n => (n_name a <> n_name n)%type) (unnest_global G Hwt Hprefs).

After normalization, a global is unnested

  Lemma iface_eq_unnested_equation : forall G G' eq,
      global_iface_eq G G' ->
      unnested_equation G eq ->
      unnested_equation G' eq.

  Corollary iface_eq_unnested_node : forall G G' n,
      global_iface_eq G G' ->
      unnested_node G n ->
      unnested_node G' n.

  Lemma unnest_node_unnested_node : forall G n Hwl Hprefs,
      unnested_node G (unnest_node G n Hwl Hprefs).

  Lemma unnest_global_unnested_global : forall G Hwl Hprefs,
      unnested_global (unnest_global G Hwl Hprefs).

Additional properties

  Fact idents_for_anns'_anon_streams : forall anns ids st st',
      idents_for_anns' anns st = (ids, st') ->
      incl (anon_streams anns) (anon_streams (map snd ids)).

  Definition without_names' (vars : list (ident * ann)) : list (ident * (Op.type * clock)) :=
    List.map (fun '(id, (ty, (cl, _))) => (id, (ty, cl))) vars.

  Fact idents_for_anns'_anon_streams_incl : forall anns ids st st',
      idents_for_anns' anns st = (ids, st') ->
      incl (anon_streams anns) (without_names' ids).

  Fact unnested_equation_not_nil : forall G eq,
      unnested_equation G eq ->
      wl_equation G eq ->
      fst eq <> [].

fresh_ins appear in the state after normalisation

  Fact unnest_reset_fresh_incl : forall k e e' eqs' st st',
      LiftO True (fun e => forall es' eqs' st st',
                   k e st = (es', eqs', st') ->
                   incl (fresh_in e) (st_anns st')) e ->
      unnest_reset k e st = (e', eqs', st') ->
      LiftO True (fun e => incl (fresh_in e) (st_anns st')) e.

  Ltac solve_st_follows :=
    match goal with
    | |- incl (st_anns ?st1) (st_anns ?st2) =>
      eapply st_follows_incl
    | |- st_follows ?st ?st =>
      reflexivity
    | H : st_follows ?st1 ?st2 |- st_follows ?st1 _ =>
      etransitivity; [eapply H |]
    | H : fresh_ident _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply fresh_ident_st_follows in H; eauto | ]
    | H : reuse_ident _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply reuse_ident_st_follows in H; eauto | ]
    | H : idents_for_anns _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply idents_for_anns_st_follows in H; eauto | ]
    | H : idents_for_anns' _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply idents_for_anns'_st_follows in H; eauto | ]
    | H : unnest_reset _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_reset_st_follows' in H; eauto | ]
    | H : unnest_noops_exps _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_noops_exps_st_follows in H; eauto | ]
    | H : map_bind2 _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply map_bind2_st_follows in H; eauto; solve_forall | ]
    | H : unnest_exp _ _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_exp_st_follows in H; eauto |]
    | H : unnest_exps _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_exps_st_follows in H; eauto |]
    | H : unnest_rhs _ _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_rhs_st_follows in H; eauto |]
    | H : unnest_rhss _ _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_rhss_st_follows in H; eauto |]
    | H : unnest_equation _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_equation_st_follows in H; eauto |]
    | H: map_bind _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply map_bind_st_follows in H; eauto; solve_forall |]
    | H : unnest_equations _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_equations_st_follows in H; eauto |]
    | H : unnest_reset (unnest_exp _ _) _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_reset_st_follows in H; eauto |]
    end.

  Fact map_bind2_fresh_incl : forall G is_control es es' eqs' st st',
      Forall (fun e => forall es' eqs' st st',
                  unnest_exp G is_control e st = (es', eqs', st') ->
                  incl (fresh_in e) (st_anns st')) es ->
      map_bind2 (unnest_exp G is_control) es st = (es', eqs', st') ->
      incl (fresh_ins es) (st_anns st').

  Fact idents_for_anns'_fresh_incl : forall anns ids st st',
      idents_for_anns' anns st = (ids, st') ->
      incl (anon_streams anns) (st_anns st').

  Fact unnest_exp_fresh_incl : forall G e is_control es' eqs' st st',
      unnest_exp G is_control e st = (es', eqs', st') ->
      incl (fresh_in e) (st_anns st').

  Corollary map_bind2_unnest_exp_fresh_incl : forall G es is_control es' eqs' st st',
      map_bind2 (unnest_exp G is_control) es st = (es', eqs', st') ->
      incl (fresh_ins es) (st_anns st').

  Corollary unnest_exps_fresh_incl : forall G es es' eqs' st st',
      unnest_exps G es st = (es', eqs', st') ->
      incl (fresh_ins es) (st_anns st').

Preservation of clockof

  Fact unnest_exp_clockof : forall G e is_control es' eqs' st st',
      wl_exp G e ->
      unnest_exp G is_control e st = (es', eqs', st') ->
      clocksof es' = clockof e.
  Hint Resolve unnest_exp_clockof.
End UNNESTING.

Module UnnestingFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Op)
       (Syn : LSYNTAX Ids Op)
<: UNNESTING Ids Op OpAux Syn.
  Include UNNESTING Ids Op OpAux Syn.
End UnnestingFun.