Appendix B: LALR (1) Grammar

B1. Introduction

In the following grammar, keywords are display in bold. Other terminal symbols have UPPERCASE names and the following meanings:

ARROW	-> or <- or <->
DBLCOLON	::
DEFAS	^=
DEFINEorREDEFINE	define or redefine
DOTDOTDOT	...
EMPTYSTRINGLITERAL	The empty string literal, i.e. ""
IDENTIFIER	An identifier
ITorSELF	it or self
LITERAL	A character, integer or real literal token, or one of false null true
NONEMPTYSTRINGLITERAL	Any string literal except the empty string literal
NOT	~
OP0	==> or <== or <==>
OP3	<= or <<= or >= or >>= or << or >>
OP3M	< or >
OP4	++ or --
OP4M	+ or -
OP5	** or %% or ##
OP5M	* or % or / or #
OP6	..
OP6M	^
OPAND	&
OPEQUAL	=
OPOR	\|
OPPROPERTY	associative, commutative or idempotent
OPRANK	~~
PREDEFCLASS	bag, map, seq or set
PREDEFTYPE	bool, byte, char, int, rank, real or void
SUCHTHAT	:-
THATorANY	that or any
TYPEOP	lowest or highest
UNITE	\|\|

The symbol 'Empty' means the empty string and the symbol 'EndOfFile' means the end of the source text. Comments are italicised.

B2. Grammar

Goal:
OptImportList GeneralDeclarations OptSEMI EndOfFile.

----------------------- Import lists -----------------------

OptImportList:
Empty;
OptImportList ImportItemList ';'.

ImportItemList:
import ImportName;
ImportItemList ',' ImportName.

ImportName:
NONEMPTYSTRINGLITERAL.

----------------- Declarations and declaration lists ----------------

- The following declarations can all occur after nonmember or in a global or local declaration list
FunctionEtcDeclaration:
FunctionDeclaration;
SchemaDeclaration.

- The following can all occur as class members
MemberFunctionEtcDeclaration:
    early PlainMemberFunctionEtcDeclaration;
    final PlainMemberFunctionEtcDeclaration;
    PlainMemberFunctionEtcDeclaration.

PlainMemberFunctionEtcDeclaration:
    FunctionDeclaration;
    SelectorDeclaration;
    MemberOperatorDeclaration;
    SchemaDeclaration;
    ModifyingSchemaDeclaration.

TheoremOrAxiomDeclaration:
TheoremDeclaration;
AxiomDeclaration.

NonmemberFunctionEtcDeclaration:
nonmember FunctionEtcDeclaration.

NonmemberTheoremOrAxiomDeclaration:
nonmember TheoremOrAxiomDeclaration.

ModifiedMemberFunctionEtcDeclaration:
DEFINEorREDEFINE MemberFunctionEtcDeclaration;
MemberFunctionEtcDeclaration.

- Deferred function and schema declarations are allowed together (i.e. only in class non-internal member sections)
DeferredDeclaration:
    deferred FunctionHeader OptRequire OptPrecondition OptRecursionVariant OptPostAssertion;
    deferred SelectorHeader OptRequire OptPrecondition OptRecursionVariant OptPostAssertion;
    deferred MemberOperatorHeader ':' TypeExpression OptRequire OpProperties OptPrecondition OptRecursionVariant OptPostAssertion;
    deferred SchemaHeader OptRequire OptPrecondition OptRecursionVariant OptPostAssertion;
    deferred ModifyingSchemaHeader OptRequire OptPrecondition OptRecursionVariant OptPostAssertion.

MemberFSOSPrototype:
    FunctionPrototype;
    SelectorPrototype;
    OperatorPrototype;
    SchemaPrototype.

AbsurdDeclaration:
    AbsurdFunctionDeclaration;
    AbsurdSelectorDeclaration;
    AbsurdOperatorDeclaration;
    AbsurdSchemaDeclaration.

- A general declaration may occur at the global level of the program
GeneralDeclaration:
    ConstantDeclarations;
    FunctionEtcDeclaration;
    TheoremOrAxiomDeclaration;
    ClassOrTypeDeclaration;
    HeapDeclarations.

- A local declaration may not include constant declarations. We treat variable and let-declarations separately.
LocalDeclaration:
    FunctionEtcDeclaration;
    TheoremOrAxiomDeclaration;
    ClassOrTypeDeclaration.

- Now for an abstract member declaration. We allow nonmember declarations
AbstractMemberDeclaration:
    ConstantDeclarations;
    AbstractVariableDeclarations;
    MemberFunctionEtcDeclaration;
    TheoremOrAxiomDeclaration;
    ModifyingTheoremDeclaration;
    NonmemberFunctionEtcDeclaration;
    NonmemberTheoremOrAxiomDeclaration;
    ConstructorDeclaration;
    ClassOrTypeDeclaration;
    HeapDeclarations;
    ClassInvariant;
    HistoryInvariant.

HeapDeclarations:
heap IdentifierOptPragmaList.

