ZUtils (CZT Corejava Z 1.6-SNAPSHOT API)

java.lang.Object
- net.sourceforge.czt.z.util.ZUtils

public final class ZUtils
extends Object

Nested Class Summary

Nested Classes
Modifier and Type Class and Description

static class ZUtils.ZExprKind
Enumerated type used to distinguish what kind of Z Expr is.

Nested Classes
Modifier and Type	Class and Description
`static class`	`ZUtils.ZExprKind` Enumerated type used to distinguish what kind of Z Expr is.

Field Summary

Fields
Modifier and Type	Field and Description
`static Factory`	`FACTORY`
`static StandardZ`	`STDZ_NAMELIST_CHECKER`
`static Comparator<ZName>`	`ZNAME_COMPARATOR`
`static Comparator<ZName>`	`ZNAME_IGNORE_STROKES_COMPARATOR`

Method Summary

All Methods Static Methods Concrete Methods
Modifier and Type	Method and Description
`static int`	`applExprArity(ApplExpr term)`
`static ZBranchList`	`assertZBranchList(Term term)`
`static ZDeclList`	`assertZDeclList(Term term)`
`static ZExprList`	`assertZExprList(Term term)`
`static ZFactoryImpl`	`assertZFactoryImpl(Object factory)`
`static ZFreetypeList`	`assertZFreetypeList(Term term)`
`static ZName`	`assertZName(Term term)`
`static ZNameList`	`assertZNameList(Term term)`
`static ZNumeral`	`assertZNumeral(Term term)`
`static ZParaList`	`assertZParaList(Term term)`
`static PrintVisitor`	`assertZPrintVisitor(Object visitor)`
`static ZSchText`	`assertZSchText(Term term)`
`static ZStrokeList`	`assertZStrokeList(Term term)`
`static TermImpl`	`assertZTermImpl(Object term)`
`static Name`	`buildName(Factory factory, Name name, List<Stroke> strokes)`
`static Name`	`buildName(Name name, List<Stroke> strokes)`
`static <T extends Term> T`	`cloneTerm(T term)` Cloning terms
`static int`	`compareTo(ZName zName1, ZName zName2)`
`static int`	`compareToIgnoreStrokes(ZName zName1, ZName zName2)`
`static boolean`	`containsID(List<ZName> list, ZName zName)` Test whether a list contains a ZName with the same ID.
`static boolean`	`containsObject(List<Term> list, Object o)` Test whether a list contains a reference to an object.
`static boolean`	`containsZName(List<ZName> list, ZName zName)` Test whether a list contains a ZName.
`static Factory`	`createConsoleFactory()` Useful factory for debugging purposes.
`static Factory`	`createFactory(boolean printUnicode, boolean printNameIds, int printLocLineOffset, int printLocColOffset)` Create a factory tailored for either debugging or UI purposes.
`static Expr`	`getAbbreviationExpr(Term term)`
`static Name`	`getAbbreviationName(Term term)`
`static ZNameList`	`getAbbreviationZGenFormals(Term term)`
`static ZExprList`	`getApplExprArguments(Term term)` Returns the ApplExpr arguments for the given term if it is a valid ApplExpr (i.e.
`static Expr`	`getApplExprRef(Term term)` Returns the ApplExpr reference expression for the given term if it is a valid ApplExpr (i.e.
`static ZDeclList`	`getAxBoxDecls(Term term)` Returns the ZDeclList of axiomatic or generic definitions, or null if term is not an AxPara with AxBox.
`static Pred`	`getAxBoxPred(Term term)` Returns the Pred of axiomatic or generic definitions, or null if term is not an AxPara with AxBox.
`static NameList`	`getAxParaGenFormals(Term term)` Returns the generic formals as NameList of a given term if it is AxPara or null otherwise.
`static Name`	`getAxParaSchOrAbbrName(Term term)`
`static ZNameList`	`getAxParaZGenFormals(Term term)` Returns the generic formals as ZNameList of a given term if it is AxPara or null otherwise This is valid for any kind of AxPara.
`static ZExprList`	`getGenOpApplZGenActuals(Term term)` Returns the list of instantiating expressions in Generic Operator Application RefExpr or null if it isn't one.
`static Expr`	`getMemPredLHS(MemPred term)` Returns the LHS of a MemPred, which is just the same as term.getLeftExpr()
`static Expr`	`getMemPredRHS(MemPred term)` Returns the RHS of a MemPred, which is just the same as term.getReftExpr(), unless term is an equality, in which case it returns the singleton set element of the RHS expression.
`static int`	`getRelOpApplPredArity(Term term)` Returns the relational operator application aritity (i.e.
`static ZExprList`	`getRelOpApplPredLHSArguments(Term term)` Returns the relational operator application arguments, or null if term is not a MemPred relational operator application (i.e.
`static RefExpr`	`getRelOpName(Term term)` Returns the relational operator name for the given term if it is a relational operator MemPred (i.e.
`static Expr`	`getSchemaDefExpr(Term term)`
`static Name`	`getSchemaName(Term term)` If the given paragraph `isSimpleSchema(para)`, returns the declared schema name.
`static ZNameList`	`getSchemaZGenFormals(Term term)`
`static ZName`	`getSpecialSchemaBaseName(Factory factory, ZName zName)` Get the base name of a delta or xi reference.
`static ZName`	`getSpecialSchemaBaseName(ZName zName)`
`static int`	`getStrokeValue(Stroke stroke)`
`static boolean`	`idsEqual(String id1, String id2)`
`static void`	`insert(List<NameTypePair> pairsA, List<NameTypePair> pairsB)` Inserts all elements from pairsB in pairsA, provided pairsA are sorted.
`static void`	`insert(List<NameTypePair> pairs, NameTypePair pair)`
`static void`	`insertNames(List<ZName> namesA, List<ZName> namesB)` Inserts all elements from namesB in namesA, provided namesA are sorted.
`static void`	`insertNames(List<ZName> names, ZName name)`
`static boolean`	`isAbbreviation(Term term)` Checks whether the given term `isHorizontalDef(Term)` and `!isSimpleSchema(Term)`
`static boolean`	`isAndPred(Term term)`
`static boolean`	`isAnonymous(ZSect zSect)`
`static boolean`	`isApplExpr(Term term)`
`static boolean`	`isApplicationExpr(Term term)` Returns true if term is an application expression.
`static boolean`	`isApplicationExprValid(ApplExpr term)` Returns true whenever the given ApplExpr is valid (i.e.
`static boolean`	`isAxPara(Term term)` Checks whether the given term is an AxPara
`static boolean`	`isAxParaSchemaOrHorizDefValid(AxPara axp)` Returns true if the AxPara has been properly encoded as either a schema box or a horizontal definition.
`static boolean`	`isBindSelExpr(Term term)`
`static boolean`	`isBoxedAxiomaticDef(Term term)` Return the generic formals of a given term if it is AxPara or null otherwise
`static boolean`	`isBoxedGenericDef(Term term)` Checks whether the given term is an AxPara with AxBox (i.e.
`static boolean`	`isChainedConjunction(Term term)` Returns true if given term is an AndPred with And.Chain
`static boolean`	`isDelta(ZName zName)`
`static boolean`	`isDeltaXi(Name name)`
`static boolean`	`isDeltaXi(ZName zName)`
`static boolean`	`isEmptySetRefExpr(Object a)` Returns whether the given expression is an empty set as a reference to `ZString.EMPTYSET.`
`static boolean`	`isEqualityPred(Term term)` Returns true if term is MemPred with Mixfix=true and the second (right) expression is a singleton set containing the right-hand side of the equality.
`static boolean`	`isExplicitGenInstExpr(Term term)` Another less common example would be (\_ \fun \_)[S, T].
`static boolean`	`isFcnOpApplExpr(Term term)` Returns true if term is an function operator application expression.
`static boolean`	`isGenInstExpr(Term term)` Returns true if term is a generic operator instantiation.
`static boolean`	`isGenOpApplExpr(Term term)` Returns true if term is Generic Operator Application.
`static boolean`	`isHorizontalDef(Term term)` Checks whether the given term is an AxPara with OmixBox.
`static boolean`	`isHorizontalSchema(Term term)` Checks whether the given term `isHorizontalDef(Term)` and `isSimpleSchema(Term)`
`static boolean`	`isLambdaExpr(Term term)`
`static boolean`	`isMembershipPred(Term term)` Returns true if term is MemPred with Mixfix=false, where the first (left) expression is the element, and the second (right) expression is the set.
`static boolean`	`isMemPred(Term term)`
`static boolean`	`isMemPredValid(MemPred term)` Returns true whenever the given MemPred is valid (i.e.
`static boolean`	`isNestedApplExpr(Term term)` Nested application expressions (e.g., (f~x)~y) are ApplExpr with mixfix FALSE and left expr as an ApplExpr.
`static boolean`	`isReferenceExpr(Term term)` Returns true if term is a reference expression.
`static boolean`	`isRefExpr(Term term)`
`static boolean`	`isRefExprValid(RefExpr term)` Returns true whenever the given RefExpr is valid (i.e.
`static boolean`	`isRelOpApplPred(Term term)` Returns true if term is MemPred with Mixfix=true, and the second (right) expression is the operator name.
`static boolean`	`isSetExpr(Term term)`
`static boolean`	`isSimpleSchema(Term term)` Checks whether the given paragraph is an `AxPara` term encoded as a schema or not.
`static boolean`	`isTupleExpr(Term term)`
`static boolean`	`isTupleSelExpr(Term term)`
`static boolean`	`isXi(ZName zName)`
`static boolean`	`isZPara(Term term)` Returns true if the given term is either a boxed or unboxed Z paragraph.
`static boolean`	`namesEqual(Name name1, Name name2)` Test whether the base name and strokes of two Names are equal.
`static boolean`	`namesEqual(ZName zName1, ZName zName2)` Test whether the base name and strokes of two ZNames are equal.
`static Set<String>`	`parentsArgListAsSetOfString(String... p)` Given a var-arg list of strings, transforms it into a set of strings (i.e.
`static List<Parent>`	`parentsAsListOfParent(Set<String> parents)` Transforms the set of string parents into list of AST Parents
`static Set<Parent>`	`parentsAsSetOfParent(Set<String> parents)` Transforms the set of string parents into set of AST Parents
`static String`	`parentsAsString(Set<String> parents)` Given a set of parent sections return it as a CSV string.
`static Set<String>`	`parentsCSVAsSetOfString(String p)` Gets a CSV string of Z section parents and transforms it back to a set of string Should satisfy the invariant akin parentsAsString(parentsCSVAsSetOfString(s)) = s (ignoring order).
`static ZSect`	`retrieveZSect(Spec term, String sectName)`
`static void`	`setToStringVisitor(Term term, PrintVisitor printer)`
`protected static void`	`setZFactoryToStringVisitor(Factory f, Visitor<String> toStringVisitor)` ; Changes the toString() method of ZFactory (within the given Factory), so that is uses the toString() strategy for the given visitor, usually one kind of PrintVisitor.
`static List<NameTypePair>`	`sort(List<NameTypePair> pairs)` Sorts the list of name type pairs given.
`static Signature`	`sort(Signature signature)` Sorts the name type pairs within the given signature.
`static List<ZName>`	`sortNames(List<ZName> names)`
`static String`	`strokeListToString(List<Stroke> strokes)` Transforms a list of strokes into a (unicode) string.
`static List<NameTypePair>`	`subsignature(Signature sig, Class<?> decor)` Computes a list of all the NameTypePairs from the given signature whose name ends with the given decoration.
`static String`	`toStringZName(ZName name)`
`static String`	`toStringZName(ZName name, boolean printUnicode, boolean printIds)`
`static String`	`trimNLCharAware(String string)` Trims the given string considering Z NLCHAR before and after.
`static void`	`unicodeToAscii(String name, StringBuffer result)`
`static ZUtils.ZExprKind`	`whatKindOfZExpr(Expr term)` Returns whether or not a given expression is part of schema calculus

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Field Detail
  - FACTORY
```
public static final Factory FACTORY
```
  - ZNAME_COMPARATOR
```
public static final Comparator<ZName> ZNAME_COMPARATOR
```
  - ZNAME_IGNORE_STROKES_COMPARATOR
```
public static final Comparator<ZName> ZNAME_IGNORE_STROKES_COMPARATOR
```
  - STDZ_NAMELIST_CHECKER
```
public static final StandardZ STDZ_NAMELIST_CHECKER
```
- Method Detail
  - createConsoleFactory
```
public static Factory createConsoleFactory()
```
    Useful factory for debugging purposes. It prints ASCII names and LocAnn offset by one in line/col count and no name IDs.
    
    Returns:
  - createFactory
```
public static Factory createFactory(boolean printUnicode,
                                    boolean printNameIds,
                                    int printLocLineOffset,
                                    int printLocColOffset)
```
    Create a factory tailored for either debugging or UI purposes. Various parameters affect the base factory underlying print visitor's parameters.
    
    Parameters:
    
    printUnicode -
    
    printNameIds -
    
    printLocLineOffset -
    
    printLocColOffset -
    
    Returns:
  - setToStringVisitor
```
public static void setToStringVisitor(Term term,
                                      PrintVisitor printer)
```
  - subsignature
```
public static List<NameTypePair> subsignature(Signature sig,
                                              Class<?> decor)
```
    Computes a list of all the NameTypePairs from the given signature whose name ends with the given decoration. If decor is null a list of all undecored names with its corresponding types is returned.
  - isAnonymous
```
public static boolean isAnonymous(ZSect zSect)
```
  - parentsAsString
```
public static String parentsAsString(Set<String> parents)
```
    Given a set of parent sections return it as a CSV string. Should satisfy the invariant akin to parentsAsString(parentsCSVAsSetOfString(s)) = s (ignoring order)
    
    Parameters:
    
    parents -
    
    Returns:
  - trimNLCharAware
```
public static String trimNLCharAware(String string)
```
    Trims the given string considering Z NLCHAR before and after. i.e. removes spaces and newlines before and after.
    
    Parameters:
    
    string -
    
    Returns:
  - parentsCSVAsSetOfString
```
public static Set<String> parentsCSVAsSetOfString(String p)
```
    Gets a CSV string of Z section parents and transforms it back to a set of string Should satisfy the invariant akin parentsAsString(parentsCSVAsSetOfString(s)) = s (ignoring order).
    
    Parameters:
    
    p -
    
    Returns:
  - parentsAsSetOfParent
```
public static Set<Parent> parentsAsSetOfParent(Set<String> parents)
```
    Transforms the set of string parents into set of AST Parents
    
    Parameters:
    
    parents -
    
    Returns:
  - parentsAsListOfParent
```
public static List<Parent> parentsAsListOfParent(Set<String> parents)
```
    Transforms the set of string parents into list of AST Parents
    
    Parameters:
    
    parents -
    
    Returns:
  - parentsArgListAsSetOfString
```
public static Set<String> parentsArgListAsSetOfString(String... p)
```
    Given a var-arg list of strings, transforms it into a set of strings (i.e. removes duplicates).
    
    Parameters:
    
    parents -
    
    Returns:
  - isZPara
```
public static boolean isZPara(Term term)
```
    Returns true if the given term is either a boxed or unboxed Z paragraph. That is, a given set, a free type, an axiomatic/generic description, a schema, a horizontal definition, a conjecture, or an operator template.
  - whatKindOfZExpr
```
public static ZUtils.ZExprKind whatKindOfZExpr(Expr term)
```
    Returns whether or not a given expression is part of schema calculus
    
    Parameters:
    
    expr -
    
    Returns:
  - isAxPara
```
public static boolean isAxPara(Term term)
```
    Checks whether the given term is an AxPara
  - getAxParaGenFormals
```
public static NameList getAxParaGenFormals(Term term)
```
    Returns the generic formals as NameList of a given term if it is AxPara or null otherwise. This is valid for any kind of AxPara. That is, it returns the generic parameters for generic boxes, horizontal definitions, and schemas.
  - getAxParaZGenFormals
```
public static ZNameList getAxParaZGenFormals(Term term)
```
    Returns the generic formals as ZNameList of a given term if it is AxPara or null otherwise This is valid for any kind of AxPara. That is, it returns the generic parameters for generic boxes, horizontal definitions, and schemas.
  - getAxBoxDecls
```
public static ZDeclList getAxBoxDecls(Term term)
```
    Returns the ZDeclList of axiomatic or generic definitions, or null if term is not an AxPara with AxBox.
  - getAxBoxPred
```
public static Pred getAxBoxPred(Term term)
```
    Returns the Pred of axiomatic or generic definitions, or null if term is not an AxPara with AxBox.
  - isBoxedAxiomaticDef
```
public static boolean isBoxedAxiomaticDef(Term term)
```
    Return the generic formals of a given term if it is AxPara or null otherwise
  - isBoxedGenericDef
```
public static boolean isBoxedGenericDef(Term term)
```
    Checks whether the given term is an AxPara with AxBox (i.e. it comes from a \begin{gendef}[...]/GENAX
  - isHorizontalDef
```
public static boolean isHorizontalDef(Term term)
```
    Checks whether the given term is an AxPara with OmixBox.
  - isHorizontalSchema
```
public static boolean isHorizontalSchema(Term term)
```
    Checks whether the given term isHorizontalDef(Term) and isSimpleSchema(Term)
  - isAbbreviation
```
public static boolean isAbbreviation(Term term)
```
    Checks whether the given term isHorizontalDef(Term) and !isSimpleSchema(Term)
  - isAxParaSchemaOrHorizDefValid
```
public static boolean isAxParaSchemaOrHorizDefValid(AxPara axp)
```
    Returns true if the AxPara has been properly encoded as either a schema box or a horizontal definition. It is useful for assertions.
  - isSimpleSchema
```
public static boolean isSimpleSchema(Term term)
```
    Checks whether the given paragraph is an AxPara term encoded as a schema or not. That is, it checks whether the term is properly encoded as either a horizontal or a boxed schema. Note that this does not include schema calculus constructs like R == S \land T on schemas S and T, but just SchExpr (usual) schemas. For the latter we need to rely on typing information.
  - isDeltaXi
```
public static boolean isDeltaXi(Name name)
```
  - isDeltaXi
```
public static boolean isDeltaXi(ZName zName)
```
  - isXi
```
public static boolean isXi(ZName zName)
```
  - isDelta
```
public static boolean isDelta(ZName zName)
```
  - cloneTerm
```
public static <T extends Term> T cloneTerm(T term)
```
    Cloning terms
    
    Type Parameters:
    
    T -
    
    Parameters:
    
    term -
    
    Returns:
  - containsObject
```
public static boolean containsObject(List<Term> list,
                                     Object o)
```
    Test whether a list contains a reference to an object.
    
    Parameters:
    
    list - the list to search.
    
    o - the reference to search for.
    
    Returns:
    
    true if and only if the reference is in the list.
  - getSpecialSchemaBaseName
```
public static ZName getSpecialSchemaBaseName(Factory factory,
                                             ZName zName)
```
    Get the base name of a delta or xi reference.
  - getSpecialSchemaBaseName
```
public static ZName getSpecialSchemaBaseName(ZName zName)
```
  - buildName
```
public static Name buildName(Factory factory,
                             Name name,
                             List<Stroke> strokes)
```
  - buildName
```
public static Name buildName(Name name,
                             List<Stroke> strokes)
```
  - getSchemaName
```
public static Name getSchemaName(Term term)
```
    If the given paragraph isSimpleSchema(para), returns the declared schema name. Otherwise, the method returns null.
  - getSchemaDefExpr
```
public static Expr getSchemaDefExpr(Term term)
```
  - getSchemaZGenFormals
```
public static ZNameList getSchemaZGenFormals(Term term)
```
  - getAxParaSchOrAbbrName
```
public static Name getAxParaSchOrAbbrName(Term term)
```
  - getAbbreviationName
```
public static Name getAbbreviationName(Term term)
```
  - getAbbreviationExpr
```
public static Expr getAbbreviationExpr(Term term)
```
  - getAbbreviationZGenFormals
```
public static ZNameList getAbbreviationZGenFormals(Term term)
```
  - isEmptySetRefExpr
```
public static boolean isEmptySetRefExpr(Object a)
```
    Returns whether the given expression is an empty set as a reference to ZString.EMPTYSET.
  isRefExpr public static boolean isRefExpr(Term term) isApplExpr public static boolean isApplExpr(Term term) isSetExpr public static boolean isSetExpr(Term term) isTupleExpr public static boolean isTupleExpr(Term term) isBindSelExpr public static boolean isBindSelExpr(Term term) isTupleSelExpr public static boolean isTupleSelExpr(Term term) isLambdaExpr public static boolean isLambdaExpr(Term term) isMemPred public static boolean isMemPred(Term term) isAndPred public static boolean isAndPred(Term term) isReferenceExpr public static boolean isReferenceExpr(Term term) Returns true if term is a reference expression. That is, a RefExpr with mixfix and explicit false, and the list of instantiating expressions is empty. For example: \arithmos, \num, \emptyset. For \emptyset, the typechecker transforms it to a generic application and explicit remains false (see 13.2.3.3) (i.e. isReferenceExpr(\emptyset) after typechecking might be false if generic actuals are given, as in \emptyset[\nat]). isGenInstExpr public static boolean isGenInstExpr(Term term) Returns true if term is a generic operator instantiation. That is, a RefExpr with mixfix false and the list of instantiating expressions is non-empty (it contains [T]). The explicit attribute indicates whether the instantiating expressions are explicitly given in the specification (explicit is true) or whether they were inferred by the typechecker (explicit is false). For example: \emptyset[T] or \emptyset. isExplicitGenInstExpr public static boolean isExplicitGenInstExpr(Term term) Another less common example would be (\_ \fun \_)[S, T]. In this case, RefExpr(ZName("_->_"), ZExprList( RefExpr(ZName("S"), MF=F, EX=F), RefExpr(ZName("T"), MF=F, EX=F)), MF=F, EX=T) isGenOpApplExpr public static boolean isGenOpApplExpr(Term term) Returns true if term is Generic Operator Application. That is, a RefExpr with mixfix and explicit true, and the list of instantiating expressions is non-empty (it contains [S,T]). For example: S \fun T. isRefExprValid public static boolean isRefExprValid(RefExpr term) Returns true whenever the given RefExpr is valid (i.e. either Reference, Generic Operator application, or Generic Instantiation). It should never be false for expressions created by the parser. This is useful for assertion whenever RefExpr are created on-the-fly. getGenOpApplZGenActuals public static ZExprList getGenOpApplZGenActuals(Term term) Returns the list of instantiating expressions in Generic Operator Application RefExpr or null if it isn't one. That is, it returns [S,T] from "S \fun T". Not that it will return null if term is "(\_ \fun \_)[S, T]" isFcnOpApplExpr public static boolean isFcnOpApplExpr(Term term) Returns true if term is an function operator application expression. That is, a ApplExpr term with mixfix TRUE, and the first (left) expression as the name (e.g. " _ + _ ") (a RefExpr) with mixfix FALSE, and the second (right) expression as the parameters (e.g., TupleExpr (S,T)). For example: "(S + T)". There is no case of ApplExpr where RefExpr mixfix is true. For instance, both "A (\_ \fun\_)[S, T] B" and "(\_ \fun\_)[S, T] (A, B)" parse with ApplExpr true/false but RefExpr mixfix false in both cases. isApplicationExpr public static boolean isApplicationExpr(Term term) Returns true if term is an application expression. That is, a ApplExpr term with mixfix FALSE, the first (left) expression is the function name (e.g., \dom), (a RefExpr with mixfix FALSE) and the second (right) expression is the argument. For example: \dom~R or \id~R. Note that this also covers the case where function operator application is given explicitly, as in "(_+_)(S,T)". Finally, the LEFT expr could also be part of a nested ApplExpr itself (e.g., (f~x)~y). isNestedApplExpr public static boolean isNestedApplExpr(Term term) Nested application expressions (e.g., (f~x)~y) are ApplExpr with mixfix FALSE and left expr as an ApplExpr. Parameters: term - Returns: isApplicationExprValid public static boolean isApplicationExprValid(ApplExpr term) Returns true whenever the given ApplExpr is valid (i.e. either function operator application ---implicitly or explicitly---, or application). It should never be false for expressions created by the parser. This is useful for assertion whenever ApplExpr are created on-the-fly. getApplExprRef public static Expr getApplExprRef(Term term) Returns the ApplExpr reference expression for the given term if it is a valid ApplExpr (i.e. isApplicationExprValid), or null otherwise. The reference is the first (left) expression of the ApplExpr as either a RefExpr or a nested ApplExpr. getApplExprArguments public static ZExprList getApplExprArguments(Term term) Returns the ApplExpr arguments for the given term if it is a valid ApplExpr (i.e. isApplicationExprValid), or null otherwise. The arguments are the second (right) expression of the ApplExpr as a ZExprList. If there are more than one argument (i.e. ApplExpr with TupleExpr as right expr) the list is greater then one. applExprArity public static int applExprArity(ApplExpr term) isEqualityPred public static boolean isEqualityPred(Term term) Returns true if term is MemPred with Mixfix=true and the second (right) expression is a singleton set containing the right-hand side of the equality. For example: "n = m" has left="n" and right="{m}". isRelOpApplPred public static boolean isRelOpApplPred(Term term) Returns true if term is MemPred with Mixfix=true, and the second (right) expression is the operator name. For example, "n < m" has left="(n,m)" and right=" _ < _ ", "disjoint s" has left="s" and right="disjoint _ ", and if foo was declared as a unary postfix operator, then "(2,3) foo" would have left= "(2,3)" and right=" _ foo". isMembershipPred public static boolean isMembershipPred(Term term) Returns true if term is MemPred with Mixfix=false, where the first (left) expression is the element, and the second (right) expression is the set. For example, "n \in S" has left="n" and right="S". Note that this accounts for explicit relational operator application, as in (0, 1) \in (\_ < \_) isMemPredValid public static boolean isMemPredValid(MemPred term) Returns true whenever the given MemPred is valid (i.e. either equality, set membership, or relational operator application). It should never be false for expressions created by the parser. This is useful for assertion whenever MemPred are created on-the-fly. getMemPredLHS public static Expr getMemPredLHS(MemPred term) Returns the LHS of a MemPred, which is just the same as term.getLeftExpr() getMemPredRHS public static Expr getMemPredRHS(MemPred term) Returns the RHS of a MemPred, which is just the same as term.getReftExpr(), unless term is an equality, in which case it returns the singleton set element of the RHS expression. * For example: "n = m" has left="n" and right="{m}", yet getMemPredRHS="m"! getRelOpName public static RefExpr getRelOpName(Term term) Returns the relational operator name for the given term if it is a relational operator MemPred (i.e. isRelOpApplPred), or null otherwise. The name is the second (right) expression of the MemPred term returned as a RefExpr. getRelOpApplPredLHSArguments public static ZExprList getRelOpApplPredLHSArguments(Term term) Returns the relational operator application arguments, or null if term is not a MemPred relational operator application (i.e. !isRelOpApplPred). For relational operator application the first (left) expression is usually a tuple containing the corresponding number of arguments. However, for a unary operator, the left expression does not have to be a tuple. For example, "n < m" has left="(n,m)", right=" _ < _ ", and arity 2; "disjoint s" has left="s", right="disjoint _ ", and arity 1; and if foo was declared as a unary postfix operator, then "(2,3) foo" would have left= "(2,3)", right=" _ foo", and arity 2. As no application has empty parameters (i.e. it would be a RefExpr), the result should never be empty (?) getRelOpApplPredArity public static int getRelOpApplPredArity(Term term) Returns the relational operator application aritity (i.e. its number of parameters), or -1 if term is not a MemPred relational operator application (i.e. !isRelOpApplPred). For relational operator application the first (left) expression is usually a tuple containing the corresponding number of arguments. However, for a unary operator, the left expression does not have to be a tuple. For example, "n < m" has left="(n,m)", right=" _ < _ ", and arity 2; "disjoint s" has left="s", right="disjoint _ ", and arity 1; and if foo was declared as a unary postfix operator, then "(2,3) foo" would have left= "(2,3)", right=" _ foo", and arity 2. As no application has empty parameters (i.e. it would be a RefExpr), arity should never be 0 ? isChainedConjunction public static boolean isChainedConjunction(Term term) Returns true if given term is an AndPred with And.Chain unicodeToAscii public static void unicodeToAscii(String name, StringBuffer result) toStringZName public static String toStringZName(ZName name) toStringZName public static String toStringZName(ZName name, boolean printUnicode, boolean printIds) setZFactoryToStringVisitor protected static void setZFactoryToStringVisitor(Factory f, Visitor<String> toStringVisitor) ; Changes the toString() method of ZFactory (within the given Factory), so that is uses the toString() strategy for the given visitor, usually one kind of PrintVisitor. They are important in order to debug/inspect easily the rather complex scoping mechanisms for basic (locally declared) processes. Parameters: f - factory toStringVisitor - new visitor assertZBranchList public static ZBranchList assertZBranchList(Term term) assertZName public static ZName assertZName(Term term) assertZNumeral public static ZNumeral assertZNumeral(Term term) assertZParaList public static ZParaList assertZParaList(Term term) assertZExprList public static ZExprList assertZExprList(Term term) assertZNameList public static ZNameList assertZNameList(Term term) assertZDeclList public static ZDeclList assertZDeclList(Term term) assertZFreetypeList public static ZFreetypeList assertZFreetypeList(Term term) assertZSchText public static ZSchText assertZSchText(Term term) assertZStrokeList public static ZStrokeList assertZStrokeList(Term term) assertZFactoryImpl public static ZFactoryImpl assertZFactoryImpl(Object factory) assertZPrintVisitor public static PrintVisitor assertZPrintVisitor(Object visitor) assertZTermImpl public static TermImpl assertZTermImpl(Object term) retrieveZSect public static ZSect retrieveZSect(Spec term, String sectName) strokeListToString public static String strokeListToString(List<Stroke> strokes) Transforms a list of strokes into a (unicode) string. namesEqual public static boolean namesEqual(ZName zName1, ZName zName2) Test whether the base name and strokes of two ZNames are equal. This ignores name ids. namesEqual public static boolean namesEqual(Name name1, Name name2) Test whether the base name and strokes of two Names are equal. This ignores name ids containsZName public static boolean containsZName(List<ZName> list, ZName zName) Test whether a list contains a ZName. Parameters: list - the list to search. zName - the ZName to search for. Returns: true if and only if the name is in the list. containsID public static boolean containsID(List<ZName> list, ZName zName) Test whether a list contains a ZName with the same ID. Parameters: list - the list to search. zName - the ZName to search for. Returns: true if and only if the name is in the list. idsEqual public static boolean idsEqual(String id1, String id2) sort public static Signature sort(Signature signature) Sorts the name type pairs within the given signature. Sorting occurs with respect to the compareTo protocol described in this class. sort public static List<NameTypePair> sort(List<NameTypePair> pairs) Sorts the list of name type pairs given. Sorting occurs with respect to the compareTo protocol described in this class. sortNames public static List<ZName> sortNames(List<ZName> names) insert public static void insert(List<NameTypePair> pairsA, List<NameTypePair> pairsB) Inserts all elements from pairsB in pairsA, provided pairsA are sorted. insertNames public static void insertNames(List<ZName> namesA, List<ZName> namesB) Inserts all elements from namesB in namesA, provided namesA are sorted. insert public static void insert(List<NameTypePair> pairs, NameTypePair pair) insertNames public static void insertNames(List<ZName> names, ZName name) compareTo public static int compareTo(ZName zName1, ZName zName2) compareToIgnoreStrokes public static int compareToIgnoreStrokes(ZName zName1, ZName zName2) getStrokeValue public static int getStrokeValue(Stroke stroke)

Class ZUtils

Nested Class Summary

Field Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

FACTORY

ZNAME_COMPARATOR

ZNAME_IGNORE_STROKES_COMPARATOR

STDZ_NAMELIST_CHECKER

Method Detail

createConsoleFactory

createFactory

setToStringVisitor

subsignature

isAnonymous

parentsAsString

trimNLCharAware

parentsCSVAsSetOfString

parentsAsSetOfParent

parentsAsListOfParent

parentsArgListAsSetOfString

isZPara

whatKindOfZExpr

isAxPara

getAxParaGenFormals

getAxParaZGenFormals

getAxBoxDecls

getAxBoxPred

isBoxedAxiomaticDef

isBoxedGenericDef

isHorizontalDef

isHorizontalSchema

isAbbreviation

isAxParaSchemaOrHorizDefValid

isSimpleSchema

isDeltaXi

isDeltaXi

isXi

isDelta

cloneTerm

containsObject

getSpecialSchemaBaseName

getSpecialSchemaBaseName

buildName

buildName

getSchemaName

getSchemaDefExpr

getSchemaZGenFormals

getAxParaSchOrAbbrName

getAbbreviationName

getAbbreviationExpr

getAbbreviationZGenFormals

isEmptySetRefExpr

isRefExpr

isApplExpr

isSetExpr

isTupleExpr

isBindSelExpr

isTupleSelExpr

isLambdaExpr

isMemPred

isAndPred

isReferenceExpr

isGenInstExpr

isExplicitGenInstExpr

isGenOpApplExpr

isRefExprValid

getGenOpApplZGenActuals

isFcnOpApplExpr

isApplicationExpr

isNestedApplExpr

isApplicationExprValid

getApplExprRef

getApplExprArguments

applExprArity

isEqualityPred

isRelOpApplPred

isMembershipPred

isMemPredValid