% Author: Olaf Chitil
% Created: 14.8.2000
% 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{\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{\tgexp}[3]{\mathcal{G}\sem{#1}^{#2}_{#3}}
\newcommand{\trhs}[2]{\mathcal{R}\sem{#1}_{#2}}
\newcommand{\tpat}[1]{\mathcal{P}\sem{#1}}
\newcommand{\tdecl}[2]{\mathcal{D}\sem{#1}_{#2}}
\newcommand{\tfun}[1]{\mathcal{F}\sem{#1}}
\newcommand{\name}[1]{\mathcal{N}\sem{#1}}
\newcommand{\arity}[1]{\text{arity}(#1)}
\newcommand{\rf}{r\!f}
\newcommand{\tf}{t\!f}
\newcommand{\defs}{de\!f\!s}

\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 12 (Version 1)\\The Redex Trail Transformation} 
\author{Olaf Chitil}
\date{\today}
\maketitle

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

\begin{abstract}
Here we describe the transformation of a program into a program that computes its redex trail besides its normal result.
The description is very close to the actual implementation.
\end{abstract}

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

\section{General Comments}

Everywhere where a runtime error may occur (e.g. no matching pattern) a call to the function fail is inserted by the transformation. Also the standard function error is replaced by primError (in the prelude definition). primError outputs an error message and then connects to the browser. If an exception handler could catch these errors, then the introduction of fail and primError would be unnecessary. Note also that the current scheme would not work anymore if we added such exception handlers to the language.

The computation can only be interrupted by Control-C when a function is entered. The advantage is that the redex trail is in a well-defined state and that computation can be resumed. The latter would hardly be possible, if Control-C were caught by an exception handler.

The transformation assumes that a source reference of an expression is only the position where the expressions starts and hence some source references are equal, for example the source references of the expression $f x$ and the $f$ inside are equal. Source references that describe whole blocks would need to be handled with more care in the transformation.

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

\section{The Data Types}

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

\begin{code}
\text{type}~\Fun~a~b = \Trace \to \R~a \to \R~b
\end{code}
(In the future this should be introduced as a newtype, so that in types $\to$ can simply be replaced by Fun, even when applied to less than two types.)

\begin{align*}
\text{data}~\Trace & = \Ap~\Trace~[\Trace]~\SR \\
& ~\mid \Nm~\Trace~\NmType~\SR \\
& ~\mid \Ind~\Trace~\Trace\\
& ~\mid \Root\\
& ~\mid \Sat~\Trace~\Trace\\
& ~\mid \Pruned\\
& ~\mid \Hidden~\Trace
\end{align*}


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

\section{Trusting}

\begin{code}
\text{trust} :: \Trace \to \text{Bool}
\\[1ex]
\text{trust}~t = \text{trustFun}~t
\\[2ex]
\text{trusted} :: \Trace \to \Trace \to \text{Bool}
\\[1ex]
\text{trusted}~t~\tf = \text{trustFun}~\tf~\&\&~\text{trustFun}~t
\\[2ex]
\text{trustFun} :: \Trace \to \text{Bool}
\\[1ex]
\text{trustFun}~(\Ap~\_~(\tf:\_)~\_) = \text{trustFun}~\tf \\
\text{trustFun}~(\Nm~\_~(\text{NTTrusted}~\_)~\_) = \True \\
\text{trustFun}~(\Nm~\_~(\text{NTId}~\_)~\_) = \False \\
\text{trustFun}~(\Nm~\_~\text{NTLambda}~\_) = \False \quad 
\text{definitely wrong, should follow trace} \\
\text{trustFun}~(\Nm~t~\text{NTCase}~\_) = \text{trustFun}~t \\
\text{trustFun}~(\Nm~t~\text{NTIf}~\_) = \text{trustFun}~t \\
\text{trustFun}~(\Nm~t~\text{NTGuard}~\_) = \text{trustFun}~t \\
\text{trustFun}~(\Sat~t~\_) = \text{trustFun}~t \\
\text{trustFun}~(\Ind~\_~t) = \text{trustFun}~t \\
\text{trustFun}~(\Root) = \False \\
\text{trustFun}~(\Pruned) = \False \\
\text{trustFun}~(\Hidden~\_) = \True \\
\end{code}
The functions trust, trusted and trustFun are actually primitive C-function (to improve performance?). trusted also increases a reduction counter (but never the counter from calls of suspected functions from trusted functions, because this should not happen; but it certainly does for higher-order functions).

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

\section{Transformation of a Pattern}

\begin{align*}
\tpat{C~p_1~\ldots~p_i} & = \R~(C~\tpat{p_1}~\ldots~\tpat{p_i}) \\
\tpat{x} & = x \\
\tpat{\_} & = \_ \\
\tpat{x\As{}p} & = x\As{}\tpat{p} \\
\tpat{\sim{}p} & = \sim\tpat{p}
\end{align*}

String literals are transformed into lists of characters. Integer and Rational literals are wrapped by dummy functions which are removed after type checking.

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

\section{Transformation of Expressions}

The boolean argument states if the expression is in a non-projective context,
that is, it is False if the expression is the result of the function in whose rhs it appears (not simply the rhs because of the case and if construct).
It is used both for introduction of indirection nodes and for trusting.

Superscripts at expressions (e.g. $M^s$) are source references.

\subsection{Variable}

$x, x_1, \ldots$ are $\lambda$-bound variables.
$y, y_1, \ldots$ are let-bound variables.

\begin{align*}
\texp{x}{\True}{t} & = x \\
\texp{x}{\False}{t} & = \text{indir}~t~x \\
\texp{y^{s}}{}{t} & = y~s~t \\
\end{align*}

\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~(\text{Ind}~t~t') 
\end{code}

\subsection{Data Constructor Application}

\begin{align*}
\texp{(C~M_1 \ldots M_i)^s}{}{t} & =
\begin{cases}
\text{con}_i~s~t~C~\name{C}~\texp{M_1}{\True}{t} \ldots \texp{M_i}{\True}{t}
& \text{, if $\arity{C}=i$} 
\\
\text{pa}_i~C~\text{cn}_{\arity{C}-i}~s~t~\name{C}~\texp{M_1}{\True}{t} \ldots \texp{M_i}{\True}{t}
& \text{, otherwise} \\
\end{cases}
\end{align*}


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 :: (R~a_1 \to \ldots \to R~a_i \to b) \to \Trace \to 
(a_1~`\Fun`~\ldots~`\Fun`~a_i~`\Fun`~b)
\\[2ex]
\text{cn}_i~f~t = t~`\text{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 application node for function that is partially applied to i
arguments and transform partial application with given function.
\begin{code}
\text{pa}_i :: (\R~a_1 \to \ldots \to \R~a_i \to b) \to (b \to \Trace \to c) \to \SR \to \Trace \to \NmType\\
\quad \to \R~a_1 \to \ldots \to \R~a_i \to c
\\[2ex]  
\text{pa}_0~cn~c~s~t~nm  = cn~c~(\Nm~t~nm~s) \\
\text{pa}_i~cn~c~s~t~nm~a_1\As(\R~\_~t_1)~\ldots~a_i\As(\R~\_~t_i) \\
\quad = cn~(c~a_1 \ldots a_i)~(\Ap~t~[\Nm~t~nm~s, t_1, \ldots, t_i]~s)
\end{code}

\subsection{Other Application}

\begin{align*}
\texp{M~N_1~\ldots~N_i}{\True}{t} 
& = \text{ap}_i~s~t~\texp{M_1}{\True}{t}~\ldots~\texp{M_i}{\True}{t}
\\
\texp{M~N_1~\ldots~N_i}{\False}{t} 
& = \text{rap}_i~s~t~\texp{M_1}{\True}{t}~\ldots~\texp{M_i}{\True}{t}
\end{align*}

If a trusted function is applied in a trusted context, then the application is not registered in the trail. In that case ap$_i$ also marks the trace as hidden. In contrast, rap$_i$ does not do the latter. Is the trace already marked as hidden?

rap$_i$ is used within a projective context, otherwise ap$_i$ is used.

\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{if}~\text{trusted}~t~\tf\\
\quad\quad\text{then}~%
\text{let}~t' = \text{hidden}~t~\text{in}~t'~`\text{seq}`~\rf~t'~a_1 \\
\quad\quad\text{else}~% 
\text{let}~t' = \Ap~t~[\tf, t_1]~s~\text{in}~
\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{if}~\text{trusted}~t~\tf\\
\quad\quad\text{then}~%
\text{let}~t' = \text{hidden}~t~\text{in}~t'~`\text{seq}`~\text{pap}_{i-1}~s~t'~(\rf~t'~a_1)~a_2~\ldots~a_i \\
\quad\quad\text{else}~% 
\text{let}~t' = \Ap~t~[\tf, t_1, \ldots, t_i]~s~\text{in}~
\text{pap}_{i-1}~s~t'~(\rf~t'~a_1)~a_2~\ldots~a_i 
\\[2ex]
\text{hidden} :: \Trace \to \Trace
\\[2ex]
\text{hidden}~h\As(\Hidden~\_) = h
\\
\text{hidden}~t = \Hidden~t
\end{code}


\begin{code}
\text{rap}_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{rap}_1~s~t~(\R~\rf~\tf)~a_1\As(\R~\_~t_1) =\\
\quad\text{if}~\text{trusted}~t~\tf\\
\quad\quad\text{then}~%
\rf~t~a_1 \\
\quad\quad\text{else}~% 
\text{let}~t' = \Ap~t~[\tf, t_1]~s~\text{in}~
\rf~t'~a_1
\\[2ex]
\text{rap}_i~s~t~(\R~\rf~\tf)~a_1\As(\R~\_~t_1)~\ldots~a_i\As(\R~\_~t_i) =\\
\quad\text{if}~\text{trusted}~t~\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' = \Ap~t~[\tf, t_1, \ldots, t_i]~s~\text{in}~
\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' = \Ap~t~[\tf, t_1, \ldots, t_i]~s~\text{in}~
\text{pap}_{i-1}~s~t'~(\rf~t'~a_1)~a_2~\ldots~a_i 
\end{code}


\subsection{Lambda Abstraction}

\begin{gather*}
\texp{(\lambda x_1 \ldots x_i.M)^s}{}{t} = 
\text{fun}_i~\name{\lambda}~(\lambda t' x_1 \ldots x_n. \texp{M}{\False}{t'})~s~t
\end{gather*}

Actually the translated $\lambda$-abstraction uses a case-construct to test if the patterns match. Otherwise it calls a function that outputs an error message and directly connects to the browser.

\begin{code}
\text{fun}_i :: \NmType \to (\Trace \to \R~a_1 \to \ldots \to \R~a_i \to \R~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\\
\R~r~rt = \text{enter}~nm~t'~(\rf~t)
\end{array}\\
\text{in}~\R~r~(\Sat~t'~rt)
\end{array}
\\[2ex]
\text{fun}_i~nm~\rf~s~t = \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}~\R~r~rt = \text{enter}~nm~t_i~(\rf~t_i~a_1~\ldots~a_i)\\
\text{in}~\R~r~(\Sat~t_i~rt))~t_{i-1}
\end{array}\\
\ldots t_1)\\
(\Nm~t~nm~s)
\end{array}
\end{code}

The primitive C-function enter connects to the redex trail browser, if the user pressed Control-C, execution is in single-stepping mode, etc. Otherwise it just returns the third argument.


\subsection{Let Expression}

\begin{gather*}
\texp{\text{let}~\{ decl_1; \ldots; decl_i \}~\text{in}~M}{}{t}
= \text{let}~\{ \tdecl{decl_1}{t}; \ldots; \tdecl{decl_i}{t} \}~\text{in}~\texp{M}{\False}{t}
\end{gather*}


\subsection{Case Expression}

\begin{gather*}
\texp{(\text{case}~M~\text{of}~\{alt_1^{\to}; \ldots; alt_i^{\to} \})^s}{b}{t} = 
\text{ap}_1~s~t~(\text{fun}_1~\name{\text{case}}~(
\text{let}~f~ alts;~\defs~\text{in}~f)~s~t)~\texp{M}{b}{t}
\end{gather*}
where
\begin{gather*}
\quad (alts,\defs) = \tfun{alt_1^{=}, \ldots, alt_i^{=}}
\end{gather*}


\subsection{If Expression}

\begin{gather*}
\texp{\text{if}~M~\text{then}~N_1~\text{else}~N_2}{b}{t} =
\text{tif}~s~\texp{M}{b}{t}~(\lambda t' \to \texp{N_1}{\False}{t'})~
(\lambda t' \to \texp{N_2}{\False}{t'})~t
\end{gather*}

\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{if}~\text{trust}~t \\
\text{then}~\text{if}~iv~\text{then}~a_1~t~\text{else}~a_2~t \\
\text{else}~
\begin{block}
\text{let}~t' = \Ap~t~[\Nm~t~\name{\text{if}}~s, it, t]~s \\
\text{in}~\text{if}~iv~\text{then}~a_1~t'~\text{else}~a_2~t'
\end{block}
\end{block}
\end{code}


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

\section{Transformation of Declarations}

Bindings in class and instance definitions are basically function bindings. A few special cases are however treated specially.

\subsection{Function binding}

Let $i$ be the arity of the definition of the function $f$.

\begin{gather*}
\tdecl{f~alts}{} = 
\begin{block}
(f~s~t = \text{fun}_i~\name{f}~f'~s~t
~\text{where}~f'~alts';~\defs)\\
\text{where}\\
(alts',\defs) = \tfun{alts}
\end{block}
\end{gather*}


Transformation of binding alternatives:
\begin{gather*}
\tfun{~} = (t~\__1 \ldots \__i = \text{fail}~t,~)
\end{gather*}

\begin{gather*}
\tfun{p_1 \ldots p_i~=~M~\text{where}~decls; alts} =\\
\begin{block}
(t~\tpat{p_1}\ldots\tpat{p_i}~=~\texp{M}{\False}{t}~\text{where}~\tdecl{decls}{t}; alts',~\defs)\\
\text{where}\\
(alts',\defs) = \tfun{alts}
\end{block}
\end{gather*}

\begin{gather*}
\tfun{p_1 \ldots p_i~gdes~\text{where}~decls; alts} \\
\begin{block}
|~\text{guards in $gdes$ may fail and $alts$ not empty} =\\
\quad\begin{block}
(t~\tpat{a_1\As{}p_1}\ldots\tpat{a_1\As{}p_i}~=~\tgexp{gdes}{\lambda t. f~t~a_1 \ldots a_i}{t}~t~\text{where}~\tdecl{decls}{t} \\
;t~a_1 \ldots a_i = f~t~a_1 \ldots a_i,~f~alts';~\defs)\\
\text{where}\\
(alts',\defs) = \tfun{alts}
\end{block}\\
|~\text{otherwise} =\\
\quad\begin{block}
(t~\tpat{a_1\As{}p_1}\ldots\tpat{a_1\As{}p_i}~=~\tgexp{gdes}{\text{fail}}{t}~t~\text{where}~\tdecl{decls}{t};~alts',~\defs)\\
\text{where}
(alts',\defs) = \tfun{alts}
\end{block}
\end{block}
\end{gather*}


Transformation of guarded expressions:
\begin{gather*}
\tgexp{~}{F}{t} = \lambda t'.\,F~t'
\\
\tgexp{~|\,N^s~=~M; gdes}{F}{t} = \text{t\_guard}~s~\texp{N}{\False}{t}~(\lambda t'. \texp{M}{\False}{t'})~\tgexp{gdes}{F}{t}
\end{gather*}

Just as for if, except for the different name.
\begin{code}
\text{t\_guard} :: \SR \to \R~\text{Bool} \to (\Trace \to a) \to (\Trace \to a)\to \Trace \to a
\\[1ex]
\text{t\_guard}~s~(\R~gv~gt)~e~cont~t~= 
\begin{block}
\text{if}~\text{trust}~t\\
\text{then}~\text{if}~gv~\text{then}~e~t~\text{else}~cont~t\\
\text{else}~
\begin{block}
\text{let}~t'~=~\Ap~t~[\Nm~t~\name{\text{guard}}~s, gt, t]~ s \\
\text{in}~\text{if}~gv~\text{then}~e~t'~\text{else}~cont~t'
\end{block}
\end{block}
\end{code}

\subsection{Constant binding}

A constant binding is transformed like a nullary function binding, except that sharing is preserved and hence the parent relationship is rather useless.
The transformation is more simple, because a constant binding consists only of a single alternative.

\begin{gather*}
\tdecl{x^s~rhs~\text{where}~decls}{t} = 
\begin{block}
(x~\_~\_~=x'\\
;x' = \text{lazySat}~\trhs{rhs}{t'}~t'\\
\quad\begin{block}
\text{where}\\
t' = \Nm~t~\name{x}~s\\
\tdecl{decls}{t'})
\end{block}
\end{block}
\end{gather*}

Transform right hand side.
\begin{gather*}
\trhs{M}{t} = \texp{M}{\False}{t}
\\
\trhs{gdes}{t} = \tgexp{gdes}{\text{fail}}{t}~t
\end{gather*}

Assure that a trace component of wrapped value exists by construction of Sat.
Similar to fun$_0$.
\begin{code}
\text{lazySat} :: \R~a \to \Trace \to \R~a
\\[1ex]
\text{lazySat}~a~t~=~ 
  \text{let}~\R~v~vt~=~a~\text{in}~\R~v~(\Sat~t~vt)
\end{code}


\subsection{Pattern binding}

Unlike all other let-defined variables, variables defined through pattern bindings are not registered in the trace. A pattern binding adds no node to the trace which is bad in practise. Note that a pattern binding with just a variable on the left is actually a constant binding; hence the trace construction should actually be similar.

Let $x_1, \ldots, x_i$ be the variables occurring in the pattern $p$.

\begin{gather*}
\tdecl{p~rhs~\text{where}~decls}{t} =
\begin{block}
(y = \text{case}~\trhs{rhs}{t}~\text{of}~\tpat{p[\overline{x}'/\overline{x}]} \to (x'_1,\ldots,x'_i); \_ \to \text{fail}~t
\\
;x_1~\_~\_~=~\text{case}~y~\text{of}~(x'_1,\ldots,x'_i) \to x_1\\
\ldots\\
;x_i~\_~\_~=~\text{case}~y~\text{of}~(x'_1,\ldots,x'_i) \to x_i\\
)
\end{block}
\end{gather*}


\subsection{Foreign Functions}

A wrapper is created that unwraps and wraps traces of arguments and result and calls the actual foreign function.

$a$ is the arity of the function.

\begin{gather*}
\tdecl{(\text{foreign import}~cname~f~a~c~::~\tau)^s}{} =
\begin{block}
(\text{foreign import}~cname~f'~a~c~::~\tau\\
;f~s~t~=~\text{prim}_a~\name{f}~f'~s~t\\
)
\end{block}
\end{gather*}

\begin{code}
\text{prim}_i :: \text{NmCoerce}~c \Rightarrow \NmType \to (a_1 \to \ldots a_i \to r) \to \SR \to \Trace \to \\
\quad\quad\quad (a_1~`\Fun`\ldots`\Fun`a_i\to r) 
\\[1ex]
\text{prim}_i~nm~f~s~t~=~ 
\begin{block}
  \text{let}~t'~=~\Nm~t~nm~s\\
  \text{in}~
\begin{block}
  \R~(\lambda t_1~(\R~a_1~t_1) \to\\
\quad\ldots\\
\quad\quad \R~(\lambda t_i~(\R~a_i~t_i) \to\\
\quad\quad\quad\quad (\lambda (\R~v~vt) \to \R~v~(\Sat~t_i~vt))\\
\quad\quad\quad\quad (\text{primEnter}~s~nm~t_i~(f~a_1\ldots a_i)))\\
\quad\quad\ldots\\
\quad\quad t_1)\\
\quad t'
\end{block}
\end{block}
\end{code}

Counterpart to 'enter' for primitives: ensures that the result trace
is fully evaluated at exactly the same time as the result value.

\begin{code}
\text{primEnter}~::~\text{NmCoerce}~a~\Rightarrow~\SR~\to~\NmType~\to~\Trace~\to~a~\to~\R~a
\\[1ex]
\text{primEnter}~s~nm~t~e~=~
\begin{block}
\text{let}~
\begin{block}
v~=~\text{enter}~nm~t~e\\
vn~=~\text{toNm}~t~v~sr
\end{block}\\
\text{in}~v~`\text{myseq}`~vn
\end{block}
\end{code}

The wrapping function toNm is the method of the class NmCoerce.


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

\end{document}
