% Author: Olaf Chitil
% Created: 10.1.2001
% 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 13 (Version 0)\\Portable File Archiving} 
\author{Olaf Chitil}
\date{\today}
\maketitle

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

\begin{abstract}
Here we propose a scheme for writing the redex trail into a file instead of constructing it in the heap. The scheme is based on redefining the Haskell combinators that build the redex trail and which are introduced by the redex trail transformation so that they write a file using unsafePerformIO.
\end{abstract}

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

\section{Goals}

\begin{itemize}
\item
Creation of the full redex trail for an arbitrary long computation. The traced program shall only use heap space proportional to the heap space used by the untraced program (aim: factor of 2). The only limit shall be the disk space.
\item
The redex trail can be used with various browsers.
\item
The redex trail can be viewed any time, it can be archived.
\item
The redex trail is portable. It can be viewed on any system that has a browser.
\item
The file archiving implementation is portable.
\item
The file archiving implementation requires limited effort.
\end{itemize}

Improved runtime is desirable, but it is unclear if the gain in reduced garbage collection time will offset the overhead of writing to a file.

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

\section{General Comments}


The implementation does not feature pruning, which does not make much sense in this setting anyway.

This version does not feature trusting. It seems quite easy to adapt the current trusting scheme to the file archiving version. Basically every Trace requires an additional boolean argument to indicate if it is being trusted (then recursively following a trace is no longer necessary for determining trustedness). However, the current trusting mechanism is not satisfactory and requires some rethinking. Also, for file archiving trusting may not be necessary. It may be more interesting to dynamically use trusting in the browser to reduce the amount of visible information.

The scheme is based on redefining the trail-building combinators that are introduced by the redex trail transformation.
Thus the transformation can be left unchanged, only the definition of these combinators has to be changed (except that in the Hat implementation the transformation sometimes handles traces directly instead of abstracting this work). Hence for the use of the transformation functions, the transformation itself, we refer to Memo 12 on the redex trail transformation.
The new definitions write trace nodes to file using unsafePerformIO.

Note that it is possible to avoid unsafePerformIO by wrapping every value into the IO data constructor, like
\begin{code}
\text{newtype}~\R~a = \R~(\text{IO}~(a,~\Trace))
\end{code}
However, that would require the transformation to handle evaluation order in pattern matching and for primitive functions explicitly. Such an implementation would be closer to a Haskell interpreter.

In the definitions of the transformation functions given in the following sections care has been taken to ensure that a trace knot is written to file at the same time (or even earlier) as it would be allocated on the heap otherwise. Basically a trace shall never be a thunk. The strictness in the definitions ensures that.

Note: seq has to refer to the untraced seq of the untraced prelude. In fact, the implicitly imported prelude should be untraced.


\subsection{Static Tables}

The tables of source references, identifiers and strings can be stored in a separate file as discussed in Memo 3. It may be easier for a first implementation to write this file every time a traced program is run.

\subsection{Output, interruption information}

The program output with its traces and error messages and an interruption point (Shall it be possible to resume an interrupted computation?) can also be handled as discussed in Memo 3. (It would be nice to obtain a usable trail file even when the traced program core dumps or hangs; but that does not seem to be achievable without efficiency loss.)
Note that a general scheme for handling any IO still has to be formulated (see also Memo 7 on the semantics of redex trails).

\subsection{Browsing Archived Redex Trails}

The discussion of Memo 3 applies as well. The best compromise is to have either a separate program or a separate part of the browser between the file and the browser, so that the browser can still use message-passing. However, this part is started by the browser, the user need not be aware of its existence.

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

\section{The Data Types}

\begin{code}
\text{data}~\R~a = \R~a~!\Trace
\end{code}

The wrapper is strict in the trace. This is already sensible for the heap redex trail version. For the file redex trail version it makes some definitions simpler, although using seq instead is possible.


\begin{code}
\text{type}~\Fun~a~b = \Trace \to \R~a \to \R~b
\end{code}
(unchanged)

\begin{code}
\text{newtype}~\Trace = \T~\Pointer
\end{code}

