net.sourceforge.czt.animation.eval

Class FlattenVisitor

java.lang.Object

net.sourceforge.czt.animation.eval.FlattenVisitor

All Implemented Interfaces:

net.sourceforge.czt.base.visitor.TermVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.util.Visitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.AndPredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.ApplExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.BindExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.BindSelExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.CondExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.ExistsPredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.FalsePredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.ForallPredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.IffPredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.ImpliesPredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.LetExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.MemPredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.MuExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.NegPredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.NumExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.OrPredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.PowerExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.ProdExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.RefExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.SchExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.SetCompExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.SetExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.TruePredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.TupleExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.TupleSelExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.ZNameVisitor<net.sourceforge.czt.z.ast.ZName>

public class FlattenVisitor
extends Object
implements net.sourceforge.czt.base.visitor.TermVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.AndPredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.OrPredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.ImpliesPredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.IffPredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.NegPredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.MemPredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.FalsePredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.TruePredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.ExistsPredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.ForallPredVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.NumExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.ApplExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.BindSelExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.TupleSelExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.RefExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.PowerExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.SetExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.SetCompExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.MuExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.ProdExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.TupleExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.BindExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.LetExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.ZNameVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.SchExprVisitor<net.sourceforge.czt.z.ast.ZName>, net.sourceforge.czt.z.visitor.CondExprVisitor<net.sourceforge.czt.z.ast.ZName>

Flattens a Pred/Expr term into a list of FlatPred objects. The visit* methods add subclasses of Pred or Expr into the list flat_. Each visit*Expr method returns a Name, which is the name of the variable that will contain the result of the expression after evaulation. Each visit*Pred method returns null.

The ZLive parameter to the constructor is used to access the section manager (to get the current context of the expr/pred).

TODO: could look for common subexpressions. Eg. keep track of all expressions translated so far in a Map<Expr,ZName>.

Constructor Summary

Constructors

Constructor and Description
FlattenVisitor(ZLive zlive, FlatPredList destination, DefinitionTable defns)

Method Summary

