% Copyright 2012-2015, 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}
=
{%
    \appendr\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
    \action\next\in\texdefaultstate
}
^^A % \yycp@==1
{%
    \edef\next{\noexpand\noexpand\the\yybyte}%
    \action\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}%
    \action\next\in\currentstate}
}

\def\texescdefault{%
    \let\currentstate\esccurrentstate
    \yycp@=`\ %
    \yybyte{\ }%
    \action\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
  \action\next\in\currentstate
}

\def\outputtexcs{%
  \expandafter\ifx\csname\the\yytext\defTpostfix\endcsname\relax
      \putother{`\\}\in\toksa
      \concat\texlinetoks\toksa
      \concat\texlinetoks\yytext
      \appendr\texlinetoks{\noexpand\hbox{$\noexpand\,$}}%
  \else
      \appendr\texlinetoks{\expandafter\expandafter\expandafter\noexpand\expandafter\csname\the\yytext xTeXmode\endcsname}%
  \fi
  \appendr\texidxtoks{%
      \termindex{{\nx\nx\nx\texcsstring{\expandafter\charstonumberse\the\yytext\end}}{\texnspace}{\nx\the\pageno}{\secno}}%
  }%
}

% the `calling conventions' for indexing \TeX\ control sequences are too different to use canned indexing macros
% (the second parameter is a register so it has to be expanded before the \charstonumberse processes it)
% we therefore invoke the macros by hand

\def\texidxdomain{T}

\def\texcsidxrank{2}

\def\writetexidxentry#1{\iftermindex\write\gindex{\nx\nx\expandafter\nx\csname\texidxdomain TI\endcsname\texcsidxrank#1}\fi}

\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

\def\TeXx(#1)#2;{% TODO
    \let\oldttdot\.\relaxcweb
    \textoks{}\let\.\dotcollect 
    #1%
    \restorecweb\let\.\oldttdot
    \expandafter\T@Xx\the\textoks}

\def\mypar{\par}

\def\TeXb(#1)#2;{% TeX material begin
    {}$%
    \let\oldsix\6%
    \let\6\ignorespaces
    \let\oldC\C
    \let\C\saveCcomments
    \let\oldttdot\.\relaxcweb
    \textoks{}\toksa{}\let\.\dotcollectb
    #1%
    \restorecweb\let\.\oldttdot
    \dotcollectstripquotes
    ${}}

\def\TeXa(#1)#2;{% TeX material add
    {}$%
    \let\oldttdot\.\relaxcweb
    \toksa{}\let\.\dotcollectb
    #1%
    \restorecweb\let\.\oldttdot
    \dotcollectstripquotes
    ${}}

\def\TeXf(#1)#2;{% TeX material add
    {}$%
    \let\oldttdot\.\relaxcweb
    \toksa{}\let\.\dotcollectb
    \textoks\expandafter{\the\textoks\hbox{\6}}%
    #1%
    \restorecweb\let\.\oldttdot
    \dotcollectstripquotes
    ${}}

\def\TeXo(#1)#2;{% TeX material output
    \let\oldttdot\.\relaxcweb
    \let\.\dotcollect
    \let\6\oldsix
    \let\C\oldC 
    #1%
    \restorecweb\let\.\oldttdot
    $\expandafter\T@Xx\expandafter"\the\textoks"$}

\def\TeXao(#1)#2;{% TeX material output
    {}$\let\oldttdot\.\relaxcweb
    \toksa{}\let\.\dotcollectb
    \let\6\oldsix
    \let\C\oldC
    #1%
    \restorecweb\let\.\oldttdot
    \dotcollectstripquotes
    $\expandafter\T@Xx\expandafter"\the\textoks"${}${}}

\def\TeXfo(#1)#2;{% TeX material output
    {}$\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"${}${}}

\let\TeXxi\TeXx
\def\inlineTeXx#1{$\TeXxi(\.{"#1"});$} % for indexing macros

\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
      \restorecsxlist\texnspace\alltexsymbols
      \let\termindex\writetexidxentry
      \yygetchar#1\end
      \toksc{#1}%
      \iftracetexpp{\newlinechar=`^^J%
          \errmessage{TeX_ input: \the\toksc^^JTeX_ first pass: \the\texlinetoks}}\fi
      \ifnum\bbalance=\z@
      \else
          \bbbalance
      \fi
      \iftracetexpp\errmessage{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\texlinetoks\expandafter{\the\texlinetoks}%
      \let\bbal\bbalempty\bbalance\z@
      \restorecsxlist\texnspace\alltexsymbols
      \let\termindex\writetexidxentry\tt\chardef\_=`\_\the\texlinetoks
  \endgroup
  \iffalse}\fi
  {}${}%$
}

\def\alltexsymbols{%
     \space\toksa\toksb\toksc\tokse\toksf\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\toksd\rhscont
     \rhscnct\rhsbool\table\ifrhsfull\rhsfulltrue\rhsfullfalse
     \yyval\tempca\tempcb\z@\@ne\tw@\m@ne\advance\ifcat\iftracebadchars
     \bb\yylexreturnptr\yylexreturn\yylexreturnval\yylexreturnchar
     \yylexreturntext\yylexnext
}

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

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

\let\defypreamble\empty % for indexing macros
\def\defypostamble{ {\rm(\.{\\\thisnamex})}}

\let\settgroup\relax

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

\defx\hspace{\hbox{$\,$\char`\ $\,$}}{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\@ne{% 
  $\,1_{\rm R}\,$%
}{texline}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\defy\toksf{$v_f$}{index}

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

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

\def\setflexreturn#1{%
  \def\setegroup{{\bf return}#1}%
  \def\setpgroup{%
      {%
      \let\texidxdomain\bisonidxdomain
      \tokse\toksa
      \expandafter\nameproc\expandafter{\the\toksa}%
      \ifyyparsefail
          \edef\next{\toksa{\termmetastyle{%
              \expandafter\gidxentry\expandafter{\expandafter\termvstring\expandafter}\expandafter{\the\toksa}%
              \let\nx\idxfont\nx\empty\nx\tt\the\toksa\nx\/%
          }}}\next
      \else
          \expandafter\settermstyle\expandafter{\the\tokse}%
      \fi
      {}$\mathop{\hbox{{\bf return}#1}}\hbox{\the\toksa}${}}%
  }\grabbalanced
}

\defx\yylexreturnptr{% 
    \setflexreturn{$_p${}}%
}{texline}

\defy\yylexreturnptr{% 
  {\bf return$_p$}%
}{index}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\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\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\getsecond{%
  {}${}\pi_2${}%
  \def\setegroup{\relax}%
  \def\setpgroup{%
    ${}(\hbox{\the\toksa}%
    \if\next]%
    \else
        )%
    \fi
    $}\grabbalanced
}{texline}

\defy\getsecond{%
  ${}\pi_2$%
}{index}

\defx\getthird{%
  {}${}\pi_3${}%
  \def\setegroup{\relax}%
  \def\setpgroup{%
    ${}(\hbox{\the\toksa}%
    \if\next]%
    \else
        )%
    \fi
    $}\grabbalanced
}{texline}

\defy\getthird{%
  ${}\pi_3$%
}{index}

\defx\getfourth{%
  {}${}\pi_4${}%
  \def\setegroup{\relax}%
  \def\setpgroup{%
    ${}(\hbox{\the\toksa}%
    \if\next]%
    \else
        )%
    \fi
    $}\grabbalanced
}{texline}

\defy\getfourth{%
  ${}\pi_4$%
}{index}

\defx\getfifth{%
  {}${}\pi_5${}%
  \def\setegroup{\relax}%
  \def\setpgroup{%
    ${}(\hbox{\the\toksa}%
    \if\next]%
    \else
        )%
    \fi
    $}\grabbalanced
}{texline}

\defy\getfifth{%
  ${}\pi_5$%
}{index}

\defx\rhscont{%
  {}${}\pi_{\{\}}${}%
  \def\setegroup{\relax}%
  \def\setpgroup{%
    ${}(\hbox{\the\toksa}%
    \if\next]%
    \else
        )%
    \fi
    $}\grabbalanced
}{texline}

\defy\rhscont{%
  ${}\pi_{\{\}}$%
}{index}

\defx\rhscnct{%
  {}${}\pi_{\leftrightarrow}${}%
  \def\setegroup{\relax}%
  \def\setpgroup{%
    ${}(\hbox{\the\toksa}%
    \if\next]%
    \else
        )%
    \fi
    $}\grabbalanced
}{texline}

\defy\rhscnct{%
  ${}\pi_{\leftrightarrow}$%
}{index}

\defx\rhsbool{%
  {}${}\pi_{\vdash}${}%
  \def\setegroup{\relax}%
  \def\setpgroup{%
    ${}(\hbox{\the\toksa}%
    \if\next]%
    \else
        )%
    \fi
    $}\grabbalanced
}{texline}

\defy\rhsbool{%
  ${}\pi_{\vdash}$%
}{index}

\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{%
  \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{}%
      \expandafter\yygetchar\the\toksc\end
%      \errmessage{\the\texlinetoks...\the\toksd...\the\bbalance}%
      \appendl\texlinetoks{\the\toksd}%
  \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
}
