equal
deleted
inserted
replaced
696 \end{center} |
696 \end{center} |
697 Sulzmann and Lu used a binary predicate, written $\vdash v:r $, |
697 Sulzmann and Lu used a binary predicate, written $\vdash v:r $, |
698 to indicate that a value $v$ could be generated from a lexing algorithm |
698 to indicate that a value $v$ could be generated from a lexing algorithm |
699 with input $r$. They call it the value inhabitation relation, |
699 with input $r$. They call it the value inhabitation relation, |
700 defined by the rules. |
700 defined by the rules. |
701 \begin{figure}[H]\label{fig:inhab} |
701 \begin{figure}[H] |
702 \begin{mathpar} |
702 \begin{mathpar} |
703 \inferrule{\mbox{}}{\vdash \Char \; c : \mathbf{c}} \hspace{2em} |
703 \inferrule{\mbox{}}{\vdash \Char \; c : \mathbf{c}} \hspace{2em} |
704 |
704 |
705 \inferrule{\mbox{}}{\vdash \Empty : \ONE} \hspace{2em} |
705 \inferrule{\mbox{}}{\vdash \Empty : \ONE} \hspace{2em} |
706 |
706 |
710 |
710 |
711 \inferrule{\vdash v_2 : r_2}{\vdash \Right \; v_2:r_1 + r_2} |
711 \inferrule{\vdash v_2 : r_2}{\vdash \Right \; v_2:r_1 + r_2} |
712 |
712 |
713 \inferrule{\forall v \in vs. \vdash v:r \land |v| \neq []}{\vdash \Stars \; vs : r^*} |
713 \inferrule{\forall v \in vs. \vdash v:r \land |v| \neq []}{\vdash \Stars \; vs : r^*} |
714 \end{mathpar} |
714 \end{mathpar} |
715 \caption{The inhabitation relation for values and regular expressions} |
715 \caption{The inhabitation relation for values and regular expressions}\label{fig:inhab} |
716 \end{figure} |
716 \end{figure} |
717 \noindent |
717 \noindent |
718 The condition $|v| \neq []$ in the premise of star's rule |
718 The condition $|v| \neq []$ in the premise of star's rule |
719 is to make sure that for a given pair of regular |
719 is to make sure that for a given pair of regular |
720 expression $r$ and string $s$, the number of values |
720 expression $r$ and string $s$, the number of values |