PrefixOpToken | ::= | ( <op_26> | <op_29> | <op_58> | <CASESEP> | <op_61> | <op_112> | <op_113> | <op_114> | <op_115> | <op_116> ) |
NEPrefixOpToken | ::= | ( <op_26> | <op_29> | <op_58> | <CASESEP> | <op_61> | <op_76> | <op_112> | <op_113> | <op_114> | <op_115> | <op_116> ) |
InfixOpToken | ::= | ( <op_1> | <AND> | <op_3> | <op_4> | <OR> | <op_6> | <op_7> | <op_8> | <op_9> | <op_10> | <op_11> | <op_12> | <op_13> | <op_14> | <op_15> | <op_16> | <op_17> | <op_18> | <op_19> | <IN> | <op_21> | <op_22> | <op_23> | <op_24> | <op_25> | <op_27> | <op_30> | <op_31> | <op_32> | <op_33> | <op_34> | <op_35> | <op_36> | <op_37> | <op_38> | <op_39> | <op_40> | <op_41> | <op_42> | <op_43> | <op_44> | <op_45> | <op_46> | <op_47> | <op_48> | <op_49> | <op_50> | <op_51> | <op_52> | <op_53> | <op_54> | <op_55> | <op_56> | <op_59> | <op_62> | <op_63> | <op_64> | <EQUALS> | <op_66> | <op_67> | <op_71> | <op_72> | <op_73> | <op_74> | <op_75> | <op_77> | <op_78> | <op_79> | <op_80> | <op_81> | <op_82> | <op_83> | <op_84> | <op_85> | <op_86> | <op_87> | <op_88> | <op_89> | <op_90> | <op_91> | <op_92> | <op_93> | <op_94> | <op_95> | <op_96> | <op_97> | <op_98> | <op_100> | <op_101> | <op_102> | <op_103> | <op_104> | <op_105> | <op_106> | <op_107> | <op_108> | <op_109> | <op_110> | <op_111> | <op_117> | <op_118> | <op_119> ) |
PostfixOpToken | ::= | ( <op_57> | <op_68> | <op_69> | <op_70> ) |
CompilationUnit | ::= | ( Prelude )? Module |
Prelude | ::= | <BEGIN_PRAGMA> ( <NUMBER> | <IDENTIFIER> )* |
Module | ::= | BeginModule Extends Body EndModule |
BeginModule | ::= | ( <_BM0> | <_BM1> | <_BM2> ) Identifier <SEPARATOR> |
EndModule | ::= | <END_MODULE> |
Extends | ::= | ( <EXTENDS> Identifier ( <COMMA> Identifier )* )? |
Body | ::= | ( ( <SEPARATOR> | VariableDeclaration | ParamDeclaration | OperatorOrFunctionDefinition | Recursive | Instance | Assumption | Theorem | Module | UseOrHideOrBy ) )* |
VariableDeclaration | ::= | <VARIABLE> Identifier ( <COMMA> Identifier )* |
ParamDeclaration | ::= | ParamSubDecl ConstantDeclarationItems ( <COMMA> ConstantDeclarationItems )* |
ParamSubDecl | ::= | <CONSTANT> |
Recursive | ::= | <RECURSIVE> ConstantDeclarationItems ( <COMMA> ConstantDeclarationItems )* |
ConstantDeclarationItems | ::= | ( Identifier ( <LBR> <US> ( <COMMA> <US> )* <RBR> )? | NonExpPrefixOp <US> | <US> ( InfixOp <US> | PostfixOp ) ) |
OperatorOrFunctionDefinition | ::= | ( <LOCAL> )? <DEFBREAK> ( Identifier <LSB> QuantBound ( <COMMA> QuantBound )* <RSB> <DEF> Expression | PostfixLHS <DEF> Expression | InfixLHS <DEF> Expression | IdentLHS <DEF> ( Expression | Instantiation ) | PrefixLHS <DEF> Expression ) |
IdentifierTuple | ::= | <LAB> ( Identifier ( <COMMA> Identifier )* )? <RAB> |
IdentLHS | ::= | Identifier ( ( <LBR> ( IdentDecl | SomeFixDecl ) ( <COMMA> ( IdentDecl | SomeFixDecl ) )* <RBR> )? ) |
PrefixLHS | ::= | NEPrefixOpToken Identifier |
InfixLHS | ::= | Identifier InfixOpToken Identifier |
PostfixLHS | ::= | Identifier PostfixOpToken |
IdentDecl | ::= | Identifier ( <LBR> <US> ( <COMMA> <US> )* <RBR> )? |
SomeFixDecl | ::= | ( NonExpPrefixOp <US> | ( <US> ( InfixOp <US> | PostfixOp ) ) ) |
Instance | ::= | ( <LOCAL> )? Instantiation |
Instantiation | ::= | <INSTANCE> Identifier ( <WITH> Substitution ( <COMMA> Substitution )* )? |
Substitution | ::= | ( Identifier | NonExpPrefixOp | InfixOp | PostfixOp ) <SUBSTITUTE> OpOrExpr |
OldSubstitution | ::= | ( Identifier | NonExpPrefixOp | InfixOp | PostfixOp ) <SUBSTITUTE> ( <op_76> | Expression | Lambda ) |
PrefixOp | ::= | PrefixOpToken |
NonExpPrefixOp | ::= | NEPrefixOpToken |
InfixOp | ::= | InfixOpToken |
PostfixOp | ::= | PostfixOpToken |
Identifier | ::= | <IDENTIFIER> |
Assumption | ::= | ( <ASSUMPTION> | <ASSUME> ) ( ( <DEFBREAK> )? Identifier <DEF> )? Expression |
AssumeProve | ::= | ( Identifier <COLONCOLON> AssumeProve )? <ASSUME> ( AssumeProve | NewSymb | Expression ) ( <COMMA> ( AssumeProve | NewSymb | Expression ) )* <PROVE> Expression |
NewSymb | ::= | ( ( <NEW> <CONSTANT> | <NEW> | <CONSTANT> ) ( IdentDecl ( <IN> Expression )? | SomeFixDecl ) | ( <NEW> )? <VARIABLE> Identifier | ( <NEW> )? ( <STATE> | <ACTION> | <TEMPORAL> ) ( IdentDecl | SomeFixDecl ) ) |
MaybeBound | ::= | ( <IN> Expression )? |
Theorem | ::= | ( <THEOREM> | <PROPOSITION> ) ( Identifier <DEF> )? ( ( ) AssumeProve | Expression ) ( Proof )? |
Proof | ::= | ( UseOrHideOrBy | ( <PROOF> )? ( <OBVIOUS> | <OMITTED> ) | ( <PROOF> )? ( Step )* QEDStep ) |
UseOrHideOrBy | ::= | ( ( <PROOF> )? <BY> ( <ONLY> )? | <USE> ( <ONLY> )? | <HIDE> ) ( ( <MODULE> Identifier | Expression ) ( <COMMA> ( <MODULE> Identifier | Expression ) )* )? ( <DF> ( <MODULE> Identifier | Expression ) ( <COMMA> ( <MODULE> Identifier | Expression ) )* )? |
StepStartToken | ::= | ( <ProofStepLexeme> | <ProofImplicitStepLexeme> | <ProofStepDotLexeme> | <BareLevelLexeme> | <UnnumberedStepLexeme> ) |
QEDStep | ::= | StepStartToken <QED> ( Proof )? |
Step | ::= | StepStartToken ( UseOrHideOrBy | Instantiation | DefStep | HaveStep | TakeStep | WitnessStep | PickStep | CaseStep | AssertStep ) ( Proof )? |
DefStep | ::= | ( <DEFINE> )? ( OperatorOrFunctionDefinition )+ |
HaveStep | ::= | <HAVE> Expression |
TakeStep | ::= | <TAKE> ( QuantBound ( <COMMA> QuantBound )* | Identifier ( <COMMA> Identifier )* ) |
WitnessStep | ::= | <WITNESS> Expression ( <COMMA> Expression )* |
PickStep | ::= | <PICK> ( Identifier ( <COMMA> Identifier )* | QuantBound ( <COMMA> QuantBound )* ) <COLON> Expression |
CaseStep | ::= | <CASE> Expression |
AssertStep | ::= | ( <SUFFICES> )? ( Expression | AssumeProve ) |
GeneralId | ::= | IdPrefix Identifier |
IdPrefix | ::= | ( IdPrefixElement )* |
IdPrefixElement | ::= | Identifier ( OpArgs )? <BANG> |
ParenthesesExpression | ::= | ( ParenExpr | BraceCases | SBracketCases | SetExcept | TupleOrAction | FairnessExpr ) |
ClosedExpressionOrOp | ::= | ( ElementaryExpression | ParenthesesExpression ) |
ClosedExpressionOnly | ::= | ClosedExpressionOrOp |
OpenExpression | ::= | ( SomeQuant | SomeTQuant | IfThenElse | Case | LetIn | UnboundOrBoundChoose ) |
ElementaryExpression | ::= | ( Extension | String | Number ) |
String | ::= | <STRING_LITERAL> |
Number | ::= | <NUMBER_LITERAL> ( <DOT> <NUMBER_LITERAL> )? |
Extension | ::= | ( PrefixOp | InfixOp | PostfixOp | Identifier ( OpArgs )? ( <BANG> Extension )? ) |
OpArgs | ::= | <LBR> OpSuite ( <COMMA> OpSuite )* <RBR> |
OpOrExpr | ::= | ( ( NonExpPrefixOp | InfixOp | PostfixOp ) | Lambda | Expression ) |
OpSuite | ::= | OpOrExpr |
ParenExpr | ::= | <LBR> Expression <RBR> |
SomeQuant | ::= | ( <EXISTS> | <FORALL> ) ( ( Identifier ( <COMMA> Identifier )* ) | QuantBound ( <COMMA> QuantBound )* ) <COLON> Expression |
SomeTQuant | ::= | ( <T_EXISTS> | <T_FORALL> ) Identifier ( <COMMA> Identifier )* <COLON> Expression |
QuantBound | ::= | ( IdentifierTuple | Identifier ( <COMMA> Identifier )* ) <IN> Expression |
BraceCases | ::= | <LBC> ( ( IdentifierTuple | Identifier ) <IN> Expression ( ( <COLON> Expression ) | ( <COMMA> Expression )+ )? | Expression ( <COMMA> Expression )* | Expression <COLON> QuantBound ( <COMMA> QuantBound )* | Expression ( <COLON> QuantBound ( <COMMA> QuantBound )* | ( <COMMA> Expression )+ )? )? <RBC> |
SBracketCases | ::= | <LSB> ( QuantBound ( <COMMA> QuantBound )* <MAPTO> Expression <RSB> | FieldVal ( <COMMA> FieldVal )* <RSB> | FieldVal ( <COMMA> FieldVal )* <RSB> | FieldSet ( <COMMA> FieldSet )* <RSB> | Expression ( ( <COMMA> Expression )* <RSB> | <ARROW> Expression <RSB> | <EXCEPT> ExceptSpec ( <COMMA> ExceptSpec )* <RSB> | <ARSB> ReducedExpression ) ) |
FieldVal | ::= | Identifier <MAPTO> Expression |
FieldSet | ::= | Identifier <COLON> Expression |
ExceptSpec | ::= | <BANG> ( ExceptComponent )+ <EQUALS> Expression |
ExceptComponent | ::= | ( <DOT> Identifier | <LSB> Expression ( <COMMA> Expression )* <RSB> ) |
SetExcept | ::= | <LWB> Expression <EXCEPT> SExceptSpec ( <COMMA> SExceptSpec )* <RWB> |
SExceptSpec | ::= | <BANG> ExceptComponent ( <EQUALS> | <IN> ) Expression |
TupleOrAction | ::= | <LAB> ( Expression ( <COMMA> Expression )* )? ( <RAB> | <ARAB> ReducedExpression ) |
NoOpExtension | ::= | ( Identifier ( OpArgs )? ( <BANG> NoOpExtension )? ) |
ReducedExpression | ::= | ( NoOpExtension | ParenExpr | BraceCases | SBracketCases | SetExcept | TupleOrAction ) |
FairnessExpr | ::= | ( <WF> | <SF> ) ReducedExpression ( <LBR> Expression <RBR> )? |
IfThenElse | ::= | <IF> Expression <THEN> Expression <ELSE> Expression |
Case | ::= | <CASE> CaseArm ( <CASESEP> CaseArm )* ( <CASESEP> OtherArm )? |
CaseArm | ::= | Expression <ARROW> Expression |
OtherArm | ::= | <OTHER> <ARROW> Expression |
LetIn | ::= | <LET> LetDefinitions <LETIN> Expression |
LetDefinitions | ::= | ( OperatorOrFunctionDefinition | Recursive )+ |
Junctions | ::= | ( DisjList | ConjList ) |
DisjList | ::= | JuncItem ( JuncItem )* |
ConjList | ::= | JuncItem ( JuncItem )* |
JuncItem | ::= | ( <OR> | <AND> ) Expression |
UnboundOrBoundChoose | ::= | <CHOOSE> ( Identifier | IdentifierTuple ) MaybeBound <COLON> Expression |
Lambda | ::= | <LAMBDA> Identifier ( <COMMA> ( Identifier ) )* <COLON> Expression |
Expression | ::= | ( ( PrefixOp | InfixOp ) )* ( OpenExpression | ExtendableExpr ) |
ExtendableExpr | ::= | ( Junctions | ParenthesesExpression | PrimitiveExp ) ( PostfixOp | <DOT> ( ) Identifier | SBracketCases )* ( InfixOp ( ( PrefixOp | InfixOp ) )* ( OpenExpression | ExtendableExpr ) | <COLONCOLON> Expression )? |
PrimitiveExp | ::= | ( String | Number | ( ( ( Identifier | ( <ProofStepLexeme> | <ProofImplicitStepLexeme> ) | InfixOp | PostfixOp | NonExpPrefixOp ) ( OpArgs )? ) ( BangExt )* ) ) |
BangExt | ::= | <BANG> ( ( Identifier | NonExpPrefixOp | InfixOp | PostfixOp ) ( OpArgs )? | OpArgs | StructOp ) |
StructOp | ::= | ( <LAB> | <RAB> | <COLON> | Number | <IDENTIFIER> ) |
OpenStart | ::= | <CASE> |
| | <CHOOSE> | |
| | <EXISTS> | |
| | <FORALL> | |
| | <IF> | |
| | <LET> | |
| | <T_EXISTS> | |
| | <T_FORALL> |