diff --git a/src/latex.c b/src/latex.c index 2651025..2e4904a 100644 --- a/src/latex.c +++ b/src/latex.c @@ -91,7 +91,7 @@ latexDone (const System sys) //! Print a term using LaTeX and highlighting. /** * Basically a recode of termPrint, now specific using latex codes and with a - * highlighting feature. + * highlighting feature. There is still some obsolete code to show variable mappings in a term. *@param term a term to be printed. *@param highlight a list of terms to be highlighted. */ @@ -134,15 +134,7 @@ latexTermPrint (Term term, Termlist highlight) if (realTermTuple (term)) { printf ("("); - while (realTermTuple (term)) - { - latexTermPrint (term->op1, highlight); - printf (","); - term = term->op2; - if (!realTermTuple (term)) - latexTermPrint (term, highlight); - - } + latexTermTuplePrint (term); printf (")"); return; } @@ -154,14 +146,14 @@ latexTermPrint (Term term, Termlist highlight) /* function application */ latexTermPrint (term->key, highlight); printf ("("); - latexTermPrint (term->op, highlight); + latexTermTuplePrint (term->op, highlight); printf (")"); } else { /* normal encryption */ printf ("\\{"); - latexTermPrint (term->op, highlight); + latexTermTuplePrint (term->op, highlight); printf ("\\}_{"); latexTermPrint (term->key, highlight); printf ("}"); @@ -169,6 +161,32 @@ latexTermPrint (Term term, Termlist highlight) } } +//! Print an inner (tuple) term using LaTeX, without brackets. +/** + * The tuple printing only works correctly for normalized terms. + * If not, they might are displayed as "((x,y),z)". Maybe that is even + * desirable to distinguish them. + */ +void +latexTermTuplePrint (Term term, Termlist hl) +{ + if (term == NULL) + { + printf ("Empty term"); + return; + } + term = deVar(term); + while (realTermTuple (term)) + { + // To remove any brackets, change this into latexTermTuplePrint. + latexTermPrint (term->op1, hl); + printf (","); + term = deVar(term->op2); + } + latexTermPrint(term, hl); + return; +} + //! Print a termlist in LaTeX using highlighting. /** * Extending LaTeX term printing to term list printing, again with highlight diff --git a/src/latex.h b/src/latex.h index ef9efac..7b1d074 100644 --- a/src/latex.h +++ b/src/latex.h @@ -17,5 +17,7 @@ void latexMessagePrint(const System sys, int from, int to); void latexLearnComment(const System sys, Termlist tl); void latexTracePrint(System sys); void attackDisplayLatex(System sys); +void latexTermPrint (Term term, Termlist hl); +void latexTermTuplePrint (Term term, Termlist hl); #endif diff --git a/src/terms.c b/src/terms.c index 2d47bdb..e602086 100644 --- a/src/terms.c +++ b/src/terms.c @@ -231,6 +231,12 @@ termOccurs (Term t, Term tsub) } //! Print a term to stdout. +/** + * The tuple printing only works correctly for normalized terms. + * If not, they might are displayed as "((x,y),z)". Maybe that is even + * desirable to distinguish them. + *\sa termTuplePrint() + */ void termPrint (Term term) { @@ -271,15 +277,7 @@ termPrint (Term term) if (realTermTuple (term)) { printf ("("); - while (realTermTuple (term)) - { - termPrint (term->op1); - printf (","); - term = term->op2; - if (!realTermTuple (term)) - termPrint (term); - - } + termTuplePrint(term); printf (")"); return; } @@ -291,7 +289,7 @@ termPrint (Term term) /* function application */ termPrint (term->key); printf ("("); - termPrint (term->op); + termTuplePrint (term->op); printf (")"); } else @@ -300,7 +298,7 @@ termPrint (Term term) if (globalLatex) { printf ("\\{"); - termPrint (term->op); + termTuplePrint (term->op); printf ("\\}_{"); termPrint (term->key); printf ("}"); @@ -308,7 +306,7 @@ termPrint (Term term) else { printf ("{"); - termPrint (term->op); + termTuplePrint (term->op); printf ("}"); termPrint (term->key); } @@ -316,6 +314,31 @@ termPrint (Term term) } } +//! Print an inner (tuple) term to stdout, without brackets. +/** + * The tuple printing only works correctly for normalized terms. + * If not, they might are displayed as "((x,y),z)". Maybe that is even + * desirable to distinguish them. + */ +void +termTuplePrint (Term term) +{ + if (term == NULL) + { + printf ("Empty term"); + return; + } + term = deVar(term); + while (realTermTuple (term)) + { + // To remove any brackets, change this into termTuplePrint. + termPrint (term->op1); + printf (","); + term = deVar(term->op2); + } + termPrint(term); + return; +} //! Make a deep copy of a term. /** diff --git a/src/terms.h b/src/terms.h index fc2a9ce..bb761a4 100644 --- a/src/terms.h +++ b/src/terms.h @@ -101,6 +101,7 @@ int hasTermVariable (Term term); int isTermEqualFn (Term term1, Term term2); int termOccurs (Term t, Term tsub); void termPrint (Term term); +void termTuplePrint (Term term); Term termDuplicate (const Term term); Term termDuplicateDeep (const Term term); Term termDuplicateUV (Term term);