Modifier and Type	Method and Description
protected String	binaryRelation(net.sourceforge.czt.z.ast.Expr e) Extracts the names of known binary relations.
protected net.sourceforge.czt.z.ast.ZName	createBoundName() Creates a fresh ZName and sets it (by default) to be a bound variable of the current FlatPredList.
protected ArrayList<net.sourceforge.czt.z.ast.ZName>	flattenExprList(List<net.sourceforge.czt.z.ast.Expr> elements) An auxiliary method for visiting a list of Expr.
static RelSet	getRelSet(net.sourceforge.czt.z.ast.LetExpr e) Non-null result means this LET encodes a relation/function space.
boolean	isGivenSet(net.sourceforge.czt.z.ast.RefExpr expr) True if expr is a given set.
boolean	isGivenValue(net.sourceforge.czt.z.ast.RefExpr expr) True if expr is a member of a given set.
protected net.sourceforge.czt.z.ast.ZName	notYet(net.sourceforge.czt.base.ast.Term t) Throws a 'not yet implemented' exception.
protected net.sourceforge.czt.z.ast.ZName	notYet(net.sourceforge.czt.base.ast.Term t, String msg) Throws a 'not yet implemented' exception.
net.sourceforge.czt.z.ast.ZName	visitAndPred(net.sourceforge.czt.z.ast.AndPred p) Adds both conjuncts to the flatten list.
net.sourceforge.czt.z.ast.ZName	visitApplExpr(net.sourceforge.czt.z.ast.ApplExpr e) Each ApplExpr is flattened into a different kind of FlatPred.
net.sourceforge.czt.z.ast.ZName	visitBindExpr(net.sourceforge.czt.z.ast.BindExpr e)
net.sourceforge.czt.z.ast.ZName	visitBindSelExpr(net.sourceforge.czt.z.ast.BindSelExpr e)
net.sourceforge.czt.z.ast.ZName	visitCondExpr(net.sourceforge.czt.z.ast.CondExpr cond)
net.sourceforge.czt.z.ast.ZName	visitExistsPred(net.sourceforge.czt.z.ast.ExistsPred p) TODO: see if we can optimize more aggressively here.
net.sourceforge.czt.z.ast.ZName	visitFalsePred(net.sourceforge.czt.z.ast.FalsePred p)
net.sourceforge.czt.z.ast.ZName	visitForallPred(net.sourceforge.czt.z.ast.ForallPred p)
net.sourceforge.czt.z.ast.ZName	visitIffPred(net.sourceforge.czt.z.ast.IffPred p)
net.sourceforge.czt.z.ast.ZName	visitImpliesPred(net.sourceforge.czt.z.ast.ImpliesPred p)
net.sourceforge.czt.z.ast.ZName	visitLetExpr(net.sourceforge.czt.z.ast.LetExpr e) This translates our special LET isFun==1;...
net.sourceforge.czt.z.ast.ZName	visitMemPred(net.sourceforge.czt.z.ast.MemPred p)
net.sourceforge.czt.z.ast.ZName	visitMuExpr(net.sourceforge.czt.z.ast.MuExpr e)
net.sourceforge.czt.z.ast.ZName	visitNegPred(net.sourceforge.czt.z.ast.NegPred p)
net.sourceforge.czt.z.ast.ZName	visitNumExpr(net.sourceforge.czt.z.ast.NumExpr e) NumExpr objects are converted into tmp = Num.
net.sourceforge.czt.z.ast.ZName	visitOrPred(net.sourceforge.czt.z.ast.OrPred p)
net.sourceforge.czt.z.ast.ZName	visitPowerExpr(net.sourceforge.czt.z.ast.PowerExpr e)
net.sourceforge.czt.z.ast.ZName	visitProdExpr(net.sourceforge.czt.z.ast.ProdExpr e)
net.sourceforge.czt.z.ast.ZName	visitRefExpr(net.sourceforge.czt.z.ast.RefExpr e) Simple RefExpr objects are returned unchanged.
net.sourceforge.czt.z.ast.ZName	visitSchExpr(net.sourceforge.czt.z.ast.SchExpr sch) This does [D | P] = \{ D | P @ \theta [D | true] \} because this is currently hard to do in preprocess.tex.
net.sourceforge.czt.z.ast.ZName	visitSetCompExpr(net.sourceforge.czt.z.ast.SetCompExpr e)
net.sourceforge.czt.z.ast.ZName	visitSetExpr(net.sourceforge.czt.z.ast.SetExpr e)
net.sourceforge.czt.z.ast.ZName	visitTerm(net.sourceforge.czt.base.ast.Term term) We throw an error if we reach a kind of term that we do not handle.
net.sourceforge.czt.z.ast.ZName	visitTruePred(net.sourceforge.czt.z.ast.TruePred p)
net.sourceforge.czt.z.ast.ZName	visitTupleExpr(net.sourceforge.czt.z.ast.TupleExpr e)
net.sourceforge.czt.z.ast.ZName	visitTupleSelExpr(net.sourceforge.czt.z.ast.TupleSelExpr e)
net.sourceforge.czt.z.ast.ZName	visitZName(net.sourceforge.czt.z.ast.ZName e) Name objects are returned unchanged, except for \emptyset, which is unfolded into {}.

Methods inherited from class java.lang.Object

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

Constructor Detail

FlattenVisitor

public FlattenVisitor(ZLive zlive,
                      FlatPredList destination,
                      DefinitionTable defns)

Method Detail

isGivenSet

public boolean isGivenSet(net.sourceforge.czt.z.ast.RefExpr expr)

True if expr is a given set. We rely on the type annotations to determine this. But this is not enough, since x:\power CAR will have the same type as CAR. TODO: The best way of identifying given sets would be to scan all the GivenParas and put those names into the definition table. Probably something similar should be done with freetype names.

createBoundName

protected net.sourceforge.czt.z.ast.ZName createBoundName()

Creates a fresh ZName and sets it (by default) to be a bound variable of the current FlatPredList.

Returns:

the fresh ZName

isGivenValue

public boolean isGivenValue(net.sourceforge.czt.z.ast.RefExpr expr)

True if expr is a member of a given set. We rely on the type annotations to determine this. As for isGivenSet, this is not enough, since in \forall x:CAR, we want to leave x as a normal variable, rather than converting it into a GivenValue. TODO: only classify global constants like this. (do this by putting appropriately typed global constants and freetype branches into the definition table, bound to a corresponding GivenValue).

notYet

protected net.sourceforge.czt.z.ast.ZName notYet(net.sourceforge.czt.base.ast.Term t)

Throws a 'not yet implemented' exception.

notYet

protected net.sourceforge.czt.z.ast.ZName notYet(net.sourceforge.czt.base.ast.Term t,
                                                 String msg)

Throws a 'not yet implemented' exception.

binaryRelation

protected String binaryRelation(net.sourceforge.czt.z.ast.Expr e)

Extracts the names of known binary relations.

flattenExprList

protected ArrayList<net.sourceforge.czt.z.ast.ZName> flattenExprList(List<net.sourceforge.czt.z.ast.Expr> elements)

An auxiliary method for visiting a list of Expr.

Parameters:

elements - a list of Expr.

Returns:

an ArrayList of ZNames (same size as elements).

visitTerm

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

We throw an error if we reach a kind of term that we do not handle.

Specified by:

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

visitAndPred

public net.sourceforge.czt.z.ast.ZName visitAndPred(net.sourceforge.czt.z.ast.AndPred p)

Adds both conjuncts to the flatten list.

Specified by:

visitAndPred in interface net.sourceforge.czt.z.visitor.AndPredVisitor<net.sourceforge.czt.z.ast.ZName>

visitOrPred

public net.sourceforge.czt.z.ast.ZName visitOrPred(net.sourceforge.czt.z.ast.OrPred p)

Specified by:

visitOrPred in interface net.sourceforge.czt.z.visitor.OrPredVisitor<net.sourceforge.czt.z.ast.ZName>

visitImpliesPred

public net.sourceforge.czt.z.ast.ZName visitImpliesPred(net.sourceforge.czt.z.ast.ImpliesPred p)

Specified by:

visitImpliesPred in interface net.sourceforge.czt.z.visitor.ImpliesPredVisitor<net.sourceforge.czt.z.ast.ZName>

visitIffPred

public net.sourceforge.czt.z.ast.ZName visitIffPred(net.sourceforge.czt.z.ast.IffPred p)

Specified by:

visitIffPred in interface net.sourceforge.czt.z.visitor.IffPredVisitor<net.sourceforge.czt.z.ast.ZName>

visitNegPred

public net.sourceforge.czt.z.ast.ZName visitNegPred(net.sourceforge.czt.z.ast.NegPred p)

Specified by:

visitNegPred in interface net.sourceforge.czt.z.visitor.NegPredVisitor<net.sourceforge.czt.z.ast.ZName>

visitMemPred

public net.sourceforge.czt.z.ast.ZName visitMemPred(net.sourceforge.czt.z.ast.MemPred p)

Specified by:

visitMemPred in interface net.sourceforge.czt.z.visitor.MemPredVisitor<net.sourceforge.czt.z.ast.ZName>

visitFalsePred

public net.sourceforge.czt.z.ast.ZName visitFalsePred(net.sourceforge.czt.z.ast.FalsePred p)

Specified by:

visitFalsePred in interface net.sourceforge.czt.z.visitor.FalsePredVisitor<net.sourceforge.czt.z.ast.ZName>

visitTruePred

public net.sourceforge.czt.z.ast.ZName visitTruePred(net.sourceforge.czt.z.ast.TruePred p)

Specified by:

visitTruePred in interface net.sourceforge.czt.z.visitor.TruePredVisitor<net.sourceforge.czt.z.ast.ZName>

visitExistsPred

public net.sourceforge.czt.z.ast.ZName visitExistsPred(net.sourceforge.czt.z.ast.ExistsPred p)

TODO: see if we can optimize more aggressively here. Eg. by using (exists D @ P) <=> (exists D | P @ true)? And by calling addExistsPred, rather than addPred, so that nested exists are flattened out.

Specified by:

visitExistsPred in interface net.sourceforge.czt.z.visitor.ExistsPredVisitor<net.sourceforge.czt.z.ast.ZName>

visitForallPred

public net.sourceforge.czt.z.ast.ZName visitForallPred(net.sourceforge.czt.z.ast.ForallPred p)

Specified by:

visitForallPred in interface net.sourceforge.czt.z.visitor.ForallPredVisitor<net.sourceforge.czt.z.ast.ZName>

visitZName

public net.sourceforge.czt.z.ast.ZName visitZName(net.sourceforge.czt.z.ast.ZName e)

Name objects are returned unchanged, except for \emptyset, which is unfolded into {}.

Specified by:

visitZName in interface net.sourceforge.czt.z.visitor.ZNameVisitor<net.sourceforge.czt.z.ast.ZName>

visitRefExpr

public net.sourceforge.czt.z.ast.ZName visitRefExpr(net.sourceforge.czt.z.ast.RefExpr e)

Simple RefExpr objects are returned unchanged. We try to unfold non-generic definitions of names. We replace \nat and \num by FlatRangeSet. Arithmos is also mapped into FlatRangeSet (integers), which means ZLive handles integers only for now. TODO: implement arithmos differently so that ZLive can eventually support non-integer numbers, such as real numbers.

Specified by:

visitRefExpr in interface net.sourceforge.czt.z.visitor.RefExprVisitor<net.sourceforge.czt.z.ast.ZName>

visitNumExpr

public net.sourceforge.czt.z.ast.ZName visitNumExpr(net.sourceforge.czt.z.ast.NumExpr e)

NumExpr objects are converted into tmp = Num.

