(*<*)

theory Paper

imports 

   "../Lexer"

   "../Simplifying" 

   "../Positions"

   "../SizeBound4" 

   "HOL-Library.LaTeXsugar"

begin

declare [[show_question_marks = false]]

notation (latex output)

  If  ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10) and

  Cons ("_\<^latex>\<open>\\mbox{$\\,$}\<close>::\<^latex>\<open>\\mbox{$\\,$}\<close>_" [75,73] 73) 

abbreviation 

  "der_syn r c \<equiv> der c r"

notation (latex output)

  der_syn ("_\\_" [79, 1000] 76) and

  ZERO ("\<^bold>0" 81) and 

  ONE ("\<^bold>1" 81) and 

  CH ("_" [1000] 80) and

  ALT ("_ + _" [77,77] 78) and

  SEQ ("_ \<cdot> _" [77,77] 78) and

  STAR ("_\<^sup>\<star>" [79] 78) and

  val.Void ("Empty" 78) and

  val.Char ("Char _" [1000] 78) and

  val.Left ("Left _" [79] 78) and

  val.Right ("Right _" [1000] 78) and

  val.Seq ("Seq _ _" [79,79] 78) and

  val.Stars ("Stars _" [79] 78) and

  Posix ("'(_, _') \<rightarrow> _" [63,75,75] 75) and

  flat ("|_|" [75] 74) and

  flats ("|_|" [72] 74) and

  injval ("inj _ _ _" [79,77,79] 76) and 

  mkeps ("mkeps _" [79] 76) and 

  length ("len _" [73] 73) and

  set ("_" [73] 73) and

  AZERO ("ZERO" 81) and 

  AONE ("ONE _" [79] 78) and 

  ACHAR ("CHAR _ _" [79, 79] 80) and

  AALTs ("ALTs _ _" [77,77] 78) and

  ASEQ ("SEQ _ _ _" [79, 79,79] 78) and

  ASTAR ("STAR _ _" [79, 79] 78) and

  code ("code _" [79] 74) and

  intern ("_\<^latex>\<open>\\mbox{$^\\uparrow$}\<close>" [900] 80) and

  erase ("_\<^latex>\<open>\\mbox{$^\\downarrow$}\<close>" [1000] 74) and

lemma better_retrieve:

   shows "rs \<noteq> Nil ==> retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"

   and   "rs \<noteq> Nil ==> retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"

  apply (metis list.exhaust retrieve.simps(4))

  by (metis list.exhaust retrieve.simps(5))

(*>*)

section {* Introduction *}

