% Copyright 2012-2020, 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 <http://www.gnu.org/licenses/>.

% 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, resulting from 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)#2;{% TODO
    \TeXxwarn
    {}$\let\oldttdot\.\relaxcweb
    \let\.\dotcollect
    \textoks{}%
    #1%
    \restorecweb\let\.\oldttdot
    \expandafter\T@Xx\the\textoks
    {}${}\aftergroup\ignorespaces}

\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
    \TeXxwarn
    {}$\let\oldttdot\.\relaxcweb
    \toksa{}\let\.\dotcollectb
    #1%
    \restorecweb\let\.\oldttdot
    \dotcollectstripquotes
    ${}\aftergroup\ignorespaces}

\def\TeXf(#1)#2;{% TeX material add
    \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
    \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
    \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\TeXxi\TeXx
\def\inlineTeXx#1{$\let\writetexidxentry\writetextxtidxentry\TeXxi(\.{"#1"});$} % for indexing macros
\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}\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\texvspace{texvisline}
\def\texispace{index}

\let\defpostfix\defTpostfix
\let\defprefix\empty

\let\settgroup\relax

\defx\space{\hbox{$\,$\char`\ $\,$}}{texline}
\defy\space{\hbox{$\,$\char`\ $\,$}}{index}

\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}

\defx\advance{% 
  $\mathop{\hbox{\bf add}}$%
}{texline}

\defy\advance{% 
  {\bf add}%
}{index}

\defx\z@{% 
  $\,0_{\rm R}\,$%
}{texline}

\defy\z@{% 
  $0_{\rm R}$%
}{index}

\defx\z@{0_R}{index:visual}

\defx\@ne{% 
  $\,1_{\rm R}\,$%
}{texline}

\defy\@ne{% 
  $1_{\rm R}$%
}{index}

\defx\@ne{1_R}{index:visual}

\defx\tw@{% 
  $\,2_{\rm R}\,$%
}{texline}

\defy\tw@{% 
  $2_{\rm R}$%
}{index}

\defx\tw@{2_R}{index:visual}

\defx\m@ne{% 
  $\,-1_{\rm R}\,$%
}{texline}

\defy\m@ne{% 
  $-1_{\rm R}$%
}{index}

\defx\m@ne{-1_R}{index:visual}

\defx\tempca{% 
  $t_a$%
}{texline}

\defy\tempca{% 
  $t_a$%
}{index}

\defx\tempca{t_a}{index:visual}

\defx\tempcb{% 
  $t_b$%
}{texline}

\defy\tempcb{% 
  $t_b$%
}{index}

\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}

\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}

\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}

\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}

\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}

\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}

\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}

\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}

\defx\yyval{% 
  {}$\Upsilon${}%
  \def\setegroup{}%
  \def\setpgroup{%
    $\leftarrow\langle\,\the\toksa
    \if\next]%
    \else
        \,\rangle%
    \fi
    $}\grabbalanced
}{texline}

\defy\yyval{% 
  $\Upsilon$%
}{index}

\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}

\defx\yylexreturnptr{return_p}{index:visual}

\defx\yylexreturnxchar{% 
    \setflexreturn{$_x${}}%
}{texline}

\defy\yylexreturnxchar{% 
  \hbox{\bf return$_x$}%
}{index}

\defx\yylexreturnxchar{return_x}{index:visual}

\defx\yylexreturnchar{%
  \hbox{\bf return$_c$}% 
}{texline}

\defy\yylexreturnchar{% 
  \hbox{\bf return$_c$}%
}{index}

\defx\yylexreturnchar{return_c}{index:visual}

\defx\yylexnext{%
  {\bf continue}% 
}{texline}

\defy\yylexnext{% 
  {\bf continue}%
}{index}

\defx\yylexnext{continue}{index:visual}

\defx\yylexreturn{% 
    \setflexreturn{$_l${}}%
}{texline}

\defy\yylexreturn{% 
  {\bf return$_l$}%
}{index}

\defx\yylexreturn{return_l}{index:visual}

\defx\yylexreturnval{% 
    \setflexreturn{$_v${}}%
}{texline}

\defy\yylexreturnval{% 
  {\bf return$_v$}%
}{index}

\defx\yylexreturnval{return_v}{index:visual}

\defx\yylexreturnsym{% 
    \setflexreturn{$_{vp}${}}%
}{texline}

\defy\yylexreturnsym{% 
  {\bf return$_{vp}$}%
}{index}

\defx\yylexreturnsym{return_vp}{index:visual}

\defx\yylexreturntext{% 
    {\bf return$_t$}% 
}{texline}

\defy\yylexreturntext{% 
  {\bf return$_t$}%
}{index}

\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}

\defx\xcclreturn{set U return^ccl}{index:visual}

\defx\yyflexoptreturn{% 
    \setflexreturn{$^{\rm opt}$}%
}{texline}

\defy\yyflexoptreturn{% 
  {\bf return$^{\rm opt}$}%
}{index}

\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}

\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}

\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}

\defx\table{{}$\Omega${}}{texline}

\defy\table{$\Omega$}{index}

\defx\table{Omega}{index:visual}

\defx\relax{\hbox{$\circ$}}{texline}

\defy\relax{\hbox{$\circ$}}{index}

\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}

\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}

\defx\ifx{%
  {\bf if$_{\rm x}\;$}%
}{texline}

\defy\ifx{%
  {\bf if$_{\rm x}$}%
}{index}

\defx\ifnum{%
  {\bf if$_\omega\;$}%
}{texline}

