Package org.smtlib.sexpr

Class Parser

java.lang.Object

org.smtlib.sexpr.Lexer

org.smtlib.sexpr.Parser

All Implemented Interfaces:

IParser

public class Parser
extends Lexer
implements IParser

Parses the standard SMT-LIB concrete syntax to produce ASTs of objects that are instances of the org.smtlib.* interfaces.

Nested Class Summary

Nested classes/interfaces inherited from class org.smtlib.sexpr.Lexer

Lexer.IPLexToken, Lexer.LexToken

Nested classes/interfaces inherited from interface org.smtlib.IParser

IParser.AbortInputException, IParser.ElementParser<T>, IParser.IFactory, IParser.ParserException, IParser.SyntaxException

Field Summary

Fields

Modifier and Type	Field	Description
protected boolean	commandHasError	Whether the command being parsed (or last returned) had a recoverable syntax error
protected boolean	commandHasLexicalError	Whether any such error was an invalid character, which the type checker does not see
IExpr.ISymbol	commandName	This field is used only to communicate the position of the name of a command to the command creator (instead of using method arguments).
protected final IExpr.IFactory	factory	The (common) factory used to generate objects
IResponse.IError	lastError	The most recent error, or null
ILexToken	savedlp	This field is used to communicate the beginning LP while parsing commands
static final String	UNEXPECTED_RESPONSE	The start of the error message for solver text that is not SMT-LIB (see parseResponse)

Fields inherited from class org.smtlib.sexpr.Lexer

badWhitespace, combined, csr, matcher, prefixCommentEnd, prefixCommentStart, prefixCommentText, sameLineTrailingEnd, sameLineTrailingStart, sameLineTrailingText, skipThroughEndOfLine

Constructor Summary

Constructors

Constructor	Description
Parser(SMT.Configuration smtConfig, ISource src)	Creates a Parser using an SMT configuration object and a source for characters; ordinarily use a factory to obtain a parser.

Method Summary