text {*

In the last fifteen or so years, Brzozowski's derivatives of regular

expressions have sparked quite a bit of interest in the functional

programming and theorem prover communities.  The beauty of

Brzozowski's derivatives \cite{Brzozowski1964} is that they are neatly

expressible in any functional language, and easily definable and

reasoned about in theorem provers---the definitions just consist of

inductive datatypes and simple recursive functions. A mechanised

correctness proof of Brzozowski's matcher in for example HOL4 has been

mentioned by Owens and Slind~\cite{Owens2008}. Another one in

Isabelle/HOL is part of the work by Krauss and Nipkow

\cite{Krauss2011}.  And another one in Coq is given by Coquand and

Siles \cite{Coquand2012}.

The notion of derivatives

\cite{Brzozowski1964}, written @{term "der c r"}, of a regular

expression give a simple solution to the problem of matching a string

@{term s} with a regular expression @{term r}: if the derivative of

@{term r} w.r.t.\ (in succession) all the characters of the string

matches the empty string, then @{term r} matches @{term s} (and {\em

vice versa}). The derivative has the property (which may almost be

regarded as its specification) that, for every string @{term s} and

regular expression @{term r} and character @{term c}, one has @{term

"cs \<in> L(r)"} if and only if \mbox{@{term "s \<in> L(der c r)"}}.

If a regular expression matches a string, then in general there is more

than one way of how the string is matched. There are two commonly used

disambiguation strategies to generate a unique answer: one is called

GREEDY matching \cite{Frisch2004} and the other is POSIX

matching~\cite{POSIX,Kuklewicz,OkuiSuzuki2010,Sulzmann2014,Vansummeren2006}.

For example consider the string @{term xy} and the regular expression

\mbox{@{term "STAR (ALT (ALT x y) xy)"}}. Either the string can be

matched in two `iterations' by the single letter-regular expressions

@{term x} and @{term y}, or directly in one iteration by @{term xy}. The

first case corresponds to GREEDY matching, which first matches with the

left-most symbol and only matches the next symbol in case of a mismatch

(this is greedy in the sense of preferring instant gratification to

delayed repletion). The second case is POSIX matching, which prefers the

longest match.

\begin{center}

\begin{tabular}{cc}

  \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}

  @{thm (lhs) der.simps(1)} & $\dn$ & @{thm (rhs) der.simps(1)}\\

  @{thm (lhs) der.simps(2)} & $\dn$ & @{thm (rhs) der.simps(2)}\\

  @{thm (lhs) der.simps(3)} & $\dn$ & @{thm (rhs) der.simps(3)}\\

  @{thm (lhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]}\\

  @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{text "if"} @{term "nullable(r\<^sub>1)"}\\

  & & @{text "then"} @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2)"}\\

  & & @{text "else"} @{term "SEQ (der c r\<^sub>1) r\<^sub>2"}\\

  % & & @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]}\\

  @{thm (lhs) der.simps(6)} & $\dn$ & @{thm (rhs) der.simps(6)}

  \end{tabular}

  &

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

  @{thm (lhs) nullable.simps(1)} & $\dn$ & @{thm (rhs) nullable.simps(1)}\\

  @{thm (lhs) nullable.simps(2)} & $\dn$ & @{thm (rhs) nullable.simps(2)}\\

  @{thm (lhs) nullable.simps(3)} & $\dn$ & @{thm (rhs) nullable.simps(3)}\\

  @{thm (lhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\

  @{thm (lhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\

  @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\medskip\\

  \end{tabular}  

\end{tabular}  

\end{center}

\begin{figure}[t]

\begin{center}

\begin{tikzpicture}[scale=2,node distance=1.3cm,

                    every node/.style={minimum size=6mm}]

\node (r1)  {@{term "r\<^sub>1"}};

\node (r2) [right=of r1]{@{term "r\<^sub>2"}};

\draw[->,line width=1mm](r1)--(r2) node[above,midway] {@{term "der a DUMMY"}};

\node (r3) [right=of r2]{@{term "r\<^sub>3"}};

\draw[->,line width=1mm](r2)--(r3) node[above,midway] {@{term "der b DUMMY"}};

\node (r4) [right=of r3]{@{term "r\<^sub>4"}};

\draw[->,line width=1mm](r3)--(r4) node[above,midway] {@{term "der c DUMMY"}};

\draw (r4) node[anchor=west] {\;\raisebox{3mm}{@{term nullable}}};

\node (v4) [below=of r4]{@{term "v\<^sub>4"}};

\draw[->,line width=1mm](r4) -- (v4);

\node (v3) [left=of v4] {@{term "v\<^sub>3"}};

\draw[->,line width=1mm](v4)--(v3) node[below,midway] {\<open>inj r\<^sub>3 c\<close>};

\node (v2) [left=of v3]{@{term "v\<^sub>2"}};

\draw[->,line width=1mm](v3)--(v2) node[below,midway] {\<open>inj r\<^sub>2 b\<close>};

\node (v1) [left=of v2] {@{term "v\<^sub>1"}};

\draw[->,line width=1mm](v2)--(v1) node[below,midway] {\<open>inj r\<^sub>1 a\<close>};

\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{@{term "mkeps"}}};

\end{tikzpicture}

\end{center}

\mbox{}\\[-13mm]

\caption{The two phases of the algorithm by Sulzmann \& Lu \cite{Sulzmann2014},

matching the string @{term "[a,b,c]"}. The first phase (the arrows from 

left to right) is \Brz's matcher building successive derivatives. If the 

last regular expression is @{term nullable}, then the functions of the 

second phase are called (the top-down and right-to-left arrows): first 

@{term mkeps} calculates a value @{term "v\<^sub>4"} witnessing

how the empty string has been recognised by @{term "r\<^sub>4"}. After

that the function @{term inj} ``injects back'' the characters of the string into

the values.

\label{Sulz}}

\end{figure} 

*}

section {* Background *}

text {*

  Sulzmann-Lu algorithm with inj. State that POSIX rules.

  metion slg is correct.

  \begin{figure}[t]

  \begin{center}

  \begin{tabular}{c}

  @{thm[mode=Axiom] Posix.intros(1)}\<open>P\<close>@{term "ONE"} \qquad

  @{thm[mode=Axiom] Posix.intros(2)}\<open>P\<close>@{term "c"}\medskip\\

  @{thm[mode=Rule] Posix.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}\<open>P+L\<close>\qquad

  @{thm[mode=Rule] Posix.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}\<open>P+R\<close>\medskip\\

  $\mprset{flushleft}

   \inferrule

   {@{thm (prem 1) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \qquad

    @{thm (prem 2) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \\\\

    @{thm (prem 3) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}

   {@{thm (concl) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}$\<open>PS\<close>\\

  @{thm[mode=Axiom] Posix.intros(7)}\<open>P[]\<close>\medskip\\

  $\mprset{flushleft}

   \inferrule

   {@{thm (prem 1) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad

    @{thm (prem 2) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad

    @{thm (prem 3) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \\\\

    @{thm (prem 4) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}

   {@{thm (concl) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}$\<open>P\<star>\<close>

  \end{tabular}

  \end{center}

  \caption{Our inductive definition of POSIX values.}\label{POSIXrules}

  \end{figure}

  \begin{center}

  \begin{tabular}{lcl}

  @{thm (lhs) mkeps.simps(1)} & $\dn$ & @{thm (rhs) mkeps.simps(1)}\\

  @{thm (lhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]}\\

  @{thm (lhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]}\\

  @{thm (lhs) mkeps.simps(4)} & $\dn$ & @{thm (rhs) mkeps.simps(4)}\\

  \end{tabular}

  \end{center}

  \begin{center}

  \begin{tabular}{l@ {\hspace{5mm}}lcl}

  \textit{(1)} & @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\

  \textit{(2)} & @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & 

      @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\

  \textit{(3)} & @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & 

      @{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\

  \textit{(4)} & @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 

      & @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\

  \textit{(5)} & @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 

      & @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\

  \textit{(6)} & @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ 

      & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\

  \textit{(7)} & @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$ 

      & @{thm (rhs) injval.simps(7)[of "r" "c" "v" "vs"]}\\

  \end{tabular}

  \end{center}

*}

section {* Bitcoded Regular Expressions and Derivatives *}

text {*

  In the second part of their paper \cite{Sulzmann2014},

  Sulzmann and Lu describe another algorithm that generates POSIX

  values but dispences with the second phase where characters are

  injected ``back'' into values. For this they annotate bitcodes to

  regular expressions, which we define in Isabelle/HOL as the datatype

  \begin{center}

  \begin{tabular}{lcl}

  @{term breg} & $::=$ & @{term "AZERO"} $\quad\mid\quad$ @{term "AONE bs"}\\

               & $\mid$ & @{term "ACHAR bs c"}\\

               & $\mid$ & @{term "AALTs bs rs"}\\

               & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\

               & $\mid$ & @{term "ASTAR bs r"}

  \end{tabular}

  \end{center}

  @{text "r\<^sub>1"} and @{text "r\<^sub>2"} for bitcoded regular

  expressions; and @{text rs} for lists of bitcoded regular

  expressions. The binary alternative @{text "ALT bs r\<^sub>1 r\<^sub>2"}

  is just an abbreviation for @{text "ALTs bs [r\<^sub>1, r\<^sub>2]"}. 

  For bitsequences we just use lists made up of the

  constants @{text Z} and @{text S}.  The idea with bitcoded regular

  expressions is to incrementally generate the value information (for

  function for how values can be coded into bitsequences.

  \begin{center}

  \begin{tabular}{cc}

  \begin{tabular}{lcl}

  @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\

  @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\

  @{thm (lhs) code.simps(3)} & $\dn$ & @{thm (rhs) code.simps(3)}\\

  @{thm (lhs) code.simps(4)} & $\dn$ & @{thm (rhs) code.simps(4)}

  \end{tabular}

  &

  \begin{tabular}{lcl}

  @{thm (lhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\

  @{thm (lhs) code.simps(6)} & $\dn$ & @{thm (rhs) code.simps(6)}\\

  @{thm (lhs) code.simps(7)} & $\dn$ & @{thm (rhs) code.simps(7)}\\

  \mbox{\phantom{XX}}\\

  \end{tabular}

  \end{tabular}

  \end{center}

  \noindent

  As can be seen, this coding is ``lossy'' in the sense that we do not

  record explicitly character values and also not sequence values (for

  @{text S} followed by some bitsequence. Similarly, we use @{text Z} to indicate

  if there is still a value coming in the list of @{text Stars}, whereas @{text S}

  indicates the end of the list. The lossiness makes the process of

  decoding a bit more involved, but the point is that if we have a

  regular expression \emph{and} a bitsequence of a corresponding value,

  then we can always decode the value accurately. The decoding can be

  defined by using two functions called $\textit{decode}'$ and

  \textit{decode}:

  \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{2mm}$\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{2mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\

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

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

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

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

  \end{tabular}    

  \end{center}

  \noindent

  The function \textit{decode} checks whether all of the bitsequence is

  consumed and returns the corresponding value as @{term "Some v"}; otherwise

  it fails with @{text "None"}. We can establish that for a value $v$

  inhabited by a regular expression $r$, the decoding of its

  bitsequence never fails.

\begin{lemma}\label{codedecode}\it

  If $\;\vdash v : r$ then

  $\;\textit{decode}\,(\textit{code}\, v)\,r = \textit{Some}\, v$.

\end{lemma}

\begin{proof}

  This follows from the property that

  $\textit{decode}'\,((\textit{code}\,v) \,@\, bs)\,r = (v, bs)$ holds

  for any bit-sequence $bs$ and $\vdash v : r$. This property can be

  easily proved by induction on $\vdash v : r$.

\end{proof}  

  Sulzmann and Lu define the function \emph{internalise}

  in order to transform standard regular expressions into annotated

  regular expressions. We write this operation as $r^\uparrow$.

  This internalisation uses the following

  \emph{fuse} function.	     

  \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{ALTs}\,bs'\,rs)$ & $\dn$ &

     $\textit{ALTs}\,(bs\,@\,bs')\,rs$\\

  $\textit{fuse}\,bs\,(\textit{SEQ}\,bs'\,r_1\,r_2)$ & $\dn$ &

     $\textit{SEQ}\,(bs\,@\,bs')\,r_1\,r_2$\\

  $\textit{fuse}\,bs\,(\textit{STAR}\,bs'\,r)$ & $\dn$ &

     $\textit{STAR}\,(bs\,@\,bs')\,r$

  \end{tabular}    

  \end{center}    

  \noindent

  A regular expression can then be \emph{internalised} into a bitcoded

  regular expression as follows.

  \begin{center}

  \begin{tabular}{lcl}

  $(\ZERO)^\uparrow$ & $\dn$ & $\textit{ZERO}$\\

  $(\ONE)^\uparrow$ & $\dn$ & $\textit{ONE}\,[]$\\

  $(c)^\uparrow$ & $\dn$ & $\textit{CHAR}\,[]\,c$\\

  $(r_1 + r_2)^\uparrow$ & $\dn$ &

         $\textit{ALT}\;[]\,(\textit{fuse}\,[\Z]\,r_1^\uparrow)\,

                            (\textit{fuse}\,[\S]\,r_2^\uparrow)$\\

  $(r_1\cdot r_2)^\uparrow$ & $\dn$ &

         $\textit{SEQ}\;[]\,r_1^\uparrow\,r_2^\uparrow$\\

  $(r^*)^\uparrow$ & $\dn$ &

         $\textit{STAR}\;[]\,r^\uparrow$\\

  \end{tabular}    

  \end{center}    

  \noindent

  There is also an \emph{erase}-function, written $a^\downarrow$, which

  transforms a bitcoded regular expression into a (standard) regular

  expression by just erasing the annotated bitsequences. We omit the

  straightforward definition. For defining the algorithm, we also need

  the functions \textit{bnullable} and \textit{bmkeps}, which are the

  ``lifted'' versions of \textit{nullable} and \textit{mkeps} acting on

  bitcoded regular expressions, instead of regular expressions.

  \begin{center}

  $\textit{bnullable}\,(\textit{ONE}\,bs)$ & $\dn$ & $\textit{true}$\\

  $\textit{bnullable}\,(\textit{CHAR}\,bs\,c)$ & $\dn$ & $\textit{false}$\\

     $\textit{true}$

     $bs \,@\, [\S]$

  \end{center}    

  \noindent

  The key function in the bitcoded algorithm is the derivative of an

  \begin{center}

  \begin{tabular}{@ {}lcl@ {}}

  $(\textit{ONE}\;bs)\backslash c$ & $\dn$ & $\textit{ZERO}$\\  

  $(\textit{CHAR}\;bs\,d)\backslash c$ & $\dn$ &

        $\textit{if}\;c=d\; \;\textit{then}\;

         \textit{ONE}\;bs\;\textit{else}\;\textit{ZERO}$\\  

      $\textit{SEQ}\;bs\,(\textit{fuse}\, [\Z] (r\backslash c))\,

       (\textit{STAR}\,[]\,r)$

  \end{tabular}    

  \end{center}

  \noindent

  just like the standard derivative.  We omit the details. Finally we

  \noindent

This bitcoded lexer first internalises the regular expression $r$ and then

the derivative is \emph{not} nullable, then $\textit{None}$ is

generates the same result as with \textit{lexer}.