A B C D E F G H I L M N P R S T U V W X _

A

a - Variable in class proof.term.Pair

The two components of the pair.

A - Variable in class proof.term.Sigma

The types of the components.

Abstr - class proof.term.Abstr.

A lambda abstraction.

Abstr(Var, Term, Term) - Constructor for class proof.term.Abstr

Constructor.

action_obj - Variable in class proof.parse.parser

Instance of action encapsulation class.

action_table() - Method in class proof.parse.parser

Access to parse-action table.

actionPerformed(ActionEvent) - Method in class proof.prove.ProverApplet

actionPerformed(ActionEvent) - Method in class proof.type.TypecheckerTestApplet

alphaEquals(Term) - Method in class proof.term.Abstr

alphaEquals(Term) - Method in class proof.term.Appl

alphaEquals(Term) - Method in class proof.term.EmptyRecord

alphaEquals(Term) - Method in class proof.term.EmptyRecordType

alphaEquals(Term) - Method in class proof.term.Field

alphaEquals(Term) - Method in class proof.term.Pair

alphaEquals(Term) - Method in class proof.term.Pi

alphaEquals(Term) - Method in class proof.term.Sigma

alphaEquals(Term) - Method in class proof.term.Sort

alphaEquals(Term) - Method in interface proof.term.Term

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

alphaEquals(Term) - Method in class proof.term.Var

Appl - class proof.term.Appl.

An application term.

Appl(Term, Term) - Constructor for class proof.term.Appl

Constructor.

ARROW - Static variable in class proof.parse.sym

B

b - Variable in class proof.term.Pair

The two components of the pair.

B - Variable in class proof.term.Sigma

The types of the components.

BACKSLASH - Static variable in class proof.parse.sym

BANG - Static variable in class proof.parse.sym

betaConvertable(Term, Term) - Method in class proof.type.Typechecker

Checks if two terms are beta-convertable.

BOX - Static variable in class proof.parse.sym

BOX - Static variable in class proof.term.Sort

C

COLON - Static variable in class proof.parse.sym

Context - class proof.type.Context.

A generic part of a Context, which is implemented as a linked list for efficient sharing.

Context() - Constructor for class proof.type.Context

Constructs an empty Context.

Context(String, Context) - Constructor for class proof.type.Context

Constructor, extending a previous Context.

contextToString() - Method in class proof.type.Context

Format this Context as a String.

contextToString() - Method in class proof.type.ExistBinding

Format this as a String.

contextToString() - Method in class proof.type.UnivBinding

Format this as a String.

D

declare(String) - Method in class proof.parse.SymbolTable

Declare a variable, creating a new Var object with the given name.

declare(Var) - Method in class proof.parse.SymbolTable

Declare a variable, which already is a Var object.

do_action(int, lr_parser, Stack, int) - Method in class proof.parse.parser

Invoke a user supplied parse action.

DOT - Static variable in class proof.parse.sym

DOTSPACE - Static variable in class proof.parse.sym

E

EmptyRecord - class proof.term.EmptyRecord.

An empty record.

EmptyRecord() - Constructor for class proof.term.EmptyRecord

Constructor.

EmptyRecordType - class proof.term.EmptyRecordType.

The type of the empty record.

EmptyRecordType() - Constructor for class proof.term.EmptyRecordType

Constructor.

EOF - Static variable in class proof.parse.sym

EOF_sym() - Method in class proof.parse.parser

EOF Symbol index.

EQUALS - Static variable in class proof.parse.sym

error - Static variable in class proof.parse.sym

error_sym() - Method in class proof.parse.parser

error Symbol index.

ExistBinding - class proof.type.ExistBinding.

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

ExistBinding(String, Context, Term) - Constructor for class proof.type.ExistBinding

Constructor, extending a previous Context.

ExistBinding(String, Context, Term, Context) - Constructor for class proof.type.ExistBinding

expand() - Method in class proof.type.Goal

Expand this subgoal, finding subgoals which would prove it.

expand() - Method in class proof.type.GoalNew

Expand this subgoal, finding subgoals which would prove it.

expandToDepth(int) - Method in class proof.type.Goal

Expand this Goal to some depth.

expandToDepth(int) - Method in class proof.type.GoalNew

Expand this Goal to some depth.

