net.sourceforge.czt.animation.eval

Class ResultTreeToZVisitor

java.lang.Object

net.sourceforge.czt.animation.eval.ResultTreeToZVisitor

All Implemented Interfaces:

EvalSetVisitor<net.sourceforge.czt.base.ast.Term>, PowerSetVisitor<net.sourceforge.czt.base.ast.Term>, ProdSetVisitor<net.sourceforge.czt.base.ast.Term>, RelSetVisitor<net.sourceforge.czt.base.ast.Term>, net.sourceforge.czt.base.visitor.TermVisitor<net.sourceforge.czt.base.ast.Term>, net.sourceforge.czt.util.Visitor<net.sourceforge.czt.base.ast.Term>, net.sourceforge.czt.z.visitor.LetExprVisitor<net.sourceforge.czt.base.ast.Term>

public class ResultTreeToZVisitor
extends Object
implements net.sourceforge.czt.base.visitor.TermVisitor<net.sourceforge.czt.base.ast.Term>, EvalSetVisitor<net.sourceforge.czt.base.ast.Term>, PowerSetVisitor<net.sourceforge.czt.base.ast.Term>, ProdSetVisitor<net.sourceforge.czt.base.ast.Term>, RelSetVisitor<net.sourceforge.czt.base.ast.Term>, net.sourceforge.czt.z.visitor.LetExprVisitor<net.sourceforge.czt.base.ast.Term>

This class converts ZLive-specific terms into standard Z AST nodes. It is typically called before printing a term. You can use setEvalSetSize to control how many elements are printed when a large or infinite EvalSet is encountered.

Author:

marku

Constructor Summary

Constructors

Constructor and Description
ResultTreeToZVisitor()

Method Summary

Modifier and Type	Method and Description
protected net.sourceforge.czt.z.ast.Expr	etc() Returns a name that represents an unknown number of elements.
static int	getEvalSetSize()
static void	setEvalSetSize(int size) Set the maximum number of set elements that the printer will try to display.
static void	setEvalSetSize(String sizeString) A convenience version of setEvalSetSize that takes a string parameter.
net.sourceforge.czt.base.ast.Term	visitEvalSet(EvalSet evalSet) Visits an EvalSet.
net.sourceforge.czt.base.ast.Term	visitLetExpr(net.sourceforge.czt.z.ast.LetExpr expr) Convert the strange LET expressions that ZLive uses for function/relation spaces back into normal function/relation spaces.
net.sourceforge.czt.base.ast.Term	visitPowerSet(PowerSet powerSet) Visits a PowerSet.
net.sourceforge.czt.base.ast.Term	visitProdSet(ProdSet prodSet) Visits a ProdSet.
net.sourceforge.czt.base.ast.Term	visitRelSet(RelSet relSet) We do not attempt to enumerate function spaces, since this is rarely useful -- they are usually too big, and they are usually used for membership tests.
net.sourceforge.czt.base.ast.Term	visitTerm(net.sourceforge.czt.base.ast.Term term)

Methods inherited from class java.lang.Object

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

Constructor Detail

ResultTreeToZVisitor

public ResultTreeToZVisitor()

Method Detail

getEvalSetSize

public static int getEvalSetSize()

setEvalSetSize

public static void setEvalSetSize(int size)

Set the maximum number of set elements that the printer will try to display. If the set contains more elements that this number, then '...' will be printed for the remaining elements. A value of -1 is interpreted as meaning 'infinite'.

Parameters:

size -

setEvalSetSize

public static void setEvalSetSize(String sizeString)

A convenience version of setEvalSetSize that takes a string parameter.

etc

protected net.sourceforge.czt.z.ast.Expr etc()

Returns a name that represents an unknown number of elements.

visitTerm

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

Specified by:

visitTerm in interface net.sourceforge.czt.base.visitor.TermVisitor<net.sourceforge.czt.base.ast.Term>

visitEvalSet

public net.sourceforge.czt.base.ast.Term visitEvalSet(EvalSet evalSet)

Description copied from interface: EvalSetVisitor

Visits an EvalSet.

Specified by:

visitEvalSet in interface EvalSetVisitor<net.sourceforge.czt.base.ast.Term>

Parameters:

evalSet - the EvalSet to be visited.

Returns:

some kind of Object.

visitPowerSet

public net.sourceforge.czt.base.ast.Term visitPowerSet(PowerSet powerSet)

Description copied from interface: PowerSetVisitor

Visits a PowerSet.

Specified by:

visitPowerSet in interface PowerSetVisitor<net.sourceforge.czt.base.ast.Term>

Parameters:

powerSet - the PowerSet to be visited.

Returns:

some kind of Object.

visitProdSet

public net.sourceforge.czt.base.ast.Term visitProdSet(ProdSet prodSet)

Description copied from interface: ProdSetVisitor

Visits a ProdSet.

Specified by:

visitProdSet in interface ProdSetVisitor<net.sourceforge.czt.base.ast.Term>

Parameters:

prodSet - the ProdSet to be visited.

Returns:

some kind of Object.

visitRelSet

public net.sourceforge.czt.base.ast.Term visitRelSet(RelSet relSet)

We do not attempt to enumerate function spaces, since this is rarely useful -- they are usually too big, and they are usually used for membership tests. Instead, this returns expressions like: domain op range, where op is one of the function space operators.

Specified by:

visitRelSet in interface RelSetVisitor<net.sourceforge.czt.base.ast.Term>

Parameters:

relSet - the RelSet to be visited.

Returns:

some kind of Object.

visitLetExpr

public net.sourceforge.czt.base.ast.Term visitLetExpr(net.sourceforge.czt.z.ast.LetExpr expr)

Convert the strange LET expressions that ZLive uses for function/relation spaces back into normal function/relation spaces. This is useful when we are printing unfolded terms.

Specified by:

visitLetExpr in interface net.sourceforge.czt.z.visitor.LetExprVisitor<net.sourceforge.czt.base.ast.Term>

Parameters:

expr -

Returns: