Library Syntax


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_proj : TypeS -> nat -> TypeS
    | Type_class : ClassSym -> TypeS
    | Type_fun : TypeS -> TypeS -> TypeS
  
    | Type_apply : TypeS -> TypeS -> TypeS
  
    | Type_var : TypeVar -> TypeS
    | Type_tuple : TypeS -> TypeS
  
    | Type_param : TypeS -> TypeS -> TypeS
  
    | Type_section : TypeS -> TypeS
  
    | Type_none : TypeS
    | Type_some : TypeS -> TypeS
  
    | 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

  
    | Term_nil : Term
    | Term_cons : Term -> Term -> Term

  
    | 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.