Module StaticEnv

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  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_inout (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_locs {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_inout senv_of_locs : list.

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

  Lemma map_fst_senv_of_inout : forall l,
      map fst (senv_of_inout l) = map fst l.
  Proof.

  Lemma map_fst_senv_of_locs {A} : forall l,
      map fst (@senv_of_locs A l) = map fst l.
  Proof.

  Global Hint Rewrite -> map_fst_senv_of_tyck.
  Global Hint Rewrite -> map_fst_senv_of_inout.
  Global Hint Rewrite -> @map_fst_senv_of_locs.

  Lemma InMembers_senv_of_locs {A} : forall x locs,
      InMembers x (@senv_of_locs A locs) <-> InMembers x locs.
  Proof.

  Global Hint Rewrite -> @InMembers_senv_of_locs : list.

  Lemma NoDupMembers_senv_of_locs {A} : forall locs,
      NoDupMembers (@senv_of_locs A locs) <-> NoDupMembers locs.
  Proof.

  Lemma IsVar_senv_of_locs {A} : forall x locs,
      IsVar (@senv_of_locs A locs) x <-> InMembers x locs.
  Proof.

  Global Hint Rewrite -> @IsVar_senv_of_locs.

  Lemma IsLast_senv_of_locs {A} : forall x locs,
      IsLast (@senv_of_locs A locs) x -> InMembers x locs.
  Proof.

  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).
  Proof.

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

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

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

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

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

  Lemma senv_of_inout_NoLast : forall Γ,
    forall x, ~IsLast (senv_of_inout Γ) x.
  Proof.

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

  Global Hint Rewrite map_fst_senv_of_inout : 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.