% FILE. . . . . /home/hak/ngo/doc/hak/design/fourpanels.tex
% EDIT BY . . . Hassan Ait Kaci
% ON MACHINE. . Latitude314.Ilog.Fr
% STARTED ON. . Tue Jun 25 09:32:32 2002

% Last modified on Wed Dec 18 18:53:49 2002 by hak

\chapter{A four-panelled architecture}

\section{The Complete Kernel}

\subsection{Sanitizing}
\subsection{Type checking \vs\ inference}
\subsection{Compiling}


\newpage
\section{The Complete Type System}
\label{CompleteTypes}

\begin{flushleft}
\textbf{Class hierarchy of types in the package\\
\texttt{ilog.language.design.types}}
\end{flushleft}
\vskip-2.5cm
\rput{90}(.5\textwidth,-.5\textheight){
\setlength{\fboxsep}{10pt}%
\setlength{\shadowsize}{8pt}%
%\shadowbox{%
\begin{minipage}{\textheight}
\begin{center}

\ACNODE{Type}

\vskip1.7cm

\ACNODE{StaticType}
\hskip4em
\ACNODE{DynamicType}

\vskip1.7cm

\ACNODE{NamedType}
\hskip.5em
\CNODE{TypeParameter}
\hskip.5em
\ACNODE{ConstructedType}
\hskip3em
\ACNODE{ExtensionalType}
\hskip.5em
\ACNODE{IntensionalType}

\vskip1.7cm

\hskip.23\textheight
\CNODE{BoxableTypeConstant}
\hskip.5em
\CNODE{FunctionType}
\hskip.5em
\CNODE{TupleType}
\hskip.5em
\CNODE{ArrayType}
\hskip.5em
\ACNODE{CollectionType}

\vskip1.7cm

\hskip1.5em
\CNODE{TypeConstant}
\hskip.5em
\ACNODE{TypeTerm}
\hskip3.5em
\CNODE{NamedTupleType}
\hskip1.5em
\CNODE{SetType}
\hskip.5em
\CNODE{BagType}
\hskip.5em
\CNODE{ListType}

\vskip1.7cm

\CNODE{CollectionTypeConstant}
\hskip6em
\CNODE{ClassType}
\hskip2em
\CNODE{DefinedType}
\hskip.33\textheight\mbox{}

\end{center}
\end{minipage}

\Extends{StaticType}{Type}
\Extends{DynamicType}{Type}

\Extends{NamedType}{StaticType}
\Extends{ConstructedType}{StaticType}
\Extends{TypeParameter}{StaticType}

\Extends{ExtensionalType}{DynamicType}
\Extends{IntensionalType}{DynamicType}

\Extends{ArrayType}{ConstructedType}
\Extends{BoxableTypeConstant}{ConstructedType}
\Extends{CollectionType}{ConstructedType}
\Extends{FunctionType}{ConstructedType}
\Extends{TupleType}{ConstructedType}

\Extends{SetType}{CollectionType}
\Extends{BagType}{CollectionType}
\Extends{ListType}{CollectionType}

\Extends{TypeConstant}{NamedType}
\Extends{TypeTerm}{NamedType}

\Extends{NamedTupleType}{TupleType}

\Extends{CollectionTypeConstant}{TypeConstant}

\Extends{ClassType}{TypeTerm}
\Extends{DefinedType}{TypeTerm}
%}
}

\newpage


\subsection{The type prover}

\section{Structure of the \texttt{TypeChecker}}


An object of the class
\iPACK{\lPACK{\dPACK{\tPACK{\CLASS{TypeChecker}}}}} is a backtracking
prover that establishes various kinds of {\em goals}. The most common
goal kind established by a type checker is a {\em typing goal}---but
there are others.

A \texttt{TypingGoal} object is a pair consisting 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. Thus, a \texttt{TypeChecker} object maintains all the
necessary structures for undoing the effects that happened since the
last choice point. These effects are:

\begin{Enumerate}
\item  type variable binding,
\item function type currying,
\item  application expression currying.
\end{Enumerate}

In addition, it is also necessary to remember all \texttt{Goal} objects
that were proven since the last choice point in order to prove them anew
upon backtracking to an alternative choice. This is necessary because
the goals are spawned by calls to the \texttt{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. In order for this to
work, any choice points that were associated to these original goals
must also be recovered. To enable this, when a choice point is created
for a \texttt{Global} symbol, choices are linked in the reverse order
({\em i.e.}, ending in the original goal) to enable reinstating all
choices that were tried for this goal.

In order to coordinate type proving, a typechecker object is passed
to all type checking and unification methods as an argument in order
to record any effect in the appropriate trail.

To recapitulate, the structures of a \texttt{TypeChecker} object are:
\begin{Itemize}
\item  a {\em goal stack} containing {\em goal} objects (\eg,
     \texttt{TypingGoal}) that are yet to be proven;
\item  a {\em binding trail stack} containing type variables and boxing
     masks to reset to "unbound" upon backtracking;
\item  a {\em 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;
\item  an {\em 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;
\item  a {\em goal trail} containing \texttt{TypingGoal} objects that
     have been proven since the last choice point, and must be reproven
     upon backtracking;
\item  a {\em choice-point stack} whose entries consists of:
     \begin{Itemize}
     \item  a queue of \texttt{TypingGoalEntry} objects wherefrom to
          constructs new \texttt{TypingGoal} objects to try upon failure;
     \item  pointers to all trails up to which to undo effects.
     \end{Itemize}
\end{Itemize}



\subsection{The type constructs}
\subsection{Defining new types}


\section{The Basic Instruction Set}

\section{The Complete Backend}

\subsection{The \texttt{Runtime} class}
\subsection{The \texttt{RuntimeObject} class}
\subsection{The \texttt{DisplayManager} class}
\subsection{The \texttt{ErrorManager} class}

