801 \noindent from which tokens with classifications (keyword-token, |
801 \noindent from which tokens with classifications (keyword-token, |
802 identifier-token and so on) can be extracted. |
802 identifier-token and so on) can be extracted. |
803 |
803 |
804 Derivatives as calculated by \Brz's method are usually more complex |
804 Derivatives as calculated by \Brz's method are usually more complex |
805 regular expressions than the initial one; the result is that the |
805 regular expressions than the initial one; the result is that the |
806 deivative-based matching and lexing algorithms are often abysmally slow. |
806 derivative-based matching and lexing algorithms are often abysmally slow. |
807 However, various optimisations are possible, such as the simplifications |
807 However, various optimisations are possible, such as the simplifications |
808 of @{term "ALT ZERO r"}, @{term "ALT r ZERO"}, @{term "SEQ ONE r"} and |
808 of @{term "ALT ZERO r"}, @{term "ALT r ZERO"}, @{term "SEQ ONE r"} and |
809 @{term "SEQ r ONE"} to @{term r}. These simplifications can speed up the |
809 @{term "SEQ r ONE"} to @{term r}. These simplifications can speed up the |
810 algorithms considerably, as noted in \cite{Sulzmann2014}. One of the |
810 algorithms considerably, as noted in \cite{Sulzmann2014}. One of the |
811 advantages of having a simple specification and correctness proof is that |
811 advantages of having a simple specification and correctness proof is that |