TypeChecker (API documentation of hlt.language packages)
Date: 2013-01-30

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 `Goal`s 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 `GlobalTypingGoal`s.

  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`