--------------------------- MODULE TLAPlus2Grammar --------------------------- 
EXTENDS Naturals, Sequences, BNFGrammars

CommaList(L) == L & (tok(",") &  L)^*
AtLeast4(s) == Tok({s \o s \o s} & {s}^+)

ReservedWord == 
  { "ASSUME",        "ELSE",       "LOCAL",       "UNION",     
    "ASSUMPTION",    "ENABLED",    "MODULE",      "VARIABLE",   
    "AXIOM",         "EXCEPT",     "OTHER",      "VARIABLES",  
    "CASE",          "EXTENDS",    "SF_",         "WF_",      
    "CHOOSE",        "IF",         "SUBSET",      "WITH", 
    "CONSTANT",      "IN",         "THEN",               
    "CONSTANTS" ,    "INSTANCE",   "THEOREM",     "COROLLARY",
    "DOMAIN",        "LET",        "UNCHANGED",   
    "BY",            "HAVE",       "QED",         "TAKE",                   
    "DEF",           "HIDE",       "RECURSIVE",   "USE", 
    "DEFINE",        "PROOF",      "WITNESS",     "PICK",
    "DEFS",          "PROVE",      "SUFFICES",    "NEW",
    "LAMBDA",        "STATE",      "ACTION",      "TEMPORAL",   
    "OBVIOUS",       "OMITTED",    "LEMMA",       "PROPOSITION",
    "ONLY"}

Letter == OneOf("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ")
Numeral   == OneOf("0123456789") 
NameChar  == Letter \cup Numeral \cup {"_"}  

Name == Tok((NameChar^* & Letter & NameChar^*)  
                   \   ({"WF_","SF_"} & NameChar^+))

Identifier == Name  \  Tok(ReservedWord)

IdentifierOrTuple  ==   
   Identifier |  tok("<<") & CommaList(Identifier) & tok(">>")

NumberLexeme == 
         Numeral^+ 
      |  (Numeral^* & {"."} & Numeral^+) 
      |  {"\\b","\\B" } & OneOf("01")^+ 
      |  {"\\o", "\\O"} & OneOf("01234567")^+ 
      |  {"\\h", "\\H"} & OneOf("0123456789abcdefABCDEF")^+ 

Number == Tok(NumberLexeme)

ProofStepId == Tok({"<"} & (Numeral^+ | {"*"}) & {">"} & (Letter | Numeral | {"_"})^+)

BeginStepToken == Tok({"<"} & (Numeral^+ | {"*", "+"}) & {">"} & 
                       (Letter | Numeral)^* & {"."}^* )

String == Tok({"\""} & STRING & {"\""})

PrefixOp  ==  
  Tok({ "-", "~", "\\lnot", "\\neg", "[]", "<>",
        "DOMAIN",  "ENABLED", "SUBSET", "UNCHANGED", "UNION"})

InfixOp   ==
  Tok({  "!!",  "#",    "##",   "$",    "$$",   "%",    "%%",  
         "&",   "&&",   "(+)",  "(-)",  "(.)",  "(/)",  "(\\X)",  
         "*",   "**",   "+",    "++",   "-",    "-+->", "--",  
         "-|",  "..",   "...",  "/",    "//",   "/=",   "/\\",  
         "::=", ":=",   ":>",   "<",    "<:",   "<=>",  "=",  
         "=<",  "=>",   "=|",   ">",    ">=",   "??", 
         "@@",  "\\",   "\\/",  "^",    "^^",   "|",    "|-",  
         "|=",  "||",   "~>",   ".",    "<=",
         "\\approx",  "\\geq",       "\\oslash",     "\\sqsupseteq",
         "\\asymp",   "\\gg",        "\\otimes",     "\\star",     
         "\\bigcirc", "\\in",        "\\prec",       "\\subset",   
         "\\bullet",  "\\intersect", "\\preceq",     "\\subseteq", 
         "\\cap",     "\\land",      "\\propto",     "\\succ",     
         "\\cdot",    "\\leq",       "\\sim",        "\\succeq",   
         "\\circ",    "\\ll",        "\\simeq",      "\\supset",   
         "\\cong",    "\\lor",       "\\sqcap",      "\\supseteq", 
         "\\cup",     "\\o",         "\\sqcup",      "\\union",    
         "\\div",     "\\odot",      "\\sqsubset",   "\\uplus",    
         "\\doteq",   "\\ominus",    "\\sqsubseteq", "\\wr",      
         "\\equiv",   "\\oplus",     "\\sqsupset",   "\\notin"     })

