131 Lexical Grammar

The lexical grammar defines how characters in the source text are grouped into tokens such as identifiers, literals, keywords, and symbolic operators. These rules operate at the character level: outside string literals, whitespace and comments act only as separators and never appear within tokens. The syntactic grammar below is defined over the tokens produced by this lexical layer.

Grammar

Literal          = BooleanLiteral | IntegerLiteral | RealLiteral | StringLiteral ;

BooleanLiteral   = "false" | "true" ;

IntegerLiteral   = Digit, { Digit } ;

RealLiteral      = Digit, { Digit }, ".", Digit, { Digit } ;

StringLiteral    = SingleQuotedString | DoubleQuotedString ;

SingleQuotedString =
    "'", { SingleQuotedStringChar }, "'" ;

DoubleQuotedString =
    '"', { DoubleQuotedStringChar }, '"' ;

SingleQuotedStringChar =
      ? any character except "'", "\", CR, or LF ?
    | EscapeSequence ;

DoubleQuotedStringChar =
      ? any character except '"', "\", CR, or LF ?
    | EscapeSequence ;

EscapeSequence =
    "\", ? any character except CR or LF ? ;

Identifier       = ( Letter | "_" ), { Letter | Digit | "_" } ;

Letter           = "A" … "Z" | "a" … "z" ;

Digit            = "0" … "9" ;

Keyword =
      "abstract" | "as" | "break" | "catch"
    | "component" | "const" | "constraints" | "continue"
    | "date" | "defined" | "disjoint" | "dropped" | "dynamic" | "either"
    | "else" | "embed" | "entity" | "enum" | "equivalence"
    | "evolve" | "extern" | "first" | "fold" | "for"
    | "func" | "if" | "in" | "intersection" | "inverse"
    | "isa" | "key" | "let" | "name" | "namespace"
    | "none" | "object" | "order" | "over" | "print" | "proc" | "quotient"
    | "releases" | "return" | "schema" | "subtype" | "then"
    | "theorems" | "this" | "try" | "type" | "union" | "unreachable"
    | "unordered" | "using" | "value" | "var" | "variant"
    | "where" | "while" ;

HorizontalWhitespace = " " | "\t" ;

LineEnding       = "\n" | "\r\n" ;

Whitespace       = { HorizontalWhitespace | LineEnding } ;

Punctuation =
      "{" | "}" | "(" | ")" | "[" | "]"
    | "," | ";" | ":" | "@" | "?" | "&" ;

SymbolicOperator =
      "++"
    | "+=" | "-=" | "*=" | "/=" | "^="
    | "∪=" | "∩=" | "∖=" | ":="
    | "+" | "-" | "*" | "/" | "^"
    | "." | "--" | ".."
    | "\" | "∖"
    | "=" | "≠" | "<" | ">" | "≤" | "≥"
    | "⊓" | "⊔" | "|" | "∩" | "∪" | "⨝"
    | "⊂" | "⊃" | "⊆" | "⊇" | "⊄" | "⊅"
    | "∈" | "∉"
    | "⇒" | "→" | "←" | "↔"
    | "∨" | "∧" | "¬"
    | "Σ" | "∅" | "∞" | "!" | "~" | "↦"
    | "↑" | "↓" ;

Comment          = LineComment | BlockComment ;

LineComment      =
    "//", { ? any character except CR or LF ? } ;

BlockComment     =
    "/*", { ? any character except "*/" ? }, "*/" ;

Predica source is UTF-8 without a byte order mark. Identifiers deliberately use only the ASCII letters listed above; non-ASCII characters remain available in string literals and in the symbolic operators defined by the language. Source files use LF or CRLF line endings. A bare CR is not a valid line ending.

Keywords are reserved and cannot be used as identifiers. The spellings true and false are reserved Boolean literals rather than identifiers or keywords. Punctuation delimits grammatical constructs; symbolic operators denote operations or form part of operator syntax.

The declaration keywords func and proc introduce functions and procedures respectively. The full words “function” and “procedure” are used in specification prose but are not alternative declaration keywords.

Within a string literal, a backslash escapes the next source character. This allows the delimiter itself and a backslash to occur without terminating the literal. Escape sequences cannot contain a physical line ending. The lexical token retains the original source spelling; interpretation of an escape sequence occurs after lexing.

Whitespace and comments separate tokens and are otherwise discarded. Block comments do not nest: the first */ terminates the comment. End of file terminates a line comment, but reaching it inside a block comment or string literal is a lexical error.

When two symbolic operators share a prefix, the lexer chooses the longest token. For example, += is one token, not + followed by =. The same rule distinguishes ∪= from ∪ and .. from ..

Predica source has canonical Unicode spellings for some operators that are not easy to type on an ordinary keyboard. For set difference, the canonical source character is Unicode set minus ∖ (U+2216). The ordinary keyboard backslash \ (U+005C, reverse solidus) is accepted as an input alias for the same operator. Tools that format or rewrite Predica source may normalize that alias to the canonical ∖ spelling.