examples.tex

Section~\ref{sec:intro} showed how a single filter can collapse a
factorial trace to its key steps. We now use a richer example,
mapping a function over a list, to introduce the full set of filter
primitives and show how they compose.

Consider the Hazel program in \autoref{fig:hazel-map}, which applies a
\code{square} function to each element of the list \code{[1, 2, 3]}
using \code{map}. To understand how this program evaluates to
\code{[1, 4, 9]}, a user can invoke the Hazel stepper. The stepper
highlights every reducible expression (redex) in the program. The user
clicks on a highlighted redex to reduce it, and the expression is
rewritten in place. A history panel lets the user expand the full
sequence of steps taken so far. \autoref{fig:full-trace} shows the
partial trace for this program: each line corresponds to one
reduction step, and the green highlight at the bottom marks the
available redexes for the next step.

\begin{figure}
  \centering
  \begin{subfigure}[T]{0.40\linewidth}
    \frame{\includegraphics[scale=0.34]{images/eg11.png}}
    \Description{Hazel code defining a list map function, a square function, and a call to map over [1, 2, 3].}
    \caption{The map example. Evaluates to \code{[1, 4, 9]}.}
    \label{fig:hazel-map}
  \end{subfigure}
  \hfill
  \begin{subfigure}[T]{0.50\linewidth}
    \frame{\includegraphics[scale=0.37]{images/eg12.png}}
    \Description{Partial stepper trace for the map example, stopped at map([1, 2, 3], square), with highlighted next-step location and substitution annotations.}
    \caption{Partial stepper trace for the map example, stopped at \code{map([1, 2, 3], square)}. Each line is one small-step transition. The green highlight at the bottom marks where the next step will be taken.}
    \label{fig:full-trace}
  \end{subfigure}
  \caption{The stepper used on a list map example.}
\end{figure}

The factorial traces in \autoref{fig:intro-fac} illustrate why showing
every step can be distracting: routine substitutions and arithmetic
quickly obscure the reductions that matter. The partial trace in
\autoref{fig:full-trace} shows the same issue arising for \code{map}.
To address this, the Hazel stepper provides \emph{filter} annotations
that the user embeds in the program text to control which steps appear
in the trace.

Each filter takes a \emph{pattern} that selects expressions by
structure. Patterns use the same syntax as Hazel expressions, so
every Hazel expression is also a valid pattern. Two additional forms
are provided: \code{\$e}, which matches any expression, and
\code{\$v}, which matches any value. For example,
\code{map(\$v, \$v)} matches any application of \code{map} to two
values. We give the formal pattern-matching rules in
Section~\ref{sec:filter}. We provide four filter constructs:
\begin{itemize}
  \item \code{debug hide(\textit{pat})}: hide \emph{one} matching step.
  \item \code{debug stop(\textit{pat})}: show \emph{one} matching step.
  \item \code{debug eval(\textit{pat})}: hide \emph{all} evaluation steps for a matching sub-expression.
  \item \code{debug step(\textit{pat})}: show \emph{all} evaluation steps for a matching sub-expression.
\end{itemize}
The first two (\code{hide}/\code{stop}) affect a single step, while the
latter two (\code{eval}/\code{step}) affect the entire evaluation of a
matching sub-expression.

To illustrate, suppose we only want to see the recursive calls to
\code{map}. In \autoref{fig:hide-stop-map} we add two filters:
\code{debug hide(\$e)} hides every step, since \code{\$e} re-matches
at every instrumentation pass, and \code{debug stop(map(\$v, \$v))}
overrides the preceding hide to show any step taken from an
expression containing \code{map} applied to two values. Since
\code{debug stop} is the inner of the two filters, it takes
priority. The resulting trace (\autoref{fig:recursive-trace}) shows
only the recursive \code{map} calls.

\begin{figure}
  \centering
  \begin{subfigure}[T]{0.40\linewidth}
    \frame{\includegraphics[scale=0.4]{images/eg21.png}}
    \Description{Map example annotated with debug eval and debug stop filters to focus on recursive calls.}
    \caption{The code from \autoref{fig:hazel-map} with added \code{debug hide} and \code{debug stop} filters.}
    \label{fig:hide-stop-map}
  \end{subfigure}
  \hfill
  \begin{subfigure}[T]{0.50\linewidth}
    \frame{\includegraphics[scale=0.4]{images/eg22.png}}
    \Description{Filtered stepper output showing only recursive map calls and the resulting list [1, 4, 9].}
    \caption{Filtered trace. Each line shows one recursive \code{map} call: the list shrinks by one element while evaluated results accumulate on the left.}
    \label{fig:recursive-trace}
  \end{subfigure}
  \caption{A filtered stepper for showing recursive calls in the list map example.}
\end{figure}