PostfixOp ==  Tok({ "^+",  "^*", "^#", "'" })
TLAPlusGrammar ==
 LET P(G) ==
   /\ G.Module ::=     AtLeast4("-") 
                   & tok("MODULE") & Name & AtLeast4("-")
                   &   (Nil | (tok("EXTENDS") & CommaList(Name)))
                   &   (G.Unit)^* 
                   &   AtLeast4("=") 

   /\ G.Unit ::= 
              G.VariableDeclaration 
           |  G.ConstantDeclaration 
           |  G.Recursive
           |  G.UseOrHide
           |  (Nil | tok("LOCAL")) & G.OperatorDefinition 
           |  (Nil | tok("LOCAL")) & G.FunctionDefinition 
           |  (Nil | tok("LOCAL")) & G.Instance           
           |  (Nil | tok("LOCAL")) & G.ModuleDefinition  
           |  G.Assumption 
           |  G.Theorem & (Nil | G.Proof)
           |  G.Module  
           |  AtLeast4("-") 

   /\ G.VariableDeclaration ::=  
          Tok({"VARIABLE", "VARIABLES"}) & CommaList(Identifier)

   /\ G.ConstantDeclaration ::=   
           Tok({"CONSTANT", "CONSTANTS"}) & CommaList(G.OpDecl)

   /\ G.Recursive ::= tok("RECURSIVE") & CommaList(G.OpDecl)

   /\ G.OpDecl ::=      Identifier 
                     |  Identifier & tok("(") & 
                               CommaList(tok("_")) & tok(")")
                     |  PrefixOp & tok("_")
                     |  tok("_") & InfixOp & tok("_")
                     |  tok("_") & PostfixOp  
   /\  G.OperatorDefinition ::=  
            (   G.NonFixLHS 
             |  PrefixOp   & Identifier 
             |  Identifier & InfixOp & Identifier 
             |  Identifier & PostfixOp )
          &  tok("==") 
          &  G.Expression

   /\ G.NonFixLHS ::=   
             Identifier 
          &  (    Nil 
              |   tok("(") 
                & CommaList(Identifier |  G.OpDecl) 
                & tok(")") ) 

   /\ G.FunctionDefinition ::=   
           Identifier  
        &  tok("[") & CommaList(G.QuantifierBound) & tok("]") 
        &  tok("==") 
        &  G.Expression  

   /\ G.QuantifierBound ::=  
           (IdentifierOrTuple | CommaList(Identifier))  
        &  tok("\\in") 
        &  G.Expression 

   /\ G.Instance ::= 
           tok("INSTANCE") 
        &  Name 
        &  (Nil | tok("WITH") & CommaList(G.Substitution))  

   /\ G.Substitution ::=  
             (Identifier | PrefixOp | InfixOp | PostfixOp ) 
          &  tok("<-") 
          &  G.Argument  

   /\ G.Argument ::= G.Expression  | G.Opname | G.Lambda

   /\ G.Lambda ::= tok("LAMBDA") & CommaList(Identifier) 
                     & tok(":") & G.Expression

   /\ G.OpName ::= 
        (Identifier | PrefixOp | InfixOp | PostfixOp | ProofStepId)
      & (  tok("!")
         & (Identifier | PrefixOp | InfixOp | PostfixOp
              | Tok({"<<", ">>", "@"} \cup Numeral^+) )
        )^*

   /\ G.OpArgs ::= tok("(") & CommaList(G.Argument) & tok(")")

   /\ G.InstOrSubexprPrefix ::=  
      (    (Nil | ProofStepId & tok("!")) 
        & ( (   Identifier & (Nil | G.OpArgs)
              | Tok({"<<", ">>", ":"} \cup Numeral^+)
              | G.OpArgs 
              | (PrefixOp | PostfixOp) & tok("(") & G.Expression & tok(")")
              | InfixOp & tok("(") & G.Expression & tok(",") 
                  & G.Expression & tok(")")
             )
            &  tok("!")
          ) ^*
      ) \ Nil

