net.sourceforge.czt.animation.eval

Class TextUI

java.lang.Object

net.sourceforge.czt.animation.eval.TextUI

public class TextUI
extends Object

A text-based user interface for the ZLive animator.

Author:

marku

Field Summary

Fields

Modifier and Type	Field and Description
protected static boolean	DEBUG Turn this on to see stack traces upon errors.
protected PrintWriter	output_ The current output stream
protected Stack<ZLiveResult>	stack_
protected ZLive	zlive_ The animator engine

Constructor Summary

Constructors

Constructor and Description
TextUI(ZLive zlive, PrintWriter output) Constructs a new ZLive textual user interface.

Method Summary

Modifier and Type	Method and Description
void	doApplyRule(String args) Implements the 'apply rulename expr' command.
void	doConjectures() Tries to prove all the conjectures in the current section.
void	doEvalExprPred(String args, PrintWriter out)
String	doLoadSpec(String filename) Loads the given specification file into ZLive.
protected void	doMove(int offset)
void	doUnknownCmd(String cmd, String args) This is called for commands that processCmd does not handle.
PrintWriter	getOutput() The current output stream for messages and errors.
ZLive	getZLive() Get the instance of ZLive that is used for evaluation.
static void	main(String[] args) main entry point, which runs ZLive with System.in and System.out.
void	mainLoop(BufferedReader input) The main read-process loop.
net.sourceforge.czt.z.ast.Expr	parseExpr(String args, PrintWriter out) Same as parseTerm, but insists on the result being an Expr.
net.sourceforge.czt.base.ast.Term	parseTerm(String args, PrintWriter out) Parses and typechecks the string args into a Pred or an Expr.
void	printHelp(PrintWriter out) Prints the ZLive help/usage message
void	printSettings(PrintWriter out) Prints the current values of all the ZLive settings.
void	printSettingsHelp(PrintWriter out) Prints a help message about all the settings.
String	printTerm(net.sourceforge.czt.base.ast.Term term, net.sourceforge.czt.session.Markup markup)
void	printTypes(String sectName) Prints the names and types of the definitions in the given section.
void	processCmd(String cmd, String args) Process one input command.
void	setOutput(PrintWriter output) Set the current output writer.
void	setSetting(String name, String value) Set one of the ZLive settings to the given value.
net.sourceforge.czt.base.ast.Term	unfoldTerm(net.sourceforge.czt.base.ast.Term term) Returns the preprocessed form of a term, before evaluation starts.

Methods inherited from class java.lang.Object

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

Field Detail

zlive_

protected ZLive zlive_

The animator engine

DEBUG

protected static boolean DEBUG

Turn this on to see stack traces upon errors.

output_

protected PrintWriter output_

The current output stream

stack_

protected Stack<ZLiveResult> stack_

Constructor Detail

TextUI

public TextUI(ZLive zlive,
              PrintWriter output)

Constructs a new ZLive textual user interface. If the output PrintWriter is null, then System.out is used as the default output device.

Parameters:

zlive - The animation engine.

output - The output writer (optional).

Method Detail

getZLive

public ZLive getZLive()

Get the instance of ZLive that is used for evaluation.

getOutput

public PrintWriter getOutput()

The current output stream for messages and errors.

setOutput

public void setOutput(PrintWriter output)

Set the current output writer.

main

public static void main(String[] args)
                 throws IOException,
                        net.sourceforge.czt.session.CommandException

main entry point, which runs ZLive with System.in and System.out.

Throws:

IOException

net.sourceforge.czt.session.CommandException

mainLoop

public void mainLoop(BufferedReader input)
              throws IOException

The main read-process loop.

Throws:

IOException

processCmd

public void processCmd(String cmd,
                       String args)

Process one input command. This handles most of the commands listed in printHelp. However, 'quit' must be handled by the caller. Unknown commands are passed on to doUnknownCmd.

doUnknownCmd

public void doUnknownCmd(String cmd,
                         String args)

This is called for commands that processCmd does not handle. The default implementation just prints an error message. However, it could be overridden to handle additional commands.

Parameters:

cmd -

args -

doLoadSpec

public String doLoadSpec(String filename)
                  throws net.sourceforge.czt.session.CommandException

Loads the given specification file into ZLive.

Throws:

net.sourceforge.czt.session.CommandException

doEvalExprPred

public void doEvalExprPred(String args,
                           PrintWriter out)
                    throws IOException,
                           net.sourceforge.czt.session.CommandException

Throws:

IOException

net.sourceforge.czt.session.CommandException

doMove

protected void doMove(int offset)

doConjectures

public void doConjectures()
                   throws net.sourceforge.czt.session.CommandException

Tries to prove all the conjectures in the current section. Proof consists of exhaustively checking all possible instantiations of the conjecture, which is similar to model-checking. This command means that conjectures are a convenient way of storing ZLive examples and regression tests in a Z section.

Throws:

net.sourceforge.czt.session.CommandException

doApplyRule

public void doApplyRule(String args)
                 throws net.sourceforge.czt.session.CommandException,
                        IOException,
                        UnboundJokerException

Implements the 'apply rulename expr' command. This is useful for debugging rules.

Parameters:

args -

Throws:

net.sourceforge.czt.session.CommandException

IOException

UnboundJokerException

printSettings

public void printSettings(PrintWriter out)

Prints the current values of all the ZLive settings. NOTE: when you change this, make sure you update printSettingsHelp too.

printSettingsHelp

public void printSettingsHelp(PrintWriter out)

Prints a help message about all the settings.

setSetting

public void setSetting(String name,
                       String value)
                throws net.sourceforge.czt.session.CommandException

Set one of the ZLive settings to the given value.

Throws:

net.sourceforge.czt.session.CommandException

printHelp

public void printHelp(PrintWriter out)

Prints the ZLive help/usage message

printTypes

public void printTypes(String sectName)
                throws net.sourceforge.czt.session.CommandException

Prints the names and types of the definitions in the given section.

Throws:

net.sourceforge.czt.session.CommandException

printTerm

public String printTerm(net.sourceforge.czt.base.ast.Term term,
                        net.sourceforge.czt.session.Markup markup)

parseTerm

public net.sourceforge.czt.base.ast.Term parseTerm(String args,
                                                   PrintWriter out)
                                            throws IOException,
                                                   net.sourceforge.czt.session.CommandException

Parses and typechecks the string args into a Pred or an Expr. The result will be null if args contains parse or type errors. Otherwise it will be a Term. You can use 'instanceof Pred' to find out if the result is a predicate or an expression.

Parameters:

args - String containing an expression or predicate

out - Where to print error and progress messages.

Returns:

The typechecked Pred/Expr, or null if it contained errors.

Throws:

IOException

net.sourceforge.czt.session.CommandException

parseExpr

public net.sourceforge.czt.z.ast.Expr parseExpr(String args,
                                                PrintWriter out)
                                         throws IOException,
                                                net.sourceforge.czt.session.CommandException

Same as parseTerm, but insists on the result being an Expr.

Throws:

IOException

net.sourceforge.czt.session.CommandException

unfoldTerm

public net.sourceforge.czt.base.ast.Term unfoldTerm(net.sourceforge.czt.base.ast.Term term)
                                             throws net.sourceforge.czt.session.CommandException,
                                                    EvalException,
                                                    UnboundJokerException

Returns the preprocessed form of a term, before evaluation starts. This is mostly used for debugging

Throws:

net.sourceforge.czt.session.CommandException

EvalException

UnboundJokerException