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

From Coq Require Import Setoid Morphisms.

From Velus Require Import Common Environment.
From Velus Require Import CommonTyping.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import Lustre.StaticEnv.
From Velus Require Import Lustre.LSyntax.
From Velus Require Fresh.

Normalization procedure

Module Type UNNESTING
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (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).

  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 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 with norm.

  Ltac simpl_In :=
    CommonList.simpl_In;
    repeat
      match goal with
      | H : In (?x1, ?x2) (combine ?l1 ?l2) |- _ =>
          specialize (in_combine_l _ _ _ _ H) as ?; apply in_combine_r in H
      end.

  Global Hint Unfold typesof annots clocksof : list.

  Ltac simpl_list :=
    simpl in *;
    autounfold with list in *;
    match goal with
    | 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.

  Definition default_ann : ann := (OpAux.bool_velus_type, Cbase).


  Definition st_senv {pref} (st: fresh_st pref _) := senv_of_tyck (st_anns st).
  Global Hint Unfold st_senv senv_of_tyck : list.

  Lemma st_senv_senv_of_decls {pref} : forall (st : fresh_st pref _),
      st_senv st = @senv_of_decls exp (map (fun xtc => (fst xtc, ((fst (snd xtc)), snd (snd xtc), xH, None))) (st_anns st)).

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

  Definition hd_default (l : list exp) : exp :=
    hd (Eenum 0 OpAux.bool_velus_type) l.

  Fixpoint idents_for_anns (anns : list ann) : FreshAnn (list (ident * ann)) :=
    match anns with
    | [] => ret []
    | (ty, cl)::tl => do x <- fresh_ident None (ty, cl);
                    do xs <- idents_for_anns tl;
                    ret ((x, (ty, cl))::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.
  Global Hint Resolve idents_for_anns_length : norm.

  Fact idents_for_anns_st_anns: forall anns ids st st',
      idents_for_anns anns st = (ids, st') ->
      Permutation (st_anns st') (ids++st_anns st).

  Definition unnest_reset k (e : exp) : FreshAnn (exp * list equation) :=
      do (e', eqs1) <- k e;
      match hd_default e' with
      | Evar v ann => ret (Evar v ann, eqs1)
      | e => let '(ty, ck) := hd default_ann (annot e) in
            do x <- fresh_ident None (ty, ck);
            ret (Evar x (ty, ck), ([x], [e])::eqs1)
      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 e st = ((Evar v ann, eqs'), st'))
      \/ exists ty ck x st'', hd default_ann (annot (hd_default es')) = (ty, ck) /\
                        fresh_ident None (ty, ck) st' = (x, st'') /\
                        unnest_reset k e st = ((Evar x (ty, ck), ([x], [hd_default es'])::eqs'), st'').

  Ltac unnest_reset_spec :=
    match goal with
    | H:unnest_reset ?k ?e ?st = (?res, ?st') |- _ =>
      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
    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).

  Fixpoint unnest_merge ckid es tys ck :=
    match tys with
    | [] => []
    | ty::tys => (Emerge ckid (List.map (fun '(i, es) => (i, [hd_default es])) es) ([ty], ck))
                 ::(unnest_merge ckid (List.map (fun '(i, es) => (i, tl es)) es) tys ck)
    end.

  Fixpoint unnest_case e es d tys ck :=
    match tys with
    | [] => []
    | ty::tys => (Ecase e (List.map (fun '(i, es) => (i, [hd_default es])) es) (option_map (fun d => [hd_default d]) d) ([ty], ck))
                 ::(unnest_case e (List.map (fun '(i, es) => (i, tl es)) es) (option_map (@tl _) d) tys ck)
    end.

  Global Hint Unfold unnest_when unnest_merge unnest_case : norm.

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

  Definition find_node_incks (G: @global nolocal local_prefs) (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) := hd default_ann (annot e) in
    if is_noops_exp cki e then ret (e, [])
    else do x <- fresh_ident None (ty, ck);
         ret (Evar x (ty, ck), [([x], [e])]).

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

  Fixpoint mk_equations (xs : list ident) (es : list exp) :=
    match xs with
    | [] => []
    | x::xs => ([x], [hd_default es])::(mk_equations xs (tl es))
    end.

  Fixpoint unnest_exp G (is_control : bool) (e : exp) {struct e} : FreshAnn (list exp * list equation) :=
    let unnest_exps := fun es => do (es, eqs) <- mmap2 (unnest_exp G false) es; ret (concat es, concat eqs) in
    let unnest_controls := fun es => do (es, eqs) <- mmap2 (unnest_exp G true) es; ret (concat es, concat eqs) in
    let unnest_resets := fun es => do (es, eqs) <- mmap2 (unnest_reset (unnest_exp G true)) es; ret (es, concat eqs) in
    match e with
    | Econst _ | Eenum _ _ | Evar _ _ | Elast _ _ => ret ([e], [])
    | 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)
    | Eextcall f es (tyout, ck) =>
      do (es', eqs1) <- unnest_exps es;
      do x <- fresh_ident None (Tprimitive tyout, ck);
      ret ([Evar x (Tprimitive tyout, ck)], ([x], [Eextcall f es' (tyout, ck)])::eqs1)
    | 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,
           (mk_equations (map fst 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 '(x, ann) => Evar x ann) xs,
           (mk_equations (map fst xs) 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 es (tys, cl) =>
      do (es', eqs1) <- mmap2 (fun '(i, es) => do (es', eqs') <- mmap2 (unnest_exp G true) es;
                                           ret (i, concat es', concat eqs')) es;
      let merges := unnest_merge ckid es' tys cl in
      if is_control then
        ret (merges, concat eqs1)
      else
        do xs <- idents_for_anns (List.map (fun ty => (ty, cl)) tys);
        ret (List.map (fun '(id, ann) => Evar id ann) xs,
             (mk_equations (map fst xs) merges)++concat eqs1)
    | Ecase e es d (tys, ck) =>
      do (e', eqs0) <- unnest_exp G false e;
      do (es', eqs1) <- mmap2 (fun '(i, es) => do (es', eqs') <- mmap2 (unnest_exp G true) es;
                                           ret (i, concat es', concat eqs')) es;
      do (d', eqs2) <- or_default_with (ret (None, [])) (fun d => do (d', eqs') <- unnest_controls d; ret (Some d', eqs')) d;
      let cases := unnest_case (hd_default e') es' d' tys ck in
      if is_control then
        ret (cases, eqs0++concat 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,
             (mk_equations (map fst xs) cases)++eqs0++concat 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_resets 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) <- mmap2 (unnest_exp G false) es;
    ret (concat es, concat eqs).

  Definition unnest_rhs G (e : exp) : FreshAnn (list exp * list equation) :=
    let unnest_resets := fun es => do (es, eqs) <- mmap2 (unnest_reset (unnest_exp G true)) es; ret (es, concat eqs) in
    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_resets er;
      ret ([Eapp f es' er' anns], eqs1++eqs2++eqs3)
    | Eextcall f es ann =>
        do (es', eqs1) <- unnest_exps G es;
        ret ([Eextcall f es' ann], eqs1)
    | 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) <- mmap2 (unnest_rhs G) es; ret (concat es, concat eqs).

  Fixpoint combine_for_numstreams {B} (es : list exp) (vs : list B) :=
    match es with
    | [] => List.map (fun v => (hd_default es, [v])) vs
    | 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).

  Fixpoint unnest_block G (d : block) : FreshAnn (list block) :=
    match d with
    | Beq e =>
      do eqs' <- unnest_equation G e;
      ret (map Beq eqs')
    | Breset blocks er =>
      do blocks' <- mmap (unnest_block G) blocks;
      do (er', eqs') <- unnest_reset (unnest_exp G true) er;
      ret ((map (fun d => Breset [d] er') (concat blocks'))++map Beq eqs')
    | _ => ret [d]
    end.

  Definition unnest_blocks G (blocks : list block) : FreshAnn (list block) :=
    do blocks' <- mmap (unnest_block G) blocks;
    ret (concat blocks').

mk_equations properties

  Lemma mk_equations_map_fst : forall xs es,
      concat (map fst (mk_equations xs es)) = xs.

  Lemma mk_equations_In : forall v xs es,
      length xs = length es ->
      In v (mk_equations xs es) ->
      exists x e, v = ([x], [e]) /\ In x xs /\ In e es.

  Lemma mk_equations_Forall : forall P xs es,
      Forall2 (fun x e => P ([x], [e])) xs es ->
      Forall P (mk_equations xs es).

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'.
  Global Hint Resolve idents_for_anns_st_follows : norm.

  Corollary idents_for_anns_incl : forall anns ids st st',
      idents_for_anns anns st = (ids, st') ->
      incl 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',
      (forall res st st',
          k e st = (res, st') ->
          st_follows st st') ->
      unnest_reset k e st = (res, st') ->
      st_follows st st'.
  Global Hint Resolve unnest_reset_st_follows' : norm.

  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'.
  Global Hint Resolve unnest_noops_exp_st_follows : norm.

  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'.
  Global Hint Resolve unnest_noops_exps_st_follows : norm.

  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 with norm | ]
    | H : idents_for_anns _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply idents_for_anns_st_follows in H; eauto with norm | ]
    | H : unnest_reset _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_reset_st_follows' in H; eauto with norm | ]
    | H : unnest_noops_exps _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_noops_exps_st_follows in H; eauto with norm | ]
    | H : mmap2 _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply mmap2_st_follows in H; eauto with norm; simpl_Forall; eauto with norm | ]
    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'.
  Global Hint Resolve unnest_exp_st_follows : norm.

  Corollary 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'.

  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'.
  Global Hint Resolve unnest_rhs_st_follows : norm.

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

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

  Lemma unnest_block_st_follows : forall G bck res st st',
      unnest_block G bck st = (res, st') ->
      st_follows st st'.
  Global Hint Resolve unnest_block_st_follows : norm.

  Corollary unnest_blocks_st_follows : forall G blocks res st st',
      unnest_blocks G blocks st = (res, st') ->
      st_follows st st'.

Length of unnested expression

  Fact mmap2_unnest_exp_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' ->
      mmap2 (unnest_exp G is_control) es st = (es', eqs', st') ->
      length (concat es') = length (annots es).

  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 es tys nck,
      length (unnest_merge ckid es tys nck) = length tys.

  Fact unnest_case_length : forall e es d tys nck,
      length (unnest_case e es d tys nck) = length tys.

  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.
  Global Hint Resolve unnest_exp_length : norm.

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

  Corollary mmap2_mmap2_unnest_exp_length {A} : forall G is_control (es : list (A * list exp)) es' eqs' st st',
    Forall (fun es => Forall (wl_exp G) (snd es)) es ->
    mmap2 (fun '(i, es0) => do (es', eqs') <- mmap2 (unnest_exp G is_control) es0;
                         ret (i, concat es', concat eqs')) es st = (es', eqs', st') ->
    Forall2 (fun es es' => length (snd es') = length (annots (snd es))) es es'.

  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).
  Global Hint Resolve unnest_exps_length : norm.

  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).
  Global Hint Resolve unnest_rhs_length : norm.

  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 mmap2_unnest_exp_numstreams : forall G es is_control es' eqs' st st',
      mmap2 (unnest_exp G is_control) es st = (es', eqs', st') ->
      Forall (fun e => numstreams e = 1) (concat es').

  Corollary mmap2_mmap2_unnest_exp_numstreams {A} G : forall (es : list (A * _)) is_control es' eqs' st st',
      mmap2 (fun '(i, es) => bind2 (mmap2 (unnest_exp G is_control) es) (fun es' eqs' => ret (i, concat es', concat eqs'))) es st = (es', eqs', st') ->
      Forall (fun es => Forall (fun e => numstreams e = 1) (snd es)) 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

  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_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_merge_annot : forall ckid es tys ck,
      Forall2 (fun ty e => annot e = [(ty, ck)]) tys (unnest_merge ckid es tys ck).

  Fact unnest_case_annot : forall e es tys d ck,
      Forall2 (fun ty e => annot e = [(ty, ck)]) tys (unnest_case e es d 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 mmap2_unnest_exp_annots': forall G is_control es es' eqs' st st',
      Forall (wl_exp G) es ->
      mmap2 (unnest_exp G is_control) es st = (es', eqs', st') ->
      Forall2 (fun es' e => annots es' = annot e) es' es.

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

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

  Corollary mmap2_mmap2_unnest_exp_annots {A} : forall G is_control (es : list (A * _)) es' eqs' st st',
      Forall (fun es => Forall (wl_exp G) (snd es)) es ->
      mmap2 (fun '(i, es) => bind2 (mmap2 (unnest_exp G is_control) es) (fun es' eqs' => ret (i, concat es', concat eqs'))) es st = (es', eqs', st') ->
      Forall2 (fun es es' => annots (snd es') = annots (snd es)) es es'.

  Fact mmap2_unnest_exp_annots_length :
    forall G is_control es es' eqs' st st',
      Forall (wl_exp G) es ->
      mmap2 (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.

  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.

  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 mmap2_vars_perm {A B} : forall (k : A -> FreshAnn (B * list equation)) es es' eqs' st st',
      mmap2 k es st = (es', eqs', st') ->
      Forall (fun e => forall es' eqs' st st',
                  k e st = (es', eqs', st') ->
                  Permutation ((flat_map fst eqs')++(st_ids st)) (st_ids st')) es ->
      Permutation ((flat_map fst (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 (flat_map fst eqs'++st_ids st) (st_ids st').

  Fact unnest_reset_vars_perm : forall k e es' eqs' st st',
      (forall es' eqs' st st',
          k e st = ((es', eqs'), st') ->
          Permutation ((flat_map fst eqs')++(st_ids st)) (st_ids st')) ->
      unnest_reset k e st = ((es', eqs'), st') ->
      Permutation ((flat_map fst eqs')++(st_ids st)) (st_ids st').

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

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

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

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

  Fact split_equation_fst : forall xs es,
      flat_map fst (split_equation (xs, es)) = xs.

  Corollary split_equations_fst : forall eqs,
      flat_map fst (flat_map split_equation eqs) = flat_map fst eqs.

  Fact unnest_equation_vars_perm : forall G eq eqs' st st',
      unnest_equation G eq st = (eqs', st') ->
      Permutation (flat_map fst eqs'++st_ids st) (fst eq++st_ids st').

  Fact mmap_vars_perm {A} pref : forall (f : block -> Fresh pref (list block) A) blks blks' xs st st',
      Forall
        (fun blk => forall blks' xs st st',
             VarsDefinedComp blk xs -> f blk st = (blks', st') ->
             exists ys, Forall2 VarsDefinedComp blks' ys /\ Permutation (concat ys ++ st_ids st) (xs ++ st_ids st')) blks ->
      Forall2 VarsDefinedComp blks xs ->
      mmap f blks st = (blks', st') ->
      exists ys, Forall2 VarsDefinedComp (concat blks') ys /\ Permutation (concat ys ++ st_ids st) (concat xs ++ st_ids st').

  Lemma unnest_block_vars_perm : forall G blk blks' xs st st',
      VarsDefinedComp blk xs ->
      unnest_block G blk st = (blks', st') ->
      exists ys, Forall2 VarsDefinedComp blks' ys /\ Permutation (concat ys ++ st_ids st) (xs ++ st_ids st').

  Corollary unnest_blocks_vars_perm : forall G blks blks' xs st st',
      Forall2 VarsDefinedComp blks xs ->
      unnest_blocks G blks st = (blks', st') ->
      exists ys, Forall2 VarsDefinedComp blks' ys /\ Permutation (concat ys ++ st_ids st) (concat xs ++ st_ids st').

Specification of an (almost) normalized node

  Inductive normalized_lexp : exp -> Prop :=
  | normalized_Econst : forall c, normalized_lexp (Econst c)
  | normalized_Eenum : forall k ty, normalized_lexp (Eenum k ty)
  | normalized_Evar : forall x ty cl, normalized_lexp (Evar x (ty, cl))
  | normalized_Eunop : forall op e1 ty cl,
      normalized_lexp e1 ->
      normalized_lexp (Eunop op e1 (ty, cl))
  | normalized_Ebinop : forall op e1 e2 ty cl,
      normalized_lexp e1 ->
      normalized_lexp e2 ->
      normalized_lexp (Ebinop op e1 e2 (ty, cl))
  | normalized_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 _ | Eenum _ _ | Evar _ _ => True
      | Ewhen [e'] _ _ _ => noops_exp ck' e'
      | _ => False
      end
    end.

  Inductive normalized_cexp : exp -> Prop :=
  | normalized_Emerge : forall x es ty cl,
      Forall (fun es => exists e, (snd es) = [e] /\ normalized_cexp e) es ->
      normalized_cexp (Emerge x es ([ty], cl))
  | normalized_Ecase : forall e es d ty cl,
      normalized_lexp e ->
      Forall (fun es => exists e, (snd es) = [e] /\ normalized_cexp e) es ->
      (forall ds, d = Some ds -> exists d, ds = [d] /\ normalized_cexp d) ->
      normalized_cexp (Ecase e es d ([ty], cl))
  | normalized_lexp_cexp : forall e,
      normalized_lexp e ->
      normalized_cexp e.

  Inductive unnested_equation {PSyn prefs} (G: @global PSyn prefs) : equation -> Prop :=
  | unnested_eq_Eapp : forall xs f n es er lann,
      Forall normalized_lexp es ->
      find_node f G = Some n ->
      Forall2 noops_exp (map (fun '(_, (_, ck, _)) => ck) n.(n_in)) es ->
      Forall (fun e => exists x ann, e = Evar x ann) er ->
      unnested_equation G (xs, [Eapp f es er 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_Eextcall: forall x f es ann,
      Forall normalized_lexp es ->
      unnested_equation G ([x], [Eextcall f es ann])
  | unnested_eq_cexp : forall x e,
      normalized_cexp e ->
      unnested_equation G ([x], [e]).

  Inductive unnested_block {PSyn prefs} (G: @global PSyn prefs) : block -> Prop :=
  | unnested_Beq : forall eq,
      unnested_equation G eq ->
      unnested_block G (Beq eq)
  | unnested_Breset : forall block x ann,
      unnested_block G block ->
      unnested_block G (Breset [block] (Evar x ann)).

  Inductive unnested_node {PSyn1 PSyn2 prefs1 prefs2} (G: @global PSyn1 prefs1) : @node PSyn2 prefs2 -> Prop :=
  | unnested_Node : forall n locs blks,
      n_block n = Blocal (Scope locs blks) ->
      Forall (fun '(x, (_, _, _, o)) => o = None) locs ->
      Forall (unnested_block G) blks ->
      unnested_node G n.

  Definition unnested_global {PSyn prefs} (G: @global PSyn prefs) :=
    wt_program unnested_node G.

  Global Hint Constructors normalized_lexp normalized_cexp unnested_equation unnested_block : norm.

  Inductive unnested_rhs {PSyn prefs} (G: @global PSyn prefs) : exp -> Prop :=
  | unnested_rhs_Eapp : forall f n es er lann,
      Forall normalized_lexp es ->
      find_node f G = Some n ->
      Forall2 noops_exp (map (fun '(_, (_, ck, _)) => ck) (n_in n)) es ->
      Forall (fun e => exists x ann, e = Evar x ann) er ->
      unnested_rhs G (Eapp f es er 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_Eextcall : forall f es ann,
      Forall normalized_lexp es ->
      unnested_rhs G (Eextcall f es ann)
  | unnested_rhs_cexp : forall e,
      normalized_cexp e ->
      unnested_rhs G e.
  Global Hint Constructors unnested_rhs : norm.


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

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

er 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 mmap2_normalized_lexp' {A2} Γ :
    forall (k : exp -> FreshAnn ((list exp) * A2)) a es' a2s st st',
      Forall (wx_exp Γ) a ->
      mmap2 k a st = (es', a2s, st') ->
      Forall (fun a => forall es' a2s st st',
                  wx_exp Γ a ->
                  k a st = (es', a2s, st') ->
                  Forall normalized_lexp es') a ->
      Forall normalized_lexp (concat es').

  Fact mmap2_normalized_cexp' {A2} Γ :
    forall (k : _ -> FreshAnn (list exp * A2)) es es' a2s st st',
      Forall (wx_exp Γ) es ->
      mmap2 k es st = (es', a2s, st') ->
      Forall (fun e => forall es' a2s st st',
                  wx_exp Γ e ->
                  k e st = (es', a2s, st') ->
                  Forall normalized_cexp es') es ->
      Forall normalized_cexp (concat es').

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

  Local Hint Resolve in_combine_l in_combine_r : norm.
  Global Hint Resolve normalized_lexp_hd_default normalized_cexp_hd_default : norm.

  Lemma unnest_exp_normalized_lexp : forall G Γ e es' eqs' st st',
      (forall x, ~IsLast Γ x) ->
      wx_exp Γ e ->
      unnest_exp G false e st = (es', eqs', st') ->
      Forall normalized_lexp es'.
  Global Hint Resolve unnest_exp_normalized_lexp : norm.

  Corollary mmap2_normalized_lexp : forall G Γ es es' eqs' st st',
      (forall x, ~IsLast Γ x) ->
      Forall (wx_exp Γ) es ->
      mmap2 (unnest_exp G false) es st = (es', eqs', st') ->
      Forall normalized_lexp (concat es').
  Global Hint Resolve mmap2_normalized_lexp : norm.

  Corollary unnest_exps_normalized_lexp: forall G Γ es es' eqs' st st',
      (forall x, ~IsLast Γ x) ->
      Forall (wx_exp Γ) es ->
      unnest_exps G es st = (es', eqs', st') ->
      Forall normalized_lexp es'.
  Global Hint Resolve unnest_exps_normalized_lexp : norm.

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

  Corollary unnest_resets_is_var : forall k es es' eqs' st st',
      mmap2 (unnest_reset k) es st = (es', eqs', st') ->
      Forall (fun e => exists x ann, e = Evar x ann) es'.

  Lemma unnest_reset_unnested_eq {PSyn} : forall (G: @global PSyn local_prefs) k e es' eqs' st st',
      (forall es' eqs' st st',
          k e st = (es', eqs', st') ->
          Forall (unnested_rhs G) es' /\ Forall (unnested_equation G) eqs') ->
      unnest_reset k e st = (es', eqs', st') ->
      Forall (unnested_equation G) eqs'.

  Corollary unnest_resets_unnested_eq {PSyn} : forall (G: @global PSyn local_prefs) k es es' eqs' st st',
      Forall (fun e => forall es' eqs' st st',
                  k e st = (es', eqs', st') ->
                  Forall (unnested_rhs G) es' /\ Forall (unnested_equation G) eqs') es ->
      mmap2 (unnest_reset k) es st = (es', eqs', st') ->
      Forall (unnested_equation G) (concat eqs').

  Fact unnest_merge_normalized_cexp : forall x es tys ck,
      Forall (fun es => Forall normalized_cexp (snd es)) es ->
      Forall normalized_cexp (unnest_merge x es tys ck).

  Fact unnest_case_normalized_cexp : forall e es d tys ck,
      normalized_lexp e ->
      Forall (fun es => Forall normalized_cexp (snd es)) es ->
      LiftO True (Forall normalized_cexp) d ->
      Forall normalized_cexp (unnest_case e es d tys ck).

  Lemma unnest_exp_normalized_cexp : forall G Γ e es' eqs' st st',
      (forall x, ~IsLast Γ x) ->
      wx_exp Γ e ->
      unnest_exp G true e st = (es', eqs', st') ->
      Forall normalized_cexp es'.
  Global Hint Resolve unnest_exp_normalized_cexp : norm.

  Corollary mmap2_normalized_cexp : forall G Γ es es' eqs' st st',
      (forall x, ~IsLast Γ x) ->
      Forall (wx_exp Γ) es ->
      mmap2 (unnest_exp G true) es st = (es', eqs', st') ->
      Forall normalized_cexp (concat es').

  Corollary mmap2_normalized_cexps : forall G Γ (es : list (enumtag * list exp)) es' eqs' st st',
      (forall x, ~IsLast Γ x) ->
      Forall (fun es => Forall (wx_exp Γ) (snd es)) es ->
      mmap2 (fun '(i, es) => do (es', eqs') <- mmap2 (unnest_exp G true) es;
                          ret (i, concat es', concat eqs')) es st = (es', eqs', st') ->
      Forall (fun es => Forall normalized_cexp (snd es)) es'.

  Fact mmap2_unnested_eq {PSyn A A1} :
    forall (G: @global PSyn local_prefs) (k : A -> FreshAnn (A1 * (list equation))) a a1s eqs' st st',
      mmap2 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 x, ~IsLast Γ x) ->
      Forall (wl_exp G) es ->
      Forall (wx_exp Γ) es ->
      length (annots es) = length (n_in n) ->
      find_node f G = Some n ->
      mmap2 (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 x, ~IsLast Γ x) ->
      Forall (wl_exp G) es ->
      Forall (wx_exp Γ) es ->
      length (annots es) = length (n_in n) ->
      find_node f G = Some n ->
      mmap2 (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',
      (forall x, ~IsLast Γ x) ->
      wl_exp G e ->
      wx_exp Γ e ->
      unnest_exp G is_control e st = (es', eqs', st') ->
      Forall (unnested_equation G) eqs'.
  Global Hint Resolve unnest_exp_unnested_eq : norm.

  Corollary unnest_exps_unnested_eq : forall G Γ es es' eqs' st st',
      (forall x, ~IsLast Γ x) ->
      Forall (wl_exp G) es ->
      Forall (wx_exp Γ) es ->
      unnest_exps G es st = (es', eqs', st') ->
      Forall (unnested_equation G) eqs'.
  Global Hint Resolve unnest_exps_unnested_eq : norm.

  Fact unnest_rhs_unnested_rhs : forall G Γ e es' eqs' st st',
      (forall x, ~IsLast Γ x) ->
      wl_exp G e ->
      wx_exp Γ 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 x, ~IsLast Γ x) ->
      Forall (wl_exp G) es ->
      Forall (wx_exp Γ) 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',
      (forall x, ~IsLast Γ x) ->
      wl_exp G e ->
      wx_exp Γ e ->
      unnest_rhs G e st = (es', eqs', st') ->
      Forall (unnested_equation G) eqs'.
  Global Hint Resolve unnest_rhs_unnested_eq : norm.

  Corollary unnest_rhss_unnested_eq : forall G Γ es es' eqs' st st',
      (forall x, ~IsLast Γ x) ->
      Forall (wl_exp G) es ->
      Forall (wx_exp Γ) es ->
      unnest_rhss G es st = (es', eqs', st') ->
      Forall (unnested_equation G) eqs'.
  Global Hint Resolve unnest_rhss_unnested_eq : norm.

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

  Lemma unnest_block_unnested_block : forall G Γ blk blks' st st',
      (forall x, ~IsLast Γ x) ->
      wl_block G blk ->
      wx_block Γ blk ->
      nolocal_block blk ->
      unnest_block G blk st = (blks', st') ->
      Forall (unnested_block G) blks'.

  Corollary unnest_blocks_unnested_blocks : forall G Γ blks blks' st st',
      (forall x, ~IsLast Γ x) ->
      Forall (wl_block G) blks ->
      Forall (wx_block Γ) blks ->
      Forall nolocal_block blks ->
      unnest_blocks G blks st = (blks', st') ->
      Forall (unnested_block G) blks'.

  Lemma unnest_block_GoodLocals G : forall prefs blk blk' st st',
      GoodLocals prefs blk ->
      unnest_block G blk st = (blk', st') ->
      Forall (GoodLocals prefs) blk'.

  Corollary unnest_blocks_GoodLocals G : forall prefs blks blks' st st',
      Forall (GoodLocals prefs) blks ->
      unnest_blocks G blks st = (blks', st') ->
      Forall (GoodLocals prefs) blks'.

  Fact mmap_NoDupLocals {pref A} (f : block -> Fresh pref (list block) A) env : forall blks blks' st st',
      Forall (fun blk => forall blks' st st',
                  NoDupLocals env blk ->
                  f blk st = (blks', st') -> Forall (NoDupLocals env) blks') blks ->
      Forall (NoDupLocals env) blks ->
      mmap f blks st = (blks', st') ->
      Forall (NoDupLocals env) (concat blks').

  Lemma unnest_block_NoDupLocals G env : forall blk blks' st st',
      NoDupLocals env blk ->
      unnest_block G blk st = (blks', st') ->
      Forall (NoDupLocals env) blks'.

  Corollary unnest_blocks_NoDupLocals G env : forall blks blks' st st',
      Forall (NoDupLocals env) blks ->
      unnest_blocks G blks st = (blks', st') ->
      Forall (NoDupLocals env) blks'.

nolocal_block

  Lemma unnest_block_nolocal : forall G blk blks' st st',
      nolocal_block blk ->
      unnest_block G blk st = (blks', st') ->
      Forall nolocal_block blks'.

  Corollary unnest_blocks_nolocal : forall G blks blks' st st',
      Forall nolocal_block blks ->
      unnest_blocks G blks st = (blks', st') ->
      Forall nolocal_block blks'.

Normalization of a full node

  Import Facts Tactics.

  Lemma norm1_not_in_local_prefs :
    ~PS.In norm1 local_prefs.

  Program Definition unnest_node G (n : @node nolocal local_prefs) : @node nolocal norm1_prefs :=
    {| n_name := (n_name n);
       n_hasstate := (n_hasstate n);
       n_in := (n_in n);
       n_out := (n_out n);
       n_block := match (n_block n) with
                  | Blocal (Scope vars blks) =>
                    let res := unnest_blocks G blks init_st in
                    let nvars := st_anns (snd res) in
                    Blocal (Scope (vars++map (fun xtc => (fst xtc, ((fst (snd xtc)), snd (snd xtc), xH, None))) nvars) (fst res))
                  | blk => blk
                  end;
       n_ingt0 := (n_ingt0 n);
       n_outgt0 := (n_outgt0 n);
    |}.

  Fixpoint unnest_nodes enums externs nds :=
    match nds with
    | [] => []
    | hd::tl => (unnest_node (Global enums externs tl) hd) :: (unnest_nodes enums externs tl)
    end.

  Definition unnest_global G :=
    Global G.(types) G.(externs) (unnest_nodes G.(types) G.(externs) G.(nodes)).

unnest_global produces an equivalent global

  Fact unnest_nodes_eq : forall enums externs nds,
      global_iface_eq (Global enums externs nds)
                      (Global enums externs (unnest_nodes enums externs nds)).

  Corollary unnest_global_eq : forall G,
      global_iface_eq G (unnest_global G).

  Fact unnest_nodes_names {PSyn prefs} : forall (nd: @node PSyn prefs) enums externs nds,
      Forall (fun n => (n_name nd <> n_name n)%type) nds ->
      Forall (fun n => (n_name nd <> n_name n)%type) (unnest_nodes enums externs nds).

er normalization, a global is unnested

  Lemma iface_eq_unnested_equation {PSyn1 PSyn2 prefs1 prefs2} : forall (G: @global PSyn1 prefs1) (G': @global PSyn2 prefs2) eq,
      global_iface_eq G G' ->
      unnested_equation G eq ->
      unnested_equation G' eq.

  Lemma iface_eq_unnested_block {PSyn1 PSyn2 prefs1 prefs2} : forall (G: @global PSyn1 prefs1) (G': @global PSyn2 prefs2) d,
      global_iface_eq G G' ->
      unnested_block G d ->
      unnested_block G' d.

  Corollary iface_eq_unnested_node {P1 P2 P3 p1 p2 p3} : forall (G: @global P1 p1) (G': @global P2 p2) (n: @node P3 p3),
      global_iface_eq G G' ->
      unnested_node G n ->
      unnested_node G' n.

  Lemma unnest_node_unnested_node : forall G n,
      wl_node G n ->
      wx_node n ->
      unnested_node G (unnest_node G n).

  Lemma unnest_global_unnested_global : forall G,
      wl_global G ->
      wx_global G ->
      unnested_global (unnest_global G).

Additional properties

  Ltac solve_st_follows :=
    repeat inv_bind;
    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 : idents_for_anns _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply idents_for_anns_st_follows in H; eauto | ]
    | H : unnest_noops_exps _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_noops_exps_st_follows in H; eauto | ]
    | H : mmap2 _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply mmap2_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: mmap _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply mmap_st_follows in H; eauto; solve_forall |]
    | H : unnest_block _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_block_st_follows in H; eauto |]
    | H : unnest_blocks _ _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_blocks_st_follows in H; eauto |]
    | H : unnest_reset (unnest_exp _ _) _ ?st = _ |- st_follows ?st _ =>
      etransitivity; [ eapply unnest_reset_st_follows in H; eauto |]
    end.

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.
  Global Hint Resolve unnest_exp_clockof : norm.
End UNNESTING.

Module UnnestingFun
       (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)
<: UNNESTING Ids Op OpAux Cks Senv Syn.
  Include UNNESTING Ids Op OpAux Cks Senv Syn.
End UnnestingFun.