136 Type Definition Grammar

(************** Type definitions **************)

(****** Top-Level Structure ******)

TypeDefinitions = { Declaration };

Declaration = 
          NamespaceBlock
        | ValueTypeDecl 
        | EntityDecl 
        | TypeAliasDecl
        | EnumTypeDecl 
        | VariantTypeDecl
        | QuotientTypeDecl
        | RetroactiveSubtypeDecl
        | SubtypeEmbeddingDecl
        | MutuallyDisjointTypesDecl
        | ConstantDecl
        | FunctionDecl
        | ProcedureDecl
        | FoldDecl
        | ExternBlockDecl;

NamespaceBlock =
    "namespace", QualifiedNamespaceName, 
    "{", 
        TypeDefinitions, 
    "}";


(****** Nominal Type Declarations ******)

ValueTypeDecl = 
        [MetaData], 
        [ "abstract" ], "value", [ "unordered" ], TypeName,
        [ GenericParameterList ], [ SuperTypeList ],
        [ GenericWhereClause ],
        "{", 
            { ValueTypeBodyItem },
        "}";

EntityDecl = 
        [MetaData], 
        [ "abstract" ], "entity", [ "unordered" ], TypeName,
        [ GenericParameterList ], [ SuperTypeList ],
        [ GenericWhereClause ],
        "{", 
            { EntityTypeBodyItem },
        "}";

ValueTypeBodyItem =
          FieldDecl
        | OrderDecl
        | TypeEvolutionItem
        | Constraints
        | Theorems;

EntityTypeBodyItem =
          FieldDecl
        | KeyConstraint
        | OrderDecl
        | TypeEvolutionItem
        | Constraints
        | Theorems;

EnumTypeDecl =
        [MetaData],
        "enum", [ "unordered" ], TypeName,
        [ GenericParameterList ],
        [ ( ":", EnumStorageType ) | SuperTypeList ],
        [ GenericWhereClause ],
        "{",
            { EnumTypeBodyItem },
        "}";

EnumStorageType =
          "Int8" | "Int16" | "Int32" | "Int64"
        | "Uint8" | "Uint16" | "Uint32" | "Uint64";

EnumTypeBodyItem =
          EnumAttributeDecl, [ "," ]
        | [MetaData], DerivedFieldDecl, ";";

EnumAttributeDecl =
          CurrentEnumAttributeDecl
        | DroppedEnumAttributeDecl;

CurrentEnumAttributeDecl =
        AttributeName, [ "=", Expression ];

DroppedEnumAttributeDecl =
        "dropped", AttributeName, [ "=", Expression ], "as", AttributeName;

(* The final "as" in DroppedEnumAttributeDecl introduces the replacement attribute. If the
   representation-value expression contains rename expressions, the final
   "as" is therefore the delimiter and any earlier occurrences belong to the
   expression. *)

VariantTypeDecl =
        [MetaData],
        "variant", [ "unordered" ], TypeName,
        [ GenericParameterList ], [ SuperTypeList ],
        [ GenericWhereClause ],
        "{",
            { VariantFieldDecl },
            [ OrderDecl ],
            [Constraints],
            [Theorems]
        "}";

VariantFieldDecl =
          CurrentVariantFieldDecl
        | DroppedVariantFieldDecl;

CurrentVariantFieldDecl =
        [MetaData],
        (
              CurrentVariantAttributeDecl, [ WhereClause ]
            | DerivedFieldDecl
        ),
        ";";

CurrentVariantAttributeDecl =
        TypedAttribute | AttributeName;

DroppedVariantFieldDecl =
        [MetaData],
        "dropped",
        ( TypedAttribute | AttributeName ),
        "as",
        AttributeName,
        [ "=", Expression ],
        ";";

TypeAliasDecl =
        [MetaData],
        "type", TypeName, [GenericParameterList], [ GenericWhereClause ], "=",
        TypeExpression, ";";

