libtlafmt 0.4.1

A formatter library for TLA+ specs, core of tlafmt
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

------------------------- MODULE ConfigFileGrammar --------------------------
EXTENDS BNFGrammars
-----------------------------------------------------------------------------
Letter == OneOf("abcdefghijklmnopqrstuvwxyz_ABCDEFGHIJKLMNOPQRSTUVWXYZ")
Num    == OneOf("0123456789")
LetterOrNum == Letter \cup Num
AnyChar     == LetterOrNum \cup OneOf("~!@#\\$%^&*-+=|(){}[],:;`'<>.?/")
SingularKW  == {"SPECIFICATION", "INIT", "NEXT", "VIEW", "SYMMETRY"}
PluralKW == 
  {"CONSTRAINT", "CONSTRAINTS", "ACTION-CONSTRAINT", "ACTION-CONSTRAINTS", 
   "INVARIANT", "INVARIANTS", "PROPERTY", "PROPERTIES"}
Keyword  == SingularKW \cup PluralKW \cup {"CONSTANT", "CONSTANTS"}
AnyIdent == LetterOrNum^* & Letter & LetterOrNum^*
Ident    == AnyIdent \ Keyword
-----------------------------------------------------------------------------
ConfigGrammar ==
  LET P(G) ==
        /\ G.File ::= G.Statement^+
        /\ G.Statement ::=   Tok(SingularKW) & Tok(Ident)
                           | Tok(PluralKW) & Tok(Ident)^*
                           |   Tok({"CONSTANT", "CONSTANTS"}) 
                             & (G.Replacement | G.Assignment)^*
        /\ G.Replacement ::= Tok(Ident) & tok("<-") & Tok(AnyIdent)
        /\ G.Assignment  ::= Tok(Ident) & tok("=") & G.IdentValue
        /\ G.IdentValue  ::=   
              Tok(AnyIdent) | G.Number | G.String
            |    tok("{") 
              &  (Nil | G.IdentValue & (tok(",") & G.IdentValue)^*)
              &  tok("}")
        /\ G.Number ::= (Nil | tok("-")) & Tok(Num^+)
        /\ G.String ::= tok("\"") & Tok(AnyChar^*) & tok("\"") 
   IN  LeastGrammar(P)
=============================================================================