Require Import Syntax.
Require Import List.
Require Import Arith.
Require Import MatchCompNat.
Require Import Util.

Module SetProgram(My_Program: Program).

Import My_Program.

Require Auxiliary.
Module My_Auxiliary := Auxiliary.SetProgram(My_Program).

Import My_Auxiliary.
Import My_Substitutions.
Import My_Binders.


Definition is_arbitraryType (T: TypeS): Prop := True.

Inductive Type_WK: TypeEnv -> TypeS -> TypeC -> Prop :=
  
  

  | WK_proj:
    forall (D: TypeEnv) (R: TypeS) (i: nat) (k: KindS) (k': KindS),
      (Type_WK D R (TypeTuple (Kind_tuple k))) ->
      (KindS_at k i k') ->
      (Type_WK D (Type_proj R i) (TypeConstr k'))

  | WK_class:
    forall (D: TypeEnv) (C: ClassSym) (k: KindS),
      (kind_of (classTypeParams C) k) ->
      (Type_WK D (Type_class C) (TypeConstr (Kind_constr k)))

  | WK_fun:
    forall (D: TypeEnv) (Pi: TypeS) (N: TypeS) (k: KindS),
      (Type_WK D Pi TypeSection) ->
      (Type_WK (snoc D Pi) N Type_) ->
      
      (is_arbitraryType N) ->
      (kind_of Pi k) ->
      (Type_WK D (Type_fun Pi N) (TypeConstr (Kind_constr k)))

  

  | WK_apply:
    forall (D: TypeEnv) (K R: TypeS) (k: KindS),
      (Type_WK D K (TypeConstr (Kind_constr k))) ->
      (Type_WK D R (TypeTuple k)) ->
      (Type_WK D (Type_apply K R) Type_)

  

  | WK_var:
    forall (D: TypeEnv) (X: TypeVar) (Pi: TypeS) (k: KindS),
      (decl_of_typeVar D X Pi) ->
      (kind_of Pi k) ->
      (Type_WK D (Type_var X) (TypeTuple k))

  | WK_tuple:
    forall (D: TypeEnv) (Ks: TypeS) (k: KindS),
      (Type_WK D Ks (TypeConstrList k)) ->
      (Type_WK D (Type_tuple Ks) (TypeTuple (Kind_tuple k)))

  

  | WK_param:
    forall (D: TypeEnv) (Pi N_opt: TypeS),
      (Type_WK D Pi TypeSection) ->
      (Type_WK (snoc D Pi) N_opt TypeOption) ->
      (Type_WK D (Type_param Pi N_opt) TypeParam)

  

  | WK_section:
    forall (D: TypeEnv) (Ps: TypeS),
      (Type_WK (snoc D (Type_section Ps)) Ps TypeParamList) ->
      (Type_WK D (Type_section Ps) TypeSection)

  

  | WK_none:
    forall (D: TypeEnv),
      (Type_WK D Type_none TypeOption)

  | WK_some:
    forall (D: TypeEnv) (N: TypeS),
      (is_classType N) ->
      (Type_WK D N Type_) ->
      (Type_WK D (Type_some N) TypeOption)

  

  | WK_param_nil:
    forall (D: TypeEnv),
      (Type_WK D Type_nil TypeParamList)

  | WK_param_cons:
    forall (D: TypeEnv) (P Ps: TypeS),
      (Type_WK D P TypeParam) ->
      (Type_WK D Ps TypeParamList) ->
      (Type_WK D (Type_cons P Ps) TypeParamList)

  

  | WK_constr_nil:
    forall (D: TypeEnv),
      (Type_WK D Type_nil (TypeConstrList Kind_nil))

  | WK_constr_cons:
    forall (D: TypeEnv) (K Ks: TypeS) (k: KindS) (ks: KindS),
      (Type_WK D K (TypeConstr k)) ->
      (Type_WK D Ks (TypeConstrList ks)) ->
      (Type_WK D (Type_cons K Ks) (TypeConstrList (Kind_cons k ks)))
.

Inductive Subtyping: TypeEnv -> TypeS -> TypeS -> Prop :=

  | S_Refl:
    forall (D: TypeEnv) (T: TypeS),
      (Subtyping D T T)

  | S_Trans:
    forall (D: TypeEnv) (T S U: TypeS),
      (Type_WK D S Type_) ->
      (Subtyping D T S) ->
      (Subtyping D S U) ->
      (Subtyping D T U)

  | S_Var:
    forall (D: TypeEnv) (X: TypeVar) (i: nat) (R Ps Pi N N': TypeS),
      (decl_of_typeVar D X (Type_section Ps)) ->
      (TypeS_at (typeSubst_in_type Ps 0 (Type_var X)) i (Type_param Pi (Type_some N))) ->
      (Subtyping D (typeSubst_in_type N 0 R) N') ->
      (Subtyping D (Var_type X i R) N')

  | S_Class:
    forall (D: TypeEnv) (C: ClassSym) (R: TypeS) (N N': TypeS),
      (classSuper C) = (Some N) ->
      (Subtyping D (typeSubst_in_type N 0 R) N') ->
      (Subtyping D (Class_type C R) N')

  | S_Beta_Left:
    forall (D: TypeEnv) (T T' U: TypeS),
      (RedType T T') ->
      (Subtyping D T' U) ->
      (Subtyping D T U)

  | S_Beta_Right:
    forall (D: TypeEnv) (T U' U: TypeS),
      (RedType U U') ->
      (Subtyping D T U') ->
      (Subtyping D T U)
.

Inductive removeBounds: TypeS -> TypeS -> Prop :=
  
  | removeBounds_param:
    forall (Pi Pi' T: TypeS),
      (removeBounds Pi Pi') ->
      (removeBounds (Type_param Pi T) (Type_param Pi' Type_none))

  | removeBounds_section:
    forall (Ps Ps': TypeS),
      (removeBounds Ps Ps') ->
      (removeBounds (Type_section Ps) (Type_section Ps'))

  | removeBounds_param_nil:
    (removeBounds Type_nil Type_nil)

  | removeBounds_param_cons:
    forall (P P' Ps Ps': TypeS),
      (removeBounds P P') ->
      (removeBounds Ps Ps') ->
      (removeBounds (Type_cons P Ps) (Type_cons P' Ps'))
.

Inductive ParamSat (D: TypeEnv) (K: TypeS): TypeS -> Prop :=

  | ParamSat_intro:
    forall (Pi Pi' N_opt: TypeS),
      (removeBounds Pi Pi') ->
      (forall (N: TypeS),
        (N_opt = (Type_some N)) ->

        (Subtyping (snoc D Pi') (Type_apply (lift_in_type K 1) (Type_var 0)) N)
      ) ->
      (ParamSat D K (Type_param Pi N_opt))
.

Definition Forall_ParamSat (D: TypeEnv) (R Ps: TypeS): Prop :=
  forall (i: nat) (P: TypeS),
    (TypeS_at Ps i P) ->
    (ParamSat D (Type_proj R i) P)
.

Inductive Forall_ParamSat_build (D: TypeEnv) (R: TypeS): nat -> TypeS -> Prop :=

  | Forall_ParamSat_build_nil:
    forall (i: nat),
      (Forall_ParamSat_build D R i Type_nil)

  | Forall_ParamSat_build_cons:
    forall (i: nat) (P Ps: TypeS),
      (ParamSat D (Type_proj R i) P) ->
      (Forall_ParamSat_build D R (S i) Ps) ->
      (Forall_ParamSat_build D R i (Type_cons P Ps))
.

Inductive SectionSat (D: TypeEnv) (R: TypeS): TypeS -> Prop :=
  
  | SectionSat_intro:
    forall (Ps: TypeS) (ks: KindS),
      (kind_of Ps ks) ->
      (Type_WK D R (TypeTuple (Kind_tuple ks))) ->
      (Forall_ParamSat D R (typeSubst_in_type Ps 0 R)) ->
      (SectionSat D R (Type_section Ps))
.

Definition IsComplete_fields (C: ClassSym) (fs: list (FieldSym)): Prop :=
  forall (f: FieldSym),
    let C' := (fieldOwner f) in
    (Subclass C C') ->
    (In f fs)
.

Definition IsComplete_methods (C: ClassSym): Prop :=
  forall (m: MethodSym),
    let C' := (methodOwner m) in
    (Subclass C C') ->
    exists A: ClassSym, exists t: Term,
      (Subclass C A) /\ (methodImpl m A) = (Some t)
.

Inductive IsComplete: ClassSym -> (list FieldSym) -> Prop :=

  | IsComplete_intro:
    forall (C: ClassSym) (fs: list FieldSym),
      (IsComplete_fields C fs) ->
      (IsComplete_methods C) ->
      (IsComplete C fs)
.

Fixpoint fields_of_fieldTermList (fts: Term): (list FieldSym) :=
  match fts with
    | FieldTerm_nil => nil
    | (FieldTerm_cons f _ fts') => f :: (fields_of_fieldTermList fts')
    | _ => nil
  end
.

Definition Pointwise_subtyping (D: TypeEnv) (Ts Us: (list TypeS)): Prop :=
  (Forall2 (fun T U => (Subtyping D T U)) Ts Us)
.

Definition typeSubst_in_typeList (ts: (list TypeS)) (k: nat) (R: TypeS): (list TypeS) :=
  map (fun t => (typeSubst_in_type t k R)) ts
.


Inductive TermInfo: Set :=
  | TermI : TypeS -> TermInfo
  | TermListI : (list TypeS) -> TermInfo
  | FieldTermListI : TypeS -> TermInfo
.

Inductive Term_WT (D: TypeEnv) (G: TermEnv): Term -> TermInfo -> Prop :=

  | T_Var:
    forall (i: nat) (T: TypeS),
      (List_from G i T) ->
      
      (Term_WT D G (Term_var i) (TermI T))

  | T_Select:
    forall (t: Term) (f: FieldSym) (S R: TypeS),
      let C := (fieldOwner f) in
      let T := (fieldType f) in

      (Term_WT D G t (TermI S)) ->
      (Subtyping D S (Class_type C R)) ->
      (Type_WK D (Class_type C R) Type_) ->
      
      (Term_WT D G (Term_select t f) (TermI (typeSubst_in_type T 0 R)))

  | T_Call:
    forall (t: Term) (m: MethodSym) (R R': TypeS)
           (ts: Term) (S: TypeS) (Ss: (list TypeS)) (k: KindS),

      let C := (methodOwner m) in
      let Pi := (methodTypeParams m) in
      let Ts := (methodParams m) in
      let T := (methodType m) in

      (Term_WT D G t (TermI S)) ->
      (Type_WK D R (TypeTuple k)) ->
      (Term_WT D G ts (TermListI Ss)) ->
      (Subtyping D S (Class_type C R')) ->
      (Type_WK D (Class_type C R') Type_) ->
      (SectionSat D R (typeSubst_in_type Pi 0 R')) ->
      (Pointwise_subtyping D Ss
         (typeSubst_in_typeList (typeSubst_in_typeList Ts 1 R') 0 R)) ->
      
      (Term_WT D G (Term_call t m R ts)
                    (TermI (typeSubst_in_type (typeSubst_in_type T 1 R') 0 R)))

  | T_New:
    forall (fts: Term) (C: ClassSym) (R: TypeS),
      let N := (Class_type C R) in
      (Type_WK D N Type_) ->
      
      (SectionSat D R (classTypeParams C)) ->
      (Term_WT D G fts (FieldTermListI N)) ->
      (IsComplete C (fields_of_fieldTermList fts)) ->
      
      (Term_WT D G (Term_new N fts) (TermI N))



   | T_term_Nil:
     
     (Term_WT D G Term_nil (TermListI nil))

   | T_term_Cons:
     forall (t: Term) (ts: Term) (T: TypeS) (Ts: (list TypeS)),
       (Term_WT D G t (TermI T)) ->
       (Term_WT D G ts (TermListI Ts)) ->
       
       (Term_WT D G (Term_cons t ts) (TermListI (cons T Ts)))



  | T_fieldTerm_Nil:
    forall (N: TypeS),
      
      (Term_WT D G FieldTerm_nil (FieldTermListI N))

  | T_fieldTerm_Cons:
    forall (N: TypeS) (f: FieldSym) (t: Term) (fts: Term) (S R: TypeS),
      let C := (fieldOwner f) in
      let T := (fieldType f) in

      (Type_WK D N Type_) ->
      (Subtyping D N (Class_type C R)) ->
      (Type_WK D (Class_type C R) Type_) ->
      (Term_WT D G t (TermI S)) ->
      (Subtyping D S (typeSubst_in_type T 0 R)) ->
      (Term_WT D G fts (FieldTermListI N)) ->
      
      (Term_WT D G (FieldTerm_cons f t fts) (FieldTermListI N))
.

End SetProgram.