(*<*)
theory PaperExt
imports 
   (*"../LexerExt"*)
   (*"../PositionsExt"*)
   "~~/src/HOL/Library/LaTeXsugar"
begin
(*>*)

(*
declare [[show_question_marks = false]]
declare [[eta_contract = false]]

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

abbreviation 
  "ders_syn r s \<equiv> ders s r"


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) and  

  ZERO ("\<^bold>0" 81) and 
  ONE ("\<^bold>1" 81) and 
  CHAR ("_" [1000] 80) and
  ALT ("_ + _" [77,77] 78) and
  SEQ ("_ \<cdot> _" [77,77] 78) and
  STAR ("_\<^sup>\<star>" [78] 78) and
  NTIMES ("_\<^bsup>'{_'}\<^esup>" [78, 50] 80) and
  FROMNTIMES ("_\<^bsup>'{_..'}\<^esup>" [78, 50] 80) and
  UPNTIMES ("_\<^bsup>'{.._'}\<^esup>" [78, 50] 80) and
  NMTIMES ("_\<^bsup>'{_.._'}\<^esup>" [78, 50,50] 80) 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 _" [1000] 78) and

  L ("L'(_')" [10] 78) and
  LV ("LV _ _" [80,73] 78) and
  der_syn ("_\\_" [79, 1000] 76) and  
  ders_syn ("_\\_" [79, 1000] 76) and
  flat ("|_|" [75] 74) and
  flats ("|_|" [72] 74) and
  Sequ ("_ @ _" [78,77] 63) and
  injval ("inj _ _ _" [81,77,79] 76) and 
  mkeps ("mkeps _" [79] 76) and 
  length ("len _" [73] 73) and
  intlen ("len _" [73] 73) and
  set ("_" [73] 73) and
 
  Prf ("_ : _" [75,75] 75) and
  Posix ("'(_, _') \<rightarrow> _" [63,75,75] 75) and
 
  lexer ("lexer _ _" [78,78] 77) and
  DUMMY ("\<^latex>\<open>\\underline{\\hspace{2mm}}\<close>")
*)  
(*>*)