Specified by:

visitNumExpr in interface net.sourceforge.czt.z.visitor.NumExprVisitor<net.sourceforge.czt.z.ast.ZName>

visitApplExpr

public net.sourceforge.czt.z.ast.ZName visitApplExpr(net.sourceforge.czt.z.ast.ApplExpr e)

Each ApplExpr is flattened into a different kind of FlatPred.

Specified by:

visitApplExpr in interface net.sourceforge.czt.z.visitor.ApplExprVisitor<net.sourceforge.czt.z.ast.ZName>

visitBindSelExpr

public net.sourceforge.czt.z.ast.ZName visitBindSelExpr(net.sourceforge.czt.z.ast.BindSelExpr e)

Specified by:

visitBindSelExpr in interface net.sourceforge.czt.z.visitor.BindSelExprVisitor<net.sourceforge.czt.z.ast.ZName>

visitTupleSelExpr

public net.sourceforge.czt.z.ast.ZName visitTupleSelExpr(net.sourceforge.czt.z.ast.TupleSelExpr e)

Specified by:

visitTupleSelExpr in interface net.sourceforge.czt.z.visitor.TupleSelExprVisitor<net.sourceforge.czt.z.ast.ZName>

visitPowerExpr

public net.sourceforge.czt.z.ast.ZName visitPowerExpr(net.sourceforge.czt.z.ast.PowerExpr e)

Specified by:

visitPowerExpr in interface net.sourceforge.czt.z.visitor.PowerExprVisitor<net.sourceforge.czt.z.ast.ZName>

visitSetExpr

public net.sourceforge.czt.z.ast.ZName visitSetExpr(net.sourceforge.czt.z.ast.SetExpr e)

Specified by:

visitSetExpr in interface net.sourceforge.czt.z.visitor.SetExprVisitor<net.sourceforge.czt.z.ast.ZName>

visitSetCompExpr

public net.sourceforge.czt.z.ast.ZName visitSetCompExpr(net.sourceforge.czt.z.ast.SetCompExpr e)

Specified by:

visitSetCompExpr in interface net.sourceforge.czt.z.visitor.SetCompExprVisitor<net.sourceforge.czt.z.ast.ZName>

visitMuExpr

public net.sourceforge.czt.z.ast.ZName visitMuExpr(net.sourceforge.czt.z.ast.MuExpr e)

Specified by:

visitMuExpr in interface net.sourceforge.czt.z.visitor.MuExprVisitor<net.sourceforge.czt.z.ast.ZName>

visitProdExpr

public net.sourceforge.czt.z.ast.ZName visitProdExpr(net.sourceforge.czt.z.ast.ProdExpr e)

Specified by:

visitProdExpr in interface net.sourceforge.czt.z.visitor.ProdExprVisitor<net.sourceforge.czt.z.ast.ZName>

visitTupleExpr

public net.sourceforge.czt.z.ast.ZName visitTupleExpr(net.sourceforge.czt.z.ast.TupleExpr e)

Specified by:

visitTupleExpr in interface net.sourceforge.czt.z.visitor.TupleExprVisitor<net.sourceforge.czt.z.ast.ZName>

visitBindExpr

public net.sourceforge.czt.z.ast.ZName visitBindExpr(net.sourceforge.czt.z.ast.BindExpr e)

Specified by:

visitBindExpr in interface net.sourceforge.czt.z.visitor.BindExprVisitor<net.sourceforge.czt.z.ast.ZName>

getRelSet

public static RelSet getRelSet(net.sourceforge.czt.z.ast.LetExpr e)

Non-null result means this LET encodes a relation/function space.

visitLetExpr

public net.sourceforge.czt.z.ast.ZName visitLetExpr(net.sourceforge.czt.z.ast.LetExpr e)

This translates our special LET isFun==1;... @ A x B constructs into FlatRelSet objects that represent function spaces.

Specified by:

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

visitSchExpr

public net.sourceforge.czt.z.ast.ZName visitSchExpr(net.sourceforge.czt.z.ast.SchExpr sch)

This does [D | P] = \{ D | P @ \theta [D | true] \} because this is currently hard to do in preprocess.tex.

Specified by:

visitSchExpr in interface net.sourceforge.czt.z.visitor.SchExprVisitor<net.sourceforge.czt.z.ast.ZName>

Parameters:

zedObject -

Returns:

visitCondExpr

public net.sourceforge.czt.z.ast.ZName visitCondExpr(net.sourceforge.czt.z.ast.CondExpr cond)

Specified by:

visitCondExpr in interface net.sourceforge.czt.z.visitor.CondExprVisitor<net.sourceforge.czt.z.ast.ZName>