--- a/thys/Paper/Paper.thy Sun Mar 06 16:51:32 2016 +0000
+++ b/thys/Paper/Paper.thy Sun Mar 06 18:40:43 2016 +0000
@@ -13,8 +13,8 @@
notation (latex output)
If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
- Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,75] 73) and
-
+ Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,75] 73) and
+
ZERO ("\<^bold>0" 78) and
ONE ("\<^bold>1" 78) and
CHAR ("_" [1000] 80) and
@@ -38,6 +38,7 @@
mkeps ("mkeps _" [79] 76) and
projval ("proj _ _ _" [1000,77,1000] 77) and
length ("len _" [78] 73) and
+ matcher ("lexer _ _" [78,78] 77) and
Prf ("\<triangleright> _ : _" [75,75] 75) and
PMatch ("'(_, _') \<rightarrow> _" [63,75,75] 75)
@@ -463,26 +464,26 @@
the shape of values.
\begin{center}
- \begin{tabular}{lcl}
- @{thm (lhs) injval.simps(1)[of "d" "DUMMY"]} & $\dn$ & @{thm (rhs) injval.simps(1)}\\
- @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ &
+ \begin{tabular}{llcl}
+ (1) & @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\
+ (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"]}\\
- @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ &
+ (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"]}\\
- @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$
+ (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"]}\\
- @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$
+ (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"]}\\
- @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$
+ (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"]}\\
- @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$
+ (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}
\noindent To better understand what is going on in this definition it
might be instructive to look first at the three sequence cases (clauses
- 4--6). In each case we need to construct an ``injected value'' for @{term
+ (4)--(6)). In each case we need to construct an ``injected value'' for @{term
"SEQ r\<^sub>1 r\<^sub>2"}. Recall the clause of the @{const der}-function
for sequence regular expressions:
@@ -492,18 +493,39 @@
\noindent Consider first the else-branch where the derivative is @{term
"SEQ (der c r\<^sub>1) r\<^sub>2"}. The corresponding value must therefore
- be the form @{term "Seq v\<^sub>1 v\<^sub>2"}, which matches the fourth
- clause of @{term inj}. In the if-branch the derivative is an alternative,
- namely @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2)"}.
- This means we either have to consider a @{text Left}- or @{text
- Right}-value. In case of the @{text Left}-value we know further it must be
- a value for a sequence regular expression. Therefore the pattern we
- match in the fifth clause is @{term "Left (Seq v\<^sub>1 v\<^sub>2)"}, while
- in the sixth it is just @{term "Right v\<^sub>2"}. One more interesting point
- is in the right-hand side of the sixth clause: since in this case the regular
- expression @{text "r\<^sub>1"} does not ``contribute'' in matching the string,
- that is only matches the empty string, we need to call @{const mkeps} in order
- to construct a value how @{term "r\<^sub>1"} can match this empty string.
+ be the form @{term "Seq v\<^sub>1 v\<^sub>2"}, which matches clause (4) of
+ @{term inj}. In the if-branch the derivative is an alternative, namely
+ @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2)"}. This
+ means we either have to consider a @{text Left}- or @{text Right}-value.
+ In case of the @{text Left}-value we know further it must be a value for a
+ sequence regular expression. Therefore the pattern we match in the clause
+ (5) is @{term "Left (Seq v\<^sub>1 v\<^sub>2)"}, while in (6) it is just
+ @{term "Right v\<^sub>2"}. One more interesting point is in the right-hand
+ side of clause (6): since in this case the regular expression @{text
+ "r\<^sub>1"} does not ``contribute'' in matching the string, that is only
+ matches the empty string, we need to call @{const mkeps} in order to
+ construct a value how @{term "r\<^sub>1"} can match this empty string. A
+ similar argument applies for why we can expect in clause (7) that the
+ value is of the form @{term "Seq v (Stars vs)"} (the derivative of a star
+ is @{term "SEQ r (STAR r)"}). Finally, the reason for why we can ignore
+ the second argument in clause (1) of @{term inj} is that it will only ever
+ be called in cases where @{term "c=d"}, but the usual linearity
+ restrictions in pattern-matches do not allow is to build this constraint
+ explicitly into the pattern.
+
+ Having defined the @{const mkeps} and @{text inj} function we can extend
+ \Brz's matcher so that a [lexical] value is constructed (assuming the
+ regular expression matches the string). The clauses of the lexer are
+
+ \begin{center}
+ \begin{tabular}{lcl}
+ @{thm (lhs) matcher.simps(1)} & $\dn$ & @{thm (rhs) matcher.simps(1)}\\
+ @{thm (lhs) matcher.simps(2)} & $\dn$ & @{text "case"} @{term "matcher (der c r) s"} @{text of}\\
+ & & \phantom{$|$} @{term "None"} @{text "\<Rightarrow>"} @{term None}\\
+ & & $|$ @{term "Some v"} @{text "\<Rightarrow>"} @{term "Some (injval r c v)"}
+ \end{tabular}
+ \end{center}
+
NOT DONE YET