Library Subclassing

Definition of Subclassing

Require Import Calculus.
Require Import List.

Module SetProgram(My_Program: Program).

Import My_Program.

Relation: subclass
Inductive Subclass: ClassSym -> ClassSym -> Prop :=
  | SC_Class:
    forall (C: ClassSym),
      (Subclass C C)
  | SC_Extends:
    forall (A B C: ClassSym),
      (classSuper A) = (Some B) ->
      (Subclass B C) ->
      (Subclass A C)

Definition ParamValueList := (list (ParamSym * Value)).

Definition ValueList := (list Value).

Predicate: check membership of a given binding in a list of bindings (field symbol, value)
Inductive FieldValueList_contains: FieldValueList -> FieldSym -> Value -> Prop :=

  | FieldValueList_contains_head:
    forall (f: FieldSym) (v: Value) (fvs: FieldValueList),
      (FieldValueList_contains (FieldValue_cons f v fvs) f v)
  | FieldValueList_contains_tail:
    forall (f f': FieldSym) (v v': Value) (fvs: FieldValueList),
      (FieldValueList_contains fvs f v) ->
      (FieldValueList_contains (FieldValue_cons f' v' fvs) f v)

Equality on variable symbols is decidable
Lemma VarSym_eqdec:
  forall (n m: VarSym), { n = m } + { n <> m }

Function: converts a value to a term
Fixpoint value_to_term (v: Value): Term :=
  match v with
    | (Value_mk C fvs) => (Term_new C (fieldValueList_to_fieldTermList fvs))
  with fieldValueList_to_fieldTermList (fvs: FieldValueList): FieldTermList :=
  match fvs with
    | FieldValue_nil => FieldTerm_nil
    | (FieldValue_cons f v fvs') =>
      (FieldTerm_cons f (value_to_term v) (fieldValueList_to_fieldTermList fvs'))

Predicate: t is a value
Definition term_evaluated (t: Term): Prop :=
  exists v: Value, (value_to_term v) = t.

Function: promotes a path to a term
Definition path_to_term (p: Path): Term :=
  match p with
    | (Path_this) => Term_this
    | (Path_param x) => (Term_param x)
    | (Path_var n) => (Term_var n)
    | (Path_value v) => (value_to_term v)

Lemma path_to_term_this:
  forall (p: Path),
    (path_to_term p) = Term_this ->
    (p = Path_this)

Lemma path_to_term_param:
  forall (p: Path) (x: ParamSym),
    (path_to_term p) = (Term_param x) ->
    (p = (Path_param x))

Lemma path_to_term_var:
  forall (p: Path) (n: VarSym),
    (path_to_term p) = (Term_var n) ->
    (p = (Path_var n))

Lemma path_to_term_select:
  forall (p: Path) (q: Path) (f: FieldSym),
    (path_to_term p) = (Term_select q f) ->

Lemma path_to_term_call:
  forall (p: Path) (q: Path) (m: MethodSym) (xts: ParamTermList),
    (path_to_term p) = (Term_call q m xts) ->

Lemma path_to_term_let:
  forall (p: Path) (T: type) (t u: Term),
    (path_to_term p) = (Term_loc T t u) ->

Lemma path_to_term_new:
  forall (p: Path) (C: ClassSym) (fts: FieldTermList),
    (path_to_term p) = (Term_new C fts) ->
    exists v: Value,
      (p = (Path_value v)) /\ ((value_to_term v) = (Term_new C fts))

End SetProgram.

This page has been generated by coqdoc