QuotientTypeDecl = 
        [MetaData], 
        "quotient", TypeName, [GenericParameterList], [SuperTypeList],
        [ GenericWhereClause ],
        "{", 
            { FieldDecl }, 
            "equivalence",
            "{",
                Identifier, "~", Identifier, "where", Expression, ";",
            "}",
            [ OrderDecl ],
            [Constraints],
            [Theorems]
        "}";

SuperTypeList = "isa", QualifiedTypeName, { ",", QualifiedTypeName };

RetroactiveSubtypeDecl =
        QualifiedTypeName, SuperTypeList, ";";

SubtypeEmbeddingDecl =
        [MetaData],
        "embed", TypeExpression, Identifier, "isa", TypeExpression,
        "=", Expression, ";";

MutuallyDisjointTypesDecl =
        "disjoint", TypeExpressionList, ";";

GenericParameterList =
        "<", [ GenericParameter, { ",", GenericParameter } ], ">";

GenericParameter =
        [MetaData],
        TypeExpression,
        Identifier,
        [ "=", GenericArgument ];

GenericArgumentList =
        GenericArgument, { ",", GenericArgument };

GenericArgument =
        TypeExpression | Expression;

GenericWhereClause =
        "where", GenericConstraint, { ",", GenericConstraint };

GenericConstraint =
          Identifier, "isa", TypeExpression
        | Expression;


(****** Field Declarations ******)

FieldDecl = 
        [MetaData],
        (
              MemberEmbedDecl
            | TypedAttribute, [ WhereClause ]
            | DerivedFieldDecl
        ),
        ";";

OrderDecl =
        "order", "[", OrderKey, { ",", OrderKey }, "]", ";";

OrderKey =
        Expression, [ OrderDirection ];

OrderDirection =
          "↑"
        | "↓";

MemberEmbedDecl =
        "embed", QualifiedTypeName, [ "as", AttributeName ];

TypedAttribute = 
        TypeExpression, AttributeWithCardinality;

AttributeWithCardinality =
        AttributeName, CardinalityQualifier;

CardinalityQualifier =  ε  
                     | "*" 
                     | "+" 
                     | "?"
                     | "[", CardinalityBound,
                         [ "..", ( "*" | "∞" | CardinalityBound ) ], "]";

CardinalityBound = AdditiveExpression;

TypeExpression =
          RefinementTypeExpression
        | TypeExpressionNoRefinement;

RefinementTypeExpression =
        "subtype", TypeExpressionNoRefinement, "where", Expression;

TypeExpressionNoRefinement =
          ObjectTypeExpression
        | NamedTypeExpression
        | TupleTypeExpression
        | UnionTypeExpression
        | IntersectionTypeExpression
        | "(", TypeExpression, ")";

ObjectTypeExpression =
        "object", TypeExpressionNoRefinement;

NamedTypeExpression =
        QualifiedTypeName, [ TypeGenericApplication ];

TypeGenericApplication =
        "<", [ GenericArgumentList ], ">";

TupleTypeExpression =
        "{", 
            [ TypedAttribute, { ";", TypedAttribute }, [ ";" ] ],
        "}";

UnionTypeExpression =
        "union", "{", TypeExpressionList, "}";

IntersectionTypeExpression =
        "intersection", "{", TypeExpressionList, "}";

TypeExpressionList =
        TypeExpression, { ",", TypeExpression };

DerivedFieldDecl =
        "→", OptTypedAttribute, "=", DerivedFieldDefinition;

DerivedFieldDefinition =
          "either", Expression, ",", Expression, { ",", Expression }
        | Expression;

OptTypedAttribute = 
        TypedAttribute | AttributeWithCardinality;


(****** Schema Evolution ******)

TypeEvolutionItem =
          DroppedAttributesBlock
        | SchemaEvolutionBlock
        | EvolveBlock;

DroppedAttributesBlock =
        "dropped",
        "{",
            { DroppedAttributeDecl },
        "}";

DroppedAttributeDecl =
        [MetaData],
        TypedAttribute,
        [ WhereClause ],
        ";";

SchemaEvolutionBlock =
        "schema",
        "{",
            { SchemaReleaseDecl, [ ";" ] },
        "}";