Alternatively, we might want to see not just which recursive calls
\code{map} makes, but also how each application of \code{square}
evaluates. In \autoref{fig:debug-map} we add a \code{debug step}
filter to achieve this. The result (\autoref{fig:debug-trace}) now
includes not only the recursive \code{map} calls, but also the
intermediate multiplications inside each \code{square} call. For
instance, the third and sixth lines show \code{<square>(1)} and
\code{<square>(2)} being expanded into their constituent steps.

\begin{figure}
  \centering
  \begin{subfigure}[T]{0.40\linewidth}
    \frame{\includegraphics[scale=0.30]{images/eg31.png}}
    \Description{Map example with eval and step filters, including debug mode for square.}
    \caption{The code from \autoref{fig:hazel-map} with added \code{debug hide}, \code{debug stop}, and \code{debug step} filters.}
    \label{fig:debug-map}
  \end{subfigure}
  \hfill
  \begin{subfigure}[T]{0.56\linewidth}
    \frame{\includegraphics[scale=0.30]{images/eg32.png}}
    \Description{Filtered trace showing recursive map steps and explicit square evaluations on list elements.}
    \caption{Filtered trace with \code{debug step}: recursive \code{map} calls are visible (as before), and each \code{square} application is expanded to show its intermediate steps.}
    \label{fig:debug-trace}
  \end{subfigure}
  \caption{A filtered stepper that demonstrates debug mode.}
\end{figure}

Note that \code{debug step} here overrides the earlier \code{debug hide}
and \code{debug stop}. Intuitively, the innermost filter surrounding
the next reduction step takes priority, a form of lexical scoping.
In the next section, we formalize these filter primitives and their
interactions as the \emph{Filtered Stepper Calculus}.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:

% \subsection{Matching}

% Terms that has the same structural form after substituting all bounded variables
% are considered \emph{matched}.

% \begin{verbatim}
% let x = 3 in
% eval x + 3 in
% x + 3
% \end{verbatim}
% shall has the same behavior as the program
% \begin{verbatim}
% let x = 3 in
% eval 3 + 3 in
% 3 + 3
% \end{verbatim}

% \begin{verbatim}
% eval $e in
% let g = fun x -> x + x in
% pause g($v) in # or pause (fun x -> x + x)($v) in
% (fun x -> x + x)(3)
% == (fun x -> x + x)(3) # or g(3) #
% \end{verbatim}

% \begin{figure}[h]
%   \includegraphics[width=0.4\textwidth]{images/match-mod-subst.png}
% \end{figure}

% As in a substitution-based evaluator, the substitution is applied to the
% the body of a function:
% \begin{verbatim}
% eval $e in
% let y = fun x -> x in
% let h = fun x -> (fun y -> y) in
% pause (fun x -> y)($v) in
% h(3)
% == h(3) # or (fun x -> (fun x -> x))(3) #
% \end{verbatim}

% \begin{figure}[h]
%   \includegraphics[width=0.4\textwidth]{images/match-recursive.png}
% \end{figure}

% A immediate corollary of this is that the stepper filter shows that
% the filter cannot be applied to a variable, since the substitution is always
% performed ahead of the matching process, and for the filter it shall not be
% able to match against a variable.

% \begin{verbatim}
% eval $e in
% let x = 3 in
% pause x in
% x + x
% == 6
% \end{verbatim}

% % \TODO{Discuss: whether or not to use alpha-equivalence here.}

% \subsection{Four filters: Hide, Eval, Pause and Debug}

% % \TODO{Discuss: mention skip all, skip one, pause all and all one?}

% Typical use case for the four basic filters.

% \subsubsection{Eval}

% We want to use the \verb|eval| to \emph{evaluate} all sub-expressions that matches the pattern.
% \begin{verbatim}
% eval 1 + 2 in
% 1 + 2
% == 3
% \end{verbatim}

% \subsubsection{Hide}

% The \verb|hide| filter will be \emph{used up} when its body
% expression is actually being evaluated.

% \begin{verbatim}
% hide let   =   in   in
% let x = 3 in
% let y = 4 in
% x + y
% == 3 + 4
% == 7
% \end{verbatim}
% Compare with \verb|eval|
% \begin{verbatim}
% eval let   =   in   in
% let x = 3 in
% let y = 4 in
% x + y
% == 7
% \end{verbatim}

% \subsubsection{Pause}

% During evaluation, we want to be able to examine every instruction
% transitioning steps.

% \begin{verbatim}
% eval 1 + 2 + 3 + 4 in
% pause 3 + 3 in
% 1 + 2 + 3 + 4
% == 3 + 3 + 4
% == 10
% \end{verbatim}

% This would be especially useful when unfolding a higher level
% expression to its individual terms, for example I want to know how
% many terms of \verb|fib(1)| I need to call to evaluate the whole
% \verb|fib(5)|.

% \subsubsection{Debug}

% On the other hand, we want to went through all the evaluation process of a
% sub-expression, for example when debugging the implementation of a function
% \begin{verbatim}
% let (is_even: Int -> Bool, is_odd: Int -> Bool) = ... in
% debug is_odd($v) in
% is_even(5)
% \end{verbatim}

