proof.type
Class Typechecker

java.lang.Object
  |
  +--proof.type.Typechecker

public class Typechecker

extends java.lang.Object

Typechecks a term.

Constructor Summary

Typechecker()
Constructor.

Method Summary

boolean	betaConvertable(Term x, Term y) Checks if two terms are beta-convertable.
Term	normalise(Term x) Reduces a term to normal form.
Term	reduceToPiOnOutside(Term x) Reduces a term until it has a pi-abstraction on the outside, if possible.
Term	reduceToSigmaOnOutside(Term x) Reduces a term until it has a sigma-type on the outside, if possible.
Term	typeOf(Context c, Term x) Finds the type of some Term, not using the constraints.
Term	typeOf(Context c, Term x, boolean usingConstraints) Finds the type of some Term, possibly using the constraints XXX We use "instanceof" a lot here, which is ugly.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Typechecker

public Typechecker()

Constructor.

Method Detail

typeOf

public Term typeOf(Context c,
                   Term x)
            throws TypecheckFailedException

Finds the type of some Term, not using the constraints.

Parameters:

c - the Context in which to typecheck the term

x - the Term to typecheck

typeOf

public Term typeOf(Context c,
                   Term x,
                   boolean usingConstraints)
            throws TypecheckFailedException

Finds the type of some Term, possibly using the constraints XXX We use "instanceof" a lot here, which is ugly.

Parameters:

c - the Context in which to typecheck the term

x - the Term to typecheck

usingConstraints - whether type constraints should be assumed to be correct. This should be false for regular type-checking, and true during some parts of proof search.

betaConvertable

public boolean betaConvertable(Term x,
                               Term y)

Checks if two terms are beta-convertable. Assumes they've both been typechecked already. For now, it just reduces both to normal form.

Parameters:

x, - y the terms to compare

Returns:

true iff x and y have the same normal form.

normalise

public Term normalise(Term x)

Reduces a term to normal form.

Parameters:

x - the term in question

reduceToPiOnOutside

public Term reduceToPiOnOutside(Term x)

Reduces a term until it has a pi-abstraction on the outside, if possible. (If not, it just reduces it to normal form.)

Parameters:

x - the term in question

Returns:

x, reduced to having a pi abstraction on the outside

reduceToSigmaOnOutside

public Term reduceToSigmaOnOutside(Term x)

Reduces a term until it has a sigma-type on the outside, if possible. (If not, it just reduces it to normal form.)

Parameters:

x - the term in question

Returns:

x, reduced to having a sigma-type on the outside