Convenience-constructors
Utilities to conveniently construct abstract syntactic entities.
These functions and macros have short and evocative names,
to support the concise and readable construction of (constituents of) rules
in the abstract syntax.
These functions and macros are used only to define
the core rules [RFC:B] and the concrete syntax rules [RFC:4].
Thus, these function and macros only need to handle
the constructs used in those rules, not all possible constructs.
Before defining the actual constructors,
we introduce some predicates used in the constructors' guards.
Subtopics
- /_
- Construct a concatenation from a variable number of repetitions.
- %x-
- Construct a hexadecimal-base range numeric value notation element
from a minimum and a maximum.
- %d-
- Construct a decimal-base range numeric value notation element
from a minimum and a maximum.
- %b-
- Construct a binary-base range numeric value notation element
from a minimum and a maximum.
- =_
- Construct a non-incremental rule from
a rule name and a variable number of concatenations.
- =/_
- Construct an incremental rule from
a rule name and a variable number of concatenations.
- Def-rule-const
- Introduce an ACL2 constant for a (non-incremental) rule.
- =_-fn
- =/_-fn
- Repetition/element/rulename/charstring-p
- Recognize repetitions, elements, rule names, and character strings.
- <>
- Construct a prose value notation element from a character string.
- %x.
- Construct a hexadecimal-base direct numeric value notation element
from a variable number of numbers.
- %d.
- Construct a decimal-base direct numeric value notation element
from a variable number of numbers.
- %b.
- Construct a binary-base direct numeric value notation element
from a variable number of numbers.
- Repetition/element/rulename/charstring-listp
- Recognize true lists of
repetitions, elements, rule names, and character strings.
- ?_
- Construct an option from a variable number of concatenations.
- !_
- Construct a group from a variable number of concatenations.
- Def-rule-const-fn
- *_
- Construct a repetition of zero or more instances of an element.
- 1*_
- Construct a repetition of one or more instances of an element.
- ?_-fn
- /_-fn
- !_-fn
- Element/rulename-p
- Recognize elements and rule names.
- %x.-fn
- %d.-fn
- %b.-fn