expandToDepth(int) - Method in class proof.type.Step

Expand the subgoal to some depth.

expandToDepth(int, int) - Method in class proof.type.Goal

Expand this Goal to some depth, with a bound on the number of holes in the Goal.

expandToDepth(int, int) - Method in class proof.type.GoalNew

Expand this Goal to some depth, with a bound on the number of holes in the Goal.

EXTERN - Static variable in class proof.term.Sort

F

Field - class proof.term.Field.

A field selector; selects a component of a record.

Field(Term, String) - Constructor for class proof.term.Field

Constructor.

G

getProofTerm(Term) - Method in class proof.type.Goal

Looks for a completed proof in subgoals.

getProofTerm(Term) - Method in class proof.type.GoalNew

Looks for a completed proof in subgoals.

getProofTerm(Term) - Method in class proof.type.Step

Get the proof of the goal, if possible.

getType() - Method in class proof.type.ExistBinding

Read-only access to the type of this variable.

getType() - Method in class proof.type.UnivBinding

Read-only access to the type of this binding.

Goal - class proof.type.Goal.

A goal to be proved.

Goal(Context) - Constructor for class proof.type.Goal

Constructor.

GoalNew - class proof.type.GoalNew.

A goal to be proved.

GoalNew(Context) - Constructor for class proof.type.GoalNew

Constructor.

H

headReduceContextOnce() - Method in class proof.type.Context

Head-reduce everything in this Context once.

headReduceOnce() - Method in class proof.term.Abstr

To reduce this, reduce inside the term's body.

headReduceOnce() - Method in class proof.term.Appl

The interesting case for headReduceOnce.

headReduceOnce() - Method in class proof.term.EmptyRecord

...

headReduceOnce() - Method in class proof.term.EmptyRecordType

...

headReduceOnce() - Method in class proof.term.Field

headReduceOnce() - Method in class proof.term.Pair

To reduce this, reduce inside the two components.

headReduceOnce() - Method in class proof.term.Pi

To reduce this, reduce inside the term's body.

headReduceOnce() - Method in class proof.term.Sigma

To reduce this, reduce inside the two components.

headReduceOnce() - Method in class proof.term.Sort

...

headReduceOnce() - Method in interface proof.term.Term

Reduces this term once in lazy order.

headReduceOnce() - Method in class proof.term.Var

This variable doesn't have a value yet, so don't do anything to reduce it.

I

ID - Static variable in class proof.parse.sym

init_actions() - Method in class proof.parse.parser

Action encapsulation object initializer.

init() - Method in class proof.prove.ProverApplet

init() - Method in class proof.type.TypecheckerTestApplet

L

label - Variable in class proof.term.Field

The label of the field.

LCURLY - Static variable in class proof.parse.sym

level - Variable in class proof.type.Context

The level of this term in the context.

localContext - Variable in class proof.type.ExistBinding

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

lookup(String) - Method in class proof.parse.SymbolTable

Look up a variable.

LPAREN - Static variable in class proof.parse.sym

M

main(String[]) - Static method in class proof.prove.SimpleProverApp

First argument is the URL of the term to try to inhabit.

main(String[]) - Static method in class proof.type.TypecheckerApp

N

name - Variable in class proof.term.Var

The name of the variable.

normalise(Term) - Method in class proof.type.Typechecker

Reduces a term to normal form.

NUMBER - Static variable in class proof.parse.sym

numberOfHoles() - Method in class proof.type.Context

Counts the number of ExistBindings ("holes") in this Context.

numberOfHoles() - Method in class proof.type.ExistBinding

This counts as a hole in the Context.

numberOfHoles() - Method in class proof.type.UnivBinding

Counts the number of ExistBindings ("holes") in this Context.

P

Pair - class proof.term.Pair.

A (dependent) pair of terms, in which the second component may depend on the first component.

Pair(Var, Term, Term) - Constructor for class proof.term.Pair

Constructor.

parent - Variable in class proof.type.Context

The Context that this extends.

ParseOne - class proof.parse.ParseOne.

Parses a single file.

ParseOne(Reader) - Constructor for class proof.parse.ParseOne

Parses a file.

ParseOne(URL) - Constructor for class proof.parse.ParseOne

Reads a file from a given URL, and parses it.

