11 abbreviation |
11 abbreviation |
12 "ders_syn r s \<equiv> ders s r" |
12 "ders_syn r s \<equiv> ders s r" |
13 |
13 |
14 notation (latex output) |
14 notation (latex output) |
15 If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and |
15 If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and |
16 Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,75] 73) and |
16 Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,75] 73) and |
17 |
17 |
18 ZERO ("\<^bold>0" 78) and |
18 ZERO ("\<^bold>0" 78) and |
19 ONE ("\<^bold>1" 78) and |
19 ONE ("\<^bold>1" 78) and |
20 CHAR ("_" [1000] 80) and |
20 CHAR ("_" [1000] 80) and |
21 ALT ("_ + _" [77,77] 78) and |
21 ALT ("_ + _" [77,77] 78) and |
22 SEQ ("_ \<cdot> _" [77,77] 78) and |
22 SEQ ("_ \<cdot> _" [77,77] 78) 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 |
39 projval ("proj _ _ _" [1000,77,1000] 77) and |
39 projval ("proj _ _ _" [1000,77,1000] 77) and |
40 length ("len _" [78] 73) and |
40 length ("len _" [78] 73) and |
|
41 matcher ("lexer _ _" [78,78] 77) and |
41 |
42 |
42 Prf ("\<triangleright> _ : _" [75,75] 75) and |
43 Prf ("\<triangleright> _ : _" [75,75] 75) and |
43 PMatch ("'(_, _') \<rightarrow> _" [63,75,75] 75) |
44 PMatch ("'(_, _') \<rightarrow> _" [63,75,75] 75) |
44 (* and ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73) *) |
45 (* and ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73) *) |
45 |
46 |
461 "v\<^sub>1"} corresponding to the input regular expression. The @{term |
462 "v\<^sub>1"} corresponding to the input regular expression. The @{term |
462 inj} function is by recursion on the regular expression and by analysing |
463 inj} function is by recursion on the regular expression and by analysing |
463 the shape of values. |
464 the shape of values. |
464 |
465 |
465 \begin{center} |
466 \begin{center} |
466 \begin{tabular}{lcl} |
467 \begin{tabular}{llcl} |
467 @{thm (lhs) injval.simps(1)[of "d" "DUMMY"]} & $\dn$ & @{thm (rhs) injval.simps(1)}\\ |
468 (1) & @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\ |
468 @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & |
469 (2) & @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & |
469 @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\ |
470 @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\ |
470 @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & |
471 (3) & @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & |
471 @{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
472 @{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
472 @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
473 (4) & @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
473 & @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
474 & @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
474 @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
475 (5) & @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
475 & @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
476 & @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
476 @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ |
477 (6) & @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ |
477 & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
478 & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
478 @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$ |
479 (7) & @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$ |
479 & @{thm (rhs) injval.simps(7)[of "r" "c" "v" "vs"]}\\ |
480 & @{thm (rhs) injval.simps(7)[of "r" "c" "v" "vs"]}\\ |
480 \end{tabular} |
481 \end{tabular} |
481 \end{center} |
482 \end{center} |
482 |
483 |
483 \noindent To better understand what is going on in this definition it |
484 \noindent To better understand what is going on in this definition it |
484 might be instructive to look first at the three sequence cases (clauses |
485 might be instructive to look first at the three sequence cases (clauses |
485 4--6). In each case we need to construct an ``injected value'' for @{term |
486 (4)--(6)). In each case we need to construct an ``injected value'' for @{term |
486 "SEQ r\<^sub>1 r\<^sub>2"}. Recall the clause of the @{const der}-function |
487 "SEQ r\<^sub>1 r\<^sub>2"}. Recall the clause of the @{const der}-function |
487 for sequence regular expressions: |
488 for sequence regular expressions: |
488 |
489 |
489 \begin{center} |
490 \begin{center} |
490 @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} $\dn$ @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} |
491 @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} $\dn$ @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} |
491 \end{center} |
492 \end{center} |
492 |
493 |
493 \noindent Consider first the else-branch where the derivative is @{term |
494 \noindent Consider first the else-branch where the derivative is @{term |
494 "SEQ (der c r\<^sub>1) r\<^sub>2"}. The corresponding value must therefore |
495 "SEQ (der c r\<^sub>1) r\<^sub>2"}. The corresponding value must therefore |
495 be the form @{term "Seq v\<^sub>1 v\<^sub>2"}, which matches the fourth |
496 be the form @{term "Seq v\<^sub>1 v\<^sub>2"}, which matches clause (4) of |
496 clause of @{term inj}. In the if-branch the derivative is an alternative, |
497 @{term inj}. In the if-branch the derivative is an alternative, namely |
497 namely @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2)"}. |
498 @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2)"}. This |
498 This means we either have to consider a @{text Left}- or @{text |
499 means we either have to consider a @{text Left}- or @{text Right}-value. |
499 Right}-value. In case of the @{text Left}-value we know further it must be |
500 In case of the @{text Left}-value we know further it must be a value for a |
500 a value for a sequence regular expression. Therefore the pattern we |
501 sequence regular expression. Therefore the pattern we match in the clause |
501 match in the fifth clause is @{term "Left (Seq v\<^sub>1 v\<^sub>2)"}, while |
502 (5) is @{term "Left (Seq v\<^sub>1 v\<^sub>2)"}, while in (6) it is just |
502 in the sixth it is just @{term "Right v\<^sub>2"}. One more interesting point |
503 @{term "Right v\<^sub>2"}. One more interesting point is in the right-hand |
503 is in the right-hand side of the sixth clause: since in this case the regular |
504 side of clause (6): since in this case the regular expression @{text |
504 expression @{text "r\<^sub>1"} does not ``contribute'' in matching the string, |
505 "r\<^sub>1"} does not ``contribute'' in matching the string, that is only |
505 that is only matches the empty string, we need to call @{const mkeps} in order |
506 matches the empty string, we need to call @{const mkeps} in order to |
506 to construct a value how @{term "r\<^sub>1"} can match this empty string. |
507 construct a value how @{term "r\<^sub>1"} can match this empty string. A |
|
508 similar argument applies for why we can expect in clause (7) that the |
|
509 value is of the form @{term "Seq v (Stars vs)"} (the derivative of a star |
|
510 is @{term "SEQ r (STAR r)"}). Finally, the reason for why we can ignore |
|
511 the second argument in clause (1) of @{term inj} is that it will only ever |
|
512 be called in cases where @{term "c=d"}, but the usual linearity |
|
513 restrictions in pattern-matches do not allow is to build this constraint |
|
514 explicitly into the pattern. |
|
515 |
|
516 Having defined the @{const mkeps} and @{text inj} function we can extend |
|
517 \Brz's matcher so that a [lexical] value is constructed (assuming the |
|
518 regular expression matches the string). The clauses of the lexer are |
|
519 |
|
520 \begin{center} |
|
521 \begin{tabular}{lcl} |
|
522 @{thm (lhs) matcher.simps(1)} & $\dn$ & @{thm (rhs) matcher.simps(1)}\\ |
|
523 @{thm (lhs) matcher.simps(2)} & $\dn$ & @{text "case"} @{term "matcher (der c r) s"} @{text of}\\ |
|
524 & & \phantom{$|$} @{term "None"} @{text "\<Rightarrow>"} @{term None}\\ |
|
525 & & $|$ @{term "Some v"} @{text "\<Rightarrow>"} @{term "Some (injval r c v)"} |
|
526 \end{tabular} |
|
527 \end{center} |
|
528 |
507 |
529 |
508 |
530 |
509 NOT DONE YET |
531 NOT DONE YET |
510 |
532 |
511 Therefore there are, for example, three |
533 Therefore there are, for example, three |