(*
section {* Extensions*}

text {*

  A strong point in favour of
  Sulzmann and Lu's algorithm is that it can be extended in various
  ways.  If we are interested in tokenising a string, then we need to not just
  split up the string into tokens, but also ``classify'' the tokens (for
  example whether it is a keyword or an identifier). This can be done with
  only minor modifications to the algorithm by introducing \emph{record
  regular expressions} and \emph{record values} (for example
  \cite{Sulzmann2014b}):

  \begin{center}  
  @{text "r :="}
  @{text "..."} $\mid$
  @{text "(l : r)"} \qquad\qquad
  @{text "v :="}
  @{text "..."} $\mid$
  @{text "(l : v)"}
  \end{center}
  
  \noindent where @{text l} is a label, say a string, @{text r} a regular
  expression and @{text v} a value. All functions can be smoothly extended
  to these regular expressions and values. For example \mbox{@{text "(l :
  r)"}} is nullable iff @{term r} is, and so on. The purpose of the record
  regular expression is to mark certain parts of a regular expression and
  then record in the calculated value which parts of the string were matched
  by this part. The label can then serve as classification for the tokens.
  For this recall the regular expression @{text "(r\<^bsub>key\<^esub> + r\<^bsub>id\<^esub>)\<^sup>\<star>"} for
  keywords and identifiers from the Introduction. With the record regular
  expression we can form \mbox{@{text "((key : r\<^bsub>key\<^esub>) + (id : r\<^bsub>id\<^esub>))\<^sup>\<star>"}}
  and then traverse the calculated value and only collect the underlying
  strings in record values. With this we obtain finite sequences of pairs of
  labels and strings, for example

  \[@{text "(l\<^sub>1 : s\<^sub>1), ..., (l\<^sub>n : s\<^sub>n)"}\]
  
  \noindent from which tokens with classifications (keyword-token,
  identifier-token and so on) can be extracted.

  In the context of POSIX matching, it is also interesting to study additional
  constructors about bounded-repetitions of regular expressions. For this let
  us extend the results from the previous section to the following four
  additional regular expression constructors:

  \begin{center}
  \begin{tabular}{lcrl@ {\hspace{12mm}}l}
  @{text r} & @{text ":="} & $\ldots\mid$ & @{term "NTIMES r n"} & exactly-@{text n}-times\\
            &              & $\mid$   & @{term "UPNTIMES r n"} & upto-@{text n}-times\\
	    &              & $\mid$   & @{term "FROMNTIMES r n"} & from-@{text n}-times\\
	    &              & $\mid$   & @{term "NMTIMES r n m"} & between-@{text nm}-times\\
  \end{tabular}
  \end{center}

  \noindent
  We will call them \emph{bounded regular expressions}.
  With the help of the power operator (definition ommited) for sets of strings, the languages
  recognised by these regular expression can be defined in Isabelle as follows:

  \begin{center}
  \begin{tabular}{lcl} 
  @{thm (lhs) L.simps(8)} & $\dn$ & @{thm (rhs) L.simps(8)}\\
  @{thm (lhs) L.simps(7)} & $\dn$ & @{thm (rhs) L.simps(7)}\\
  @{thm (lhs) L.simps(9)} & $\dn$ & @{thm (rhs) L.simps(9)}\\
  @{thm (lhs) L.simps(10)} & $\dn$ & @{thm (rhs) L.simps(10)}\\
  \end{tabular}
  \end{center}

  \noindent This definition implies that in the last clause @{term
  "NMTIMES r n m"} matches no string in case @{term "m < n"}, because
  then the interval @{term "{n..m}"} is empty.  While the language
  recognised by these regular expressions is straightforward, some
  care is needed for how to define the corresponding lexical
  values. First, with a slight abuse of language, we will (re)use
  values of the form @{term "Stars vs"} for values inhabited in
  bounded regular expressions. Second, we need to introduce inductive
  rules for extending our inhabitation relation shown on
  Page~\ref{prfintros}, from which we then derived our notion of
  lexical values. Given the rule for @{term "STAR r"}, the rule for
  @{term "UPNTIMES r n"} just requires additionally that the length of
  the list of values must be smaller or equal to @{term n}:

  \begin{center}
  @{thm[mode=Rule] Prf.intros(7)[of "vs"]}
  \end{center}

  \noindent Like in the @{term "STAR r"}-rule, we require with the
  left-premise that some non-empty part of the string is `chipped'
  away by \emph{every} value in @{text vs}, that means the corresponding
  values do not flatten to the empty string. In the rule for @{term
  "NTIMES r n"} (that is exactly-@{term n}-times @{text r}) we clearly need to require
  that the length of the list of values equals to @{text n}. But enforcing
  that every of these @{term n} values `chipps' away some part of a string
  would be too strong. 


  \begin{center}
  @{thm[mode=Rule] Prf.intros(8)[of "vs\<^sub>1" r "vs\<^sub>2"]}
  \end{center}

  \begin{center}
  \begin{tabular}{lcl} 
  @{thm (lhs) der.simps(8)} & $\dn$ & @{thm (rhs) der.simps(8)}\\
  @{thm (lhs) der.simps(7)} & $\dn$ & @{thm (rhs) der.simps(7)}\\
  @{thm (lhs) der.simps(9)} & $\dn$ & @{thm (rhs) der.simps(9)}\\
  @{thm (lhs) der.simps(10)} & $\dn$ & @{thm (rhs) der.simps(10)}\\
  \end{tabular}
  \end{center} 


  \begin{center}
  \begin{tabular}{lcl}
  @{thm (lhs) mkeps.simps(5)} & $\dn$ & @{thm (rhs) mkeps.simps(5)}\\
  @{thm (lhs) mkeps.simps(6)} & $\dn$ & @{thm (rhs) mkeps.simps(6)}\\
  @{thm (lhs) mkeps.simps(7)} & $\dn$ & @{thm (rhs) mkeps.simps(7)}\\
  @{thm (lhs) mkeps.simps(8)} & $\dn$ & @{thm (rhs) mkeps.simps(8)}\\
  \end{tabular}
  \end{center}

  \begin{center}
  \begin{tabular}{lcl}
  @{thm (lhs) injval.simps(8)} & $\dn$ & @{thm (rhs) injval.simps(8)}\\
  @{thm (lhs) injval.simps(9)} & $\dn$ & @{thm (rhs) injval.simps(9)}\\
  @{thm (lhs) injval.simps(10)} & $\dn$ & @{thm (rhs) injval.simps(10)}\\
  @{thm (lhs) injval.simps(11)} & $\dn$ & @{thm (rhs) injval.simps(11)}\\
  \end{tabular}
  \end{center}
  

  @{thm [mode=Rule] Posix_NTIMES1[of "s\<^sub>1" r v "s\<^sub>2"]}

  @{thm [mode=Rule] Posix_NTIMES2}

  @{thm [mode=Rule] Posix_UPNTIMES1[of "s\<^sub>1" r v "s\<^sub>2"]}

  @{thm [mode=Rule] Posix_UPNTIMES2}

  @{thm [mode=Rule] Posix_FROMNTIMES1[of "s\<^sub>1" r v "s\<^sub>2"]}

  @{thm [mode=Rule] Posix_FROMNTIMES3[of "s\<^sub>1" r v "s\<^sub>2"]}

  @{thm [mode=Rule] Posix_FROMNTIMES2}

  @{thm [mode=Rule] Posix_NMTIMES1[of "s\<^sub>1" r v "s\<^sub>2"]}

  @{thm [mode=Rule] Posix_NMTIMES3[of "s\<^sub>1" r v "s\<^sub>2"]}

  @{thm [mode=Rule] Posix_NMTIMES2}



   @{term "\<Sum> i \<in> {m..n} . P i"}  @{term "\<Sum> i \<in> {..n} . P i"}
  @{term "\<Union> i \<in> {m..n} . P i"}  @{term "\<Union> i \<in> {..n} . P i"}
   @{term "\<Union> i \<in> {0::nat..n} . P i"}



*}



section {* The Correctness Argument by Sulzmann and Lu\label{argu} *}

text {*
%  \newcommand{\greedy}{\succcurlyeq_{gr}}
 \newcommand{\posix}{>}

  An extended version of \cite{Sulzmann2014} is available at the website of
  its first author; this includes some ``proofs'', claimed in
  \cite{Sulzmann2014} to be ``rigorous''. Since these are evidently not in
  final form, we make no comment thereon, preferring to give general reasons
  for our belief that the approach of \cite{Sulzmann2014} is problematic.
  Their central definition is an ``ordering relation'' defined by the
  rules (slightly adapted to fit our notation):

  ??

  \noindent The idea behind the rules (A1) and (A2), for example, is that a
  @{text Left}-value is bigger than a @{text Right}-value, if the underlying
  string of the @{text Left}-value is longer or of equal length to the
  underlying string of the @{text Right}-value. The order is reversed,
  however, if the @{text Right}-value can match a longer string than a
  @{text Left}-value. In this way the POSIX value is supposed to be the
  biggest value for a given string and regular expression.

  Sulzmann and Lu explicitly refer to the paper \cite{Frisch2004} by Frisch
  and Cardelli from where they have taken the idea for their correctness
  proof. Frisch and Cardelli introduced a similar ordering for GREEDY
  matching and they showed that their GREEDY matching algorithm always
  produces a maximal element according to this ordering (from all possible
  solutions). The only difference between their GREEDY ordering and the
  ``ordering'' by Sulzmann and Lu is that GREEDY always prefers a @{text
  Left}-value over a @{text Right}-value, no matter what the underlying
  string is. This seems to be only a very minor difference, but it has
  drastic consequences in terms of what properties both orderings enjoy.
  What is interesting for our purposes is that the properties reflexivity,
  totality and transitivity for this GREEDY ordering can be proved
  relatively easily by induction.
*}
*)

section {* Conclusion *}

text {*

  We have implemented the POSIX value calculation algorithm introduced by
  Sulzmann and Lu
  \cite{Sulzmann2014}. Our implementation is nearly identical to the
  original and all modifications we introduced are harmless (like our char-clause for
  @{text inj}). We have proved this algorithm to be correct, but correct
  according to our own specification of what POSIX values are. Our
  specification (inspired from work by Vansummeren \cite{Vansummeren2006}) appears to be
  much simpler than in \cite{Sulzmann2014} and our proofs are nearly always
  straightforward. We have attempted to formalise the original proof
  by Sulzmann and Lu \cite{Sulzmann2014}, but we believe it contains
  unfillable gaps. In the online version of \cite{Sulzmann2014}, the authors
  already acknowledge some small problems, but our experience suggests
  that there are more serious problems. 
  
  Having proved the correctness of the POSIX lexing algorithm in
  \cite{Sulzmann2014}, which lessons have we learned? Well, this is a
  perfect example for the importance of the \emph{right} definitions. We
  have (on and off) explored mechanisations as soon as first versions
  of \cite{Sulzmann2014} appeared, but have made little progress with
  turning the relatively detailed proof sketch in \cite{Sulzmann2014} into a
  formalisable proof. Having seen \cite{Vansummeren2006} and adapted the
  POSIX definition given there for the algorithm by Sulzmann and Lu made all
  the difference: the proofs, as said, are nearly straightforward. The
  question remains whether the original proof idea of \cite{Sulzmann2014},
  potentially using our result as a stepping stone, can be made to work?
  Alas, we really do not know despite considerable effort.


  Closely related to our work is an automata-based lexer formalised by
  Nipkow \cite{Nipkow98}. This lexer also splits up strings into longest
  initial substrings, but Nipkow's algorithm is not completely
  computational. The algorithm by Sulzmann and Lu, in contrast, can be
  implemented with ease in any functional language. A bespoke lexer for the
  Imp-language is formalised in Coq as part of the Software Foundations book
  by Pierce et al \cite{Pierce2015}. The disadvantage of such bespoke lexers is that they
  do not generalise easily to more advanced features.
  Our formalisation is available from the Archive of Formal Proofs \cite{aduAFP16}
  under \url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}.\medskip

 \noindent
  {\bf Acknowledgements:}
  We are very grateful to Martin Sulzmann for his comments on our work and 
  moreover for patiently explaining to us the details in \cite{Sulzmann2014}. We
  also received very helpful comments from James Cheney and anonymous referees.
  %  \small
  \bibliographystyle{plain}
  \bibliography{root}

*}

(*<*)
end
(*>*)