		Search-engine friendly clone of the ACL2 documentation.

Concrete-syntax

Parser

An executable parser of PFCS.

If you are looking for API functions for calling the PFCS parser, please see parser-interface.

This is a fairly simple parser for the PFCS syntactic grammar. The parser consists of a collection of parsing functions that operate on a sequence of tokens. Most parsing functions take a lookahead token (an optional ABNF tree) and a sequence of the remaining tokens (list of ABNF trees).

Each ABNF tree in the sequence of tokens (and the lookahead token) should have a rulename from the right hand side of the ABNF rule for token indicating the kind of token it is:

token = identifier / integer / operator / separator

All the parsing functions return, as first result, an ABNF tree or list of trees that represents the parsed input. This is called a CST (Concrete Syntax Tree).

Almost all the parsing functions also return the next unparsed token and the tokens that follow it. That is, they prefetch the token, so it is ready for the next function. If the end of the input is reached, the next token is nil (and so is the list of tokens after it).

Subtopics

Parse-separator: Parse a specified separator.
Parse-operator: Parse a specified operator.
Parse-definition: Parse a definition.
Parse-relation-constraint: Parse a relation-constraint.
Parse-equality-constraint: Parse an equality-constraint.
Parse-*-comma-identifier: Parse a *( "," identifier ).
Parse-*-comma-expression: Parse a *( "," expression ).
Parse-*-comma-constraint: Parse a *( "," constraint ).
Parse-system: Parse a PFCS system.
Parse-identifier: Parse an identifier.
Parse-primary-expression: Parse a primary-expression.
Parse-pfcs-integer: Parse an integer token.
Parse-constraint: Parse a constraint.
Parse-*-definition: Parse a *definition.
Parse-*-constraint: Parse a *constraint.
Parse-expression: Parse an expression.
Parsize: Size of the parser input.
Check-token-string: Check if the given token is present and has the given string as fringe.
Check-token-root: Check if the given token is present and has the given rule name as root.
Parse-token: Parse a token.
Token-stringp: Check if the given token has the given string as fringe.
Token-rootp: Check if the given token has the given rule name as root.
Patbind-pok<: b* binder for checking and propagating error results of parsing functions and ensuring termination.
Parse-multiplication-expression-rest: Parse the rest of a multiplication-expression.
Parse-addition-expression-rest: Parse the rest of a addition-expression.
Parse-multiplication-expression: Parse a multiplication-expression.
Parse-addition-expression: Parse a addition-expression.
Patbind-pok: b* binder for checking and propagating error results of parsing functions.
Perr: Returning a parsing error.