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

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

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

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

    36   Sequ ("_ @ _" [78,77] 63) and

    36   Sequ ("_ @ _" [78,77] 63) and

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

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

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

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

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

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

    43   Prf ("_ : _" [75,75] 75) and  

    41   Prf ("_ : _" [75,75] 75) and  

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

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

    47   F_RIGHT ("F\<^bsub>Right\<^esub> _") and

    45   F_RIGHT ("F\<^bsub>Right\<^esub> _") and

    48   F_LEFT ("F\<^bsub>Left\<^esub> _") and  

    46   F_LEFT ("F\<^bsub>Left\<^esub> _") and  

    49   F_ALT ("F\<^bsub>Alt\<^esub> _ _") and

    47   F_ALT ("F\<^bsub>Alt\<^esub> _ _") and

    50   F_SEQ1 ("F\<^bsub>Seq1\<^esub> _ _") and

    48   F_SEQ1 ("F\<^bsub>Seq1\<^esub> _ _") and

    51   F_SEQ2 ("F\<^bsub>Seq2\<^esub> _ _") and

    49   F_SEQ2 ("F\<^bsub>Seq2\<^esub> _ _") and

    52   F_SEQ ("F\<^bsub>Seq\<^esub> _ _") and

    50   F_SEQ ("F\<^bsub>Seq\<^esub> _ _") and

    53   simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and

    51   simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and

    54   simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and

    52   simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and

    56 

    54 

    57 definition 

    55 definition 

    58   "match r s \<equiv> nullable (ders s r)"

    56   "match r s \<equiv> nullable (ders s r)"

    59 

    57 

    60 (*>*)

    58 (*>*)

   556   \Brz's matcher so that a [lexical] value is constructed (assuming the

   554   \Brz's matcher so that a [lexical] value is constructed (assuming the

   557   regular expression matches the string). The clauses of the Sulzmann and Lu lexer are

   555   regular expression matches the string). The clauses of the Sulzmann and Lu lexer are

   558 

   556 

   559   \begin{center}

   557   \begin{center}

   560   \begin{tabular}{lcl}

   558   \begin{tabular}{lcl}

   563                      & & \phantom{$|$} @{term "None"}  @{text "\<Rightarrow>"} @{term None}\\

   561                      & & \phantom{$|$} @{term "None"}  @{text "\<Rightarrow>"} @{term None}\\

   564                      & & $|$ @{term "Some v"} @{text "\<Rightarrow>"} @{term "Some (injval r c v)"}                          

   562                      & & $|$ @{term "Some v"} @{text "\<Rightarrow>"} @{term "Some (injval r c v)"}                          

   565   \end{tabular}

   563   \end{tabular}

   566   \end{center}

   564   \end{center}

   567 

   565 

   868   we do not simplify under stars: this seems to slow down the algorithm,

   866   we do not simplify under stars: this seems to slow down the algorithm,

   869   rather than speed up. The optimised lexer is then given by the clauses:

   867   rather than speed up. The optimised lexer is then given by the clauses:

   870   

   868   

   871   \begin{center}

   869   \begin{center}

   872   \begin{tabular}{lcl}

   870   \begin{tabular}{lcl}

   875                          @{text "let (r\<^sub>s, f\<^sub>r) = simp (r "}$\backslash$@{text " c) in"}\\

   873                          @{text "let (r\<^sub>s, f\<^sub>r) = simp (r "}$\backslash$@{text " c) in"}\\

   877                      & & \phantom{$|$} @{term "None"}  @{text "\<Rightarrow>"} @{term None}\\

   875                      & & \phantom{$|$} @{term "None"}  @{text "\<Rightarrow>"} @{term None}\\

   878                      & & $|$ @{term "Some v"} @{text "\<Rightarrow>"} @{text "Some (inj r c (f\<^sub>r v))"}                          

   876                      & & $|$ @{term "Some v"} @{text "\<Rightarrow>"} @{text "Some (inj r c (f\<^sub>r v))"}                          

   879   \end{tabular}

   877   \end{tabular}

   880   \end{center}

   878   \end{center}

   881 

   879 

   886   is then recursively called with the simplified derivative, but before

   884   is then recursively called with the simplified derivative, but before

   887   we inject the character @{term c} into value, we need to rectify

   885   we inject the character @{term c} into value, we need to rectify

   888   it (that is construct @{term "f\<^sub>r v"}). We can prove that

   886   it (that is construct @{term "f\<^sub>r v"}). We can prove that

   889 

   887 

   890   \begin{lemma}

   888   \begin{lemma}

   892   \end{lemma}

   890   \end{lemma}

   893 

   891 

   894   \noindent

   892   \noindent

   895   holds but for lack of space refer the reader to our mechanisation for details.

   893   holds but for lack of space refer the reader to our mechanisation for details.

   896 

   894