(* This module defines the typing relation
 * where each expression is assigned a type.
 *)
From Coq Require Import Strings.String.
Require Import terms.
Require Import subst.
Require Import equiv.
Require Import subtype.

Include Terms.
Include Subst.
Include Equiv.
Include Subtype.

Module Typing.

(** Typing Derivation *)

Inductive context : Type :=
  | ctx_assign : string -> type_term -> context -> context
  | ctx_empty : context
.

Inductive context_contains : context -> string -> type_term -> Prop :=
  | C_take : forall (x:string) (X:type_term) (Γ:context),
    (context_contains (ctx_assign x X Γ) x X)
  | C_shuffle : forall x X y Y Γ,
    (context_contains Γ x X) ->
    (context_contains (ctx_assign y Y Γ) x X).

Reserved Notation "Gamma '|-' x '\is' X"  (at level 101, x at next level, X at level 0).
Reserved Notation "Gamma '|-' x '\compatible' X"  (at level 101, x at next level, X at level 0).

Inductive expr_type : context -> expr_term -> type_term -> Prop :=
  | T_Var : forall Γ x τ,
    (context_contains Γ x τ) ->
    (Γ |- (expr_var x) \is τ)

  | T_Let : forall Γ s (σ:type_term) t τ x,
    (Γ |- s \is σ) ->
    (Γ |- t \is τ) ->
    (Γ |- (expr_let x σ s t) \is τ)

  | T_TypeAbs : forall Γ (e:expr_term) (τ:type_term) α,
    Γ |- e \is τ ->
    Γ |- (expr_ty_abs α e) \is (type_univ α τ)

  | T_TypeApp : forall Γ α (e:expr_term) (σ:type_term) (τ:type_term),
    Γ |- e \is (type_univ α τ) ->
    Γ |- (expr_ty_app e σ) \is (type_subst α σ τ)

  | T_Abs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term),
    (context_contains Γ x σ) ->
    Γ |- t \is τ ->
    Γ |- (expr_abs x σ t) \is (type_fun σ τ)

  | T_App : forall (Γ:context) (f:expr_term) (a:expr_term) (σ:type_term) (τ:type_term),
    Γ |- f \is (type_fun σ τ) ->
    Γ |- a \is σ ->
    Γ |- (expr_app f a) \is τ

  | T_MorphAbs : forall Γ x σ e τ,
    (context_contains Γ x σ) ->
    Γ |- e \is τ ->
    Γ |- (expr_morph x σ e) \is (type_morph σ τ)

  | T_MorphFun : forall Γ f σ τ,
    Γ |- f \is (type_morph σ τ) ->
    Γ |- f \is (type_fun σ τ)

  | T_Ascend : forall Γ e τ τ',
    (Γ |- e \is τ) ->
    (τ' :<= τ) ->
    (Γ |- (expr_ascend τ' e) \is τ')

  | T_Descend : forall Γ x τ τ',
    Γ |- x \is τ ->
    (τ :<= τ') ->
    Γ |- x \is τ'

where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).


Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
  | TCompat_Native : forall Γ e τ,
    (Γ |- e \is τ) ->
    (Γ |- e \compatible τ)

  | TCompat_Let : forall Γ s (σ:type_term) t τ x,
    (Γ |- s \is σ) ->
    (context_contains Γ x σ) ->
    (Γ |- t \compatible τ) ->
    (Γ |- (expr_let x σ s t) \compatible τ)

  | T_CompatTypeApp : forall Γ α (e:expr_term) (σ:type_term) (τ:type_term),
    Γ |- e \compatible (type_univ α τ) ->
    Γ |- (expr_ty_app e σ) \compatible (type_subst α σ τ)

  | TCompat_App : forall Γ f a σ τ,
    (Γ |- f \compatible (type_fun σ τ)) ->
    (Γ |- a \compatible σ) ->
    (Γ |- (expr_app f a) \compatible τ)

  | TCompat_Morph : forall Γ h x τ τ',
    (context_contains Γ h (type_morph τ τ')) ->
    (Γ |- x \compatible τ) ->
    (Γ |- x \compatible τ')

  | TCompat_Sub : forall Γ x τ τ',
    (Γ |- x \compatible τ) ->
    (τ ~<= τ') ->
    (Γ |- x \compatible τ')

where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).

Definition is_well_typed (e:expr_term) : Prop :=
  exists Γ τ,
  Γ |- e \compatible τ
.

Definition is_exactly_typed (e:expr_term) : Prop :=
  exists Γ τ,
  Γ |- e \is τ
.

(* Examples *)

Example typing1 :
  forall Γ,
  (context_contains Γ "x" [< %"T"% >]) ->
  Γ |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"T", %"T"% -> %"T"% >].
   (* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
Proof.
  intros.
  apply T_TypeAbs.
  apply T_Abs.
  apply H.
  apply T_Var.
  apply H.
Qed.

Example typing2 :
  forall Γ,
  (context_contains Γ "x" [< %"T"% >]) ->
  Γ |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"U", %"U"% -> %"U"% >].
Proof.
  intros.
  apply T_Descend with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
  apply T_TypeAbs.
  apply T_Abs.
  apply H.
  apply T_Var.
  apply H.

  apply TSubRepr_Refl.
  apply TEq_Alpha.
  apply TAlpha_Rename.
  apply TSubst_Fun.
  apply TSubst_VarReplace.
  apply TSubst_VarReplace.
Qed.

Example typing3 :
  forall Γ,
  (context_contains Γ "x" [< %"T"% >]) ->
  (context_contains Γ "y" [< %"U"% >]) ->
  Γ |- [{
    Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"y"%
  }] \is [<
       ∀"S",∀"T",(%"S"%->%"T"%->%"T"%)
  >].
Proof.
  intros.
  apply T_Descend with (τ:=[< ∀"T",∀"U",(%"T"%->%"U"%->%"U"%) >]) (τ':=[< ∀"S",∀"T",(%"S"%->%"T"%->%"T"%) >]).
  apply T_TypeAbs, T_TypeAbs, T_Abs.
  apply H.
  apply T_Abs.
  apply H0.
  apply T_Var, H0.

  apply TSubRepr_Refl.
  apply TEq_Trans with (y:= [< ∀"S",∀"U",(%"S"%->%"U"%->%"U"%) >] ).
  apply TEq_Alpha.
  apply TAlpha_Rename.
  apply TSubst_UnivReplace. discriminate.
  easy.
  apply TSubst_Fun.
  apply TSubst_VarReplace.
  apply TSubst_Fun.
  apply TSubst_VarKeep. discriminate.
  apply TSubst_VarKeep. discriminate.

  apply TEq_Alpha.
  apply TAlpha_SubUniv.
  apply TAlpha_Rename.
  apply TSubst_Fun.
  apply TSubst_VarKeep. discriminate.
  apply TSubst_Fun.
  apply TSubst_VarReplace.
  apply TSubst_VarReplace.
Qed.


Example typing4 : (is_well_typed
  [{ Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"x"% }]
).
Proof.
  unfold is_well_typed.
  exists (ctx_assign "x" [< %"T"% >]
            (ctx_assign "y" [< %"U"% >] ctx_empty)).
  exists [< ∀"T",∀"U",%"T"%->%"U"%->%"T"% >].
  apply TCompat_Native.
  apply T_TypeAbs.
  apply T_TypeAbs.
  apply T_Abs.
  apply C_take.
  apply T_Abs.
  apply C_shuffle. apply C_take.
  apply T_Var.
  apply C_take.
Qed.

End Typing.