- Internal members may be anything which may be a general declaration, or a redeclaration of an abstract member
InternalMemberDeclaration:
    ConstantDeclarations;
    VariableDeclarations;
    MemberFunctionEtcDeclaration;
    TheoremOrAxiomDeclaration;
    ModifyingTheoremDeclaration;
    NonmemberFunctionEtcDeclaration;
    NonmemberTheoremOrAxiomDeclaration;
    ConstructorDeclaration;
    ClassOrTypeDeclaration;
    HeapDeclarations;
    ClassInvariant;
    InternalRedeclaration.

InternalRedeclaration:
    - Redeclarations of abstract variables as internal functions
    function SimpIdentifier DEFAS Expression OptImplementation;
    - Reimplementations of other abstract members
    function SimpIdentifier OptParmList Implementation;
    MemberOperatorHeader2 Implementation;
    EqualityOperatorHeader Implementation;
    selector SimpIdentifier OptParmList Implementation;
    selector IndexOp OptParmList Implementation;
    schema SimpIdentifier OptSchemaParmList Implementation;
    ModifyingSchemaHeader2 Implementation;
    schema '!' RedefinableOp OperatorParam Implementation;
    build '{' OptConstructorParams '}' Implementation.

ClassParameterList:
SimpIdentifier;
ClassParameterList Separator SimpIdentifier.

TwoOrMoreSimpIdentifiers:
SimpIdentifier ',' SimpIdentifier;
TwoOrMoreSimpIdentifiers ',' SimpIdentifier.

SimpIdentifierList:
SimpIdentifier;
TwoOrMoreSimpIdentifiers.

- Interface members may not be variables, constants, classes, types or templates but may be redeclarations of abstract members
InterfaceOrConfinedDeclaration:
    ModifiedMemberFunctionEtcDeclaration;
    TheoremOrAxiomDeclaration;
    ModifyingTheoremDeclaration;
    NonmemberFunctionEtcDeclaration;
    NonmemberTheoremOrAxiomDeclaration;
    ConstructorDeclaration;
    DeferredDeclaration;
    AbsurdDeclaration;
    InterfaceRedeclarations.

InterfaceRedeclarations:
    function SimpIdentifierList;
    ghost function SimpIdentifierList;
    selector SimpIdentifierList;
    ghost selector SimpIdentifierList.

----------------------- Declaration lists ------------------------

GeneralDeclarations:
    GeneralDeclaration;
    GeneralDeclarationWithPragma;
    GeneralDeclarations ';' GeneralDeclaration;
    GeneralDeclarations ';' GeneralDeclarationWithPragma.

GeneralDeclarationWithPragma:
Pragma ';' GeneralDeclaration.

----------------------- Forms of declaration ----------------------

ConstantDeclarations:
const ConstDeclList;
ghost const ConstDeclList.

ConstDeclList:
ConstDeclItem;
ConstDeclList ',' ConstDeclItem.

ConstDeclItem:
IdentifierOptPragma ':' TypeExpression DEFAS Expression OptNvImplementation;
IdentifierOptPragma DEFAS Expression OptNvImplementation.

VariableDeclarations:
var DataDeclarationList.

AbstractVariableDeclarations:
VariableDeclarations;
ghost VariableDeclarations.

DataDeclarationList:
DataDeclarations;
DataDeclarationList ',' DataDeclarations.

DataDeclarations:
    TwoOrMoreIdentifiersOptPragma ':' PossConstrainedTypeExpression;
    IdentifierOptPragma ':' PossConstrainedTypeExpression;
    IdentifierOptPragma ':' AbbrevTypeExpr;
    when GuardedDataDeclarationList end.

TwoOrMoreIdentifiersOptPragma:
IdentifierOptPragma ',' IdentifierOptPragma;
TwoOrMoreIdentifiersOptPragma ',' IdentifierOptPragma.

GuardedDataDeclarationList:
'[' Expression ']' ':' DataDeclarationList;
'[' Expression ']' ':' DataDeclarationList ',' GuardedDataDeclarationList.

- Function and schema declarations

FunctionDeclaration:
FunctionHeader OptExceptionSignature OptRequire OptPrecondition OptRecursionVariant FunctionBody.

FunctionHeader:
    FunctionHeader2;
    opaque FunctionHeader2;
    ghost FunctionHeader2.

FunctionHeader2:
function SimpIdentifier OptParmList FunctionType;
function IdWithPragma OptParmList FunctionType.

FunctionBody:
DEFAS PossiblyMultipleExpression OptImplementation OptPostAssertion;
satisfy ListOfPredicates OptImplementation OptPostAssertion.

FunctionPrototype:
FunctionHeader OptExceptionSignature OptRequire OptPrecondition OptPostAssertion.

AbsurdFunctionDeclaration:
absurd FunctionHeader.

SelectorDeclaration:
SelectorHeader OptExceptionSignature OptRequire OptPrecondition OptRecursionVariant DEFAS Expression OptImplementation OptPostAssertion.

SelectorHeader:
    SelectorHeader2;
    opaque SelectorHeader2;
    ghost SelectorHeader2.

SelectorHeader2:
    selector SimpIdentifier OptParmList ':' TypeExpression;
    selector SimpIdentifier OptParmList ':' limited TypeExpression;
    selector IdWithPragma OptParmList ':' TypeExpression;
    selector IdWithPragma OptParmList ':' limited TypeExpression;
    selector IndexOp OptParmList ':' TypeExpression;
    selector IndexOp OptParmList ':' limited TypeExpression;
    selector IndexOpWithPragma OptParmList ':' TypeExpression;
    selector IndexOpWithPragma OptParmList ':' limited TypeExpression.

