net.sourceforge.czt.animation.eval

Class Preprocess

java.lang.Object

net.sourceforge.czt.animation.eval.Preprocess

public final class Preprocess
extends Object

Preprocesses a term to get it ready for evaluation. This unfolds some Z constructs into simpler ones, using sets of rewrite rules. This class is marked as final just to remind developers that any subclass should re-implement the getClass().getResource(...) call in the setRules method.

Author:

marku

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
class	Preprocess.FixIdVisitor A temporary hack to fix up any incorrect ZName ids left/created by the typechecker.

Constructor Summary

Constructors

Constructor and Description
Preprocess(net.sourceforge.czt.session.SectionManager sectman) Create a term preprocessor that will apply a set of rules (see setRules) to a given term.

Method Summary

Modifier and Type	Method and Description
net.sourceforge.czt.base.ast.Term	fixIds(net.sourceforge.czt.base.ast.Term term) A temporary hack to fix up any incorrect ZName ids left/created by the typechecker.
net.sourceforge.czt.base.ast.Term	preprocess(String sectname, net.sourceforge.czt.base.ast.Term term) Rewrites the given term by firstly unfolding VarDecls with multiple variables (x,y:T), then appling all the rewrite rules of this Preprocess object to that term.
void	setRules(String rulesFile) Collects the rules of the first ZSect in a given source file.

Methods inherited from class java.lang.Object

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

Constructor Detail

Preprocess

public Preprocess(net.sourceforge.czt.session.SectionManager sectman)

Create a term preprocessor that will apply a set of rules (see setRules) to a given term.

Parameters:

sectman - The section manager used to find rule tables.

Method Detail

setRules

public void setRules(String rulesFile)
              throws IOException,
                     ParseException,
                     net.sourceforge.czt.session.CommandException

Collects the rules of the first ZSect in a given source file.

Parameters:

rulesFile - The name of the source file that contains the rules.

Throws:

IOException

ParseException

net.sourceforge.czt.session.CommandException

preprocess

public net.sourceforge.czt.base.ast.Term preprocess(String sectname,
                                                    net.sourceforge.czt.base.ast.Term term)
                                             throws net.sourceforge.czt.session.CommandException,
                                                    UnboundJokerException

Rewrites the given term by firstly unfolding VarDecls with multiple variables (x,y:T), then appling all the rewrite rules of this Preprocess object to that term. This should be called after type checking, so that VarDecls with multiple variables can be expanded correctly. (Section C.7.3.1 of the Z standard implies that x,y:T cannot be expanded until any generics in type T have been fully instantiated).

Parameters:

sectname - Gives the context for the proofs of rewrite rules.

term - The input term to rewrite.

Returns:

The rewritten term.

Throws:

net.sourceforge.czt.session.CommandException

UnboundJokerException

fixIds

public net.sourceforge.czt.base.ast.Term fixIds(net.sourceforge.czt.base.ast.Term term)

A temporary hack to fix up any incorrect ZName ids left/created by the typechecker.