Modifier and Type	Method	Description
boolean	checkNoArg()	A helper check, called by command-specific parse methods in which the commands have no arguments
boolean	commandHasError()	Returns true if the command most recently returned by parseCommand() had a syntax error that parsing recovered from; such a command is not sent to a solver
boolean	commandHasLexicalError()	Returns true if one of the errors commandHasError() reports was an invalid character
IParser.ParserException	error(String msg, IPos pos)	Creates a ParserException with the given message and position; callers should throw the result.
IParser.ParserException	error(String msg, ILexToken token)	Creates a ParserException from the given message and token; callers should throw the result.
protected ILexToken	getToken(Matcher m)	Reports a vertical tab or form feed between tokens (except with --relax), which is then read as white space, and a keyword that is not a colon followed by a simple symbol (#185)
IResponse.IError	lastError()	Returns the most recent error, or null
List<IExpr>	parseAssertionList()	Parses a parenthesized list of terms, as returned by a get-assertions response.
List<IResponse.IPair<IExpr.ISymbol,Boolean>>	parseAssignmentList()	Parses a parenthesized list of (symbol bool) pairs, as returned by a get-assignment response.
IResponse.IPair<IExpr.ISymbol,Boolean>	parseAssignmentPair()	Parses one (symbol bool) pair, as found in a get-assignment response.
IExpr.IAttribute<?>	parseAttribute()	Parse an attribute (keyword with optional value), returning null with error messages if an error occurs.
protected IExpr.IAttribute<?>	parseAttributeRest(IExpr.IKeyword keyword)	Parses the (optional) value of an attribute whose keyword has already been parsed.
List<IExpr.IAttribute<?>>	parseAttributeSequence()	Parse a sequence of attributes (keyword with optional value) terminated by a right parenthesis, returning null with error messages if an error occurs.
IAttributeValue	parseAttributeValue()	Parse an attribute (keyword with optional value), returning null with error messages if an error occurs.
IExpr.IBinaryLiteral	parseBinary()	Parses a binary literal, returning null with the given message if an error occurs; if the next token is not a binary literal, the token is not consumed,
IExpr.IBinding	parseBinding()	Parses a binding "(id expression)", returning null with error messages if an error occurs
List<IExpr.IBinding>	parseBindings()	Parses a parenthesized sequence of let-bindings
Command	parseCommand()	Parses the next text in the source as a SMT-LIB command; if an error occurs, the error is logged and the method skips through a matching number of right parentheses
IExpr.IConstructor	parseConstructor()	Parses a constructor declaration "(symbol selector*)"
ISort.IDatatype	parseDatatype()	Parses a datatype declaration: "( constructor+ )" or "( par ( symbol+ ) ( constructor+ ) )"
IExpr.IDecimal	parseDecimal()	Parses a decimal, returning null with the given message if an error occurs; if the next token is not a decimal, the token is not consumed,
IExpr.IDeclaration	parseDeclaration()	Parses a declaration "(id sort)", returning null with error messages if an error occurs
List<IExpr.IDeclaration>	parseDeclarations()	Parses a parenthesized sequence of IDeclaration items
IExpr	parseExpr()	Parses an expression, returning null with error messages if there is not a valid expression in the token stream.
IExpr.IFunctionDeclaration	parseFunctionDeclaration()	Parses a function declaration "( symbol ( sorted_var* ) sort )" used in define-funs-rec
IExpr.IHexLiteral	parseHex()	Parses a hex literal, returning null with the given message if an error occurs; if the next token is not a hex literal, the token is not consumed,
IExpr.IIdentifier	parseIdentifier()	Parses an identifier (either symbol or parameterized identifier) from the token stream, returning null with logged error messages if there is not one.
SMTExpr.Keyword	parseKeyword()	Parses a keyword, returning null with an error message if an error occurs; if the next token is not a keyword, the token is not consumed.
<T> List<T>	parseList(IParser.ElementParser<T> elementParser, String kind, boolean allowEmpty)	Parses a parenthesized list of elements using the given element parser.
IExpr.ILiteral	parseLiteral()	Parses a literal, returning null with error messages if an error occurs.
ILogic	parseLogic()	Parses a logic definition (including beginning and ending parentheses, returning null with error messages if it fails; only part of the checking of the contents is performed in this call (the rest is done in loadLogic).
ILexToken	parseLP()	Parses a left parenthesis, returning null and emitting an error message if there isn't one (and the next token is not consumed)
IExpr.IMatchCase	parseMatchCase()	Parses a single match case: "(pattern term)"
IExpr.INumeral	parseNumeral()	Parses a numeral, returning null with error messages if an error occurs; if the next token is not a numeral, the token is not consumed,
IExpr.IPattern	parsePattern()	Parses a match pattern: either a bare symbol (or wildcard _) or "(symbol symbol*)" where params may include _
IExpr.IQualifiedIdentifier	parseQualifiedIdentifier()	Parses a qualified identifier (either a symbol, a parameterized identifier, or an as identifier) from the token stream, returning null (with logged error messages) if there is not one.
IResponse	parseResponse(String response)
ILexToken	parseRP()	Parses a right parenthesis, returning null and emitting an error message if there isn't one (and the next token is not consumed)
ICommand.IScript	parseScript()	Parses an SMT-LIB command script.
IExpr.ISelector	parseSelector()	Parses a selector declaration "(symbol sort)"
Sexpr.Seq	parseSeq(ILexToken lp)	Parses and adds Sexpr to a list until parseSexpr returns null (indicating a RightParen has been seen or end of input or an error)
ISexpr	parseSexpr()	Parses an Sexpr
Sort	parseSort(List<ISort.IParameter> parameters)	Parses a sort, returning null with error messages if a valid sort is not in the next parser tokens.
List<ISort>	parseSortList(List<ISort.IParameter> parameters)	Parses sequence of sorts up to a right-parenthesis, returning null with error messages if an error occurs.
SMTExpr.StringLiteral	parseStringLiteral()	Parses a string literal, returning null with an error message if an error occurs; if the next token is not a string literal, the token is not consumed,
SMTExpr.Symbol	parseSymbol()	Parses a symbol, returning null with messages and not advancing the parser if an error occurs
SMTExpr.Symbol	parseSymbol(String msg)	Parses a symbol (but not a reserved word unless the configuration field 'relax' is true), returning null with messages if an error occurs; the parser is advanced only if an actual symbol is parsed.
List<IExpr.ISymbol>	parseSymbolList()	Parses a parenthesized list of names, as returned by a get-unsat-core response.
SMTExpr.Symbol	parseSymbolOrReservedWord(String msg)	Parses a symbol or a reserved word, returning null with messages if an error occurs.
List<IExpr.IAttribute<?>>	parseTermAttributeSequence()	Parses the attributes of an annotated term (! t attr+) up to the right parenthesis.
List<IExpr>	parseTermList()	Parses a parenthesized list of terms, as returned by a get-unsat-assumptions response.
ITheory	parseTheory()	Parses a theory definition (including beginning and ending parentheses, returning null with error messages if it fails; only part of the checking of the contents is performed in this call (the rest is done in loadTheory).
List<IResponse.IPair<IExpr,IExpr>>	parseValueList()	Parses a parenthesized list of (term value) pairs, as returned by a get-value response.
IResponse.IPair<IExpr,IExpr>	parseValuePair()	Parses one (term value) pair, as found in a get-value response.
IPos	pos(int start, int end)	Returns an IPos object for the given character start and end positions and including a reference to the parser's source object.
IPos	pos(IPos start, IPos end)	Returns an IPos object for the given character start and end positions and including a reference to the parser's source object.
SMT.Configuration	smt()	Returns a handle to the parent SMTConfig object, in order to see command-line options etc.

Methods inherited from class org.smtlib.sexpr.Lexer

abortLine, currentPos, EOD, getToken, getToken, getToken, isEOD, isLP, isRP, LP, peekToken, RP, setPos, skipThruRP, source

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface org.smtlib.IParser

abortLine, checkUserId, isEOD, parseListDatatypes, parseListTerms

Field Details

lastError

public IResponse.IError lastError

The most recent error, or null

commandHasError

protected boolean commandHasError

Whether the command being parsed (or last returned) had a recoverable syntax error

commandHasLexicalError

protected boolean commandHasLexicalError

Whether any such error was an invalid character, which the type checker does not see

factory

protected final IExpr.IFactory factory

The (common) factory used to generate objects

savedlp

public ILexToken savedlp

This field is used to communicate the beginning LP while parsing commands

commandName

public IExpr.ISymbol commandName

This field is used only to communicate the position of the name of a command to the command creator (instead of using method arguments).

UNEXPECTED_RESPONSE

public static final String UNEXPECTED_RESPONSE

The start of the error message for solver text that is not SMT-LIB (see parseResponse)

See Also:

• Constant Field Values

Constructor Details

Parser

public Parser(SMT.Configuration smtConfig,
 ISource src)

Creates a Parser using an SMT configuration object and a source for characters; ordinarily use a factory to obtain a parser.

Method Details

smt

public SMT.Configuration smt()

Returns a handle to the parent SMTConfig object, in order to see command-line options etc. that are fields of smtConfig

Specified by:

smt in interface IParser

lastError

public IResponse.IError lastError()

Description copied from interface: IParser

Returns the most recent error, or null

Specified by:

lastError in interface IParser

commandHasError

public boolean commandHasError()

Description copied from interface: IParser

Returns true if the command most recently returned by parseCommand() had a syntax error that parsing recovered from; such a command is not sent to a solver

Specified by:

commandHasError in interface IParser

commandHasLexicalError

public boolean commandHasLexicalError()

Description copied from interface: IParser

Returns true if one of the errors commandHasError() reports was an invalid character

Specified by:

commandHasLexicalError in interface IParser

pos

public IPos pos(IPos start,
 IPos end)

Returns an IPos object for the given character start and end positions and including a reference to the parser's source object.

Parameters:

start - the start character position (counting from 0)

end - the end character position (one past the last actual character to be included)

Returns:

the IPos object representing the character range within the parser's current source

pos

public IPos pos(int start,
 int end)

Returns an IPos object for the given character start and end positions and including a reference to the parser's source object.

Overrides:

pos in class Lexer

Parameters:

start - the start character position (counting from 0)

end - the end character position (one past the last actual character to be included)

Returns:

the IPos object representing the character range within the parser's current source

parseScript

public ICommand.IScript parseScript()

Description copied from interface: IParser

Parses an SMT-LIB command script. The result is either a string literal or a parenthesized list of commands (which are parenthesized themselves); the string literal denotes the name of a file from which the commands are read when the command is executed; if the script is included directly, it is parsed, but typechecking is performed in context upon execution. If any errors occur, messages are logged and null is returned, with the parser advancing through a matching right parenthesis.

Specified by:

parseScript in interface IParser

Returns:

the parsed script

parseCommand

public Command parseCommand()

Parses the next text in the source as a SMT-LIB command; if an error occurs, the error is logged and the method skips through a matching number of right parentheses

Specified by:

parseCommand in interface IParser

Returns:

returns the parsed command, or EOD.eod if the end of input has been reached, or null if no valid command could be parsed

checkNoArg

public boolean checkNoArg()

A helper check, called by command-specific parse methods in which the commands have no arguments

parseSexpr

public ISexpr parseSexpr()
                  throws IParser.ParserException

Parses an Sexpr

Returns:

an Sexpr or null if no more input

Throws:

IParser.ParserException - if a parsing problem occurred, such as an invalid token or mismatched parentheses

parseSeq

public Sexpr.Seq parseSeq(ILexToken lp)
                   throws IParser.ParserException

Parses and adds Sexpr to a list until parseSexpr returns null (indicating a RightParen has been seen or end of input or an error)

Returns:

a SExpr.Seq containing the sequence of SExpr seen

Throws:

IParser.ParserException - FIXME - no more of these?

parseQualifiedIdentifier

public IExpr.IQualifiedIdentifier parseQualifiedIdentifier()
                                                    throws IParser.ParserException

Parses a qualified identifier (either a symbol, a parameterized identifier, or an as identifier) from the token stream, returning null (with logged error messages) if there is not one.

Specified by:

parseQualifiedIdentifier in interface IParser

Throws:

IParser.ParserException

parseIdentifier

public IExpr.IIdentifier parseIdentifier()
                                  throws IParser.ParserException

Parses an identifier (either symbol or parameterized identifier) from the token stream, returning null with logged error messages if there is not one.

Specified by:

parseIdentifier in interface IParser

Throws:

IParser.ParserException

parseExpr

public IExpr parseExpr()
                throws IParser.ParserException

Parses an expression, returning null with error messages if there is not a valid expression in the token stream.

Specified by:

parseExpr in interface IParser

Throws:

IParser.ParserException

parseDeclarations

public List<IExpr.IDeclaration> parseDeclarations()
                                           throws IParser.ParserException

Parses a parenthesized sequence of IDeclaration items

Specified by:

parseDeclarations in interface IParser

Throws:

IParser.ParserException

parseBindings

public List<IExpr.IBinding> parseBindings()
                                   throws IParser.ParserException

Parses a parenthesized sequence of let-bindings

Specified by:

parseBindings in interface IParser

Throws:

IParser.ParserException

parseSelector

public IExpr.ISelector parseSelector()
                              throws IParser.ParserException

Parses a selector declaration "(symbol sort)"

Specified by:

parseSelector in interface IParser

Throws:

IParser.ParserException

parseConstructor

public IExpr.IConstructor parseConstructor()
                                    throws IParser.ParserException

Parses a constructor declaration "(symbol selector*)"

Specified by:

parseConstructor in interface IParser

Throws:

IParser.ParserException

parseDatatype

public ISort.IDatatype parseDatatype()
                              throws IParser.ParserException

Parses a datatype declaration: "( constructor+ )" or "( par ( symbol+ ) ( constructor+ ) )"

Specified by:

parseDatatype in interface IParser

Throws:

IParser.ParserException

parseFunctionDeclaration

public IExpr.IFunctionDeclaration parseFunctionDeclaration()
                                                    throws IParser.ParserException

Parses a function declaration "( symbol ( sorted_var* ) sort )" used in define-funs-rec

Specified by:

parseFunctionDeclaration in interface IParser

Throws:

IParser.ParserException

parseDeclaration

public IExpr.IDeclaration parseDeclaration()
                                    throws IParser.ParserException

Parses a declaration "(id sort)", returning null with error messages if an error occurs

Specified by:

parseDeclaration in interface IParser

Throws:

IParser.ParserException

parseBinding

public IExpr.IBinding parseBinding()
                            throws IParser.ParserException

Parses a binding "(id expression)", returning null with error messages if an error occurs

Specified by:

parseBinding in interface IParser

Throws:

IParser.ParserException

parseList

public <T> List<T> parseList(IParser.ElementParser<T> elementParser,
 String kind,
 boolean allowEmpty)
                      throws IParser.ParserException

Parses a parenthesized list of elements using the given element parser.

Parameters:

elementParser - lambda that parses one element

kind - singular noun describing the element type (e.g. "term"), used in error messages

allowEmpty - if false, throws when the list is empty

Throws:

IParser.ParserException

parseSymbol

public SMTExpr.Symbol parseSymbol()
                           throws IParser.ParserException

Parses a symbol, returning null with messages and not advancing the parser if an error occurs

Specified by:

parseSymbol in interface IParser

Throws:

IParser.ParserException

parseSymbol

public SMTExpr.Symbol parseSymbol(String msg)
                           throws IParser.ParserException

Parses a symbol (but not a reserved word unless the configuration field 'relax' is true), returning null with messages if an error occurs; the parser is advanced only if an actual symbol is parsed. The error message is given by the argument; it may contain a '#' character that will be replaced by the kind() of the token actually observed; if the argument is null, no error message is emitted.

Throws:

IParser.ParserException

parseSymbolOrReservedWord

public SMTExpr.Symbol parseSymbolOrReservedWord(String msg)
                                         throws IParser.ParserException

Parses a symbol or a reserved word, returning null with messages if an error occurs. The error message is given by the argument; it may contain a '#' character that will be replaced by the kind() of the token actually observed.

Throws:

IParser.ParserException

parseLiteral

public IExpr.ILiteral parseLiteral()
                            throws IParser.ParserException

Parses a literal, returning null with error messages if an error occurs.

Specified by:

parseLiteral in interface IParser

Throws:

IParser.ParserException

parseNumeral

public IExpr.INumeral parseNumeral()
                            throws IParser.ParserException

Parses a numeral, returning null with error messages if an error occurs; if the next token is not a numeral, the token is not consumed,

Specified by:

parseNumeral in interface IParser

Throws:

IParser.ParserException

parseDecimal

public IExpr.IDecimal parseDecimal()
                            throws IParser.ParserException

Parses a decimal, returning null with the given message if an error occurs; if the next token is not a decimal, the token is not consumed,

Specified by:

parseDecimal in interface IParser

Throws:

IParser.ParserException

parseBinary

public IExpr.IBinaryLiteral parseBinary()
                                 throws IParser.ParserException

Parses a binary literal, returning null with the given message if an error occurs; if the next token is not a binary literal, the token is not consumed,

Specified by:

parseBinary in interface IParser

Throws:

IParser.ParserException

parseHex

public IExpr.IHexLiteral parseHex()
                           throws IParser.ParserException

Parses a hex literal, returning null with the given message if an error occurs; if the next token is not a hex literal, the token is not consumed,

Specified by:

parseHex in interface IParser

Throws:

IParser.ParserException

parseStringLiteral

public SMTExpr.StringLiteral parseStringLiteral()
                                         throws IParser.ParserException

Parses a string literal, returning null with an error message if an error occurs; if the next token is not a string literal, the token is not consumed,

Specified by:

parseStringLiteral in interface IParser

Throws:

IParser.ParserException

parseKeyword

public SMTExpr.Keyword parseKeyword()
                             throws IParser.ParserException

Parses a keyword, returning null with an error message if an error occurs; if the next token is not a keyword, the token is not consumed.

Specified by:

parseKeyword in interface IParser

Throws:

IParser.ParserException

parseSort

public Sort parseSort(List<ISort.IParameter> parameters)
               throws IParser.ParserException

Parses a sort, returning null with error messages if a valid sort is not in the next parser tokens.

Specified by:

parseSort in interface IParser

Throws:

IParser.ParserException

getToken

protected ILexToken getToken(Matcher m)
                      throws IParser.ParserException

Reports a vertical tab or form feed between tokens (except with --relax), which is then read as white space, and a keyword that is not a colon followed by a simple symbol (#185)

Overrides:

getToken in class Lexer

Throws:

IParser.ParserException

parseSortList

public List<ISort> parseSortList(List<ISort.IParameter> parameters)
                          throws IParser.ParserException

Parses sequence of sorts up to a right-parenthesis, returning null with error messages if an error occurs.

Throws:

IParser.ParserException

parseAttributeValue

public IAttributeValue parseAttributeValue()
                                    throws IParser.ParserException

Parse an attribute (keyword with optional value), returning null with error messages if an error occurs.

Specified by:

parseAttributeValue in interface IParser

Throws:

IParser.ParserException

parseAttribute

public IExpr.IAttribute<?> parseAttribute()
                                   throws IParser.ParserException

Parse an attribute (keyword with optional value), returning null with error messages if an error occurs.

Specified by:

parseAttribute in interface IParser

Throws:

IParser.ParserException

parseAttributeRest

protected IExpr.IAttribute<?> parseAttributeRest(IExpr.IKeyword keyword)
                                          throws IParser.ParserException

Parses the (optional) value of an attribute whose keyword has already been parsed.

Throws:

IParser.ParserException

parseAttributeSequence

public List<IExpr.IAttribute<?>> parseAttributeSequence()
                                                 throws IParser.ParserException

Parse a sequence of attributes (keyword with optional value) terminated by a right parenthesis, returning null with error messages if an error occurs.

Throws:

IParser.ParserException

parseTermAttributeSequence

public List<IExpr.IAttribute<?>> parseTermAttributeSequence()
                                                     throws IParser.ParserException

Parses the attributes of an annotated term (! t attr+) up to the right parenthesis. Like parseAttributeSequence(), except that a :pattern value is parsed as what SMT-LIB defines it to be, a parenthesized (possibly empty, per SMT-LIB 2.7) list of terms, giving an IExpr.IPatternTerms -- the same representation the expression factory builds. A :pattern value that is not a list is left for the TypeChecker to report.

Throws:

IParser.ParserException

parseLogic

public ILogic parseLogic()
                  throws IParser.ParserException

Parses a logic definition (including beginning and ending parentheses, returning null with error messages if it fails; only part of the checking of the contents is performed in this call (the rest is done in loadLogic).

Specified by:

parseLogic in interface IParser

Throws:

IParser.ParserException

parseTheory

public ITheory parseTheory()
                    throws IParser.ParserException

Parses a theory definition (including beginning and ending parentheses, returning null with error messages if it fails; only part of the checking of the contents is performed in this call (the rest is done in loadTheory).

Specified by:

parseTheory in interface IParser

Throws:

IParser.ParserException

parseAssertionList

public List<IExpr> parseAssertionList()
                               throws IParser.ParserException

Parses a parenthesized list of terms, as returned by a get-assertions response.

Throws:

IParser.ParserException

parseTermList

public List<IExpr> parseTermList()
                          throws IParser.ParserException

Parses a parenthesized list of terms, as returned by a get-unsat-assumptions response.

Throws:

IParser.ParserException

parseSymbolList

public List<IExpr.ISymbol> parseSymbolList()
                                    throws IParser.ParserException

Parses a parenthesized list of names, as returned by a get-unsat-core response.

Throws:

IParser.ParserException

parseValuePair

public IResponse.IPair<IExpr,IExpr> parseValuePair()
                                            throws IParser.ParserException

Parses one (term value) pair, as found in a get-value response.

Throws:

IParser.ParserException

parseValueList

public List<IResponse.IPair<IExpr,IExpr>> parseValueList()
                                                  throws IParser.ParserException

Parses a parenthesized list of (term value) pairs, as returned by a get-value response.

Throws:

IParser.ParserException

parseAssignmentPair

public IResponse.IPair<IExpr.ISymbol,Boolean> parseAssignmentPair()
                                                           throws IParser.ParserException

Parses one (symbol bool) pair, as found in a get-assignment response.

Throws:

IParser.ParserException

parseAssignmentList

public List<IResponse.IPair<IExpr.ISymbol,Boolean>> parseAssignmentList()
                                                                 throws IParser.ParserException

Parses a parenthesized list of (symbol bool) pairs, as returned by a get-assignment response.

Throws:

IParser.ParserException

parseResponse

public IResponse parseResponse(String response)
                        throws IParser.ParserException

Throws:

IParser.ParserException

parseLP

public ILexToken parseLP()
                  throws IParser.ParserException

Parses a left parenthesis, returning null and emitting an error message if there isn't one (and the next token is not consumed)

Throws:

IParser.ParserException

parseRP

public ILexToken parseRP()
                  throws IParser.ParserException

Parses a right parenthesis, returning null and emitting an error message if there isn't one (and the next token is not consumed)

Throws:

IParser.ParserException

error

public IParser.ParserException error(String msg,
 IPos pos)

Creates a ParserException with the given message and position; callers should throw the result.

error

public IParser.ParserException error(String msg,
 ILexToken token)

Creates a ParserException from the given message and token; callers should throw the result. If the token is a lexical error token, the exception carries the lexer's message instead.

parseMatchCase

public IExpr.IMatchCase parseMatchCase()
                                throws IParser.ParserException

Parses a single match case: "(pattern term)"

Throws:

IParser.ParserException

parsePattern

public IExpr.IPattern parsePattern()
                            throws IParser.ParserException

Parses a match pattern: either a bare symbol (or wildcard _) or "(symbol symbol*)" where params may include _

Throws:

IParser.ParserException