Require Import Syntax.
Require Import List.

Require Import Util.

Module SetProgram(My_Program: Program).

Import My_Program.

Require Typing.
Module My_Typing := Typing.SetProgram(My_Program).

Import My_Typing.
Import My_Auxiliary.
Import My_Substitutions.
Import My_Binders.


Inductive classInheritance: ClassSym -> ClassSym -> Prop :=
  
  | classInheritance_intro:
    forall (C C': ClassSym) (R: TypeS),
      (classSuper C) = (Some (Class_type C' R)) ->
      (classInheritance C C')
.


Definition ClassSat (D: TypeEnv) (N: TypeS): Prop :=
  forall (C: ClassSym) (R: TypeS),
    (N = (Class_type C R)) ->

    (SectionSat D R (classTypeParams C))
.

Inductive Class_WK (C: ClassSym): Prop :=
 
 | Class_WK_intro:
   let Pi := (classTypeParams C) in
     (Type_WK nil Pi TypeSection) ->
     (forall (N: TypeS),
       (classSuper C) = (Some N) ->
       (is_classType N) /\
       ((Type_WK (Pi :: nil) N Type_)
       /\ (ClassSat (Pi :: nil) N))
     ) ->
   (Class_WK C)
.

Inductive FieldDecl_WF (f: FieldSym): Prop :=

  | FieldDecl_WF_intro:
      let C := (fieldOwner f) in
      let T := (fieldType f) in
      let Pi := (classTypeParams C) in
      (Type_WK (Pi :: nil) T Type_) ->
      (FieldDecl_WF f)
.

Inductive MethodDecl_WF (m: MethodSym): Prop :=

  | MethodDecl_WF_intro:
    let C := (methodOwner m) in
    let PiC := (classTypeParams C) in
    let Pim := (methodTypeParams m) in
    let Ts := (methodParams m) in
    let T := (methodType m) in
    let D := PiC :: Pim :: nil in
      (Type_WK (PiC :: nil) Pim TypeSection) ->
      (List_forall (fun U => (Type_WK D U Type_)) Ts) ->
      (Type_WK D T Type_) ->
      
      (MethodDecl_WF m)
.

Inductive MethodImpl_WF (C: ClassSym) (m: MethodSym) (t: Term): Prop :=

  | MethodImpl_WF_intro:
    forall (Rm: TypeS) (S: TypeS),
      let PiC := (classTypeParams C) in
      let Cm := (methodOwner m) in
      let Pim := (methodTypeParams m) in
      let Ts := (methodParams m) in
      let T := (methodType m) in
      (Subtyping (PiC :: nil) (Class_type C (Type_var 0)) (Class_type Cm Rm)) ->
      (Type_WK (PiC :: nil) (Class_type Cm Rm) Type_) ->
      let D := PiC :: (typeSubst_in_type Pim 0 Rm) :: nil in
      let G := (Class_type C (Type_var 1)) ::
                 (map (fun U => typeSubst_in_type U 1 Rm) Ts) in
         (Term_WT D G t (TermI S)) ->
         (Subtyping D S (typeSubst_in_type T 1 Rm)) ->
         
         (MethodImpl_WF C m t)
.


Axiom Class_inheritance_is_well_founded:
  (well_founded (symRel classInheritance))
.

Axiom classes_are_well_kinded:
  forall (C: ClassSym),
    (Class_WK C)
.

Axiom field_declarations_are_well_formed:
  forall (f: FieldSym),
    (FieldDecl_WF f)
.

Axiom method_declarations_are_well_formed:
  forall (m: MethodSym),
    (MethodDecl_WF m)
.

Axiom method_implementations_are_well_formed:
  forall (m: MethodSym) (C: ClassSym) (t: Term),
    (methodImpl m C) = (Some t) ->
    (MethodImpl_WF C m t)
.

Axiom main_term_is_well_typed:
  exists T: TypeS,
    (Term_WT nil nil mainTerm (TermI T))
.


End SetProgram.