657 & |
657 & |
658 \begin{tabular}{@{\hspace{0mm}}rrl@{}} |
658 \begin{tabular}{@{\hspace{0mm}}rrl@{}} |
659 \multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\ |
659 \multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\ |
660 $v$ & $::=$ & \\ |
660 $v$ & $::=$ & \\ |
661 & & $\Empty$ \\ |
661 & & $\Empty$ \\ |
662 & $\mid$ & $\Char(c)$ \\ |
662 & $\mid$ & $\Char \; c$ \\ |
663 & $\mid$ & $\Seq\,v_1\, v_2$\\ |
663 & $\mid$ & $\Seq\,v_1\, v_2$\\ |
664 & $\mid$ & $\Left(v)$ \\ |
664 & $\mid$ & $\Left \;v$ \\ |
665 & $\mid$ & $\Right(v)$ \\ |
665 & $\mid$ & $\Right\;v$ \\ |
666 & $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\ |
666 & $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\ |
667 \end{tabular} |
667 \end{tabular} |
668 \end{tabular} |
668 \end{tabular} |
669 \end{center} |
669 \end{center} |
670 \noindent |
670 \noindent |
672 can be calculated by the ``flatten" function $|\_|$: |
672 can be calculated by the ``flatten" function $|\_|$: |
673 \begin{center} |
673 \begin{center} |
674 \begin{tabular}{lcl} |
674 \begin{tabular}{lcl} |
675 $|\Empty|$ & $\dn$ & $[]$\\ |
675 $|\Empty|$ & $\dn$ & $[]$\\ |
676 $|\Char \; c|$ & $ \dn$ & $ [c]$\\ |
676 $|\Char \; c|$ & $ \dn$ & $ [c]$\\ |
677 $|\Seq(v_1, v_2)|$ & $ \dn$ & $ v_1| @ |v_2|$\\ |
677 $|\Seq \; v_1, \;v_2|$ & $ \dn$ & $ v_1| @ |v_2|$\\ |
678 $|\Left(v)|$ & $ \dn$ & $ |v|$\\ |
678 $|\Left \; v|$ & $ \dn$ & $ |v|$\\ |
679 $|\Right(v)|$ & $ \dn$ & $ |v|$\\ |
679 $|\Right \; v|$ & $ \dn$ & $ |v|$\\ |
680 $|\Stars([])|$ & $\dn$ & $[]$\\ |
680 $|\Stars \; []|$ & $\dn$ & $[]$\\ |
681 $|\Stars(v::vs)|$ & $\dn$ & $ |v| @ |\Stars(vs)|$ |
681 $|\Stars \; v::vs|$ & $\dn$ & $ |v| @ |\Stars(vs)|$ |
682 \end{tabular} |
682 \end{tabular} |
683 \end{center} |
683 \end{center} |
684 Sulzmann and Lu used a binary predicate, written $\vdash v:r $, |
684 Sulzmann and Lu used a binary predicate, written $\vdash v:r $, |
685 to indicate that a value $v$ could be generated from a lexing algorithm |
685 to indicate that a value $v$ could be generated from a lexing algorithm |
686 with input $r$. They call it the value inhabitation relation. |
686 with input $r$. They call it the value inhabitation relation. |
687 \begin{mathpar} |
687 \begin{mathpar} |
688 \inferrule{\mbox{}}{\vdash \Char(c) : \mathbf{c}} \hspace{2em} |
688 \inferrule{\mbox{}}{\vdash \Char \; c : \mathbf{c}} \hspace{2em} |
689 |
689 |
690 \inferrule{\mbox{}}{\vdash \Empty : \ONE} \hspace{2em} |
690 \inferrule{\mbox{}}{\vdash \Empty : \ONE} \hspace{2em} |
691 |
691 |
692 \inferrule{\vdash v_1 : r_1 \;\; \vdash v_2 : r_2 }{\vdash \Seq(v_1, v_2) : (r_1 \cdot r_2)} |
692 \inferrule{\vdash v_1 : r_1 \;\; \vdash v_2 : r_2 }{\vdash \Seq \; v_1,\; v_2 : (r_1 \cdot r_2)} |
693 |
693 |
694 \inferrule{\vdash v_1 : r_1}{\vdash \Left(v_1):r_1+r_2} |
694 \inferrule{\vdash v_1 : r_1}{\vdash \Left \; v_1 : r_1+r_2} |
695 |
695 |
696 \inferrule{\vdash v_2 : r_2}{\vdash \Right(v_2):r_1 + r_2} |
696 \inferrule{\vdash v_2 : r_2}{\vdash \Right \; v_2:r_1 + r_2} |
697 |
697 |
698 \inferrule{\forall v \in vs. \vdash v:r \land |v| \neq []}{\vdash \Stars(vs):r^*} |
698 \inferrule{\forall v \in vs. \vdash v:r \land |v| \neq []}{\vdash \Stars \; vs : r^*} |
699 \end{mathpar} |
699 \end{mathpar} |
700 \noindent |
700 \noindent |
701 The condition $|v| \neq []$ in the premise of star's rule |
701 The condition $|v| \neq []$ in the premise of star's rule |
702 is to make sure that for a given pair of regular |
702 is to make sure that for a given pair of regular |
703 expression $r$ and string $s$, the number of values |
703 expression $r$ and string $s$, the number of values |