hlt.language.design.types

Class TypeChecker

java.lang.Object

hlt.language.design.types.TypeChecker

All Implemented Interfaces:

GoalProver

public class TypeChecker
extends java.lang.Object
implements GoalProver

A TypeChecker is a backtracking prover that establishes Goal objects. The most common goal is a TypingGoal, and consists of an expression and a type. Proving a typing goal amounts to unifying its expression component's type with its type component. Such goals are spawned by the type checking method of expressions as per their type checking rules.

Some globally defined symbols having multiple types, it is necessary to keep choices of these and backtrack to alternative types upon failure. Therefore, a special goal is used to handle the typing of a Global: a GlobalTypingGoal. Thus, a TypeChecker object maintains all the necessary structures for undoing the effects that happened since the latest choice point. These effects are:

1. type variable binding,
2. function type currying,
3. application expression currying.

In addition, it is also necessary to remember all Goals that were proven since the latest choice point in order to prove them anew upon backtracking to an alternative choice. This is necessary because the goals are spawned by typeCheck method of expressions that may be exited long before a failure occurs. Then, all the original typing goals that were spawned in the mean time since the current choice point's goal must be reestablished. This is why we use a goal trail that remembers the sequence of goals that was spawned. In order for this to work, any choice points that were associated to these original goals must also be reinitialized. All this machinery (including choice point stack pushing and popping) is appropriately set up and managed as it should be by GlobalTypingGoals.

In order to maintain consistency of the effects of type checking, a typechecker object is passed as an argument to all goal proving as well as type unification methods to enable recording of any such effect in the appropriate trail. These effects may then be accordingly undone upon backtracking by unwinding the trails back to where the latest choice point indicates.

To recapitulate, the structures of a TypeChecker object are:

• a goal stack containing Goal objects that are yet to be proven;

• a binding trail stack containing type variables and boxing masks to reset to "unbound" upon backtracking;

• a function type currying trail containing 4-tuples of the form (function type, previous domains, previous range, previous boxing mask) for resetting the function type to the recorded domains, range, and mask upon backtracking;

• an application currying trail containing triples of the form (application type, previous function, previous arguments) for resetting the application to the recorded function and arguments upon backtracking;

• a goal trail containing Goal objects that have been proven since the last choice point, and must be reproven upon backtracking;

• a choice-point stack whose entries consists of ChoicePoint objects containing:
  • a queue of CodeEntry objects wherefrom to constructs new TypingGoal objects to try upon failure;
  • pointers to all trails up to which to undo effects (a TypingState).

Field Summary

Fields

Modifier and Type	Field and Description
static boolean	ALLOWS_POSITIONAL_NAMED_TUPLES This is a boolean switch to dis/allow unification of position vs. named tuple types; default is false.
static boolean	ALLOWS_UNIFYING_OPAQUE_TUPLES This is a boolean switch to dis/allow unification of opaquely defined tuple types against plain tuple types; default is false.
static boolean	GIVES_DETAILS This is a static boolean switch to make type clash errors give the actual incompatible types that it found.

Constructor Summary

Constructors

Constructor and Description
TypeChecker()

Method Summary

Methods

Modifier and Type	Method and Description
void	allTypes(Expression expression, java.util.AbstractList types) Performs an exhaustive type checking of the specifed expression, recording the types it finds in the specified list.
void	disallowVoid(Type type, Locatable extent, java.lang.Object info) Proves a residuated NoVoidTypeGoal for the specified type.
void	error(StaticSemanticsErrorException error)
void	error(StaticSemanticsErrorException error, Locatable locatable)
TypingState	getTypingState() Returns the current TypingState of this typechecker.
boolean	isTracing()
TypingState	popCutPoint() Pops and returns the latest typing state on the cut-point stack.
void	popExitable() Pops the latest exitable scope.
void	prove(Goal goal) Proves the specfied goal by pushing it on the goal stack and calling the _typecheck() method.
void	prune(Global global, Type filter, Locatable extent) Triggers the proving of a PruningGoal for the specified global an filtering type, and records the specified location extent into the goal.
void	pushCutPoint() Pushes the current typing state on the cut-point stack.
void	pushExitable(Scope scope) Pushes the specified exitable scope onto the exitable scope stack.
void	pushGoal(Goal goal) Pushes the specified goal on the goal stack.
void	remainingTypes(Expression expression, java.util.AbstractList types) Finds all remaining types for the specifed expression starting in the current typing state of this typechecker, recording the types it finds in the specified list.
void	reportError()
TypeChecker	reset() Puts this type checker in a "virginal" state (i.e., as if it had just been constructed).
void	residuate(Type type, Goal goal) Constructs and proves a residuation wrapper for the specified goal in the form of a ResiduatedGoal on which the specified type is added as a trigger.
void	setTracing(boolean flag)
void	toggleTrace()
void	trail(Application application, Expression function, Expression[] arguments) Pushes the specified four objects on the application trail (corresponding to the form of an application before being curryed).
void	trail(Bindable bindable) Pushes the specified Bindable object on the binding trail.
void	trail(Goal goal) Pushes the specified goal on the goal trail.
void	typeCheck(Expression expression, Type type) Proves a TypingGoal constructed with the specified expression and type.
void	undoCutPoint()
void	unify(Type t1, Type t2) Triggers the unification of the two specified types by proving a UnifyGoal constructed with the two types.
void	unify(Type t1, Type t2, Locatable extent) Triggers the unification of the two specified types by proving a UnifyGoal constructed with the two types and recording the specified location extent.

