From Velus Require Import Common.
From Velus Require Import CommonProgram.
From Velus Require Import CommonTyping.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import Lustre.StaticEnv.
From Velus Require Import Lustre.LSyntax.

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

From Coq Require Import Morphisms.

From Velus Require Import Environment.
From Velus Require Import Operators.

Lustre typing

Module Type LTYPING
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import 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).

Clocks

  Section WellTyped.

    Variable types : list type.
    Variable Γ : static_env.

    Inductive wt_clock : clock -> Prop :=
    | wt_Cbase:
        wt_clock Cbase
    | wt_Con: forall ck x tx tn c,
        HasType Γ x (Tenum tx tn) ->
        In (Tenum tx tn) types ->
        c < length tn ->
        wt_clock ck ->
        wt_clock (Con ck x (Tenum tx tn, c)).

  End WellTyped.

  Import Permutation.

Expressions and equations

  Section WellTyped.
    Context {PSyn : list decl -> block -> Prop}.
    Context {prefs : PS.t}.

    Variable G : @global PSyn prefs.
    Variable Γ : static_env.

    Inductive wt_exp : exp -> Prop :=
    | wt_Econst: forall c,
        wt_exp (Econst c)

    | wt_Eenum: forall k tx tn,
        wt_type G.(types) (Tenum tx tn) ->
        k < length tn ->
        wt_exp (Eenum k (Tenum tx tn))

    | wt_Evar: forall x ty nck,
        HasType Γ x ty ->
        wt_clock G.(types) Γ nck ->
        wt_exp (Evar x (ty, nck))

    | wt_Elast: forall x ty nck,
        HasType Γ x ty ->
        IsLast Γ x ->
        wt_clock G.(types) Γ nck ->
        wt_exp (Elast x (ty, nck))

    | wt_Eunop: forall op e tye ty nck,
        wt_exp e ->
        typeof e = [tye] ->
        type_unop op tye = Some ty ->
        wt_type G.(types) ty ->
        wt_clock G.(types) Γ nck ->
        wt_exp (Eunop op e (ty, nck))

    | wt_Ebinop: forall op e1 e2 ty1 ty2 ty nck,
        wt_exp e1 ->
        wt_exp e2 ->
        typeof e1 = [ty1] ->
        typeof e2 = [ty2] ->
        type_binop op ty1 ty2 = Some ty ->
        wt_type G.(types) ty ->
        wt_clock G.(types) Γ nck ->
        wt_exp (Ebinop op e1 e2 (ty, nck))

    | wt_Eextcall: forall f es tyout ck tyins,
        Forall wt_exp es ->
        Forall2 (fun ty cty => ty = Tprimitive cty) (typesof es) tyins ->
        typesof es <> [] ->
        In (f, (tyins, tyout)) G.(externs) ->
        wt_clock G.(types) Γ ck ->
        wt_exp (Eextcall f es (tyout, ck))

    | wt_Efby: forall e0s es anns,
        Forall wt_exp e0s ->
        Forall wt_exp es ->
        typesof es = map fst anns ->
        typesof e0s = map fst anns ->
        Forall (wt_clock G.(types) Γ) (map snd anns) ->
        wt_exp (Efby e0s es anns)

    | wt_Earrow: forall e0s es anns,
        Forall wt_exp e0s ->
        Forall wt_exp es ->
        typesof es = map fst anns ->
        typesof e0s = map fst anns ->
        Forall (wt_clock G.(types) Γ) (map snd anns) ->
        wt_exp (Earrow e0s es anns)

    | wt_Ewhen: forall es x b tx tn tys nck,
        HasType Γ x (Tenum tx tn) ->
        In (Tenum tx tn) G.(types) ->
        b < length tn ->
        Forall wt_exp es ->
        typesof es = tys ->
        wt_clock G.(types) Γ nck ->
        wt_exp (Ewhen es (x, Tenum tx tn) b (tys, nck))

    | wt_Emerge: forall x tx tn es tys nck,
        HasType Γ x (Tenum tx tn) ->
        In (Tenum tx tn) G.(types) ->
        Permutation (map fst es) (seq 0 (length tn)) ->
        es <> nil ->
        Forall (fun es => Forall wt_exp (snd es)) es ->
        Forall (fun es => typesof (snd es) = tys) es ->
        wt_clock G.(types) Γ nck ->
        wt_exp (Emerge (x, Tenum tx tn) es (tys, nck))

    | wt_EcaseTotal: forall e es tx tn tys nck,
        wt_exp e ->
        typeof e = [Tenum tx tn] ->
        In (Tenum tx tn) G.(types) ->
        Permutation (map fst es) (seq 0 (length tn)) ->
        es <> nil ->
        Forall (fun es => Forall wt_exp (snd es)) es ->
        Forall (fun es => typesof (snd es) = tys) es ->
        wt_clock G.(types) Γ nck ->
        wt_exp (Ecase e es None (tys, nck))

    | wt_EcaseDefault: forall e es d tx tn tys nck,
        wt_exp e ->
        typeof e = [Tenum tx tn] ->
        In (Tenum tx tn) G.(types) ->
        incl (map fst es) (seq 0 (length tn)) ->
        NoDupMembers es ->
        es <> nil ->
        Forall (fun es => Forall wt_exp (snd es)) es ->
        Forall (fun es => typesof (snd es) = tys) es ->
        Forall wt_exp d ->
        typesof d = tys ->
        wt_clock G.(types) Γ nck ->
        wt_exp (Ecase e es (Some d) (tys, nck))

    | wt_Eapp: forall f es er anns n,
        Forall wt_exp es ->
        Forall wt_exp er ->
        find_node f G = Some n ->
        Forall2 (fun et '(_, (t, _, _)) => et = t) (typesof es) n.(n_in) ->
        Forall2 (fun a '(_, (t, _, _, _)) => fst a = t) anns n.(n_out) ->
        Forall (fun e => typeof e = [bool_velus_type]) er ->
        Forall (fun a => wt_clock G.(types) Γ (snd a)) anns ->
        wt_exp (Eapp f es er anns).

    Definition wt_equation (eq : equation) : Prop :=
      let (xs, es) := eq in
      Forall wt_exp es
      /\ Forall2 (HasType Γ) xs (typesof es).

  End WellTyped.

  Definition wt_clocks types Γ : static_env -> Prop :=
    Forall (fun '(_, ann) => wt_clock types Γ ann.(clo)).

  Inductive wt_scope {A} (P_wt : static_env -> A -> Prop) {PSyn prefs} (G: @global PSyn prefs) :
    static_env -> scope A -> Prop :=
  | wt_Scope : forall Γ locs blks,
      let Γ' := Γ ++ senv_of_decls locs in
      wt_clocks G.(types) Γ' (senv_of_decls locs) ->
      Forall (wt_type G.(types)) (map (fun '(_, (ty, _, _, _)) => ty) locs) ->
      Forall (fun '(_, (ty, _, _, o)) => LiftO True (fun '(e, _) => wt_exp G Γ' e /\ typeof e = [ty]) o) locs ->
      P_wt Γ' blks ->
      wt_scope P_wt G Γ (Scope locs blks).

  Inductive wt_branch {A} (P_wt : A -> Prop) : branch A -> Prop :=
  | wt_Branch : forall caus blks,
      P_wt blks ->
      wt_branch P_wt (Branch caus blks).

  Inductive wt_block {PSyn prefs} (G: @global PSyn prefs) : static_env -> block -> Prop :=
  | wt_Beq: forall Γ eq,
      wt_equation G Γ eq ->
      wt_block G Γ (Beq eq)

  | wt_Breset: forall Γ blocks er,
      Forall (wt_block G Γ) blocks ->
      wt_exp G Γ er ->
      typeof er = [bool_velus_type] ->
      wt_block G Γ (Breset blocks er)

  | wt_Bswitch : forall Γ ec branches tx tn,
      wt_exp G Γ ec ->
      typeof ec = [Tenum tx tn] ->
      In (Tenum tx tn) G.(types) ->
      Permutation (map fst branches) (seq 0 (length tn)) ->
      branches <> nil ->
      Forall (fun blks => wt_branch (Forall (wt_block G Γ)) (snd blks)) branches ->
      wt_block G Γ (Bswitch ec branches)

  | wt_BautoWeak : forall Γ ini oth states ck,
      wt_clock G.(types) Γ ck ->
      Forall (fun '(e, t) => wt_exp G Γ e /\ typeof e = [bool_velus_type] /\ InMembers t (map fst states)) ini ->
      InMembers oth (map fst states) ->
      Permutation (map fst (map fst states)) (seq 0 (length states)) ->
      NoDup (map snd (map fst states)) ->
      states <> [] ->
      Forall (fun blks =>
                wt_branch
                  (fun blks =>
                     fst blks = []
                     /\ wt_scope (fun Γ' blks => Forall (wt_block G Γ') (fst blks)
                                             /\ Forall (fun '(e, (t, _)) => wt_exp G Γ' e
                                                                        /\ typeof e = [bool_velus_type]
                                                                        /\ InMembers t (map fst states)) (snd blks))
                         G Γ (snd blks))
                  (snd blks)) states ->
      wt_block G Γ (Bauto Weak ck (ini, oth) states)

  | wt_BautoStrong : forall Γ oth states ck,
      wt_clock G.(types) Γ ck ->
      InMembers oth (map fst states) ->
      Permutation (map fst (map fst states)) (seq 0 (length states)) ->
      NoDup (map snd (map fst states)) ->
      states <> [] ->
      Forall (fun blks =>
                wt_branch
                  (fun blks =>
                     Forall (fun '(e, (t, _)) => wt_exp G Γ e
                                              /\ typeof e = [bool_velus_type]
                                              /\ InMembers t (map fst states)) (fst blks)
                     /\ wt_scope (fun Γ' blks => Forall (wt_block G Γ') (fst blks) /\ snd blks = [])
                         G Γ (snd blks))
                  (snd blks)) states ->
      wt_block G Γ (Bauto Strong ck ([], oth) states)

  | wt_Blocal: forall Γ scope,
      wt_scope (fun Γ' => Forall (wt_block G Γ')) G Γ scope ->
      wt_block G Γ (Blocal scope).

  Inductive wt_node {PSyn prefs} (G: @global PSyn prefs) : @node PSyn prefs -> Prop :=
  | wt_Node : forall n,
      let Γ := senv_of_ins n.(n_in) ++ senv_of_decls n.(n_out) in
      wt_clocks G.(types) (senv_of_ins n.(n_in)) (senv_of_ins n.(n_in)) ->
      wt_clocks G.(types) Γ (senv_of_decls n.(n_out)) ->
      Forall (fun '(_, ann) => wt_type G.(types) ann.(typ)) Γ ->
      Forall (fun '(_, (ty, _, _, o)) => LiftO True (fun '(e, _) => wt_exp G Γ e /\ typeof e = [ty]) o) n.(n_out) ->
      wt_block G Γ n.(n_block) ->
      wt_node G n.

  Definition wt_global {PSyn prefs} (G: @global PSyn prefs) : Prop :=
    wt_type G.(types) bool_velus_type /\
    wt_program wt_node G.

  Global Hint Constructors wt_type wt_clock wt_exp wt_block wt_node : ltyping.
  Global Hint Unfold wt_equation : ltyping.

  Ltac inv_exp :=
    match goal with
    | H:wt_exp _ _ _ |- _ => inv H
    end.

  Ltac inv_scope :=
    match goal with
    | H:wt_scope _ _ _ _ |- _ => inv H
    end;
    destruct_conjs; subst.

  Ltac inv_branch :=
    match goal with
    | H:wt_branch _ _ |- _ => inv H
    end;
    destruct_conjs; subst.

  Ltac inv_block :=
    match goal with
    | H:wt_block _ _ _ |- _ => inv H
    end.

  Lemma wt_global_NoDup {PSyn prefs}:
    forall (g : @global PSyn prefs),
      wt_global g ->
      NoDup (map name (nodes g)).

  Lemma wt_find_node {PSyn prefs}:
    forall (G : @global PSyn prefs) f n,
      wt_global G ->
      find_node f G = Some n ->
      exists G', wt_node G' n /\ types G' = types G.

  Lemma wt_clock_add:
    forall x v types env ck,
      ~InMembers x env ->
      wt_clock types env ck ->
      wt_clock types ((x, v) :: env) ck.

  Global Instance wt_clock_Proper types:
    Proper (@Permutation.Permutation _ ==> @eq clock ==> iff)
           (wt_clock types).

  Global Instance wt_clock_types_Proper :
    Proper (@incl _ ==> @eq _ ==> @eq _ ==> Basics.impl) wt_clock.

  Global Instance wt_clock_pointwise_Proper types :
    Proper (@Permutation.Permutation _
                                     ==> pointwise_relation clock iff)
           (wt_clock types).

  Global Instance wt_clock_incl_Proper :
    Proper (@incl _ ==> @eq _ ==> @eq _ ==> Basics.impl) wt_clock.

  Import Permutation.

  Global Instance wt_exp_Proper {PSyn prefs}:
    Proper (@eq (@global PSyn prefs) ==> @Permutation _
                ==> @eq exp ==> iff)
           wt_exp.

  Global Instance wt_exp_pointwise_Proper {PSyn prefs}:
    Proper (@eq (@global PSyn prefs) ==> @Permutation _
                                     ==> pointwise_relation exp iff) wt_exp.

  Global Instance wt_equation_Proper {PSyn prefs}:
    Proper (@eq (@global PSyn prefs) ==> @Permutation _
                ==> @eq equation ==> iff)
           wt_equation.


  Section incl.

    Fact wt_clock_incl : forall types Γ Γ' cl,
        (forall x ty, HasType Γ x ty -> HasType Γ' x ty) ->
        wt_clock types Γ cl ->
        wt_clock types Γ' cl.
    Local Hint Resolve wt_clock_incl : ltyping.

    Lemma wt_exp_incl {PSyn prefs} : forall (G: @global PSyn prefs) Γ Γ' e,
        (forall x ty, HasType Γ x ty -> HasType Γ' x ty) ->
        (forall x, IsLast Γ x -> IsLast Γ' x) ->
        wt_exp G Γ e ->
        wt_exp G Γ' e.

    Lemma wt_equation_incl {PSyn prefs} : forall (G: @global PSyn prefs) Γ Γ' eq,
        (forall x ty, HasType Γ x ty -> HasType Γ' x ty) ->
        (forall x, IsLast Γ x -> IsLast Γ' x) ->
        wt_equation G Γ eq ->
        wt_equation G Γ' eq.

    Lemma wt_scope_incl {A} (P_wt : static_env -> A -> Prop) {PSyn prefs} : forall (G: @global PSyn prefs) Γ Γ' locs blks,
        (forall x ty, HasType Γ x ty -> HasType Γ' x ty) ->
        (forall x, IsLast Γ x -> IsLast Γ' x) ->
        (forall Γ Γ', (forall x ty, HasType Γ x ty -> HasType Γ' x ty) ->
                 (forall x, IsLast Γ x -> IsLast Γ' x) ->
                 P_wt Γ blks ->
                 P_wt Γ' blks) ->
        wt_scope P_wt G Γ (Scope locs blks) ->
        wt_scope P_wt G Γ' (Scope locs blks).

    Lemma wt_block_incl {PSyn prefs} : forall (G: @global PSyn prefs) d Γ Γ',
        (forall x ty, HasType Γ x ty -> HasType Γ' x ty) ->
        (forall x, IsLast Γ x -> IsLast Γ' x) ->
        wt_block G Γ d ->
        wt_block G Γ' d .

  End incl.

  Lemma wt_exp_clockof {PSyn prefs}:
    forall (G: @global PSyn prefs) Γ e,
      wt_exp G Γ e ->
      Forall (wt_clock G.(types) Γ) (clockof e).

  Module NatOrder <: Orders.TotalLeBool.
    Definition t := nat.
    Definition leb := Nat.leb.
    Theorem leb_total :
      forall a1 a2, Nat.leb a1 a2 = true \/ Nat.leb a2 a1 = true.
  End NatOrder.

  Module SortNat := Mergesort.Sort(NatOrder).

Validation

  Section ValidateExpression.

    Context {PSyn : list decl -> block -> Prop}.
    Context {prefs : PS.t}.

    Variable G : @global PSyn prefs.
    Variable tenv : Env.t type.
    Variable extenv : Env.t (list ctype * ctype).
    Variable venv venvl : Env.t type.
    Variable env : static_env.

    Hypothesis Htypes : forall x ty, Env.find x tenv = Some ty -> wt_type G.(types) ty.
    Hypothesis Hexterns : forall x ty, Env.find x extenv = Some ty -> In (x, ty) G.(externs).
    Hypothesis Henv : forall x ty, Env.find x venv = Some ty -> HasType env x ty.
    Hypothesis Henvl : forall x ty, Env.find x venvl = Some ty -> HasType env x ty /\ IsLast env x.

    Open Scope option_monad_scope.

    Definition check_type_in ty : bool :=
      match ty with
      | Tenum x n =>
          match Env.find x tenv with
          | Some ty' => ty' ==b ty
          | None => false
          end
      | _ => true
      end.

    Lemma check_type_in_correct : forall ty,
        check_type_in ty = true ->
        wt_type G.(types) ty.

    Opaque check_type_in.

    Fixpoint check_clock (ck : clock) : bool :=
      match ck with
      | Cbase => true
      | Con ck' x (ty, k) =>
          match Env.find x venv with
          | Some (Tenum xt n) => (ty ==b Tenum xt n)
                                && (k <? length n)
                                && check_type_in ty
                                && check_clock ck'
          | _ => false
          end
      end.

    Lemma check_clock_correct:
      forall ck,
        check_clock ck = true ->
        wt_clock G.(types) env ck.

    Scheme Equality for list.