Records in the File:
\begin{quote}
\begin{tabular}{ll}
 \Ap~\Pointer~[\Pointer]~\SR & \text{size info needed for the list} \\
\Nm~\Pointer~\NmType~\SR & \text{both \NmType{} and \SR{} are pointers to static info}\\
\Ind~\Pointer~Pointer & \text{first has full history, second is creator} \\
\Sat~\Pointer & \text{only one argument which is updated} \\
\Root & \text{only needed once, could use pointer=0}
\end{tabular}
\end{quote}


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

\section{Writing to a File}

The IO file operations of the standard library are unsatisfactory, because they only support files of type String. The system may add return characters and do even more weird things to handle unicode characters. 

For the redex trail it is best to write bytes. We need to know (or fix) the size of a file position (4 bytes?) and know if a file starts with position 0 or 1.
(probably BinaryMode from the hslibs should be useable; I suppose Chars are then considered as bytes).


\subsection{The unsafe Operations}

writeTrail writes the bytes for a trace node to the trail, returning a pointer to this node.
writeTrailAt overwrites a given trace node at a given point.

\begin{code}
\text{trailFilename} :: \text{String}
\\[1ex]
\text{trailFilename} = "Program.trl" \quad \emph{needs to be set by runtime system}
\\[2ex]
\text{trailFileHandle} :: \text{FileHandle}
\\[1ex]
\text{trailFileHandle} = \text{unsafePerformIO}~\$~\text{openFile}~\text{trailFilename}~\text{WriteMode}
\\[2ex]
\text{trailFilePosition} :: \text{IORef}~\Pointer
\\[1ex]
\text{trailFilePosition} = \text{unsafePerformIO}~\$~\text{newIORef}~0
\\[2ex]
\text{writeTrail} :: [\text{Word8}] \to \Pointer
\\[1ex]
\text{writeTrail}~ws = \text{unsafePerformIO}~\$~\text{do}\\
\quad pos \leftarrow \text{readIORef}~\text{trailFilePosition} \\
\quad \text{mapM}~(\text{hPutWord8}~\text{trailFileHandle})~ws\\
\quad \text{writeIORef}~\text{trailFilePosition}~(pos + \text{length}~ws) \\
\quad \text{return}~pos
\\[2ex]
\text{writeTrailAt} :: \Pointer \to [\text{Word8}] \to ()
\\[1ex]
\text{writeTrailAt}~pos~ws = \text{unsafePerformIO}~\$~\text{do}\\
\quad \text{hSeek}~\text{trailFileHandle}~\text{AbsoluteSeek}~pos \\
\quad \text{mapM}~(\text{hPutWord8}~\text{trailFileHandle})~ws\\
\quad endPos \leftarrow \text{readIORef}~\text{trailFilePosition} \\
\quad \text{hSeek}~\text{trailFileHandle}~\text{AbsoluteSeek}~endPos \\
\end{code}

It is probably cheaper to keep track of the current file position in trailFilePosition instead of always making an operating system call.


\subsection{Creation of the Redex Trail}

\begin{code}
\writeAp :: \Trace \to [\Trace] \to \SR \to \Trace
\\[2ex]
\writeAp~t~ts~s = \T~\$~\text{writeTrail}~\$\\
\quad
1~\operatorname{:}~(\text{trace2Word8}~t)~\operatorname{++}~\text{int2Word8}~(\text{length}~ts)~\operatorname{++}~\text{concatMap}~\text{trace2Word8}~ts\\
\quad\operatorname{++}~\text{sr2Word8}~s
\\[2ex]
\writeNm :: \Trace \to \NmType \to \SR \to \Trace
\\[2ex]
\writeNm~t~nm~s = \T~\$~\text{writeTrail}~\$\\
\quad 2~\operatorname{:}~(\text{trace2Word8}~t)~\operatorname{++}~(\text{nm2Word8} nm)~\operatorname{++}~\text{sr2Word8}~s
\\[2ex]
\writeInd :: \Trace \to \Trace \to \Trace
\\[2ex]
\writeInd~t_1~t_2 = \T~\$~\text{writeTrail}~\$\\
\quad 3~\operatorname{:}~(\text{trace2Word8}~t_1)~\operatorname{++}~(\text{trace2Word8}~t_2)
\\[2ex]
\writeSat :: \Trace \to \Trace
\\[2ex]
\writeSat~t = \T~\$~\text{writeTrail}~\$\\
\quad 4~\operatorname{:}~(\text{trace2Word8}~t)
\end{code}

