orbital.moon.logic
Class LogicParser

java.lang.Object
  orbital.moon.logic.LogicParser

All Implemented Interfaces:

LogicParserConstants

public class LogicParser
extends java.lang.Object
implements LogicParserConstants

It parses a concrete syntax (usually respecting the notation of symbols). This class implements a parser for logic and mathematical formulas that can be used for every logic after being bound to it. This parser calls ExpressionBuilder on every connection point (which specify the parser actions). Most ExpressionBuilders will simply construct a tree of Expressions (usually Formulas) whose implementation depends on the logic.

Although this distinction may sometimes sound artificial, we will - for the moment - distinguish three types of syntactic expressions:

• (arithmetic and functional) terms
• (logical) formulas
• unspecific expressions combining both terms and formulas

This parser can be used by implementations of ExpressionSyntax. So there is no need to interface with this parser directly. Instead, it is sufficient to call the ExpressionSyntax.createExpression(String) implementation of the specific logic - which could in turn invoke this parser.

Author:

André Platzer

See Also:

Grammar, ExpressionSyntax.createExpression(String), parseFormula(), parseFormulas(), parseTerm()

Field Summary

Token	jj_nt
boolean	lookingAhead
protected orbital.moon.logic.LogicParser.Scope	root The root scope, containing only the core signature.
protected orbital.moon.logic.LogicParser.Scope	scope The current scope.
protected ExpressionSyntax	syntax Delegate to the current syntax implementation that is used for building expressions.
Token	token
LogicParserTokenManager	token_source

Fields inherited from interface orbital.moon.logic.LogicParserConstants

AND, BOX, DECIMAL_LITERAL, DECLARE_FREE, DEFAULT, DIAMOND, DIGIT, DIGIT_OR_ALIKE, DIVIDE, EOF, EOL, EQUAL, EQUIV, EXISTS, EXPONENT, FLOATING_POINT_LITERAL, FORALL, FORMAL_COMMENT, GREATER, GREATER_EQUAL, IDENTIFIER, IMPLY, INTEGER_LITERAL, LAMBDA, LESS, LESS_EQUAL, LETTER, MINUS, MULTI_LINE_COMMENT, NOT, OR, PI, PLUS, PRODUCT, SINGLE_LINE_COMMENT, STRING_LITERAL, TIMES, tokenImage, UNEQUAL, XOR

Constructor Summary

LogicParser(java.io.InputStream stream)

LogicParser(java.io.InputStream stream, java.lang.String encoding)

LogicParser(LogicParserTokenManager tm)

LogicParser(java.io.Reader stream)

Method Summary

Expression	AndExpression()
protected Expression	apply(Token optok, Expression[] a, Type reqResult) n-ary predicates or functions.
Expression[]	Argument_list()
Expression[]	Arguments()
protected Type	asType(Expression f) Converts an expression to the type it represents.
Expression	Atom() A formula that is a logical atom.
Expression	AtomicTerm() Parse an atomic term (function application, number or string) for the current logic.
protected Expression	combine(Token optok, Expression[] a)
protected Expression	combine(Token optok, Symbol x, Expression a) quantifiers.
Expression	CompoundFormula() Parse a compound predicate formula for the current logic.
Expression	CompoundTerm() Parse a compound function term for the current logic.
Expression	CompoundType() A compound type.
Symbol	ConstantOrVariable() Parses a constant or a variable atomic term, depending upon known symbols in context.
void	disable_tracing()
void	enable_tracing()
Expression	EqualityExpression()
Expression	EquivalenceExpression()
Expression	ExclusiveOrExpression()
Expression	expression() Central expression parsing production.
Expression	FreeDeclarationExpression() free scope "quantifier" A "quantifier" with a purely syntactic function of declaring a variable.
ParseException	generateParseException()
Token	getNextToken()
Token	getToken(int index)
Expression	ImplicationExpression()
Expression	InclusiveOrExpression()
Expression	LambdaAbstraction() λ-abstraction term.
Expression	LambdaAbstractionPredicate() λ-abstraction predicate.
Symbol	LiteralValue() atomic term literal value (in the sense of constant primitive type), f.ex.
Expression	MapType()
Expression	ModalExpression()
Symbol	NumberLiteralValue() purely numeric atomic term literal value (in the sense of constant primitive type).
Expression	parseFormula() Start production parsing a logic formula with the current syntax.
Expression	parseFormulas() Start production parsing a set of logic formulas with the current syntax.
Expression	parseTerm() Start production parsing an arithmetic formula expression.
Type	parseType() Start production parsing a type expression with the current syntax.
Expression	PiAbstractionType()
Expression	PowerTerm()
Expression	PrimaryExpression() Final expression parsing production (in addition to Atom()).
Expression	PrimaryTerm() Final term parsing production (in addition to AtomicTerm()).
Expression	PrimaryType() A primary type.
Expression	ProductTerm()
Expression	ProductType()
Expression	QuantifiedExpression()
static Substitution	readTRS(java.io.Reader reader, ExpressionSyntax syntax) Reads a term-rewrite system from a stream.
static Substitution	readTRS(java.io.Reader reader, ExpressionSyntax syntax, Function expressionTransformation) Reads a term-rewrite system from a stream.
void	ReInit(java.io.InputStream stream)
void	ReInit(java.io.InputStream stream, java.lang.String encoding)
void	ReInit(LogicParserTokenManager tm)
void	ReInit(java.io.Reader stream)
void	setSyntax(ExpressionSyntax syntax) Set the current syntax for parsing.
Expression	SumTerm()
Expression	term() Central term parsing production.
Expression[]	Type_list()
Expression	type() Central type parsing production.
Expression[]	Types()
Type	typeUse() A type use.
Expression	UnaryExpression()
Expression	UnaryTerm()
Symbol	Variable() an atomic variable term.
Symbol	VariableDeclaration() an atomic variable term with a type declaration.

