Arend's specification syntax is based on Prolog, but is more flexible, with fewer predefined operators.
Arend's lexical syntax is largely defined in terms of Unicode character categories. Only a few characters are treated specially.
Whitespace is ignored, but required to separate some tokens. Comments normally count as whitespace.
Comments come in two forms:
// Single-line comment /* Multi-line comment */
Tokens are broken into three groups:
Atomic tokens start with a lowercase alphabetic (Ll or Lo) or numeric (Nd, Nl, or No) character, and are followed by any contiguous sequence of zero or more non-separator (see below) characters. As a special case, the empty list
is considered to be an atomic token.
Variable tokens start with an uppercase (Lu) alphabetic character or an underscore, and are followed by any contiguous sequence of zero or more non-separator (see below) characters.
Symbolic tokens are those that start with a character in one of the following classes: Sc, Sm, Sk, So, Pc, Pd, Po. This includes most symbolic and punctuation characters. This can be followed by any contiguous sequence of zero or more non-separator characters. (Grammatically, all symbolic tokens are assumed to be infix operators.)
Separator tokens are the following:
.This list may be extended to include all bracketing (Ps, Pe) and paired quoting (Pi, Pf) characters.
A raw token is any other type of token enclosed in backquotes. A raw token is exactly equivalent to the unquoted token, except that for symbolic tokens it is not assumed to be infix. Thus, the following are equivalent (assuming the term-based parsing described below):
a + b `+`(a,b)
Although Arend's specification language has only a handful of built-in operations, it's syntax includes support for a number of common extensions, under the assumption that specifications will want to use them in their natural forms. Thus, e.g., arithmetic operators are parsed according to the usual precedence, even though there are no built-in arithmetic operations.
The specification parser outputs a list of terms, from the
terms module. Atomic and variable tokens are translated into
Variables, respectively. Compound terms of the form
head(args...) or the infix form
lhs OP rhs are translated into
Compounds; for infix operators, the
OP becomes the head.
Bracket-enclosed lists are parsed specially. The internal syntax for lists is
a:b:c:, being equivalent to
[a,b,c]. The elements of the list can be any term.
Curly-braces are currently reserved for future extension, as are single- and double-quoted strings.
The grammatical syntax of Arend's specification language is roughly
specification = definition* definition = head ":-" body "." / head "." head = term body = term term = atomicTerm / infixTerm / prefixTerm / listTerm / "(" term ")" atomicTerm = atom infixTerm = term OP term // oversimplification termList = (term ("," term)*)? prefixTerm = atom "(" termList ")" listTerm = "[" termList "]"
Note that, due to the ambiguity with
,, infix terms with
, as their head inside lists must either be enclosed in parentheses or use the raw form of
Infix operators are parsed according to the following precedence table, from lowest to highest. The second column lists associativity.
Operator Assoc. Description ================= ======= ============================== h(...) (t) Compounds, parenthesized terms - ! Prefix minus, not ^ right Exponentiation * / % left Multiplication, division, mod + - left Addition, subtraction < <= > >= == != non Comparison : right Cons <user-defined infix operators> = other* Unification , & r,l Conjunction | ; left Disjunction :- left Predicate definition
Note that in the first group of operators, the descriptions are just the "standard" interpretations. These operators have no predefined meaning in Arend. The second group of operators includes those which have some semantic meaning in Arend.
Associativity of unification:
A = B = C is parsed as
A = B, B = C, except that the entire unification is setup all at once, so it's slightly more efficient.
Also note that while
, is right associative,
& is left associative.
Note that, in its current state, Arend's grammar requires memoization to be enabled in order to avoid exponential parsing time in some cases. Hopefully this will be remedied in the future.