|
|||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object | +--org.xmloperator.lambda.tree.util.AlphaUtils
Utilities about cloning, scope extrusion and alpha-equality.
Constructor Summary | |
AlphaUtils()
|
Method Summary | |
static int |
abstractionIndex(Term rootTerm,
Abstraction abstraction)
Returns the index of an Abstraction within a Term. |
static boolean |
alphaEquals(Term rootTerm1,
Term rootTerm2)
Evaluates the alpha-equivalence of two closed Terms. |
static Term |
clone(Term rootTerm)
Clones a Term. |
static void |
extrude(EndOfScope endOfScope)
Extrudes an EndOfScope completely. |
static void |
main(java.lang.String[] args)
|
static Abstraction |
matchingAbstraction(Term variable)
Returns the Abstraction matching a given variable. |
static Term |
normalizedClone(Term rootTerm)
Create a normalized clone, whose all internal EndOfScopes are extruded. |
static boolean |
strictlyEquals(Term rootTerm1,
Term rootTerm2)
Evaluates the strict-equivalence of two Terms. |
static boolean |
test(java.io.PrintStream out,
boolean isVerbose)
Verify equality and unequality between some terms. |
static void |
verifyClosure(Term rootTerm)
Verify that a Term is closed, i.e. there is no free variable in it. |
static void |
verifyScopeExtrusion(Term rootTerm)
Verify that all the EndOfScopes of a Term are extruded. |
Methods inherited from class java.lang.Object |
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Constructor Detail |
public AlphaUtils()
Method Detail |
public static final Abstraction matchingAbstraction(Term variable)
variable
- a Leaf or an EndOfScope.
public static final int abstractionIndex(Term rootTerm, Abstraction abstraction)
rootTerm
- a Term containing the given Abstraction.abstraction
- an Abstraction.
public static final void verifyClosure(Term rootTerm)
rootTerm
- a Term.
org.xmloperator.lambda.tree.exception.MissingContextException
- if the given Term is not closed. The free
variable is provided by the exception.
java.lang.NullPointerException
- if the given Term is broken.public static final boolean strictlyEquals(Term rootTerm1, Term rootTerm2)
java.lang.IllegalArgumentException
- if some argument is null.
java.lang.NullPointerException
- if some argument term is broken.public static final boolean alphaEquals(Term rootTerm1, Term rootTerm2)
java.lang.IllegalArgumentException
- if some argument is null.
java.lang.NullPointerException
- if some argument term is broken.
org.xmloperator.lambda.tree.exception.MissingContextException
- if one of the given Term is not closed.public static final Term clone(Term rootTerm)
rootTerm
- a Term.
java.lang.NullPointerException
- if the given Term is broken.public static final void verifyScopeExtrusion(Term rootTerm)
rootTerm
- a Term.
org.xmloperator.lambda.tree.exception.UnextrudedEndOfScopeException
- if there is some EndOfScope
whose child is an Abstraction or an Application.public static final Term normalizedClone(Term rootTerm)
rootTerm
- a Term.
java.lang.NullPointerException
- if the given Term is broken.public static final void extrude(EndOfScope endOfScope)
endOfScope
- an EndOfScope.public static void main(java.lang.String[] args)
public static boolean test(java.io.PrintStream out, boolean isVerbose)
out
- the PrintStream to print results.isVerbose
- if true then all tests have to be displayed.
|
|||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |