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

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

Remove Local Blocks

Module Type INLINELOCAL
       (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).

Rename some variables

  Section rename.
    Variable sub : Env.t ident.

    Definition rename_var (x : ident) :=
      or_default x (Env.find x sub).

    Fixpoint rename_clock (ck : clock) :=
      match ck with
      | Cbase => Cbase
      | Con ck' x t => Con (rename_clock ck') (rename_var x) t
      end.

    Definition rename_nclock (nck : nclock) :=
      (rename_clock (fst nck), option_map rename_var (snd nck)).

    Definition rename_ann {A} (ann : (A * clock)) :=
      (fst ann, rename_clock (snd ann)).

    Fixpoint rename_exp (e : exp) :=
      match e with
      | Econst _ | Eenum _ _ => e
      | Evar x ann => Evar (rename_var x) (rename_ann ann)
      | Elast x ann => Elast (rename_var x) (rename_ann ann)
      | Eunop op e1 ann => Eunop op (rename_exp e1) (rename_ann ann)
      | Ebinop op e1 e2 ann => Ebinop op (rename_exp e1) (rename_exp e2) (rename_ann ann)
      | Eextcall f es (tyout, ck) => Eextcall f (map rename_exp es) (tyout, rename_clock ck)
      | Efby e0s e1s anns => Efby (map rename_exp e0s) (map rename_exp e1s) (map rename_ann anns)
      | Earrow e0s e1s anns => Earrow (map rename_exp e0s) (map rename_exp e1s) (map rename_ann anns)
      | Ewhen es (x, tx) t ann => Ewhen (map rename_exp es) (rename_var x, tx) t (rename_ann ann)
      | Emerge (x, ty) es ann => Emerge (rename_var x, ty) (map (fun '(i, es) => (i, map rename_exp es)) es) (rename_ann ann)
      | Ecase e es d ann =>
        Ecase (rename_exp e) (map (fun '(i, es) => (i, map rename_exp es)) es) (option_map (map rename_exp) d) (rename_ann ann)
      | Eapp f es er ann => Eapp f (map rename_exp es) (map rename_exp er) (map rename_ann ann)
      end.

    Definition rename_equation '(xs, es) : equation :=
      (map rename_var xs, map rename_exp es).

Properties

    Lemma rename_ann_clock {A} : forall (ann : (A * clock)),
        snd (rename_ann ann) = rename_clock (snd ann).

    Corollary map_rename_ann_clock {A} : forall (anns : list (A * clock)),
        map snd (map rename_ann anns) = map rename_clock (map snd anns).

    Lemma map_rename_ann_type {A} : forall (anns : list (A * clock)),
        map fst (map rename_ann anns) = map fst anns.

  End rename.

  Section rename_clockof.

    Variable sub : Env.t ident.

    Lemma rename_exp_nclockof : forall e,
        nclockof (rename_exp sub e) = map (rename_nclock sub) (nclockof e).

    Corollary rename_exp_nclocksof : forall es,
        nclocksof (map (rename_exp sub) es) = map (rename_nclock sub) (nclocksof es).

    Corollary rename_exp_clockof : forall e,
        clockof (rename_exp sub e) = map (rename_clock sub) (clockof e).

    Corollary rename_exp_clocksof : forall es,
        clocksof (map (rename_exp sub) es) = map (rename_clock sub) (clocksof es).

  End rename_clockof.

  Section rename_typeof.

    Variable bck : clock.
    Variable sub : Env.t ident.

    Lemma rename_exp_typeof : forall e,
        typeof (rename_exp sub e) = typeof e.

    Corollary rename_exp_typesof : forall es,
        typesof (map (rename_exp sub) es) = typesof es.
  End rename_typeof.

  Section rename_empty.

    Fact rename_var_empty : forall x,
      rename_var (Env.empty _) x = x.

    Corollary rename_vars_empty : forall xs,
        map (rename_var (Env.empty _)) xs = xs.

  End rename_empty.

  Lemma rename_var_IsLast sub Γ Γ' : forall x,
      (forall x y, Env.find x sub = Some y -> IsLast Γ x -> IsLast Γ' y) ->
      (forall x, Env.find x sub = None -> IsLast Γ x -> IsLast Γ' x) ->
      IsLast Γ x ->
      IsLast Γ' (rename_var sub x).

More properties

  Fact not_in_union_rename2 : forall x sub ys zs,
      ~In x ys ->
      rename_var (Env.adds ys zs sub) x = rename_var sub x.

  Corollary not_in_union_map_rename2 : forall xs sub ys zs,
      Forall (fun x => ~In x ys) xs ->
      map (rename_var (Env.adds ys zs sub)) xs = map (rename_var sub) xs.

  Lemma disjoint_union_rename_var : forall (sub1: Env.t ident) xs ys x,
      (forall x, Env.In x sub1 -> ~In x xs) ->
      (forall x y, Env.MapsTo x y sub1 -> ~In y xs) ->
      rename_var (Env.from_list (combine xs ys)) (rename_var sub1 x) = rename_var (Env.adds xs ys sub1) x.

  Corollary disjoint_union_rename_in_clock : forall (sub1: Env.t ident) xs ys ck,
      (forall x, Env.In x sub1 -> ~In x xs) ->
      (forall x y, Env.MapsTo x y sub1 -> ~In y xs) ->
      rename_clock (Env.from_list (combine xs ys)) (rename_clock sub1 ck) = rename_clock (Env.adds xs ys sub1) ck.

Inlining of local blocks

  Module Fresh := Fresh.Fresh(Ids).
  Import Fresh Notations Facts Tactics.

  Record reuse_st := {
      fresh_st: fresh_st local unit;
      used: PS.t;
    }.

  Definition Reuse A := reuse_st -> (A * reuse_st).

  Definition reuse_ident (x : ident) : Reuse ident :=
    fun st =>
      if PS.mem x st.(used) then
        let (y, st') := fresh_ident (Some x) tt st.(fresh_st) in
        (y, {| fresh_st := st'; used := st.(used) |})
      else
        (x, {| fresh_st := st.(fresh_st); used := PS.add x st.(used) |}).

  Section ret.
    Context {A : Type}.
    Definition ret (x : A) : Reuse A := fun st => (x, st).

    Fact ret_spec : forall a st,
        ret a st = (a, st).
  End ret.

  Section bind.
    Context {A B : Type}.
    Definition bind (x : Reuse A) (k : A -> Reuse B) : Reuse B :=
      fun st => let '(a, st') := x st in k a st'.

    Lemma bind_spec : forall (x : Reuse A) (k : A -> Reuse B) st a' st'',
        (bind x k) st = (a', st'') <->
        exists a, exists st', (x st = (a, st') /\ k a st' = (a', st'')).
  End bind.

  Section bind2.
    Context {A1 A2 B : Type}.
    Definition bind2 (x : Reuse (A1 * A2)) (k : A1 -> A2 -> Reuse B) : Reuse B :=
      fun st => let '((a1, a2), st') := x st in k a1 a2 st'.

    Lemma bind2_spec : forall (x : Reuse (A1 * A2)) (k : A1 -> A2 -> Reuse B) st a' st'',
        (bind2 x k) st = (a', st'') <->
          exists a1, exists a2, exists st', (x st = ((a1, a2), st') /\ k a1 a2 st' = (a', st'')).
  End bind2.

  Definition st_In x (st : reuse_st) :=
    In x (st_ids (fresh_st st)) \/ PS.In x (used st).

  Definition st_valid (st : reuse_st) :=
    PS.For_all (AtomOrGensym switch_prefs) (used st).

  Definition st_follows (st1 st2 : reuse_st) :=
    st_follows (fresh_st st1) (fresh_st st2) /\ PS.Subset (used st1) (used st2).

  Global Instance st_follows_Reflexive : Reflexive st_follows.
  Global Instance st_follows_Transitive : Transitive st_follows.

  Lemma st_follows_In : forall st1 st2,
      st_follows st1 st2 ->
      forall x, st_In x st1 -> st_In x st2.

  Declare Scope reuse_monad_scope.
  Notation "'do' X <- A ; B" :=
    (bind A (fun X => B))
      (at level 200, X name, A at level 100, B at level 200): reuse_monad_scope.
  Notation "'do' ( X , Y ) <- A ; B" :=
    (bind2 A (fun X Y => B))
      (at level 200, X name, Y name, A at level 100, B at level 200): reuse_monad_scope.
  Open Scope reuse_monad_scope.

  Ltac monadInv :=
    simpl in *;
    match goal with
    | H : context c [ret _ _] |- _ =>
        rewrite ret_spec in H
    | H : (_, _) = (_, _) |- _ =>
        inv H
    | H : bind _ _ _ = (_, _) |- _ =>
        apply bind_spec in H; destruct H as [? [? [? ?]]]; simpl in *
    | H : bind2 _ _ _ = (_, _) |- _ =>
        apply bind2_spec in H; destruct H as [? [? [? [? ?]]]]; simpl in *
    | |- context c [ret _ _] =>
        rewrite ret_spec
    | |- bind _ _ _ = (_, _) =>
        rewrite bind_spec; repeat esplit
    | |- bind2 _ _ _ = (_, _) =>
        rewrite bind2_spec; repeat esplit
    end.

  Section mmap.
    Context {A B : Type}.
    Variable k : A -> Reuse B.
    Fixpoint mmap a :=
      match a with
      | nil => ret nil
      | hd::tl => do a1 <- k hd;
                do a1s <- mmap tl;
                ret (a1::a1s)
      end.

    Fact mmap_values : forall a st a1s st',
        mmap a st = (a1s, st') ->
        Forall2 (fun a a1 => exists st'', exists st''', k a st'' = (a1, st''')) a a1s.

    Fact mmap_st_valid : forall a a1s st st',
        mmap a st = (a1s, st') ->
        Forall (fun a => forall a1 st st', k a st = (a1, st') -> st_valid st -> st_valid st') a ->
        st_valid st ->
        st_valid st'.

    Fact mmap_st_follows : forall a a1s st st',
        mmap a st = (a1s, st') ->
        Forall (fun a => forall a1 st st', k a st = (a1, st') -> st_follows st st') a ->
        st_follows st st'.

    Fact mmap_values_follows : forall a st a1s st',
        (forall a a1 st st', k a st = (a1, st') -> st_follows st st') ->
        mmap a st = (a1s, st') ->
        Forall2 (fun a a1 =>
                   exists st'' st''',
                     st_follows st st''
                     /\ st_follows st''' st'
                     /\ k a st'' = (a1, st''')) a a1s.

    Fact mmap_values' : forall a st a1s st',
        Forall (fun a => forall a1 st st', k a st = (a1, st') -> st_valid st -> st_valid st') a ->
        (forall a a1 st st', k a st = (a1, st') -> st_follows st st') ->
        mmap a st = (a1s, st') ->
        st_valid st ->
        Forall2 (fun a a1 =>
                   exists st'' st''',
                     st_valid st''
                     /\ st_follows st st''
                     /\ st_follows st''' st'
                     /\ k a st'' = (a1, st''')) a a1s.
  End mmap.

  Section mmap2.
    Context {A A1 A2 : Type}.
    Variable k : A -> Reuse (A1 * A2).
    Fixpoint mmap2 (a : list A) : Reuse (list A1 * list A2) :=
      match a with
      | nil => ret (nil, nil)
      | hd::tl => do (a1, a2) <- k hd;
                do (a1s, a2s) <- mmap2 tl;
                ret (a1::a1s, a2::a2s)
      end.

    Fact mmap2_values : forall a st a1s a2s st',
        mmap2 a st = (a1s, a2s, st') ->
        Forall3 (fun a a1 a2 => exists st'', exists st''', k a st'' = (a1, a2, st''')) a a1s a2s.

    Fact mmap2_st_valid : forall a a1s a2s st st',
        mmap2 a st = (a1s, a2s, st') ->
        Forall (fun a => forall a1 a2 st st', k a st = (a1, a2, st') -> st_valid st -> st_valid st') a ->
        st_valid st ->
        st_valid st'.

    Fact mmap2_st_follows : forall a a1s a2s st st',
        mmap2 a st = (a1s, a2s, st') ->
        Forall (fun a => forall a1 a2 st st', k a st = (a1, a2, st') -> st_follows st st') a ->
        st_follows st st'.

    Fact mmap2_values_follows : forall a st a1s a2s st',
        (forall a a1 a2 st st', k a st = (a1, a2, st') -> st_follows st st') ->
        mmap2 a st = (a1s, a2s, st') ->
        Forall3 (fun a a1 a2 =>
                   exists st'' st''',
                     st_follows st st''
                     /\ st_follows st''' st'
                     /\ k a st'' = (a1, a2, st''')) a a1s a2s.

    Fact mmap2_values' : forall a st a1s a2s st',
        Forall (fun a => forall a1 a2 st st', k a st = (a1, a2, st') -> st_valid st -> st_valid st') a ->
        (forall a a1 a2 st st', k a st = (a1, a2, st') -> st_follows st st') ->
        mmap2 a st = (a1s, a2s, st') ->
        st_valid st ->
        Forall3 (fun a a1 a2 =>
                   exists st'' st''',
                     st_valid st''
                     /\ st_follows st st''
                     /\ st_follows st''' st'
                     /\ k a st'' = (a1, a2, st''')) a a1s a2s.
  End mmap2.

  Fixpoint inlinelocal_block sub (blk : block) : Reuse (list decl * list block) :=
    match blk with
    | Beq eq => ret ([], [Beq (rename_equation sub eq)])
    | Blast x e => ret ([], [Blast (rename_var sub x) (rename_exp sub e)])
    | Breset blks er =>
        do (locs, blks') <- mmap2 (inlinelocal_block sub) blks;
        ret (concat locs, [Breset (concat blks') (rename_exp sub er)])
    | Blocal (Scope locs blks) =>
        let xs := map fst locs in
        do newlocs <- mmap reuse_ident xs;
        let sub' := Env.adds xs newlocs sub in
        let locs' := map (fun '(x, (ty, ck, cx, clx)) => (rename_var sub' x, (ty, (rename_clock sub' ck), cx, clx))) locs in
        do (locs1, blks') <- mmap2 (inlinelocal_block sub') blks;
        ret (locs'++concat locs1, concat blks')
    | _ => ret ([], [blk])
    end.

Wellformedness properties

VarsDefinedComp

  Import Permutation.

  Fact mmap_vars_perm : forall (f : _ -> block -> Reuse (list decl * list block)) blks sub locs' blks' xs st st',
      Forall
        (fun blk => forall sub locs' blks' xs st st',
             noswitch_block blk ->
             VarsDefinedComp blk xs ->
             NoDupLocals (map fst (Env.elements sub) ++ xs) blk ->
             f sub blk st = (locs', blks', st') ->
             exists ys, Forall2 VarsDefinedComp blks' ys /\ Permutation (concat ys) (map (rename_var sub) xs ++ map fst locs')) blks ->
      Forall noswitch_block blks ->
      Forall2 VarsDefinedComp blks xs ->
      Forall (NoDupLocals (map fst (Env.elements sub) ++ concat xs)) blks ->
      mmap2 (f sub) blks st = (locs', blks', st') ->
      exists ys, Forall2 VarsDefinedComp (concat blks') ys /\ Permutation (concat ys) (map (rename_var sub) (concat xs) ++ map fst (concat locs')).

  Lemma inlinelocal_block_vars_perm : forall blk sub locs' blks' xs st st',
      noswitch_block blk ->
      VarsDefinedComp blk xs ->
      NoDupLocals (map fst (Env.elements sub) ++ xs) blk ->
      inlinelocal_block sub blk st = (locs', blks', st') ->
      exists ys, Forall2 VarsDefinedComp blks' ys /\ Permutation (concat ys) (map (rename_var sub) xs ++ map fst locs').

LastsDefined

  Fact mmap_lasts_perm : forall (f : _ -> block -> Reuse (list decl * list block)) blks sub locs' blks' xs st st',
      Forall
        (fun blk => forall sub locs' blks' xs st st',
             noswitch_block blk ->
             LastsDefined blk xs ->
             NoDupLocals (map fst (Env.elements sub) ++ xs) blk ->
             f sub blk st = (locs', blks', st') ->
             exists ys, Forall2 LastsDefined blks' ys /\ Permutation (concat ys) (map (rename_var sub) xs ++ lasts_of_decls locs')) blks ->
      Forall noswitch_block blks ->
      Forall2 LastsDefined blks xs ->
      Forall (NoDupLocals (map fst (Env.elements sub) ++ concat xs)) blks ->
      mmap2 (f sub) blks st = (locs', blks', st') ->
      exists ys, Forall2 LastsDefined (concat blks') ys /\ Permutation (concat ys) (map (rename_var sub) (concat xs) ++ lasts_of_decls (concat locs')).

  Lemma inlinelocal_block_lasts_perm : forall blk sub locs' blks' xs st st',
      noswitch_block blk ->
      LastsDefined blk xs ->
      NoDupLocals (map fst (Env.elements sub) ++ xs) blk ->
      inlinelocal_block sub blk st = (locs', blks', st') ->
      exists ys, Forall2 LastsDefined blks' ys /\ Permutation (concat ys) (map (rename_var sub) xs ++ lasts_of_decls locs').

st_valid

  Lemma reuse_ident_st_valid : forall x y st st',
      AtomOrGensym switch_prefs x ->
      reuse_ident x st = (y, st') ->
      st_valid st ->
      st_valid st'.

  Corollary reuse_idents_st_valid : forall locs locs' st st',
      Forall (AtomOrGensym switch_prefs) locs ->
      mmap reuse_ident locs st = (locs', st') ->
      st_valid st ->
      st_valid st'.

  Lemma inlinelocal_block_st_valid : forall blk sub locs' blks' st st',
      GoodLocals switch_prefs blk ->
      inlinelocal_block sub blk st = (locs', blks', st') ->
      st_valid st ->
      st_valid st'.

st_follows

  Lemma reuse_ident_st_follows : forall x y st st',
      reuse_ident x st = (y, st') ->
      st_follows st st'.

  Lemma inlinelocal_block_st_follows : forall blk sub locs' blks' st st',
      inlinelocal_block sub blk st = (locs', blks', st') ->
      st_follows st st'.

GoodLocals

  Lemma inlinelocal_block_GoodLocals : forall blk sub blks' locs' st st',
      noswitch_block blk ->
      inlinelocal_block sub blk st = (locs', blks', st') ->
      Forall (GoodLocals local_prefs) blks'.

  Lemma reuse_idents_find {A} : forall (locs: list (ident * A)) locs' st st' sub x,
      NoDupMembers locs ->
      mmap reuse_ident (map fst locs) st = (locs', st') ->
      InMembers x locs ->
      exists st st' y,
        reuse_ident x st = (y, st')
        /\ Env.find x (Env.adds (map fst locs) locs' sub) = Some y.

  Lemma reuse_idents_find_follows {A} : forall (locs: list (ident * A)) locs' st st' x sub,
      NoDupMembers locs ->
      mmap reuse_ident (map fst locs) st = (locs', st') ->
      InMembers x locs ->
      exists st1 st1' y,
        st_follows st st1
        /\ st_follows st1' st'
        /\ reuse_ident x st1 = (y, st1')
        /\ Env.find x (Env.adds (map fst locs) locs' sub) = Some y.

  Lemma reuse_idents_find' {A} : forall (locs: list (ident * A)) locs' st st' x sub,
      NoDupMembers locs ->
      Forall (AtomOrGensym switch_prefs) (map fst locs) ->
      mmap reuse_ident (map fst locs) st = (locs', st') ->
      st_valid st ->
      InMembers x locs ->
      exists st1 st1' y,
        st_valid st1
        /\ st_follows st st1
        /\ st_follows st1' st'
        /\ reuse_ident x st1 = (y, st1')
        /\ Env.find x (Env.adds (map fst locs) locs' sub) = Some y.

  Lemma inlinelocal_block_AtomOrGensym : forall blk Γ sub blks' locs' st st',
      NoDupLocals Γ blk ->
      GoodLocals switch_prefs blk ->
      inlinelocal_block sub blk st = (locs', blks', st') ->
      Forall (fun '(x, _) => AtomOrGensym local_prefs x) locs'.

NoDupLocals

  Lemma inlinelocal_block_NoDupLocals xs : forall blk sub locs' blks' st st',
      noswitch_block blk ->
      inlinelocal_block sub blk st = (locs', blks', st') ->
      Forall (NoDupLocals xs) blks'.

  Lemma local_not_in_switch_prefs :
    ~PS.In local switch_prefs.

  Lemma reuse_ident_In : forall x y st st',
      reuse_ident x st = (y, st') ->
      PS.In x (used st').

  Corollary reuse_idents_In : forall locs locs' st st',
    mmap reuse_ident locs st = (locs', st') ->
    Forall (fun x => PS.In x (used st')) locs.

  Lemma reuse_ident_st_In : forall x y st st',
      reuse_ident x st = (y, st') ->
      st_In y st'.

  Corollary reuse_idents_st_In : forall locs locs' st st',
    mmap reuse_ident locs st = (locs', st') ->
    Forall (fun x => st_In x st') locs'.

  Lemma inlinelocal_block_st_In : forall blk Γ sub blks' locs' st st',
      NoDupLocals Γ blk ->
      inlinelocal_block sub blk st = (locs', blks', st') ->
      Forall (fun '(x, _) => st_In x st') locs'.

  Lemma reuse_ident_st_nIn : forall x y st st',
      AtomOrGensym switch_prefs x ->
      st_valid st ->
      reuse_ident x st = (y, st') ->
      ~st_In y st.

  Corollary reuse_idents_st_nIn : forall locs locs' st st',
      Forall (AtomOrGensym switch_prefs) locs ->
      st_valid st ->
      mmap reuse_ident locs st = (locs', st') ->
      Forall (fun y => ~st_In y st) locs'.

  Lemma inlinelocal_block_st_nIn : forall blk Γ sub blks' locs' st st',
      NoDupLocals Γ blk ->
      GoodLocals switch_prefs blk ->
      st_valid st ->
      inlinelocal_block sub blk st = (locs', blks', st') ->
      Forall (fun '(x, _) => ~ (st_In x st)) locs'.

  Corollary inlinelocal_blocks_st_nIn : forall blks Γ sub blks' locs' st st',
      Forall (NoDupLocals Γ) blks ->
      Forall (GoodLocals switch_prefs) blks ->
      st_valid st ->
      mmap2 (inlinelocal_block sub) blks st = (locs', blks', st') ->
      Forall (fun '(x, _) => ~ (st_In x st)) (concat locs').

  Corollary inlinelocal_block_nIn : forall blk sub xs locs' blks' st st',
      Forall (fun x => PS.In x (used st)) xs ->
      NoDupLocals xs blk ->
      GoodLocals switch_prefs blk ->
      st_valid st ->
      inlinelocal_block sub blk st = (locs', blks', st') ->
      Forall (fun '(x, _) => ~In x xs) locs'.

  Lemma mmap_inlinelocal_block_NoDupMembers : forall blks Γ sub locs' blks' st st',
      Forall
        (fun blk =>
           forall Γ sub locs' blks' st st',
             NoDupLocals Γ blk ->
             GoodLocals switch_prefs blk ->
             st_valid st ->
             inlinelocal_block sub blk st = (locs', blks', st') ->
             NoDupMembers locs') blks ->
      Forall (NoDupLocals Γ) blks ->
      Forall (GoodLocals switch_prefs) blks ->
      st_valid st ->
      mmap2 (inlinelocal_block sub) blks st = (locs', blks', st') ->
      NoDupMembers (concat locs').

  Lemma reuse_idents_rename {A} sub : forall (locs : list (ident * A)) locs' st st',
      NoDupMembers locs ->
      mmap reuse_ident (map fst locs) st = (locs', st') ->
      map (rename_var (Env.adds (map fst locs) locs' sub)) (map fst locs) = locs'.

  Lemma reuse_idents_NoDup {A} : forall (locs : list (ident * A)) locs' st st',
      Forall (AtomOrGensym switch_prefs) (map fst locs) ->
      st_valid st ->
      mmap reuse_ident (map fst locs) st = (locs', st') ->
      NoDup locs'.

  Lemma inlinelocal_block_NoDupMembers : forall blk Γ sub locs' blks' st st',
      NoDupLocals Γ blk ->
      GoodLocals switch_prefs blk ->
      st_valid st ->
      inlinelocal_block sub blk st = (locs', blks', st') ->
      NoDupMembers locs'.

No local block

  Lemma inlinelocal_block_nolocal : forall blk sub locs' blks' st st',
      noswitch_block blk ->
      inlinelocal_block sub blk st = (locs', blks', st') ->
      Forall nolocal_block blks'.

Transformation of node and program

  Program Definition inlinelocal_node (n: @node noswitch switch_prefs) : @node nolocal local_prefs :=
    let res := inlinelocal_block (Env.empty _)
                 (n_block n)
                 {| fresh_st := init_st; used := PSP.of_list (map fst (n_in n) ++ map fst (n_out n)) |} in
    {|
      n_name := (n_name n);
      n_hasstate := (n_hasstate n);
      n_in := (n_in n);
      n_out := (n_out n);
      n_block := Blocal (Scope (fst (fst res)) (snd (fst res)));
      n_ingt0 := (n_ingt0 n);
      n_outgt0 := (n_outgt0 n);
    |}.

  Global Program Instance inlinelocal_node_transform_unit: TransformUnit (@node noswitch switch_prefs) node :=
    { transform_unit := inlinelocal_node }.

  Global Program Instance inlinelocal_global_without_units : TransformProgramWithoutUnits (@global noswitch switch_prefs) (@global nolocal local_prefs) :=
    { transform_program_without_units := fun g => Global g.(types) g.(externs) [] }.

  Definition inlinelocal_global : @global noswitch switch_prefs -> @global nolocal local_prefs :=
    transform_units.

Equality of interfaces

  Lemma inlinelocal_global_iface_eq : forall G,
      global_iface_eq G (inlinelocal_global G).


  Definition senv_of_anns (locs' : list (ident * ann)) : static_env :=
    map (fun '(x, (ty, ck)) => (x, (Build_annotation ty ck xH None))) locs'.
  Global Hint Unfold senv_of_anns : list.

  Fact senv_of_anns_app : forall locs1 locs2,
      senv_of_anns (locs1 ++ locs2) = senv_of_anns locs1 ++ senv_of_anns locs2.

  Fact senv_of_anns_concat_incl Γ : forall locs locs',
      In locs locs' ->
      incl (Γ ++ senv_of_anns locs) (Γ ++ senv_of_anns (concat locs')).
  Global Hint Resolve senv_of_anns_concat_incl : senv.

  Fact senv_of_decls_concat_incl Γ : forall locs locs',
      In locs locs' ->
      incl (Γ ++ senv_of_decls locs) (Γ ++ senv_of_decls (concat locs')).
  Global Hint Resolve senv_of_decls_concat_incl : senv.

  Lemma reuse_ident_gensym : forall x y st st',
      reuse_ident x st = (y, st') ->
      y = x \/ exists n hint, y = gensym local hint n.

  Lemma reuse_idents_gensym {A} : forall (locs : list (ident * A)) locs' st st',
      mmap reuse_ident (map fst locs) st = (locs', st') ->
      Forall (fun x => InMembers x locs \/ exists n hint, x = gensym local hint n) locs'.

  Fact IsLast_sub1 : forall vars1 vars2 vars3 sub,
      (forall x, InMembers x vars1 -> ~InMembers x vars2) ->
      (forall x, Env.In x sub <-> InMembers x vars2) ->
      (forall x y, Env.find x sub = Some y -> IsLast vars2 x -> IsLast vars3 y) ->
      forall x y, Env.find x sub = Some y -> IsLast (vars1 ++ vars2) x -> IsLast (vars1 ++ vars3) y.

  Fact IsLast_sub2 : forall vars1 vars2 vars3 sub,
      (forall x, Env.In x sub <-> InMembers x vars2) ->
      (forall x y, Env.find x sub = Some y -> IsLast vars2 x -> IsLast vars3 y) ->
      forall x, Env.find x sub = None -> IsLast (vars1 ++ vars2) x -> IsLast (vars1 ++ vars3) x.

End INLINELOCAL.

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