SelectorPrototype:
SelectorHeader OptExceptionSignature OptRequire OptPrecondition OptPostAssertion.

AbsurdSelectorDeclaration:
absurd SelectorHeader.

MemberOperatorDeclaration:
MemberOperatorHeader ':' TypeExpression OptExceptionSignature OptRequire OpProperties OptPrecondition OptRecursionVariant OperatorBody.

EqualityOrRankDeclaration:
    GhostEqualityOperatorHeader;
    EqualityOperatorHeader;
    RankOperatorHeader OptRecursionVariant OperatorBody.

OperatorBody:
DEFAS Expression OptImplementation OptPostAssertion;
satisfy ListOfPredicates OptImplementation OptPostAssertion.

OperatorPrototype:
MemberOperatorHeader ':' TypeExpression OptExceptionSignature OptRequire OptPrecondition OptPostAssertion.

EqualityOrRankPrototype:
EqualityOperatorHeader;
RankOperatorHeader.

AbsurdOperatorDeclaration:
absurd MemberOperatorHeader ':' TypeExpression.

MemberOperatorHeader:
    MemberOperatorHeader2;
    opaque MemberOperatorHeader2;
    ghost MemberOperatorHeader2.

MemberOperatorHeader2:
    LeftOperatorHeader;
    RightOperatorHeader;
    NeitherOperatorHeader.

LeftOperatorHeader:
operator OperatorParam RevRedefinableOp;
operator OperatorParam RevRedefinableOpWithPragma

RightOperatorHeader:
operator RedefinableOp OperatorParam;
operator RedefinableOpWithPragma OperatorParam.

EqualityOperatorHeader:
operator OPEQUAL TypelessOperatorParam.

GhostEqualityOperatorHeader:
ghost EqualityOperatorHeader.

RankOperatorHeader:
RankOperatorHeader2;
total RankOperatorHeader2.

RankOperatorHeader2:
operator OPRANK TypelessOperatorParam.

NeitherOperatorHeader:
operator RedefinableOp;
operator RedefinableOpWithPragma.

OpProperties:
SimpleOpProperties;
SimpleOpProperties identity Expression.

SimpleOpProperties:
SimpleOpProperties OPPROPERTY;
Empty.

Precondition:
pre ListOfPredicates.

OptPrecondition:
Precondition;
Empty.

OptParmList:
'(' FormalParams ')';
Empty.

FormalParams:
    FormalParameterList;
    RepeatedParams;
    FormalParameterList Separator RepeatedParams.

RepeatedParams:
repeated FormalParameterList.

FormalParameterList:
ParameterDeclarations;
FormalParameterList Separator ParameterDeclarations.

Separator:
',';
ARROW.

OperatorParam:
'(' SingleParm ')'.

TypelessOperatorParam:
'(' IdentifierOptPragma ')'.

ParameterDeclarations:
SingleParm;
TwoOrMoreParameters ':' ParameterType.

SingleParm:
IdentifierOptPragma ':' ParameterType.

TwoOrMoreParameters:
IdentifierOptPragma Separator ParameterNameList.

ParameterNameList:
IdentifierOptPragma;
ParameterNameList Separator IdentifierOptPragma.

ModifyingSchemaDeclaration:
ModifyingSchemaHeader OptExceptionSignature OptRequire OptPrecondition OptRecursionVariant post Postcondition OptImplementation OptPostAssertion.

SchemaDeclaration:
SchemaHeader OptExceptionSignature OptRequire OptPrecondition OptRecursionVariant post Postcondition OptImplementation OptPostAssertion.

SchemaPrototype:
SchemaHeader OptExceptionSignature OptRequire OptPrecondition OptPostAssertion;
ModifyingSchemaHeader OptExceptionSignature OptRequire OptPrecondition OptPostAssertion.

AbsurdSchemaDeclaration:
absurd SchemaHeader;
absurd ModifyingSchemaHeader.

SchemaHeader:
schema SchemaHead;
OpaqueOrGhost schema SchemaHead.

ModifyingSchemaHeader:
ModifyingSchemaHeader2;
OpaqueOrGhost ModifyingSchemaHeader2.

ModifyingSchemaHeader2:
schema '!' SchemaHead.

SchemaHead:
SimpIdentifier OptSchemaParmList;
IdWithPragma OptSchemaParmList.

OptSchemaParmList:
'(' SchemaParams ')';
Empty.

SchemaParams:
    SchemaParameterList;
    RepeatedParams;
    SchemaParameterList Separator RepeatedParams.

SchemaParameterList:
SchemaParameterDeclarations;
SchemaParameterList Separator SchemaParameterDeclarations.

SchemaParameterDeclarations:
    DecoratedIdentifierOptPragma ':' ParameterType;
    DecoratedIdentifierOptPragma ':' limited ParameterType;
    DecoratedIdentifierOptPragma ':' out ParameterType;
    TwoOrMoreSchemaParameters ':' ParameterType;
    TwoOrMoreSchemaParameters ':' limited ParameterType;
    TwoOrMoreSchemaParameters ':' out ParameterType.