\defy\ifnum{%
  {\bf if$_\omega$}%
}{index}

\defx\ifcat{%
  {\bf if$_{\rm cat}\;$}%
}{texline}

\defy\ifcat{%
  {\bf if$_{\rm cat}$}%
}{index}

\defx\iftracebadchars{%
  {\bf if$_t$ {\rm[{\tt bad char}]}$\;$}%
}{texline}

\defy\iftracebadchars{%
  {\bf if$_t$ {\rm[{\tt bad char}]}}%
}{index}

\defx\else{%
  {\bf else$\;$}%
}{texline}

\defy\else{%
  {\bf else}%
}{index}

\defx\fi{%
  {\bf fi$\;$}%
}{texline}

\defy\fi{%
  {\bf fi}%
}{index}

\defx\def{%
  {\bf def$\;$}%
}{texline}

\defy\def{%
  {\bf def}%
}{index}

\defx\edef{%
  {\bf def$_{\rm x}\;$}%
}{texline}

\defy\edef{%
  {\bf def$_{\rm x}$}%
}{index}

\defx\edef{def_x}{index:visual}

\defx\let{%
  {\bf let$\;$}%
}{texline}

\defx\next{%
  {\bf next$\;$}%
}{texline}

\defx\empty{%
  $\emptyset$%
}{texline}

\defy\empty{%
  $\emptyset$%
}{index}

\defx\ifrhsfull{%
  {\bf if {\rm ($\,$rhs${}={}$full$\,$)}$\;$}%
}{texline}

\defy\ifrhsfull{%
  {\bf if {\rm ($\,$rhs${}={}$full$\,$)}}%
}{index}

\defx\rhsfulltrue{%
  {\rm rhs${}={}$full$\,$}%
}{texline}

\defy\rhsfulltrue{%
  {\rm rhs${}={}$full}%
}{index}

\defx\rhsfullfalse{%
  {\rm rhs${}={}$not full$\,$}%
}{texline}

\defy\rhsfullfalse{%
  {\rm rhs${}={}$not full}%
}{index}

\defx\noexpand{%
  $^{\rm nox}$%
}{texline}

\defx\nx{%
  $^{\rm nx}$%
}{texline}

\defy\noexpand{%
  $^{\rm nox}$%
}{index}

\defy\nx{%
  $^{\rm nx}$%
}{index}

\defx\to{%
  ${}\mapsto{}$%
}{texline}

\defy\to{%
  $\mapsto$%
}{index}

\defx\emptyterm{%
  \hbox{$\ulcorner\ldots\urcorner$}%
}{texline}

\defy\emptyterm{%
  \hbox{$\ulcorner\ldots\urcorner$}%
}{index}

\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}

\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\seeksymtt#1[{{$\Upsilon\kern-1pt{}_{\rm#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}

\defx\bb{Y_??}{index:visual}

\defx\switchon{%
  \hbox{\bf switch$\;$}%
  \def\setpgroup{{$($}\the\toksa{$)$}$\,$}%
  \def\setegroup{}%
  \grabbalanced
}{texline}

\defy\switchon{%
  \hbox{\bf switch$\;$}%
}{index}

\defx\in{%
  $\,\varepsilon\,$%
}{texline}

\defy\in{%
  $\,\varepsilon\,$%
}{index}

\defx\concat#1#2{%
  \hbox{#1${}\leftarrow{}$#1${}+_{\rm s}{}$#2$\;$}%
}{texline}

\defy\concat{%
  \hbox{$A\leftarrow A+_{\rm s}B$}%
}{index}

\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}

\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}

\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}

\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}

\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}

\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}

\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}

\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}

\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}

\defx\rhsbool{pi_implies}{index:visual}

\defx\%{%
    {\.{\harmlesscomment}}%
}{texline}

\defy\%{%
    {\.{\harmlesscomment}}\let\defypostamble\relax%
}{index}

\defx\%{\%}{index:visual}

\defx\harmlesscomment{%
    {\.{\harmlesscomment}}%
}{texline}

\defy\harmlesscomment{%
    {\.{\harmlesscomment}}\let\defypostamble\relax%
}{index}

\defx\harmlesscomment{\%}{index:visual}

\defx\\{%
    {\.{\\}}%
}{texline}

\defy\\{%
    {\.{\\}}\let\defypostamble\relax%
}{index}

\defx\\{\\}{index:visual}

\defx\lbchar{% 
  \.{\{}%
}{texline}

\defy\lbchar{% 
  \.{\{}%
}{index}

\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\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{\the\toksd})${}%
            \gidxentryxb{\termvstring}{\the\toksa}{\the\tokse}}\next
        \let\termindex\eatone
    }\grabbalanced
}{texline}

\defy\yyBEGIN{% 
  {\bf enter}%
}{index}

\defx\yyBEGIN{enter}{index:visual}

\defx\yyBEGINr{% 
    {\bf enter$_x\,$}%
}{texline}

\defy\yyBEGINr{% 
  {\bf enter$_x$}%
}{index}

\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{\the\toksd})\,${}
            \gidxentryxb{\termvstring}{\the\toksa}{\the\tokse}}\next
        \let\termindex\eatone
    }\grabbalanced
}{texline}

\defy\yypushstate{% 
  {\bf push state}%
}{index}

\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}

\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{\the\toksd})\,${}%
            \gidxentryxb{\termvstring}{\the\toksa}{\the\tokse}}\next
        \let\termindex\eatone
    }\grabbalanced
}{texline}

\defy\yylexstate{% 
  {\bf state}%
}{index}

\defx\yylexstate{state}{index:visual}