proof.term
Class Field

java.lang.Object
  |
  +--proof.term.Field

All Implemented Interfaces:

java.io.Serializable, Term

public class Field

extends java.lang.Object

implements Term

A field selector; selects a component of a record.

See Also:

Serialized Form

Field Summary

java.lang.String	label The label of the field.
Term	record The term we're taking a field of.

Constructor Summary

Field(Term record, java.lang.String label)
Constructor.

Method Summary

boolean	alphaEquals(Term t) Compares this term to another term, up to variable renaming.
Term	headReduceOnce() Reduces this term once in lazy order.
Term	substitute(Var y, Term t) To substitute into this, just substitute into the record.
java.lang.String	toString() Convert this term to a string.

Methods inherited from class java.lang.Object

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

Field Detail

record

public Term record

The term we're taking a field of.

label

public java.lang.String label

The label of the field.

Constructor Detail

Field

public Field(Term record,
             java.lang.String label)

Constructor.

Method Detail

substitute

public Term substitute(Var y,
                       Term t)

To substitute into this, just substitute into the record. XXX although this works, it shouldn't create so many new objects

Specified by:

substitute in interface Term

Following copied from interface: proof.term.Term

Parameters:

y - the Var to substitute in for

t - the term to substitute in.

Returns:

the result of substituting

headReduceOnce

public Term headReduceOnce()

Description copied from interface: Term

Reduces this term once in lazy order. This actually reduces more than that usually, so perhaps it should be renamed.

Specified by:

headReduceOnce in interface Term

Following copied from interface: proof.term.Term

Returns:

this term, reduced once

alphaEquals

public boolean alphaEquals(Term t)

Description copied from interface: Term

Compares this term to another term, up to variable renaming.

Specified by:

alphaEquals in interface Term

Following copied from interface: proof.term.Term

Parameters:

t - the term to compare this to

Returns:

true iff this and t are equal (ignoring the names of variables)

toString

public java.lang.String toString()

Description copied from interface: Term

Convert this term to a string. There's no guarantee that the resulting term will be parseable.

Specified by:

toString in interface Term

Overrides:

toString in class java.lang.Object