Methods inherited from class java.lang.Object

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

Field Detail

GIVES_DETAILS

public static boolean GIVES_DETAILS

This is a static boolean switch to make type clash errors give the actual incompatible types that it found. Due to backtracking over overloaded types, this information is often wrong, and so it is not reported when this flag is false (default).

ALLOWS_POSITIONAL_NAMED_TUPLES

public static boolean ALLOWS_POSITIONAL_NAMED_TUPLES

This is a boolean switch to dis/allow unification of position vs. named tuple types; default is false.

ALLOWS_UNIFYING_OPAQUE_TUPLES

public static boolean ALLOWS_UNIFYING_OPAQUE_TUPLES

This is a boolean switch to dis/allow unification of opaquely defined tuple types against plain tuple types; default is false.

Constructor Detail

TypeChecker

public TypeChecker()

Method Detail

isTracing

public final boolean isTracing()

setTracing

public final void setTracing(boolean flag)

toggleTrace

public final void toggleTrace()

pushGoal

public final void pushGoal(Goal goal)

Pushes the specified goal on the goal stack.

pushExitable

public final void pushExitable(Scope scope)

Pushes the specified exitable scope onto the exitable scope stack.

popExitable

public final void popExitable()

Pops the latest exitable scope.

pushCutPoint

public final void pushCutPoint()

Pushes the current typing state on the cut-point stack.

popCutPoint

public final TypingState popCutPoint()

Pops and returns the latest typing state on the cut-point stack.

trail

public final void trail(Bindable bindable)

Pushes the specified Bindable object on the binding trail.

Specified by:

trail in interface GoalProver

trail

public final void trail(Application application,
         Expression function,
         Expression[] arguments)

Pushes the specified four objects on the application trail (corresponding to the form of an application before being curryed).

trail

public final void trail(Goal goal)

Pushes the specified goal on the goal trail.

Specified by:

trail in interface GoalProver

unify

public final void unify(Type t1,
         Type t2)
                 throws TypingErrorException

Triggers the unification of the two specified types by proving a UnifyGoal constructed with the two types.

Throws:

TypingErrorException

unify

public final void unify(Type t1,
         Type t2,
         Locatable extent)
                 throws TypingErrorException

Triggers the unification of the two specified types by proving a UnifyGoal constructed with the two types and recording the specified location extent.

Throws:

TypingErrorException

typeCheck

public final void typeCheck(Expression expression,
             Type type)
                     throws TypingErrorException

Proves a TypingGoal constructed with the specified expression and type.

Throws:

TypingErrorException

prune

public final void prune(Global global,
         Type filter,
         Locatable extent)
                 throws TypingErrorException

Triggers the proving of a PruningGoal for the specified global an filtering type, and records the specified location extent into the goal.

Throws:

TypingErrorException

residuate

public final void residuate(Type type,
             Goal goal)
                     throws TypingErrorException

Constructs and proves a residuation wrapper for the specified goal in the form of a ResiduatedGoal on which the specified type is added as a trigger. Adding a type as a trigger on a residuated goal enables control of the goal's proving based on the type's state of instantiation: even though the prove method is called immediately after on this goal, the effective proving happens only when the triggering type becomes fully instantiated.

Throws:

TypingErrorException

disallowVoid

public final void disallowVoid(Type type,
                Locatable extent,
                java.lang.Object info)
                        throws TypingErrorException

Proves a residuated NoVoidTypeGoal for the specified type. In other words, this prevents the specified type from ever being instantiated to void. The specified extent locates the goal and the info is used to describe the specific reason for disallowing void.

Throws:

TypingErrorException

prove

public final void prove(Goal goal)
                 throws TypingErrorException

Proves the specfied goal by pushing it on the goal stack and calling the _typecheck() method.

Specified by:

prove in interface GoalProver

Throws:

TypingErrorException

allTypes

public final void allTypes(Expression expression,
            java.util.AbstractList types)

Performs an exhaustive type checking of the specifed expression, recording the types it finds in the specified list.

remainingTypes

public final void remainingTypes(Expression expression,
                  java.util.AbstractList types)

Finds all remaining types for the specifed expression starting in the current typing state of this typechecker, recording the types it finds in the specified list.

getTypingState

public final TypingState getTypingState()

Returns the current TypingState of this typechecker.

reset

public final TypeChecker reset()

Puts this type checker in a "virginal" state (i.e., as if it had just been constructed).

undoCutPoint

public final void undoCutPoint()

error

public final void error(StaticSemanticsErrorException error)
                 throws StaticSemanticsErrorException

Throws:

StaticSemanticsErrorException

error

public final void error(StaticSemanticsErrorException error,
         Locatable locatable)
                 throws StaticSemanticsErrorException

Throws:

StaticSemanticsErrorException

reportError

public final void reportError()
                       throws StaticSemanticsErrorException

Throws:

StaticSemanticsErrorException