Library WellFormedness

Require Import Calculus.
Require Import Arith.
Require Import List.

Module SetProgram(My_Program: Program).

Import My_Program.

Require Semantics.
Module My_Semantics := Semantics.SetProgram(My_Program).

Import My_Semantics.
Import My_Typing.
Import My_TypeOrdering.
Import My_DeBruijn.
Import My_Substitutions.
Import My_Subclassing.

Relation: type well-formedness
Inductive Kinding: Env -> type -> Prop :=

  | K_Class:
    forall (G: Env) (C: ClassSym),
      (Kinding G (type_class C))

  | K_Virtual:
    forall (G: Env) (p: Path) (L: TypeSym) (C: ClassSym),
      (Gen_PathTyping G p (type_class C)) ->
      (typeOwner L) = C ->
      (Kinding G (type_virtual p L))
.

Property: unicity of method valuations
Definition no_method_overriding: Prop :=
  forall (m: MethodSym) (t u: Term) (C C': ClassSym),
    (methodValue m C) = (Some t) ->
    (methodValue m C') = (Some u) ->
    (Subclass C C') ->
    (t = u) /\ (C = C')
.

Property: unicity of type valuations
Definition no_type_overriding: Prop :=
  forall (L: TypeSym) (T U: type) (C C': ClassSym),
    (typeValue L C) = (Some T) ->
    (typeValue L C') = (Some U) ->
    (Subclass C C') ->
    (T = U) /\ (C = C')
.

Property: symRel is well-founded
Definition symRel_is_well_founded := (well_founded symRel).

Predicate: well-formedness of field declarations
Inductive WF_fieldDef: ClassSym -> FieldSym -> Prop :=
  | WF_fieldDef_intro:
    forall (C: ClassSym) (f: FieldSym) (T: type),
      (fieldType f) = T ->
      (Kinding (classEnv C) T) ->
      (WF_fieldDef C f)
.

Predicate: well-formedness of type declarations
Inductive WF_typeDef: ClassSym -> TypeSym -> Prop :=
  | WF_typeDef_intro:
    forall (C: ClassSym) (L: TypeSym) (U: type),
      (typeUpperBound L) = U ->
      (Kinding (classEnv C) U) ->
      (symRel (symbol_of_type U) (inr _ L)) ->
      (forall (T: type),
        (typeLowerBound L) = (Some T) ->
        ((Kinding (classEnv C) T) /\ (symRel (symbol_of_type T) (inr _ L)))
      ) ->
      (WF_typeDef C L)
.

Predicate: well-formedness of type valuations
Inductive WF_typeVal: ClassSym -> TypeSym -> type -> Prop :=
  | WF_typeVal_intro:
  forall (C C': ClassSym) (L: TypeSym) (S U: type),
    (Kinding (classEnv C) S) ->
    (symRel (symbol_of_type S) (inr _ L)) ->
    (typeOwner L) = C' ->
    (Subclass C C') ->
    (typeUpperBound L) = U ->
    (Subtyping (classEnv C) S U) ->
    (forall (T: type), (typeLowerBound L) = (Some T) -> (Subtyping (classEnv C) T S)) ->
    (WF_typeVal C L S)
.

Predicate: well-formedness of method declarations
Inductive WF_methodDef: ClassSym -> MethodSym -> Prop :=
  | WF_methodDef_intro:
    forall (C: ClassSym) (m: MethodSym) (T: type),
      (methodType m) = T ->
      (Kinding (classEnv C) T) ->
      (forall (x: ParamSym) (S: type),
        (paramOwner x) = m ->
        (paramType x) = S ->
        (Kinding (classEnv C) S)
      ) ->
      (WF_methodDef C m)
.

Function: returns the list of parameters of a method
Definition method_parameters (m: MethodSym): ParamTypeList :=
  let (xTs,_) := (method_parameters_spec m) in xTs
.

Lemma parameters_as_lists:
  forall (m: MethodSym) (x: ParamSym) (T: type),
    ((paramOwner x) = m /\ (paramType x) = T) <-> (In (x, T) (method_parameters m))
.

Lemma parameters_as_lists1:
  forall (m: MethodSym) (x: ParamSym) (T: type),
    ((paramOwner x) = m /\ (paramType x) = T) ->
    (In (x, T) (method_parameters m))
.

Lemma parameters_as_lists2:
  forall (m: MethodSym) (x: ParamSym) (T: type),
     (In (x, T) (method_parameters m)) ->
     ((paramOwner x) = m /\ (paramType x) = T)
.

Predicate: well-formedness of method implementations
Inductive WF_methodVal: ClassSym -> MethodSym -> Term -> Prop :=
  | WF_methodVal_intro:
    forall (G: Env) (C C': ClassSym) (m: MethodSym) (t: Term),
      (methodOwner m) = C' ->
      (Subclass C C') ->
      G = (Env_mk (Owner_class C) (method_parameters m) nil) ->
      (Typing G t (methodType m)) ->
      (WF_methodVal C m t)
.

Definition fieldDefs_are_well_formed (C: ClassSym): Prop :=
  forall (f: FieldSym), (fieldOwner f) = C -> (WF_fieldDef C f)
.

Definition typeDefs_are_well_formed (C: ClassSym): Prop :=
  forall (L: TypeSym), (typeOwner L) = C -> (WF_typeDef C L)
.

Definition typeVals_are_well_formed (C: ClassSym): Prop :=
  forall (L: TypeSym) (T: type), (typeValue L C) = (Some T) -> (WF_typeVal C L T)
.

Definition methodDefs_are_well_formed (C: ClassSym): Prop :=
  forall (m: MethodSym), (methodOwner m) = C -> (WF_methodDef C m)
.

Definition methodVals_are_well_formed (C: ClassSym): Prop :=
  forall (m: MethodSym) (t: Term), (methodValue m C) = (Some t) -> (WF_methodVal C m t)
.

Predicate: well-formedness of class declarations
Inductive WF_class: ClassSym -> Prop :=
  WF_class_intro:
  forall (C: ClassSym),
    (forall (C': ClassSym), (classSuper C) = (Some C') -> (symRel (inl _ C') (inl _ C))) ->
    (fieldDefs_are_well_formed C) ->
    (typeDefs_are_well_formed C) ->
    (typeVals_are_well_formed C) ->
    (methodDefs_are_well_formed C) ->
    (methodVals_are_well_formed C) ->
   (WF_class C)
.

Property: all classes are well-formed
Definition classes_are_well_formed: Prop :=
  forall (C: ClassSym), (WF_class C).

Property: class symbols are smaller than type symbols
Definition classes_smaller_than_types: Prop :=
  forall (C: ClassSym) (L: TypeSym), (symRel (inl _ C) (inr _ L))
.

Relation: the program is well-formed
Inductive WF_program: Prop :=
  | WF_program_intro:
    symRel_is_well_founded ->
    classes_smaller_than_types ->
    classes_are_well_formed ->
    no_method_overriding ->
    no_type_overriding ->
    (exists T: type, (Typing rootEnv main T)) ->
    WF_program
.

End SetProgram.

Index
This page has been generated by coqdoc