Library Calculus






Definition of Syntax



Require Import List.

Programs

Module Type Program.

Symbols

  Parameter ClassSym : Set.
  Parameter TypeSym : Set.
  Parameter FieldSym : Set.
  Parameter MethodSym : Set.
  Parameter ParamSym : Set.
  Definition VarSym : Set := nat.

Decidability of equality for all kinds of symbols

  Axiom ClassSym_eq : forall (C C': ClassSym), { C = C' } + { C <> C' }.
  Axiom TypeSym_eq : forall (L L': TypeSym), { L = L' } + { L <> L' }.
  Axiom FieldSym_eq : forall (f f': FieldSym), { f = f' } + { f <> f' }.
  Axiom MethodSym_eq : forall (m m': MethodSym), { m = m' } + { m <> m' }.
  Axiom ParamSym_eq : forall (x x': ParamSym), { x = x' } + { x <> x' }.

Well-founded relation over class and type symbols

  Definition Sym: Set := (ClassSym + TypeSym)%type.
  Parameter symRel: Sym -> Sym -> Prop.

Values

  Inductive Value: Set :=
    | Value_mk: ClassSym -> FieldValueList -> Value

Lists of bindings from field symbols to values

  with FieldValueList: Set :=
    | FieldValue_nil : FieldValueList
    | FieldValue_cons : FieldSym -> Value -> FieldValueList -> FieldValueList
  .

Mutual induction schemes for values

  Scheme Value_prop := Induction for Value Sort Prop
    with FieldValueList_prop := Induction for FieldValueList Sort Prop
  .
  Scheme Value_set := Induction for Value Sort Set
    with FieldValueList_set := Induction for FieldValueList Sort Set
  .

Paths

  Inductive Path: Set :=
    | Path_this : Path
    | Path_param : ParamSym -> Path
    | Path_var : VarSym -> Path
    | Path_value : Value -> Path
  .

Types

  Inductive type : Set :=
    | type_virtual: Path -> TypeSym -> type
    | type_class: ClassSym -> type
  .

Terms

  Inductive Term: Set :=
    | Term_this : Term
    | Term_param : ParamSym -> Term
    | Term_var : VarSym -> Term
    | Term_select : Path -> FieldSym -> Term
    | Term_new : ClassSym -> FieldTermList -> Term
    | Term_call : Path -> MethodSym -> ParamTermList -> Term
    | Term_loc : type -> Term -> Term -> Term

Lists of bindings from field symbols to terms

  with FieldTermList: Set :=
    | FieldTerm_nil : FieldTermList
    | FieldTerm_cons : FieldSym -> Term -> FieldTermList -> FieldTermList

Lists of bindings from parameter symbols to terms

  with ParamTermList: Set :=
    | ParamTerm_nil : ParamTermList
    | ParamTerm_cons : ParamSym -> Term -> ParamTermList -> ParamTermList
  .

Mutual induction schemes for terms

  Scheme Term_prop := Induction for Term Sort Prop
    with FieldTermList_prop := Induction for FieldTermList Sort Prop
    with ParamTermList_prop := Induction for ParamTermList Sort Prop
  .

Class attributes

  Parameter classSuper : ClassSym -> (option ClassSym).
  
Type member attributes

  Parameter typeOwner : TypeSym -> ClassSym.
  Parameter typeUpperBound : TypeSym -> type.
  Parameter typeLowerBound : TypeSym -> (option type).
  Parameter typeValue : TypeSym -> ClassSym -> (option type).

Field attributes

  Parameter fieldOwner : FieldSym -> ClassSym.
  Parameter fieldType : FieldSym -> type.

Method attributes

  Parameter methodOwner : MethodSym -> ClassSym.
  Parameter methodType : MethodSym -> type.
  Parameter methodValue : MethodSym -> ClassSym -> (option Term).

Parameter attributes

  Parameter paramOwner : ParamSym -> MethodSym.
  Parameter paramType : ParamSym -> type.

Main expression

  Parameter main : Term.

List of parameters of a method

  Axiom method_parameters_spec:
    forall (m: MethodSym), { xTs: (list (ParamSym * type)) |
      forall (x: ParamSym) (T: type),
        ((paramOwner x) = m /\ (paramType x) = T) <-> (In (x, T) xTs)
    }
  .

End Program.

Index
This page has been generated by coqdoc