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

From Coq Require Import Morphisms.

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

Static environment for analysis of Lustre programs

Module Type STATICENV
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Ids Op)
       (Import Cks : CLOCKS Ids Op OpAux).

  Record annotation :=
    { typ : type;
      clo : clock;
      causl : ident;
      causl_last : option ident;
    }.

  Definition ann_with_clock (ann : annotation) (ck : clock) :=
    Build_annotation ann.(typ) ck ann.(causl) ann.(causl_last).

  Definition ann_with_caus (ann : annotation) (cx : ident) :=
    Build_annotation ann.(typ) ann.(clo) cx ann.(causl_last).

  Definition static_env := list (ident * annotation).

  Inductive IsVar : static_env -> ident -> Prop :=
  | IsVarC : forall senv x,
      InMembers x senv ->
      IsVar senv x.

  Lemma IsVar_fst : forall Γ x,
      IsVar Γ x <-> In x (map fst Γ).

  Inductive HasType : static_env -> ident -> type -> Prop :=
  | HasTypeC : forall senv x ty e,
      In (x, e) senv ->
      e.(typ) = ty ->
      HasType senv x ty.

  Inductive HasClock : static_env -> ident -> clock -> Prop :=
  | HasClockC : forall senv x ck e,
      In (x, e) senv ->
      e.(clo) = ck ->
      HasClock senv x ck.

  Inductive HasCaus : static_env -> ident -> ident -> Prop :=
  | HasCausC : forall senv x cx e,
      In (x, e) senv ->
      e.(causl) = cx ->
      HasCaus senv x cx.

  Inductive IsLast : static_env -> ident -> Prop :=
  | IsLastC : forall senv x e,
      In (x, e) senv ->
      e.(causl_last) <> None ->
      IsLast senv x.

  Inductive HasLastCaus : static_env -> ident -> ident -> Prop :=
  | HasLastCausC : forall senv x cx e,
      In (x, e) senv ->
      e.(causl_last) = Some cx ->
      HasLastCaus senv x cx.

  Global Hint Constructors IsVar HasType HasClock HasCaus IsLast HasLastCaus : senv.

  Global Instance IsVar_proper:
    Proper (@Permutation.Permutation _ ==> @eq _ ==> iff) IsVar.

  Global Instance HasType_proper:
    Proper (@Permutation.Permutation _ ==> @eq _ ==> @eq _ ==> iff) HasType.

  Global Instance HasClock_proper:
    Proper (@Permutation.Permutation _ ==> @eq _ ==> @eq _ ==> iff) HasClock.

  Global Instance HasCaus_proper:
    Proper (@Permutation.Permutation _ ==> @eq _ ==> @eq _ ==> iff) HasCaus.

  Global Instance IsLast_proper:
    Proper (@Permutation.Permutation _ ==> @eq _ ==> iff) IsLast.

  Global Instance HasLastCaus_proper:
    Proper (@Permutation.Permutation _ ==> @eq _ ==> @eq _ ==> iff) HasLastCaus.

  Lemma IsVar_incl : forall senv1 senv2 x,
      incl senv1 senv2 ->
      IsVar senv1 x ->
      IsVar senv2 x.

  Lemma IsVar_incl_fst : forall senv1 senv2,
      (forall x, IsVar senv1 x -> IsVar senv2 x) ->
      incl (map fst senv1) (map fst senv2).

  Lemma HasType_incl : forall senv1 senv2 x ty,
      incl senv1 senv2 ->
      HasType senv1 x ty ->
      HasType senv2 x ty.

  Lemma HasClock_incl : forall senv1 senv2 x ck,
      incl senv1 senv2 ->
      HasClock senv1 x ck ->
      HasClock senv2 x ck.

  Lemma HasCaus_incl : forall senv1 senv2 x cx,
      incl senv1 senv2 ->
      HasCaus senv1 x cx ->
      HasCaus senv2 x cx.

  Lemma IsLast_incl : forall senv1 senv2 x,
      incl senv1 senv2 ->
      IsLast senv1 x ->
      IsLast senv2 x.

  Lemma HasLastCaus_incl : forall senv1 senv2 x cx,
      incl senv1 senv2 ->
      HasLastCaus senv1 x cx ->
      HasLastCaus senv2 x cx.

  Global Hint Resolve IsVar_incl HasType_incl HasClock_incl HasCaus_incl IsLast_incl HasLastCaus_incl : senv.

  Lemma HasType_IsVar : forall env x ty,
      HasType env x ty ->
      IsVar env x.

  Lemma HasClock_IsVar : forall env x ck,
      HasClock env x ck ->
      IsVar env x.

  Lemma IsLast_IsVar : forall env x,
      IsLast env x ->
      IsVar env x.

  Global Hint Resolve HasType_IsVar HasClock_IsVar IsLast_IsVar : senv.

  Fact IsVar_app : forall env1 env2 x,
      IsVar (env1 ++ env2) x <-> IsVar env1 x \/ IsVar env2 x.

  Fact IsVar_concat : forall env1 env2 x,
      In env1 env2 ->
      IsVar env1 x ->
      IsVar (concat env2) x.
  Global Hint Resolve IsVar_concat : senv.

  Fact IsVar_concat' : forall env2 x,
      IsVar (concat env2) x ->
      exists env1, In env1 env2 /\ IsVar env1 x.

  Fact IsLast_app : forall env1 env2 x,
      IsLast (env1 ++ env2) x <-> IsLast env1 x \/ IsLast env2 x.

  Fact HasType_app : forall env1 env2 x cx,
      HasType (env1 ++ env2) x cx <-> HasType env1 x cx \/ HasType env2 x cx.

  Fact HasClock_app : forall env1 env2 x cx,
      HasClock (env1 ++ env2) x cx <-> HasClock env1 x cx \/ HasClock env2 x cx.

  Fact HasCaus_app : forall env1 env2 x cx,
      HasCaus (env1 ++ env2) x cx <-> HasCaus env1 x cx \/ HasCaus env2 x cx.

  Fact HasLastCaus_app : forall env1 env2 x cx,
      HasLastCaus (env1 ++ env2) x cx <-> HasLastCaus env1 x cx \/ HasLastCaus env2 x cx.

  Global Hint Rewrite IsLast_app HasType_app HasClock_app HasCaus_app HasLastCaus_app : list.

  Definition senv_of_tyck (l : list (ident * (type * clock))) : static_env :=
    List.map (fun '(x, (ty, ck)) => (x, Build_annotation ty ck xH None)) l.

  Definition senv_of_ins (l : list (ident * (type * clock * ident))) : static_env :=
    List.map (fun '(x, (ty, ck, cx)) => (x, Build_annotation ty ck cx None)) l.

  Definition senv_of_decls {A} (l : list (ident * (type * clock * ident * option (A * ident)))) : static_env :=
    List.map (fun '(x, (ty, ck, cx, o)) => (x, Build_annotation ty ck cx (option_map snd o))) l.

  Global Hint Unfold senv_of_ins senv_of_decls : list.

  Lemma senv_of_decls_app {A} : forall xs ys,
      @senv_of_decls A (xs ++ ys) = senv_of_decls xs ++ senv_of_decls ys.

  Lemma map_fst_senv_of_tyck : forall l,
      map fst (senv_of_tyck l) = map fst l.

  Lemma map_fst_senv_of_ins : forall l,
      map fst (senv_of_ins l) = map fst l.

  Lemma map_fst_senv_of_decls {A} : forall l,
      map fst (@senv_of_decls A l) = map fst l.

  Global Hint Rewrite -> map_fst_senv_of_tyck.
  Global Hint Rewrite -> map_fst_senv_of_ins.
  Global Hint Rewrite -> @map_fst_senv_of_decls.

  Lemma InMembers_senv_of_decls {A} : forall x locs,
      InMembers x (@senv_of_decls A locs) <-> InMembers x locs.

  Global Hint Rewrite -> @InMembers_senv_of_decls : list.

  Lemma NoDupMembers_senv_of_decls {A} : forall locs,
      NoDupMembers (@senv_of_decls A locs) <-> NoDupMembers locs.

  Lemma IsVar_senv_of_decls {A} : forall x locs,
      IsVar (@senv_of_decls A locs) x <-> InMembers x locs.

  Global Hint Rewrite -> @IsVar_senv_of_decls.

  Lemma IsLast_senv_of_decls {A} : forall x locs,
      IsLast (@senv_of_decls A locs) x -> InMembers x locs.

  Definition idty (env : static_env) : list (ident * type) :=
    map (fun '(x, entry) => (x, entry.(typ))) env.

  Definition idck (env : static_env) : list (ident * clock) :=
    map (fun '(x, entry) => (x, entry.(clo))) env.

  Global Hint Unfold idty idck : list.

  Definition idcaus_of_senv (env : static_env) : list (ident * ident) :=
    map (fun '(x, e) => (x, e.(causl))) env
    ++ map_filter (fun '(x, e) => option_map (fun cx => (x, cx)) e.(causl_last)) env.

  Import Permutation.

  Fact idcaus_of_senv_app : forall Γ1 Γ2,
      Permutation (idcaus_of_senv (Γ1 ++ Γ2))
                  (idcaus_of_senv Γ1 ++ idcaus_of_senv Γ2).

  Fact idcaus_of_senv_In : forall Γ x cx,
      (HasCaus Γ x cx \/ HasLastCaus Γ x cx)
      <-> In (x, cx) (idcaus_of_senv Γ).

  Fact HasCaus_snd_det Γ : forall x1 x2 cx,
      NoDup (map snd (idcaus_of_senv Γ)) ->
      HasCaus Γ x1 cx ->
      HasCaus Γ x2 cx ->
      x1 = x2.

  Fact HasLastCaus_snd_det Γ : forall x1 x2 cx,
      NoDup (map snd (idcaus_of_senv Γ)) ->
      HasLastCaus Γ x1 cx ->
      HasLastCaus Γ x2 cx ->
      x1 = x2.

  Fact NoDup_HasCaus_HasLastCaus Γ : forall x1 x2 cx,
      NoDup (map snd (idcaus_of_senv Γ)) ->
      HasCaus Γ x1 cx ->
      HasLastCaus Γ x2 cx ->
      False.

  Lemma senv_of_tyck_NoLast : forall Γ,
    forall x, ~IsLast (senv_of_tyck Γ) x.

  Lemma senv_of_ins_NoLast : forall Γ,
    forall x, ~IsLast (senv_of_ins Γ) x.

  Lemma NoLast_app : forall Γ1 Γ2,
      (forall x, ~IsLast (Γ1 ++ Γ2) x)
      <-> (forall x, ~IsLast Γ1 x) /\ (forall x, ~IsLast Γ2 x).

  Global Hint Rewrite map_fst_senv_of_ins : list.

End STATICENV.

Module StaticEnvFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Cks : CLOCKS Ids Op OpAux) <: STATICENV Ids Op OpAux Cks.
  Include STATICENV Ids Op OpAux Cks.
End StaticEnvFun.