SchemaReleaseDecl =
        IntegerLiteral, ":", { SchemaChange, [ "," ] };

SchemaChange =
          "+", AttributeName
        | "-", AttributeName;

EvolveBlock =
        "evolve",
        "{",
            { EvolveFunctionDecl },
        "}";

EvolveFunctionDecl =
        AttributeName, "(", [ EvolveParameterList ], ")",
        "{", AttributeName, "=", Expression, ";", "}";

EvolveParameterList =
        Identifier, { ",", Identifier };


(****** Keys, constraints, and theorems ******)

KeyConstraint = 
        "key", 
        "{", 
            AttributeName, { ",", AttributeName }, 
        "}", ";";

Constraints =
        "constraints",
        "{",
            { ConstraintDecl },
        "}";

ConstraintDecl = DisjointConstraint | ExpressionConstraint;

DisjointConstraint = 
        "disjoint", 
        "{", 
            AttributePath, { ",", AttributePath }, 
        "}", ";";

AttributePath  = AttributeName, { ".", AttributeName };

ExpressionConstraint = Expression, ";";

Theorems =
        "theorems",
        "{",
            { TheoremDecl }, 
        "}";

TheoremDecl = DisjointConstraint | ExpressionConstraint;


(****** Constants, functions, procedures, and folds ******)

ConstantDecl =
        [MetaData],
        "const", [ TypeExpression ], Identifier,
        [ GenericParameterList ], [ GenericWhereClause ], "=", Expression, ";";

FunctionDecl =
        [MetaData],
        "func", TypeExpression, FunctionName, [CallableGenericClause],
        "(", [ FunctionParameterList ], ")",
        FunctionBody;

CallableGenericClause =
        GenericParameterList, [ GenericWhereClause ];

FunctionBody =
          "=", Expression, ";"
        | BlockStatement;

ProcedureDecl =
        [MetaData],
        "proc", ProcedureName, [CallableGenericClause],
        "(", [ ProcedureParameterList ], ")",
        BlockStatement;

FoldDecl =
        [MetaData],
        "fold", TypeExpression, FoldName, [GenericParameterList],
        [ "(", [ FoldParameterList ], ")" ],
        FoldDeclTail, ";";

FoldParameterList =
        ReadOnlyParameter, { ",", ReadOnlyParameter };

FoldDeclTail =
      [ GenericWhereClause ], "=", "Σ", FoldBlock
    | "over", Identifier, [ GenericWhereClause ], "=", Expression,
        [ DefinedWhereClause ];

DefinedWhereClause =
        "defined", WhereClause;

ExternBlockDecl =
        "extern", StringLiteral,
        "{",
            { ExternFunctionDecl },
        "}";

ExternFunctionDecl =
        [MetaData],
        TypeExpression, FunctionName, [CallableGenericClause],
        "(", [ ReadOnlyParameterList ], ")",
        ";";

FunctionName =
          Identifier
        | SymbolicFunctionName;

SymbolicFunctionName =
          "=" | "≠"
        | "<" | ">" | "≤" | "≥"
        | "⊂" | "⊃" | "⊆" | "⊇" | "⊄" | "⊅"
        | "∈" | "∉"
        | "+" | "-" | "*" | "/" | "^"
        | "∩" | "∪" | "∖" | "\"
        | "⊓" | "⊔" | "⨝" | "|"
        | "⇒" | "→" | "←" | "↔"
        | "∧" | "∨" | "¬";

ProcedureName =
        Identifier;

WhereClause =
        "where", Expression, { ",", Expression };

FunctionParameterList =
        FunctionParameter, { ",", FunctionParameter };

FunctionParameter =
        [ "^" ], TypeExpression, Identifier;

ProcedureParameterList =
        ProcedureParameter, { ",", ProcedureParameter };

ProcedureParameter =
        [ "&" | "^" ], TypeExpression, Identifier;

ReadOnlyParameterList =
        ReadOnlyParameter, { ",", ReadOnlyParameter };

ReadOnlyParameter =
        TypeExpression, Identifier;