fmrisc.ProofNavigator

Class PNParser

java.lang.Object

antlr.Parser

antlr.LLkParser

fmrisc.ProofNavigator.PNParser

All Implemented Interfaces:

PNParserTokenTypes

public class PNParser
extends antlr.LLkParser
implements PNParserTokenTypes

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String[]	_tokenNames
static antlr.collections.impl.BitSet	_tokenSet_0
static antlr.collections.impl.BitSet	_tokenSet_1
static antlr.collections.impl.BitSet	_tokenSet_2

Fields inherited from interface fmrisc.ProofNavigator.PNParserTokenTypes

ARROW, ASSIGNMENT, BITAND, BITNOT, BITOR, COLON, COMMA, COMMENT, DIGIT, DIVIDES, DOTDOT, EOF, EOL, EQUALITY, EQUIV, GREATER, GREATEREQ, IDENT, IGNORE, IMPLIES, LABEL, LBRACK, LBRACKGRID, LESS, LESSEQ, LETTER, LITERAL_AND, LITERAL_ARRAY, LITERAL_assume, LITERAL_auto, LITERAL_autostar, LITERAL_AXIOM, LITERAL_BIT, LITERAL_BITFALSE, LITERAL_BITTRUE, LITERAL_BOOLEAN, LITERAL_case, LITERAL_counterexample, LITERAL_decompose, LITERAL_ELSE, LITERAL_ELSIF, LITERAL_ENDIF, LITERAL_environment, LITERAL_EXISTS, LITERAL_expand, LITERAL_FALSE, LITERAL_flatten, LITERAL_flip, LITERAL_FORALL, LITERAL_FORMULA, LITERAL_goal, LITERAL_goto, LITERAL_IF, LITERAL_in, LITERAL_IN, LITERAL_induction, LITERAL_instantiate, LITERAL_INT, LITERAL_LAMBDA, LITERAL_lemma, LITERAL_LET, LITERAL_LOGICAL, LITERAL_LOGICALFALSE, LITERAL_LOGICALTRUE, LITERAL_NAT, LITERAL_newcontext, LITERAL_next, LITERAL_NOT, LITERAL_OF, LITERAL_open, LITERAL_option, LITERAL_OR, LITERAL_prev, LITERAL_printf, LITERAL_printt, LITERAL_printv, LITERAL_proof, LITERAL_prove, LITERAL_quit, LITERAL_read, LITERAL_REAL, LITERAL_redo, LITERAL_scatter, LITERAL_simplify, LITERAL_skolemize, LITERAL_split, LITERAL_state, LITERAL_SUBTYPE, LITERAL_tcc, LITERAL_THEN, LITERAL_TRUE, LITERAL_TYPE, LITERAL_typeaxiom, LITERAL_undo, LITERAL_WITH, LITERAL_XOR, LPAR, LPARGRID, MINUS, NONEQUALITY, NULL_TREE_LOOKAHEAD, NUMBER, PERIOD, PLUS, POWER, RBRACK, RBRACKGRID, REALLETTER, RPAR, RPARGRID, SEMICOLON, STRING, TIMES, UNDERSCORE, WS

Constructor Summary

Constructors

Constructor and Description
PNParser(antlr.ParserSharedInputState state)
PNParser(antlr.TokenBuffer tokenBuf)
PNParser(antlr.TokenStream lexer)

Method Summary

Methods

Modifier and Type	Method and Description
Declaration	declaration()
Command	main()
void	param(java.util.Vector sequence)
TypedIdentifier[]	paramList()
Type	typeExp()
Type	typeExpBase()
Expression	valueExp()
Expression	valueExp0()
Expression	valueExp10()
Expression	valueExp3()
Expression	valueExp30()
Expression	valueExp40()
Expression	valueExp43()
Expression	valueExp45()
Expression	valueExp5()
Expression	valueExp50()
Expression	valueExp6()
Expression	valueExp60()
Expression	valueExp70()
Expression	valueExp8()
Expression	valueExp9()
Expression	valueExp90()
ValueDeclaration	vdeclaration()