TwoOrMoreSchemaParameters:
DecoratedIdentifierOptPragma Separator DecoratedIdentifierOptPragma;
TwoOrMoreSchemaParameters Separator DecoratedIdentifierOptPragma.

DecoratedIdentifierOptPragma:
IdentifierOptPragma;
IdentifierOptPragma '!'.

- Theorem and axiom declarations
TheoremDeclaration:
property OptIdentifier OptSchemaParmList OptPrecondition GeneralAssertion;
property OptIdentifier OptSchemaParmList OptPrecondition post Postcondition GeneralAssertion.

ModifyingTheoremDeclaration:
'!' property OptIdentifier OptSchemaParmList OptPrecondition post Postcondition GeneralAssertion.

- An axiom declaration is like a theorem declaration but cannot have a proof
AxiomDeclaration:
axiom OptIdentifier OptParmList OptPrecondition AssertionWithoutProof.

OptIdentifier:
SimpIdentifier;
Empty.

Postcondition:
Postcondition0;
'?'.

Postcondition0:
PostconditionList;
change Expr8pList satisfy ListOfPredicates.

PostconditionList:
PostconditionList ',' PostconditionElement;
PostconditionElement.

PostconditionElement:
forall BoundVariableDeclarations SUCHTHAT PostconditionElement;
PostconditionElem0.

PostconditionElem0:
PostconditionElem0 then PostconditionElem1;
PostconditionElem1.

PostconditionElem1:
PostconditionElem1 OPAND PostconditionElem2;
PostconditionElem2.

PostconditionElem2:
    Expr8lp '!' OPEQUAL Expr3to4;
    Expr8lp '!' AssignableOp Expr3to4;
    Expr8lp '!' BoolAssignableOp Expr3to4;
    '(' InBracketsPostconditionElem ')';
    SchemaCall;
    pass.

SchemaCall:
    - Schema calls that modify the current object
    '!' IdOrMember SchemaActualParameterList;
    '!' IdOrMember OptActualParameterList;
    Expr8lp '!' IdOrMember SchemaActualParameterList;
    Expr8lp '!' IdOrMember OptActualParameterList;
    - Schema calls that do not modify the current object
    Expr8np '.' IdOrMember SchemaActualParameterList;
    Expr8lp '.' IdOrMember SchemaActualParameterList;
    GeneralIdOrMember SchemaActualParameterList.

InBracketsPostconditionElem:
LetDeclAssertionList InBracketsPostconditionElem2;
InBracketsPostconditionElem2.

InBracketsPostconditionElem2:
    LocalVarDecls ';' InBracketsPostconditionElem;
    Postcondition0;
    GuardedPostconditionElements.

GuardedPostconditionElements:
    GuardedPostconditionElemsNoElse;
    opaque GuardedPostconditionElemsNoElse;
    GuardedElemsComma EmptyGuard PostconditionList;
    GuardedElemsComma NullGuard.

GuardedPostconditionElemsNoElse:
'[' Expression ']' ':' PostconditionList;
GuardedElemsComma '[' Expression ']' ':' PostconditionList.

GuardedElemsComma:
'[' Expression ']' ':' PostconditionList ',';
GuardedElemsComma '[' Expression ']' ':' PostconditionList ','.

Expr8pList:
    Expr8pNotCall;
    FuncOrSelecCall;
    Expr8pList ',' Expr8pNotCall;
    Expr8pList ',' FuncOrSelecCall.

FuncOrSelecCall:
Expr8lp '.' IdOrMember OptActualParameterList;
GeneralIdOrMember OptActualParameterList.

GeneralAssertion:
    AssertionWithoutProof;
    AssertionWithoutProof proof ProofList end;
    AssertionWithoutProof proof ProofListSEMI end.

AssertionWithoutProof:
assert ListOfPredicates.

OptPostAssertion:
    GeneralAssertion;
    AssertionWithInherit;
    AssertionWithInherit proof ProofList end;
    AssertionWithInherit proof ProofListSEMI end;
    Empty.

AssertionWithInherit:
assert DOTDOTDOT ',' ListOfPredicates;
assert DOTDOTDOT.

ProofList:
SimpleProofList;
ConditionalProof.

ConditionalProof:
    if ConditionalProofList fi;
    if ConditionalProofListSEMI fi;
    SimpleProofListSEMI if ConditionalProofList fi;
    SimpleProofListSEMI if ConditionalProofListSEMI fi.

ProofListSEMI:
SimpleProofListSEMI;
ConditionalProof ';'.

SimpleProofList:
ProofItem;
SimpleProofListSEMI ProofItem.

SimpleProofListSEMI:
SimpleProofList ';'.

ProofItem:
LetDeclaration;
AssertionStatement.

ConditionalProofList:
GuardedProofList;
ConditionalProofListSEMI GuardedProofList.

ConditionalProofListSEMI:
GuardedProofListSEMI;
ConditionalProofListSEMI GuardedProofListSEMI.

GuardedProofList:
'[' Expression ']' ':' ProofList.

