public class ZPredTransformer extends AbstractPredTransformer
factory_, termVisitor_| Constructor and Description |
|---|
ZPredTransformer(Factory factory,
net.sourceforge.czt.util.Visitor<Pred> termV) |
| 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]
|
andPred, andPredList, checkNeg, existsPred, existsPred, falsePred, forAllPred, forAllPred, impliesPred, orPred, truePredgetFactory, getTermVisitor, isApplyingTransformer, setApplyTransformer, visitprotected Pred getZSchTextPred(ZSchText schText)
schText - public Expr predAsSchExpr(Pred pred)
pred - public AxPara createSchExpr(List<? extends Name> formals, Name schName, ZSchText zSchText)
formals - genFormals - schName - zSchText - public boolean isOnlyConstDecl(ZDeclList decls)
decls - Copyright © 2003–2016 Community Z Tools Project. All rights reserved.