--- a/ninems/ninems.tex Wed Jul 03 22:39:47 2019 +0100
+++ b/ninems/ninems.tex Wed Jul 03 23:02:48 2019 +0100
@@ -610,9 +610,26 @@
\end{tabular}
\end{center}
%\end{definition}
+
+Here $fuse$ is an auxiliary function that helps to attach bits to the front of an annotated regular expression. Its definition goes as follows:
+\begin{center}
+\begin{tabular}{lcl}
+ $\textit{fuse}\,bs\,(\textit{ZERO})$ & $\dn$ & $\textit{ZERO}$\\
+ $\textit{fuse}\,bs\,(\textit{ONE}\,bs')$ & $\dn$ &
+ $\textit{ONE}\,(bs\,@\,bs')$\\
+ $\textit{fuse}\,bs\,(\textit{CHAR}\,bs'\,c)$ & $\dn$ &
+ $\textit{CHAR}\,(bs\,@\,bs')\,c$\\
+ $\textit{fuse}\,bs\,(\textit{ALT}\,bs'\,a_1\,a_2)$ & $\dn$ &
+ $\textit{ALT}\,(bs\,@\,bs')\,a_1\,a_2$\\
+ $\textit{fuse}\,bs\,(\textit{SEQ}\,bs'\,a_1\,a_2)$ & $\dn$ &
+ $\textit{SEQ}\,(bs\,@\,bs')\,a_1\,a_2$\\
+ $\textit{fuse}\,bs\,(\textit{STAR}\,bs'\,a)$ & $\dn$ &
+ $\textit{STAR}\,(bs\,@\,bs')\,a$
+\end{tabular}
+\end{center}
+
After internalise we do successive derivative operations on the annotated regular expression.
-Here $fuse$ is an auxiliary function that helps to attach bits to the front of an annotated regular expression.
- This derivative operation is the same as what we previously have for the simple regular expressions, except that we take special care of the bits to store the parse tree information:\\
+ This derivative operation is the same as what we previously have for the simple regular expressions, except that we take special care of the bits :\\
%\begin{definition}{bder}
\begin{center}
\begin{tabular}{@{}lcl@{}}
@@ -634,7 +651,13 @@
\end{tabular}
\end{center}
%\end{definition}
-This way, we do not have to use an injection function and a second phase, but instead only need to collect the bits while running $mkeps$:
+For instance, when we unfold $STAR \; bs \; a$ into a sequence, we attach an additional bit Z to the front of $r \backslash c$ to indicate that there is one more star iteration.
+The other example, the $SEQ$ clause is more subtle-- when $a_1$ is $bnullable$(here bnullable is exactly the same as nullable, except that it is for annotated regular expressions, therefore we omit the definition).
+Assume that $bmkeps$ correctly extracts the bitcode for how $a_1$ matches the string prior to character c(more on this later), then the right branch of $ALTS$, which is $fuse \; bmkeps \; a_1 (a_2 \backslash c)$ will collapse the regular expression $a_1$(as it has already been fully matched) and store the parsing information at the head of the regular expression $a_2 \backslash c$ by fusing to it. The bitsequence $bs$, which was initially attached to the head of $SEQ$, has now been elevated to the top-level of ALT,
+as this information will be needed whichever way the $SEQ$ is matched--no matter whether c belongs to $a_1$ or $ a_2$.
+After carefully doing these derivatives and maintaining all the parsing information, we complete the parsing by collecting the bits using a special $mkeps$ function for annotated regular expressions--$bmkeps$:
+
+
%\begin{definition}[\textit{bmkeps}]\mbox{}
\begin{center}
\begin{tabular}{lcl}
@@ -650,7 +673,10 @@
\end{tabular}
\end{center}
%\end{definition}
-and then decode the bits using the regular expression. After putting these pieces together, the whole process looks like this:\\
+This function completes the parse tree information by
+travelling along the path on the regular epxression that corresponds to a POSIX value snd collect all the bits, and
+using S to indicate the end of star iterations. If we take the bitsproduced by $bmkeps$ and decode it,
+we get the parse tree we need, the working flow looks like this:\\
\begin{center}
\begin{tabular}{lcl}
$\textit{blexer}\;r\,s$ & $\dn$ &