GuardedProofListSEMI:
'[' Expression ']' ':' ProofListSEMI.

------------------ Class and type declarations -------------------

ClassOrTypeDeclaration:
    ClassDeclName DEFAS tag;
    ClassDeclName DEFAS tag '(' Expression ')';
    ClassDeclName DEFAS EnumDefinition;
    PossiblyFinalClassDeclaration;
    ClassDeclName OptClassParamsDefas PossConstrainedTypeExpression.

PossiblyFinalClassDeclaration:
    final ClassDeclaration;
    deferred ClassDeclaration;
    ClassDeclaration.

ClassDeclaration:
ClassDeclName OptClassParamsDefas ClassBody.

ClassDeclName:
class IdentifierOptPragma.

OptClassParamsDefas:
    of '(' ClassParameterList ')' OptRequire DEFAS;
    of SimpIdentifier OptRequire DEFAS;
    DEFAS.

ClassBody:
    ClassBody2;
    storable ClassBody2;
    inherits ClassName ClassBody2.

ClassBody2:
    AbstractDeclarations OptInternalDeclarations OptConfinedDeclarations OptInterfaceDeclarations end;
    ConfinedDeclarations OptInterfaceDeclarations end;
    InterfaceDeclarations end.

EnumDefinition:
enum IdentifierOptPragmaList OptCOMMA end.

IdentifierOptPragmaList:
IdentifierOptPragma;
IdentifierOptPragmaList ',' IdentifierOptPragma.

AbstractDeclarations:
abstract AbstractMemberDeclarations OptSEMI;
abstract .

AbstractMemberDeclarations:
AbstractMemberDeclaration;
AbstractMemberDeclarations ';' AbstractMemberDeclaration.

OptCOMMA:
',';
Empty.

ClassInvariant:
invariant ListOfPredicates.

HistoryInvariant:
'!' invariant ListOfPredicates OptExempt.

OptExempt:
exempt SimpIdentifierList;
Empty.

OptInternalDeclarations:
    internal InternalDeclarations OptSEMI;
    internal ;
    Empty.

InternalDeclarations:
InternalMemberDeclaration;
InternalDeclarations ';' InternalMemberDeclaration.

InterfaceDeclarations:
interface InterfaceDecls OptSEMI;
interface.

OptInterfaceDeclarations:
InterfaceDeclarations;
Empty.

ConfinedDeclarations:
confined ConfinedDecls OptSEMI;
confined.

OptConfinedDeclarations:
ConfinedDeclarations;
Empty.

InterfaceDecls:
    InterfaceOrConfinedDeclaration;
    EqualityOrRankDeclaration;
    InterfaceDecls ';' InterfaceOrConfinedDeclaration;
    InterfaceDecls ';' EqualityOrRankDeclaration.

ConfinedDecls:
InterfaceOrConfinedDeclaration;
ConfinedDecls ';' InterfaceOrConfinedDeclaration.

ExpressionList:
Expression;
ExpressionList ',' Expression.

ListOfPredicates:
ExpressionList.

ConstructorDeclaration:
ConstrDecl2;
OpaqueOrGhost ConstrDecl2.

ConstrDecl2:
build '{' OptConstructorParams '}' OptExceptionSignature OptRequire OptPrecondition OptRecursionVariant OptConstructorBody;
build Pragma '{' OptConstructorParams '}' OptExceptionSignature OptRequire OptPrecondition OptRecursionVariant OptConstructorBody.

ConstructorPrototype:
'{' OptConstructorParams '}' OptExceptionSignature OptRequire OptPrecondition OptPostAssertion.

OptConstructorParams:
    ConstructorParameterList;
    RepeatedParams;
    ConstructorParameterList Separator RepeatedParams;
    Empty.

ConstructorParameterList:
ConstructorParams;
ConstructorParameterList Separator ConstructorParams.

- Note that constructor parameters cannot be polymorphic.
ConstructorParams:
ParamOptDecBang ':' TypeExpression;
TwoOrMoreConstructorParameters ':' TypeExpression.

ParamOptDecBang:
IdentifierOptPragma;
'!' SimpIdentifier.

TwoOrMoreConstructorParameters:
ParamOptDecBang Separator ParamOptDecBang;
TwoOrMoreConstructorParameters Separator ParamOptDecBang.

OptConstructorBody:
    DEFAS Expression OptImplementation OptPostAssertion;
    inherits Expression OptConstructorPostcondition OptPostAssertion;
    OptConstructorPostcondition OptPostAssertion.

OptConstructorPostcondition:
post Postcondition OptImplementation;
Empty.

----------------------- 'require' parts ----------------------

OptRequire:
require RequirementList;
Empty.

RequirementList:
RequirementItem;
RequirementList ',' RequirementItem.

RequirementItem:
identifier within TypeExpression;
identifier has MemberDeclarationPrototypeList OptSEMI end.

MemberDeclarationPrototypeList:
MemberDeclarationPrototype;
MemberDeclarationPrototypeList ';' MemberDeclarationPrototype.

MemberDeclarationPrototype:
    MemberFSOSPrototype;
    EqualityOrRankPrototype;
    ConstructorPrototype.

------------------- Exception signatures ------------------

OptExceptionSignature:
throw TypeExpression;
Empty.

