% Author: Olaf Chitil
% Created: 1.2.2002
% Last Update: 
  
\documentclass[12pt]{article}
\usepackage{pst-node}
\usepackage[a4paper]{geometry}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{alltt}
\usepackage{url}

%------------------------------------------------------------------------------

\newcommand{\As}{\text{\char64}}
\newcommand{\True}{\text{True}}
\newcommand{\False}{\text{False}}
\newcommand{\Fun}{\text{Fun}}
\newcommand{\Trace}{\text{Trace}}
\newcommand{\NmType}{\text{NmType}}
\newcommand{\SR}{\text{SR}}
\newcommand{\R}{\text{R}}
\newcommand{\Nm}{\text{Nm}}
\newcommand{\Ap}{\text{Ap}}
\newcommand{\Ind}{\text{Ind}}
\newcommand{\Root}{\text{Root}}
\newcommand{\Sat}{\text{Sat}}
\newcommand{\writeNm}{\text{mkNm}}
\newcommand{\writeAp}{\text{mkAp}}
\newcommand{\writeInd}{\text{mkInd}}
\newcommand{\writeSat}{\text{mkSat}}
\newcommand{\updateSat}{\text{updateSat}}
\newcommand{\Pruned}{\text{Pruned}}
\newcommand{\Hidden}{\text{Hidden}}
\newcommand{\lsem}{[\![}
\newcommand{\rsem}{]\!]}
\newcommand{\sem}[1]{\lsem#1\rsem}
\newcommand{\texp}[3]{\mathcal{E}\sem{#1}^{#2}_{#3}}
\newcommand{\tpat}[1]{\mathcal{P}\sem{#1}}
\newcommand{\tdecl}[2]{\mathcal{D}\sem{#1}_{#2}}
\newcommand{\talt}[2]{\mathcal{A}\sem{#1}_{#2}}
\newcommand{\name}[1]{\mathcal{N}\sem{#1}}
\newcommand{\arity}[1]{\text{arity}(#1)}
\newcommand{\rf}{r\!f}
\newcommand{\tf}{t\!f}
\newcommand{\T}{\text{T}}
\newcommand{\Pointer}{\text{FilePointer}}
\newcommand{\seq}{\text{seq}}

\newenvironment{code}{\begin{quote}\begin{math}\begin{array}{@{}l}}{\end{array}\end{math}\end{quote}}

\newenvironment{block}{\begin{array}[t]{@{}l}}{\end{array}}

%------------------------------------------------------------------------------

\begin{document}
\thispagestyle{empty}

\title{ART Memo 36 (Version 0)\\The Implementation of Hat-Trans} 
\author{Olaf Chitil}
\date{March 19, 2002}
\maketitle

%------------------------------------------------------------------------------

\begin{abstract}
Hat-trans is the tool that transforms a Haskell module into another Haskell module that writes a trace file besides its normal operation. For this purpose the transformed Haskell module uses a library of combinators, Hat.hs/hat.c. Furthermore the Prelude and some primitive libraries are handled specially.
Here we describe the design of all these parts the ideas behind them.
(well, this version is a start)
\end{abstract}

%------------------------------------------------------------------------------

\section{Hat-trans}

The program hat-trans was built from the front end of nhc98. It consists of the following parts which are sequentially composed:

\begin{enumerate}
\item Process command line arguments.
\item Lexical analysis.
\item Parser.
\item If building the prelude, then strip of Prelude qualifiers.
\item If necessary, then add implicit import of Prelude.
\item Write .hx file.
\item Read .hx files of imported modules and annotate all identifiers in current module.
\item Transform module.
\item If building the prelude, then strip of TPrelude qualifiers.
\item Pretty print module.
\end{enumerate}

%------------------------------------------------------------------------------

\subsection{Records --- Labelled fields}

Labelled fields introduce a lot of syntactic sugar that needs to be handled by the transformation.  
The transformation is designed to be as simple and produce as little code as possible. It reuses the labelled field mechanisms in the transformed code as far as possible.
Nonetheless wrapping and the necessity to construct traces still make the transformation of some operations with labelled fields complicated.

\subsubsection{The data type definition}

A data type with labelled field is transformed into a data type with the same fields being labelled. A field label gets a prefix that distinguishes it from other sorts of identifiers.

As a result we obtain pattern matching with field labels for free in the transformation. The field labels in patterns just need to be prefixed.

\subsubsection{Construction and Update using Field Labels}

Basically both operations need to be performed on wrapped expressions and the result needs to be wrapped and equipped with a trace that describes the result value and its history.

For construction the normal construction cannot be used, because it initialises non-mentioned fields with \texttt{undefined}, not the wrapped version of \texttt{undefined}. Hence we build the application of the data constructor to $n$ wrapped \texttt{undefined}, where $n$ is the arity of the data constructor. Construction can then be defined as update of this value.

Update unwraps the data type value and then applies the normal update operation.

The results of both operations are wrapped with a new overloaded operation \texttt{wrapVal}. An instance exists for every data type (because construction can be used for any data type). This operation pattern matches on the outermost data constructor and creates the appropriate trace. Hence the operation is strict in the value to be wrapped. It also takes a parent trace as argument. For construction the parent is the normal parent of the context. 

A construction is a value but an update expression is not. Hence \texttt{ulazySat} is used for the latter to have a trace for the unevaluated update expression as well.

For update the parent is constructed from the parent of the wrapped expression to be updated. To reduce code size a combinator \texttt{(u)update} is defined and used by the transformation. Currently update is registered like a \texttt{case} in the trace; in the future a new sort of trace node will be needed to register it properly, including the label names. 

The definition of \texttt{wrapVal} is not small, hence it is defined only once per type instead of the expression being repeated at every occurrence of a construction or update. When no or only few field label operations are used this is a bad choice. A class is used to make the transformation easier; it does not need to determine the type.

\subsubsection{Field labels as selectors}

The selector associated with a field label has type such as \texttt{T -> R Int}, a traced selector however needs type \texttt{SR -> Trace -> R (Fun T Int)}. The selector identifier is the field label with the prefix of a normal transformed function. 


\subsubsection{Runtime errors}

The selector and the update operation can yield runtime errors if the argument does not have the desired field(s). Because of our simple transformation these errors are not caught like a pattern match error. They need to be handled differently, like division by zero or Control-C.


%------------------------------------------------------------------------------

\subsection{Writing the Trace --- Untraced Code}

The trace is actually written by the C-functions in hat.c. These are accessed from Haskell via the foreign declarations in Hat.hs. The functions all have a prefix \texttt{mkT} or \texttt{mkNT}.

All the expressions of the original module are wrapped in the transformed module. The wrapper augments each expression with a trace that describes the expression and its computation history. The transformation introduces combinators that handle wrapped expressions. In particular these combinators replace function abstraction and application. The combinators are defined in Hat.hs.

A trace has a hiddeness attribute, i.e. it can be hidden or not. A hidden trace denotes that some information may have been lost because of untraced code. A hidden trace may not describe the expression that should be there, but an ancestor of it. A parent trace is passed to every called function (not to constants). In a call from untraced code this parent is always hidden, so that a test for hiddeness of a parent establishes whether the code was called from untraced code.

Transformed traced and untraced code differ only in so much that a few combinators are different. Untraced code uses \texttt{ufun?}, \texttt{uap?} and \texttt{ulazySat} instead of \texttt{fun?}, \texttt{ap?} and \texttt{lazySat}. All other combinators do not need to differ. They all construct wrapped expressions in a way that the trace part is only evaluated when needed. Only the three mentioned sorts of combinators need to plumb traces together in different ways and possibly force evaluation of a trace.

\begin{description}
\item[\texttt{fun}]
Build \texttt{Fun} data structure, so that function in innermost \texttt{Fun} performs evaluation. Outermost \texttt{R} has given \texttt{NmType} as trace, other \texttt{R}s have respective parent as trace.
\begin{description}
\item[traced]
If called from untraced code (= parent of innermost function hidden), then application for this function and arguments is created and used as parent.
\item[untraced]
The parent passed to innermost function is always made hidden.
\end{description}
\item[\texttt{ap}]
Unwraps and applies \texttt{Fun}s to each argument individually.
\begin{description}
\item[traced]
Creates the application in trace.
Tests for each partial application if it is already a redex. If it is, then creates application in trace for remaining application (pseudo-solution for oversaturated applications).
\item[untraced]
If it is the partial application of an untraced function (= result trace of partial application is hidden), then creates appropriate application in the trace (for each 1-ary application individually).
\end{description}
\end{description}

Only when untraced code calls untraced code neither the redex nor the result are recorded in the trace. In all other cases both are recorded. In traced code the caller records the redex. A call from untraced code to traced code is recorded by the \texttt{fun} combinator.

For every recorded redex its final value must be recorded (literal, constructor application or partial application).
\begin{description}
\item[traced code] records full rhss anyway.
\item[untraced code] Trace component of every wrapped expression is deferred record of its value (as far as evaluated) with hidden parent for unevaluated expressions and parents. This trace is only recorded when the trace component is forced.
\end{description}

The idea is that the untraced combinators never force evaluation and hence writing of the trace of a wrapped expression. Only the traced combinators force evaluation of traces. They also force evaluation of the trace of a call of an untraced function and the trace of its result.

Furthermore, if the trace of a wrapped expression is demanded, then it shall always be demanded before the expression itself is demanded, never afterwards. The implementation of the combinator \texttt{ulazySat} relies on that invariant. If it is broken, the combinator just returns the hidden parent as trace. This is, because it seems impossible to create a trace correctly after evaluation of the expression, because SATs can no longer be created in accordance with the runtime stack. But only SATs enable forward references which are needed for representing cyclic structures. Unfortunately the invariant of demand on trace and expression seems to be broken sometimes. However, this does not seem to be a problem in practise, no lack of information has yet been observed.

\begin{alltt}
lazySat :: R a -> Trace -> R a
lazySat x t = 
  let sat = mkTSatA t
  in mkR (mkTSatB sat `Prelude.seq` -- mark entering of evaluation
          case x of -- create trace for (unevaluated x/v)
            R v vt ->
              mkTSatC sat vt `Prelude.seq` -- set trace for evaluated v
              v) -- return value
       sat

ap1 :: SR -> Trace -> R (Fun a r) -> R a -> R r 

ap1 sr t (R (Fun rf) tf) a@(R _ at) = 
  let t' = mkTAp1 t tf at sr
  in  lazySat (rf t' a) t'

ap1 :: SR -> Trace -> R (Fun a (Fun b r)) -> R a -> R b -> R r 
ap2 sr t (R (Fun rf) tf) a@(R _ at) b@(R _ bt) = 
  let t' = mkTAp2 t tf at bt sr
  in  lazySat (pap1 sr t t' (rf t' a) b) t'

pap0 :: Trace -> R r -> R r
pap0 t e = e

pap1 :: SR -> Trace -> Trace -> R (Fun a r) -> R a -> R r
pap1 sr p t (R (Fun rf) tf) a =
  if t `sameAs` tf 
    then rf t a
    else case a of 
           R _ at ->
             let t' = mkTAp1 p tf at sr
             in  t' `Prelude.seq` eagerSat (rf t' a) t'

fun1 :: NmType -> (Trace -> R a -> R r) -> SR -> Trace 
     -> R (Fun a r)
fun1 nm rf sr t = 
  let tf = mkTNm t nm sr
  in R (Fun (\char92t a -> 
               if hidden t
                 then let t' = mkTAp1 t tf (trace a) mkNoSourceRef
                      in lazySat (rf t' a) t'
                 else rf t a))
       tf
\end{alltt}

\begin{alltt}
ulazySat :: R a -> Trace -> R a

ulazySat x h =
  let status = unsafePerformIO (newIORef (Hidden h))
  in status `seq`
     R (case unsafePerformIO (readIORef status) of
          Hidden _ -> 
            case x of 
              R rv tv -> unsafePerformIO (writeIORef status Eval) `seq` rv
          Sat sat -> mkTSatBLonely sat `seq` 
                     case x of 
                       R rv tv -> mkTSatCLonely sat tv `seq` rv)
       (case unsafePerformIO (readIORef status) of
          Hidden h -> let sat = mkTSatALonely h 
                      in unsafePerformIO (writeIORef status (Sat sat)) `seq` 
                         sat
          Eval -> h)
        
data Status = Hidden Trace  -- neither value nor trace yet demanded
            | Sat Trace     -- trace demanded, value not yet
            | Eval          -- value demanded, trace not      

uap1 :: SR -> Trace -> R (Fun a r) -> R a -> R r
uap1 sr h (R (Fun rf) tf) a = ulazySat
  (case rf h a of
     R rv tv -> R rv (if hidden tv 
                        then mkTAp1 h tf (trace a) sr
                        else tv))
  h

uap2 :: SR -> Trace -> R (Fun a (Fun b r)) -> R a -> R b -> R r
uap2 sr h f a b = ulazySat
  (case uap1 sr h f a of
     R (Fun rf) tf -> case rf h b of
                        R rv tv -> R rv
                          (if hidden tv
                            then mkTAp1 h tf (trace b) sr
                            else tv))
  h

ufun1 :: NmType -> (Trace -> R a -> R r) -> SR -> Trace -> R (Fun a r)
ufun1 nm rf sr t = R (Fun (\char92t a -> rf (mkTHidden t) a)) (mkTNm t nm sr)

ufun2 :: NmType -> (Trace -> R a -> R b -> R r) -> SR -> Trace
     -> R (Fun a (Fun b r))
ufun2 nm rf sr t =
  R (Fun (\char92t a ->
    R (Fun (\char92t b -> rf (mkTHidden t) a b))
      t))
    (mkTNm t nm sr)
\end{alltt}

%------------------------------------------------------------------------------

\end{document}
