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.