----------------------- Expressions -----------------------

PossiblyMultipleExpression:
Expression;
TwoOrMoreExpressions.

TwoOrMoreExpressions:
Expression ',' Expression;
TwoOrMoreExpressions ',' Expression.

- Single expressions

Expression:
PrimableExpression;
UnprimableExpression.

UnprimableExpression:
    Expr0np;
    - The following types of expression involve constructs which span to the end of the expression and have to be treated specially
    Expr3to4np ASorIS TypeExpression;
    Expr3to4np WithinOrNot TypeExpression;
    Expr8lp WithinOrNot TypeExpression;
    Expr3to4 after PostconditionElement;
    THATorANY Expression;
    THATorANY BoundVariableDeclaration SUCHTHAT Expression;
    those BoundVariableDeclaration SUCHTHAT Expression;
    forall BoundVariableDeclarations SUCHTHAT Expression;
    exists BoundVariableDeclarations SUCHTHAT Expression;
    for those BoundVariableDeclaration SUCHTHAT Expression yield Expression;
    for BoundVariableDeclaration yield Expression.

PrimableExpression:
Expr8lp ASorIS TypeExpression;
Expr8lp.

BoundVariableDeclaration:
SimpIdentifier ':' TypeExpr2;
SimpIdentifier DBLCOLON Expr4.

BoundVariableDeclarations:
BoundVariableDecls;
BoundVariableDeclarations ',' BoundVariableDecls.

BoundVariableDecls:
SimpIdentifierList ':' TypeExpr2;
SimpIdentifierList DBLCOLON Expr4.

Expr0np:
Expr0 Op0 Expr1; - Op0 are ==> <==> <==
Expr1np.

Expr0:
Expr0np;
Expr8lp.

Expr1np:
Expr1 Op1 Expr2; - Op1 is |
Expr2np.

Expr1:
Expr1np;
Expr8lp.

Expr2np:
Expr2 Op2 Expr3; - Op2 is &
Expr3np.

Expr2:
Expr2np;
Expr8lp.

Expr3np:
CompareList Expr3to4;
Expr3to4np.

Expr3:
Expr3np;
Expr8lp.

CompareList:
    Expr3to4np Op3;                 - Op3 are the comparisons and negated comparisons
    Expr8lp Op3;
    CompareList Expr3to4np Op3;
    CompareList Expr8lp Op3.

Expr3to4np:
    Expr3to4 OPRANK Expr4;
    Expr3to4 like Expr4;
    Expr3to4np NOT like Expr4;
    Expr8lp NOT like Expr4;
    Expr3to4np Op3to4 Expr4;       - Op3to4 are "in" and "~in"
    Expr8lp Op3to4 Expr4;
    Expr4np.

Expr3to4:
Expr3to4np;
Expr8lp.

Expr4np:
Expr4 Op4 Expr5; - Op4 are + - ++ --
Expr5np.

Expr4:
Expr4np;
Expr8lp.

Expr5np:
Expr5 Op5 Expr6; - Op5 are * / % ** # %% ##
Expr6np.

Expr5:
Expr5np;
Expr8lp.

Expr6np:
Expr6 Op6 Expr7; - OP6 are ^ and ..
Expr7np.

Expr6:
Expr6np;
Expr8lp.

Expr7np:
    NOT Expr7;
    Monop Expr7;
    TYPEOP TypeName;
    OverOp over Expr7;
    Expr8np.

Expr7:
Expr7np;
Expr8lp.

