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.
From Velus Require Import Lustre.SubClock.SubClock.

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

  Module Import SC := SubClockFun Ids Op OpAux Cks Senv Syn.

  Definition rename_in_clock := subclock_clock Cbase.
  Definition rename_in_exp := subclock_exp Cbase.
  Definition rename_in_equation := subclock_equation Cbase.

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_in_clock (Env.from_list (combine xs ys)) (rename_in_clock sub1 ck) = rename_in_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 ident, 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 ident, Y ident, 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 (ident * ann) * list block) :=
    match blk with
    | Beq eq => ret ([], [Beq (rename_in_equation sub eq)])
    | Breset blks er =>
        do (locs, blks') <- mmap2 (inlinelocal_block sub) blks;
        ret (concat locs, [Breset (concat blks') (rename_in_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, _, _)) => (rename_var sub' x, (ty, (rename_in_clock sub' ck)))) 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 (ident * ann) * 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').

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 rename_var_injective : forall sub x y,
      Env.In x sub ->
      Env.In y sub ->
      NoDup (map snd (Env.elements sub)) ->
      rename_var sub x = rename_var sub y ->
      x = y.

  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
                      (map (fun xtc => (fst xtc, ((fst (snd xtc)), snd (snd xtc), xH, None)))
                           (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.

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

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.