\documentclass{article}
\input camila.mac
\begin{document}

\INCLUDE{txt.cam}
\INCLUDE{seq.cam}
\SORTS

$\begin{array}{lcll}
TeX & \cong & {TeXObj^{\star}}  \\
TeXObj & \cong & {{TeXCmd + TeXTabRow} + str}  \\
TeXCmd & \cong & 
\PROD O \TYPE str \NEXT A \TYPE {TeXArg^{\star}} \DORP
  \\
TeXTabRow & \cong & 
\PROD R \TYPE {TeXArg^{\star}} \DORP
  \\
TeXArg & \cong & {{{{str + int} + TeXCmd} + Opt} + TeX}  \\
Opt & \cong & 
\PROD A \TYPE TeXArg \DORP
  \\
\end{array}$

\OPERS

$\begin{array}{l}
texDef:str \times TeX \tfunc{TeXCmd} \\ texDef(m,l) \deff \\ \rule{3ex}{0pt}  
TeXCmd(\!\!\mattt{
"def\\"} \conc m,l)
\end{array}$

\traco

$\begin{array}{l}
texNDef:int \times str \times TeX \tfunc{TeXCmd} \\ texNDef(n,m,l) \deff \\ \rule{3ex}{0pt}  
\LET 
s = 
strCAT( 

\LAMBDA{n}\!\!\mattt{
\mbox{\texttt{"#"}}} \conc 
itoa(n)^* (
seqInseg(n))) 
\IN 
TeXCmd(\!\!\mattt{
"def\\"} \conc m \conc s,l) 
\TEL
\end{array}$

\traco

$\begin{array}{l}
texGdef:str \times TeX \tfunc{TeXCmd} \\ texGdef(m,l) \deff \\ \rule{3ex}{0pt}  
TeXCmd(
strcat(\!\!\mattt{
"gdef\\"},m),l)
\end{array}$

\traco

$\begin{array}{l}
texLdef:str \times TeX \tfunc{TeXCmd} \\ texLdef(m,l) \deff \\ \rule{3ex}{0pt}  
TeXCmd(
strcat(\!\!\mattt{
"long\\def\\"},m),l)
\end{array}$

\traco

$\begin{array}{l}
texCons:str \tfunc{TeXCmd} \\ texCons(c) \deff \\ \rule{3ex}{0pt}  
TeXCmd(c,\emptylist)
\end{array}$

\traco

$\begin{array}{l}
texDefMap:str \pfunc{str} \tfunc{TeX} \\ texDefMap(ff) \deff \\ \rule{3ex}{0pt}  \enlist{
texDef(a,\enlist{ ff(a)}) \asor a \in 
dom(ff)}
\end{array}$

\traco

$\begin{array}{l}
texTeX2txt:TeX \tfunc{txt} \\ texTeX2txt(l) \deff \\ \rule{3ex}{0pt}  
\conc (\enlist{
\COND{\is{str}(c)}{\enlist{c}}{
\COND{\is{TeXCmd}(c)}{
texTeXCmd2txt(c)}{
texTeXTabRow2txt(c)}} \conc \enlist{\!\!\mattt{
\mbox{\texttt{"(cr)"}}}} \asor c \in l})
\end{array}$

\traco

$\begin{array}{l}
texTeXTabRow2txt:TeXTabRow \tfunc{txt} \\ texTeXTabRow2txt(x) \deff \\ \rule{3ex}{0pt}  
\conc (
seqAddSep(\enlist{
texTeXArg2txt(c) \asor c \in 
R(x)},\enlist{\!\!\mattt{\mbox{\texttt{"$\backslash$&"}}}}))
\end{array}$

\traco

$\begin{array}{l}
texTeXArg2txt:TeXArg \tfunc{txt} \\ texTeXArg2txt(x) \deff \\ \rule{3ex}{0pt}  
\COND{\is{str}(x)}{\enlist{x}}{
\COND{\is{int}(x)}{\enlist{
itoa(x)}}{
\COND{\is{TeXCmd}(x)}{
texTeXCmd2txt(x)}{
texTeX2txt(x)}}}
\end{array}$

\traco

$\begin{array}{l}
texTeXCmd2txt:TeXCmd \tfunc{txt} \\ texTeXCmd2txt(c) \deff \\ \rule{3ex}{0pt}  
\LET 
o = 
O(c)\\
l = 
A(c) 
\IN \enlist{
strcat(\!\!\mattt{\mbox{\texttt{"\$$\backslash$backslash$\backslash$backslash\$"}}},o)} \conc 
\conc (\enlist{
\COND{\is{Opt}(x)}{\enlist{\!\!\mattt{
\mbox{\texttt{"["}}}} \conc 
texTeXArg2txt(
A(x)) \conc \enlist{\!\!\mattt{
\mbox{\texttt{"]"}}}}}{\enlist{\!\!\mattt{
\mbox{\texttt{"\{"}}}} \conc 
texTeXArg2txt(x) \conc \enlist{\!\!\mattt{
\mbox{\texttt{"\}"}}}}} \asor x \in l}) 
\TEL
\end{array}$

\traco
\end{document}
