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
34
35
36
37
38

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/ConfigFileGrammar.tla
---
--------------------------- MODULE ConfigFileGrammar ---------------------------
EXTENDS BNFGrammars
--------------------------------------------------------------------------------
Letter == OneOf("abcdefghijklmnopqrstuvwxyz_ABCDEFGHIJKLMNOPQRSTUVWXYZ")
Num == OneOf("0123456789")
LetterOrNum == Letter \union Num
AnyChar == LetterOrNum \union OneOf("~!@#\\$%^&*-+=|(){}[],:;`'<>.?/")
SingularKW == {"SPECIFICATION", "INIT", "NEXT", "VIEW", "SYMMETRY"}
PluralKW ==
    {"CONSTRAINT", "CONSTRAINTS", "ACTION-CONSTRAINT", "ACTION-CONSTRAINTS",
        "INVARIANT", "INVARIANTS", "PROPERTY", "PROPERTIES"}
Keyword == SingularKW \union PluralKW \union {"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)
================================================================================