Saving updates of Sats in a separate file and processing this file after termination of the traced program is probably more efficient. However, a first version can simply update in the redex file directly.

The first argument of updateSat is the Sat that shall be updated and the second argument contains the new trace it shall point to. The function returns the second argument. Note that a Sat node is basically an indirection (different from the indirection node). 

\begin{code}
\updateSat :: \Trace \to \R~a \to \R~a
\\[2ex]
\updateSat~(\T~pos)~e\As(\R~r~rt) = \text{writeTrailAt}~(pos+1)~(\text{trace2Word8}~rt)~
`\seq`~e
\end{code}

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

\section{Transformation of a Pattern}

No transformation function used.

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

\section{Transformation of Expressions}


\subsection{Variable}

For projections:

\begin{code}
\text{indir} :: \text{Trace} \to \text{R}~a \to \text{R}~a 
\\[2ex]
\text{indir}~t~(\text{R}~v~t') = \text{R}~v~(\writeInd~t~t') 
\end{code}

\subsection{Data Constructor Application}


ToDo.

Apply data constructor to wrapped arguments and wrap it with a trace, an application node for the constructor application.

\begin{code}
\text{con}_i :: \text{SR} \to \text{Trace} \to 
(\text{R}~a_1 \to \ldots \to \text{R}~a_n \to b) \to \NmType \to 
\text{R}~a_1 \to \ldots \to \text{R}~a_n \to \text{R}~b
\\[2ex]
\text{con}_0~s~t~c~nm  = \text{R}~c~(\text{Nm}~t~nm~s) \\
\text{con}_i~s~t~c~nm~a_1\As(\text{R}~\_~t_1)~\ldots~a_i\As(\text{R}~\_~t_i)
 = \text{R}~(c~a_1~\ldots~a_i)~(\text{Ap}~t~[\text{Nm}~t~nm, t_1, \ldots, t_i]~s) 
\end{code}

Transform a function into a wrapped function with the given trace.
For $i > 0$:
\begin{code}
\text{cn}_i :: (a_1 \to \ldots \to a_i \to b) \to \Trace \to 
(a_1~`\Fun`~\ldots~`\Fun`~a_i~`\Fun`~b)
\\[2ex]
\text{cn}_i~f~t = t~`\seq`~(\text{R}~(\lambda t_1~a_1 \to \ldots
\text{R}~(\lambda t_i~a_i \to R~(f~a_1~\ldots~a_i)~t)~t\ldots)~t)
\end{code}

Create an application node.
\begin{code}
\text{pa}_i :: \SR \to \Trace \to \NmType \to \R~a_1 \to \ldots \to \R~a_i \to \Trace
\\[2ex]
\text{pa}_0~s~t~nm  = \Nm~t~nm~s \\
\text{pa}_i~s~t~nm~a_1\As(\R~\_~t_1)~\ldots~a_i\As(\R~\_~t_i) 
= \Ap~t~[\Nm~t~nm~s, t_1, \ldots, t_i]~s
\end{code}

\subsection{Other Application}

Except for some additional seqs there is nothing special here.

Because rap$_i$ only differs with respect to trusting from ap$_i$, here the functions are equal.

