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 State Machines

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

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

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

  Definition fresh_ident : FreshAnn _ := fresh_ident None (OpAux.bool_velus_type, Cbase).

  Fixpoint init_state_exp ty ck (ini : list (exp * enumtag)) oth : exp :=
    match ini with
    | [] => add_whens (Eenum oth ty) ty ck
    | (e, k)::ini =>
        Ecase (subclock_exp ck (@Env.empty _) e)
              [(OpAux.true_tag, [add_whens (Eenum k ty) ty ck]);
              (OpAux.false_tag, [init_state_exp ty ck ini oth])]
              None ([ty], ck)
    end.

  Fixpoint trans_exp ty (trans : list (exp * (enumtag * bool))) current : list exp :=
    match trans with
    | [] => [Eenum current ty; Eenum OpAux.false_tag OpAux.bool_velus_type]
    | (e, (k, r))::trans =>
      [Ecase e [(OpAux.true_tag, [Eenum k ty; Eenum (if r then OpAux.true_tag else OpAux.false_tag) OpAux.bool_velus_type]);
               (OpAux.false_tag, trans_exp ty trans current)]
             None ([ty; OpAux.bool_velus_type], Cbase)]
    end.

  Section auto_scope.
    Context {A : Type}.
    Variable f_auto : A -> FreshAnn (list block * list (list type)).

    Definition auto_scope (s : scope A) : FreshAnn (_ * list type) :=
      let 'Scope locs blks := s in
      do (blks', tys) <- f_auto blks;
      ret (Scope locs blks', concat tys).

  End auto_scope.

  Fixpoint auto_block (blk : block) : FreshAnn (block * list type) :=
    match blk with
    | Beq _ => ret (blk, [])
    | Breset blks er =>
        do (blks', tys) <- mmap2 auto_block blks;
        ret (Breset blks' er, concat tys)
    | Bswitch ec branches =>
        do (branches', tys) <- mmap2 (fun '(e, Branch _ blks) =>
                                       do (blks', tys) <- mmap2 auto_block blks;
                                       ret ((e, Branch [] blks'), concat tys)) branches;
        ret (Bswitch ec branches', concat tys)
    | Blocal s =>
        do (s', tys) <- auto_scope (mmap2 auto_block) s;
        ret (Blocal s', tys)
    | Bauto Weak ck (ini, oth) states =>
        do tyid <- fresh_ident;
        let xs := map snd (map fst states) in
        let ty := Tenum tyid xs in
        do st <- fresh_ident;
        do pst <- fresh_ident;
        do res <- fresh_ident;
        do pres <- fresh_ident;
        let stateq := Beq ([st; res],
                            [Efby [ init_state_exp ty ck ini oth;
                                    add_whens (Eenum OpAux.false_tag OpAux.bool_velus_type) OpAux.bool_velus_type ck]
                                  [Evar pst (ty, ck); Evar pres (OpAux.bool_velus_type, ck)]
                                  [(ty, ck); (OpAux.bool_velus_type, ck)]]) in
        do (branches, tys) <- mmap2 (fun '((e, _), Branch _ (_, s)) =>
                                      do (s', tys) <- auto_scope
                                                       (fun '(blks, trans) =>
                                                          do (blks', tys) <- mmap2 auto_block blks;
                                                          let transeq := Beq ([pst; pres], trans_exp ty trans e) in
                                                          ret (transeq::blks', tys))
                                                       s;
                                      ret ((e, (Branch [] [Breset [Blocal s'] (Evar res (OpAux.bool_velus_type, Cbase))])), tys)) states;
        let switch := Bswitch (Evar st (ty, ck)) branches in
        ret (Blocal (Scope [(st, (ty, ck, xH, None));
                            (pst, (ty, ck, xH, None));
                            (res, (OpAux.bool_velus_type, ck, xH, None));
                            (pres, (OpAux.bool_velus_type, ck, xH, None))]
                           [stateq;switch]), ty::concat tys)
    | Bauto Strong ck (_, oth) states =>
        do tyid <- fresh_ident;
        let xs := map snd (map fst states) in
        let ty := Tenum tyid xs in
        do st <- fresh_ident;
        do st1 <- fresh_ident;
        do res <- fresh_ident;
        do res1 <- fresh_ident;
        let stateq := Beq ([st; res],
                            [Efby [ add_whens (Eenum oth ty) ty ck;
                                    add_whens (Eenum OpAux.false_tag OpAux.bool_velus_type) OpAux.bool_velus_type ck]
                                  [Evar st1 (ty, ck); Evar res1 (OpAux.bool_velus_type, ck)]
                                  [(ty, ck); (OpAux.bool_velus_type, ck)]]) in
        let branches := map (fun '((e, _), Branch _ (unl, _)) =>
                               let transeq := Beq ([st1; res1], trans_exp (ty) unl e) in
                               (e, Branch [] [Breset [transeq] (Evar res (OpAux.bool_velus_type, Cbase))])) states in
        let switch1 := Bswitch (Evar st (ty, ck)) branches in
        do (branches, tys) <- mmap2 (fun '((e, _), Branch _ (_, s)) =>
                                      do (s', tys) <- auto_scope
                                                       (fun '(blks, trans) =>
                                                          do (blks', tys) <- mmap2 auto_block blks;
                                                          ret (blks', tys))
                                                       s;
                                      ret ((e, (Branch [] [Breset [Blocal s'] (Evar res1 (OpAux.bool_velus_type, Cbase))])), tys)) states;
        let switch2 := Bswitch (Evar st1 (ty, ck)) branches in
        ret (Blocal (Scope [(st, (ty, ck, xH, None));
                            (st1, (ty, ck, xH, None));
                            (res, (OpAux.bool_velus_type, ck, xH, None));
                            (res1, (OpAux.bool_velus_type, ck, xH, None))]
                           [stateq;switch1;switch2]), ty::concat tys)
    end.


  Lemma auto_block_st_follows : forall blk blk' tys st st',
      auto_block blk st = ((blk', tys), st') ->
      st_follows st st'.


  Import Permutation.

  Ltac auto_block_simpl_Forall :=
    repeat
      (match goal with
       | Hmap: mmap2 _ _ _ = (?blks', _, _) |- Forall _ ?blks' =>
         apply mmap2_values, Forall3_ignore13 in Hmap; simpl_Forall
       end; repeat inv_bind);
    eauto.

  Lemma auto_block_VarsDefinedComp : forall blk xs blk' tys st st',
      VarsDefinedComp blk xs ->
      auto_block blk st = ((blk', tys), st') ->
      VarsDefinedComp blk' xs.


  Lemma auto_not_in_last_prefs :
    ~PS.In auto last_prefs.

  Lemma fresh_idents_NoDup : forall x1 x2 x3 x4 st st1 st2 st3 st4,
      fresh_ident st = (x1, st1) ->
      fresh_ident st1 = (x2, st2) ->
      fresh_ident st2 = (x3, st3) ->
      fresh_ident st3 = (x4, st4) ->
      NoDup [x1;x2;x3;x4].

  Lemma auto_scope_NoDupScope {A} P_good P_nd f_auto : forall locs (blk: A) xs s' tys st st',
      auto_scope f_auto (Scope locs blk) st = ((s', tys), st') ->
      Forall (fun x => AtomOrGensym last_prefs x \/ In x (st_ids st)) xs ->
      GoodLocalsScope P_good last_prefs (Scope locs blk) ->
      NoDupScope P_nd xs (Scope locs blk) ->
      (forall xs blks' tys st st',
          f_auto blk st = ((blks', tys), st') ->
          Forall (fun x => AtomOrGensym last_prefs x \/ In x (st_ids st)) xs ->
          P_good blk ->
          P_nd xs blk ->
          Forall (NoDupLocals xs) blks') ->
      NoDupScope (fun xs => Forall (NoDupLocals xs)) xs s'.

  Lemma auto_block_NoDupLocals : forall blk xs blk' tys st st',
      auto_block blk st = ((blk', tys), st') ->
      Forall (fun x => AtomOrGensym last_prefs x \/ In x (st_ids st)) xs ->
      GoodLocals last_prefs blk ->
      NoDupLocals xs blk ->
      NoDupLocals xs blk'.


  Lemma auto_block_GoodLocals : forall blk blk' tys st st',
      GoodLocals last_prefs blk ->
      auto_block blk st = ((blk', tys), st') ->
      GoodLocals auto_prefs blk'.


  Lemma auto_block_noauto : forall blk blk' tys st st',
      nolast_block blk ->
      auto_block blk st = ((blk', tys), st') ->
      noauto_block blk'.

  Program Definition auto_node (n: @node nolast last_prefs) : @node noauto auto_prefs * list type :=
    let res := auto_block (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 (fst res));
        n_ingt0 := n_ingt0 n;
        n_outgt0 := n_outgt0 n
     |}, snd (fst res)).

  Definition auto_global (G : @global nolast last_prefs) : @global noauto auto_prefs :=
    let ndstys := map auto_node G.(nodes) in
    Global (G.(types)++flat_map snd ndstys) G.(externs) (map fst ndstys).

  Lemma auto_node_iface_eq : forall n,
      node_iface_eq n (fst (auto_node n)).

  Lemma auto_global_find_node : forall G f n,
      find_node f G = Some n ->
      exists n', find_node f (auto_global G) = Some n' /\ node_iface_eq n n'.

  Lemma auto_global_iface_incl : forall G,
      global_iface_incl G (auto_global G).

  Lemma auto_global_find_node' : forall G f n,
      find_node f (auto_global G) = Some n ->
      exists n', find_node f G = Some n' /\ node_iface_eq n n'.

End COMPAUTO.

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