net.sourceforge.czt.vcg.z.transformer

Class ZPredTransformer

java.lang.Object

net.sourceforge.czt.vcg.z.transformer.AbstractTermTransformer<Pred>

net.sourceforge.czt.vcg.z.transformer.AbstractPredTransformer

net.sourceforge.czt.vcg.z.transformer.ZPredTransformer

All Implemented Interfaces:

TermTransformer<Pred>

Direct Known Subclasses:

ZPredTransformerDC, ZPredTransformerFSB

public class ZPredTransformer
extends AbstractPredTransformer

Z-Centric predicate transformers and auxiliary methods.

Author:

Leo Freitas

Field Summary

Fields inherited from class net.sourceforge.czt.vcg.z.transformer.AbstractTermTransformer

factory_, termVisitor_

Constructor Summary

Constructors

Constructor and Description
ZPredTransformer(Factory factory, net.sourceforge.czt.util.Visitor<Pred> termV)

Method Summary

Modifier and Type	Method and Description
AxPara	createSchExpr(List<? extends Name> formals, Name schName, ZSchText zSchText) For a zSchText (D | P) creates an \begin{schema}{schName}[genFormals] D \where P \end{schema}
protected Pred	getZSchTextPred(ZSchText schText) Extract schema text predicates.
boolean	isOnlyConstDecl(ZDeclList decls) Checks whether the list of declarations are ConstDecl only.
Expr	predAsSchExpr(Pred pred) Transforms a predicate into a (Sch)Expr (with empty Decl): P --> [ |P]

Methods inherited from class net.sourceforge.czt.vcg.z.transformer.AbstractPredTransformer

andPred, andPredList, checkNeg, existsPred, existsPred, falsePred, forAllPred, forAllPred, impliesPred, orPred, truePred

Methods inherited from class net.sourceforge.czt.vcg.z.transformer.AbstractTermTransformer

getFactory, getTermVisitor, isApplyingTransformer, setApplyTransformer, visit

Methods inherited from class java.lang.Object

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

Constructor Detail

ZPredTransformer

public ZPredTransformer(Factory factory,
                        net.sourceforge.czt.util.Visitor<Pred> termV)

Method Detail

getZSchTextPred

protected Pred getZSchTextPred(ZSchText schText)

Extract schema text predicates. When null (see Z Std syntactic transformations for when that is the case), just returns true.

Parameters:

schText -

Returns:

predAsSchExpr

public Expr predAsSchExpr(Pred pred)

Transforms a predicate into a (Sch)Expr (with empty Decl): P --> [ |P]

Parameters:

pred -

Returns:

createSchExpr

public AxPara createSchExpr(List<? extends Name> formals,
                            Name schName,
                            ZSchText zSchText)

For a zSchText (D | P) creates an \begin{schema}{schName}[genFormals] D \where P \end{schema}

Parameters:

formals -

genFormals -

schName -

zSchText -

Returns:

isOnlyConstDecl

public boolean isOnlyConstDecl(ZDeclList decls)

Checks whether the list of declarations are ConstDecl only. This is important while checking for LetExpr, and BindExpr (syntactic/parsing) consistency.

Parameters:

decls -

Returns: