equal
deleted
inserted
replaced
898 |
898 |
899 %----------------------------------- |
899 %----------------------------------- |
900 % SUBSECTION 1 |
900 % SUBSECTION 1 |
901 %----------------------------------- |
901 %----------------------------------- |
902 \section{Specifications of Certain Functions to be Used} |
902 \section{Specifications of Certain Functions to be Used} |
903 To be completed. |
903 Here we give some functions' definitions, |
904 |
904 which we will use later. |
905 |
905 \begin{center} |
|
906 \begin{tabular}{ccc} |
|
907 $\retrieve \; \ACHAR \, \textit{bs} \, c \; \Char(c) = \textit{bs} |
|
908 \end{tabular} |
|
909 \end{center} |
906 |
910 |
907 |
911 |
908 %---------------------------------------------------------------------------------------- |
912 %---------------------------------------------------------------------------------------- |
909 % SECTION correctness proof |
913 % SECTION correctness proof |
910 %---------------------------------------------------------------------------------------- |
914 %---------------------------------------------------------------------------------------- |
931 prove some stepwise properties of lexing nicely: |
935 prove some stepwise properties of lexing nicely: |
932 \begin{lemma}\label{flexStepwise} |
936 \begin{lemma}\label{flexStepwise} |
933 $\textit{flex} \; r \; f \; s@[c] \; v= \flex \; r \; f\; s \; (\inj \; (r\backslash s) \; c \; v) $ |
937 $\textit{flex} \; r \; f \; s@[c] \; v= \flex \; r \; f\; s \; (\inj \; (r\backslash s) \; c \; v) $ |
934 \end{lemma} |
938 \end{lemma} |
935 |
939 |
936 And for $\blexer$ we have something with stepwise properties like $\flex$ as well, |
940 And for $\blexer$ we have a function with stepwise properties like $\flex$ as well, |
937 called $\retrieve$: |
941 called $\retrieve$\ref{retrieveDef}. |
938 \[ |
|
939 \retrieve \; \ACHAR \, \textit{bs} \, c \; \Char(c) = \textit{bs} |
|
940 \] |
|
941 $\retrieve$ takes bit-codes from annotated regular expressions |
942 $\retrieve$ takes bit-codes from annotated regular expressions |
942 guided by a value. |
943 guided by a value. |
943 $\retrieve$ is connected to the $\blexer$ in the following way: |
944 $\retrieve$ is connected to the $\blexer$ in the following way: |
944 \begin{lemma}\label{blexer_retrieve} |
945 \begin{lemma}\label{blexer_retrieve} |
945 $\blexer \; r \; s = \decode \; (\retrieve \; (\internalise \; r) \; (\mkeps \; (r \backslash s) )) \; r$ |
946 $\blexer \; r \; s = \decode \; (\retrieve \; (\internalise \; r) \; (\mkeps \; (r \backslash s) )) \; r$ |