proof.type
Class Context

java.lang.Object
  |
  +--proof.term.Var
        |
        +--proof.type.Context

All Implemented Interfaces:

java.io.Serializable, Term

Direct Known Subclasses:

ExistBinding, UnivBinding

public class Context

extends Var

A generic part of a Context, which is implemented as a linked list for efficient sharing. The base class also stands for an "empty Context", so that other things don't have to check for null parent pointers. This is somewhat odd.

See Also:

Serialized Form

Field Summary

protected int	level The level of this term in the context.
protected Context	parent The Context that this extends.

Fields inherited from class proof.term.Var

name

Constructor Summary

	Context() Constructs an empty Context.
protected	Context(java.lang.String name, Context parent) Constructor, extending a previous Context.

Method Summary

java.lang.String	contextToString() Format this Context as a String.
Context	headReduceContextOnce() Head-reduce everything in this Context once.
int	numberOfHoles() Counts the number of ExistBindings ("holes") in this Context.
protected Context	substituteIntoContext(Var x, Context c, Term s) Substitute into this Context.
boolean	wellFormedUsingConstraints() True iff this context is "well-formed using the constraints."

Methods inherited from class proof.term.Var

alphaEquals, headReduceOnce, substitute, toString

Methods inherited from class java.lang.Object

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

Field Detail

parent

protected Context parent

The Context that this extends.

level

protected int level

The level of this term in the context. This is used when we're comparing terms for beta-convertability. We can possibly just reduce the head of the term with the higher level. Now that I see how useful the depths are for lazily checking alpha-convertability, I start to wonder about using the de Bruijn nameless representation after all...

Constructor Detail

Context

public Context()

Constructs an empty Context.

Context

protected Context(java.lang.String name,
                  Context parent)

Constructor, extending a previous Context.

Parameters:

name - the name of the variable being bound here

parent - the Context we're extending

Method Detail

substituteIntoContext

protected Context substituteIntoContext(Var x,
                                        Context c,
                                        Term s)

Substitute into this Context. Note that this is different from substituting into a Term (only the proof-search stuff should need to use this routine.)

Parameters:

x - the variable to substitute in for

c - the Context to add to the left of that variable (it should extend the context that's to the left of x)

s - the Term to substitute in

headReduceContextOnce

public Context headReduceContextOnce()

Head-reduce everything in this Context once.

wellFormedUsingConstraints

public boolean wellFormedUsingConstraints()

True iff this context is "well-formed using the constraints."

numberOfHoles

public int numberOfHoles()

Counts the number of ExistBindings ("holes") in this Context. If this is zero, then there are no "holes" left, and this is a "success context."

contextToString

public java.lang.String contextToString()

Format this Context as a String.