Methods inherited from class java.lang.Object

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

Field Detail

syntax

protected ExpressionSyntax syntax

Delegate to the current syntax implementation that is used for building expressions.

root

protected transient orbital.moon.logic.LogicParser.Scope root

The root scope, containing only the core signature.

scope

protected orbital.moon.logic.LogicParser.Scope scope

The current scope.

token_source

public LogicParserTokenManager token_source

token

public Token token

jj_nt

public Token jj_nt

lookingAhead

public boolean lookingAhead

Constructor Detail

LogicParser

public LogicParser(java.io.InputStream stream)

LogicParser

public LogicParser(java.io.InputStream stream,
                   java.lang.String encoding)

LogicParser

public LogicParser(java.io.Reader stream)

LogicParser

public LogicParser(LogicParserTokenManager tm)

Method Detail

setSyntax

public void setSyntax(ExpressionSyntax syntax)

Set the current syntax for parsing.

Parameters:

syntax - the expression syntax to use for parsing expressions (formulas).

asType

protected Type asType(Expression f)

Converts an expression to the type it represents.

Expression*	→	Type
f	↦	(Type) I0(f)

combine

protected Expression combine(Token optok,
                             Expression[] a)
                      throws ParseException

Throws:

ParseException

combine

protected Expression combine(Token optok,
                             Symbol x,
                             Expression a)
                      throws ParseException

quantifiers.

Throws:

ParseException

apply

protected Expression apply(Token optok,
                           Expression[] a,
                           Type reqResult)
                    throws ParseException

n-ary predicates or functions.

Parameters:

reqResult - specifies the required result type, as derived from the context. Object.class for functions, and Boolean.class for predicates.

Throws:

ParseException

See Also:

ExpressionBuilder.compose(Expression,Expression[])

readTRS

public static final Substitution readTRS(java.io.Reader reader,
                                         ExpressionSyntax syntax,
                                         Function expressionTransformation)
                                  throws java.io.IOException,
                                         ParseException

Reads a term-rewrite system from a stream. The concrete syntax of the TRS specification source is

 <matchingSide> |- <replacementSide>    # <comment> <EOL>
 ...
 

where <matchingSide> and <replacementSide> are well-formed expressions of the (concrete) syntax defined by syntax.

Parameters:

reader - the source for the TRS specification.

syntax - the syntax for parsing expressions.

expressionTransformation - the function Expression→T used for transforming the expressions parsed (<matchingSide> and <replacementSide>) prior to constructing the substitution.

Throws:

java.io.IOException - when an error occurs while reading from the reader.

ParseException - when a syntax error occurs in the source.

See Also:

ModernLogic#proveAll(Reader,ModernLogic,boolean)

readTRS

public static final Substitution readTRS(java.io.Reader reader,
                                         ExpressionSyntax syntax)
                                  throws java.io.IOException,
                                         ParseException

Reads a term-rewrite system from a stream. Using the identity transformation.

Throws:

java.io.IOException

ParseException

See Also:

readTRS(Reader,ExpressionSyntax,Function)

parseFormulas

public final Expression parseFormulas()
                               throws ParseException

Start production parsing a set of logic formulas with the current syntax.

Returns:

the set of formulas parsed, or an array of length 0 if only the empty set of formulas was found.

Throws:

ParseException

See Also:

parseFormula()

parseFormula

public final Expression parseFormula()
                              throws ParseException

Start production parsing a logic formula with the current syntax.

Throws:

ParseException

See Also:

parseFormulas()

parseTerm

public final Expression parseTerm()
                           throws ParseException

Start production parsing an arithmetic formula expression.

Throws:

ParseException

parseType

public final Type parseType()
                     throws ParseException

Start production parsing a type expression with the current syntax.

Throws:

ParseException

expression

public final Expression expression()
                            throws ParseException

Central expression parsing production.

Throws:

ParseException

FreeDeclarationExpression

public final Expression FreeDeclarationExpression()
                                           throws ParseException

free scope "quantifier" A "quantifier" with a purely syntactic function of declaring a variable.

Throws:

ParseException

EquivalenceExpression

public final Expression EquivalenceExpression()
                                       throws ParseException

Throws:

ParseException

ImplicationExpression

public final Expression ImplicationExpression()
                                       throws ParseException

Throws:

ParseException

InclusiveOrExpression

