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))
end
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'))
end.
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)
end
.
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) ->
False
.
Lemma path_to_term_call:
forall (p: Path) (q: Path) (m: MethodSym) (xts: ParamTermList),
(path_to_term p) = (Term_call q m xts) ->
False
.
Lemma path_to_term_let:
forall (p: Path) (T: type) (t u: Term),
(path_to_term p) = (Term_loc T t u) ->
False
.
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.