% Copyright 2012-2024, Alexander Shibakov % This file is part of SPLinT % % SPLinT is free software: you can redistribute it and/or modify % it under the terms of the GNU General Public License as published by % the Free Software Foundation, either version 3 of the License, or % (at your option) any later version. % % SPLinT is distributed in the hope that it will be useful, % but WITHOUT ANY WARRANTY; without even the implied warranty of % MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the % GNU General Public License for more details. % % You should have received a copy of the GNU General Public License % along with SPLinT. If not, see . % parsing \TeX\ input for pretty-printing; % scanning and parsing are both done by using a low-level % finite automaton; \def\yygetchar{% single buffered input \ifyytextbackup \yybyte\yytextseen \yycp@\yytextseenlastchar \yytextbackupfalse \let\next\yyreturn \else \let\next\yyinput \fi \next } % \TeX\ input \def\texdefaultstate{% <>+-()^~!?*[]:.,`'\%\$\_ \raw digit letter \raw {% \putother\yycp@\in\yybyte \appendyybyte} = {% \appendrnx\texlinetoks{{}${}={}${}}% \yygetchar } \{ {% \putother\yycp@\in\yybyte \appendl\yybyte{\noexpand\bbal[\the\bbalance]}% \advance\bbalance1\relax \appendyybyte} \} {% \putother\yycp@\in\yybyte \advance\bbalance-1\relax \appendl\yybyte{\noexpand\bbal[\the\bbalance]}% \appendyybyte} 0123456789 {% \expandafter\ifcat\expandafter\noexpand\the\yybyte1% \def\next{digit}% \else \def\next{^^A}% \fi \switchon\next\in\texdefaultstate } ^^A % \yycp@==1 {% \edef\next{\noexpand\noexpand\the\yybyte}% \switchon\next\in\texdefaultstate} \raw\hbox\raw {% \appendnext} \raw\end\raw {% \relax} \raw\\ \_ \raw {% \appendyybyte} \ \ {% \appendyybyte} \\ {% \getcescape } / \raw escape \raw {% \let\currentstate\texcsname \yygetchar} }% \def\texcsname{% <>+-()^~!?*\{\}[]:.,`'=\%\$\_/ 0123456789 ^^A \ \ \raw \end \\ \_ \ \raw \raw escape \raw {% \let\currentstate\texdefaultstate \putother\yycp@\in\yytext \outputtexcs \yygetchar} % \\ {% \getcescape } \raw letter \raw {% \let\currentstate\texcsnamelong \yytext\yybyte \yygetchar} }% \def\texcsnamelong{% <>+-()^~!?*\{\}[]:.,`'=\%\$\_\& 0123456789 ^^A \ \ \raw \end \\ \_ \raw {% \let\currentstate\texdefaultstate \yytextseenlastchar=\yycp@ \yytextseen=\yybyte \yytextbackuptrue \outputtexcs \yygetchar} \\ {% \getcescape } / \raw escape \raw {% \let\currentstate\texcsname \outputtexcs \yygetchar} \raw letter \raw {% \concat\yytext\yybyte \yygetchar} }% \def\texcescape{% \\ {% \let\currentstate\esccurrentstate \yycp@=`\\% \putother\yycp@\in\yybyte \def\next{escape}% \switchon\next\in\currentstate} } \def\texescdefault{% \let\currentstate\esccurrentstate \yycp@=`\ % \yybyte{\ }% \caction\yycp@\in\currentstate } \def\getcescape{% \let\esccurrentstate\currentstate \let\currentstate\texcescape \let\default\texescdefault \yygetchar } \setspecialcharsfrom\texdefaultstate \setspecialcharsfrom\texcsname \setspecialcharsfrom\texcsnamelong \setspecialcharsfrom\texcescape \newtoks\texlinetoks % parsed \TeX\ tokens \newtoks\texidxtoks % indexing commands \def\texlexer{% \let\default\yygetchar \let\next\yycp@ \ifnum\yycp@>"20 % \ifnum\yycp@<"7F % a character \expandafter\ifcat\expandafter\noexpand\the\yybyte a% % this test allows one some control over what constitutes a control % sequence name (by saying, for example, \let\$a or manipulating \catcodes) % this is bordering on a bug \def\next{letter}% \fi \fi \fi \switchonwithtype\next\in\currentstate } \def\outputtexcs{% \expandafter\ifx\csname\defprefix\the\yytext\defpostfix\endcsname\relax %\putother{`\\}\in\toksa \toksa{\hbox{\sixpoint\tt\char`\\}}% \concat\texlinetoks\toksa \concat\texlinetoks\yytext \appendrnx\texlinetoks{\hbox{$\,$}}% \toksb{}% no visual key \else \appendr\texlinetoks{\expandafter\noexpand\csname\defprefix\the\yytext\defpostfix\endcsname}% \expandafter\ifx\csname\restorecsxname{index:visual}{.\the\yytext}\endcsname\relax \toksb{}% no visual key \else \toksb\expandafter\expandafter\expandafter{\csname\restorecsxname{index:visual}{.\the\yytext}\endcsname}% \fi \fi \appendr\texidxtoks{\gidxentryxb{\texcsstring}{\the\yytext}{\the\toksb}}% } % indexing of \TeX\ control sequences \def\texidxdomain{T} \def\texcsidxrank{2} \def\texcstxtidxrank{5} \def\writetexidxentry#1{\indxe\gindex{{\secno}{{}{\texispace}}{\texidxdomain}{\texcsidxrank}#1}} \def\writetextxtidxentry#1{\indxe\gindex{{\secno}{{}{\texispace}}{\texidxdomain}{\texcstxtidxrank}#1}} \def\appendyybyte{\concat\texlinetoks\yybyte\yygetchar} \def\appendnext#1{\toksa{#1}\concat\texlinetoks\toksa\yygetchar} \def\defTpostfix{[xTeXmode]} \def\stripyybyte{% \expandafter\stripyyb@te\the\yybyte } \def\stripyyb@te#1#2{\noexpand#2} % TODO: % the macros below are in their present shape due to the forces of `historical evolution': % \TeX\ pretty printing needs to be completely rewritten, however, the existing macros % do a passable job so they remain in this rather random shape. % the items below need more urgent attention: % % o introduce TeXn_ that take a number and a string argument \newcount\bbalance \newif\iftracetexpp \newtoks\textoks % the most common way for a \TeX? macro to appear in in the input is being inserted by % \CWEB\ itself; in this case \CWEB\ makes sure that the macro is expanded in math mode; % this assumption is relied upon in the design of these macros, and violating it may % result in sume rather puzzling error messages due to the insertion of % \ignorespaces outside of the current group; the warning macro below makes this % dependence explicit. \def\TeXxwarn{% \relax \ifmmode \else \errhelp{Check stash collecting macros.}% \errmessage{\nx\\TeXx macro is used outside of math mode.}% \fi } \def\TeXx(#1);{% TODO \TeXxwarn {}$\let\oldttdot\.\relaxcweb \let\.\dotcollect \textoks{}% \setbox\z@=\hbox{#1\expandafter}\expandafter \textoks\expandafter{\the\textoks}% \restorecweb\let\.\oldttdot \expandafter\T@Xx\the\textoks {}${}\aftergroup\ignorespaces} \def\BZ(#1){} \def\mypar{\par} \def\TeXb(#1)#2;{% TeX material begin \TeXxwarn {}$\let\oldttdot\.\relaxcweb \toksa{}\let\.\dotcollectb \textoks{}% \let\oldsix\6% \let\6\ignorespaces \let\oldC\C \let\C\saveCcomments #1% \restorecweb\let\.\oldttdot \dotcollectstripquotes ${}\aftergroup\ignorespaces} \def\TeXa(#1)#2;{% TeX material add (stitch the \TeX\ chunks together) \TeXxwarn {}$\let\oldttdot\.\relaxcweb \toksa{}\let\.\dotcollectb #1% \restorecweb\let\.\oldttdot \dotcollectstripquotes ${}\aftergroup\ignorespaces} \def\TeXf(#1)#2;{% TeX material add (output each chunk on a separate line) \TeXxwarn {}$\let\oldttdot\.\relaxcweb \toksa{}\let\.\dotcollectb \textoks\expandafter{\the\textoks\hbox{\6}}% #1% \restorecweb\let\.\oldttdot \dotcollectstripquotes ${}\aftergroup\ignorespaces} \def\TeXao(#1)#2;{% TeX material output (stitch the \TeX\ chunks together) \TeXxwarn {}$\let\oldttdot\.\relaxcweb \toksa{}\let\.\dotcollectb \let\6\oldsix \let\C\oldC #1% \restorecweb\let\.\oldttdot \dotcollectstripquotes \expandafter\T@Xx\expandafter "\the\textoks"{}${}\aftergroup\ignorespaces} \def\TeXfo(#1)#2;{% TeX material output (output each chunk on a separate line) \TeXxwarn {}$\let\oldttdot\.\relaxcweb \toksa{}\let\.\dotcollectb \textoks\expandafter{\the\textoks\hbox{\6}}% \let\6\oldsix \let\C\oldC #1% \restorecweb\let\.\oldttdot \dotcollectstripquotes \expandafter\T@Xx\expandafter "\the\textoks"{}${}\aftergroup\ignorespaces} \let\TeXxx\TeXx \let\TeXaxx\TeXa \let\TeXbxx\TeXb \let\TeXaoxx\TeXao \let\TeXfxx\TeXf \let\TeXxi\TeXx \def\inlineTeXx#1{{\let\writetexidxentry\writetextxtidxentry$\TeXxi(\.{"#1"});$}} % for indexing macros \def\texref#1{% convenient shortcut {% \def\texnspace{texline}\def\texispace{index:tex}\inlineTeXx{#1}% }% } \def\texrefx#1#2{% convenient shortcut {% \def\texnspace{#2}\def\texispace{index:tex}\inlineTeXx{#1}% }% } \def\TeXlit{\iffalse{\fi}{\setbox0\lastbox}\removewhitespace \expandafter\.\expandafter{\iffalse}\fi} % to help with \CWEB's @t...@> cleanup % e.g.\ |TeXao(@t\TeXlit"\hbox{\TeX\ stuff}"@>);| \def\dotcollect#1{\toksa{#1}\concat\textoks\toksa} \def\dotcollectb#1{\toksb{#1}\concat\toksa\toksb} \def\dotcollectstripquotes{\expandafter\d@tcollectstripquotes\the\toksa} \def\d@tcollectstripquotes"#1"{\toksa{#1}\concat\textoks\toksa} \def\saveCcomments#1{\toksc{\hbox{\oldC{#1}}}\concat\textoks\toksc} \def\relaxcweb{\savehcs{local-namespace}{\)}} \def\restorecweb{\restorecs{local-namespace}{\)}} \def\T@Xx"#1"{% \iffalse{\fi % alignment! \begingroup % tune up the standard input routines \let\yyreturn\texlexer \let\multicharswitch\empty \let\onecharswitch\empty \setspecialcharsfrom\multicharswitch % debugging \setspecialcharsfrom\onecharswitch % \let\currentstate\texdefaultstate \texlinetoks{}\texidxtoks{}\bbalance\z@ \let\bbal\bbalempty \yytextbackupfalse \let\defpostfix\defTpostfix\let\defprefix\empty \restorecsxlist\texnspace\alltexsymbols \let\termindex\writetexidxentry \yygetchar#1\end \iftracetexpp{\newlinechar=`^^J% \toksc{#1}\ferrmessage{TeX_ input: \the\toksc^^JTeX_ first pass: \the\texlinetoks}}\fi \ifnum\bbalance=\z@ \else \bbbalance{#1}% \fi \iftracetexpp\ferrmessage{TeX_ final pass: \the\texlinetoks (idx: \the\texidxtoks)}\fi \concat\texlinetoks\texidxtoks \expandafter \endgroup \expandafter \begingroup % the actual typesetting must happen outside the group % otherwise there is a risk that an output routine is called before % the group is complete and \yyreturn definition is wrong so \yyparse % will not be able to function \expandafter\T@Xpretypeset\the\texlinetoks \endgroup \iffalse}\fi } \def\T@Xpretypeset{% \let\bbal\bbalempty\bbalance\z@ \let\defpostfix\defTpostfix\let\defprefix\empty \restorecsxlist\texnspace\alltexsymbols \tt\chardef\_=`\_% } \def\alltexsymbols{% \space\toksa\toksb\toksc\toksd\tokse\toksf\toksg\toksh\the\ifx \ifnum\fi\else\def\edef\let\empty\next\switchon\in\concat\appendr \default\noexpand\emptyterm\print\relax\yy\inmath\omit\hfil\getfirst \getsecond\getthird\getfourth\getfifth\nx\to\hspace\rhscont\rhscnct \rhsbool\table\ifrhsfull\rhsfulltrue\rhsfullfalse\yyval\tempca \tempcb\z@\@ne\tw@\m@ne\advance\ifcat\iftracebadchars\bb \yylexreturnptr\yylexreturn\yylexreturnval\yylexreturnsym \yylexreturnchar\yylexreturnxchar\yylexreturntext\yylexnext \%\harmlesscomment\\\yyfatal\yywarn\yyBEGIN\yypushstate\yypopstate \yyBEGINr\yylexstate\yypdeprecated } % TODO: make this the mechanism for updating \alltexsymbols \def\extendcs#1\with#2{% \expandafter\def\expandafter#1\expandafter{#1#2}% } \def\collectspaces#1{% \def\next{#1}% \ifx#1\endcontainer \let\next\relax \else \ifx\next\spacecontainer \appendr\toksa\next \let\next\collectspaces \else \let\next\eattoend \fi \fi \next } \def\spacecontainer{\ } \def\texnspace{texline} \def\texispace{index:tex} \let\defpostfix\defTpostfix \let\defprefix\empty \let\settgroup\relax \defx\space{\hbox{$\,$\char`\ $\,$}}{texline} \defy\space{\hbox{$\,$\char`\ $\,$}}{index:tex} \defx\hspace{% somewhat precarious definition \hbox{\char`\ }% \def\setegroup{{}$\,${}}% \def\setpgr@up{^{\hbox{\sscmd\the\toksa}}\,$}% \def\setegr@up{\,$}% \def\setpgroup{% ${}_{\hbox{\sscmd\the\toksa}}% \let\setpgroup\setpgr@up \let\setegroup\setegr@up \grabbalanced }\grabbalanced }{texline} \defy\hspace{\hbox{$\,$\char`\ $\,$}}{index:tex} \defx\advance{% $\mathop{\hbox{\bf add}}$% }{texline} \defy\advance{% {\bf add}% }{index:tex} \defx\z@{% $\,0_{\rm R}\,$% }{texline} \defy\z@{% $0_{\rm R}$% }{index:tex} \defx\z@{0_R}{index:visual} \defx\@ne{% $\,1_{\rm R}\,$% }{texline} \defy\@ne{% $1_{\rm R}$% }{index:tex} \defx\@ne{1_R}{index:visual} \defx\tw@{% $\,2_{\rm R}\,$% }{texline} \defy\tw@{% $2_{\rm R}$% }{index:tex} \defx\tw@{2_R}{index:visual} \defx\m@ne{% $\,-1_{\rm R}\,$% }{texline} \defy\m@ne{% $-1_{\rm R}$% }{index:tex} \defx\m@ne{-1_R}{index:visual} \defx\tempca{% $t_a$% }{texline} \defy\tempca{% $t_a$% }{index:tex} \defx\tempca{t_a}{index:visual} \defx\tempcb{% $t_b$% }{texline} \defy\tempcb{% $t_b$% }{index:tex} \defx\tempcb{t_b}{index:visual} \defx\toksa{% {}$v_a${}% \def\setegroup{}% \def\setpgroup{% $\leftarrow\langle\,\hbox{\the\toksa}% \if\next]% \else \,\rangle% \fi $}\grabbalanced }{texline} \defx\toksa{va}{index:visual} \defy\toksa{% $v_a$% }{index:tex} \defx\toksb{% {}$v_b${}% \def\setegroup{}% \def\setpgroup{% $\leftarrow\langle\,\hbox{\the\toksa}% \if\next]% \else \,\rangle% \fi $}\grabbalanced }{texline} \defx\toksb{vb}{index:visual} \defy\toksb{% $v_b$% }{index:tex} \defx\toksc{% {}$v_c${}% \def\setegroup{}% \def\setpgroup{% $\leftarrow\langle\,\hbox{\the\toksa}% \if\next]% \else \,\rangle% \fi $}\grabbalanced }{texline} \defx\toksc{vc}{index:visual} \defy\toksc{% $v_c$% }{index:tex} \defx\toksd{% {}$v_d${}% \def\setegroup{}% \def\setpgroup{% $\leftarrow\langle\,\hbox{\the\toksa}% \if\next]% \else \,\rangle% \fi $}\grabbalanced }{texline} \defx\toksd{vd}{index:visual} \defy\toksd{% $v_d$% }{index:tex} \defx\tokse{% {}$v_e${}% \def\setegroup{}% \def\setpgroup{% $\leftarrow\langle\,\hbox{\the\toksa}% \if\next]% \else \,\rangle% \fi $}\grabbalanced }{texline} \defx\tokse{ve}{index:visual} \defy\tokse{% $v_e$% }{index:tex} \defx\toksf{% {}$v_f${}% \def\setegroup{}% \def\setpgroup{% $\leftarrow\langle\,\hbox{\the\toksa}% \if\next]% \else \,\rangle% \fi $}\grabbalanced }{texline} \defx\toksf{vf}{index:visual} \defy\toksf{$v_f$}{index:tex} \defx\toksg{% {}$v_g${}% \def\setegroup{}% \def\setpgroup{% $\leftarrow\langle\,\hbox{\the\toksa}% \if\next]% \else \,\rangle% \fi $}\grabbalanced }{texline} \defx\toksg{vg}{index:visual} \defy\toksg{$v_g$}{index:tex} \defx\toksh{% {}$v_h${}% \def\setegroup{}% \def\setpgroup{% $\leftarrow\langle\,\hbox{\the\toksa}% \if\next]% \else \,\rangle% \fi $}\grabbalanced }{texline} \defx\toksh{vh}{index:visual} \defy\toksh{$v_h$}{index:tex} \defx\yyval{% {}$\Upsilon${}% \def\setegroup{}% \def\setpgroup{% $\leftarrow\langle\,\the\toksa \if\next]% \else \,\rangle% \fi $}\grabbalanced }{texline} \defy\yyval{% $\Upsilon$% }{index:tex} \defx\yyval{Y}{index:visual} \def\setcfreturn#1{% more flexible return statement \def\setegroup{{}$\mathop{\hbox{#1}}${}}% \let\settgroup\setegroup \def\setpgroup{% {% \let\termindex\writeidxentry % the indexed term is a \bison\ token \toksc\toksa \expandafter\nameproc\expandafter{\the\toksa}\with\parsebin \ifyyparsefail \edef\next{\toksa{\termmetastyle{% \gidxentryxb{\termvstring}{\the\toksa}{}% \let\nx\idxfont\nx\empty\nx\tt\the\toksa\nx\/% }}}\next \else \edef\next{\noexpand\settermstyle{\the\toksb}{\the\toksc}}\next \fi {}$\mathop{\hbox{#1}}\hbox{\the\toksa}${}}% }\grabbalanced } \def\setflexreturn#1{% \setcfreturn{{\bf return}#1}% } \defx\yylexreturnptr{% \setflexreturn{$_p${}}% }{texline} \defy\yylexreturnptr{% {\bf return$_p$}% }{index:tex} \defx\yylexreturnptr{return_p}{index:visual} \defx\yylexreturnxchar{% \setflexreturn{$_x${}}% }{texline} \defy\yylexreturnxchar{% \hbox{\bf return$_x$}% }{index:tex} \defx\yylexreturnxchar{return_x}{index:visual} \defx\yylexreturnchar{% \hbox{\bf return$_c$}% }{texline} \defy\yylexreturnchar{% \hbox{\bf return$_c$}% }{index:tex} \defx\yylexreturnchar{return_c}{index:visual} \defx\yylexnext{% {\bf continue}% }{texline} \defy\yylexnext{% {\bf continue}% }{index:tex} \defx\yylexnext{continue}{index:visual} \defx\yylexreturn{% \setflexreturn{$_l${}}% }{texline} \defy\yylexreturn{% {\bf return$_l$}% }{index:tex} \defx\yylexreturn{return_l}{index:visual} \defx\yylexreturnval{% \setflexreturn{$_v${}}% }{texline} \defy\yylexreturnval{% {\bf return$_v$}% }{index:tex} \defx\yylexreturnval{return_v}{index:visual} \defx\yylexreturnsym{% \setflexreturn{$_{vp}${}}% }{texline} \defy\yylexreturnsym{% {\bf return$_{vp}$}% }{index:tex} \defx\yylexreturnsym{return_vp}{index:visual} \defx\yylexreturntext{% {\bf return$_t$}% }{texline} \defy\yylexreturntext{% {\bf return$_t$}% }{index:tex} \defx\yylexreturntext{return_t}{index:visual} \defx\xcclreturn{% \setcfreturn{\bf set $\Upsilon$ {\rm and} return$^{\rm ccl}$}% }{texline} \defy\xcclreturn{% {\bf set $\Upsilon$ {\rm and} return$^{\rm ccl}$}% }{index:tex} \defx\xcclreturn{set U return^ccl}{index:visual} \defx\yyflexoptreturn{% \setflexreturn{$^{\rm opt}$}% }{texline} \defy\yyflexoptreturn{% {\bf return$^{\rm opt}$}% }{index:tex} \defx\yyflexoptreturn{return^opt}{index:visual} \extendcs\alltexsymbols\with{\xcclreturn\yyflexoptreturn} \defx\yyfatal{% {}$\mathop{\bf fatal}${}% \def\setegroup{}% \def\setpgroup{% $\langle\,\hbox{\the\toksa}% \if\next]% \else \,\rangle% \fi$% }\grabbalanced }{texline} \defx\yyfatal{fatal}{index:visual} \defy\yyfatal{% {\bf fatal}% }{index:tex} \defx\yywarn{% {}$\mathop{\bf warn}${}% \def\setegroup{}% \def\setpgroup{% $\langle\,\hbox{\the\toksa}% \if\next]% \else \,\rangle% \fi$% }\grabbalanced }{texline} \defx\yywarn{warn}{index:visual} \defy\yywarn{% {\bf warn}% }{index:tex} \defx\yypdeprecated{% {}$\mathop{\bf deprecated}${}% \def\setegroup{}% \def\setpgroup{% $\langle\,\hbox{\the\toksa}% \if\next]% \else \,\rangle% \fi$% }\grabbalanced }{texline} \defx\yypdeprecated{deprecated}{index:visual} \defy\yypdeprecated{% {\bf deprecated}% }{index:tex} \defx\table{{}$\Omega${}}{texline} \defy\table{$\Omega$}{index:tex} \defx\table{Omega}{index:visual} \defx\relax{\hbox{$\circ$}}{texline} \defy\relax{\hbox{$\circ$}}{index:tex} \defx\the#1{% \toksa{#1}% \let\prevdefault\default \def\default{\let\default\prevdefault{}$\mathop{\rm val}\,${}#1}% \taction{\the\toksa}\in\thecomaction }{texline} \defy\the{% $\mathop{\rm val}\cdot$ {\rm or }% \lcenclose{$\cdot$}% }{index:tex} \defx\the{val}{index:visual} \def\thecomaction{% \raw \toksaxTeXmode\toksbxTeXmode\tokscxTeXmode\toksdxTeXmode\toksexTeXmode\toksfxTeXmode \raw {% \let\default\prevdefault \lcenclose{\the\toksa}% }% } \setspecialcharsfrom\thecomaction \def\lcenclose#1{% {}$\llcorner\hbox{#1}\lrcorner${}% } \defx\inmath{% {}$^\bullet${}% \def\setegroup{}% \def\setpgroup{% $(\,\hbox{\the\toksa}% \if\next]% \else )% \fi $}\grabbalanced }{texline} \defy\inmath{% $^\bullet(\,\cdot\,)$% }{index:tex} \defx\ifx{% {\bf if$_{\rm x}\;$}% }{texline} \defy\ifx{% {\bf if$_{\rm x}$}% }{index:tex} \defx\ifnum{% {\bf if$_\omega\;$}% }{texline} \defy\ifnum{% {\bf if$_\omega$}% }{index:tex} \defx\ifcat{% {\bf if$_{\rm cat}\;$}% }{texline} \defy\ifcat{% {\bf if$_{\rm cat}$}% }{index:tex} \defx\iftracebadchars{% {\bf if$_t$ {\rm[{\tt bad char}]}$\;$}% }{texline} \defy\iftracebadchars{% {\bf if$_t$ {\rm[{\tt bad char}]}}% }{index:tex} \defx\else{% {\bf else$\;$}% }{texline} \defy\else{% {\bf else}% }{index:tex} \defx\fi{% {\bf fi$\;$}% }{texline} \defy\fi{% {\bf fi}% }{index:tex} \defx\def{% {\bf def$\;$}% }{texline} \defy\def{% {\bf def}% }{index:tex} \defx\edef{% {\bf def$_{\rm x}\;$}% }{texline} \defy\edef{% {\bf def$_{\rm x}$}% }{index:tex} \defx\edef{def_x}{index:visual} \defx\let{% {\bf let$\;$}% }{texline} \defx\next{% {\bf next$\;$}% }{texline} \defx\empty{% $\emptyset$% }{texline} \defy\empty{% $\emptyset$% }{index:tex} \defx\ifrhsfull{% {\bf if {\rm ($\,$rhs${}={}$full$\,$)}$\;$}% }{texline} \defy\ifrhsfull{% {\bf if {\rm ($\,$rhs${}={}$full$\,$)}}% }{index:tex} \defx\rhsfulltrue{% {\rm rhs${}={}$full$\,$}% }{texline} \defy\rhsfulltrue{% {\rm rhs${}={}$full}% }{index:tex} \defx\rhsfullfalse{% {\rm rhs${}={}$not full$\,$}% }{texline} \defy\rhsfullfalse{% {\rm rhs${}={}$not full}% }{index:tex} \defx\noexpand{% $^{\rm nox}$% }{texline} \defx\nx{% $^{\rm nx}$% }{texline} \defy\noexpand{% $^{\rm nox}$% }{index:tex} \defy\nx{% $^{\rm nx}$% }{index:tex} \defx\to{% ${}\mapsto{}$% }{texline} \defy\to{% $\mapsto$% }{index:tex} \defx\emptyterm{% \hbox{$\ulcorner\ldots\urcorner$}% }{texline} \defy\emptyterm{% \hbox{$\ulcorner\ldots\urcorner$}% }{index:tex} \defx\hfil{\hbox{$\,\Leftrightarrow\,$}}{texline} \defx\omit{\hbox{$\,{\times\atop\times}$}}{texline} \defx\yy#1{% \if\noexpand#1]% \let\next\seeksymtt \else \if\noexpand#1[% \let\next\seeksymts \else \if\noexpand#1(% \let\next\seeknott \else \def\next{\seeknots#1}% \fi \fi \fi \next }{texline} \defy\yy{% $\Upsilon\kern-1pt{}_{\rm?}$% }{index:tex} \defx\yy{Y_?}{index:visual} \def\seeknots#1\bbal{% \let\setegroup\relax \ifnum#1>0\relax \def\setpgroup{% \edef\next{\the\toksa}% \ifx\next\empty $\Upsilon\kern-1pt{}_{\number\tempca}$% \else $\Upsilon\kern-1pt{}_{\number\tempca}\rightarrow[{}${\tt\the\toksa}]$\;$% \fi}% \else \def\setpgroup{% $\Upsilon\leftarrow\langle{}${\tt\the\toksa}%${}% \if\next]% \else $\rangle\;$% \fi}% \fi \tempca#1\relax\printtermt } \def\seeksymts#1]{% \let\setegroup\relax \def\setpgroup{$\Upsilon\kern-1pt{}_{\rm#1}\langle{}${\tt\the\toksa}${}\rangle\;$}\grabbalanced } %\def\scriptswitch{\the\scriptfont0} \def\scriptswitch{% \sscmd\it \let\_\uscore % \let\acharswitch\textadustacharswitch } \def\seeksymtt#1[{{$\Upsilon\kern-1pt{}_{\rm#1}$}} \def\seeksymtt#1[{{$\Upsilon\kern-1pt{}_{\hbox{\scriptswitch\nameproc{#1}\with\parsebin\the\toksa}}$}} \def\seeksymtt#1[{{$\Upsilon\kern-1pt{}_{\hbox{\sscmd\prodstyle{#1}}}$}} \def\seeknott#1){{$\Upsilon\kern-1pt{}_{\rm#1}$}} \def\printtermt{\grabbalanced\bbal} \defx\print{% \hbox{\it print$\;$}% \def\setpgroup{{\tt"}\the\toksa{\tt"}$\,$}% \def\setegroup{}% \grabbalanced }{texline} \defx\bb#1\bbal{% \let\setegroup\relax \ifnum#1>0\relax \def\setpgroup{% \edef\next{\the\toksa}% \ifx\next\empty ${}_{\number\tempca}\kern-1.5pt\Upsilon$% \else ${}_{\number\tempca}\kern-1.5pt\Upsilon\rightarrow[{}${\tt\the\toksa}$]\;$% \fi}% \else \def\setpgroup{% $\Upsilon\leftarrow\langle{}${\tt\the\toksa}%${}% \if\next]% \else $\rangle\;$% \fi}% \fi \tempca#1\relax\printtermt }{texline} \defy\bb{% ${}_{\rm?}\kern-2pt\Upsilon$% }{index:tex} \defx\bb{Y_??}{index:visual} \defx\switchon{% \hbox{\bf switch$\;$}% \def\setpgroup{{$($}\the\toksa{$)$}$\,$}% \def\setegroup{}% \grabbalanced }{texline} \defy\switchon{% \hbox{\bf switch$\;$}% }{index:tex} \defx\in{% $\,\varepsilon\,$% }{texline} \defy\in{% $\,\varepsilon\,$% }{index:tex} \defx\concat#1#2{% \hbox{#1${}\leftarrow{}$#1${}+_{\rm s}{}$#2$\;$}% }{texline} \defy\concat{% \hbox{$A\leftarrow A+_{\rm s}B$}% }{index:tex} \defx\appendr#1{% \hbox{#1${}\leftarrow{}$#1${}+_{\rm sx}{}$}% \def\setpgroup{{$[\,$}\the\toksa{$\,]$}$\,$}% \def\setegroup{}% \grabbalanced }{texline} \defy\appendr{% \hbox{$A\leftarrow A+_{\rm sx}B$}% }{index:tex} \defx\default{% {\tt default}$\;$% }{texline} \defx\getfirst{% {}$\pi_1${}% \def\setegroup{\relax}% \def\setpgroup{% ${}(\hbox{\the\toksa}% \if\next]% \else )% \fi $}\grabbalanced }{texline} \defy\getfirst{% $\pi_1$% }{index:tex} \defx\getfirst{pi_1}{index:visual} \defx\getsecond{% {}$\pi_2${}% \def\setegroup{\relax}% \def\setpgroup{% $(\hbox{\the\toksa}% \if\next]% \else )% \fi $}\grabbalanced }{texline} \defy\getsecond{% $\pi_2$% }{index:tex} \defx\getsecond{pi_2}{index:visual} \defx\getthird{% {}$\pi_3${}% \def\setegroup{\relax}% \def\setpgroup{% ${}(\hbox{\the\toksa}% \if\next]% \else )% \fi $}\grabbalanced }{texline} \defy\getthird{% $\pi_3$% }{index:tex} \defx\getthird{pi_3}{index:visual} \defx\getfourth{% {}$\pi_4${}% \def\setegroup{\relax}% \def\setpgroup{% $(\hbox{\the\toksa}% \if\next]% \else )% \fi $}\grabbalanced }{texline} \defy\getfourth{% $\pi_4$% }{index:tex} \defx\getfourth{pi_4}{index:visual} \defx\getfifth{% {}$\pi_5${}% \def\setegroup{\relax}% \def\setpgroup{% $(\hbox{\the\toksa}% \if\next]% \else )% \fi $}\grabbalanced }{texline} \defy\getfifth{% $\pi_5$% }{index:tex} \defx\getfifth{pi_5}{index:visual} \defx\rhscont{% {}$\pi_{\{\}}${}% \def\setegroup{\relax}% \def\setpgroup{% ${}(\hbox{\the\toksa}% \if\next]% \else )% \fi $}\grabbalanced }{texline} \defy\rhscont{% $\pi_{\{\}}$% }{index:tex} \defx\rhscont{pi_brace}{index:visual} \defx\rhscnct{% {}$\pi_{\leftrightarrow}${}% \def\setegroup{\relax}% \def\setpgroup{% ${}(\hbox{\the\toksa}% \if\next]% \else )% \fi $}\grabbalanced }{texline} \defy\rhscnct{% $\pi_{\leftrightarrow}$% }{index:tex} \defx\rhscnct{pi_arrow}{index:visual} \defx\rhsbool{% {}$\pi_{\vdash}${}% \def\setegroup{\relax}% \def\setpgroup{% ${}(\hbox{\the\toksa}% \if\next]% \else )% \fi $}\grabbalanced }{texline} \defy\rhsbool{% $\pi_{\vdash}$% }{index:tex} \defx\rhsbool{pi_implies}{index:visual} \defx\%{% {\.{\harmlesscomment}}% }{texline} \defy\%{% {\.{\harmlesscomment}}\let\defypostamble\relax% }{index:tex} \defx\%{\%}{index:visual} \defx\harmlesscomment{% {\.{\harmlesscomment}}% }{texline} \defy\harmlesscomment{% {\.{\harmlesscomment}}\let\defypostamble\relax% }{index:tex} \defx\harmlesscomment{\%}{index:visual} \defx\\{% {\.{\\}}% }{texline} \defy\\{% {\.{\\}}\let\defypostamble\relax% }{index:tex} \defx\\{\\}{index:visual} \defx\lbchar{% \.{\{}% }{texline} \defy\lbchar{% \.{\{}% }{index:tex} \expandafter\defx\expandafter\lbchar\expandafter{\lbchar lbchar}{index:visual} \extendcs\alltexsymbols\with\lbchar \def\bbalempty[#1]#2{% \ifx#2]\relax \else \ifx#2[\relax \else \ifnum`#2=`\{% #2\hbox{$\,$}% \else \unskip\hbox{$\,$}#2% \fi \fi \fi }% \def\bbbalance#1{% \ifnum\bbalance>0 \loop \advance\bbalance-1\relax \appendr\texlinetoks{\noexpand\bbal[\the\bbalance]]}% \ifnum\bbalance>0 \repeat \else \tempca-\bbalance \toksd{}% \loop \advance\tempca-1\relax \appendl\toksd{\noexpand\bbal[\the\tempca][}% \ifnum\tempca>0 \repeat \tempca-\bbalance \bbalance\tempca \texlinetoks{}\texidxtoks{}% \yygetchar#1\end % \errmessage{\the\texlinetoks...\the\toksd...\the\bbalance}% \concatl\toksd\texlinetoks \fi } \def\grabbalanced{% \futurelet\next\gr@bbalanced } \def\gr@bbalanced{% \ifx\next\bbal \let\next\gr@bb@lanced \else \let\next\settgroup \fi \next } \def\gr@bb@lanced\bbal[#1]#2{% \ifnum`#2=`\}% this is a closing parenthesis we are inside a group \def\next{\setegroup\bbal[#1]#2}% \toksa{#2}% \else \ifnum`#2=`]% \def\next{\setegroup\bbal[#1]#2}% \toksa{#2}% \else \def\next##1\bbal[#1]##2{% \toksa{##1}\let\next##2% \setpgroup }% \fi \fi \next } \defx\yyBEGIN{% \def\setegroup{{\bf enter}}% \def\settgroup{{\bf enter}}% for text examples \def\setpgroup{% {% \let\parsernamespace\flexpseudonamespace \expandafter\nameproc\expandafter{\the\toksa}\with\parsebin \edef\next{% \toksd{\toksd{\the\toksa}\tokse{\the\toksb}}% }\next % a trick to `reshuffle' the output of \nameproc: % the parsed name goes to \toksd and the visual key is put in \tokse \expandafter }\the\toksd \let\termindex\writeidxfsentry \edef\next{{}$\nx\mathop{\hbox{\nx\bf enter}}(\hbox{\nx\flexsndisplay{\the\toksd}})\,${}% \gidxentryxb{\termvstring}{\the\toksa}{\the\tokse}}\next \let\termindex\eatone }\grabbalanced }{texline} \defy\yyBEGIN{% {\bf enter}% }{index:tex} \defx\yyBEGIN{enter}{index:visual} \defx\yyBEGINr{% {\bf enter$_x\,$}% }{texline} \defy\yyBEGINr{% {\bf enter$_x$}% }{index:tex} \defx\yyBEGINr{enter_x}{index:visual} \defx\yypushstate{% \def\setegroup{{\bf push state}}% \def\setpgroup{% {% \let\parsernamespace\flexpseudonamespace \expandafter\nameproc\expandafter{\the\toksa}\with\parsebin \edef\next{% \toksd{\toksd{\the\toksa}\tokse{\the\toksb}}% }\next % a trick to `reshuffle' the output of \nameproc: % the parsed name goes to \toksd and the visual key is put in \tokse \expandafter }\the\toksd \let\termindex\writeidxfsentry \edef\next{{}$\nx\mathop{\hbox{\nx\bf push state}}(\hbox{\nx\flexsndisplay{\the\toksd}})\,${} \gidxentryxb{\termvstring}{\the\toksa}{\the\tokse}}\next \let\termindex\eatone }\grabbalanced }{texline} \defy\yypushstate{% {\bf push state}% }{index:tex} \defx\yypushstate{push\_state}{index:visual} \defx\yypopstate{% \def\setegroup{{\bf pop state}}% \def\setpgroup{% {% \let\parsernamespace\flexpseudonamespace \expandafter\nameproc\expandafter{\the\toksa}\with\parsebin \edef\next{% \toksd{\toksd{\the\toksa}\tokse{\the\toksb}}% }\next % a trick to `reshuffle' the output of \nameproc: % the parsed name goes to \toksd and the visual key is put in \tokse \expandafter }\the\toksd \let\termindex\writeidxfsentry \edef\next{{}$\nx\mathop{\hbox{\nx\bf pop state}}(\hbox{\the\toksd})\,${} \gidxentryxb{\termvstring}{\the\toksa}{\the\tokse}}\next \let\termindex\eatone }\grabbalanced }{texline} \defy\yypopstate{% {\bf pop state}% }{index:tex} \defx\yypopstate{pop state}{index:visual} \defx\yylexstate{% \def\setegroup{{\bf state}}% \def\setpgroup{% {% \let\parsernamespace\flexpseudonamespace \expandafter\nameproc\expandafter{\the\toksa}\with\parsebin \edef\next{% \toksd{\toksd{\the\toksa}\tokse{\the\toksb}}% }\next % a trick to `reshuffle' the output of \nameproc: % the parsed name goes to \toksd and the visual key is put in \tokse \expandafter }\the\toksd \let\termindex\writeidxfsentry \edef\next{{}$\nx\mathop{\hbox{\nx\bf state}}(\hbox{\nx\flexsndisplay{\the\toksd}})\,${}% \gidxentryxb{\termvstring}{\the\toksa}{\the\tokse}}\next \let\termindex\eatone }\grabbalanced }{texline} \defy\yylexstate{% {\bf state}% }{index:tex} \defx\yylexstate{state}{index:visual}