org.xmloperator.lambda.tree.util
Class AlphaUtils

java.lang.Object
  |
  +--org.xmloperator.lambda.tree.util.AlphaUtils

public abstract class AlphaUtils
extends java.lang.Object

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

AlphaUtils

public AlphaUtils()
Method Detail

matchingAbstraction

public static final Abstraction matchingAbstraction(Term variable)
Returns the Abstraction matching a given variable. Returns null if there is the variable is free.

Parameters:
variable - a Leaf or an EndOfScope.
Returns:
the Abstraction matching a given variable, if any, null elsewhere.

abstractionIndex

public static final int abstractionIndex(Term rootTerm,
                                         Abstraction abstraction)
Returns the index of an Abstraction within a Term. The first Abstraction in the Term has 0 as index. Ignores the EndOfSCopes.

Parameters:
rootTerm - a Term containing the given Abstraction.
abstraction - an Abstraction.
Returns:
the index of an Abstraction within a Term.

verifyClosure

public static final void verifyClosure(Term rootTerm)
Verify that a Term is closed, i.e. there is no free variable in it.

Parameters:
rootTerm - a Term.
Throws:
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.

strictlyEquals

public static final boolean strictlyEquals(Term rootTerm1,
                                           Term rootTerm2)
Evaluates the strict-equivalence of two Terms.

Returns:
true if the two given Term are strictly equivalent.
Throws:
java.lang.IllegalArgumentException - if some argument is null.
java.lang.NullPointerException - if some argument term is broken.

alphaEquals

public static final boolean alphaEquals(Term rootTerm1,
                                        Term rootTerm2)
Evaluates the alpha-equivalence of two closed Terms.

Returns:
true if the two given Term are alpha-equivalent.
Throws:
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.

clone

public static final Term clone(Term rootTerm)
Clones a Term.

Parameters:
rootTerm - a Term.
Returns:
the created Term.
Throws:
java.lang.NullPointerException - if the given Term is broken.

verifyScopeExtrusion

public static final void verifyScopeExtrusion(Term rootTerm)
Verify that all the EndOfScopes of a Term are extruded. There must be no EndOfScope whose child is an Abstraction or an Application.

Parameters:
rootTerm - a Term.
Throws:
org.xmloperator.lambda.tree.exception.UnextrudedEndOfScopeException - if there is some EndOfScope whose child is an Abstraction or an Application.

normalizedClone

public static final Term normalizedClone(Term rootTerm)
Create a normalized clone, whose all internal EndOfScopes are extruded.

Parameters:
rootTerm - a Term.
Returns:
the created normalized Term.
Throws:
java.lang.NullPointerException - if the given Term is broken.

extrude

public static final void extrude(EndOfScope endOfScope)
Extrudes an EndOfScope completely. Does nothing if the body of the given EndOfScope is neither an Abstraction nor an Application.

Parameters:
endOfScope - an EndOfScope.

main

public static void main(java.lang.String[] args)

test

public static boolean test(java.io.PrintStream out,
                           boolean isVerbose)
Verify equality and unequality between some terms.

Parameters:
out - the PrintStream to print results.
isVerbose - if true then all tests have to be displayed.
Returns:
true if all is Ok.