public class ConstraintException extends DataException {

	/**
	 * Constructs a new <code>ConstraintException</code> with the
	 * specified detail message.
	 *
	 * @param message detail message.
	 */
	public ConstraintException(final String message) {
		this(message, null);
	}

	/**
	 * Constructs a new <code>ConstraintException</code> with the
	 * specified detail message and cause.
	 *
	 * @param message detail message.
	 * @param cause (A <code>null</code> value is permitted, and
	 * 	indicates that the cause is nonexistent or unknown.)
	 */
	public ConstraintException(final String message, final Throwable cause) {
		super(message, cause);
	}

} public interface DVConstraints extends Iterable<Variable[]>, Serializable {

	/**
	 * Adds the specified variables to these <code>DVConstraints</code>
	 * by adding each non-diagonal pair.
	 *
	 * @param vars variables to be added.
	 *
	 * @throws DataException if the same variable appears twice in the
	 * 	specified array.
	 */
	public void add(Variable... vars) throws ConstraintException;

	/**
	 * Adds the entire DV constraints specified to these
	 * <code>DVConstraints</code>.
	 *
	 * @param dvConstraints DV constraints to add
	 */
	public void add(DVConstraints dvConstraints);

	/**
	 * Adds the cartesian product of the two specified sets of variables.
	 *
	 * @param varSet1 first set.
	 * @param varSet2 second set.
	 *
	 * @throws ConstraintException if the two sets are not disjoint.
	 */
	public void addProduct(Set<Variable> varSet1, Set<Variable> varSet2) throws ConstraintException;

	/**
	 * Checks whether the specified variable pair is contained in these
	 * <code>DVConstraints</code>.
	 *
	 * @param var1 first variable.
	 * @param var2 second variable.
	 *
	 * @return <code>true</code> if {<code>var1</code>, <code>var2</code>}
	 * 	is contained in these constraints, <code>false</code>
	 * 	otherwise.
	 */
	public boolean contains(Variable var1, Variable var2);

	/**
	 * Checks whther the specified DV constraints are contained in these
	 * DV constraints.
	 *
	 * @param dv other disjoint variable constraints.
	 *
	 * @return <code>true</code> if <code>dv</code> is contained in these
	 * 	constraints, <code>false</code> otherwise.
	 */
	public boolean contains(DVConstraints dv);

	/**
	 * Removes all variable pairs from these <code>DVConstraints</code>
	 * whose elements are not both contained in the specified set.
	 *
	 * @param varSet variable set to restrict these constraints to.
	 */
	public void restrict(Set<Variable> varSet);

} public abstract class DataFactory {

	/**
	 * Instance.
	 */
	private static final DataFactory instance = new jhilbert.data.impl.DataFactory();

	/**
	 * Obtains a <code>DataFactory</code> instance.
	 *
	 * @return a <code>DataFactory</code> instance.
	 */
	public static DataFactory getInstance() {
		return instance;
	}

	/**
	 * Creates a new unversioned {@link Module} with the specified name.
	 *
	 * @param name module name.
	 *
	 * @return new unversioned module.
	 */
	public final Module createModule(String name) {
		try {
			return createModule(name, -1);
		} catch (DataException e) {
			assert false: "Revision -1 invalid: this should not happen";
			throw new IllegalArgumentException("Revision -1 invalid: this should not happen");
		}
	}

	/**
	 * Creates a new {@link Module} with the specified name and revision
	 * number.
	 * The revision number is a non-negative integer. A value of
	 * <code>-1</code> is also permitted, indicating an unversioned module.
	 *
	 * @param name module name.
	 * @param revision module revision number.
	 *
	 * @return new versioned module.
	 *
	 * @throws DataException if the <code>revision</code> is smaller than
	 * 	<code>-1</code>.
	 */
	public abstract Module createModule(String name, long revision) throws DataException;

	public Module createInterface(String name, long revision) throws DataException {
		assert name != "" : "An interface must have a name";
		return createModule(name, revision);
	}

	public Module createProofModule(long revision) throws DataException {
		return createModule("", revision);
	}

	/**
	 * Creates a new {@link Kind} with the specified name in the specified
	 * kind {@link Namespace}.
	 *
	 * @param name name of the new kind.
	 * @param namespace namespace in which the new kind should be
	 * 	registered.
	 *
	 * @return the new kind.
	 *
	 * @throws DataException if a kind with the specified name already
	 * 	exists in the specified namespace.
	 */
	public final Kind createKind(String name, Namespace<? extends Kind> namespace) throws DataException {
		return createKind(name, null, -1, namespace);
	}

	/**
	 * Creates a new {@link Kind} derived from the specified old kind in
	 * the specified kind {@link Namespace}. A value of <code>null</code>
	 * is permissible for the old kind, indicating that the new kind is not
	 * derived from any other kind.
	 *
	 * @param name name of the new kind.
	 * @param oldkind old kind the new kind should be derived from.
	 * @param parameterIndex index of parameter of <code>oldkind</code>.
	 * @param namespace namespace in which the new kind should be
	 * 	registered.
	 *
	 * @return the new kind.
	 *
	 * @throws DataException if a kind with the specified name already
	 * 	exists in the specified namespace.
	 */
	public abstract Kind createKind(String name, Kind oldkind, int parameterIndex, Namespace<? extends Kind> namespace)
	throws DataException;

	/**
	 * Creates a new {@link Variable} of the specified {@link Kind} in the
	 * specified symbol {@link Namespace}.
	 *
	 * @param name name of the new variable.
	 * @param kind kind of the new variable.
	 * @param namespace namespace in which the new variable should be
	 * 	registered.
	 *
	 * @return the new variable.
	 *
	 * @throws DataException if a variable with the specified name already
	 * 	exists in the specified namespace.
	 */
	public abstract Variable createVariable(String name, Kind kind, Namespace<? extends Symbol> namespace) throws DataException;

	/**
	 * Creates a new unnamed {@link Variable} of the specified
	 * {@link Kind}.
	 * This is useful for anonymising expressions.
	 *
	 * @param kind kind of the new unnamed variable.
	 *
	 * @return the new unnamed variable.
	 */
	public abstract Variable createUnnamedVariable(Kind kind);

	/**
	 * Creates a new dummy {@link Variable} of the specified {@link Kind}.
	 * This method is similar to {@link #createUnnamedVariable} except
	 * that the new variable's {@link Variable#isDummy} method returns
	 * <code>true</code>.
	 *
	 * @param kind kind of the new unnamed variable.
	 *
	 * @return the new dummy variable.
	 */
	public abstract Variable createDummyVariable(Kind kind);

	/**
	 * Creates a new {@link Functor} with the specified name, kind and
	 * input kinds in the specified namespace.
	 *
	 * @param name name of new functor.
	 * @param kind kind of new functor.
	 * @param inputKinds List of input kinds.
	 * @param namespace namespace in which the new functor will be
	 * 	registered.
	 *
	 * @return the new functor.
	 *
	 * @throws DataException if a functor with the specified name already
	 * 	exists in the specified namespace.
	 */
	public final Functor createFunctor(final String name, final Kind kind, final List<Kind> inputKinds, final Namespace<? extends Functor> namespace)
	throws DataException {
		return createFunctor(name, null, -1, kind, inputKinds, namespace);
	}

	/**
	 * Creates a new {@link Functor} derived from the specified original
	 * functor with the specified name, kind and input kinds in the
	 * specified namespace.
	 *
	 * @param name name of the new functor.
	 * @param orig name this functor should be derived from.
	 * @param parameterIndex index of the parameter of <code>orig</code>.
	 * @param kind kind of new functor.
	 * @param inputKinds List of input kinds.
	 * @param namespace namespace in which the new functor will be
	 * 	registered.
	 *
	 * @return the new functor.
	 *
	 * @throws DataException if a functor with the specified name already
	 * 	exists in the specified namespace.
	 */
	public abstract Functor createFunctor(String name, Functor orig, int parameterIndex, Kind kind, List<Kind> inputKinds, Namespace<? extends Functor> namespace)
	throws DataException;

	/**
	 * Creates a new {@link Definition} with the specified name,
	 * argument list and definiens.
	 *
	 * @param name name of new definition.
	 * @param dvConstraints DV constraints of definition, or
	 * 	<code>null</code> if there are no constraints.
	 * @param argList argument list.
	 * @param definiens definiens of the new definition.
	 * @param namespace namespace in which the new definition will be
	 * 	registered.
	 *
	 * @return the new definition.
	 *
	 * @throws DataException if <code>argList</code> contains the same
	 * 	entry more than once.
	 */
	public final Definition createDefinition(final String name, final DVConstraints dvConstraints,
			final List<Variable> argList, final Expression definiens,
			final Namespace<? extends Functor> namespace)
	throws DataException {
		return createDefinition(name, null, -1, dvConstraints, argList, definiens, namespace);
	}

	/**
	 * Creates a new {@link Definition} derived from the specified original
	 * definition with the specified name, kind and input kinds in the
	 * specified namespace.
	 *
	 * @param name name of new definition.
	 * @param orig name this definition should be derived from.
	 * @param parameterIndex index of the parameter of <code>orig</code>.
	 * @param dvConstraints DV constraints of definition, or
	 * 	<code>null</code> if there are no constraints.
	 * @param argList argument list.
	 * @param definiens definiens of the new definition.
	 * @param namespace namespace in which the new definition will be
	 * 	registered.
	 *
	 * @return the new definition.
	 *
	 * @throws DataException if <code>argList</code> contains the same
	 * 	entry more than once.
	 */
	public abstract Definition createDefinition(String name, Definition orig, int parameterIndex,
			DVConstraints dvConstraints, List<Variable> argList, Expression definiens,
			Namespace<? extends Functor> namespace)
	throws DataException;

	/**
	 * Creates new, empty {@link DVConstraints}.
	 *
	 * @return new, empty disjoint variable constraints.
	 */
	public abstract DVConstraints createDVConstraints();

	/**
	 * Scans new {@link DVConstraints} from the specified
	 * {@link TokenFeed} containing variables from the specified symbol
	 * namespace.
	 *
	 * @param namespace namespace to obtain variables from.
	 * @param tokenFeed token feed to scan constraints from.
	 *
	 * @return the new constraints.
	 *
	 * @throws ConstraintException if a scanner error occurs or if a variable
	 * 	could not be found.
	 */
	public abstract DVConstraints createDVConstraints(Namespace<? extends Symbol> namespace, TokenFeed tokenFeed) throws ConstraintException;

	/**
	 * Creates a new {@link Statement} with the specified name, disjoint
	 * variable constraints, hypotheses and consequent in the specified
	 * namespace.
	 *
	 * @param name name of new statement.
	 * @param dv disjoint variable constraints.
	 * @param hypotheses {@link List} of hypotheses.
	 * @param consequent consequent of new statement.
	 * @param namespace namespace in which the new statement will be
	 * 	created.
	 *
	 * @return the new statement.
	 *
	 * @throws DataException if a statement with the specified name has
	 * 	already been registered in the specified namespace.
	 * @throws ConstraintException if the statements contains expressions
	 * 	with invalid DV constraints.
	 */
	public final Statement createStatement(final String name, final DVConstraints dv, final List<Expression> hypotheses, final Expression consequent,
		final Namespace<? extends Symbol> namespace)
	throws DataException {
		return createStatement(name, null, -1, dv, hypotheses, consequent, namespace);
	}

	/**
	 * Creates a new {@link Statement} derived from the specified
	 * original statement with the specified name, disjoint variable
	 * constraints, hypotheses and consequent.
	 *
	 * @param name name of new statement.
	 * @param orig statement this statement is derived from.
	 * @param parameterIndex index of the parameter of <code>orig</code>.
	 * @param dv disjoint variable constraints.
	 * @param hypotheses {@link List} of hypotheses.
	 * @param consequent consequent of new statement.
	 * @param namespace namespace in which the new statement will be created.
	 *
	 * @return the new statement.
	 *
	 * @throws DataException if a statement with the specified name has
	 * 	already been registered in the specified namespace.
	 */
	public abstract Statement createStatement(String name, Statement orig, int parameterIndex, DVConstraints dv, List<Expression> hypotheses, Expression consequent,
		Namespace<? extends Symbol> namespace)
	throws DataException;

	/**
	 * Creates a new {@link Parameter} with the specified name, locator,
	 * parameter list and prefix.
	 *
	 * @param name name of new parameter.
	 * @param locator module locator of new parameter.
	 * @param parameterList parameter list.
	 * @param prefix namespace prefix.
	 *
	 * @return new parameter.
	 */
	public abstract Parameter createParameter(String name, String locator, List<Parameter> parameterList, String prefix);

	/**
	 * Scans a new {@link Parameter} from the specified token feed using
	 * data from the specified module.
	 *
	 * @param module data module.
	 * @param tokenFeed {@link TokenFeed} to obtain parameter data.
	 *
	 * @return the new parameter.
	 *
	 * @throws DataException if a syntax error occurs.
	 */
	public abstract Parameter createParameter(Module module, TokenFeed tokenFeed) throws DataException;

	/**
	 * Creates a new {@link ParameterLoader} to load the specified
	 * {@link Parameter} into the specified {@link Module}.
	 *
	 * @param parameter parameter to load/import/export.
	 * @param module module to load/import/export parameter into.
	 *
	 * @return the new parameter loader.
	 *
	 * @throws DataException if the parameter module cannot be loaded.
	 */
	public abstract ParameterLoader createParameterLoader(final Parameter parameter, final Module module)
	throws DataException;
	
	/**
	 * Creates a new {@link ParameterLoader} to load the specified
	 * {@link Parameter} into the specified {@link Module}. Rather than
	 * fetch the parameter's module from the default location (for example,
	 * a file named by the parameter's locator), fetch it from parameterModule.
	 * 
	 * @param parameter parameter to load/import/export.
	 * @param module module to load/import/export parameter into.
	 * @param parameterModule contents of parameter's module.
	 *
	 * @return the new parameter loader.
	 *
	 * @throws DataException if the parameter module cannot be loaded.
	 */
	public abstract ParameterLoader createParameterLoader(
			final Parameter parameter, final Module parameterModule, final Module module)
	throws DataException;

} public interface Kind extends Name {

	public Namespace<? extends Kind> getNamespace();

	public Kind getOriginalName();

} public interface Module extends Serializable {

	/**
	 * Obtains the name of the module.
	 * The name of the module is an identifier for the interface in which
	 * the data are defined. If this module contains the data of the
	 * current main proof module, the empty string is returned.
	 *
	 * @return module name, or the empty string, if this is the main proof
	 * 	module.
	 */
	public String getName();

	/**
	 * Obtains the revision number of the current module.
	 * Revision numbers allow for simple versioning of interfaces. They are
	 * useful for a storage backend to decide where the data goes.
	 *
	 * @return the revision number of this module, which must be a
	 * 	non-negative integer, or <code>-1</code> if this module is not
	 * 	versioned.
	 */
	public long getRevision();

	/**
	 * Obtains the parameters of this module in proper order.
	 *
	 * @return parameters of this module.
	 */
	public List<Parameter> getParameters();

	/**
	 * Obtains the parameter by the specified name.
	 *
	 * @param name name of parameter.
	 *
	 * @return parameter with name <code>name</code>, or <code>null</code>
	 * 	if no such parameter exists in this module.
	 */
	public Parameter getParameter(String name);

	/**
	 * Adds the specified {@link Parameter} to this <code>Module</code>.
	 *
	 * @param parameter parameter to be added.
	 *
	 * @throws DataException if a parameter with the same name as
	 * 	<code>parameter</code> has previously been added.
	 */
	public void addParameter(Parameter parameter) throws DataException;

	/**
	 * Obtains the {@link Namespace} containing the {@link Kind}s defined
	 * in this module.
	 *
	 * @return the kind namespace of this module.
	 */
	public Namespace<? extends Kind> getKindNamespace();

	/**
	 * Obtains the {@link Namespace} containing the {@link Symbol}s defined
	 * in this module.
	 *
	 * @return the symbol namespace of this module.
	 */
	public Namespace<? extends Symbol> getSymbolNamespace();

	/**
	 * Obtains the {@link Namespace} containing the {@link Functor}s
	 * defined in this module.
	 *
	 * @return the functor namespace of this module.
	 */
	public Namespace<? extends Functor> getFunctorNamespace();

	public boolean isProofModule();

} public interface Namespace<E extends Name> extends Serializable {

	/**
	 * Obtains the {@link Module} this <code>Namespace</code> belongs to.
	 *
	 * @return {@link Module} this <code>Namespace</code> belongs to.
	 */
	public Module getModule();

	/**
	 * Registers the specified {@link Name}-derived object with this
	 * namespace.
	 * If the same name has already been registered, a
	 * {@link DataException} is thrown. &quot;Same&quot; here means
	 * that the {@link Name#getNameString} method returns a string which
	 * is equal to the name string of a previously registered name.
	 *
	 * @param o object to register. Must be convertible to <code>E</code>.
	 * 
	 * @throws DataException if the same name has already been registered.
	 */
	public void registerObject(Name o) throws DataException;

	/**
	 * Obtains a previously registered object by its name string.
	 *
	 * @param name name string.
	 *
	 * @return the object which was previously registered under the
	 * 	specified name, or <code>null</code> if no object with the
	 * 	specified name has been registered with this namespace.
	 *
	 * @see #registerObject
	 */
	public E getObjectByString(String name);

	/**
	 * Checks the two specified {@link Name}-derived objects for equality.
	 * <p>
	 * <strong>Warning:</strong> This is <em>not</em> the same as calling
	 * {@link java.lang.Object#equals} on one of the objects with the other
	 * as parameter.
	 * <p>
	 * If both objects are registered with this namespace, they are
	 * considered equal if they are the same, or if they have been
	 * identified in this namespace.
	 * <p>
	 * If only one of the objects is registered with this namespace, they
	 * are not considered equal.
	 * <p>
	 * If <em>none</em> of the objects are registered with this namespace,
	 * an exception is thrown.
	 *
	 * @param obj1 first object to be checked for equality.
	 * @param obj2 second object to be checked for equality.
	 *
	 * @return <code>true</code> if <code>obj1</code> and <code>obj2</code>
	 * 	are equal in the sense described above, <code>false</code>
	 * 	otherwise.
	 *
	 * @throws DataException if none of the two parameters is registered
	 * 	with this namespace.
	 *
	 * @see #identify
	 */
	public boolean checkEquality(Name obj1, Name obj2) throws DataException;

	/**
	 * Creates an alias for a previously registered object. The object
	 * can then be retrieved by {@link #getObjectByString} using the
	 * alias.
	 *
	 * @param obj registered object.
	 * @param name new name for the object <code>obj</code>.
	 *
	 * @throws DataException if <code>obj</code> has not been registered
	 * 	with this <code>Namespace</code>, or if <code>name</code> has
	 * 	already been created as an alias, or is the name of another
	 * 	registered object.
	 *
	 * @see #registerObject
	 * @see #getObjectByString
	 */
	public void createAlias(Name obj, String name) throws DataException;

	/**
	 * Identifies two previously registered objects with each other.
	 * A call of {@link #checkEquality} on the specified objects will
	 * subsequently return <code>true</code>.
	 *
	 * @param obj1 first object
	 * @param obj2 second object
	 *
	 * @throws DataException if one of the objects has not been registered
	 * 	with this namespace.
	 *
	 * @see #checkEquality
	 */
	public void identify(Name obj1, Name obj2) throws DataException;

	/**
	 * Returns a view of the objects in this <code>Namespace</code>.
	 * This includes identified, but not aliased entries. Use
	 * {@link #equivalenceClasses} to obtain equivalence classes.
	 *
	 * @return view of the objects in this namespace. The returned
	 * 	collection does not contain duplicate entries. The collection's
	 * 	iteration order corresponds to the order in which the objects
	 * 	were registered.
	 *
	 * @see #equivalenceClasses
	 * @see #createAlias
	 * @see #identify
	 */
	public Collection<E> objects();

	/**
	 * Returns a view of the aliases in this <code>Namespace</code>.
	 *
	 * @return view of the aliases in this namespace.
	 */
	public Map<String, E> aliases();

	/**
	 * Returns a view of all equivalence classes in this
	 * <code>Namespace</code> which contain more than one element.
	 *
	 * @return view of all equivalence classes in this namespace which
	 * 	contain more than element. The returned collection does not
	 * 	contain duplicate entries.
	 */
	public Collection<Set<E>> equivalenceClasses();

} public interface Statement extends Symbol {

	/**
	 * Returns the {@link DVConstraints} of this <code>Statement</code>.
	 *
	 * @return disjoint variable constraints.
	 */
	public DVConstraints getDVConstraints();

	/**
	 * Returns the hypotheses of this <code>Statement</code>.
	 *
	 * @return hypotheses of this statement.
	 */
	public List<Expression> getHypotheses();

	/**
	 * Returns the consequent of this statement.
	 */
	public Expression getConsequent();

	/**
	 * Returns the mandatory variables of this statement.
	 */
	public List<Variable> getMandatoryVariables();

} public interface Symbol extends Name {

	public Namespace<? extends Symbol> getNamespace();

	/**
	 * Returns whether this <code>Symbol</code> is a {@link Variable}.
	 *
	 * @return <code>true</code> if this <code>Symbol</code> is a
	 * 	{@link Variable}, <code>false</code> otherwise.
	 */
	public boolean isVariable();

} public interface Variable extends Symbol, Term {

	/**
	 * Reimplemented from {@link Name#getOriginalName}, this method always
	 * returns <code>null</code> as variables are always local.
	 *
	 * @return <code>null</code>.
	 */
	public Name getOriginalName();

	/**
	 * Returns whether this <code>Variable</code> is a dummy variable.
	 *
	 * @return <code>true</code> if this <code>Variable</code> is a dummy
	 * 	variable, <code>false</code> otherwise.
	 */
	public boolean isDummy();

} public interface Expression extends TreeNode<Term>, Serializable {

	/**
	 * Returns the kind of this <code>Expression</code>.
	 *
	 * @return kind of this expression.
	 */
	public Kind getKind();

	/**
	 * Returns the sub-expressions of this <code>Expression</code> in
	 * proper order.
	 *
	 * @return list of subexpressions.
	 */
	public List<Expression> getChildren();

	/**
	 * Returns the {@link DVConstraints} applicable to this
	 * <code>Expression</code>.
	 *
	 * @return applicable DVConstraints
	 *
	 * @throws ConstraintException if the DV constraints cannot be met
	 * 	ever.
	 */
	public DVConstraints dvConstraints() throws ConstraintException;

	/**
	 * Returns the {@link Variable}s occurring in this
	 * <code>Expression</code>, in order of first appearance.
	 *
	 * @return variables occurring in this expression.
	 */
	public LinkedHashSet<Variable> variables();

	/**
	 * Returns the totally unfolded version of this expression.
	 *
	 * @return totally unfolded expression.
	 */
	public Expression totalUnfold();

} public class ExpressionException extends JHilbertException {

	/**
	 * Constructs a new <code>ExpressionException</code> with the
	 * specified detail message.
	 *
	 * @param message detail message.
	 */
	public ExpressionException(final String message) {
		this(message, null);
	}

	/**
	 * Constructs a new <code>ExpressionException</code> with the
	 * specified detail message and cause.
	 *
	 * @param message detail message.
	 * @param cause the cause.
	 */
	public ExpressionException(final String message, final Throwable cause) {
		super(message, cause);
	}

} public abstract class ExpressionFactory {

	/**
	 * Instance.
	 */
	private static final ExpressionFactory instance = new jhilbert.expressions.impl.ExpressionFactory();

	/**
	 * Obtains an instance of a <code>ExpressionFactory</code>.
	 *
	 * @return expression factory instance.
	 */
	public static ExpressionFactory getInstance() {
		return instance;
	}

	/**
	 * Scans a new {@link Expression} from the specified
	 * {@link TokenFeed} using data from the specified {@link Module}.
	 *
	 * @param module data module.
	 * @param tokenFeed token feed.
	 *
	 * @return the new expression.
	 *
	 * @throws ExpressionException if an error occurs.
	 */
	public abstract Expression createExpression(Module module, TokenFeed tokenFeed) throws ExpressionException;

	/**
	 * Creates a new {@link Expression} consisting just of the specified
	 * {@link Variable}.
	 *
	 * @param var variable.
	 *
	 * @return a new expression consisting just of <code>var</code>.
	 */
	public abstract Expression createExpression(Variable var);

	/**
	 * Creates a new {@link Expression} from the specified functor
	 * and children.
	 *
	 * @param functor functor.
	 * @param children list of children.
	 */
	public abstract Expression createExpression(Functor functor, List<Expression> children);

	/**
	 * Creates a new {@link Matcher}.
	 *
	 * @return new matcher.
	 */
	public abstract Matcher createMatcher();

	/**
	 * Creates a new {@link Substituter} from the specified substitution
	 * map.
	 *
	 * @param v2eMap substitution map.
	 *
	 * @return the new substituter.
	 */
	public abstract Substituter createSubstituter(Map<Variable, Expression> v2eMap);

	/**
	 * Creates a new {@link Anonymiser} from the spcified variable set.
	 *
	 * @param varSet variable set.
	 *
	 * @return the new anonymiser.
	 */
	public abstract Anonymiser createAnonymiser(Set<Variable> varSet);

	/**
	 * Creates a new {@link Translator} for the specified {@link Kind} and
	 * {@link Functor} mappings.
	 *
	 * @param kindMap kind map.
	 * @param functorMap functor map.
	 *
	 * @return the new translator.
	 */
	public abstract Translator createTranslator(Map<Kind, Kind> kindMap, Map<Functor, Functor> functorMap);

} public interface Matcher {

	/**
	 * Checks the source and the target expression for <em>definition
	 * equivalence</em> as specified in the interface description.
	 *
	 * @param source source expression.
	 * @param target target expression.
	 *
	 * @return <code>true</code> if <code>source</code> and
	 * 	<code>target</code> are equal as specified, <code>false</code>
	 * 	otherwise.
	 */
	public boolean checkDEquality(Expression source, Expression target);

	/**
	 * Checks the source and the target expression for <em>variable
	 * equivalence</em> as specified in the interface description.
	 * The internal variable assignment map is updated accordingly. This
	 * means it may be left in an undefined state if this method throws an
	 * exception or returns <code>false</code>.
	 *
	 * @param source source expression.
	 * @param target target expression.
	 * @param blacklist list of not-to-dummy-assignable variables.
	 *
	 * @return <code>true</code> if <code>source</code> and
	 * 	<code>target</code> are equal as specified, <code>false</code>
	 * 	otherwise.
	 *
	 * @throws UnifyException if an otherwise well-formed assignment is
	 * 	forbidden by the <code>blacklist</code>.
	 */
	public boolean checkVEquality(Expression source, Expression target, Set<Variable> blacklist) throws UnifyException;

	/**
	 * Like {@link #checkVEquality(Expression, Expression, Set)}, except
	 * that the <code>blacklist</code> is assumed to be empty.
	 *
	 * @param source source expression.
	 * @param target target expression.
	 *
	 * @return <code>true</code> if <code>source</code> and
	 * 	<code>target</code> are equal as specified, <code>false</code>
	 * 	otherwise.
	 *
	 * @see #checkVEquality(Expression, Expression, Set)
	 */
	public boolean checkVEquality(Expression source, Expression target);

	/**
	 * Returns the current internal assignment map of this
	 * <code>Matcher</code>.
	 *
	 * @return translation map of this matcher.
	 */
	public Map<Variable, Variable> getAssignmentMap();

} public interface Substituter {

	/**
	 * Returns the current {@link Variable} to {@link Expression}
	 * assignments of this <code>Substituter</code>.
	 *
	 * @return the current variable to expression assigments.
	 */
	public Map<Variable, Expression> getAssignments();

	/**
	 * Creates a new {@link Expression} by substituting the specified
	 * expression using the substitution rule inherent to this
	 * <code>Substituter</code>.
	 *
	 * @param expr expression to be substituted.
	 *
	 * @return new substituted expression.
	 */
	public Expression substitute(Expression expr);

	/**
	 * This method performs the reverse of {@link #substitute}. The
	 * internal variable assignments are updated so that applying
	 * {@link #substitute} to the specified source expression would yield
	 * the specified target expression.
	 *
	 * @param source source expression.
	 * @param target target expression.
	 *
	 * @throws UnifyException if a well-formed update of the internal
	 * 	variable assigments to meet the specification above is not
	 * 	possible. If this exception is thrown, the internal assignment
	 * 	map may be left in an undefined state.
	 *
	 * @see #getAssignments
	 */
	public void unify(Expression source, Expression target) throws UnifyException;

	/**
	 * This is a special method to unify cross-module expressions.
	 * Source expressions are completely unfolded before translated and
	 * unified. This is necessary for definition compatibility.
	 *
	 * @param source source expression.
	 * @param target target expression.
	 * @param translator module translator.
	 *
	 * @throws UnifyException if the unfolded expressions cannot be
	 * 	unified with {@link #unify(Expression, Expression)}.
	 */
	public void crossUnify(Expression source, Expression target, Translator translator) throws UnifyException;

} public class UnifyException extends ExpressionException {

	/**
	 * Source term of failed unification.
	 */
	private final Expression source;

	/**
	 * Target term of failed unification.
	 */
	private final Expression target;

	/**
	 * Creates a new <code>UnifyException</code> with the specified detail
	 * message, source and target of the failed unification.
	 *
	 * @param message detail message.
	 * @param source source term.
	 * @param target target term.
	 */
	public UnifyException(final String message, final Expression source, final Expression target) {
		this(message, source, target, null);
	}

	/**
	 * Creates a new <code>UnifyException</code> with the specified detail
	 * message, source, target and cause.
	 *
	 * @param message detail message.
	 * @param source source term.
	 * @param cause the cause.
	 */
	public UnifyException(final String message, final Expression source, final Expression target, final Throwable cause) {
		super(message, cause);
		this.source = source;
		this.target = target;
	}

	/**
	 * Returns the source term of the failed unification.
	 *
	 * @return source term of failed unification.
	 */
	public Expression getSource() {
		return source;
	}

	/**
	 * Returns the target term of the failed unification.
	 *
	 * @return target term of failed unification.
	 */
	public Expression getTarget() {
		return target;
	}

} public class ScannerException extends JHilbertException {

	/**
	 * Scanner which created the exception.
	 */
	private final Scanner scanner;

	/**
	 * Creates a new <code>ScannerException</code> with the specified
	 * detail message. This constructor should only be used by a
	 * {@link Scanner}, which the constructor is provided with.
	 *
	 * @param message detail message.
	 * @param scanner the scanner which created the exception.
	 */
	public ScannerException(final String message, final Scanner scanner) {
		this(message, scanner, null);
	}

	/**
	 * Creates a new <code>ScannerException</code> with the specified
	 * detail message and cause.
	 * This constructor should only be used by a {@link Scanner}, which
	 * the constructor is provided with.
	 *
	 * @param message detail message.
	 * @param scanner the scanner which created the exception.
	 * @param cause the cause. (A <code>null</code> value is permitted, and
	 * 	indicates that the cause is nonexistent or unknown.)
	 */
	public ScannerException(final String message, final Scanner scanner, final Throwable cause) {
		super(message, cause);
		this.scanner = scanner;
	}

	/**
	 * Obtains the scanner which caused this exception.
	 *
	 * @return scanner which caused this exception.
	 */
	public final Scanner getScanner() {
		return scanner;
	}

} public interface Token {

	/**
	 * Token classes.
	 */
	public static enum Class {

		/**
		 * Beginning of a LISP list.
		 */
		BEGIN_EXP,

		/**
		 * End of a LISP list.
		 */
		END_EXP,

		/**
		 * Atomic LISP symbolic expression.
		 */
		ATOM

	}

	/**
	 * Valid ATOM tokens.
	 */
	public static final Pattern VALID_ATOM
		= Pattern.compile("[^\\p{Cn}\\p{Cf}\\p{Cc}\\p{Zs}\\p{Zl}\\p{Zp}\\t\\(\\)\\r\\n\\#]+");

	/**
	 * Obtains a string representation of this token.
	 *
	 * @return string representation of this token.
	 */
	public String getTokenString();

	/**
	 * Obtains the class of this token.
	 *
	 * @return class of this token.
	 */
	public Class getTokenClass();

} public interface TokenFeed extends Scanner<Token> {
	// FIXME: it's not a good idea to extend Scanner<Token> but I'm lazy...

	/**
	 * Keyword confirmation message.
	 */
	public static final String KEYWORD = "keyword";

	/**
	 * Expression start confirmation message.
	 */
	public static final String BEGIN_EXP = "beginexp";

	/**
	 * Expression end confirmation message.
	 */
	public static final String END_EXP = "endexp";

	/**
	 * Kind confirmation message.
	 */
	public static final String KIND = "kind";

	/**
	 * Variable confirmation message.
	 */
	public static final String VARIABLE = "var";

	/**
	 * Term confirmation message.
	 */
	public static final String TERM = "term";

	/**
	 * Definition confirmation message.
	 */
	public static final String DEFINITION = "def";

	/**
	 * Statement confirmation message.
	 */
	public static final String STATEMENT = "stat";

	/**
	 * Label confirmation message.
	 */
	public static final String LABEL = "label";

	/**
	 * Parameter confirmation message.
	 */
	public static final String PARAMETER = "param";

	/**
	 * Locator confirmation message
	 */
	public static final String LOCATOR = "locator";

	/**
	 * String confirmation message.
	 */
	public static final String STRING = "string";

	/**
	 * Reads a LISP atom.
	 * This convenience method reads a token and returns it if it is an
	 * atom, otherwise the token will be rejected and a
	 * {@link ScannerException} is thrown.
	 *
	 * @return a new {@link Token} whose {@link Token.Class} is
	 * 	{@link Token.Class#ATOM}.
	 *
	 * @throws ScannerException if the next token is not an atom, or if
	 * 	reading the token fails.
	 */
	public String getAtom() throws ScannerException;

	/**
	 * Reads the beginning of a LISP s-expression.
	 * This convenience method reads a token and returns normally it if it
	 * is the beginning of a LISP s-expression (that is, an opening
	 * parenthesis), otherwise the token will be rejected and a
	 * {@link ScannerException} is thrown.
	 *
	 * @throws ScannerException if the next token is not of class
	 * 	{@link Token.Class#BEGIN_EXP}, or if reading the token fails.
	 */
	public void beginExp() throws ScannerException;

	/**
	 * Reads the end of a LISP s-expression.
	 * This convenience method reads a token and returns normally it if it
	 * is the end of a LISP s-expression (that is, a closing
	 * parenthesis), otherwise the token will be rejected and a
	 * {@link ScannerException} is thrown.
	 *
	 * @throws ScannerException if the next token is not of class
	 * 	{@link Token.Class#END_EXP}, or if reading the token fails.
	 */
	public void endExp() throws ScannerException;

	/**
	 * Reads a string.
	 * This convenience method reads a string, that is either an atom or
	 * a {@link Token} of class {@link Token.Class#BEGIN_EXP} immediately
	 * followed by a <code>Token</code> of class
	 * {@link Token.Class#END_EXP}, in which case the string is empty.
	 * In case of an empty string, the opening parenthesis is confirmed.
	 * If the input is not a string, the infringing token is rejected and
	 * a {@link ScannerException} os thrown.
	 *
	 * @return a string as specified.
	 *
	 * @throws ScannerException if a string as specified could not be
	 * 	found, or if reading the token(s) fails.
	 */
	public String getString() throws ScannerException;

	/**
	 * Confirms the last token.
	 * Once a token has been confirmed, it cannot be put back.
	 *
	 * @param msg confirmation message.
	 *
	 * @throws ScannerException if confirmation fails.
	 *
	 * @see #putToken
	 */
	public void confirm(String msg) throws ScannerException;

	/**
	 * Rejects the last token.
	 * Once a token has been rejected, scanning should cease.
	 *
	 * @param msg rejection message.
	 *
	 * @throws ScannerException if rejection fails.
	 */
	public void reject(String msg) throws ScannerException;

	/**
	 * Convenience method to confirm a keyword.
	 *
	 * @throws ScannerException if confirmation fails.
	 */
	public void confirmKeyword() throws ScannerException;

	/**
	 * Convenience method to confirm an expression start.
	 *
	 * @throws ScannerException if confirmation fails.
	 */
	public void confirmBeginExp() throws ScannerException;

	/**
	 * Convenience method to confirm an expression end.
	 *
	 * @throws ScannerException if confirmation fails.
	 */
	public void confirmEndExp() throws ScannerException;

	/**
	 * Confirm end of command.
	 *
	 * @throws ScannerException if confirmation fails.
	 */
	public void confirmEndCmd() throws ScannerException;

	/**
	 * Convenience method to confirm a kind.
	 *
	 * @throws ScannerException if confirmation fails.
	 */
	public void confirmKind() throws ScannerException;

	/**
	 * Convenience method to confirm a variable.
	 *
	 * @throws ScannerException if confirmation fails.
	 */
	public void confirmVar() throws ScannerException;

	/**
	 * Convenience method to confirm a term.
	 *
	 * @throws ScannerException if confirmation fails.
	 */
	public void confirmTerm() throws ScannerException;

	/**
	 * Convenience method to confirm a definition.
	 *
	 * @throws ScannerException if confirmation fails.
	 */
	public void confirmDef() throws ScannerException;

	/**
	 * Convenience method to confirm a {@link Functor}.
	 * Will call {@link #confirmTerm} or {@link #confirmDef} depending on
	 * whether the provided functor is a term or a definition.
	 *
	 * @param functor functor to confirm.
	 *
	 * @throws ScannerException if confirmation fails.
	 */
	public void confirmFunctor(Functor functor) throws ScannerException;

	/**
	 * Convenience method to confirm a {@link jhilbert.data.Statement}.
	 *
	 * @throws ScannerException if confirmation fails.
	 */
	public void confirmStatement() throws ScannerException;

	/**
	 * Convenience method to confirm a label.
	 *
	 * @throws ScannerException if confirmation fails.
	 */
	public void confirmLabel() throws ScannerException;

	/**
	 * Convenience method to confirm a parameter.
	 *
	 * @throws ScannerException if confirmation fails.
	 */
	public void confirmParameter() throws ScannerException;

	/**
	 * Convenience method to confirm a locator.
	 *
	 * @throws ScannerException if confirmation fails.
	 */
	public void confirmLocator() throws ScannerException;

	/**
	 * Convenience method to confirm a string.
	 *
	 * @throws ScannerException if confirmation fails.
	 */
	public void confirmString() throws ScannerException;

} public interface Verifier {

	/**
	 * Verifies the proof with respect to the specified disjoint variable
	 * constraints and hypotheses.
	 * Succeeds if the proof is correct and its final outcome is compatible
	 * with the specified consequent.
	 *
	 * @param dvConstraints DV constraints. If necessary, the verifier will
	 * 	restrict the constraints.
	 * @param hypotheses the labelled hypotheses.
	 * @param consequent the consequent.
	 *
	 * @throws VerifyException if the proof does not verify.
	 */
	public void verify(DVConstraints dvConstraints, Map<String, Expression> hypotheses, Expression consequent)
	throws VerifyException;

} public class VerifyException extends JHilbertException {

	/**
	 * Creates a new <code>VerifyException</code> with the specified detail
	 * message.
	 *
	 * @param message detail message.
	 */
	public VerifyException(final String message) {
		this(message, null);
	}

	/**
	 * Creates a new <code>VerifyException</code> with the specified detail
	 * message and cause.
	 *
	 * @param message detail message.
	 * @param cause the cause.
	 */
	public VerifyException(final String message, final Throwable cause) {
		super(message, cause);
	}

}
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.Stack;
import jhilbert.data.ConstraintException;
import jhilbert.data.DVConstraints;
import jhilbert.data.DataFactory;
import jhilbert.data.Kind;
import jhilbert.data.Module;
import jhilbert.data.Namespace;
import jhilbert.data.Statement;
import jhilbert.data.Symbol;
import jhilbert.data.Variable;
import jhilbert.expressions.Expression;
import jhilbert.expressions.ExpressionException;
import jhilbert.expressions.ExpressionFactory;
import jhilbert.expressions.Matcher;
import jhilbert.expressions.Substituter;
import jhilbert.expressions.UnifyException;
import jhilbert.scanners.ScannerException;
import jhilbert.scanners.Token;
import jhilbert.scanners.TokenFeed;
import jhilbert.verifier.Verifier;
import jhilbert.verifier.VerifyException;
import org.apache.log4j.Logger;
/*
    JHilbert, a verifier for collaborative theorem proving

    Copyright © 2008, 2009, 2011 The JHilbert Authors
      See the AUTHORS file for the list of JHilbert authors.
      See the commit logs ("git log") for a list of individual contributions.

    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <http://www.gnu.org/licenses/>.

    You may contact the author on this Wiki page:
    http://www.wikiproofs.de/w/index.php?title=User_talk:GrafZahl
*/

package jhilbert.verifier.impl;




/**
 * {@link Verifier} implementation.
 */
final class VerifierImpl implements Verifier {

	/**
	 * Logger for this class.
	 */
	private static final Logger logger = Logger.getLogger(VerifierImpl.class);

	/**
	 * Data module.
	 */
	private final Module module;