Module StcSyntax

From Velus Require Import Common.
From Velus Require Import Operators.
From Velus Require Import CoreExpr.CESyntax.
From Velus Require Import Clocks.

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

Module Type STCSYNTAX
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import CESyn : CESYNTAX Op).

Transition constraints

  Inductive trconstr :=
  | TcDef : ident -> clock -> cexp -> trconstr
  | TcNext : ident -> clock -> exp -> trconstr
  | TcReset: ident -> clock -> ident -> trconstr
  | TcCall : ident -> list ident -> clock -> bool -> ident -> list exp -> trconstr.

  Definition variables_tc (tc: trconstr): list ident :=
    match tc with
    | TcDef x _ _ => [x]
    | TcCall _ xs _ _ _ _ => xs
    | _ => []
    end.

  Definition variables := flat_map variables_tc.

  Inductive Is_sub_in_tc: ident -> nat -> trconstr -> Prop :=
  | SubTcReset:
      forall s ck b,
        Is_sub_in_tc s 0 (TcReset s ck b)
  | SubTcCall:
      forall s xs ck rst b es,
        Is_sub_in_tc s 1 (TcCall s xs ck rst b es).

  Definition Is_sub_in (s: ident) (k: nat) (tcs: list trconstr) : Prop :=
    Exists (Is_sub_in_tc s k) tcs.

  Definition Reset_in (s: ident) := Is_sub_in s 0.

  Definition Step_in (s: ident) := Is_sub_in s 1.

  Inductive Step_with_reset_in_tc: ident -> bool -> trconstr -> Prop :=
    Step_with_reset_in_tc_intro:
      forall s ys ck rst f es,
        Step_with_reset_in_tc s rst (TcCall s ys ck rst f es).

  Definition Step_with_reset_in (s: ident) (rst: bool) (tcs: list trconstr) : Prop :=
    Exists (Step_with_reset_in_tc s rst) tcs.

  Definition reset_consistency (tcs: list trconstr) : Prop :=
    forall s rst,
      Step_with_reset_in s rst tcs ->
      if rst then Reset_in s tcs else ~ Reset_in s tcs.

  Fixpoint lasts_of (tcs: list trconstr) : list ident :=
    match tcs with
    | [] => []
    | TcNext x _ _ :: tcs => x :: (lasts_of tcs)
    | _ :: tcs => lasts_of tcs
    end.

  Fixpoint calls_of (tcs: list trconstr) : list (ident * ident) :=
    match tcs with
    | [] => []
    | TcCall s _ _ _ b _ :: tcs => (s, b) :: calls_of tcs
    | _ :: tcs => calls_of tcs
    end.

  Fixpoint resets_of (tcs: list trconstr) : list (ident * ident) :=
    match tcs with
    | [] => []
    | TcReset s _ b :: tcs => (s, b) :: resets_of tcs
    | _ :: tcs => resets_of tcs
    end.

  Record system :=
    System {
        s_name : ident;
        s_in : list (ident * (type * clock));
        s_vars : list (ident * (type * clock));
        s_lasts: list (ident * (const * clock));
        s_subs : list (ident * ident);
        s_out : list (ident * (type * clock));
        s_tcs : list trconstr;

        s_ingt0 : 0 < length s_in;

        s_nodup : NoDup (map fst s_in ++ map fst s_vars ++
                                        map fst s_out ++ map fst s_lasts);
        s_nodup_lasts_subs : NoDup (map fst s_lasts ++ map fst s_subs);

        s_subs_in_tcs : forall f, In f (map snd s_subs)
                                       <-> In f (map snd (calls_of s_tcs ++ resets_of s_tcs));
        s_subs_calls_of : Permutation s_subs (calls_of s_tcs);

        s_lasts_in_tcs : Permutation (map fst s_lasts) (lasts_of s_tcs);
        s_vars_out_in_tcs : Permutation (map fst s_vars ++ map fst s_out) (variables s_tcs);

        s_no_single_reset : forall s, Reset_in s s_tcs -> Step_with_reset_in s true s_tcs;
        s_reset_consistency: reset_consistency s_tcs;
        s_reset_incl : incl (resets_of s_tcs) (calls_of s_tcs);

        s_good : Forall (AtomOrGensym (PSP.of_list gensym_prefs)) (map fst (s_in ++ s_vars ++ s_out))
                             /\ Forall (AtomOrGensym (PSP.of_list gensym_prefs)) (map fst s_lasts)
                             /\ Forall (AtomOrGensym (PSP.of_list gensym_prefs)) (map fst s_subs)
                             /\ atom s_name
      }.

  Lemma s_nodup_lasts:
    forall b, NoDupMembers b.(s_lasts).

  Lemma s_nodup_subs:
    forall b, NoDupMembers b.(s_subs).

  Lemma s_nodup_vars:
    forall b, NoDupMembers (s_in b ++ s_vars b ++ s_out b).

  Lemma s_nodup_variables:
    forall b, NoDup (variables b.(s_tcs)).

  Definition program := list system.

  Fixpoint find_system (b: ident) (P: program) : option (system * program) :=
   match P with
   | [] => None
   | bl :: P =>
     if ident_eqb bl.(s_name) b
     then Some (bl, P) else find_system b P
   end.


  Remark find_system_app:
    forall b P bl P',
      find_system b P = Some (bl, P') ->
      exists P'',
        P = P'' ++ bl :: P'
        /\ find_system b P'' = None.

  Remark find_system_name:
    forall b P bl P',
      find_system b P = Some (bl, P') ->
      bl.(s_name) = b.

  Remark find_system_other:
    forall b P bl,
      bl.(s_name) <> b ->
      find_system b (bl :: P) = find_system b P.

  Remark find_system_In:
    forall b P bl P',
      find_system b P = Some (bl, P') ->
      In bl P.

  Lemma find_system_app':
    forall b P P',
      find_system b (P ++ P') =
      match find_system b P with
      | None => find_system b P'
      | Some (bl, P'') => Some (bl, P'' ++ P')
      end.

  Lemma Step_with_reset_in_Step_in:
    forall tcs s rst,
      Step_with_reset_in s rst tcs ->
      Step_in s tcs.

  Lemma Step_with_reset_in_cons_not_call:
    forall tcs tc s rst,
      (forall s ys ck rst f es, tc <> TcCall s ys ck rst f es) ->
      (Step_with_reset_in s rst (tc :: tcs) <-> Step_with_reset_in s rst tcs).

  Lemma Step_with_reset_in_cons_call:
    forall tcs s (rst: bool) s' ys ck rst' f es,
      s <> s' ->
      (Step_with_reset_in s rst (TcCall s' ys ck rst' f es :: tcs) <-> Step_with_reset_in s rst tcs).

  Lemma calls_of_In:
    forall tcs s b,
      In (s, b) (calls_of tcs) ->
      exists xs ck rst es, In (TcCall s xs ck rst b es) tcs.

  Lemma calls_of_Is_sub_in:
    forall tcs s,
      InMembers s (calls_of tcs) -> exists k, Is_sub_in s k tcs.

  Lemma resets_of_app:
    forall tcs tcs',
      resets_of (tcs ++ tcs') = resets_of tcs ++ resets_of tcs'.

  Definition is_step_in_tc_b (s: ident) (tc: trconstr) : bool :=
    match tc with
    | TcCall s' _ _ _ _ _ => ident_eqb s s'
    | _ => false
    end.

  Definition is_step_in_tcs_b (s: ident) (tcs: list trconstr) : bool :=
    existsb (is_step_in_tc_b s) tcs.

  Definition is_reset_in_tc_b (s: ident) (tc: trconstr) : bool :=
    match tc with
    | TcReset s' _ _ => ident_eqb s s'
    | _ => false
    end.

  Definition is_reset_in_tcs_b (s: ident) (tcs: list trconstr) : bool :=
    existsb (is_reset_in_tc_b s) tcs.

  Fact Step_in_tc_reflect:
    forall s tc,
      Is_sub_in_tc s 1 tc <-> is_step_in_tc_b s tc = true.

  Corollary Step_in_reflect:
    forall s tcs,
      Step_in s tcs <-> is_step_in_tcs_b s tcs = true.

  Lemma Step_in_dec:
    forall s tcs,
      { Step_in s tcs } + { ~ Step_in s tcs }.

  Fact Reset_in_tc_reflect:
    forall s tc,
      Is_sub_in_tc s 0 tc <-> is_reset_in_tc_b s tc = true.

  Corollary Reset_in_reflect:
    forall s tcs,
      Reset_in s tcs <-> is_reset_in_tcs_b s tcs = true.

  Lemma Reset_in_dec:
    forall s tcs,
      { Reset_in s tcs } + { ~ Reset_in s tcs }.

  Lemma variables_app:
    forall tcs tcs',
      variables (tcs ++ tcs') = variables tcs ++ variables tcs'.

  Lemma not_Is_sub_in_cons:
    forall s tc tcs,
      (forall k, ~ Is_sub_in s k (tc :: tcs)) <-> (forall k, ~ Is_sub_in_tc s k tc) /\ (forall k, ~ Is_sub_in s k tcs).

End STCSYNTAX.

Module StcSyntaxFun
       (Ids : IDS)
       (Op : OPERATORS)
       (CESyn : CESYNTAX Op)
       <: STCSYNTAX Ids Op CESyn.
  Include STCSYNTAX Ids Op CESyn.
End StcSyntaxFun.