Give the step function.

1 files changed, 51 insertions, 6 deletions

diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index 8babf3c..a781a0c 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -77,12 +77,57 @@ let rename (t : Term) : (Nat -> Nat) -> Term =
   \caption{Implementation of term renaming.}\label{lst:rename}
 \end{listing}
 
-\TODO{
-  \begin{itemize}
-    \item show some example snippets
-    \item explain why fuel is necessary for the reducer
-  \end{itemize}
-}
+The main driver in the reducer is the \verb|step| function, which
+performs a complete development of a term. We give its definition in
+\cref{lst:step}. By induction, all terms within the \verb|foldcase|
+have been completely developed. Most cases pass through their
+arguments unchanged: the only reductions for \(\suc~t\) happen within
+\(t\) for instance. The two interesting cases are \verb|Primrec| and
+\verb|App|. Here we match on the ``active'' term, performing a
+reduction if possible. If the active term is either a neutral
+(\verb|Var|) or absurd (\verb|Zero| as a function) we return the
+inductive argument without further computation applied. Our fuelled
+reducer applies the \verb|step| function to the input for each unit of
+fuel it is given.
+
+\begin{listing}
+  \begin{verbatim}
+let step (t : Term) : Term =
+  foldcase t by
+    { Var n     => ~(Var n)
+    ; Zero _    => ~(Zero <>)
+    ; Suc t     => ~(Suc t)
+    ; Primrec p =>
+      let default = ~(Primrec p) in
+      case p.Target of
+        { Var _     => default
+        ; Zero _    => p.Zero
+        ; Suc t     =>
+          sub p.Suc [ ~(Primrec <Zero: p.Zero; Suc: p.Suc; Target: t>) ]
+        ; Primrec _ => default
+        ; Abs _     => default
+        ; App _     => default
+        }
+    ; Abs t     => ~(Abs t)
+    ; App p     =>
+      let default = ~(App p) in
+      case p.Fun of
+        { Var _     => default
+        ; Zero _    => default
+        ; Suc t     => default
+        ; Primrec _ => default
+        ; Abs t     => sub t [ p.Arg ]
+        ; App _     => default
+        }
+    }
+  \end{verbatim}
+  \caption{Implementation of complete development.}\label{lst:rename}
+\end{listing}
+
+\TODO{explain why fuel is necessary for the reducer}
+
+\subsection{Encoding Algorithm}%
+\label{subsec:encoding}
 
 \TODO{
   \begin{itemize}