\* /\ G.InstancePrefix ::= ...

   /\ G.GeneralIdentifier ::= 
           (G.InstOrSubexprPrefix | Nil) & Identifier 
         | ProofStepId

\* /\ G.GeneralIdentifier ::= ...
\* /\ G.GeneralPrefixOp   ::= ...
\* /\ G.GeneralInfixOp    ::= ...
\* /\ G.GeneralPostfixOp  ::= ...

   /\ G.ModuleDefinition ::=   G.NonFixLHS 
                             & tok("==")  
                             & G.Instance  

   /\ G.Assumption ::=  
          Tok({"ASSUME", "ASSUMPTION", "AXIOM"}) 
             & (Nil | Name & tok("==")) & G.Expression

   /\ G.Theorem ::= 
          Tok({"THEOREM", "PROPOSITION", "LEMMA", "COROLLARY"}) 
             & (Nil | Name & tok("==")) & (G.Expression | G.AssumeProve)

   /\ G.AssumeProve ::=    tok("ASSUME") 
                         & CommaList(G.Expression | G.New | G.InnerAssumeProve)
                         & tok("PROVE") 
                         & G.Expression

   /\ G.InnerAssumeProve ::= (Nil | Name & tok("::")) & G.AssumeProve

   /\ G.New ::=   ((  (Nil | tok("NEW")) 
                    & (Nil | tok("CONSTANT") | tok("VARIABLE") | tok("STATE") 
                           | tok("ACTION") | tok("TEMPORAL") ) 
                   ) \ Nil)
                & ((Identifier & tok("\\in") & G.Expression) | G.OpDecl)

   /\ G.Proof ::=   G.TerminalProof 
                  | G.NonTerminalProof

   /\ G.TerminalProof ::=   (tok("PROOF") | Nil)
                          & (  tok("BY") &  (tok("ONLY") | Nil) & G.UseBody
                             | tok("OBVIOUS")
                             | tok("OMITTED")
                            )

   /\ G.NonTerminalProof ::= 
             (Nil | tok("PROOF")) 
           & G.Step^*
           & G.QEDStep

   /\ G.Step ::=
          BeginStepToken
        & (  (  G.UseOrHide
              | (  (Nil | tok("DEFINE"))
                 & (  G.OperatorDefinition 
                    | G.FunctionDefinition
                    | G.ModuleDefinition )^+
                 )
              | G.Instance
              | tok("HAVE") & G.Expression
              | tok("WITNESS") & CommaList(G.Expression)
              | tok("TAKE") & (  CommaList(G.QuantifierBound) 
                               | CommaList(Identifier) )
             )
           | (  (  (  (Nil | tok("SUFFICES"))
                    & (G.Expression | G.AssumeProve)
                   )
                 | (tok("CASE") & G.Expression)
                 | (  tok("PICK") 
                    & ( CommaList(G.QuantifierBound) | CommaList(Identifier) )
                    & tok(":")
                    & G.Expression
                   )
                )
              & (Nil | G.Proof)
             )
          )

   /\ G.QEDStep ::= 
        BeginStepToken &  tok("QED") & (Nil | G.Proof)

   /\ G.UseOrHide ::=   (  (tok("USE") & (Nil | tok("ONLY")))
                         | tok("HIDE") )
                       & G.UseBody

   /\ G.UseBody  ::=  (  (Nil | CommaList(G.Expression | tok("MODULE") & Name ))
                       & (Nil | Tok({"DEF", "DEFS"}) 
                                  & CommaList(G.OpName | 
                                                tok("MODULE") & Name ))
                      ) \ Nil


   /\ G.Expression ::= 