Methods inherited from class antlr.LLkParser

consume, LA, LT, traceIn, traceOut

Methods inherited from class antlr.Parser

addMessageListener, addParserListener, addParserMatchListener, addParserTokenListener, addSemanticPredicateListener, addSyntacticPredicateListener, addTraceListener, consumeUntil, consumeUntil, getAST, getASTFactory, getFilename, getInputState, getTokenName, getTokenNames, getTokenTypeToASTClassMap, isDebugMode, mark, match, match, matchNot, panic, recover, removeMessageListener, removeParserListener, removeParserMatchListener, removeParserTokenListener, removeSemanticPredicateListener, removeSyntacticPredicateListener, removeTraceListener, reportError, reportError, reportWarning, rewind, setASTFactory, setASTNodeClass, setASTNodeType, setDebugMode, setFilename, setIgnoreInvalidDebugCalls, setInputState, setTokenBuffer, traceIndent

Methods inherited from class java.lang.Object

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

Field Detail

_tokenNames

public static final java.lang.String[] _tokenNames

_tokenSet_0

public static final antlr.collections.impl.BitSet _tokenSet_0

_tokenSet_1

public static final antlr.collections.impl.BitSet _tokenSet_1

_tokenSet_2

public static final antlr.collections.impl.BitSet _tokenSet_2

Constructor Detail

PNParser

public PNParser(antlr.TokenBuffer tokenBuf)

PNParser

public PNParser(antlr.TokenStream lexer)

PNParser

public PNParser(antlr.ParserSharedInputState state)

Method Detail

main

public final Command main()
                   throws antlr.RecognitionException,
                          antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

declaration

public final Declaration declaration()
                              throws antlr.RecognitionException,
                                     antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

valueExp

public final Expression valueExp()
                          throws antlr.RecognitionException,
                                 antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

typeExp

public final Type typeExp()
                   throws antlr.RecognitionException,
                          antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

typeExpBase

public final Type typeExpBase()
                       throws antlr.RecognitionException,
                              antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

paramList

public final TypedIdentifier[] paramList()
                                  throws antlr.RecognitionException,
                                         antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

valueExp90

public final Expression valueExp90()
                            throws antlr.RecognitionException,
                                   antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

vdeclaration

public final ValueDeclaration vdeclaration()
                                    throws antlr.RecognitionException,
                                           antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

valueExp70

public final Expression valueExp70()
                            throws antlr.RecognitionException,
                                   antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

valueExp60

public final Expression valueExp60()
                            throws antlr.RecognitionException,
                                   antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

valueExp50

public final Expression valueExp50()
                            throws antlr.RecognitionException,
                                   antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

valueExp45

public final Expression valueExp45()
                            throws antlr.RecognitionException,
                                   antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

valueExp43

public final Expression valueExp43()
                            throws antlr.RecognitionException,
                                   antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

valueExp40

public final Expression valueExp40()
                            throws antlr.RecognitionException,
                                   antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

valueExp30

public final Expression valueExp30()
                            throws antlr.RecognitionException,
                                   antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

valueExp10

public final Expression valueExp10()
                            throws antlr.RecognitionException,
                                   antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

valueExp9

public final Expression valueExp9()
                           throws antlr.RecognitionException,
                                  antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

valueExp8

public final Expression valueExp8()
                           throws antlr.RecognitionException,
                                  antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

valueExp6

public final Expression valueExp6()
                           throws antlr.RecognitionException,
                                  antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

valueExp5

public final Expression valueExp5()
                           throws antlr.RecognitionException,
                                  antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

valueExp3

public final Expression valueExp3()
                           throws antlr.RecognitionException,
                                  antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

valueExp0

public final Expression valueExp0()
                           throws antlr.RecognitionException,
                                  antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException

param

public final void param(java.util.Vector sequence)
                 throws antlr.RecognitionException,
                        antlr.TokenStreamException

Throws:

antlr.RecognitionException

antlr.TokenStreamException