proof.type
Class ExistBinding

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

All Implemented Interfaces:

java.io.Serializable, Term

public class ExistBinding

extends Context

An existentially bound variable (a "hole" in a Term.)

See Also:

Serialized Form

Field Summary

Context

localContext The "local context", which contains UnivBindings variables which may be used to inhabit this term.

Fields inherited from class proof.type.Context

level, parent

Fields inherited from class proof.term.Var

name

Constructor Summary

ExistBinding(java.lang.String name, Context parent, Term type)
Constructor, extending a previous Context.

ExistBinding(java.lang.String name, Context parent, Term type, Context localContext)

Method Summary

java.lang.String	contextToString() Format this as a String.
Term	getType() Read-only access to the type of this variable.
int	numberOfHoles() This counts as a hole in the Context.
Context	substituteIntoContext(Var x, Context c, Term s) Substitute into this Binding.
java.lang.String	toString() Print this as a question mark, followed by the variable name.
boolean	wellTypedUsingConstraints() This is well-formed using the constraints if it's a valid type in its parent Context.

Methods inherited from class proof.type.Context

headReduceContextOnce, wellFormedUsingConstraints

Methods inherited from class proof.term.Var

alphaEquals, headReduceOnce, substitute

Methods inherited from class java.lang.Object

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

Field Detail

localContext

public Context localContext

The "local context", which contains UnivBindings variables which may be used to inhabit this term. When this ExistBinding is substituted into, this is "inherited" from the parent Context. FIXME: there are a bunch of ugly hacks associated with this

Constructor Detail

ExistBinding

public ExistBinding(java.lang.String name,
                    Context parent,
                    Term type)

Constructor, extending a previous Context.

Parameters:

name - the name of the variable being bound here

parent - the Context we're extending

type - the type of this existential variable

ExistBinding

public ExistBinding(java.lang.String name,
                    Context parent,
                    Term type,
                    Context localContext)

Method Detail

substituteIntoContext

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

Substitute into this Binding. Probably will only be used by the proof-synthesis routines.

Overrides:

substituteIntoContext in class Context

Following copied from class: proof.type.Context

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

getType

public Term getType()

Read-only access to the type of this variable.

Returns:

the type of this binding

toString

public java.lang.String toString()

Print this as a question mark, followed by the variable name.

Overrides:

toString in class Var

wellTypedUsingConstraints

public boolean wellTypedUsingConstraints()

This is well-formed using the constraints if it's a valid type in its parent Context.

numberOfHoles

public int numberOfHoles()

This counts as a hole in the Context.

Overrides:

numberOfHoles in class Context

contextToString

public java.lang.String contextToString()

Format this as a String.

Overrides:

contextToString in class Context