\*          G.GeneralIdentifier

            Name & (Nil | tok("(") & CommaList(Identifier) & tok(")")) 
               & tok("::") & G.Expression

         |  G.InstOrSubexprPrefix 
               & (Tok({"<<", ">>", ":"} \cup Numeral^+) | G.OpArgs)


         |  G.GeneralIdentifier & (Nil | G.OpArgs)

         |  PrefixOp & G.Expression 

         |  G.Expression & InfixOp & G.Expression 

         |  G.Expression & PostfixOp

         |  tok("(") & G.Expression & tok(")") 

         |   Tok({"\\A", "\\E"}) 
           & CommaList(G.QuantifierBound)   
           & tok(":") 
           & G.Expression 

         |    Tok({"\\A", "\\E", "\\AA", "\\EE"})
           &  CommaList(Identifier) 
           &  tok(":") 
           &  G.Expression 

        |     tok("CHOOSE") 
           &  IdentifierOrTuple 
           &  (Nil | tok("\\in") & G.Expression) 
           &  tok(":") 
           &  G.Expression 

        |     tok("{")
           & (Nil | CommaList(G.Expression))
           & tok("}") 

        |     tok("{") 
           &  IdentifierOrTuple & tok("\\in") & G.Expression 
           &  tok(":") 
           &  G.Expression 
           &  tok("}") 

        |     tok("{") 
           &  G.Expression  
           &  tok(":")  
           &  CommaList(G.QuantifierBound) 
           &  tok("}") 

        |  G.Expression & tok("[") & CommaList(G.Expression)
             & tok("]")

        |     tok("[") 
           &  CommaList(G.QuantifierBound)
           &  tok("|->")  
           &  G.Expression 
           &  tok("]") 

       |  tok("[") & G.Expression & tok("->") 
                 & G.Expression & tok("]") 

       |     tok("[") 
           & CommaList(Name & tok("|->") & G.Expression) 
           & tok("]") 

       |     tok("[") 
           & CommaList(Name & tok(":") & G.Expression)  
           & tok("]") 

       |      tok("[") 
           &  G.Expression 
           &  tok("EXCEPT") 
           &  CommaList(    tok("!")
                         & ( tok(".") & Name 
                             |  tok("[") & CommaList(G.Expression) & tok("]") )^+ 
                         &  tok("=") & G.Expression ) 
           &  tok("]") 

      |  G.Expression & tok(".") & Name

      |  tok("<<") & (CommaList(G.Expression) | Nil) & tok(">>") 

      |  G.Expression & (Tok({"\\X", "\\times"}) 
              & G.Expression)^+ 

      |  tok("[")  & G.Expression & tok("]_")  
           & G.Expression 

      | tok("<<") & G.Expression & tok(">>_") & G.Expression 

      |       Tok({"WF_", "SF_"}) 
           & G.Expression  
           & tok("(") & G.Expression & tok(")") 

      |       tok("IF")   & G.Expression 
           & tok("THEN")  & G.Expression  
           & tok("ELSE") & G.Expression 

      |  tok("CASE") 
         &  ( LET CaseArm == 
                     G.Expression & tok("->") & G.Expression
              IN  CaseArm & (tok("[]") & CaseArm)^* )

         &  (      Nil 
              |  (tok("[]") & tok("OTHER") & tok("->") & G.Expression)) 

     |        tok("LET") 
           &  (    G.OperatorDefinition 
                |  G.FunctionDefinition 
                |  G.ModuleDefinition)^+ 
           &  tok("IN") 
           &  G.Expression

     |  (tok("/\\") & G.Expression)^+ 

     |  (tok("\\/") & G.Expression)^+ 

     |  Number 

     |  String 

     |  tok("@")

IN LeastGrammar(P)

=============================================================================