Library Semantics

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.

This page has been generated by coqdoc