% Chapter Template

% Main chapter title

\chapter{Bit-coded Algorithm of Sulzmann and Lu}

\label{Bitcoded1} % Change X to a consecutive number; for referencing this chapter elsewhere, use \ref{ChapterX}

%Then we illustrate how the algorithm without bitcodes falls short for such aggressive 

%simplifications and therefore introduce our version of the bitcoded algorithm and 

%its correctness proof in 

%Chapter 3\ref{Chapter3}. 

In this chapter, we are going to describe the bit-coded algorithm

introduced by Sulzmann and Lu \parencite{Sulzmann2014} to address the growth problem of 

regular expressions. 

\section{Bit-coded Algorithm}

stores information of previous lexing steps

on a stack, in the form of regular expressions

and characters: $r_0$, $c_0$, $r_1$, $c_1$, etc.

\begin{ceqn}

\begin{equation}%\label{graph:injLexer}

	\begin{tikzcd}[ampersand replacement=\&, execute at end picture={

			\begin{scope}[on background layer]

				\node[rectangle, fill={red!30},

					pattern=north east lines, pattern color=red,

					fit={(-3,-1) (-3, 1) (1, -1) 

						(1, 1)}

				     ] 

				     {}; ,

				\node[rectangle, fill={blue!20},

					pattern=north east lines, pattern color=blue,

					fit= {(1, -1) (1, 1) (3, -1) (3, 1)}

					]

					{};

				\end{scope}}

					]

r_0 \arrow[r, "\backslash c_0"]  \arrow[d] \& r_1 \arrow[r, "\backslash c_1"] \arrow[d] \& r_2 \arrow[r, dashed] \arrow[d] \& r_n \arrow[d, "mkeps" description] \\

v_0           \& v_1 \arrow[l,"inj_{r_0} c_0"]                \& v_2 \arrow[l, "inj_{r_1} c_1"]              \& v_n \arrow[l, dashed]         \\

\end{tikzcd}

\end{equation}

\end{ceqn}

\noindent

The red area expands as we move towards $r_n$, 

the forward derivative phase, we choose to store them

information on the fly, while still using regular expression 

derivatives.

lexing steps, and use red and blue areas as before

to indicate consumed (seen) input and constructed

partial value (before recovering the rest of the stack),

one could see that the seen part's lexical information

is stored in the form of a regular expression.

Consider the regular expression $(aa)^* \cdot bc$ matching the string $aabc$

and assume we have just read the two characters $aa$:

\begin{center}

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

    \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]

	    {Partial lexing info: $\ONE \cdot a \cdot (aa)^* \cdot bc$ etc.

         \nodepart{two} $\Seq(\ldots, \Seq(\Char(b), \Char(c)))$};

\end{tikzpicture}

\end{center}

\noindent

In the injection-based lexing algorithm, we ``neglect" the red area

by putting all the characters we have consumed and

intermediate regular expressions on the stack when 

we go from left to right in the derivative phase.

The red area grows till the string is exhausted.

During the injection phase, the value in the blue area

is built up incrementally, while the red area shrinks.

Before we have recovered all characters and intermediate

derivative regular expressions from the stack,

what values these characters and regular expressions correspond 

to are unknown: 

\begin{center}

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

    \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={white!30,blue!20},]

	    {$(\ONE \cdot \ONE) \cdot (aa)^* \cdot bc $ correspond to:$???$

         \nodepart{two}  $b c$ corresponds to  $\Seq(\ldots, \Seq(\Char(b), \Char(c)))$};

%\caption{term 1 \ref{term:1}'s matching configuration}

\end{tikzpicture}

\end{center}

\noindent

However, they should be calculable,

as characters and regular expression shapes

after taking derivative w.r.t those characters

have already been known, therefore in our example,

we know that the value starts with two $a$s,

and makes up to an iteration in a Kleene star:

(We have put the injection-based lexing's partial 

result in the right part of the split rectangle

to contrast it with the partial valued produced

in a forward manner)

\begin{center}

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

    \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]

	    {$\stackrel{Bitcoded}{\longrightarrow} \Seq(\Stars[\Char(a), \Char(a)], ???)$

	\nodepart{two} $\Seq(\ldots, \Seq(\Char(b), \Char(c)))$  $\stackrel{Inj}{\longleftarrow}$};