% The difference between \verb|pause| and \verb|debug| is subtle. For
% example, considering the following two piece of code:
% \begin{verbatim}
% eval $e in
% pause (1 + 2) + (3 + 4) + (5 + 6) in
% eval 3 + 7 + (5 + 6) in
% (1 + 2) + (3 + 4) + (5 + 6)
% == (1 + 2) + (3 + 4) + (5 + 6)
% == 21
% \end{verbatim}
% and
% \begin{verbatim}
% eval $e in
% debug (1 + 2) + (3 + 4) + (5 + 6) in
% eval 3 + 7 + (5 + 6) in
% (1 + 2) + (3 + 4) + (5 + 6)
% == (1 + 2) + (3 + 4) + (5 + 6)
% == 3 + (3 + 4) + (5 + 6)
% == 21
% \end{verbatim}
% The first one will immediately evaluate to final value is because it is a \verb|pause| statement, which will be only effective once.

% \subsection{Interaction between filter statements}

% % \TODO{Q: Do we need formalise these properties?}

% We want nested filter statements to behave correctly, i.e.
% \begin{enumerate}
% \item For every pattern \verb|p|, \verb|pause p| cancels the effects
%   of \verb|eval p| and \verb|hide p|, vice versa.
% \item Inner filter statements take precedences.
% \end{enumerate}

% \subsubsection{``Newer'' Expression overrides ``Older'' Expressions}

% \begin{verbatim}
% pause 1 + 2 + 3 + 4 in
% eval 1 + 2 + 3 + 4 in
% 1 + 2 + 3 + 4
% == 10
% \end{verbatim}

% \begin{verbatim}
% pause $e in
% eval 1 + 2 + 3 + 4 in
% pause 1 + 2 + 3 + 4 in
% 1 + 2 + 3 + 4
% == 1 + 2 + 3 + 4
% \end{verbatim}

% \begin{verbatim}
% pause $e in
% hide (let   =   in  ) in
% pause (let   =   in  ) in
% let x = 3 in
% x + 4
% == let x = 3 in x + 4
% \end{verbatim}

% \subsubsection{The nesting properties should works across bindings}

% \begin{verbatim}
% eval $e in
% let x = 1 in
% pause 3 + 3 in
% let y = 2 in
% eval 3 + 3 in
% x + y + 3 + 4
% == 10
% \end{verbatim}

% \begin{verbatim}
% let add = fun x, y -> pause $e in x + y in
% eval $e in
% add(3, 4)
% == [3 + 4]
% \end{verbatim}


% \subsubsection{We want the filter to recover to \emph{older} state when it finish
% evaluating matched sub-expression.}

% \begin{verbatim}
% pause $e in
% eval 1 + 2 + 3 + 4 in
% pause 3 + 3 in
% 1 + 2 + 3 + 4
% == 3 + 3 + 4
% == 10
% \end{verbatim}

% After evaluating \verb|3 + 3|, the stepper falls back to eval mode
% since eval filter matches \verb|1 + 2 + 3 + 4|, so it directly
% evaluates to \verb|10|.

% We also want a \verb|eval| filter to automatically evaluate all sub-expression
% until it cannot proceed.



% \subsection{Handling inconsistency between DHExp and UExp}

% \TODO{Discuss: Move to implementation.tex?}

% There are inconsistencies between the surface expression and expression for
% evaluation in Hazel. For example, fix-points are inserted in the expression
% during elaboration. We want the filters to work with fix-points, with-out user
% acknowledging that they actually needs a fix-point to implement the recursion.

% \begin{verbatim}
% let map : ([Int], Int -> Int) -> [Int] = fun xs, f ->
%   case xs
%   | [] => []
%   | hd :: tl => f(hd)::map(tl, f)
%   end
% in
% let square = fun x -> x * x in
% pause map($v) in
% map([1, 2, 3], square)
% == 1::map([2, 3], f)
% == 1::4::map([3], f)
% \end{verbatim}

% In the example above, we don't want to use to click twice to do unroll and apply, instead we want to merge these two transition
% in one step.

% \subsection{Good but unrealistic for now}

% \TODO{Discuss: Is it better remove in total?}

% There are also something that we think would be intuitive and useful but not possible with current implementation

% \begin{verbatim}
% let fib : Int -> Int =
%   fun n ->
%     if n <= 1 then
%       n
%     else
%       fib(n - 1) + fib(n - 2)
% in
% pause fib($v) + fib($v) in
% fib(5)
% == 3
% \end{verbatim}

% Intuitively we shall see a evaluation trace like this:
% \begin{verbatim}
% ...
% == fib(4) + fib(3)
% == fib(3) + fib(2) + fib(3)
% == fib(3) + fib(2) + fib(2) + fib(1)
% == ...
% \end{verbatim}

% This is no possible since this require us to traverse all possible
% evaluation sequence given a program, which would be super powerful,
% but at the same time super slow.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: