fmrisc.ProofNavigator

Class Main

java.lang.Object

fmrisc.ProofNavigator.Main

public final class Main
extends java.lang.Object

Command line interface to ProofNavigator.

Constructor Summary

Constructors

Constructor and Description
Main()

Method Summary

Methods

Modifier and Type	Method and Description
static boolean	ask(java.lang.String question) Ask question to be answered by user with 'y' or 'n'
static java.lang.String	askText(java.lang.String question) Prompt a question and read the answer.
static void	displayDeclarations() Signal that declarations are to be displayed.
static boolean	displayGoal(Declaration[] decls, FormulaDeclaration goal) Display goal
static void	exit(int code) Terminate program with denoted exit code.
static java.lang.String	getVersion() Return version string.
static void	init() Initialize the system state.
static boolean	isRunning() Signal whether command is being processed.
static void	main(java.lang.String[] args) Command line interface to ProofNavigator.
static void	mainInternal(Top top) ProgramExplorer interface to ProofNavigator
static boolean	newDeclaration(Declaration decl) Signal new declaration.
static boolean	open(java.lang.String path) Read command from file with denoted path.
static Command	parse() Parse next command.
static Command	parseString(java.lang.String string) Parse string as command.
static void	proofDone(Proof proof) Signal that proof is completed.
static void	quit() Quit (session or current proof) after asking user whether to do so.
static java.lang.String	readLine() Read line of input from console.
static int	readNumber(java.lang.String prompt, int a, int b) Ask user for a number in the range a..b.
static void	resetProof() Signal there is no current proof.
static void	run() Run ProofNavigator interpreter.
static boolean	setContext(java.lang.String path) Set context directory.
static void	setProof(Proof proof) Signal current proof.
static void	setProofState(ProofState state) Signal current proof state.
static void	setProperties(java.lang.String context, java.lang.String cvcl, State.ProverVersion version, boolean firstOrder, boolean toLogical) Set various properties.

Methods inherited from class java.lang.Object

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

Constructor Detail

Main

public Main()

Method Detail

main

public static void main(java.lang.String[] args)

Command line interface to ProofNavigator.

Parameters:

args - command line arguments (call with "--help" to see which)

mainInternal

public static void mainInternal(Top top)

ProgramExplorer interface to ProofNavigator

Parameters:

top - the Top instance used by the ProgramExplorer

getVersion

public static java.lang.String getVersion()

Return version string.

init

public static void init()

Initialize the system state.

run

public static void run()

Run ProofNavigator interpreter. Assumes that input/output interface has been initialized.

parse

public static Command parse()

Parse next command.

Returns:

next command parsed (null, if a syntax error occured).

parseString

public static Command parseString(java.lang.String string)

Parse string as command.

Parameters:

string - the string to be passed.

Returns:

the command (null, if a syntax error occured).

exit

public static void exit(int code)

Terminate program with denoted exit code.

Parameters:

code - the exit code

quit

public static void quit()

Quit (session or current proof) after asking user whether to do so. Saves the proof in current store, if this is what the user wants.

readLine

public static java.lang.String readLine()

Read line of input from console.

Returns:

the line (null, if an error occured)

askText

public static java.lang.String askText(java.lang.String question)

Prompt a question and read the answer.

Parameters:

question - the question.

Returns:

the answer.

readNumber

public static int readNumber(java.lang.String prompt,
             int a,
             int b)

Ask user for a number in the range a..b.

Parameters:

prompt - the message printed for asking.

a - the lower bound of the number.

b - the upper bound of the number.

Returns:

number in range a..b or -1 (if no number was given)

ask

public static boolean ask(java.lang.String question)

Ask question to be answered by user with 'y' or 'n'

Parameters:

question - the question asked

Returns:

true iff answer was 'y'

setProof

public static void setProof(Proof proof)

Signal current proof.

Parameters:

proof - the current proof

resetProof

public static void resetProof()

Signal there is no current proof.

setProofState

public static void setProofState(ProofState state)

Signal current proof state.

Parameters:

state - the current proof state.

newDeclaration

public static boolean newDeclaration(Declaration decl)

Signal new declaration.

Parameters:

decl - the new declaration.

Returns:

true iff everything went okay.

displayGoal

public static boolean displayGoal(Declaration[] decls,
                  FormulaDeclaration goal)

Display goal

Parameters:

decls - the declaration list.

goal - the goal declaration.

Returns:

true iff everything went okay.

displayDeclarations

public static void displayDeclarations()

Signal that declarations are to be displayed.

open

public static boolean open(java.lang.String path)

Read command from file with denoted path.

Parameters:

path - the (absolute or relative) path to the file.

Returns:

true iff everything went okay.

setContext

public static boolean setContext(java.lang.String path)

Set context directory.

Parameters:

path - the (absolute or relative) path to context directory (if null, a default path is used).

Returns:

true iff everything went okay.

isRunning

public static boolean isRunning()

Signal whether command is being processed.

Returns:

true iff command is being processed.

proofDone

public static void proofDone(Proof proof)

Signal that proof is completed.

Parameters:

proof - the completed proof.

setProperties

public static void setProperties(java.lang.String context,
                 java.lang.String cvcl,
                 State.ProverVersion version,
                 boolean firstOrder,
                 boolean toLogical)

Set various properties.

Parameters:

context - the context directory.

cvcl - the prover command path.

version - the prover version.

firstOrder - true if logic is first order

toLogical - true if formula type is LOGICAL.