%\caption{term 1 \ref{term:1}'s matching configuration}

\end{tikzpicture}

\end{center}

\noindent

If we do this kind of "attachment"

and each time augment the attached partially

constructed value when taking off a 

character:

\begin{center}

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

	\node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},] (spPoint)

        {$\Seq(\Stars[\Char(a), \Char(a)], \ldots)$

         \nodepart{two} Remaining: $b c$};

\end{tikzpicture}\\

$\downarrow$\\

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

    \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]

        {$\Seq(\Stars[\Char(a), \Char(a)], \Seq(\Char(b), \ldots))$

         \nodepart{two} Remaining: $c$};

\end{tikzpicture}\\

$\downarrow$\\

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

    \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]

        {$\Seq(\Stars[\Char(a), \Char(a)], \Seq(\Char(b), \Char(c)))$

         \nodepart{two} EOF};

\end{tikzpicture}

\end{center}

\noindent

In the end we could recover the value without a backward phase.

But (partial) values are a bit clumsy to stick together with a regular expression, so 

we instead use bit-codes to encode them.

Bits and bitcodes (lists of bits) are defined as:

\begin{center}

		$b ::=   S \mid  Z \qquad

bs ::= [] \mid b::bs    

$

\end{center}

\noindent

Using $S$ and $Z$ rather than $1$ and $0$ is to avoid

confusion with the regular expressions $\ZERO$ and $\ONE$.

Bitcodes (or

bit-lists) can be used to encode values (or potentially incomplete values) in a

compact form. This can be straightforwardly seen in the following

coding function from values to bitcodes: 

\begin{center}

\begin{tabular}{lcl}

  $\textit{code}(\Empty)$ & $\dn$ & $[]$\\

  $\textit{code}(\Char\,c)$ & $\dn$ & $[]$\\

  $\textit{code}(\Left\,v)$ & $\dn$ & $Z :: code(v)$\\

  $\textit{code}(\Right\,v)$ & $\dn$ & $S :: code(v)$\\

  $\textit{code}(\Seq\,v_1\,v_2)$ & $\dn$ & $code(v_1) \,@\, code(v_2)$\\

  $\textit{code}(\Stars\,[])$ & $\dn$ & $[Z]$\\

  $\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $S :: code(v) \;@\;

                                                 code(\Stars\,vs)$

\end{tabular}    

\end{center} 

\noindent

Here $\textit{code}$ encodes a value into a bit-code by converting

$\Left$ into $Z$, $\Right$ into $S$, and marks the start of any non-empty

star iteration by $S$. The border where a local star terminates

is marked by $Z$. 

This coding is lossy, as it throws away the information about

characters, and also does not encode the ``boundary'' between two

sequence values. Moreover, with only the bitcode we cannot even tell

whether the $S$s and $Z$s are for $\Left/\Right$ or $\Stars$. The

reason for choosing this compact way of storing information is that the

relatively small size of bits can be easily manipulated and ``moved

around" in a regular expression. 

Because of the lossiness, the process of decoding a bitlist requires additionally 

a regular expression. The function $\decode$ is defined as:

%\begin{definition}[Bitdecoding of Values]\mbox{}

\begin{center}

\begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}

  $\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\

  $\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\

  $\textit{decode}'\,(Z\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &

     $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\;

       (\Left\,v, bs_1)$\\

  $\textit{decode}'\,(S\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &

     $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\;

       (\Right\,v, bs_1)$\\                           

  $\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ &

        $\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\

  & &   $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\

  & &   \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\

  $\textit{decode}'\,(Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\

  $\textit{decode}'\,(S\!::\!bs)\,(r^*)$ & $\dn$ & 

         $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\

  & &   $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\

  & &   \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\

  $\textit{decode}\,bs\,r$ & $\dn$ &

     $\textit{let}\,(v, bs') = \textit{decode}'\,bs\,r\;\textit{in}$\\

  & & $\textit{if}\;bs' = []\;\textit{then}\;\textit{Some}\,v\;

       \textit{else}\;\textit{None}$                       

\end{tabular}    

\end{center} 

%\end{definition}