Orbital library

orbital.moon.logic
Class LogicParser

java.lang.Object
  extended by 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:

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()

Orbital library
1.3.0: 11 Apr 2009

Copyright © 1996-2009 André Platzer
All Rights Reserved.