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.