Definition of Semantics |
Require Import Calculus.
Require Import Arith.
Require Import List.
Module SetProgram(My_Program: Program).
Import My_Program.
Require Typing.
Module My_Typing := Typing.SetProgram(My_Program).
Import My_Typing.
Import My_TypeOrdering.
Import My_DeBruijn.
Import My_Substitutions.
Import My_Subclassing.
| Relation: reduction of terms |
Inductive Red_term: Term -> Term -> Prop :=
| R_Select:
forall (C: ClassSym) (fvs: FieldValueList) (f: FieldSym) (v: Value),
(FieldValueList_contains fvs f v) ->
(Red_term (Term_select (Path_value (Value_mk C fvs)) f) (value_to_term v))
| R_Field:
forall (C: ClassSym) (fts fts': FieldTermList),
(Red_fieldTermList fts fts') ->
(Red_term (Term_new C fts) (Term_new C fts'))
| R_Arg:
forall (v: Value) (m: MethodSym) (xts xts': ParamTermList),
(Red_paramTermList xts xts') ->
(Red_term (Term_call (Path_value v) m xts) (Term_call (Path_value v) m xts'))
| R_Local:
forall (T: type) (t u t': Term),
(Red_term t t') ->
(Red_term (Term_loc T t u) (Term_loc T t' u))
| R_Let:
forall (T: type) (t u: Term) (v: Value),
(value_to_term v) = t ->
(Red_term (Term_loc T t u) (varSubst_in_term u 0 v))
| R_Call:
forall (C C': ClassSym) (v: Value) (fws: FieldValueList) (m: MethodSym)
(xts: ParamTermList) (xvs: list (ParamSym * Value)) (t: Term),
v = (Value_mk C fws) ->
(Subclass C C') ->
(methodValue m C') = (Some t) ->
(paramValueList_to_ParamTermList xvs) = xts ->
(Red_term (Term_call (Path_value v) m xts) (map_paramSubst_in_term (thisSubst_in_term t (Path_value v)) xvs))
| Relation: reduction of field bindings |
with Red_fieldTermList: FieldTermList -> FieldTermList -> Prop :=
| R_FieldTermList_head:
forall (f: FieldSym) (t u: Term) (fts: FieldTermList),
(Red_term t u) ->
(Red_fieldTermList (FieldTerm_cons f t fts) (FieldTerm_cons f u fts))
| R_FieldTermList_tail:
forall (f: FieldSym) (t: Term) (fts fts': FieldTermList),
(term_evaluated t) ->
(Red_fieldTermList fts fts') ->
(Red_fieldTermList (FieldTerm_cons f t fts) (FieldTerm_cons f t fts'))
| Relation: reduction of parameter bindings |
with Red_paramTermList: ParamTermList -> ParamTermList -> Prop :=
| R_ParamTermList_head:
forall (x: ParamSym) (t u: Term) (xts: ParamTermList),
(Red_term t u) ->
(Red_paramTermList (ParamTerm_cons x t xts) (ParamTerm_cons x u xts))
| R_ParamTermList_tail:
forall (x: ParamSym) (t: Term) (xts xts': ParamTermList),
(term_evaluated t) ->
(Red_paramTermList xts xts') ->
(Red_paramTermList (ParamTerm_cons x t xts) (ParamTerm_cons x t xts'))
.
| Relation: evaluation of a term |
Inductive Evaluate: Term -> Value -> Prop :=
| Evaluate_end:
forall (t: Term) (v: Value),
(value_to_term v) = t ->
(Evaluate t v)
| Evaluate_step:
forall (t u: Term) (v: Value),
(Red_term t u) ->
(Evaluate u v) ->
(Evaluate t v)
.
| Relation: evaluation of the main expression of the program |
Definition EvaluateMain (v: Value): Prop :=
(Evaluate main v)
.
End SetProgram.