Module Qcert.NNRS.Typing.TNNRS

Require Import String.
Require Import List.
Require Import Arith.
Require Import Program.
Require Import EquivDec.
Require Import Morphisms.
Require Import Utils.
Require Import DataSystem.
Require Import NNRS.
Require Import NNRSEval.
Require Import NNRSSem.
Require Import NNRSSemEval.
Require Import NNRSVars.

Import ListNotations.
Local Open Scope list_scope.

Section TNNRS.
  Context {m:basic_model}.

  Definition pd_tbindings := list (string*option rtype).
  Definition mc_tbindings := list (string*rtype).
  Definition md_tbindings := list (string*rtype).

  Definition preserves_Some {A B} (f:A->option B) (xd yd:A) : Prop
    := forall xd', f xd = Some xd' -> exists yd', f yd= Some yd'.

  Global Instance preserves_Some_pre {A B} (f:A->option B)
    : PreOrder (preserves_Some f).


  Lemma Forall2_preserves_Some_snd_update_first {B} l v (d:B) :
    Forall2 (preserves_Some snd) l (update_first string_dec l v (Some d)).
  
  Definition pd_bindings_type (b:pd_bindings) (t:pd_tbindings)
    := Forall2 (fun xy1 xy2 =>
                  (fst xy1) = (fst xy2)
                  /\ lift2Pr data_type (snd xy1) (snd xy2)) b t.

  Definition mc_bindings_type (b:mc_bindings) (t:mc_tbindings)
    := Forall2 (fun xy1 xy2 =>
                  (fst xy1) = (fst xy2)
                  /\ Forall (fun d => data_type d (snd xy2)) (snd xy1)) b t.

  Definition md_bindings_type (b:md_bindings) (t:md_tbindings)
    := Forall2 (fun xy1 xy2 =>
                  (fst xy1) = (fst xy2)
                  /\ forall d, Some d = snd xy1 ->
                               data_type d (snd xy2)) b t.
  
  Section typ.
    Context (Γc:tbindings).

    Reserved Notation "[ Γ ⊢ e ▷ τ ]".

    Inductive nnrs_expr_type : pd_tbindings -> nnrs_expr -> rtype -> Prop :=
    | type_NNRSGetConstant {τ} Γ s :
        tdot Γc s = Some τ ->
        [ Γ ⊢ NNRSGetConstant s ▷ τ ]
    | type_NNRSVar {τ} Γ v :
        lookup equiv_dec Γ v = Some (Some τ) ->
        [ Γ ⊢ NNRSVar v ▷ τ ]
    | type_NNRSConst {τ} Γ c :
        normalize_data brand_relation_brands c ▹ τ ->
        [ Γ ⊢ NNRSConst c ▷ τ ]
    | type_NNRSBinop {τ₁ τ₂ τ} Γ b e₁ e₂ :
        binary_op_type b τ₁ τ₂ τ ->
        [ Γ ⊢ e₁ ▷ τ₁ ] ->
        [ Γ ⊢ e₂ ▷ τ₂ ] ->
        [ Γ ⊢ NNRSBinop b e₁ e₂ ▷ τ ]
    | type_NNRSUnop {τ₁ τ} Γ u e :
        unary_op_type u τ₁ τ ->
        [ Γ ⊢ e ▷ τ₁ ] ->
        [ Γ ⊢ NNRSUnop u e ▷ τ ]
    | type_NNRSGroupBy {τl k pf} Γ g sl e :
        sublist sl (domain τl) ->
        [ Γ ⊢ e ▷ Coll (Rec k τl pf) ] ->
        [ Γ ⊢ NNRSGroupBy g sl e ▷ GroupBy_type g sl k τl pf ]
    where
    "[ Γ ⊢ e ▷ τ ]" := (nnrs_expr_type Γ e τ) : nnrs_scope
    .

    Notation "[ Γ ⊢ e ▷ τ ]" := (nnrs_expr_type Γ e τ) : nnrs_scope.


    Fixpoint nnrs_stmt_must_assign (s:nnrs_stmt) (x:var) : Prop
      := match s with
         | NNRSSeq s₁ s₂ =>
           nnrs_stmt_must_assign s₁ x \/ nnrs_stmt_must_assign s₂ x
         | NNRSLet v e₁ s₂ =>
           nnrs_stmt_must_assign s₂ x
         | NNRSLetMut v s₁ s₂ =>
           (v <> x /\ nnrs_stmt_must_assign s₁ x) \/ nnrs_stmt_must_assign s₂ x
         | NNRSLetMutColl v s₁ s₂ =>
           nnrs_stmt_must_assign s₁ x \/ nnrs_stmt_must_assign s₂ x
         | NNRSAssign v e =>
           v = x
         | NNRSPush v e =>
           False
         | NNRSFor v e s₀ =>
           False
         | NNRSIf e s₁ s₂ =>
           nnrs_stmt_must_assign s₁ x /\ nnrs_stmt_must_assign s₂ x
         | NNRSEither e x₁ s₁ x₂ s₂ =>
           nnrs_stmt_must_assign s₁ x /\ nnrs_stmt_must_assign s₂ x
         end.

    Reserved Notation "[ Γ , Δc , Δd ⊢ s ]".

    Inductive nnrs_stmt_type :
      pd_tbindings -> mc_tbindings -> md_tbindings ->
      nnrs_stmt -> Prop :=
    | type_NNRSSeq Γ Δc Δd s₁ s₂ :
        [ Γ , Δc , Δd ⊢ s₁ ] ->
        [ Γ , Δc , Δd ⊢ s₂ ] ->
        [ Γ , Δc , Δd ⊢ NNRSSeq s₁ s₂ ]
    | type_NNRSLet Γ Δc Δd τ x e₁ s₂ :
        [ Γ ⊢ e₁ ▷ τ ] ->
        [ (x,Some τ)::Γ , Δc , Δd ⊢ s₂ ] ->
        [ Γ , Δc , Δd ⊢ NNRSLet x e₁ s₂ ]
    | type_NNRSLetMutDef Γ Δc Δd τ x s₁ s₂ :
        nnrs_stmt_must_assign s₁ x ->
        [ Γ , Δc , (x,τ)::Δd ⊢ s₁ ] ->
        [ (x,Some τ)::Γ, Δc , Δd ⊢ s₂ ] ->
        [ Γ , Δc , Δd ⊢ NNRSLetMut x s₁ s₂ ]
    | type_NNRSLetMutNotUsed Γ Δc Δd x τ s₁ s₂ :
        [ Γ , Δc , (x,τ)::Δd ⊢ s₁ ] ->
        [ (x,None)::Γ, Δc , Δd ⊢ s₂ ] ->
        [ Γ , Δc , Δd ⊢ NNRSLetMut x s₁ s₂ ]
    | type_NNRSLetMutColl Γ Δc Δd τ x s₁ s₂ :
        [ Γ , (x,τ)::Δc , Δd ⊢ s₁ ] ->
        [ (x,Some (Coll τ))::Γ, Δc , Δd ⊢ s₂ ] ->
        [ Γ , Δc , Δd ⊢ NNRSLetMutColl x s₁ s₂ ]
    | type_NNRSAssign Γ Δc Δd τ x e :
        [ Γ ⊢ e ▷ τ ] ->
        lookup string_dec Δd x = Some τ ->
        [ Γ , Δc , Δd ⊢ NNRSAssign x e ]
    | type_NNRSPush Γ Δc Δd τ x e :
        [ Γ ⊢ e ▷ τ ] ->
        lookup string_dec Δc x = Some τ ->
        [ Γ , Δc , Δd ⊢ NNRSPush x e ]
    | type_NNRSFor Γ Δc Δd τ x e₁ s₂ :
        [ Γ ⊢ e₁ ▷ Coll τ ] ->
        [ (x,Some τ)::Γ , Δc , Δd ⊢ s₂ ] ->
        [ Γ , Δc , Δd ⊢ NNRSFor x e₁ s₂ ]
    | type_NNRSIf Γ Δc Δd e s₁ s₂ :
        [ Γ ⊢ e ▷ Bool] ->
        [ Γ , Δc , Δd ⊢ s₁ ] ->
        [ Γ , Δc , Δd ⊢ s₂ ] ->
        [ Γ , Δc , Δd ⊢ NNRSIf e s₁ s₂ ]
    | type_NNRSEither Γ Δc Δd τl τr e x₁ s₁ x₂ s₂ :
        [ Γ ⊢ e ▷ Either τl τr] ->
        [ (x₁,Some τl)::Γ , Δc , Δd ⊢ s₁ ] ->
        [ (x₂,Some τr)::Γ , Δc , Δd ⊢ s₂ ] ->
        [ Γ , Δc , Δd ⊢ NNRSEither e x₁ s₁ x₂ s₂ ]
    where
    "[ Γ , Δc , Δd ⊢ s ]" := (nnrs_stmt_type Γ Δc Δd s) : nnrs_scope
    .

    Notation "[ Γ , Δc , Δd ⊢ s ]" := (nnrs_stmt_type Γ Δc Δd s) : nnrs_scope.
  End typ.

  Notation "[ Γc ; Γ ⊢ e ▷ τ ]" := (nnrs_expr_type Γc Γ e τ) : nnrs_scope.
  Notation "[ Γc ; Γ , Δc , Δd ⊢ s ]" := (nnrs_stmt_type Γc Γ Δc Δd s) : nnrs_scope.

  Local Open Scope nnrs.
  
  Definition nnrs_type Γc (si:nnrs) τ
    := let (s, ret) := si in
       [ Γc ; nil , nil , (ret, τ)::nil ⊢ s ].

  Notation "[ Γc ⊢ si ▷ τ ]" := (nnrs_type Γc si τ) : nnrs_scope.

  
  Lemma typed_nnrs_expr_yields_typed_data {σc Γc} {σ Γ} {e τ} :
    bindings_type σc Γc ->
    pd_bindings_type σ Γ ->
    [ Γc ; Γ ⊢ e ▷ τ ] ->
    exists d,
      nnrs_expr_eval brand_relation_brands σc σ e = Some d
      /\ d ▹ τ.

  Theorem typed_nnrs_expr_yields_typed_data_compute {σc Γc} {σ Γ} {e τ} :
    bindings_type σc Γc ->
    pd_bindings_type σ Γ ->
    [ Γc ; Γ ⊢ e ▷ τ ] ->
    {d |
     nnrs_expr_eval brand_relation_brands σc σ e = Some d
     & d ▹ τ}.

  Lemma nnrs_stmt_md_preserves_some {s σc σ ψc ψd σ' ψc' ψd'} :
    nnrs_stmt_eval brand_relation_brands σc σ ψc ψd s =
    Some (σ', ψc', ψd') ->
    Forall2 (preserves_Some snd) ψd ψd'.

  Lemma nnrs_stmt_md_preserves_some2 {s σc σ ψc ψd σ' ψc' ψd'} :
    nnrs_stmt_eval brand_relation_brands σc σ ψc ψd s =
    Some (σ', ψc', ψd') ->
    Forall2 (fun d1 d2 => fst d1 = fst d2 /\ flip (preserves_Some id) (snd d1) (snd d2)) ψd' ψd.

  Lemma nnrs_stmt_preserves_md_some_cons {s x σc σ ψc i ψd σ' ψc' o l} :
    nnrs_stmt_eval brand_relation_brands σc σ ψc ((x, Some i) :: ψd) s =
    Some (σ', ψc', (x, o) :: l) ->
    exists d, o = Some d.

  Lemma nnrs_stmt_must_assign_assigns {s x σc σ ψc ψd σ' ψc' ψd'} :
    nnrs_stmt_must_assign s x ->
    nnrs_stmt_eval brand_relation_brands σc σ ψc ψd s =
    Some (σ', ψc', ψd') ->
    In x (domain ψd) ->
    exists d, lookup string_dec ψd' x = Some (Some d).
  
  Lemma nnrs_stmt_must_assign_assigns_cons {s x σc σ ψc i ψd σ' ψc' o l} :
    nnrs_stmt_must_assign s x ->
    nnrs_stmt_eval brand_relation_brands σc σ ψc ((x, i) :: ψd) s =
    Some (σ', ψc', (x, o) :: l) ->
    exists d, o = Some d.

  Lemma mc_bindings_type_lookup_back {ψc Δc τd x} :
    mc_bindings_type ψc Δc ->
    lookup string_dec Δc x = Some τd ->
    exists dl,
      lookup string_dec ψc x = Some dl
      /\ Forall (fun d => d ▹ τd) dl.

  Lemma md_bindings_type_lookup_back {ψd Δd τd x} :
    md_bindings_type ψd Δd ->
    lookup string_dec Δd x = Some τd ->
    exists o,
      lookup string_dec ψd x = Some o
      /\ forall d : data, Some d = o -> d ▹ τd.

  Lemma mc_bindings_type_update_first_same ψc Δc x dl τd :
    mc_bindings_type ψc Δc ->
    lookup string_dec Δc x = Some τd ->
    Forall (fun d => d ▹ τd) dl ->
    mc_bindings_type (update_first string_dec ψc x dl) Δc.

  Lemma md_bindings_type_update_first_same ψd Δd x d τd :
    md_bindings_type ψd Δd ->
    lookup string_dec Δd x = Some τd ->
    d ▹ τd ->
    md_bindings_type (update_first string_dec ψd x (Some d)) Δd.


  Theorem typed_nnrs_stmt_yields_typed_data {σc σ ψc ψd} {Γc Γ Δc Δd} (s:nnrs_stmt) :
    bindings_type σc Γc ->
    pd_bindings_type σ Γ ->
    mc_bindings_type ψc Δc ->
    md_bindings_type ψd Δd ->
    [ Γc ; Γ , Δc , Δd ⊢ s ] ->
    (exists σ' ψc' ψd',
        (nnrs_stmt_eval brand_relation_brands σc σ ψc ψd s) = Some (σ', ψc', ψd')
        /\ pd_bindings_type σ' Γ
        /\ mc_bindings_type ψc' Δc
        /\ md_bindings_type ψd' Δd).

  Theorem typed_nnrs_yields_typed_data {σc} {Γc} {τ} {si:nnrs}:
    bindings_type σc Γc ->
    [ Γc ⊢ si ▷ τ ] ->
    exists o,
      nnrs_eval brand_relation_brands σc si = Some o
      /\ forall d, o = Some d -> d ▹ τ.

  Theorem typed_nnrs_yields_typed_data_used {σc} {Γc} {τ} {si:nnrs}:
    nnrs_stmt_must_assign (fst si) (snd si) ->
    bindings_type σc Γc ->
    [ Γc ⊢ si ▷ τ ] ->
    exists d,
      nnrs_eval brand_relation_brands σc si = Some (Some d)
      /\ d ▹ τ.

  Theorem typed_nnrs_top_yields_typed_data {σc} {Γc} {τ} {si:nnrs}:
    bindings_type σc Γc ->
    [ rec_sort Γc ⊢ si ▷ τ ] ->
    forall d,
      nnrs_eval_top brand_relation_brands σc si = Some d
      -> d ▹ τ.

  Theorem typed_nnrs_top_yields_typed_data_used {σc} {Γc} {τ} {si:nnrs}:
    nnrs_stmt_must_assign (fst si) (snd si) ->
    bindings_type σc Γc ->
    [ rec_sort Γc ⊢ si ▷ τ ] ->
    exists d,
      nnrs_eval_top brand_relation_brands σc si = Some d
      /\ d ▹ τ.
  
  Section sem.

    Theorem typed_nnrs_yields_typed_data_sem {σc} {Γc} {τ} {si:nnrs}:
      bindings_type σc Γc ->
      [ Γc ⊢ si ▷ τ ] ->
      exists o,
        [ brand_relation_brands , σc ⊢ si ⇓ o ]
        /\ forall d, o = Some d -> d ▹ τ.

    Theorem typed_nnrs_yields_typed_data_used_sem {σc} {Γc} {τ} {si:nnrs}:
      nnrs_stmt_must_assign (fst si) (snd si) ->
      bindings_type σc Γc ->
      [ Γc ⊢ si ▷ τ ] ->
      exists d,
        [ brand_relation_brands , σc ⊢ si ⇓ Some d ]
        /\ d ▹ τ.
  End sem.
  
  Global Instance nnrs_expr_type_lookup_equiv_prop :
    Proper (eq ==> lookup_equiv ==> eq ==> eq ==> iff) nnrs_expr_type.

  Global Instance nnrs_stmt_type_lookup_equiv_prop :
    Proper (eq ==> lookup_equiv ==> lookup_equiv ==> lookup_equiv ==> eq ==> iff) nnrs_stmt_type.

  Section unused.
    Local Open Scope nnrs.

    Local Hint Constructors nnrs_expr_type : qcert.
    Local Hint Constructors nnrs_stmt_type : qcert.

    Section remove.
      
      Lemma nnrs_expr_type_unused_remove_env Γc l Γ e v τ τo:
        (In v (domain l) \/
         ~ In v (nnrs_expr_free_vars e)) ->
        [ Γc ; l++(v,τ)::Γ ⊢ e ▷ τo ] ->
        [ Γc ; l++Γ ⊢ e ▷ τo ].

      Lemma nnrs_stmt_type_unused_remove_env Γc l Γ Δc Δd s v τ:
        (In v (domain l) \/
         ~ In v (nnrs_stmt_free_env_vars s)) ->
        [ Γc ; l++(v,τ)::Γ , Δc , Δd ⊢ s ] ->
        [ Γc ; l++Γ , Δc , Δd ⊢ s ].

      Lemma nnrs_stmt_type_unused_remove_mdenv Γc l Γ Δc Δd s v τ:
        (In v (domain l) \/
         ~ In v (nnrs_stmt_free_mdenv_vars s)) ->
        [ Γc ; Γ , Δc , l++(v,τ)::Δd ⊢ s ] ->
        [ Γc ; Γ , Δc , l++Δd ⊢ s ].

      Lemma nnrs_stmt_type_unused_remove_mcenv Γc l Γ Δc Δd s v τ:
        (In v (domain l) \/
         ~ In v (nnrs_stmt_free_mcenv_vars s)) ->
        [ Γc ; Γ , l++(v,τ)::Δc , Δd ⊢ s ] ->
        [ Γc ; Γ , l++Δc , Δd ⊢ s ].

    End remove.
    
    Section add.
      
      Lemma nnrs_expr_type_unused_add_env Γc l Γ e v τ τo:
        (In v (domain l) \/
         ~ In v (nnrs_expr_free_vars e)) ->
        [ Γc ; l++Γ ⊢ e ▷ τo ] ->
        [ Γc ; l++(v,τ)::Γ ⊢ e ▷ τo ].

      Lemma nnrs_stmt_type_unused_add_env Γc l Γ Δc Δd s v τ:
        (In v (domain l) \/
         ~ In v (nnrs_stmt_free_env_vars s)) ->
        [ Γc ; l++Γ , Δc , Δd ⊢ s ] ->
        [ Γc ; l++(v,τ)::Γ , Δc , Δd ⊢ s ].

      Lemma nnrs_stmt_type_unused_add_mdenv Γc l Γ Δc Δd s v τ:
        (In v (domain l) \/
         ~ In v (nnrs_stmt_free_mdenv_vars s)) ->
        [ Γc ; Γ , Δc , l++Δd ⊢ s ] ->
        [ Γc ; Γ , Δc , l++(v,τ)::Δd ⊢ s ].

      Lemma nnrs_stmt_type_unused_add_mcenv Γc l Γ Δc Δd s v τ:
        (In v (domain l) \/
         ~ In v (nnrs_stmt_free_mcenv_vars s)) ->
        [ Γc ; Γ , l++Δc , Δd ⊢ s ] ->
        [ Γc ; Γ , l++(v,τ)::Δc , Δd ⊢ s ].

    End add.
  End unused.

  Lemma nnrs_stmt_must_assign_is_free s x : nnrs_stmt_must_assign s x -> In x (nnrs_stmt_free_mdenv_vars s).

  Lemma nnrs_expr_unused_tenv_free_env {Γc Γ e τ}:
    [Γc; Γ ⊢ e ▷ τ] ->
    forall x,
      lookup equiv_dec Γ x = Some None ->
      ~ In x (nnrs_expr_free_vars e).

  Lemma nnrs_expr_type_env_in_none_some {l1 Γc Γ v e τ} :
    [Γc; l1++(v, None) :: Γ ⊢ e ▷ τ] ->
    ~ In v (domain l1) ->
    forall τ',
      [Γc; l1++(v, Some τ') :: Γ ⊢ e ▷ τ].

  Lemma nnrs_stmt_type_env_in_none_some {l1 Γc Γ Δc Δd v s} :
    [Γc; l1++(v, None) :: Γ, Δc, Δd ⊢ s] ->
    ~ In v (domain l1) ->
    forall τ,
      [Γc; l1++(v, Some τ) :: Γ, Δc, Δd ⊢ s].

  Lemma nnrs_stmt_type_env_cons_none_some {Γc Γ Δc Δd v s} :
    [Γc; (v, None) :: Γ, Δc, Δd ⊢ s] ->
    forall τ,
      [Γc; (v, Some τ) :: Γ, Δc, Δd ⊢ s].
  

End TNNRS.

Notation "[ Γc ; Γ ⊢ e ▷ τ ]" := (nnrs_expr_type Γc Γ e τ) : nnrs_scope.
Notation "[ Γc ; Γ , Δc , Δd ⊢ s ]" := (nnrs_stmt_type Γc Γ Δc Δd s) : nnrs_scope.
Notation "[ Γc ⊢ si ▷ τ ]" := (nnrs_type Γc si τ) : nnrs_scope.