Library Typing

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.

Index
This page has been generated by coqdoc