Definition of Syntax |
Require Import List.
| Programs |
Module Type Program.
| Symbols |
Parameter ClassSym : Set.
Parameter MethodSym : Set.
Parameter FieldSym : Set.
| Variables |
Definition Var : Set := nat.
Definition TypeVar : Set := nat.
| Decidability of equality for all kinds of symbols |
Axiom ClassSym_eqdec : forall (C C': ClassSym), { C = C' } + { C <> C' }.
Axiom FieldSym_eqdec : forall (f f': FieldSym), { f = f' } + { f <> f' }.
Axiom MethodSym_eqdec : forall (m m': MethodSym), { m = m' } + { m <> m' }.
| Type syntax |
Inductive TypeS: Set :=
| Type constructors -- K |
| Type_proj : TypeS -> nat -> TypeS
| Type_class : ClassSym -> TypeS
| Type_fun : TypeS -> TypeS -> TypeS
| Types -- T |
| Type_apply : TypeS -> TypeS -> TypeS
| Tuples of type constructors -- R |
| Type_var : TypeVar -> TypeS
| Type_tuple : TypeS -> TypeS
| Type constructor parameters (TCP) -- P |
| Type_param : TypeS -> TypeS -> TypeS
| Sections of type constructor parameters -- Pi |
| Type_section : TypeS -> TypeS
| Optional types -- T_opt |
| Type_none : TypeS
| Type_some : TypeS -> TypeS
| Lists of TCPs and type constructors -- Ps and Ks |
| Type_nil : TypeS
| Type_cons : TypeS -> TypeS -> TypeS
.
| Kinds -- k |
Inductive KindS: Set :=
| Kind_tuple : KindS -> KindS
| Kind_constr : KindS -> KindS
| Kind_nil : KindS
| Kind_cons : KindS -> KindS -> KindS
.
| Kinds categories -- c |
Inductive KindC: Set :=
| TupleKind : KindC
| ConstrKind : KindC
| ConstrKindList : KindC
.
Inductive Kind_WD: KindS -> KindC -> Prop :=
| WD_tuple:
forall (k: KindS),
(Kind_WD k ConstrKindList) ->
(Kind_WD (Kind_tuple k) TupleKind)
| WD_constr:
forall (k: KindS),
(Kind_WD k TupleKind) ->
(Kind_WD (Kind_constr k) ConstrKind)
| WD_nil:
(Kind_WD Kind_nil ConstrKindList)
| WD_cons:
forall (k ks: KindS),
(Kind_WD k ConstrKind) ->
(Kind_WD ks ConstrKindList) ->
(Kind_WD (Kind_cons k ks) ConstrKindList)
.
| Type categories |
| Type categories |
Inductive TypeC: Set :=
| TypeConstr : KindS -> TypeC
| Type_ : TypeC
| TypeTuple : KindS -> TypeC
| TypeParam : TypeC
| TypeSection : TypeC
| TypeOption : TypeC
| TypeParamList : TypeC
| TypeConstrList : KindS -> TypeC
.
| Builder: create a class type C<Ks> |
Definition Class_type (C: ClassSym) (R: TypeS): TypeS :=
(Type_apply (Type_class C) R)
.
| Builder: create a tuple type X@i<R> |
Definition Var_type (X: TypeVar) (i: nat) (R: TypeS): TypeS :=
(Type_apply (Type_proj (Type_var X) i) R)
.
| Builder: create a lambda-redex (<Pi> => T)<R> |
Definition Fun_type (Pi: TypeS) (T: TypeS) (R: TypeS): TypeS :=
(Type_apply (Type_fun Pi T) R)
.
Property: T is a class type -- N
|
Definition is_classType (T: TypeS): Prop :=
exists C: ClassSym, exists R: TypeS,
T = (Class_type C R)
.
| Terms -- t |
Inductive Term: Set :=
| Term_var : Var -> Term
| Term_select : Term -> FieldSym -> Term
| Term_call : Term -> MethodSym -> TypeS -> Term -> Term
| Term_new : TypeS -> Term -> Term
| Lists of terms -- ts |
| Term_nil : Term
| Term_cons : Term -> Term -> Term
| Lists of bindings from field symbols to terms -- fts |
| FieldTerm_nil : Term
| FieldTerm_cons : FieldSym -> Term -> Term -> Term
.
| Class attributes |
Parameter classTypeParams : ClassSym -> TypeS.
Parameter classSuper : ClassSym -> (option TypeS).
| Method attributes |
Parameter methodOwner : MethodSym -> ClassSym.
Parameter methodTypeParams : MethodSym -> TypeS.
Parameter methodParams : MethodSym -> (list TypeS).
Parameter methodType : MethodSym -> TypeS.
| Field attributes |
Parameter fieldOwner : FieldSym -> ClassSym.
Parameter fieldType : FieldSym -> TypeS.
| Method implementations |
Parameter methodImpl : MethodSym -> ClassSym -> (option Term).
| Main expression |
Parameter mainTerm : Term.
| Typing context for types and terms -- D(elta) and G(amma) |
Definition TypeEnv: Set := (list TypeS).
Definition TermEnv: Set := (list TypeS).
End Program.