parser - class proof.parse.parser.

CUP v0.10k generated parser.

parser() - Constructor for class proof.parse.parser

Default constructor.

parser(Scanner) - Constructor for class proof.parse.parser

Constructor which sets the default scanner.

Pi - class proof.term.Pi.

A Pi abstraction.

Pi(Var, Term, Term) - Constructor for class proof.term.Pi

Constructor.

PLUS - Static variable in class proof.parse.sym

POUND - Static variable in class proof.parse.sym

production_table() - Method in class proof.parse.parser

Access to production table.

ProverApplet - class proof.prove.ProverApplet.

Applet to try to find a term of a given type.

ProverApplet() - Constructor for class proof.prove.ProverApplet

R

rand - Variable in class proof.term.Appl

The argument.

rator - Variable in class proof.term.Appl

The term being applied.

RCURLY - Static variable in class proof.parse.sym

record - Variable in class proof.term.Field

The term we're taking a field of.

reduce_table() - Method in class proof.parse.parser

Access to reduce_goto table.

reduceToPiOnOutside(Term) - Method in class proof.type.Typechecker

Reduces a term until it has a pi-abstraction on the outside, if possible.

reduceToSigmaOnOutside(Term) - Method in class proof.type.Typechecker

Reduces a term until it has a sigma-type on the outside, if possible.

RPAREN - Static variable in class proof.parse.sym

S

s - Variable in class proof.term.Abstr

The body of the abstraction.

s - Variable in class proof.term.Pi

The body of the abstraction.

SEMI - Static variable in class proof.parse.sym

Sigma - class proof.term.Sigma.

A sigma type.

Sigma(Var, Term, Term) - Constructor for class proof.term.Sigma

Constructor.

SimpleProverApp - class proof.prove.SimpleProverApp.

Application which attempts to prove something in a fairly naive, brute-force way.

SimpleProverApp() - Constructor for class proof.prove.SimpleProverApp

sort - Variable in class proof.term.Sort

Which sort this is.

Sort - class proof.term.Sort.

A sort.

Sort(int) - Constructor for class proof.term.Sort

Constructor which expects Sort.STAR or Sort.BOX .

Sort(String) - Constructor for class proof.term.Sort

Constructor.

STAR - Static variable in class proof.term.Sort

Constants for the two sorts, plus the one used in proof search.

start_production() - Method in class proof.parse.parser

Indicates start production.

start_state() - Method in class proof.parse.parser

Indicates start state.

start() - Method in class proof.prove.ProverApplet

start() - Method in class proof.type.TypecheckerTestApplet

Step - class proof.type.Step.

One "step" in breaking down a proof, in which one hole gets substituted into (which may create other holes.)

Step(Context, ExistBinding, Context, Term) - Constructor for class proof.type.Step

Constructor.

STRING - Static variable in class proof.parse.sym

subgoals - Variable in class proof.type.Goal

Ways in which this subgoal could be proved.

subgoals - Variable in class proof.type.GoalNew

Ways in which this subgoal could be proved.

substitute(Var, Term) - Method in class proof.term.Abstr

Substitute into this term.

substitute(Var, Term) - Method in class proof.term.Appl

Substitute into this term.

substitute(Var, Term) - Method in class proof.term.EmptyRecord

Substituting into this does nothing...

substitute(Var, Term) - Method in class proof.term.EmptyRecordType

Substituting into this does nothing...

substitute(Var, Term) - Method in class proof.term.Field

To substitute into this, just substitute into the record.

substitute(Var, Term) - Method in class proof.term.Pair

Substitute into this term.

substitute(Var, Term) - Method in class proof.term.Pi

Substitute into this term.

substitute(Var, Term) - Method in class proof.term.Sigma

Substitute into this term.

substitute(Var, Term) - Method in class proof.term.Sort

Substituting into this does nothing...

substitute(Var, Term) - Method in interface proof.term.Term

Calculates the result of substituting into this term.

substitute(Var, Term) - Method in class proof.term.Var

Substitute into this term.

substituteIntoContext(Var, Context, Term) - Method in class proof.type.Context

Substitute into this Context.

substituteIntoContext(Var, Context, Term) - Method in class proof.type.ExistBinding

Substitute into this Binding.

substituteIntoContext(Var, Context, Term) - Method in class proof.type.UnivBinding