\begin{code}
\text{ap}_i :: \SR \to \Trace \to \R~(a_1~`\Fun`~\ldots~`\Fun`~a_i~`\Fun`~b)
\to \R~a_1 \to \ldots \to \R~a_i \to R~b 
\\[2ex]
\text{ap}_1~s~t~(\R~\rf~\tf)~a_1\As(\R~\_~t_1) =\\
\quad\text{let}~t' = \writeAp~t~[\tf, t_1]~s~\text{in}~
t'~`\seq`~\rf~t'~a_1
\\[2ex]
\text{ap}_i~s~t~(\R~\rf~\tf)~a_1\As(\R~\_~t_1)~\ldots~a_i\As(\R~\_~t_i) =\\
\quad\text{let}~t' = \writeAp~t~[\tf, t_1, \ldots, t_i]~s~\text{in}~
t'~`\seq`~\text{pap}_{i-1}~s~t'~(\rf~t'~a_1)~a_2~\ldots~a_i 
\end{code}


$i \geq 0$:
\begin{code}
\text{pap}_i :: \SR \to \Trace \to \R~(a_1~`\Fun`~\ldots~`\Fun`~a_i~`\Fun`~b)
\to \R~a_1 \to \ldots \to \R~a_i \to R~b 
\\[2ex]
\text{pap}_0~s~t~e = e
\\[2ex]
\text{pap}_i~s~t~(\R~\rf~\tf)~a_1\As(\R~\_~t_1)~\ldots~a_i\As(\R~\_~t_i) =\\
\quad\text{if}~t~`\text{sameAs}`~\tf\\
\quad\quad\text{then}~%
\text{pap}_{i-1}~s~t~(\rf~t~a_1)~a_2~\ldots~a_i \\
\quad\quad\text{else}~% 
\text{let}~t' = \writeAp~t~[\tf, t_1, \ldots, t_i]~s~\text{in}~
t'~`\seq`~\text{pap}_{i-1}~s~t'~(\rf~t'~a_1)~a_2~\ldots~a_i 
\end{code}


\subsection{Lambda Abstraction}


\begin{code}
\text{fun}_i :: \NmType \to (\Trace \to a_1 \to \ldots \to a_i \to b) 
\to SR \to \Trace \\
\phantom{\text{fun}_i :: }\to \R (a_1~`\Fun`~\ldots~`\Fun`~a_i~`\Fun`~b)
\\[2ex]
\text{fun}_0~nm~\rf~s~t = 
\begin{array}[t]{@{}l}
\text{let}~
\begin{array}[t]{@{}l}
t' = \Nm~t~nm~s\\
ts = \writeSat~t'
\R~r~rt = \text{enter}~nm~t'~\$~\updateSat~ts~\$~(\rf~t)
\end{array}\\
\text{in}~\R~r~ts
\end{array}
\\[2ex]
\text{fun}_i~nm~\rf~s~t = \\
\quad\R~
\begin{array}[t]{@{}l}
(\lambda t_1 a_1 \to \ldots 
\R~(\lambda t_i a_i \to 
\begin{array}[t]{@{}l}
\text{let}~ts = \writeSat~t_i\\
\phantom{let}~\R~r~rt = \text{enter}~nm~t_i~\$~\updateSat~ts~\$~(\rf~t_i~a_1~\ldots~a_i)\\
\text{in}~\R~r~ts)~t_{i-1}
\end{array}\\
\ldots t_1)\\
(\Nm~t~nm~s)
\end{array}
\end{code}

Note that updateSat is evaluated just after the application has been evaluated.


\subsection{Let Expression}


No transformation function used.


\subsection{Case Expression}

Only $\text{ap}_1$ and $\text{fun}_1$ used, if we ignore guards for the moment.

\subsection{If Expression}


\begin{code}
\text{tif} :: \SR \to \R~\text{Bool} \to (\Trace \to a) \to (\Trace \to a) \to \Trace \to a
\\[2ex]
\text{tif}~s~(\R~iv~it)~a_1~a_2~t =
\begin{block}
\text{let}~t' = \Ap~t~[\Nm~t~\text{NTIf}~s, it, t]~s \\
\text{in}~t'~`\seq`~\text{if}~iv~\text{then}~a_1~t'~\text{else}~a_2~t'
\end{block}
\end{code}


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

\section{Transformation of Declarations}

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

\end{document}
