Definition of Path Typing, Subtyping, Term Typing |
Require Import Calculus.
Require Import List.
Require Import ListSet.
Module SetProgram(My_Program: Program).
Import My_Program.
Require TypeOrdering.
Module My_TypeOrdering := TypeOrdering.SetProgram(My_Program).
Import My_TypeOrdering.
Import My_DeBruijn.
Import My_Substitutions.
Import My_Subclassing.
Predicate: the current instance belongs to the path p
|
Definition this_in_path (p: Path): Prop :=
match p with
| Path_this => True
| (Path_param x) => False
| (Path_var n) => False
| (Path_value v) => False
end
.
Predicate: the current instance belongs to the type T
|
Definition this_in_type (T: type): Prop :=
match T with
| (type_class C) => False
| (type_virtual p L) => (this_in_path p)
end
.
| Sets of parameters |
Definition ParamSet := (set ParamSym).
Definition empty_paramset := (empty_set ParamSym).
Definition paramset_add (n: ParamSym) (vs: ParamSet) := (set_add (ParamSym_eq) n vs).
Definition paramset_union (vs: ParamSet) (vs': ParamSet) := (set_union (ParamSym_eq) vs vs').
Definition paramset_In (n: ParamSym) (vs: ParamSet): Prop := (set_In n vs).
Function: returns the free parameters in a path p
|
Definition fp_in_path (p: Path): ParamSet :=
match p with
| Path_this => empty_paramset
| (Path_param x) => (paramset_add x empty_paramset)
| (Path_var n) => empty_paramset
| (Path_value v) => empty_paramset
end
.
Function: returns the free parameters in a type T
|
Definition fp_in_type (T: type): ParamSet :=
match T with
| (type_class C) => empty_paramset
| (type_virtual p L) => (fp_in_path p)
end
.
Function: returns the free parameters in a term t
|
Fixpoint fp_in_term (t: Term): ParamSet :=
match t with
| (Term_this) => empty_paramset
| (Term_param x) => (paramset_add x empty_paramset)
| (Term_var i) => empty_paramset
| (Term_select p f) => (fp_in_path p)
| (Term_new C fts) => (fp_in_fieldTermList fts)
| (Term_call p m xts) => (paramset_union (fp_in_path p) (fp_in_paramTermList xts))
| (Term_loc T u u') => (paramset_union (paramset_union (fp_in_type T) (fp_in_term u)) (fp_in_term u'))
end
Function: returns the free parameters in the bindings xts
|
with fp_in_paramTermList (xts: ParamTermList): ParamSet :=
match xts with
| (ParamTerm_nil) => empty_paramset
| (ParamTerm_cons x t xts') => (paramset_union (fp_in_term t) (fp_in_paramTermList xts'))
end
Function: returns the free parameters in the bindings fts
|
with fp_in_fieldTermList (fts: FieldTermList): ParamSet :=
match fts with
| (FieldTerm_nil) => empty_paramset
| (FieldTerm_cons f t fts') => (paramset_union (fp_in_term t) (fp_in_fieldTermList fts'))
end
.
Predicate: the parameter x belongs to the path p
|
Definition param_in_path (x: ParamSym) (p: Path): Prop :=
paramset_In x (fp_in_path p)
.
Predicate: the parameter x belongs to the type T
|
Definition param_in_type (x: ParamSym) (T: type): Prop :=
paramset_In x (fp_in_type T)
.
Predicate: the parameter x belongs to the term t
|
Definition param_in_term (x: ParamSym) (t: Term): Prop :=
paramset_In x (fp_in_term t)
.
Predicate: the type T is closed
|
Definition type_is_closed (T: type): Prop :=
~(this_in_type T) /\
(fp_in_type T) = empty_paramset /\
(fv_in_type T) = empty_varset
.
| Owner contexts |
Inductive Owner: Set :=
| Owner_root : Owner
| Owner_class : ClassSym -> Owner
.
| Lists of bindings from parameter symbols to types |
Definition ParamTypeList: Set := list (ParamSym * type).
| Lists of types |
Definition TypeList: Set := list (type).
| Relation: computes the n-th element of a list of types |
Inductive TypeList_at: TypeList -> nat -> type -> Prop :=
| TypeList_at_head:
forall (Ts: TypeList) (T: type),
(TypeList_at (cons T Ts) 0 T)
| TypeList_at_tail:
forall (T: type) (Ts: TypeList) (n: nat) (U: type),
(TypeList_at Ts n U) ->
(TypeList_at (cons T Ts) (S n) U)
.
| Typing environments |
Inductive Env: Set :=
| Env_mk: Owner -> ParamTypeList -> TypeList -> Env
.
| Notation: pure context of a class |
Definition classEnv (C: ClassSym): Env :=
(Env_mk (Owner_class C) (nil) (nil))
.
| Notation: pure context of root |
Definition rootEnv: Env :=
(Env_mk (Owner_root) (nil) (nil))
.
| Property: all visible fields are implemented |
Definition IsComplete_fields (C: ClassSym) (fs: list FieldSym): Prop :=
forall (C': ClassSym) (f: FieldSym),
(Subclass C C') ->
(fieldOwner f) = C' ->
(In f fs)
.
| Property: all visible methods are implemented |
Definition IsComplete_methods (C: ClassSym): Prop :=
forall (C': ClassSym) (m: MethodSym),
(Subclass C C') ->
(methodOwner m) = C' ->
exists A: ClassSym, exists t: Term,
(Subclass C A) /\ (methodValue m A) = (Some t)
.
| Property: all visible types are implemented |
Definition IsComplete_types (C: ClassSym): Prop :=
forall (C': ClassSym) (L: TypeSym),
(Subclass C C') ->
(typeOwner L) = C' ->
exists A: ClassSym, exists T: type,
(Subclass C A) /\ (typeValue L A) = (Some T)
.
Relation: class C is complete when values for fields fs are provided
|
Inductive IsComplete: ClassSym -> (list FieldSym) -> Prop :=
| IsComplete_intro:
forall (C: ClassSym) (fs: list FieldSym),
(IsComplete_fields C fs) ->
(IsComplete_methods C) ->
(IsComplete_types C) ->
(IsComplete C fs)
.
Function: collects fields of fvs
|
Fixpoint fields_of_fieldValueList (fvs: FieldValueList): (list FieldSym) :=
match fvs with
| FieldValue_nil => nil
| (FieldValue_cons f _ fvs') => f :: (fields_of_fieldValueList fvs')
end
.
Predicate: list xs contains disjoint elements
|
Fixpoint List_disjoint (A: Set) (xs: (list A)) {struct xs}: Prop :=
match xs with
| nil => True
| x :: xs' =>
(forall (y: A), ~(In x xs')) /\ (List_disjoint A xs')
end
.
| Module containing a constraint on the types in the transitivity rule |
Module Type TransitivityConstraint.
Parameter applyTo: type -> type -> type -> Prop.
End TransitivityConstraint.
Module TypingRelations(TC: TransitivityConstraint).
| Relation: type assignment to paths |
Inductive PathTyping: Env -> Path -> type -> Prop :=
| P_This:
forall (G: Env) (C: ClassSym) (xTs: ParamTypeList) (Ts: TypeList) (S: type),
G = (Env_mk (Owner_class C) xTs Ts) ->
(Subtyping G (type_class C) S) ->
(PathTyping G (Path_this) S)
| P_Param:
forall (G: Env) (x: ParamSym) (O: Owner) (xTs: ParamTypeList) (Ts: TypeList) (T S: type),
G = (Env_mk O xTs Ts) ->
(In (x, T) xTs) ->
(Subtyping G T S) ->
(PathTyping G (Path_param x) S)
| P_Var:
forall (G: Env) (n: VarSym) (O: Owner) (xTs: ParamTypeList) (Ts: TypeList) (T S: type),
G = (Env_mk O xTs Ts) ->
((n < (length Ts)) /\ (TypeList_at Ts ((length Ts) - n - 1) T)) ->
(Subtyping G (lift_in_type T (n + 1)) S) ->
(PathTyping G (Path_var n) S)
| P_Value:
forall (G: Env) (C: ClassSym) (fvs: FieldValueList) (S: type),
(List_disjoint _ (fields_of_fieldValueList fvs)) ->
(FieldValueListTyping G C fvs) ->
(IsComplete C (fields_of_fieldValueList fvs)) ->
(Subtyping G (type_class C) S) ->
(PathTyping G (Path_value (Value_mk C fvs)) S)
| Relation: typing of fields with values |
with FieldValueListTyping: Env -> ClassSym -> FieldValueList -> Prop :=
| FieldValueListTyping_nil:
forall (G: Env) (C: ClassSym),
(FieldValueListTyping G C FieldValue_nil)
| FieldValueListTyping_cons:
forall (G: Env) (C: ClassSym)
(f: FieldSym) (v: Value) (fvs: FieldValueList) (T U: type),
(PathTyping G (Path_value v) U) ->
(type_is_closed U) ->
(fieldType f) = T ->
(Subtyping (classEnv C) U T) ->
(FieldValueListTyping G C fvs) ->
(FieldValueListTyping G C (FieldValue_cons f v fvs))
| Relation: subtyping |
with Subtyping: Env -> type -> type -> Prop :=
| S_Class:
forall (G: Env) (C: ClassSym),
(Subtyping G (type_class C) (type_class C))
| S_Extends:
forall (G: Env) (C C': ClassSym) (T: type),
(classSuper C) = (Some C') ->
(Subtyping G (type_class C') T) ->
(Subtyping G (type_class C) T)
| S_Up:
forall (G: Env) (p: Path) (L: TypeSym) (C: ClassSym) (T S: type),
(PathTyping G p (type_class C)) ->
(typeOwner L) = C ->
(typeUpperBound L) = T ->
(Subtyping G (thisSubst_in_type T p) S) ->
(Subtyping G (type_virtual p L) S)
| S_Down:
forall (G: Env) (p: Path) (L: TypeSym) (C: ClassSym) (T S: type),
(PathTyping G p (type_class C)) ->
(typeOwner L) = C ->
(typeLowerBound L) = (Some T) ->
(Subtyping G S (thisSubst_in_type T p)) ->
(Subtyping G S (type_virtual p L))
| S_Alias_Left:
forall (G: Env) (p: Path) (L: TypeSym) (C: ClassSym) (T S: type),
(PathTyping G p (type_class C)) ->
(typeValue L C) = (Some T) ->
(Subtyping G (thisSubst_in_type T p) S) ->
(Subtyping G (type_virtual p L) S)
| S_Alias_Right:
forall (G: Env) (p: Path) (L: TypeSym) (C: ClassSym) (T S: type),
(PathTyping G p (type_class C)) ->
(typeValue L C) = (Some T) ->
(Subtyping G S (thisSubst_in_type T p)) ->
(Subtyping G S (type_virtual p L))
| S_Virtual:
forall (G: Env) (p: Path) (L: TypeSym) (C: ClassSym),
(PathTyping G p (type_class C)) ->
(typeOwner L) = C ->
(Subtyping G (type_virtual p L) (type_virtual p L))
| S_Trans:
forall (G: Env) (T S U: type),
(Subtyping G T S) ->
(Subtyping G S U) ->
(TC.applyTo T S U) ->
(Subtyping G T U)
.
| Mutual induction schemes for typing and subtyping |
Scheme PathTyping_prop := Induction for PathTyping Sort Prop
with Subtyping_prop := Induction for Subtyping Sort Prop
with FieldValueListTyping_prop := Induction for FieldValueListTyping Sort Prop
.
| Mutual induction schemes for typing and field-value list typing |
Scheme PathTyping_prop2 := Induction for PathTyping Sort Prop
with FieldValueListTyping_prop2 := Induction for FieldValueListTyping Sort Prop
.
End TypingRelations.
| No constraint in the subtyping transitivity rule |
Module NoConstraint.
Definition applyTo (T: type) (S: type) (U: type): Prop := True.
End NoConstraint.
| Symbol-based constraint in the subtyping transitivity rule |
Module SymbolConstraint.
Definition applyTo (T: type) (S: type) (U: type): Prop := (typeRel S T) /\ (typeRel S U).
End SymbolConstraint.
Module StructuredTypingRelations := TypingRelations(SymbolConstraint).
Export StructuredTypingRelations.
| Relation: type assignment to paths |
Inductive Gen_PathTyping: Env -> Path -> type -> Prop :=
| Gen_P_This:
forall (G: Env) (C: ClassSym) (xTs: ParamTypeList) (Ts: TypeList) (S: type),
G = (Env_mk (Owner_class C) xTs Ts) ->
(Gen_Subtyping G (type_class C) S) ->
(Gen_PathTyping G (Path_this) S)
| Gen_P_Param:
forall (G: Env) (x: ParamSym) (O: Owner) (xTs: ParamTypeList) (Ts: TypeList) (T S: type),
G = (Env_mk O xTs Ts) ->
(In (x, T) xTs) ->
(Gen_Subtyping G T S) ->
(Gen_PathTyping G (Path_param x) S)
| Gen_P_Var:
forall (G: Env) (n: VarSym) (O: Owner) (xTs: ParamTypeList) (Ts: TypeList) (T S: type),
G = (Env_mk O xTs Ts) ->
((n < (length Ts)) /\ (TypeList_at Ts ((length Ts) - n - 1) T)) ->
(Gen_Subtyping G (lift_in_type T (n + 1)) S) ->
(Gen_PathTyping G (Path_var n) S)
| Gen_P_Value:
forall (G: Env) (C: ClassSym) (fvs: FieldValueList) (S: type),
(List_disjoint _ (fields_of_fieldValueList fvs)) ->
(Gen_FieldValueListTyping G C fvs) ->
(IsComplete C (fields_of_fieldValueList fvs)) ->
(Gen_Subtyping G (type_class C) S) ->
(Gen_PathTyping G (Path_value (Value_mk C fvs)) S)
| Relation: typing of fields with values |
with Gen_FieldValueListTyping: Env -> ClassSym -> FieldValueList -> Prop :=
| Gen_FieldValueListTyping_nil:
forall (G: Env) (C: ClassSym),
(Gen_FieldValueListTyping G C FieldValue_nil)
| Gen_FieldValueListTyping_cons:
forall (G: Env) (C: ClassSym)
(f: FieldSym) (v: Value) (fvs: FieldValueList) (T U: type),
(Gen_PathTyping G (Path_value v) U) ->
(type_is_closed U) ->
(fieldType f) = T ->
(Subtyping (classEnv C) U T) ->
(Gen_FieldValueListTyping G C fvs) ->
(Gen_FieldValueListTyping G C (FieldValue_cons f v fvs))
| Relation: subtyping |
with Gen_Subtyping: Env -> type -> type -> Prop :=
| Gen_S_Class:
forall (G: Env) (C: ClassSym),
(Gen_Subtyping G (type_class C) (type_class C))
| Gen_S_Extends:
forall (G: Env) (C C': ClassSym) (T: type),
(classSuper C) = (Some C') ->
(Gen_Subtyping G (type_class C') T) ->
(Gen_Subtyping G (type_class C) T)
| Gen_S_Up:
forall (G: Env) (p: Path) (L: TypeSym) (C: ClassSym) (T S: type),
(Gen_PathTyping G p (type_class C)) ->
(typeOwner L) = C ->
(typeUpperBound L) = T ->
(Gen_Subtyping G (thisSubst_in_type T p) S) ->
(Gen_Subtyping G (type_virtual p L) S)
| Gen_S_Down:
forall (G: Env) (p: Path) (L: TypeSym) (C: ClassSym) (T S: type),
(Gen_PathTyping G p (type_class C)) ->
(typeOwner L) = C ->
(typeLowerBound L) = (Some T) ->
(Gen_Subtyping G S (thisSubst_in_type T p)) ->
(Gen_Subtyping G S (type_virtual p L))
| Gen_S_Alias_Left:
forall (G: Env) (p: Path) (L: TypeSym) (C: ClassSym) (T S: type),
(Gen_PathTyping G p (type_class C)) ->
(typeValue L C) = (Some T) ->
(Gen_Subtyping G (thisSubst_in_type T p) S) ->
(Gen_Subtyping G (type_virtual p L) S)
| Gen_S_Alias_Right:
forall (G: Env) (p: Path) (L: TypeSym) (C: ClassSym) (T S: type),
(Gen_PathTyping G p (type_class C)) ->
(typeValue L C) = (Some T) ->
(Gen_Subtyping G S (thisSubst_in_type T p)) ->
(Gen_Subtyping G S (type_virtual p L))
| Gen_S_Virtual:
forall (G: Env) (p: Path) (L: TypeSym) (C: ClassSym),
(Gen_PathTyping G p (type_class C)) ->
(typeOwner L) = C ->
(Gen_Subtyping G (type_virtual p L) (type_virtual p L))
| Gen_S_Trans:
forall (G: Env) (T S U: type),
(Gen_Subtyping G T S) ->
(Gen_Subtyping G S U) ->
(NoConstraint.applyTo T S U) ->
(Gen_Subtyping G T U)
.
| Mutual induction schemes for typing and subtyping |
Scheme Gen_PathTyping_prop := Induction for Gen_PathTyping Sort Prop
with Gen_Subtyping_prop := Induction for Gen_Subtyping Sort Prop
with Gen_FieldValueListTyping_prop := Induction for Gen_FieldValueListTyping Sort Prop
.
| Mutual induction schemes for typing and field-value list typing |
Scheme Gen_PathTyping_prop2 := Induction for Gen_PathTyping Sort Prop
with Gen_FieldValueListTyping_prop2 := Induction for Gen_FieldValueListTyping Sort Prop
.
| Mutual induction schemes for typing and field-value list typing |
Scheme Gen_PathTyping_prop3 := Induction for Gen_PathTyping Sort Prop
with Gen_Subtyping_prop3 := Induction for Gen_Subtyping Sort Prop
.
Function: collects fields of fts
|
Fixpoint fields_of_fieldTermList (fts: FieldTermList): (list FieldSym) :=
match fts with
| FieldTerm_nil => nil
| (FieldTerm_cons f _ fts') => f :: (fields_of_fieldTermList fts')
end
.
Function: collects parameters of xts
|
Fixpoint params_of_paramTermList (xts: ParamTermList): (list ParamSym) :=
match xts with
| ParamTerm_nil => nil
| (ParamTerm_cons x _ xts') => x :: (params_of_paramTermList xts')
end
.
| Property: all parameters are represented |
Definition IsComplete_params (m: MethodSym) (xs: list ParamSym): Prop :=
forall (x: ParamSym),
(paramOwner x) = m ->
(In x xs)
.
| Relation: type assignment to terms |
Inductive Typing: Env -> Term -> type -> Prop :=
| T_This:
forall (G: Env) (C: ClassSym) (xTs: ParamTypeList) (Ts: TypeList) (S: type),
G = (Env_mk (Owner_class C) xTs Ts) ->
(Gen_Subtyping G (type_class C) S) ->
(Typing G (Term_this) S)
| T_Param:
forall (G: Env) (x: ParamSym) (O: Owner) (xTs: ParamTypeList) (Ts: TypeList) (T S: type),
G = (Env_mk O xTs Ts) ->
(In (x, T) xTs) ->
(Gen_Subtyping G T S) ->
(Typing G (Term_param x) S)
| T_Var:
forall (G: Env) (n: VarSym) (O: Owner) (xTs: ParamTypeList) (Ts: TypeList) (T S: type),
G = (Env_mk O xTs Ts) ->
((n < (length Ts)) /\ (TypeList_at Ts ((length Ts) - n - 1) T)) ->
(Gen_Subtyping G (lift_in_type T (n + 1)) S) ->
(Typing G (Term_var n) S)
| T_Select:
forall (G: Env) (p: Path) (f: FieldSym) (C: ClassSym) (S T: type),
(Gen_PathTyping G p (type_class C)) ->
(fieldOwner f) = C ->
(fieldType f) = T ->
(Gen_Subtyping G (thisSubst_in_type T p) S) ->
(Typing G (Term_select p f) S)
| T_Call:
forall (G: Env) (p: Path) (m: MethodSym) (xts: ParamTermList) (C: ClassSym) (S T: type),
(Gen_PathTyping G p (type_class C)) ->
(methodOwner m) = C ->
(methodType m) = T ->
(IsComplete_params m (params_of_paramTermList xts)) ->
(ParamTermListTyping G p m xts) ->
(Gen_Subtyping G (thisSubst_in_type T p) S) ->
(Typing G (Term_call p m xts) S)
| T_New:
forall (G: Env) (C: ClassSym) (fts: FieldTermList) (S: type),
(List_disjoint _ (fields_of_fieldTermList fts)) ->
(FieldTermListTyping G C fts) ->
(IsComplete C (fields_of_fieldTermList fts)) ->
(Gen_Subtyping G (type_class C) S) ->
(Typing G (Term_new C fts) S)
| T_Let:
forall (G: Env) (S T U: type) (t u: Term) (O: Owner) (xTs: ParamTypeList) (Ts: TypeList),
G = (Env_mk O xTs Ts) ->
(Typing G t T) ->
(Typing (Env_mk O xTs (app Ts (T :: nil))) u U) ->
~(var_in_type 0 U) ->
(Gen_Subtyping G (drop_in_type U) S) ->
(Typing G (Term_loc T t u) S)
| Relation: typing of parameters with values |
with ParamTermListTyping: Env -> Path -> MethodSym -> ParamTermList -> Prop :=
| ParamTermListTyping_nil:
forall (G: Env) (p: Path) (m: MethodSym),
(ParamTermListTyping G p m ParamTerm_nil)
| ParamTermListTyping_cons:
forall (G: Env) (p: Path) (m: MethodSym)
(x: ParamSym) (t: Term) (xts: ParamTermList) (T: type),
(paramType x) = T ->
(Typing G t (thisSubst_in_type T p)) ->
(ParamTermListTyping G p m xts) ->
(ParamTermListTyping G p m (ParamTerm_cons x t xts))
| Relation: typing of fields with values |
with FieldTermListTyping: Env -> ClassSym -> FieldTermList -> Prop :=
| FieldTermListTyping_nil:
forall (G: Env) (C: ClassSym),
(FieldTermListTyping G C FieldTerm_nil)
| FieldTermListTyping_cons:
forall (G: Env) (C: ClassSym)
(f: FieldSym) (t: Term) (fts: FieldTermList) (T U: type),
(Typing G t U) ->
(type_is_closed U) ->
(fieldType f) = T ->
(Subtyping (classEnv C) U T) ->
(FieldTermListTyping G C fts) ->
(FieldTermListTyping G C (FieldTerm_cons f t fts))
.
| Mutual induction schemes for term typing, parameters typing and fields typing |
Scheme Typing_prop := Induction for Typing Sort Prop
with ParamTermListTyping_prop := Induction for ParamTermListTyping Sort Prop
with FieldTermListTyping_prop := Induction for FieldTermListTyping Sort Prop
.
Lemma typeList_at_intro:
forall (Ts: TypeList) (n: nat),
(n < (length Ts)) ->
{ T: type | (TypeList_at Ts n T) }
.
Lemma typeList_at_elim:
forall (Ts: TypeList) (n: nat),
(exists T: type, (TypeList_at Ts n T)) ->
(n < (length Ts))
.
Lemma typeList_at_append:
forall (Ts Us: TypeList) (n: nat) (T: type),
(TypeList_at Ts n T) ->
(TypeList_at (Us ++ Ts) ((length Us) + n) T)
.
Lemma typeList_at_map:
forall (Ts: TypeList) (n: nat) (T: type) (f: type -> type),
(TypeList_at Ts n T) ->
(TypeList_at (map f Ts) n (f T))
.
Lemma typeList_at_cons:
forall (T U: type) (Ts: TypeList) (n: nat),
(n > 0) ->
(TypeList_at (T :: Ts) n U) ->
(TypeList_at Ts (pred n) U)
.
Lemma typeList_at_head:
forall (T U: type) (Ts: TypeList),
(TypeList_at (T :: Ts) 0 U) ->
U = T
.
End SetProgram.