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

Remove Switches

Module Type CLOCKSWITCH
       (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 Import SC := SubClockFun Ids Op OpAux Cks Senv Syn.

Eliminating switches

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

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

  Section mmap2.
    Import Tactics Notations.
    Open Scope fresh_monad_scope.
    Context {A1 A2 B : Type}.
    Variable k : A1 -> A2 -> FreshAnn B.

    Fixpoint mmap2 a1 a2 :=
      match a1, a2 with
      | hd1::tl1, hd2::tl2 => do b <- k hd1 hd2;
                           do bs <- mmap2 tl1 tl2;
                           ret (b::bs)
      | _, _ => ret nil
      end.

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

    Fact mmap2_values : forall a1s a2s bs st st',
        length a1s = length a2s ->
        mmap2 a1s a2s st = (bs, st') ->
        Forall3 (fun a1 a2 b => exists st1 st2, k a1 a2 st1 = (b, st2)) a1s a2s bs.

    Fact mmap2_values' : forall a1s a2s bs st st',
        length a1s = length a2s ->
        (forall a1 a2 b st st', k a1 a2 st = (b, st') -> st_follows st st') ->
        mmap2 a1s a2s st = (bs, st') ->
        Forall3 (fun a1 a2 b => exists st1 st2, st_follows st st1 /\ k a1 a2 st1 = (b, st2)) a1s a2s bs.

  End mmap2.

  Definition cond_eq e tx bck : FreshAnn (ident * list (ident * (type * clock)) * list equation) :=
    match e with
    | Evar x (ty, ck) => ret (x, [], [])
    | _ =>
      do xc <- fresh_ident None (tx, bck);
      ret (xc, [(xc, (tx, bck))], [([xc], [e])])
    end.

  Definition new_idents bck xc tx k (ids : static_env) : FreshAnn _ :=
    mmap (fun '(x, ann) => do y <- fresh_ident (Some x) (ann.(typ), bck);
                        ret (x, y, (ann.(typ), Con bck xc (tx, k)))) ids.

  Definition when_free (x y : ident) ty ck xc tx k :=
    Beq ([y], [Ewhen [Evar x (ty, ck)] (xc, tx) k ([ty], Con ck xc (tx, k))]).

  Definition merge_defs sub (y : ident) ty ck xc tx (brs : list (enumtag * Env.t ident)) :=
    Beq ([rename_var sub y], [Emerge (xc, tx)
                                     (map (fun '(k, sub') => (k, [Evar (rename_var sub' y) (ty, Con ck xc (tx, k))])) brs)
                                     ([ty], ck)]).

  Section switch_scope.
    Context {A : Type}.
    Variable f_s : static_env -> A -> FreshAnn A.

    Definition switch_scope (env : static_env) bck sub scop : FreshAnn (scope A) :=
      let 'Scope locs blks := scop in
      let locs' := map (fun '(x, (ty, ck, cx, o)) => (x, (ty, subclock_clock bck sub ck, cx, o))) locs in
      let env := env++senv_of_decls locs in
      do blks' <- f_s env blks;
      ret (Scope locs' blks').

  End switch_scope.

  Fixpoint switch_block (env : static_env) bck sub blk : FreshAnn block :=
    match blk with
    | Beq eq => ret (Beq (subclock_equation bck sub eq))

    | Breset blks er =>
      do blks' <- mmap (switch_block env bck sub) blks;
      ret (Breset blks' (subclock_exp bck sub er))

    | Blocal s =>
        do s' <- switch_scope (fun env => mmap (switch_block env bck sub)) env bck sub s;
        ret (Blocal s')

    | Bswitch ec branches =>
      let vd := vars_defined (Bswitch ec branches) in

      let (defs, frees) := partition (fun '(x, _) => PS.mem x vd) env in

      let eck := hd Cbase (clockof ec) in
      let frees := List.filter (fun '(_, ann) => ann.(clo) ==b eck) frees in

      let ec' := subclock_exp bck sub ec in
      let tx := hd OpAux.bool_velus_type (typeof ec') in
      let bck := hd Cbase (clockof ec') in
      do (xcs, condeqs) <- cond_eq ec' tx bck;
      let (xc, xcs) := xcs in

      do xs' <- mmap (fun '(k, _) =>
                       do nfrees <- new_idents bck xc tx k frees;
                       do ndefs <- new_idents bck xc tx k defs;
                       let sub' := Env.from_list (map (fun '(x, y, _) => (x, y)) (nfrees++ndefs)) in
                       ret (k, sub', nfrees, ndefs)
                    ) branches;

      let env := map (fun '(x, ann) => (x, ann_with_clock ann Cbase)) (defs++frees) in
      do blks' <-
         mmap2 (fun '(k, Branch _ blks) '(_, sub', nfrees, ndefs) =>
                  let wheneqs := List.map (fun '(x, y, (ty, _)) => when_free (rename_var sub x) y ty bck xc tx k) nfrees in
                  do blks' <- mmap (switch_block env (Con bck xc (tx, k)) sub') blks;
                  ret (blks'++wheneqs)
               ) branches xs';
      let mergeeqs := map (fun '(x, ann) => merge_defs sub x ann.(typ) bck xc tx (map (fun '(k, sub, _, _) => (k, sub)) xs')) defs in
      let locs := flat_map (fun '(_, _, nfrees, ndefs) => (map (fun '(_, x, (ty, ck)) => (x, (ty, ck, xH, None))) (nfrees++ndefs))) xs' in
      ret (Blocal (Scope (List.map (fun '(xc, (ty, ck)) => (xc, (ty, ck, xH, None))) xcs++locs) (mergeeqs++concat blks'++map Beq condeqs)))

    | Bauto _ _ _ _ => ret blk
    end.

Some properties

  Lemma switch_not_in_auto_prefs :
    ~PS.In switch auto_prefs.

  Lemma new_idents_old : forall bck xc tx k ids nids st st',
      new_idents bck xc tx k ids st = (nids, st') ->
      map (fun '(x, _, _) => x) nids = map fst ids.

  Lemma rename_vars_idem : forall sub xs,
      (forall x, Env.In x sub -> ~In x xs) ->
      map (rename_var sub) xs = xs.

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

  Lemma switch_block_NoDupMembers_env {A B} pred1 pred2 : forall (env defs frees : list (A * B)),
      NoDupMembers env ->
      Partition pred1 env defs frees ->
      NoDupMembers (defs ++ filter pred2 frees).

VarsDefinedComp

  Import Permutation.

  Lemma new_idents_rename : forall bck xc tx k ids1 ids2 nids1 nids2 sub st1 st2 st3 st4,
      NoDupMembers (ids1++ids2) ->
      new_idents bck xc tx k ids1 st1 = (nids1, st2) ->
      new_idents bck xc tx k ids2 st3 = (nids2, st4) ->
      sub = Env.from_list (map (fun '(x, y, _) => (x, y)) (nids1++nids2)) ->
      map (fun '(_, x, _) => x) nids1 = map (rename_var sub) (map fst ids1) /\
      map (fun '(_, x, _) => x) nids2 = map (rename_var sub) (map fst ids2).

  Lemma incl_Permutation : forall (xs ys zs : list ident),
      incl xs (ys ++ zs) ->
      (forall x, In x xs <-> In x ys) ->
      NoDup xs ->
      NoDup (ys ++ zs) ->
      Permutation xs ys.

  Lemma cond_eq_VarsDefinedComp: forall e tx bck xc xcs eqs st st',
      cond_eq e tx bck st = ((xc, xcs), eqs, st') ->
      Forall2 VarsDefinedComp (map Beq eqs) (map (fun '(x, _) => [x]) xcs).

  Lemma switch_scope_VarsDefinedComp {A} P_na P_vd P_nd f_switch :
    forall xs env bck sub locs (blk: A) s' st st',
      incl xs (map fst env) ->
      (forall x, Env.In x sub -> InMembers x env) ->
      NoDupMembers env ->
      NoDup xs ->
      noauto_scope P_na (Scope locs blk) ->
      VarsDefinedCompScope P_vd (Scope locs blk) xs ->
      NoDupScope P_nd (map fst env) (Scope locs blk) ->
      switch_scope f_switch env bck sub (Scope locs blk) st = (s', st') ->
      (forall xs env blk' st st',
          incl xs (map fst env) ->
          (forall x, Env.In x sub -> InMembers x env) ->
          NoDupMembers env ->
          NoDup xs ->
          P_na blk ->
          P_vd blk xs ->
          P_nd (map fst env) blk ->
          f_switch env blk st = (blk', st') ->
          P_vd blk' (map (rename_var sub) xs)) ->
      VarsDefinedCompScope P_vd s' (map (rename_var sub) xs).

  Lemma switch_block_VarsDefinedComp : forall blk xs bck sub env blk' st st',
      incl xs (map fst env) ->
      (forall x, Env.In x sub -> InMembers x env) ->
      NoDupMembers env ->
      NoDup xs ->
      noauto_block blk ->
      VarsDefinedComp blk xs ->
      NoDupLocals (map fst env) blk ->
      switch_block env bck sub blk st = (blk', st') ->
      VarsDefinedComp blk' (map (rename_var sub) xs).

Preservation of st_follows

  Lemma cond_eq_st_follows : forall e tx bck xcs eqs' st st',
      cond_eq e tx bck st = (xcs, eqs', st') ->
      st_follows st st'.

  Lemma new_idents_st_follows : forall ck xc tx k ids nids st st',
      new_idents ck xc tx k ids st = (nids, st') ->
      st_follows st st'.

  Global Hint Resolve cond_eq_st_follows new_idents_st_follows : fresh.

  Lemma switch_block_st_follows : forall blk env bck sub blk' st st',
      switch_block env bck sub blk st = (blk', st') ->
      st_follows st st'.

  Corollary switch_scope_st_follows : forall blk env bck sub blk' st st',
      switch_scope (fun env => mmap (switch_block env bck sub)) env bck sub blk st = (blk', st') ->
      st_follows st st'.

NoDup

  Lemma cond_eq_NoDupMembers : forall e tx bck xc xcs eqs st st',
      cond_eq e tx bck st = (xc, xcs, eqs, st') ->
      NoDupMembers xcs.

  Lemma cond_eq_st_ids : forall e tx bck xc xcs eqs st st',
      cond_eq e tx bck st = (xc, xcs, eqs, st') ->
      Permutation (st_ids st') (st_ids st ++ map fst xcs).

  Corollary cond_eq_incl : forall e tx bck xc xcs eqs st st',
      cond_eq e tx bck st = (xc, xcs, eqs, st') ->
      incl (map fst xcs) (st_ids st').

  Lemma new_idents_st_ids : forall ck xc tx k ids nids st st',
      new_idents ck xc tx k ids st = (nids, st') ->
      Permutation (st_ids st') (st_ids st++map (fun '(_, x, _) => x) nids).

  Lemma new_idents_st_ids' {A} : forall (branches : list (_ * A)) ck xc tx frees defs nids st st',
      mmap
        (fun '(k, _) =>
           do nfrees <- new_idents ck xc tx k frees;
           do ndefs <- new_idents ck xc tx k defs;
           ret (k, Env.from_list (map (fun '(x, y2, _) => (x, y2)) (nfrees ++ ndefs)), nfrees, ndefs)) branches st = (nids, st') ->
      Permutation (st_ids st')
                  (st_ids st ++ map fst (flat_map (fun '(_, _, nfrees, ndefs) => map (fun '(_, x4, (ty, ck)) => (x4, (ty, ck, xH))) (nfrees ++ ndefs)) nids)).

  Fact switch_blocks_NoDupLocals' : forall blks xs env bck sub blks' st st',
      Forall
        (fun blk => forall xs env bck sub blk' st st',
             NoDup xs ->
             NoDupLocals xs blk ->
             Forall (fun x : ident => AtomOrGensym auto_prefs x \/ In x (st_ids st)) xs ->
             GoodLocals auto_prefs blk ->
             switch_block env bck sub blk st = (blk', st') ->
             NoDupLocals xs blk') blks ->
      NoDup xs ->
      Forall (NoDupLocals xs) blks ->
      Forall (fun x => AtomOrGensym auto_prefs x \/ In x (st_ids st)) xs ->
      Forall (GoodLocals auto_prefs) blks ->
      mmap (switch_block env bck sub) blks st = (blks', st') ->
      Forall (NoDupLocals xs) blks'.

  Lemma switch_scope_NoDupScope {A} P_nd P_good f_switch :
    forall locs (blk: A) xs env bck sub s' st st',
      NoDup xs ->
      NoDupScope P_nd xs (Scope locs blk) ->
      Forall (fun x => AtomOrGensym auto_prefs x \/ In x (st_ids st)) xs ->
      GoodLocalsScope P_good auto_prefs (Scope locs blk) ->
      switch_scope f_switch env bck sub (Scope locs blk) st = (s', st') ->
      (forall xs env blk' st st',
          NoDup xs ->
          P_nd xs blk ->
          Forall (fun x => AtomOrGensym auto_prefs x \/ In x (st_ids st)) xs ->
          P_good blk ->
          f_switch env blk st = (blk', st') ->
          P_nd xs blk') ->
      NoDupScope P_nd xs s'.

  Lemma switch_block_NoDupLocals : forall blk xs env bck sub blk' st st',
      NoDup xs ->
      NoDupLocals xs blk ->
      Forall (fun x => AtomOrGensym auto_prefs x \/ In x (st_ids st)) xs ->
      GoodLocals auto_prefs blk ->
      switch_block env bck sub blk st = (blk', st') ->
      NoDupLocals xs blk'.

GoodLocals

  Lemma new_idents_prefixed : forall bck xc tx k ids nids st st',
      new_idents bck xc tx k ids st = (nids, st') ->
      Forall (fun '(_, x, _) => exists n hint, x = gensym switch hint n) nids.

  Corollary new_idents_AtomOrGensym : forall bck xc tx k ids nids st st',
      new_idents bck xc tx k ids st = (nids, st') ->
      Forall (fun '(_, x, _) => AtomOrGensym switch_prefs x) nids.

  Lemma cond_eq_AtomOrGensym : forall e tx bck xc xcs eqs' st st',
      cond_eq e tx bck st = ((xc, xcs), eqs', st') ->
      Forall (AtomOrGensym switch_prefs) (map fst xcs).

  Lemma switch_scope_GoodLocals {A} P_good f_switch : forall locs (blk: A) env bck sub s' st st',
      (forall x y, Env.MapsTo x y sub -> AtomOrGensym switch_prefs y) ->
      GoodLocalsScope P_good switch_prefs (Scope locs blk) ->
      switch_scope f_switch env bck sub (Scope locs blk) st = (s', st') ->
      (forall env blk' st st',
          (forall x y, Env.MapsTo x y sub -> AtomOrGensym switch_prefs y) ->
          P_good blk -> f_switch env blk st = (blk', st') -> P_good blk') ->
      GoodLocalsScope P_good switch_prefs s'.

  Lemma switch_block_GoodLocals : forall blk env bck sub blk' st st',
      (forall x y, Env.MapsTo x y sub -> AtomOrGensym switch_prefs y) ->
      GoodLocals switch_prefs blk ->
      switch_block env bck sub blk st = (blk', st') ->
      GoodLocals switch_prefs blk'.

noswitch_block

  Lemma switch_noswitch : forall blk env bck sub blk' st st',
      noauto_block blk ->
      switch_block env bck sub blk st = (blk', st') ->
      noswitch_block blk'.

Transformation of a node and program

  Program Definition switch_node (n: @node noauto auto_prefs) : @node noswitch switch_prefs :=
    let res := switch_block (senv_of_ins (n_in n) ++ senv_of_decls (n_out n)) Cbase (@Env.empty _) (n_block n) init_st in
    {| n_name := n_name n;
       n_hasstate := n_hasstate n;
       n_in := n_in n;
       n_out := n_out n;
       n_block := fst res;
       n_ingt0 := n_ingt0 n;
       n_outgt0 := n_outgt0 n
    |}.

  Global Program Instance switch_node_transform_unit: TransformUnit node node :=
    { transform_unit := switch_node }.

  Global Program Instance switch_global_without_units : TransformProgramWithoutUnits (@global noauto auto_prefs) (@global noswitch switch_prefs) :=
    { transform_program_without_units := fun g => Global g.(types) g.(externs) [] }.

  Definition switch_global : @global noauto auto_prefs -> @global noswitch switch_prefs :=
    transform_units.

Equality of interfaces

  Lemma switch_global_iface_eq : forall G,
      global_iface_eq G (switch_global G).

Additional properties

  Lemma new_idents_In_inv : forall ck cx tx k ids nids st st' x y ck1 ty,
      new_idents ck cx tx k ids st = (nids, st') ->
      In (x, y, (ty, ck1)) nids ->
      exists ann, In (x, ann) ids /\ ann.(typ) = ty.

End CLOCKSWITCH.

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