- Unprimable expressions
Expr8np:
    Expr8np IndexingExpression;
    Expr8np '.' value;
    Expr8p ''';                             - primed expression
    Expr8np '.' IdOrMember OptActualParameterList;
    ref Expression on IDENTIFIER;
    - Constructor calls
    ClassNameNotPoly '{' OptActConstructorParams '}';
    - Literals
    NONEMPTYSTRINGLITERAL;
    EMPTYSTRINGLITERAL;
    LITERAL;
    - Brackets
    '(' UnprimableInBracketsExpr ')';
    '(' LetDeclAssertionList UnprimableInBracketsExpr ')';
    - Allow '?' to represent an unfinished program
    '?'.

- Primable and limited-primable expressions
Expr8lp:
    Expr8pNotCall;
    - Function and selector calls (we can't tell which, so assume selector which is primable)
    - Also variables and member expressions
    FuncOrSelecCall;
    result;
    - Bracketed expressions are here because expressions of the form "(e is T)" may be primable
    '(' PrimableExpression ')';
    '(' LetDeclAssertionList PrimableExpression ')'.

- Fully Primable expressions
Expr8pNotCall:
    ITorSELF;
    Expr8lp '.' value;
    Expr8lp IndexingExpression.

IndexingExpression:
'[' Expression ']'.

Expr8p:
    Expr8pNotCall;
    - Function and selector calls (we can't tell which, so assume selector which is primable)
    - Also variables and member expressions
    FuncOrSelecCall.

IdOrMember:
IDENTIFIER;
super IDENTIFIER.

GeneralIdOrMember:
    IDENTIFIER;
    super IDENTIFIER;
    IDENTIFIER '@' ClassName;     - deprecated syntax
    ClassName IDENTIFIER.           - new syntax

OptActualParameterList:
'(' ExpressionSepList ')';
Empty.

OptActConstructorParams:
ExpressionSepList;
Empty.

ExpressionSepList:
Expression;
ExpressionSepList Separator Expression.

- A schema actual parameter list must have at least one "!" actual parameter in it
SchemaActualParameterList:
'(' SchemaActualParameters ')';
'(' ExpressionSepList Separator SchemaActualParameters ')'.

SchemaActualParameters:
    Expr8lp '!';
    SchemaActualParameters Separator Expression;
    SchemaActualParameters Separator Expr8lp '!'.

- Various forms of expressions in brackets
UnprimableInBracketsExpr:
    UnprimableExpression;
    TwoOrMoreExpressions;
    ChoicesWithElse;
    opaque ChoicesNoElse;
    ChoicesNoElse.

LetDeclAssertionList:
    LetDeclaration ';';
    AssertionStatement ';';
    TraceStatement ';';
    LetDeclAssertionList LetDeclaration ';';
    LetDeclAssertionList AssertionStatement ';';
    LetDeclAssertionList TraceStatement ';'.

LetDeclaration:
let IdentifierOptPragma DEFAS Expression OptNvImplementation.

AssertionStatement:
GeneralAssertion.

TraceStatement:
trace ExpressionSepList;
trace '[' Expression ']' ':' ExpressionSepList.

ChoicesWithElse:
ChoicesNoElse ',' EmptyGuard Expression.

ChoicesNoElse:
Choice;
ChoicesNoElse ',' Choice.

Choice:
'[' Expression ']' ':' Expression.

EmptyGuard:
'[' ']' ':'.

NullGuard:
'[' ']'.

---------------------- Type expressions ---------------------

ParameterType:
TypeExpression;
TemplateParameter.

TemplateParameter:
class SimpIdentifier.

FunctionType:
FunctionTypeList;
':' TypeExpression.

FunctionTypeList:
FunctionTypeElements;
FunctionTypeList ',' FunctionTypeElements.

FunctionTypeElements:
SimpIdentifierList ':' TypeExpression.

ConstrainedTypeExpression:
    those IDENTIFIER':' TypeExpr2 SUCHTHAT Expression;
    TypeExpr3 Op3 Expr4;
    TypeExpr3 Op3to4 Expr4;
    BracketedConstrainedTypeExpr.

BracketedConstrainedTypeExpr:
'(' ConstrainedTypeExpression ')'.

PossConstrainedTypeExpression:
ConstrainedTypeExpression;
TypeExpression.

TypeExpression:
TypeExpression UNITE TypeExpr2;
TypeExpr2.

TypeExpr2:
RefClassName;
TypeExpr2a.

TypeExpr2a:
FromClassName;
TypeExpr3.

TypeExpr3:
ClassName;
'(' TypeExpression ')'.

ClassName:
    IDENTIFIER of ClassNameParameters;
    PREDEFCLASS of ClassNameParameters;
    IDENTIFIER;
    PREDEFTYPE.

- Template type argument lists
ClassNameParameters:
    TemplateParameter;
    ClassNameAsTypeExpr;
    FromClassName;
    RefClassName;
    '(' TypeExpressionList ')'.

ClassNameAsTypeExpr:
ClassName.

FromClassName:
from ClassName.

RefClassName:
ref limited TypeExpr2a on IDENTIFIER;
ref TypeExpr2a on IDENTIFIER.

- ClassNameNotPoly is used in the syntax for constructors.
ClassNameNotPoly:
    IDENTIFIER of ClassNameParameters;
    PREDEFCLASS of ClassNameParameters;
    TypeName.

TypeExpressionList:
ParameterType;
TypeExpressionList Separator ParameterType.

TypeName:
IDENTIFIER;
PREDEFTYPE.

- Abbreviated type expressions are permitted after ":" when declaring a single non-bound local variable
AbbrevTypeExpr:
those TypeExpr2 SUCHTHAT Expression;
AbbrevTypeExpr1.

AbbrevTypeExpr1:
'(' AbbrevTypeExpr ')'.

--------------------- Implementations ----------------------

OptImplementation:
Implementation;
Empty.

Implementation:
via OptImplVariantSemi ImplList OptSEMI end.

- Same as above but no variant permitted
OptNvImplementation:
via ImplList OptSEMI end;
Empty.

ImplList:
    ImplItem;
    LocalVarDecls;
    HeapDeclarations;
    ImplList ';' ImplItem;
    ImplList ';' LocalVarDecls;
    ImplList ';' HeapDeclarations.

- Implementation items valid in both functions and schemas
ImplItem:
    begin ImplList OptSEMI end;
    par ImplList OptSEMI end;
    if Conditional fi;
    value PossiblyMultipleExpression;
    done;
    LocalDeclaration;
    LetDeclaration;
    TraceStatement;
    Postcondition OptNvImplementation;
    GeneralAssertion;
    IdentifierOptPragma ':' Precondition;
    goto IDENTIFIER;
    - A loop must either have a 'change' part, or some local variable declarations, otherwise it really can't do anything.
    loop OptLocalVars change Expr8pList keep ListOfPredicates OptLoopUntil LoopVariant ';' ImplList OptSEMI end;
    loop LocalVarDecls ';' keep ListOfPredicates OptLoopUntil LoopVariant ';' ImplList OptSEMI end;
    throw Expression;
    throw;
    try ImplList OptSEMI catch CatchList end.

LocalVarDecls:
var LocalVarDeclGroup;
LocalVarDecls ',' LocalVarDeclGroup.

LocalVarDeclGroup:
    SimpIdentifier ':' PossConstrainedTypeExpression;
    SimpIdentifier ':' TypeExpression '!' OPEQUAL Expression;
    SimpIdentifier ':' BracketedConstrainedTypeExpr '!' OPEQUAL Expression;
    SimpIdentifier ':' AbbrevTypeExpr;
    SimpIdentifier ':' AbbrevTypeExpr1 '!' OPEQUAL Expression;
    TwoOrMoreSimpIdentifiers ':' PossConstrainedTypeExpression.

OptLocalVars:
LocalVarDecls ';';
Empty.

OptLoopUntil:
until ListOfPredicates;
Empty.

Conditional:
    ConditionalNoElse;
    ConditionalNoElseSemi;
    ConditionalNoElseSemi EmptyGuard ImplList OptSEMI;
    ConditionalNoElseSemi NullGuard.

ConditionalNoElse:
GuardedImplList;
ConditionalNoElseSemi GuardedImplList.

ConditionalNoElseSemi:
GuardedImplList ';';
ConditionalNoElseSemi GuardedImplList ';'.

GuardedImplList:
    '[' Expression ']' ':' ImplItem;
    '[' Expression ']' ':' LocalVarDecls;
    GuardedImplList ';' ImplItem;
    GuardedImplList ';' LocalVarDecls.

CatchList:
    CatchItem;
    CatchItem ';';
    CatchItem ';' CatchList.

CatchItem:
    '[' IdentifierOptPragma ':' TypeExpression ']' ':' ImplItem;
    '[' IdentifierOptPragma ':' TypeExpression ']' ':' LocalVarDecls;
    CatchItem ';' ImplItem;
    CatchItem ';' LocalVarDecls.

--------------------- Variants ---------------------

OptRecursionVariant:
    decrease ExpressionList;
    decrease DOTDOTDOT;
    decrease DOTDOTDOT ',' ExpressionList;
    Empty.

OptImplVariantSemi:
decrease ExpressionList ';';
Empty.

LoopVariant:
decrease ExpressionList.

--------------------- Operators ---------------------

- Some operators can be both unary and binary. The following allows such operators to be both (e.g. OP3M represents the operators ">" and "<").
- Also, all Op3 operators return Boolean results and can be prefixed by "~" to generate the inverse operator

Op0:
OP0.

Op1:
OPOR.

Op2:
OPAND.

Op3:
PlainOp3;
NOT PlainOp3.

PlainOp3:
    OP3;                     - binary only, <= <<= >= >>= << >>
    OPEQUAL;
    OP3M.                 - unary or binary, < >

Op3to4:
in;
NOT in.

Op4:
OP4; - binary only, ++ --
OP4M. - unary or binary, + -

Op5:
OP5; - binary only, **
OP5M. - unary or binary, * % /

Op6:
OP6;
OP6M.

Monop:
    OP3M;
    OP4M;
    OP5M;
    OP6M.

IndexOp:
'[' ']'.

IndexOpWithPragma:
IndexOp Pragma.

RedefinableOp:
RevRedefinableOp;
IndexOp.

RedefinableOpWithPragma:
RevRedefinableOpWithPragma;
IndexOpWithPragma.

RevRedefinableOp:
    OP3;
    OP3M;
    OP4;
    OP4M;
    OP5;
    OP5M;
    OP6;
    OP6M;
    in.

RevRedefinableOpWithPragma:
RevRedefinableOp Pragma.

- All bound binary operators except the comparisons can be used with "over"
OverOp:
    Op4;
    Op5;
    Op6.

- All binary operators except the comparisons can be used after "!"
AssignableOp:
    Op4;
    Op5;
    Op6.

- Boolean operators
BoolAssignableOp:
    Op0;
    Op1;
    Op2.

WithinOrNot:
within;
NOT within.

------------------- Miscellaneous ------------------

OpaqueOrGhost:
opaque;
ghost.

SimpIdentifier:
IDENTIFIER.

- When declaring most names, we allow the identifier to be modified by a pragma
IdentifierOptPragma:
IDENTIFIER;
IdWithPragma.

IdWithPragma:
IDENTIFIER Pragma.

Pragma:
pragma PragmaMapping.

PragmaMapping:
'(' PragmaMapList ')'.

PragmaMapList:
PragmaMapItem;
PragmaMapList ',' PragmaMapItem.

PragmaMapItem:
    IDENTIFIER OPEQUAL NONEMPTYSTRINGLITERAL;
    IDENTIFIER OPEQUAL IDENTIFIER;
    IDENTIFIER OPEQUAL PragmaMapping.

OptSTRINGLITERAL:
NONEMPTYSTRINGLITERAL;
Empty.

OptSEMI:
';' ;
Empty.

------------------ End of grammar -----------------