public final Expression InclusiveOrExpression()
                                       throws ParseException

Throws:

ParseException

ExclusiveOrExpression

public final Expression ExclusiveOrExpression()
                                       throws ParseException

Throws:

ParseException

AndExpression

public final Expression AndExpression()
                               throws ParseException

Throws:

ParseException

UnaryExpression

public final Expression UnaryExpression()
                                 throws ParseException

Throws:

ParseException

QuantifiedExpression

public final Expression QuantifiedExpression()
                                      throws ParseException

Throws:

ParseException

ModalExpression

public final Expression ModalExpression()
                                 throws ParseException

Throws:

ParseException

PrimaryExpression

public final Expression PrimaryExpression()
                                   throws ParseException

Final expression parsing production (in addition to Atom()). primary formulas that have truth values

Throws:

ParseException

Atom

public final Expression Atom()
                      throws ParseException

A formula that is a logical atom.

Throws:

ParseException

CompoundFormula

public final Expression CompoundFormula()
                                 throws ParseException

Parse a compound predicate formula for the current logic.

Throws:

ParseException

EqualityExpression

public final Expression EqualityExpression()
                                    throws ParseException

Throws:

ParseException

LambdaAbstractionPredicate

public final Expression LambdaAbstractionPredicate()
                                            throws ParseException

λ-abstraction predicate.

Throws:

ParseException

See Also:

Substitutions.lambda

term

public final Expression term()
                      throws ParseException

Central term parsing production. Parse a (non-formula) functional term for the current logic.

Throws:

ParseException

SumTerm

public final Expression SumTerm()
                         throws ParseException

Throws:

ParseException

ProductTerm

public final Expression ProductTerm()
                             throws ParseException

Throws:

ParseException

PowerTerm

public final Expression PowerTerm()
                           throws ParseException

Throws:

ParseException

UnaryTerm

public final Expression UnaryTerm()
                           throws ParseException

Throws:

ParseException

PrimaryTerm

public final Expression PrimaryTerm()
                             throws ParseException

Final term parsing production (in addition to AtomicTerm()).

Throws:

ParseException

CompoundTerm

public final Expression CompoundTerm()
                              throws ParseException

Parse a compound function term for the current logic.

Throws:

ParseException

LambdaAbstraction

public final Expression LambdaAbstraction()
                                   throws ParseException

λ-abstraction term.

Throws:

ParseException

See Also:

Substitutions.lambda

Note:

that (\x.2*x) can be parsed as expected because .2 is not a real number but only 0.2

AtomicTerm

public final Expression AtomicTerm()
                            throws ParseException

Parse an atomic term (function application, number or string) for the current logic.

Throws:

ParseException

LiteralValue

public final Symbol LiteralValue()
                          throws ParseException

atomic term literal value (in the sense of constant primitive type), f.ex. number or string value.

Throws:

ParseException

NumberLiteralValue

public final Symbol NumberLiteralValue()
                                throws ParseException

purely numeric atomic term literal value (in the sense of constant primitive type).

Throws:

ParseException

ConstantOrVariable

public final Symbol ConstantOrVariable()
                                throws ParseException

Parses a constant or a variable atomic term, depending upon known symbols in context.

Throws:

ParseException

See Also:

Variable()

Variable

public final Symbol Variable()
                      throws ParseException

an atomic variable term.

Throws:

ParseException

See Also:

ConstantOrVariable()

VariableDeclaration

public final Symbol VariableDeclaration()
                                 throws ParseException

an atomic variable term with a type declaration.

Throws:

ParseException

typeUse

public final Type typeUse()
                   throws ParseException

A type use.

Throws:

ParseException

type

public final Expression type()
                      throws ParseException

Central type parsing production. Parse a type expression for the current logic.

Throws:

ParseException

MapType

public final Expression MapType()
                         throws ParseException

Throws:

ParseException

ProductType

public final Expression ProductType()
                             throws ParseException

Throws:

ParseException

PiAbstractionType

public final Expression PiAbstractionType()
                                   throws ParseException

Throws:

ParseException

PrimaryType

public final Expression PrimaryType()
                             throws ParseException

A primary type.

Throws:

ParseException

CompoundType

public final Expression CompoundType()
                              throws ParseException

A compound type.

Throws:

ParseException

Arguments

public final Expression[] Arguments()
                             throws ParseException

Throws:

ParseException

Argument_list

public final Expression[] Argument_list()
                                 throws ParseException

Throws:

ParseException

Types

public final Expression[] Types()
                         throws ParseException

Throws:

ParseException

Type_list

public final Expression[] Type_list()
                             throws ParseException

Throws:

ParseException

ReInit

public void ReInit(java.io.InputStream stream)

ReInit

public void ReInit(java.io.InputStream stream,
                   java.lang.String encoding)

ReInit

public void ReInit(java.io.Reader stream)

ReInit

public void ReInit(LogicParserTokenManager tm)

getNextToken

public final Token getNextToken()

getToken

public final Token getToken(int index)

generateParseException

public ParseException generateParseException()

enable_tracing

public final void enable_tracing()

disable_tracing

public final void disable_tracing()