(* 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.
Include Terms.
Include Subst.
Include Equiv.

Module Typing.


(** Subtyping *)

Reserved Notation "s ':<=' t" (at level 50).
Reserved Notation "s '~=~' t" (at level 50).

Inductive is_syntactic_subtype : type_term -> type_term -> Prop :=
  | S_Refl : forall t t', (t === t') -> (t :<= t')
  | S_Trans : forall x y z, (x :<= y) -> (y :<= z) -> (x :<= z)
  | S_SynRepr : forall x' x y, (x :<= y) -> ((type_ladder x' x) :<= y)
where "s ':<=' t" := (is_syntactic_subtype s t).

Inductive is_semantic_subtype : type_term -> type_term -> Prop :=
  | S_Synt : forall x y,
    (x :<= y) -> (x ~=~ y)

  | S_SemRepr : forall x y y',
    (type_ladder x y) ~=~ (type_ladder x y')
where "s '~=~' t" := (is_semantic_subtype s t).


Open Scope ladder_type_scope.

Example sub0 :
  [   < $"Seq"$ < $"Digit"$ $"10"$ > >
    ~ < $"Seq"$ $"Char"$ > ]
  :<=
  [   < $"Seq"$ $"Char"$ > ]
.
Proof.
apply S_SynRepr.
apply S_Refl.
apply L_Refl.
Qed.

Example sub1 :
  [ < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > ]
  :<= [ < $"Seq"$ $"Char"$ > ]
.
Proof.
  set [ < $"Seq"$ < $"Digit"$ $"10"$ > > ~ < $"Seq"$ $"Char"$ > ].
  set [ < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > ].
  set [ < $"Seq"$ $"Char"$ > ].
  set (t0 === t).
  set (t :<= t0).
  set (t :<= t2).
  apply S_Trans with t1.
  apply S_Refl.
Qed.


(** 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),
    (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 τ) ->
    (Γ |- 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_tm_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_tm_app f a) \is τ

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



Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=

  | T_Compatible : forall Γ x τ,
    (Γ |- x \is τ) ->
    (Γ |- x \compatible τ)

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

Example typing1 :
  forall Γ,
  (context_contains Γ "x" (type_var "T")) ->
  Γ |- (expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \is
    (type_univ "T" (type_fun (type_var "T") (type_var "T"))).
Proof.
  intros.
  apply T_TypeAbs.
  apply T_Abs.
  apply H.
  apply T_Var.
  apply H.
Admitted.

Example typing2 :
  ctx_empty |- (expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \is
    (type_univ "T" (type_fun (type_var "T") (type_var "T"))).
Proof.
  apply T_TypeAbs.
  apply T_Abs.
  
Admitted.

End Typing.