search

tlaplus / tlaplus-standard

A collection of various standards, proposed or established, related to TLA+
MIT License
5 stars 1 forks source link

Updated TLA+2 BNF grammar spec to better conform with language standard, including subexpressions #2

Closed ahelwer closed 1 year ago

ahelwer commented 3 years ago

These changes fix numerous issues with the existing TLA+2 BNF grammar spec, backporting a number of changes from the SANY parser and adding some missing rules. Changelist:

  1. Restricted allowed syntax for INSTANCE substitutions
  2. Allowed use of RECURSIVE operator declarations inside LET-IN constructs
  3. Removed underscore from allowed characters in ProofStepId
  4. Made large changes to InstOrSubexprPrefix rule to match SANY functioning
  5. Encoded when to use - vs -. for the negative prefix operator
  6. Separated ProofStepId from GeneralIdentifier rule
  7. Added nonfix operators, for example +(1,2)
  8. Broke up Expression rule to allow definition of SubscriptExpression rule