Substitute into this Context entry.

sym - class proof.parse.sym.

CUP generated class containing symbol constants.

sym() - Constructor for class proof.parse.sym

SymbolTable - class proof.parse.SymbolTable.

A simple symbol table, using a Hashtable, and Vectors for scoping.

SymbolTable() - Constructor for class proof.parse.SymbolTable

Constructor.

T

Term - interface proof.term.Term.

An attempt at implementing terms using references to handle variable binding.

termCache - Variable in class proof.parse.parser

Cache of Terms being loaded, indexed by URL.

TIMES - Static variable in class proof.parse.sym

toString() - Method in class proof.term.Abstr

Convert this to a String.

toString() - Method in class proof.term.Appl

Print this term as a String.

toString() - Method in class proof.term.EmptyRecord

Convert this term to a String.

toString() - Method in class proof.term.EmptyRecordType

Convert this term to a String.

toString() - Method in class proof.term.Field

toString() - Method in class proof.term.Pair

Convert this to a String.

toString() - Method in class proof.term.Pi

Convert this to a String.

toString() - Method in class proof.term.Sigma

Convert this to a String.

toString() - Method in class proof.term.Sort

Convert this term to a String.

toString() - Method in interface proof.term.Term

Convert this term to a string.

toString() - Method in class proof.term.Var

Convert this term to a String.

toString() - Method in class proof.type.ExistBinding

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

toStringWithoutBraces() - Method in class proof.term.Pair

Same as above, but leaves off the braces

toStringWithoutBraces() - Method in class proof.term.Sigma

Same as above, but leaves off the braces.

type - Variable in class proof.term.Abstr

The type of the variable.

type - Variable in class proof.term.Pi

The type of the variable.

Typechecker - class proof.type.Typechecker.

Typechecks a term.

Typechecker() - Constructor for class proof.type.Typechecker

Constructor.

TypecheckerApp - class proof.type.TypecheckerApp.

Application to run the type checker.

TypecheckerApp() - Constructor for class proof.type.TypecheckerApp

TypecheckerTestApplet - class proof.type.TypecheckerTestApplet.

Applet to test the type checker.

TypecheckerTestApplet() - Constructor for class proof.type.TypecheckerTestApplet

TypecheckFailedException - exception proof.type.TypecheckFailedException.

Exception indicating that something didn't typecheck.

TypecheckFailedException() - Constructor for class proof.type.TypecheckFailedException

TypecheckFailedException(String) - Constructor for class proof.type.TypecheckFailedException

Constructor, specifying an error message.

typeOf(Context, Term) - Method in class proof.type.Typechecker

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

typeOf(Context, Term, boolean) - Method in class proof.type.Typechecker

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

U

undeclare(String) - Method in class proof.parse.SymbolTable

"Undeclare" a variable, removing it from scope.

UnivBinding - class proof.type.UnivBinding.

Binds a variable in some Context.

UnivBinding(String, Context, Term) - Constructor for class proof.type.UnivBinding

Constructor for "making assumptions." (Note that it's protected, since this amounts to "adding an axiom.")

url - Variable in class proof.parse.parser

Base URL of this file, used so that relative URLs work.

USE - Static variable in class proof.parse.sym

V

value - Variable in class proof.parse.ParseOne

The value of the term that was parsed.

Var - class proof.term.Var.

A variable term.

Var() - Constructor for class proof.term.Var

Constructor for variables without a specific name.

Var(String) - Constructor for class proof.term.Var

Constructor.

W

wellFormedUsingConstraints() - Method in class proof.type.Context

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

wellTypedUsingConstraints() - Method in class proof.type.ExistBinding

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

wellTypedUsingConstraints() - Method in class proof.type.UnivBinding

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

X

x - Variable in class proof.term.Abstr

The bound variable.

x - Variable in class proof.term.Pair

The bound variable.

x - Variable in class proof.term.Pi

The bound variable.

x - Variable in class proof.term.Sigma

The bound variable.

_

_action_table - Static variable in class proof.parse.parser

Parse-action table.

_production_table - Static variable in class proof.parse.parser

Production table.

_reduce_table - Static variable in class proof.parse.parser

reduce_goto table.

A B C D E F G H I L M N P R S T U V W X _