/*****************************************************************************/ /* Copyright (C) 2020 NORMAN MEGILL nm at alum.mit.edu */ /* License terms: GNU General Public License */ /*****************************************************************************/ /*34567890123456 (79-character line to adjust editor window) 2345678901234567*/ /* mmcmds.c - assorted user commands */ #include #include #include #include #include #include #include /* 28-May-04 nm For clock() */ #include "mmvstr.h" #include "mmdata.h" #include "mmcmdl.h" /* For g_texFileName */ #include "mmcmds.h" #include "mminou.h" #include "mmpars.h" #include "mmveri.h" #include "mmwtex.h" /* For g_htmlVarColor,... */ #include "mmpfas.h" #include "mmunif.h" /* 26-Sep-2010 nm For g_bracketMatchInit, g_minSubstLen */ /* 1-Oct-2017 nm ...and g_firstConst */ /* 12-Nov-2018 nm */ /* Local prototypes */ vstring bigAdd(vstring bignum1, vstring bignum2); vstring bigSub(vstring bignum1, vstring bignum2); /* vstring mainFileName = ""; */ /* 28-Dec-05 nm Obsolete */ flag g_printHelp = 0; /* For HTML output */ vstring g_printStringForReferencedBy = ""; /* For MIDI */ flag g_midiFlag = 0; vstring g_midiParam = ""; /* Type (i.e. print) a statement */ void typeStatement(long showStmt, flag briefFlag, flag commentOnlyFlag, flag texFlag, flag htmlFlg) { /* From HELP SHOW STATEMENT: Optional qualifiers: / TEX - This qualifier will write the statement information to the LaTeX file previously opened with OPEN TEX. [Note: texFlag=1 and htmlFlg=0 with this qualifier.] / HTML - This qualifier will write the statement information to the HTML file previously opened with OPEN HTML. [Note: texFlag=1 and htmlFlg=1 with this qualifier.] / COMMENT_ONLY - This qualifier will show only the comment that immediatley precedes the statement. This is useful when you are using Metamath to preprocess LaTeX source you have created (see HELP TEX) / BRIEF - This qualifier shows the statement and its $e hypotheses only. */ long i, j, k, m, n; vstring str1 = "", str2 = "", str3 = ""; nmbrString *nmbrTmpPtr1; /* Pointer only; not allocated directly */ nmbrString *nmbrTmpPtr2; /* Pointer only; not allocated directly */ nmbrString *nmbrDDList = NULL_NMBRSTRING; flag q1, q2; flag type; flag subType; vstring htmlDistinctVars = ""; /* 12/23/01 */ char htmlDistinctVarsCommaFlag = 0; /* 12/23/01 */ vstring str4 = ""; /* 10/10/02 */ vstring str5 = ""; /* 19-Sep-2012 nm */ long distVarGrps = 0; /* 11-Aug-2006 nm */ /* For syntax breakdown of definitions in HTML page */ long zapStatement1stToken; static long wffToken = -1; /* array index of the hard-coded token "wff" - static so we only have to look it up once - set to -2 if not found */ subType = 0; /* Assign to prevent compiler warnings - not theor. necessary */ if (!showStmt) bug(225); /* Must be 1 or greater */ if (!commentOnlyFlag && !briefFlag) { assignStmtFileAndLineNum(showStmt); /* 9-Jan-2018 nm */ let(&str1, cat("Statement ", str((double)showStmt), " is located on line ", str((double)(g_Statement[showStmt].lineNum)), " of the file ", NULL)); if (!texFlag) { assignMathboxInfo(); /* In case it hasn't been assigned yet */ /* We need to call assignMathboxInfo() to do the initial assignment, in order to prevent "let(&" from executing during the getMathboxUser() call below, which would corrupt the "cat()" temporary stack (since "let(&" empties the stack). */ printLongLine(cat(str1, "\"", g_Statement[showStmt].fileName, "\".", /* 8-Feb-2007 nm Added HTML page info to SHOW STATEMENT ... /FULL */ (g_Statement[showStmt].pinkNumber == 0) ? /* !=0 means $a or $p */ "" : cat(" Its statement number for HTML pages is ", str((double)(g_Statement[showStmt].pinkNumber)), ".", NULL), /* 5-Aug-2020 nm Added mathbox user to SHOW STATEMENT ... /FULL */ ((getMathboxUser(showStmt))[0] == 0) ? "" : cat(" It is in the mathbox for ", getMathboxUser(showStmt), ".", NULL), NULL), "", " "); } else { if (!htmlFlg) let(&g_printString, ""); g_outputToString = 1; /* Flag for print2 to add to g_printString */ /* Note that printTexLongMathString resets it */ if (!(htmlFlg && texFlag)) { /* printLongLine(cat(str1, "{\\tt ", asciiToTt(g_Statement[showStmt].fileName), "}.", NULL), "", " "); */ } else { /* For categorizing html pages, we use the source file convention that syntax statements don't start with "|-" and that axioms have labels starting with "ax-". It is up to the database creator to follow this standard, which is not enforced. */ #define SYNTAX 1 #define DEFINITION 2 #define AXIOM 3 #define THEOREM 4 if (g_Statement[showStmt].type == (char)p_) { subType = THEOREM; } else { /* Must be a_ due to filter in main() */ if (g_Statement[showStmt].type != (char)a_) bug(228); if (strcmp("|-", g_MathToken[ (g_Statement[showStmt].mathString)[0]].tokenName)) { subType = SYNTAX; } else { if (!strcmp("ax-", left(g_Statement[showStmt].labelName, 3))) { subType = AXIOM; } else { subType = DEFINITION; } } } switch (subType) { case SYNTAX: let(&str1, "Syntax Definition"); break; case DEFINITION: let(&str1, "Definition"); break; case AXIOM: let(&str1, "Axiom"); break; case THEOREM: let(&str1, "Theorem"); break; default: bug(229); } /* Print a small pink statement number after the statement */ let(&str2, ""); str2 = pinkHTML(showStmt); printLongLine(cat("
", str1, " ", g_Statement[showStmt].labelName, "", str2, "
", NULL), "", "\""); } /* (htmlFlg && texFlag) */ g_outputToString = 0; } /* texFlag */ } if (!briefFlag || commentOnlyFlag) { let(&str1, ""); str1 = getDescription(showStmt); if (!str1[0] /* No comment */ #ifdef DATE_BELOW_PROOF /* 12-May-2017 nm */ || (str1[0] == '[' && str1[strlen(str1) - 1] == ']') /* 7-Sep-04 Allow both "$([])$" and "$( [] )$" */ || (strlen(str1) > 1 && str1[1] == '[' && str1[strlen(str1) - 2] == ']') /* Make sure getDescription() didn't pick up date stamp from previous proof */ #endif /* 12-May-2017 nm */ ) { print2("?Warning: Statement \"%s\" has no comment\n", g_Statement[showStmt].labelName); /* 14-Sep-2010 nm We must print a blank comment to have \begin{lemma} */ if (texFlag && !htmlFlg && !g_oldTexFlag) { let(&str1, "TO DO: PUT DESCRIPTION HERE"); } } if (str1[0]) { if (!texFlag) { printLongLine(cat("\"", str1, "\"", NULL), "", " "); } else { /* 10/10/02 This is now done in mmwtex.c printTexComment */ /* Although it will affect the 2nd (and only other) call to printTexComment below, that call is obsolete and there should be no side effect. */ /******* if (htmlFlg && texFlag) { let(&str1, cat("
Description: ", str1, "

", NULL)); } *******/ if (!htmlFlg) { /* LaTeX */ if (!g_oldTexFlag) { /* 14-Sep-2010 */ /* 1-May-2017 nm */ /* Distinguish axiom, definition, theorem */ /* Note: changes here must be mirrored in the \end{...} below */ if (g_Statement[showStmt].type == a_) { if (!strcmp(left(g_Statement[showStmt].labelName, 3), "ax-")) { let(&str3, "axiom"); } else { let(&str3, "definition"); } } else { let(&str3, "theorem"); } let(&str1, cat("\\begin{", str3, "}\\label{", left(str3, 3), ":", g_Statement[showStmt].labelName, "} ", str1, NULL)); /* old code before 1-May-2017: let(&str1, cat("\\begin{lemma}\\label{lem:", g_Statement[showStmt].labelName, "} ", str1, NULL)); */ } else { /* 6-Dec-03 Add separation space between theorems */ let(&str1, cat("\n\\vspace{1ex} %2\n\n", str1, NULL)); } } /* printTexComment(str1, 1); */ /* 17-Nov-2015 nm Add 3rd & 4th arguments */ printTexComment(str1, /* Sends result to g_texFilePtr */ 1, /* 1 = htmlCenterFlag */ PROCESS_EVERYTHING, /* actionBits */ /* 13-Dec-2018 nm */ 0 /* 1 = noFileCheck */); } } } if (commentOnlyFlag && !briefFlag) goto returnPoint; if ((briefFlag && !texFlag) || (htmlFlg && texFlag) /* HTML page 12/23/01 */) { /* In BRIEF mode screen output, show $d's */ /* This section was added 8/31/99 */ /* 12/23/01 - added algorithm to HTML pages also; the string to print out is stored in htmlDistinctVars for later printing */ /* 12/23/01 */ if (htmlFlg && texFlag) { let(&htmlDistinctVars, ""); htmlDistinctVarsCommaFlag = 0; } /* Note added 22-Aug-04: This algorithm is used to re-merge $d pairs into groups of 3 or more when possible, for a more compact display. The algorithm does not merge groups optimally, but it should be adequate. For example, in set.mm (e.g. old r19.23aivv): $d x ps $. $d y ps $. $d y A $. $d x y $. produces in SHOW STATEMENT (note redundant 3rd $d): $d ps x y $. $d y A $. $d x y $. However, in set.mm the equivalent (and better anyway): $d x y ps $. $d y A $. produces the same thing when remerged in SHOW STATEMENT. */ let(&str1, ""); nmbrTmpPtr1 = g_Statement[showStmt].reqDisjVarsA; nmbrTmpPtr2 = g_Statement[showStmt].reqDisjVarsB; i = nmbrLen(nmbrTmpPtr1); if (i /* Number of mandatory $d pairs */) { nmbrLet(&nmbrDDList, NULL_NMBRSTRING); for (k = 0; k < i; k++) { /* Is one of the variables in the current list? */ if (!nmbrElementIn(1, nmbrDDList, nmbrTmpPtr1[k]) && !nmbrElementIn(1, nmbrDDList, nmbrTmpPtr2[k])) { /* No, so close out the current list */ if (!(htmlFlg && texFlag)) { /* 12/23/01 */ if (k == 0) let(&str1, "$d"); else let(&str1, cat(str1, " $. $d", NULL)); } else { /* 12/23/01 */ let(&htmlDistinctVars, cat(htmlDistinctVars, "   ", NULL)); htmlDistinctVarsCommaFlag = 0; distVarGrps++; /* 11-Aug-2006 nm */ } nmbrLet(&nmbrDDList, NULL_NMBRSTRING); } /* Are both variables required to be distinct from all others in current list? */ for (n = 0; n < nmbrLen(nmbrDDList); n++) { if (nmbrDDList[n] != nmbrTmpPtr1[k] && nmbrDDList[n] != nmbrTmpPtr2[k]) { q1 = 0; q2 = 0; for (m = 0; m < i; m++) { if ((nmbrTmpPtr1[m] == nmbrDDList[n] && nmbrTmpPtr2[m] == nmbrTmpPtr1[k]) || (nmbrTmpPtr2[m] == nmbrDDList[n] && nmbrTmpPtr1[m] == nmbrTmpPtr1[k])) { q1 = 1; /* 1st var is required to be distinct */ } if ((nmbrTmpPtr1[m] == nmbrDDList[n] && nmbrTmpPtr2[m] == nmbrTmpPtr2[k]) || (nmbrTmpPtr2[m] == nmbrDDList[n] && nmbrTmpPtr1[m] == nmbrTmpPtr2[k])) { q2 = 1; /* 2nd var is required to be distinct */ } if (q1 && q2) break; /* Found both */ } /* Next m */ if (!q1 || !q2) { /* One of the variables is not required to be distinct from all others in the current list, so close out current list */ if (!(htmlFlg && texFlag)) { if (k == 0) let(&str1, "$d"); else let(&str1, cat(str1, " $. $d", NULL)); } else { /* 12/23/01 */ let(&htmlDistinctVars, cat(htmlDistinctVars, "   ", NULL)); htmlDistinctVarsCommaFlag = 0; distVarGrps++; /* 11-Aug-2006 nm */ } nmbrLet(&nmbrDDList, NULL_NMBRSTRING); break; /* Out of n loop */ } } /* If $d var in current list is not same as one we're adding */ } /* Next n */ /* If the variable is not already in current list, add it */ if (!nmbrElementIn(1, nmbrDDList, nmbrTmpPtr1[k])) { if (!(htmlFlg && texFlag)) { let(&str1, cat(str1, " ", g_MathToken[nmbrTmpPtr1[k]].tokenName, NULL)); } else { /* 12/23/01 */ if (htmlDistinctVarsCommaFlag) { let(&htmlDistinctVars, cat(htmlDistinctVars, ",", NULL)); } htmlDistinctVarsCommaFlag = 1; let(&str2, ""); str2 = tokenToTex(g_MathToken[nmbrTmpPtr1[k]].tokenName, showStmt); /* tokenToTex allocates str2; we must deallocate it */ let(&htmlDistinctVars, cat(htmlDistinctVars, str2, NULL)); } nmbrLet(&nmbrDDList, nmbrAddElement(nmbrDDList, nmbrTmpPtr1[k])); } if (!nmbrElementIn(1, nmbrDDList, nmbrTmpPtr2[k])) { if (!(htmlFlg && texFlag)) { let(&str1, cat(str1, " ", g_MathToken[nmbrTmpPtr2[k]].tokenName, NULL)); } else { /* 12/23/01 */ if (htmlDistinctVarsCommaFlag) { let(&htmlDistinctVars, cat(htmlDistinctVars, ",", NULL)); } htmlDistinctVarsCommaFlag = 1; let(&str2, ""); str2 = tokenToTex(g_MathToken[nmbrTmpPtr2[k]].tokenName, showStmt); /* tokenToTex allocates str2; we must deallocate it */ let(&htmlDistinctVars, cat(htmlDistinctVars, str2, NULL)); } nmbrLet(&nmbrDDList, nmbrAddElement(nmbrDDList, nmbrTmpPtr2[k])); } } /* Next k */ /* Close out entire list */ if (!(htmlFlg && texFlag)) { let(&str1, cat(str1, " $.", NULL)); printLongLine(str1, " ", " "); } else { /* 12/23/01 */ /* (do nothing) */ /*let(&htmlDistinctVars, cat(htmlDistinctVars, "
", NULL));*/ } } /* if i(#$d's) > 0 */ } if (briefFlag || texFlag /*(texFlag && htmlFlg)*/) { /* 6-Dec-03 */ /* For BRIEF mode, print $e hypotheses (only) before statement */ /* Also do it for HTML output */ /* 6-Dec-03 For the LaTeX output, now print hypotheses before statement */ j = nmbrLen(g_Statement[showStmt].reqHypList); k = 0; for (i = 0; i < j; i++) { /* Count the number of essential hypotheses */ if (g_Statement[g_Statement[showStmt].reqHypList[i]].type == (char)e_) k++; /* Added 5/26/03 */ /* For syntax definitions, also include $f hypotheses so user can more easily match them in syntax breakdowns of axioms and definitions */ if (subType == SYNTAX && (texFlag && htmlFlg)) { if (g_Statement[g_Statement[showStmt].reqHypList[i]].type == (char)f_) k++; } } if (k) { if (texFlag) { /* Note that printTexLongMath resets it to 0 */ g_outputToString = 1; } if (texFlag && htmlFlg) { print2("
\n", (k == 1) ? "Hypothesis" : "Hypotheses"); print2("\n", (k == 1) ? "Hypothesis" : "Hypotheses"); print2("\n"); } for (i = 0; i < j; i++) { k = g_Statement[showStmt].reqHypList[i]; if (g_Statement[k].type != (char)e_ /* Added 5/26/03 */ /* For syntax definitions, include $f hypotheses so user can more easily match them in syntax breakdowns of axioms & definitions */ && !(subType == SYNTAX && (texFlag && htmlFlg) && g_Statement[k].type == (char)f_) ) continue; if (!texFlag) { let(&str2, cat(str((double)k), " ", NULL)); } else { let(&str2, " "); } let(&str2, cat(str2, g_Statement[k].labelName, " $", chr(g_Statement[k].type), " ", NULL)); if (!texFlag) { printLongLine(cat(str2, nmbrCvtMToVString(g_Statement[k].mathString), " $.", NULL), " "," "); } else { /* if texFlag */ /* texFlag was (misleadingly) included below to facilitate search for "htmlFlg && texFlag". */ if (!(htmlFlg && texFlag)) { if (!g_oldTexFlag) { /* 14-Sep-2010 nm */ /* Do nothing */ } else { let(&str3, space((long)strlen(str2))); printTexLongMath(g_Statement[k].mathString, str2, str3, 0, 0); } } else { g_outputToString = 1; print2("
%s
Ref\n"); print2("Expression
%s\n", g_Statement[k].labelName); /* Print hypothesis */ printTexLongMath(g_Statement[k].mathString, "", "", 0, 0); } } } /* next i */ if (texFlag && htmlFlg) { g_outputToString = 1; print2("
\n"); } } /* if k (#essential hyp) */ } let(&str1, ""); type = g_Statement[showStmt].type; if (type == p_) let(&str1, " $= ..."); if (!texFlag) let(&str2, cat(str((double)showStmt), " ", NULL)); else let(&str2, " "); let(&str2, cat(str2, g_Statement[showStmt].labelName, " $",chr(type), " ", NULL)); if (!texFlag) { printLongLine(cat(str2, nmbrCvtMToVString(g_Statement[showStmt].mathString), str1, " $.", NULL), " ", " "); } else { if (!(htmlFlg && texFlag)) { /* really !htmlFlg & texFlag */ if (!g_oldTexFlag) { /* 14-Sep-2010 nm new LaTeX code: */ g_outputToString = 1; print2("\\begin{align}\n"); let(&str3, ""); /* Get HTML hypotheses => assertion */ str3 = getTexOrHtmlHypAndAssertion(showStmt); /* In mmwtex.c */ printLongLine(cat(str3, /* No space before \label to make it easier to find last parenthesis in a post-processing script */ "\\label{eq:", g_Statement[showStmt].labelName, "}", /* 1-May-2017 nm */ /* Add "\tag{..}" to use .mm labels instead of equation numbers */ /* (Suggested by Ari Ferrera) */ "\\tag{", g_Statement[showStmt].labelName, "}", NULL), " ", " "); /* print2(" \\label{eq:%s}\n",g_Statement[showStmt].labelName); */ print2("\\end{align}\n"); /* 1-May-2017 nm */ /* Distinguish axiom, definition, theorem for LaTeX */ /* Note: changes here must be mirrored in the \begin{...} above */ if (g_Statement[showStmt].type == a_) { if (!strcmp(left(g_Statement[showStmt].labelName, 3), "ax-")) { let(&str3, "axiom"); } else { let(&str3, "definition"); } } else { let(&str3, "theorem"); } print2("%s\n", cat("\\end{", str3, "}", NULL)); /* old code before 1-May-2017: print2("\\end{lemma}\n"); */ fprintf(g_texFilePtr, "%s", g_printString); let(&g_printString, ""); g_outputToString = 0; } else { /* old TeX code */ let(&str3, space((long)strlen(str2))); /* 3rd argument of printTexLongMath cannot be temp allocated */ printTexLongMath(g_Statement[showStmt].mathString, str2, str3, 0, 0); } } else { /* (htmlFlg && texFlag) */ g_outputToString = 1; print2("
\n"); print2("\n"); print2("\n"); printLongLine(cat( "
Assertion
Ref\n"); print2("Expression
", g_Statement[showStmt].labelName, "", NULL), " ", " "); printTexLongMath(g_Statement[showStmt].mathString, "", "", 0, 0); g_outputToString = 1; print2("
\n"); } } if (briefFlag) goto returnPoint; /* 6-Dec-03 In the LaTeX output, the hypotheses used to be printed after the statement. Now they are printed before (see above 6-Dec-03 comments), so some code below is commented out. */ switch (type) { case a_: case p_: /* 6-Dec-03 This is not really needed but keeps output consistent with previous version. It puts a blank line before the HTML "distinct variable" list. */ if (texFlag && htmlFlg) { /* 6-Dec-03 */ g_outputToString = 1; print2("\n"); g_outputToString = 0; } /*if (!(htmlFlg && texFlag)) {*/ if (!texFlag) { /* 6-Dec-03 fix */ print2("Its mandatory hypotheses in RPN order are:\n"); } /*if (texFlag) g_outputToString = 0;*/ /* 6-Dec-03 */ j = nmbrLen(g_Statement[showStmt].reqHypList); for (i = 0; i < j; i++) { k = g_Statement[showStmt].reqHypList[i]; if (g_Statement[k].type != (char)e_ && (!htmlFlg && texFlag)) continue; /* 9/2/99 Don't put $f's in LaTeX output */ let(&str2, cat(" ",g_Statement[k].labelName, " $", chr(g_Statement[k].type), " ", NULL)); if (!texFlag) { printLongLine(cat(str2, nmbrCvtMToVString(g_Statement[k].mathString), " $.", NULL), " "," "); } else { if (!(htmlFlg && texFlag)) { /* LaTeX */ /*let(&str3, space((long)strlen(str2)));*/ /* 6-Dec-03 */ /* This clears out g_printString */ /*printTexLongMath(g_Statement[k].mathString, str2, str3, 0, 0);*/ /* 6-Dec-03 */ } } } /* 6-Dec-03 This is not really needed but keeps output consistent with previous version. It puts a blank line before the HTML "distinct variable" list. */ if (texFlag && htmlFlg) { /* 6-Dec-03 */ g_outputToString = 1; print2("\n"); g_outputToString = 0; } /*if (j == 0 && !(htmlFlg && texFlag)) print2(" (None)\n");*/ if (j == 0 && !texFlag) print2(" (None)\n"); /* 6-Dec-03 fix */ let(&str1, ""); nmbrTmpPtr1 = g_Statement[showStmt].reqDisjVarsA; nmbrTmpPtr2 = g_Statement[showStmt].reqDisjVarsB; i = nmbrLen(nmbrTmpPtr1); if (i) { for (k = 0; k < i; k++) { if (!texFlag) { let(&str1, cat(str1, ", <", g_MathToken[nmbrTmpPtr1[k]].tokenName, ",", g_MathToken[nmbrTmpPtr2[k]].tokenName, ">", NULL)); } else { if (htmlFlg && texFlag) { let(&str2, ""); str2 = tokenToTex(g_MathToken[nmbrTmpPtr1[k]].tokenName, showStmt); /* tokenToTex allocates str2; we must deallocate it */ let(&str1, cat(str1, "   ", str2, NULL)); let(&str2, ""); str2 = tokenToTex(g_MathToken[nmbrTmpPtr2[k]].tokenName, showStmt); let(&str1, cat(str1, ",", str2, NULL)); } } } if (!texFlag) printLongLine(cat( "Its mandatory disjoint variable pairs are: ", right(str1,3),NULL)," "," "); } if (type == p_ && nmbrLen(g_Statement[showStmt].optHypList) && !texFlag) { printLongLine(cat( "Its optional hypotheses are: ", nmbrCvtRToVString( g_Statement[showStmt].optHypList, /* 25-Jan-2016 nm */ 0, /*explicitTargets*/ 0 /*statemNum, used only if explicitTargets*/), NULL), " "," "); } nmbrTmpPtr1 = g_Statement[showStmt].optDisjVarsA; nmbrTmpPtr2 = g_Statement[showStmt].optDisjVarsB; i = nmbrLen(nmbrTmpPtr1); if (i && type == p_) { if (!texFlag) { let(&str1, ""); } else { if (htmlFlg && texFlag) { /* 12/1/01 don't output dummy variables let(&str1, cat(str1, "   (Dummy variables for use in proof:) ", NULL)); */ } } for (k = 0; k < i; k++) { if (!texFlag) { let(&str1, cat(str1, ", <", g_MathToken[nmbrTmpPtr1[k]].tokenName, ",", g_MathToken[nmbrTmpPtr2[k]].tokenName, ">", NULL)); } /* if !texFlag */ } /* next k */ if (!texFlag) { printLongLine(cat( "Its optional disjoint variable pairs are: ", right(str1,3),NULL)," "," "); } } /* if (i && type == p_) */ /* Before 12/23/01 ********** Future: once stable, take out redundant code producing str1 if (texFlag && htmlFlg && str1[0]) { g_outputToString = 1; printLongLine(cat("
Substitutions into these variable", " pairs may not have variables in common: ", str1, "
", NULL), "", " "); g_outputToString = 0; } ***********/ /* 12/23/01 */ if (texFlag && htmlFlg) { /* It's a web page */ if (htmlDistinctVars[0] != 0) { g_outputToString = 1; printLongLine(cat( "
", " 0) ? "mmset.html" : /* The following link will work in the NF and other "Proof Explorers" */ "../mpeuni/mmset.html", /* 19-Aug-2017, 26-Sep-2017 nm */ "#distinct\">Distinct variable group", /* 11-Aug-2006 nm Determine whether "group" or "groups". */ distVarGrps > 1 ? "s" : "", /* 11-Aug-2006 */ ": ", /* 14-Jan-2016 nm Put a span around the variable list to localize the use of the special math font for ALT_HTML */ (g_altHtmlFlag ? cat("", NULL) : ""), /* 14-Jan-2016 nm */ htmlDistinctVars, (g_altHtmlFlag ? "" : ""), "
", NULL), "", "\""); g_outputToString = 0; } /* 26-Aug-2017 nm Moved this down into proof section */ /* /@ 13-Aug-2017 nm @/ let(&str3, ""); if (type == p_) { str3 = htmlDummyVars(showStmt); if (str3[0] != 0) { g_outputToString = 1; /@ We don't need
if code is surrounded by
...
if (htmlDistinctVars[0] != 0) print2("
\n"); @/ /@ Print the list of dummy variables @/ printLongLine(str3, "", "\""); g_outputToString = 0; } } /@ (end of 13-Aug-2017) @/ */ /* 4-Jan-2014 nm */ let(&str2, ""); str2 = htmlAllowedSubst(showStmt); if (str2[0] != 0) { g_outputToString = 1; /* We don't need
if code is surrounded by
...
if (htmlDistinctVars[0] != 0 || str3[0] != 0) print2("
\n"); */ /* Print the list of allowed free variables */ printLongLine(str2, "", "\""); g_outputToString = 0; } } /* if (texFlag && htmlFlg) */ if (texFlag) { g_outputToString = 1; if (htmlFlg && texFlag) print2("
\n"); g_outputToString = 0; /* Restore normal output */ /* will be done automatically at closing fprintf(g_texFilePtr, "%s", g_printString); let(&g_printString, ""); */ break; /* case a_ or p_ */ } let(&str1, nmbrCvtMToVString( g_Statement[showStmt].reqVarList)); if (!strlen(str1)) let(&str1, "(None)"); printLongLine(cat( "The statement and its hypotheses require the variables: ", str1, NULL), " ", " "); if (type == p_ && nmbrLen(g_Statement[showStmt].optVarList)) { printLongLine(cat( "These additional variables are allowed in its proof: " ,nmbrCvtMToVString( g_Statement[showStmt].optVarList),NULL)," ", " "); /*??? Add variables required by proof */ } /* Note: g_Statement[].reqVarList is only stored for $a and $p statements, not for $e or $f. */ let(&str1, nmbrCvtMToVString( g_Statement[showStmt].reqVarList)); if (!strlen(str1)) let(&str1, "(None)"); printLongLine(cat("The variables it contains are: ", str1, NULL), " ", " "); break; /* case a_ or p_ */ default: break; } /* End switch(type) */ if (texFlag) { g_outputToString = 0; /* will be done automatically at closing fprintf(g_texFilePtr, "%s", g_printString); let(&g_printString, ""); */ } /* Start of finding definition for syntax statement */ if (htmlFlg && texFlag) { /* For syntax declarations, find the first definition that follows it. It is up to the user to arrange the database so that a meaningful definition is picked. */ if (subType == SYNTAX) { for (i = showStmt + 1; i <= g_statements; i++) { if (g_Statement[i].type == (char)a_) { if (!strcmp("|-", g_MathToken[ (g_Statement[i].mathString)[0]].tokenName)) { /* It's a definition or axiom */ /* See if each constant token in the syntax statement exists in the definition; if not don't use the definition */ j = 1; /* We start with k=1 for 2nd token (1st is wff, class, etc.) */ for (k = 1; k < g_Statement[showStmt].mathStringLen; k++) { if (g_MathToken[(g_Statement[showStmt].mathString)[k]]. tokenType == (char)con_) { if (!nmbrElementIn(1, g_Statement[i].mathString, (g_Statement[showStmt].mathString)[k])) { /* The definition being considered doesn't have one of the constant symbols in the syntax statement, so reject it */ j = 0; break; /* Out of k loop */ } } } /* Next k */ if (j) { /* Successful - use this definition or axiom as the reference */ g_outputToString = 1; let(&str1, left(g_Statement[i].labelName, 3)); let(&str2, ""); str2 = pinkHTML(i); if (!strcmp(str1, "ax-")) { printLongLine(cat( "
This syntax is primitive.", " The first axiom using it is ", g_Statement[i].labelName, "", str2, ".
", NULL), "", "\""); } else { printLongLine(cat( "
See definition ", g_Statement[i].labelName, "", str2, " for more information.
", NULL), "", "\""); } /* 10/10/02 Moved here from mmwtex.c */ /*print2("Colors of variables:\n");*/ printLongLine(cat( "
", NULL), "", "\""); g_outputToString = 0; break; /* Out of i loop */ } } } } /* Next i */ } /* if (subType == SYNTAX) */ /* For definitions, we pretend that the definition is a "wff" (hard-coded here; the .mm database provided by the user must use this convention). We use the proof assistant tools to prove that the statement is a wff, then we print the wff construction proof to the HTML file. */ if (subType == DEFINITION || subType == AXIOM) { /* Look up the token "wff" if we haven't found it before */ if (wffToken == -1) { /* First time */ wffToken = -2; /* In case it's not found because the user's source used a convention different for "wff" for wffs */ for (i = 0; i < g_mathTokens; i++) { if (!strcmp("wff", g_MathToken[i].tokenName)) { wffToken = i; break; } } } if (wffToken >= 0) { /* Temporarily zap statement type from $a to $p */ if (g_Statement[showStmt].type != (char)a_) bug(231); g_Statement[showStmt].type = (char)p_; /* Temporarily zap statement with "wff" token in 1st position so parseProof will not give errors (in typeProof() call) */ zapStatement1stToken = (g_Statement[showStmt].mathString)[0]; (g_Statement[showStmt].mathString)[0] = wffToken; if (strcmp("|-", g_MathToken[zapStatement1stToken].tokenName)) bug(230); nmbrTmpPtr1 = NULL_NMBRSTRING; nmbrLet(&nmbrTmpPtr1, g_Statement[showStmt].mathString); /* Find proof of formula or simple theorem (no new vars in $e's) */ /* maxEDepth is the maximum depth at which statements with $e hypotheses are considered. A value of 0 means none are considered. */ nmbrTmpPtr2 = proveFloating(nmbrTmpPtr1 /*mString*/, showStmt /*statemNum*/, 0 /*maxEDepth*/, 0, /*step: 0 = step 1 */ /*For messages*/ 0, /*not noDistinct*/ /* 3-May-2016 nm */ 2, /* override discouraged-usage statements silently */ 1 /* Always allow other mathboxes */ /* 5-Aug-2020 nm */ ); if (nmbrLen(nmbrTmpPtr2)) { /* A proof for the step was found. */ /* Get packed form of proof for shorter display */ nmbrLet(&nmbrTmpPtr2, nmbrSquishProof(nmbrTmpPtr2)); /* Temporarily zap proof into statement structure */ /* (The bug check makes sure there is no proof attached to the definition - this would be impossible) */ if (strcmp(g_Statement[showStmt].proofSectionPtr, "")) bug(231); if (g_Statement[showStmt].proofSectionLen != 0) bug(232); let(&str1, nmbrCvtRToVString(nmbrTmpPtr2, /* 25-Jan-2016 nm */ 0, /*explicitTargets*/ 0 /*statemNum, used only if explicitTargets*/)); /* Temporarily zap proof into the $a statement */ g_Statement[showStmt].proofSectionPtr = str1; g_Statement[showStmt].proofSectionLen = (long)strlen(str1) - 1; /* Display the HTML proof of syntax breakdown */ typeProof(showStmt, 0 /*pipFlag*/, 0 /*startStep*/, 0 /*endStep*/, 0 /*endIndent*/, 0 /*essentialFlag*/, /* <- also used as def flag in typeProof */ 1 /*renumberFlag*/, 0 /*unknownFlag*/, 0 /*notUnifiedFlag*/, 0 /*reverseFlag*/, 1 /*noIndentFlag*/, 0 /*splitColumn*/, 0 /*skipRepeatedSteps*/, /* 28-Jun-2013 nm */ 1 /*texFlag*/, /* Means either latex or html */ 1 /*htmlFlg*/); /* Restore the zapped statement structure */ g_Statement[showStmt].proofSectionPtr = ""; g_Statement[showStmt].proofSectionLen = 0; /* Deallocate storage */ let(&str1, ""); nmbrLet(&nmbrTmpPtr2, NULL_NMBRSTRING); } else { /* if (nmbrLen(nmbrTmpPtr2)) else */ /* 5-Aug-2011 nm */ /* Proof was not found - probable syntax error */ if (g_outputToString != 0) bug(246); printLongLine(cat( "?Warning: Unable to generate syntax breakdown for \"", g_Statement[showStmt].labelName, "\".", NULL), " ", " "); } /* Restore the zapped statement structure */ g_Statement[showStmt].type = (char)a_; (g_Statement[showStmt].mathString)[0] = zapStatement1stToken; /* Deallocate storage */ nmbrLet(&nmbrTmpPtr1, NULL_NMBRSTRING); } /* if (wffToken >= 0) */ } /* if (subType == DEFINITION) */ } /* if (htmlFlg && texFlag) */ /* End of finding definition for syntax statement */ /* 10/6/99 - Start of creating used-by list for html page */ if (htmlFlg && texFlag) { /* 10/25/02 Clear out any previous g_printString accumulation for g_printStringForReferencedBy case below */ fprintf(g_texFilePtr, "%s", g_printString); let(&g_printString, ""); /* Start outputting to g_printString */ if (g_outputToString != 0) bug(242); g_outputToString = 1; if (subType != SYNTAX) { /* Only do this for definitions, axioms, and theorems, not syntax statements */ let(&str1, ""); g_outputToString = 0; /* Switch output to console in case traceUsage reports an error */ /* 8-Dec-2018 nm */ str1 = traceUsage(showStmt, 0, /* recursiveFlag */ 0 /* cutoffStmt */); g_outputToString = 1; /* Restore output to string */ /* 8-Dec-2018 nm */ /* if (str1[0]) { */ /* Used by at least one */ /* 18-Jul-2015 nm */ /* 30-Oct-2018 nm Commented out, and block unindented: */ /*if (str1[0] == 'Y') {*/ /* Used by at least one */ /* 30-Oct-2018 nm */ /* We now output this all the time, using "(None)" if none, per request of Benoit Jubin */ /* str1[i] will be 'Y' if used by showStmt */ /* Convert usage list str1 to html links */ switch (subType) { case AXIOM: let(&str3, "axiom"); break; case DEFINITION: let(&str3, "definition"); break; case THEOREM: let(&str3, "theorem"); break; default: bug(233); } /******* pre 10/10/02 let(&str2, cat("This ", str3, " is referenced by: ", NULL)); *******/ /* 10/10/02 */ let(&str2, cat("", NULL)); @/ /@ old @/ /@ 19-Sep-2012 nm Include buffer in output string@/ let(&str2, cat(str5, str2, "", NULL)); printLongLine(str2, "", "\""); */ /**************** 18-Jul-2015 End of deleted code *********/ let(&str5, ""); /* Buffer for very long strings */ /* 19-Sep-2012 nm */ /* Scan all future statements in str1 Y/N list */ for (m = showStmt + 1; m <= g_statements; m++) { /* Scan the used-by map */ if (str1[m] != 'Y') continue; /* Get the label */ let(&str3, g_Statement[m].labelName); /* It should be a $p */ if (g_Statement[m].type != p_) bug(241); /* Get the pink number */ let(&str4, ""); str4 = pinkHTML(m); /* Assemble the href */ let(&str2, cat(str2, "  ", /*str3, "", str4, NULL));*/ str3, "\n", str4, NULL)); /* 18-Jul-2015 nm */ /* 8-Aug-2008 nm If line is very long, print it out and reset it to speed up program (SHOW STATEMENT syl/HTML is very slow) */ /* 8-Aug-2008 nm This doesn't solve problem, because the bottleneck is printing g_printStringForReferencedBy below. This whole code section needs to be redesigned to solve the speed problem. */ /* 19-Sep-2012 nm Try again to fix SHOW STATEMENT syl/HTML speed without a major rewrite. Unfortunately, made little difference. */ /* 18-Jul-2015: Part of slowdown was due to the old traceUsage algorithm that built a huge string of labels. Improved from 313 sec to 280 sec for 'sh st syl/a'; still a problem. */ /* Accumulate large cat buffer when small cats exceed certain size */ if (strlen(str2) > 5000) { let(&str5, cat(str5, str2, NULL)); let(&str2, ""); } /* End 19-Sep-2012 */ } /* next m (statement number) */ /* 30-Oct-2018 nm Added "else" clause to print "(None)" if no refs */ } else { /* There is no usage of this statement; print "(None)" */ let(&str5, ""); let(&str2, cat(str2, " (None)", NULL)); } /* if (str1[0] == 'Y') */ /* let(&str2, cat(str2, "", NULL)); */ /* old */ /* 19-Sep-2012 nm Include buffer in output string*/ let(&str2, cat(str5, str2, "", NULL)); /*printLongLine(str2, "", "\"");*/ /* 18-Jul-2015 nm Deleted */ if (g_printString[0]) { bug(256); /* 18-Jul-2015 nm */ } let(&g_printString, str2); /* 18-Jul-2015 nm */ } /* if (subType != SYNTAX) */ if (subType == THEOREM) { /* 10/25/02 The "referenced by" does not show up after the proof because we moved the typeProof() to below. Therefore, we save g_printString into a temporary global holding variable to print at the proper place inside of typeProof(). Ugly but necessary with present design. */ /* In the case of THEOREM, we save and reset the g_printString. In the case of != THEOREM (i.e. AXIOM and DEFINITION), g_printString will be printed and cleared below. */ let(&g_printStringForReferencedBy, g_printString); let(&g_printString, ""); } /* Printing of the trailer in mmwtex.c will close out string later */ g_outputToString = 0; } /* if (htmlFlg && texFlag) */ /* 10/6/99 - End of used-by list for html page */ /* 10/25/02 Moved this to after the block above, so referenced statements show up first for convenience */ if (htmlFlg && texFlag) { /*** Output the html proof for $p statements ***/ /* Note that we also output the axiom and definition usage lists inside this function */ if (g_Statement[showStmt].type == (char)p_) { typeProof(showStmt, 0 /*pipFlag*/, 0 /*startStep*/, 0 /*endStep*/, 0 /*endIndent*/, 1 /*essentialFlag*/, 1 /*renumberFlag*/, 0 /*unknownFlag*/, 0 /*notUnifiedFlag*/, 0 /*reverseFlag*/, 1 /*noIndentFlag*/, 0 /*splitColumn*/, 0 /*skipRepeatedSteps*/, /* 28-Jun-2013 nm */ 1 /*texFlag*/, /* Means either latex or html */ 1 /*htmlFlg*/); } /* if (g_Statement[showStmt].type == (char)p_) */ } /* if (htmlFlg && texFlag) */ /* End of html proof for $p statements */ /* typeProof should have cleared this out */ if (g_printStringForReferencedBy[0]) bug(243); returnPoint: /* Deallocate strings */ nmbrLet(&nmbrDDList, NULL_NMBRSTRING); let(&str1, ""); let(&str2, ""); let(&str3, ""); let(&str4, ""); let(&str5, ""); let(&htmlDistinctVars, ""); } /* typeStatement */ /* 13-Aug-2017 nm */ /* Get the HTML string of dummy variables used by a proof for the theorem's web page. It should be called only if we're in HTML output mode i.e. SHOW STATEMENT .../HTML or /ALT_HTML */ /* This is HARD-CODED FOR SET.MM and will not produce meaningful output for other databases (so far none) with $d's */ /* Caller must deallocate returned string */ vstring htmlDummyVars(long showStmt) { nmbrString *optDVA; /* Pointer only; not allocated directly */ nmbrString *optDVB; /* Pointer only; not allocated directly */ long numDVs; nmbrString *optHyp; /* Pointer only; not allocated directly */ long numOptHyps; vstring str1 = ""; long k, l, n, hypStmt; /* Variables used while collecting a statement's dummy variables in $d's */ long dummyVarCount; /* # of (different) dummy vars found in $d statements */ vstring dummyVarUsed = ""; /* 'Y'/'N' indicators that we found that var */ vstring htmlDummyVarList = ""; /* Output HTML string */ long dummyVar; /* Current variable in a $d; test if it's a dummy variable */ /* This function should be called only for web page generation */ /*if (!(g_htmlFlag && texFlag)) bug(261);*/ /* texFlag is not global */ if (!g_htmlFlag) bug(261); if (g_Statement[showStmt].type != p_) bug(262); if (strcmp("|-", g_MathToken[ (g_Statement[showStmt].mathString)[0]].tokenName)) { /* Don't process syntax statements */ goto RETURN_POINT; } optDVA = g_Statement[showStmt].optDisjVarsA; optDVB = g_Statement[showStmt].optDisjVarsB; numDVs = nmbrLen(optDVA); optHyp = g_Statement[showStmt].optHypList; numOptHyps = nmbrLen(optHyp); if (numDVs == 0) { /* Don't create a hint list if no $d's */ /*let(&htmlDummyVarList, "(no restrictions)");*/ goto RETURN_POINT; } dummyVarCount = 0; if (numDVs != 0) { /* Update g_WrkProof.proofString with current proof so we can search it later to see if it uses the dummy variable */ parseProof(showStmt); /* Prints message if severe error */ /* Create an array of Y/N indicators that variable is occurs in a $d statement as a dummy variable */ let(&dummyVarUsed, string(g_mathTokens, 'N')); for (k = 0; k < numDVs; k++) { for (l = 1; l <= 2; l++) { if (l == 1) { dummyVar = optDVA[k]; } else { dummyVar = optDVB[k]; } /* At this point, dummyVar is just a var in the $d; we must still check that it is in the optHypList */ /* See if potential dummyVar is in optHypList */ if (dummyVarUsed[dummyVar] == 'N') { for (n = 0; n < numOptHyps; n++) { /* Check whether dummyVar matches the 2nd token of an optional hypothesis list entry e.g. "x" in "set x" */ hypStmt = g_Statement[showStmt].optHypList[n]; if (g_Statement[hypStmt].mathString[1] == dummyVar) { /* dummyVar is a dummy variable */ /* See if it is used by the proof */ /* g_WrkProof.proofString was updated by parseProof(showStmt) above */ if (nmbrElementIn(1, g_WrkProof.proofString, hypStmt) == 0) { break; /* It's not used by the proof; stop hyp scan */ } dummyVarUsed[dummyVar] = 'Y'; dummyVarCount++; /* tokenToTex allocates str1; must deallocate it first */ let(&str1, ""); /* Convert token to htmldef/althtmldef string */ str1 = tokenToTex(g_MathToken[dummyVar].tokenName, showStmt); let(&htmlDummyVarList, cat(htmlDummyVarList, " ", str1, NULL)); break; /* Found a match, so stop further checking */ } } /* next n, 0 to numOptHyps-1*/ } /* if dummy var not used (yet) */ } /* next l */ } /* next k */ } /* if (numDVs != 0) */ if (dummyVarCount > 0) { let(&htmlDummyVarList, cat( "
", " 0) ? "mmset.html" : /* The following link will work in the NF and other "Proof Explorers" */ "../mpeuni/mmset.html", /* 19-Aug-2017, 26-Sep-2017 nm */ "#dvnote1\">Dummy variable", /* Determine whether singular or plural */ dummyVarCount > 1 ? "s" : "", " ", /* 14-Aug-2017 nm */ /* 14-Jan-2016 nm Put a span around the variable list to localize the use of the special math font for ALT_HTML */ (g_altHtmlFlag ? cat("", NULL) : ""), /* 14-Jan-2016 nm */ htmlDummyVarList, (g_altHtmlFlag ? "" : ""), /* dummyVarCount > 1 ? " are assumed to be mutually distinct and" : " is assumed to be", */ dummyVarCount > 1 ? " are mutually distinct and" : " is", " distinct from all other variables.", "
", NULL)); } /* htmlDummyVars */ RETURN_POINT: /* Deallocate strings */ let(&dummyVarUsed, ""); let(&str1, ""); return htmlDummyVarList; } /* htmlDummyVars */ /* 4-Jan-2014 nm */ /* Get the HTML string of "allowed substitutions" list for an axiom or theorem's web page. It should be called only if we're in HTML output mode i.e. SHOW STATEMENT .../HTML or /ALT_HTML */ /* This is HARD-CODED FOR SET.MM and will not produce meaningful output for other databases (so far none) with $d's */ /* Caller must deallocate returned string */ vstring htmlAllowedSubst(long showStmt) { nmbrString *reqHyp; /* Pointer only; not allocated directly */ long numReqHyps; nmbrString *reqDVA; /* Pointer only; not allocated directly */ nmbrString *reqDVB; /* Pointer only; not allocated directly */ long numDVs; nmbrString *setVar = NULL_NMBRSTRING; /* set (individual) variables */ char *strptr; vstring str1 = ""; long setVars; long wffOrClassVar; vstring setVarDVFlag = ""; flag found, first; long i, j, k; vstring htmlAllowedList = ""; long countInfo = 0; reqDVA = g_Statement[showStmt].reqDisjVarsA; reqDVB = g_Statement[showStmt].reqDisjVarsB; numDVs = nmbrLen(reqDVA); reqHyp = g_Statement[showStmt].reqHypList; numReqHyps = nmbrLen(reqHyp); /* This function should be called only for web page generation */ /*if (!(g_htmlFlag && texFlag)) bug(250);*/ /* texFlag is not global */ if (!g_htmlFlag) bug(250); if (g_Statement[showStmt].mathStringLen < 1) bug(254); if (strcmp("|-", g_MathToken[ (g_Statement[showStmt].mathString)[0]].tokenName)) { /* Don't process syntax statements */ goto RETURN_POINT; } if (numDVs == 0) { /* Don't create a hint list if no $d's */ /*let(&htmlAllowedList, "(no restrictions)");*/ goto RETURN_POINT; } /* Collect list of all set variables in the theorem */ /* First, count the number of set variables */ setVars = 0; for (i = 0; i < numReqHyps; i++) { /* Scan "setvar" variables */ if (g_Statement[reqHyp[i]].type == (char)e_) continue; if (g_Statement[reqHyp[i]].type != (char)f_) bug(251); if (g_Statement[reqHyp[i]].mathStringLen != 2) bug(252); /* $f must have 2 tokens */ strptr = g_MathToken[ (g_Statement[reqHyp[i]].mathString)[0]].tokenName; /* THE FOLLOWING IS SPECIFIC TO set.mm */ if (strcmp("setvar", strptr)) continue; /* Not a set variable */ setVars++; } /* Next, create a list of them in setVar[] */ j = 0; nmbrLet(&setVar, nmbrSpace(setVars)); for (i = 0; i < numReqHyps; i++) { /* Scan "setvar" variables */ if (g_Statement[reqHyp[i]].type == (char)e_) continue; strptr = g_MathToken[ (g_Statement[reqHyp[i]].mathString)[0]].tokenName; if (strcmp("setvar", strptr)) continue; /* Not a set variable */ setVar[j] = (g_Statement[reqHyp[i]].mathString)[1]; j++; } if (j != setVars) bug(253); /* Scan "wff" and "class" variables for attached $d's */ for (i = 0; i < numReqHyps; i++) { /* Look for a "wff" and "class" variable */ if (g_Statement[reqHyp[i]].type == (char)e_) continue; strptr = g_MathToken[ (g_Statement[reqHyp[i]].mathString)[0]].tokenName; if (strcmp("wff", strptr) && strcmp("class", strptr)) continue; /* Not a wff or class variable */ wffOrClassVar = (g_Statement[reqHyp[i]].mathString)[1]; let(&setVarDVFlag, string(setVars, 'N')); /* No $d yet */ /* Scan for attached $d's */ for (j = 0; j < numDVs; j++) { found = 0; if (wffOrClassVar == reqDVA[j]) { for (k = 0; k < setVars; k++) { if (setVar[k] == reqDVB[j]) { setVarDVFlag[k] = 'Y'; found = 1; break; } } } if (found) continue; /* Repeat with swapped $d arguments */ if (wffOrClassVar == reqDVB[j]) { for (k = 0; k < setVars; k++) { if (setVar[k] == reqDVA[j]) { setVarDVFlag[k] = 'Y'; break; } } } } /* next $d */ /* Collect set vars that don't have $d's with this wff or class var */ /* First, if there aren't any, then omit this wff or class var */ found = 0; for (j = 0; j < setVars; j++) { if (setVarDVFlag[j] == 'N') { found = 1; break; } } if (found == 0) continue; /* All set vars have $d with this wff or class */ let(&str1, ""); str1 = tokenToTex(g_MathToken[wffOrClassVar].tokenName, showStmt); /* tokenToTex allocates str1; we must deallocate it eventually */ countInfo++; let(&htmlAllowedList, cat(htmlAllowedList, "   ", str1, "(", NULL)); first = 1; for (j = 0; j < setVars; j++) { if (setVarDVFlag[j] == 'N') { let(&str1, ""); str1 = tokenToTex(g_MathToken[setVar[j]].tokenName, showStmt); let(&htmlAllowedList, cat(htmlAllowedList, (first == 0) ? "," : "", str1, NULL)); if (first == 0) countInfo++; first = 0; } } let(&htmlAllowedList, cat(htmlAllowedList, ")", NULL)); } /* next i (wff or class var) */ RETURN_POINT: if (htmlAllowedList[0] != 0) { let(&htmlAllowedList, cat("
", " 0) ? "mmset.html" : /* The following link will work in the NF and other "Proof Explorers" */ "../mpeuni/mmset.html", /* 19-Aug-2017, 26-Sep-2017 nm */ "#allowedsubst\">Allowed substitution hint", ((countInfo != 1) ? "s" : ""), ": ", (g_altHtmlFlag ? cat("", NULL) : ""), /* 14-Jan-2016 nm */ htmlAllowedList, (g_altHtmlFlag ? "" : ""), /* 14-Jan-2016 nm */ "
", NULL)); } /* Deallocate strings */ nmbrLet(&setVar, NULL_NMBRSTRING); let(&str1, ""); let(&setVarDVFlag, ""); return htmlAllowedList; } /* htmlAllowedSubst */ /* Displays a proof (or part of a proof, depending on arguments). */ /* Note that parseProof() and verifyProof() are assumed to have been called, so that the g_WrkProof structure elements are assigned for the current statement. */ /* 8/28/00 - this is also used for the MIDI output, since we conveniently have the necessary proof information here. The function outputMidi() is called from within. */ void typeProof(long statemNum, flag pipFlag, /* Means use g_ProofInProgress; statemNum must be proveStatement*/ long startStep, long endStep, long endIndent, flag essentialFlag, /* <- also used as definition/axiom flag for HTML syntax breakdown when called from typeStatement() */ flag renumberFlag, flag unknownFlag, flag notUnifiedFlag, flag reverseFlag, flag noIndentFlag, /* Means Lemmon-style proof */ long splitColumn, /* START_COLUMN */ flag skipRepeatedSteps, /* NO_REPEATED_STEPS */ /* 28-Jun-2013 nm */ flag texFlag, flag htmlFlg /* htmlFlg added 6/27/99 */ /* flag g_midiFlag - global to avoid changing many calls to typeProof() */ ) { /* From HELP SHOW PROOF: Optional qualifiers: / ESSENTIAL - the proof tree is trimmed of all $f hypotheses before being displayed. / FROM_STEP - the display starts at the specified step. If this qualifier is omitted, the display starts at the first step. / TO_STEP - the display ends at the specified step. If this qualifier is omitted, the display ends at the last step. / TREE_DEPTH - Only steps at less than the specified proof tree depth are displayed. Useful for obtaining an overview of the proof. / REVERSE - the steps are displayed in reverse order. / RENUMBER - when used with / ESSENTIAL, the steps are renumbered to correspond only to the essential steps. / TEX - the proof is converted to LaTeX and stored in the file opened with OPEN TEX. / HTML - the proof is converted to HTML and stored in the file opened with OPEN HTML. / LEMMON - The proof is displayed in a non-indented format known as Lemmon style, with explicit previous step number references. If this qualifier is omitted, steps are indented in a tree format. / START_COLUMN - Overrides the default column at which the formula display starts in a Lemmon style display. May be used only in conjuction with / LEMMON. / NO_REPEATED_STEPS - When a proof step is identical to an earlier step, it will not be repeated. Instead, a reference to it will be changed to a reference to the earlier step. In particular, SHOW PROOF
", "Colors of variables: ", g_htmlVarColor, "
This ", str3, " is referenced by:", NULL)); if (str1[0] == 'Y') { /* Used by at least one */ /********* 18-Jul-2015 Deleted code *********************/ /* /@ Convert str1 to trailing space after each label @/ let(&str1, cat(right(str1, 2), " ", NULL)); let(&str5, ""); /@ Buffer for very long strings @/ /@ 19-Sep-2012 nm @/ i = 0; while (1) { j = i + 1; i = instr(j, str1, " "); if (!i) break; /@ Extract the label @/ let(&str3, seg(str1, j, i - 1)); /@ Find the statement number @/ m = lookupLabel(str3); if (m < 0) { /@ The lookup should never fail @/ bug(240); continue; } /@ It should be a $p @/ if (g_Statement[m].type != p_) bug(241); /@ Get the pink number @/ let(&str4, ""); str4 = pinkHTML(m); /@ Assemble the href @/ let(&str2, cat(str2, "  ", str3, "", str4, NULL)); /@ 8-Aug-2008 nm If line is very long, print it out and reset it to speed up program (SHOW STATEMENT syl/HTML is very slow) @/ /@ 8-Aug-2008 nm This doesn't solve problem, because the bottleneck is printing g_printStringForReferencedBy below. This whole code section needs to be redesigned to solve the speed problem. @/ /@ if (strlen(str2) > 500) { printLongLine(str2, "", "\""); let(&str2, ""); } @/ /@ 19-Sep-2012 nm Try again to fix SHOW STATEMENT syl/HTML speed without a major rewrite @/ /@ Unfortunately, makes little difference. Using lcc: orig real 1m6.676s 500 real 1m2.285s 3000 real 1m2.181s 3000 real 1m1.663s 3000 real 1m1.785s 5000 real 1m0.678s 5000 real 1m0.169s 5000 real 1m1.951s 5000 real 1m2.307s 5000 real 1m1.717s 7000 real 1m2.048s 7000 real 1m2.012s 7000 real 1m1.817s 10000 real 1m2.779s 10000 real 1m1.830s 20000 real 1m1.431s 50000 real 1m1.325s 100000 real 1m3.172s 100000 real 1m4.657s (Added 17-Jul-2015: The 1 minute is probably due to the old traceUsage algorithm that built a huge string of labels; should be faster now.) @/ /@ Accumulate large cat buffer when small cats exceed certain size @/ if (strlen(str2) > 5000) { let(&str5, cat(str5, str2, NULL)); let(&str2, ""); } /@ End 19-Sep-2012 @/ } /@ let(&str2, cat(str2, "
\n"); } else { /* End of 26-Aug-2017 */ /* For bobby.cast.org approval */ print2("
\n"); print2("", NULL), "", "\""); } } else { /* This is a syntax breakdown "proof" of a definition called from typeStatement */ print2("
Proof of Theorem ", asciiToTt(g_Statement[statemNum].labelName), "
\n"); print2("", NULL), "", "\""); } print2( "\n"); g_outputToString = 0; /* printTexLongMath in typeProof will do this fprintf(g_texFilePtr, "%s", g_printString); let(&g_printString, ""); */ } if (!pipFlag) { parseProof(g_showStatement); if (g_WrkProof.errorSeverity > 1) { /* 2-Nov-2014 nm Prevent population of g_printString outside of web page generation to fix bug 1114 (reported by Sefan O'Rear). */ if (htmlFlg && texFlag) { /* Print warning and close out proof table */ g_outputToString = 1; print2( "\n"); g_outputToString = 0; /* 18-Nov-2012 nm Fix bug 243 */ /* Clear out g_printStringForReferencedBy to prevent bug 243 above */ let(&g_printStringForReferencedBy, ""); } return; /* verifyProof() could crash */ } verifyProof(g_showStatement); } if (!pipFlag) { nmbrLet(&proof, g_WrkProof.proofString); /* The proof */ if (g_midiFlag) { /* 8/28/00 */ /* Get the uncompressed version of the proof */ nmbrLet(&proof, nmbrUnsquishProof(proof)); } } else { nmbrLet(&proof, g_ProofInProgress.proof); /* The proof */ } plen = nmbrLen(proof); /* 6/27/99 - to reduce the number of steps displayed in an html proof, we will use a local label to reference the 2nd or later reference to a hypothesis, so the hypothesis won't have to be shown multiple times in the proof. 31-Jan-2010 - do this for all Lemmon-style proofs */ if (htmlFlg && texFlag && !noIndentFlag /* Lemmon */) { /* Only Lemmon-style proofs are implemented for html */ bug(218); } /*if (htmlFlg && texFlag) {*/ /* pre-31-Jan-2010 */ /* 31-Jan-2010 nm Do this for all Lemmon-style proofs */ if (skipRepeatedSteps) { for (step = 0; step < plen; step++) { stmt = proof[step]; if (stmt < 0) continue; /* Unknown or label ref */ type = g_Statement[stmt].type; if (type == f_ || type == e_ /* It's a hypothesis */ || g_Statement[stmt].numReqHyp == 0) { /* A statement w/ no hyp */ for (i = 0; i < step; i++) { if (stmt == proof[i]) { /* The hypothesis at 'step' matches an earlier hypothesis at i, so we will backreference 'step' to i with a local label */ proof[step] = -1000 - i; break; } } /* next i */ } } /* next step */ } /* Collect local labels */ for (step = 0; step < plen; step++) { stmt = proof[step]; if (stmt <= -1000) { stmt = -1000 - stmt; if (!nmbrElementIn(1, localLabels, stmt)) { nmbrLet(&localLabels, nmbrAddElement(localLabels, stmt)); } } } /* localLabelNames[] hold an integer which, when converted to string, is the local label name. */ nmbrLet(&localLabelNames, nmbrSpace(plen)); /* Get the indentation level */ nmbrLet(&indentationLevel, nmbrGetIndentation(proof, 0)); /* Get the target hypotheses */ nmbrLet(&targetHyps, nmbrGetTargetHyp(proof, statemNum)); /* Get the essential step flags, if required */ if (essentialFlag || g_midiFlag) { nmbrLet(&essentialFlags, nmbrGetEssential(proof)); } else { nmbrLet(&essentialFlags, NULL_NMBRSTRING); } /* 8/28/00 We now have enough information for the MIDI output, so do it */ if (g_midiFlag) { outputMidi(plen, indentationLevel, essentialFlags, g_midiParam, g_Statement[statemNum].labelName); goto typeProof_return; } /* Get the step renumbering */ nmbrLet(&stepRenumber, nmbrSpace(plen)); /* This initializes all step renumbering to step 0. Later, we will use (for html) the fact that a step renumbered to 0 is a step to be skipped (6/27/99). */ i = 0; maxStepNum = 0; for (step = 0; step < plen; step++) { stepPrintFlag = 1; /* Note: stepPrintFlag is reused below with a slightly different meaning (i.e. it will be printed after a filter such as notUnified is applied) */ if (renumberFlag && essentialFlag) { if (!essentialFlags[step]) stepPrintFlag = 0; } /* if (htmlFlg && texFlag && proof[step] < 0) stepPrintFlag = 0; */ /* 31-Jan-2010 nm changed to: */ if (skipRepeatedSteps && proof[step] < 0) stepPrintFlag = 0; /* For standard numbering, stepPrintFlag will be always be 1 here */ if (stepPrintFlag) { i++; stepRenumber[step] = i; /* Numbering for step to be printed */ maxStepNum = i; /* To compute maxStepNumLen below */ } } /* 22-Apr-2015 nm */ /* Get the relative offset (0, -1, -2,...) for unknown steps */ if (unknownFlag) { /* 21-Aug-2017 nm There could be unknown steps outside of MM-PA So remove this bugcheck, which seems spurious. I can't see that getRelStepNums() cares whether we are in MM-PA. */ /* if (!pipFlag) { bug(255); } */ relativeStepNums = getRelStepNums(g_ProofInProgress.proof); } /* Get steps not unified (pipFlag only) */ if (notUnifiedFlag) { if (!pipFlag) bug(205); nmbrLet(¬UnifiedFlags, nmbrSpace(plen)); for (step = 0; step < plen; step++) { notUnifiedFlags[step] = 0; if (nmbrLen(g_ProofInProgress.source[step])) { if (!nmbrEq(g_ProofInProgress.target[step], g_ProofInProgress.source[step])) notUnifiedFlags[step] = 1; } if (nmbrLen(g_ProofInProgress.user[step])) { if (!nmbrEq(g_ProofInProgress.target[step], g_ProofInProgress.user[step])) notUnifiedFlags[step] = 1; } } } /* Get the printed character length of the largest step number */ i = maxStepNum; while (i >= 10) { i = i/10; /* The number is printed in base 10 */ maxStepNumLen++; } /* 22-Apr-2015 nm */ /* Add extra space for negative offset numbers e.g. "3:-1" */ if (unknownFlag) { maxStepNumOffsetLen = 3; /* :, -, # */ j = 0; for (i = 0; i < plen; i++) { j = relativeStepNums[i]; if (j <= 0) break; /* Found first unknown step (largest offset) */ } while (j <= -10) { j = j/10; /* The number is printed in base 10 */ maxStepNumOffsetLen++; } } /* Get local labels and maximum label length */ /* lent = target length, lens = source length */ for (step = 0; step < plen; step++) { lent = (long)strlen(g_Statement[targetHyps[step]].labelName); stmt = proof[step]; if (stmt < 0) { if (stmt <= -1000) { stmt = -1000 - stmt; /* stmt is now the step number a local label refers to */ lens = (long)strlen(str((double)(localLabelNames[stmt]))); let(&tmpStr1, ""); /* Clear temp alloc stack for str function */ } else { if (stmt != -(long)'?') bug (219); /* the only other possibility */ lens = 1; /* '?' (unknown step) */ } } else { if (nmbrElementIn(1, localLabels, step)) { /* 6/27/99 The new philosophy is to number all local labels with the actual step number referenced, for better readability. This means that if a *.mm label is a pure number, there may be ambiguity in the proof display, but this is felt to be too rare to be a serious drawback. */ localLabelNames[step] = stepRenumber[step]; } lens = (long)strlen(g_Statement[stmt].labelName); } /* Find longest label assignment, excluding local label declaration */ if (maxLabelLen < lent + 1 + lens) { maxLabelLen = lent + 1 + lens; /* Target, =, source */ } } /* Next step */ /* Print the steps */ if (reverseFlag && !g_midiFlag /* 8/28/00 */ ) { fromStep = plen - 1; toStep = -1; byStep = -1; } else { fromStep = 0; toStep = plen; byStep = 1; } for (step = fromStep; step != toStep; step = step + byStep) { /* Filters to decide whether to print the step */ stepPrintFlag = 1; if (startStep > 0) { /* The user's FROM_STEP */ if (step + 1 < startStep) stepPrintFlag = 0; } if (endStep > 0) { /* The user's TO_STEP */ if (step + 1 > endStep) stepPrintFlag = 0; } if (endIndent > 0) { /* The user's INDENTATION_DEPTH */ if (indentationLevel[step] + 1 > endIndent) stepPrintFlag = 0; } if (essentialFlag) { if (!essentialFlags[step]) stepPrintFlag = 0; } if (notUnifiedFlag) { if (!notUnifiedFlags[step]) stepPrintFlag = 0; } if (unknownFlag) { if (proof[step] != -(long)'?') stepPrintFlag = 0; } /* 6/27/99 Skip steps that are local label references for html */ /* if (htmlFlg && texFlag) { */ /* 31-Jan-2010 nm changed to: */ if (skipRepeatedSteps) { if (stepRenumber[step] == 0) stepPrintFlag = 0; } /* 8/28/00 For MIDI files, ignore all qualifiers and process all steps */ if (g_midiFlag) stepPrintFlag = 1; if (!stepPrintFlag) continue; if (noIndentFlag) { let(&tgtLabel, ""); } else { let(&tgtLabel, g_Statement[targetHyps[step]].labelName); } let(&locLabDecl, ""); /* Local label declaration */ stmt = proof[step]; if (stmt < 0) { if (stmt <= -1000) { stmt = -1000 - stmt; /* if (htmlFlg && texFlag) bug(220); */ /* 31-Jan-2010 nm Changed to: */ if (skipRepeatedSteps) bug(220); /* If html, a step referencing a local label will never be printed since it will be skipped above */ /* stmt is now the step number a local label refers to */ if (noIndentFlag) { let(&srcLabel, cat("@", str((double)(localLabelNames[stmt])), NULL)); } else { let(&srcLabel, cat("=", str((double)(localLabelNames[stmt])), NULL)); } type = g_Statement[proof[stmt]].type; } else { if (stmt != -(long)'?') bug(206); if (noIndentFlag) { let(&srcLabel, chr(-stmt)); /* '?' */ } else { let(&srcLabel, cat("=", chr(-stmt), NULL)); /* '?' */ } type = '?'; } } else { if (nmbrElementIn(1, localLabels, step)) { /* This statement declares a local label */ if (noIndentFlag) { /* if (!(htmlFlg && texFlag)) { */ /* 31-Jan-2010 nm Changed to: */ if (!(skipRepeatedSteps)) { /* No local label declaration is shown for html */ let(&locLabDecl, cat("@", str((double)(localLabelNames[step])), ":", NULL)); } } else { let(&locLabDecl, cat(str((double)(localLabelNames[step])), ":", NULL)); } } if (noIndentFlag) { let(&srcLabel, g_Statement[stmt].labelName); /* For non-indented mode, add step numbers of hypotheses after label */ let(&hypStr, ""); hypStep = step - 1; hypPtr = g_Statement[stmt].reqHypList; for (hyp = g_Statement[stmt].numReqHyp - 1; hyp >=0; hyp--) { if (!essentialFlag || g_Statement[hypPtr[hyp]].type == (char)e_) { i = stepRenumber[hypStep]; if (i == 0) { /* if (!(htmlFlg && texFlag)) bug(221); */ /* 31-Jan-2010 nm Changed to: */ if (!(skipRepeatedSteps)) bug(221); if (proof[hypStep] != -(long)'?') { if (proof[hypStep] > -1000) bug(222); if (localLabelNames[-1000 - proof[hypStep]] == 0) bug(223); if (localLabelNames[-1000 - proof[hypStep]] != stepRenumber[-1000 - proof[hypStep]]) bug(224); /* Get the step number the hypothesis refers to */ i = stepRenumber[-1000 - proof[hypStep]]; } else { /* The hypothesis refers to an unknown step - use i as flag */ i = -(long)'?'; } } if (!hypStr[0]) { if (i != -(long)'?') { let(&hypStr, str((double)i)); } else { let(&hypStr, "?"); } } else { /* Put comma between more than one hypothesis reference */ if (i != -(long)'?') { let(&hypStr, cat(str((double)i), ",", hypStr, NULL)); } else { let(&hypStr, cat("?", ",", hypStr, NULL)); } } } if (hyp < g_Statement[stmt].numReqHyp) { /* Move down to previous hypothesis */ hypStep = hypStep - subproofLen(proof, hypStep); } } /* Next hyp */ if (hypStr[0]) { /* Add hypothesis list after label */ let(&srcLabel, cat(hypStr, " ", srcLabel, NULL)); } } else { let(&srcLabel, cat("=", g_Statement[stmt].labelName, NULL)); } type = g_Statement[stmt].type; } #define PF_INDENT_INC 2 /* Print the proof line */ if (stepPrintFlag) { if (noIndentFlag) { let(&startPrefix, cat( space(maxStepNumLen - (long)strlen(str((double)(stepRenumber[step])))), str((double)(stepRenumber[step])), " ", srcLabel, space(splitColumn - (long)strlen(srcLabel) - (long)strlen(locLabDecl) - 1 - maxStepNumLen - 1), " ", locLabDecl, NULL)); if (pipFlag) { let(&tgtPrefix, startPrefix); let(&srcPrefix, cat( space(maxStepNumLen - (long)strlen(str((double)(stepRenumber[step])))), space((long)strlen(str((double)(stepRenumber[step])))), " ", space(splitColumn - 1 - maxStepNumLen), NULL)); let(&userPrefix, cat( space(maxStepNumLen - (long)strlen(str((double)(stepRenumber[step])))), space((long)strlen(str((double)(stepRenumber[step])))), " ", "(User)", space(splitColumn - (long)strlen("(User)") - 1 - maxStepNumLen), NULL)); } let(&contPrefix, space((long)strlen(startPrefix) + 4)); } else { /* not noIndentFlag */ /* 22-Apr-2015 nm */ /* Compute prefix with and without step number. For 'show new_proof /unknown', unknownFlag is set, and we add the negative offset. */ let(&tmpStr, ""); if (unknownFlag) { if (relativeStepNums[step] < 0) { let(&tmpStr, cat(" ", str((double)(relativeStepNums[step])), NULL)); } let(&tmpStr, cat(tmpStr, space(maxStepNumOffsetLen - (long)(strlen(tmpStr))), NULL)); } let(&startStringWithNum, cat( space(maxStepNumLen - (long)strlen(str((double)(stepRenumber[step])))), str((double)(stepRenumber[step])), tmpStr, " ", NULL)); let(&startStringWithoutNum, space(maxStepNumLen + 1)); let(&startPrefix, cat( startStringWithNum, space(indentationLevel[step] * PF_INDENT_INC - (long)strlen(locLabDecl)), locLabDecl, tgtLabel, srcLabel, space(maxLabelLen - (long)strlen(tgtLabel) - (long)strlen(srcLabel)), NULL)); if (pipFlag) { let(&tgtPrefix, cat( startStringWithNum, space(indentationLevel[step] * PF_INDENT_INC - (long)strlen(locLabDecl)), locLabDecl, tgtLabel, space((long)strlen(srcLabel)), space(maxLabelLen - (long)strlen(tgtLabel) - (long)strlen(srcLabel)), NULL)); let(&srcPrefix, cat( startStringWithoutNum, space(indentationLevel[step] * PF_INDENT_INC - (long)strlen(locLabDecl)), space((long)strlen(locLabDecl)), space((long)strlen(tgtLabel)), srcLabel, space(maxLabelLen - (long)strlen(tgtLabel) - (long)strlen(srcLabel)), NULL)); let(&userPrefix, cat( startStringWithoutNum, space(indentationLevel[step] * PF_INDENT_INC - (long)strlen(locLabDecl)), space((long)strlen(locLabDecl)), space((long)strlen(tgtLabel)), "=(User)", space(maxLabelLen - (long)strlen(tgtLabel) - (long)strlen("=(User)")), NULL)); } /* let(&contPrefix, space(maxStepNumLen + 1 + indentationLevel[step] * PF_INDENT_INC + maxLabelLen + 4)); */ let(&contPrefix, ""); /* Continuation lines use whole screen width */ } if (!pipFlag) { if (!texFlag) { if (!g_midiFlag) { /* 8/28/00 */ printLongLine(cat(startPrefix," $", chr(type), " ", nmbrCvtMToVString(g_WrkProof.mathStringPtrs[step]), NULL), contPrefix, chr(1)); /* chr(1) is right-justify flag for printLongLine */ } } else { /* TeX or HTML */ printTexLongMath(g_WrkProof.mathStringPtrs[step], cat(startPrefix, " $", chr(type), " ", NULL), contPrefix, stmt, indentationLevel[step]); } } else { /* pipFlag */ if (texFlag) { /* nm 3-Feb-04 Added this bug check - it doesn't make sense to do this and it hasn't been tested anyway */ print2("?Unsupported: HTML or LaTeX proof for NEW_PROOF.\n"); bug(244); } if (!nmbrEq(g_ProofInProgress.target[step], g_ProofInProgress.source[step]) && nmbrLen(g_ProofInProgress.source[step])) { if (!texFlag) { printLongLine(cat(tgtPrefix, " $", chr(type), " ", nmbrCvtMToVString(g_ProofInProgress.target[step]), NULL), contPrefix, chr(1)); /* chr(1) is right-justify flag for printLongLine */ printLongLine(cat(srcPrefix," = ", nmbrCvtMToVString(g_ProofInProgress.source[step]), NULL), contPrefix, chr(1)); /* chr(1) is right-justify flag for printLongLine */ } else { /* TeX or HTML */ printTexLongMath(g_ProofInProgress.target[step], cat(tgtPrefix, " $", chr(type), " ", NULL), contPrefix, 0, 0); printTexLongMath(g_ProofInProgress.source[step], cat(srcPrefix, " = ", NULL), contPrefix, 0, 0); } } else { if (!texFlag) { printLongLine(cat(startPrefix, " $", chr(type), " ", nmbrCvtMToVString(g_ProofInProgress.target[step]), NULL), contPrefix, chr(1)); /* chr(1) is right-justify flag for printLongLine */ } else { /* TeX or HTML */ printTexLongMath(g_ProofInProgress.target[step], cat(startPrefix, " $", chr(type), " ", NULL), contPrefix, 0, 0); } } if (nmbrLen(g_ProofInProgress.user[step])) { if (!texFlag) { printLongLine(cat(userPrefix, " = ", nmbrCvtMToVString(g_ProofInProgress.user[step]), NULL), contPrefix, chr(1)); /* chr(1) is right-justify flag for printLongLine */ } else { printTexLongMath(g_ProofInProgress.user[step], cat(userPrefix, " = ", NULL), contPrefix, 0, 0); } } } } } /* Next step */ if (!pipFlag) { cleanWrkProof(); /* Deallocate verifyProof storage */ } if (htmlFlg && texFlag) { g_outputToString = 1; print2("
Detailed syntax breakdown of Axiom \n"); print2("Detailed syntax breakdown of Definition ", asciiToTt(g_Statement[statemNum].labelName), "
StepHypRef\n"); print2("Expression
WARNING: Proof has a severe error.\n"); print2("
\n"); /* 10/10/02 Moved here from mmwtex.c */ /*print2("Colors of variables:\n");*/ printLongLine(cat( "
", NULL), "", "\""); if (essentialFlag) { /* Means this is not a syntax breakdown of a definition which is called from typeStatement() */ /* Create list of syntax statements used */ let(&statementUsedFlags, string(g_statements + 1, 'N')); /* Init. to 'no' */ for (step = 0; step < plen; step++) { stmt = proof[step]; /* Convention: collect all $a's that don't begin with "|-" */ if (stmt > 0) { if (g_Statement[stmt].type == a_) { if (strcmp("|-", g_MathToken[ (g_Statement[stmt].mathString)[0]].tokenName)) { statementUsedFlags[stmt] = 'Y'; /* Flag to use it */ } } } } /******************************************************************/ /* Start of section added 2/5/02 - for a more complete syntax hints list in the HTML pages, parse the wffs comprising the hypotheses and the statement, and add their syntax to the hints list. */ /* Look up the token "wff" (hard-coded) if we haven't found it before */ if (wffToken == -1) { /* First time */ wffToken = -2; /* In case it's not found because the user's source used a convention different for "wff" for wffs */ for (i = 0; i < g_mathTokens; i++) { if (!strcmp("wff", g_MathToken[i].tokenName)) { wffToken = i; break; } } } if (wffToken >= 0) { /* Scan the statement being proved and its essential hypotheses, and find a proof for each of them expressed as a wff */ for (i = -1; i < g_Statement[statemNum].numReqHyp; i++) { /* i = -1 is the statement itself; i >= 0 is hypotheses i */ if (i == -1) { /* If it's not a $p we shouldn't be here */ if (g_Statement[statemNum].type != (char)p_) bug(245); nmbrTmpPtr1 = NULL_NMBRSTRING; nmbrLet(&nmbrTmpPtr1, g_Statement[statemNum].mathString); } else { /* Ignore $f */ if (g_Statement[g_Statement[statemNum].reqHypList[i]].type == (char)f_) continue; /* Must therefore be a $e */ if (g_Statement[g_Statement[statemNum].reqHypList[i]].type != (char)e_) bug(234); nmbrTmpPtr1 = NULL_NMBRSTRING; nmbrLet(&nmbrTmpPtr1, g_Statement[g_Statement[statemNum].reqHypList[i]].mathString); } if (strcmp("|-", g_MathToken[nmbrTmpPtr1[0]].tokenName)) { /* 1-Oct-05 nm Since non-standard logics may not have this, just break out of this section gracefully */ nmbrTmpPtr2 = NULL_NMBRSTRING; /* To be known after break */ break; /* bug(235); */ /* 1-Oct-05 nm No longer a bug */ } /* Turn "|-" assertion into a "wff" assertion */ nmbrTmpPtr1[0] = wffToken; /* Find proof of formula or simple theorem (no new vars in $e's) */ /* maxEDepth is the maximum depth at which statements with $e hypotheses are considered. A value of 0 means none are considered. */ nmbrTmpPtr2 = proveFloating(nmbrTmpPtr1 /*mString*/, statemNum /*statemNum*/, 0 /*maxEDepth*/, 0, /* step; 0 = step 1 */ /*For messages*/ 0, /*not noDistinct*/ /* 3-May-2016 nm */ 2, /* override discouraged-usage statements silently */ 1 /* Always allow other mathboxes */ /* 5-Aug-2020 nm */ ); if (!nmbrLen(nmbrTmpPtr2)) { /* 1-Oct-05 nm Since a proof may not be found for non-standard logics, just break out of this section gracefully */ break; /* bug(236); */ /* Didn't find syntax proof */ } /* Add to list of syntax statements used */ for (step = 0; step < nmbrLen(nmbrTmpPtr2); step++) { stmt = nmbrTmpPtr2[step]; /* Convention: collect all $a's that don't begin with "|-" */ if (stmt > 0) { if (statementUsedFlags[stmt] == 'N') { /* For slight speedup */ if (g_Statement[stmt].type == a_) { if (strcmp("|-", g_MathToken[ (g_Statement[stmt].mathString)[0]].tokenName)) { statementUsedFlags[stmt] = 'Y'; /* Flag to use it */ } else { /* In a syntax proof there should be no |- */ /* (In the future, we may want to break instead of calling it a bug, if it's a problem for non-standard logics.) */ bug(237); } } } } else { /* proveFloating never returns a compressed proof */ bug(238); } } /* Deallocate memory */ nmbrLet(&nmbrTmpPtr2, NULL_NMBRSTRING); nmbrLet(&nmbrTmpPtr1, NULL_NMBRSTRING); } /* next i */ /* 1-Oct-05 nm Deallocate memory in case we broke out above */ nmbrLet(&nmbrTmpPtr2, NULL_NMBRSTRING); nmbrLet(&nmbrTmpPtr1, NULL_NMBRSTRING); } /* if (wffToken >= 0) */ /* End of section added 2/5/02 */ /******************************************************************/ let(&tmpStr, ""); for (stmt = 1; stmt <= g_statements; stmt++) { if (statementUsedFlags[stmt] == 'Y') { if (!tmpStr[0]) { let(&tmpStr, /* 10/10/02 */ /*"Syntax hints: ");*/ "", NULL)); printLongLine(tmpStr, "", "\""); } /* End of syntax hints list */ /* 10/25/02 Output "referenced by" list here */ /* 30-Oct-2018 nm Moved this block to after axioms/defs lists */ /* if (g_printStringForReferencedBy[0]) { /@ printLongLine takes 130 sec for 'sh st syl/a' @/ /@printLongLine(g_printStringForReferencedBy, "", "\"");@/ /@ 18-Jul-2015 nm Speedup for 'sh st syl/a' @/ if (g_outputToString != 1) bug(257); let(&g_printString, cat(g_printString, g_printStringForReferencedBy, NULL)); let(&g_printStringForReferencedBy, ""); } */ /* Get list of axioms and definitions assumed by proof */ let(&statementUsedFlags, ""); traceProofWork(statemNum, 1, /*essentialFlag*/ "", /*traceToList*/ /* 18-Jul-2015 nm */ &statementUsedFlags, /*&statementUsedFlags*/ &unprovedList /* &unprovedList */); if ((signed)(strlen(statementUsedFlags)) != g_statements + 1) bug(227); /* First get axioms */ let(&tmpStr, ""); for (stmt = 1; stmt <= g_statements; stmt++) { if (statementUsedFlags[stmt] == 'Y' && g_Statement[stmt].type == a_) { let(&tmpStr1, left(g_Statement[stmt].labelName, 3)); if (!strcmp(tmpStr1, "ax-")) { if (!tmpStr[0]) { let(&tmpStr, /******* 10/10/02 "The theorem was proved from these axioms: "); *******/ "", NULL)); printLongLine(tmpStr, "", "\""); } /* 10/10/02 Then get definitions */ let(&tmpStr, ""); for (stmt = 1; stmt <= g_statements; stmt++) { if (statementUsedFlags[stmt] == 'Y' && g_Statement[stmt].type == a_) { let(&tmpStr1, left(g_Statement[stmt].labelName, 3)); if (!strcmp(tmpStr1, "df-")) { if (!tmpStr[0]) { let(&tmpStr, "", NULL)); printLongLine(tmpStr, "", "\""); } /* Print any unproved statements */ if (nmbrLen(unprovedList)) { if (nmbrLen(unprovedList) == 1 && !strcmp(g_Statement[unprovedList[0]].labelName, g_Statement[statemNum].labelName)) { /* When the unproved list consists only of the statement that was traced, it means the statement traced has no proof (or it has a proof, but is incomplete and all earlier ones do have complete proofs). */ printLongLine(cat( "", NULL), "", "\""); } else { printLongLine(cat( "", NULL), "", "\""); } } /* End of axiom list */ /* 30-Oct-2018 nm Moved down from above to put referenced by list last */ if (g_printStringForReferencedBy[0]) { /* printLongLine takes 130 sec for 'sh st syl/a' */ /*printLongLine(g_printStringForReferencedBy, "", "\"");*/ /* 18-Jul-2015 nm Speedup for 'sh st syl/a' */ if (g_outputToString != 1) bug(257); /* 30-Oct-2018 nm Deleted line: */ /*let(&g_printString, cat(g_printString, g_printStringForReferencedBy, NULL));*/ /* 30-Oct-2018 nm Added line: */ printLongLine(g_printStringForReferencedBy, "", "\""); let(&g_printStringForReferencedBy, ""); /* 30-Oct-2018 nm */ } else { /* Since we now always print ref-by list even if "(None)", g_printStringForReferencedBy should never be empty */ bug(263); } } /* if essentialFlag */ /* Printing of the trailer in mmwtex.c will close out string later */ g_outputToString = 0; } typeProof_return: let(&tmpStr, ""); let(&tmpStr1, ""); let(&statementUsedFlags, ""); let(&locLabDecl, ""); let(&tgtLabel, ""); let(&srcLabel, ""); let(&startPrefix, ""); let(&tgtPrefix, ""); let(&srcPrefix, ""); let(&userPrefix, ""); let(&contPrefix, ""); let(&hypStr, ""); let(&startStringWithNum, ""); /* 22-Apr-2015 nm */ let(&startStringWithoutNum, ""); /* 22-Apr-2015 nm */ nmbrLet(&unprovedList, NULL_NMBRSTRING); nmbrLet(&localLabels, NULL_NMBRSTRING); nmbrLet(&localLabelNames, NULL_NMBRSTRING); nmbrLet(&proof, NULL_NMBRSTRING); nmbrLet(&targetHyps, NULL_NMBRSTRING); nmbrLet(&indentationLevel, NULL_NMBRSTRING); nmbrLet(&essentialFlags, NULL_NMBRSTRING); nmbrLet(&stepRenumber, NULL_NMBRSTRING); nmbrLet(¬UnifiedFlags, NULL_NMBRSTRING); nmbrLet(&relativeStepNums, NULL_NMBRSTRING); /* 22-Apr-2015 nm */ } /* typeProof() */ /* Show details of one proof step */ /* Note: detailStep is the actual step number (starting with 1), not the actual step - 1. */ void showDetailStep(long statemNum, long detailStep) { long i, j, plen, step, stmt, sourceStmt, targetStmt; vstring tmpStr = ""; vstring tmpStr1 = ""; nmbrString *proof = NULL_NMBRSTRING; nmbrString *localLabels = NULL_NMBRSTRING; nmbrString *localLabelNames = NULL_NMBRSTRING; nmbrString *targetHyps = NULL_NMBRSTRING; long nextLocLabNum = 1; /* Next number to be used for a local label */ void *voidPtr; /* bsearch result */ char type; /* Error check */ i = parseProof(statemNum); if (i) { printLongLine("?The proof is incomplete or has an error", "", " "); return; } plen = nmbrLen(g_WrkProof.proofString); if (plen < detailStep || detailStep < 1) { printLongLine(cat("?The step number should be from 1 to ", str((double)plen), NULL), "", " "); return; } /* Structure getStep is declared in mmveri.h. */ getStep.stepNum = detailStep; /* Non-zero is flag for verifyProof */ parseProof(statemNum); /* ???Do we need to do this again? */ verifyProof(statemNum); nmbrLet(&proof, g_WrkProof.proofString); /* The proof */ plen = nmbrLen(proof); /* Collect local labels */ for (step = 0; step < plen; step++) { stmt = proof[step]; if (stmt <= -1000) { stmt = -1000 - stmt; if (!nmbrElementIn(1, localLabels, stmt)) { nmbrLet(&localLabels, nmbrAddElement(localLabels, stmt)); } } } /* localLabelNames[] hold an integer which, when converted to string, is the local label name. */ nmbrLet(&localLabelNames, nmbrSpace(plen)); /* Get the target hypotheses */ nmbrLet(&targetHyps, nmbrGetTargetHyp(proof, statemNum)); /* Get local labels */ for (step = 0; step < plen; step++) { stmt = proof[step]; if (stmt >= 0) { if (nmbrElementIn(1, localLabels, step)) { /* This statement declares a local label */ /* First, get a name for the local label, using the next integer that does not match any integer used for a statement label. */ let(&tmpStr1, str((double)nextLocLabNum)); while (1) { voidPtr = (void *)bsearch(tmpStr, g_allLabelKeyBase, (size_t)g_numAllLabelKeys, sizeof(long), labelSrchCmp); if (!voidPtr) break; /* It does not conflict */ nextLocLabNum++; /* Try the next one */ let(&tmpStr1, str((double)nextLocLabNum)); } localLabelNames[step] = nextLocLabNum; nextLocLabNum++; /* Prepare for next local label */ } } } /* Next step */ /* Print the step */ let(&tmpStr, g_Statement[targetHyps[detailStep - 1]].labelName); let(&tmpStr1, ""); /* Local label declaration */ stmt = proof[detailStep - 1]; if (stmt < 0) { if (stmt <= -1000) { stmt = -1000 - stmt; /* stmt is now the step number a local label refers to */ let(&tmpStr, cat(tmpStr,"=", str((double)(localLabelNames[stmt])), NULL)); type = g_Statement[proof[stmt]].type; } else { if (stmt != -(long)'?') bug(207); let(&tmpStr, cat(tmpStr,"=",chr(-stmt), NULL)); /* '?' */ type = '?'; } } else { if (nmbrElementIn(1, localLabels, detailStep - 1)) { /* This statement declares a local label */ let(&tmpStr1, cat(str((double)(localLabelNames[detailStep - 1])), ":", NULL)); } let(&tmpStr, cat(tmpStr, "=", g_Statement[stmt].labelName, NULL)); type = g_Statement[stmt].type; } /* Print the proof line */ printLongLine(cat("Proof step ", str((double)detailStep), ": ", tmpStr1, tmpStr, " $", chr(type), " ", nmbrCvtMToVString(g_WrkProof.mathStringPtrs[detailStep - 1]), NULL), " ", " "); /* Print details about the step */ let(&tmpStr, cat("This step assigns ", NULL)); let(&tmpStr1, ""); stmt = proof[detailStep - 1]; sourceStmt = stmt; if (stmt < 0) { if (stmt <= -1000) { stmt = -1000 - stmt; /* stmt is now the step number a local label refers to */ let(&tmpStr, cat(tmpStr, "step ", str((double)stmt), " (via local label reference \"", str((double)(localLabelNames[stmt])), "\") to ", NULL)); } else { if (stmt != -(long)'?') bug(208); let(&tmpStr, cat(tmpStr, "an unknown statement to ", NULL)); } } else { let(&tmpStr, cat(tmpStr, "source \"", g_Statement[stmt].labelName, "\" ($", chr(g_Statement[stmt].type), ") to ", NULL)); if (nmbrElementIn(1, localLabels, detailStep - 1)) { /* This statement declares a local label */ let(&tmpStr1, cat(" This step also declares the local label ", str((double)(localLabelNames[detailStep - 1])), ", which is used later on.", NULL)); } } targetStmt = targetHyps[detailStep - 1]; if (detailStep == plen) { let(&tmpStr, cat(tmpStr, "the final assertion being proved.", NULL)); } else { let(&tmpStr, cat(tmpStr, "target \"", g_Statement[targetStmt].labelName, "\" ($", chr(g_Statement[targetStmt].type), ").", NULL)); } let(&tmpStr, cat(tmpStr, tmpStr1, NULL)); if (sourceStmt >= 0) { if (g_Statement[sourceStmt].type == a_ || g_Statement[sourceStmt].type == p_) { j = nmbrLen(g_Statement[sourceStmt].reqHypList); if (j != nmbrLen(getStep.sourceHyps)) bug(209); if (!j) { let(&tmpStr, cat(tmpStr, " The source assertion requires no hypotheses.", NULL)); } else { if (j == 1) { let(&tmpStr, cat(tmpStr, " The source assertion requires the hypothesis ", NULL)); } else { let(&tmpStr, cat(tmpStr, " The source assertion requires the hypotheses ", NULL)); } for (i = 0; i < j; i++) { let(&tmpStr, cat(tmpStr, "\"", g_Statement[g_Statement[sourceStmt].reqHypList[i]].labelName, "\" ($", chr(g_Statement[g_Statement[sourceStmt].reqHypList[i]].type), ", step ", str((double)(getStep.sourceHyps[i] + 1)), ")", NULL)); if (i == 0 && j == 2) { let(&tmpStr, cat(tmpStr, " and ", NULL)); } if (i < j - 2 && j > 2) { let(&tmpStr, cat(tmpStr, ", ", NULL)); } if (i == j - 2 && j > 2) { let(&tmpStr, cat(tmpStr, ", and ", NULL)); } } let(&tmpStr, cat(tmpStr, ".", NULL)); } } } if (detailStep < plen) { let(&tmpStr, cat(tmpStr, " The parent assertion of the target hypothesis is \"", g_Statement[getStep.targetParentStmt].labelName, "\" ($", chr(g_Statement[getStep.targetParentStmt].type),", step ", str((double)(getStep.targetParentStep)), ").", NULL)); } else { let(&tmpStr, cat(tmpStr, " The target has no parent because it is the assertion being proved.", NULL)); } printLongLine(tmpStr, "", " "); if (sourceStmt >= 0) { if (g_Statement[sourceStmt].type == a_ || g_Statement[sourceStmt].type == p_) { print2("The source assertion before substitution was:\n"); printLongLine(cat(" ", g_Statement[sourceStmt].labelName, " $", chr(g_Statement[sourceStmt].type), " ", nmbrCvtMToVString( g_Statement[sourceStmt].mathString), NULL), " ", " "); j = nmbrLen(getStep.sourceSubstsNmbr); if (j == 1) { printLongLine(cat( "The following substitution was made to the source assertion:", NULL),""," "); } else { printLongLine(cat( "The following substitutions were made to the source assertion:", NULL),""," "); } if (!j) { print2(" (None)\n"); } else { print2(" Variable Substituted with\n"); for (i = 0; i < j; i++) { printLongLine(cat(" ", g_MathToken[getStep.sourceSubstsNmbr[i]].tokenName," ", space(9 - (long)strlen( g_MathToken[getStep.sourceSubstsNmbr[i]].tokenName)), nmbrCvtMToVString(getStep.sourceSubstsPntr[i]), NULL), " ", " "); } } } } if (detailStep < plen) { print2("The target hypothesis before substitution was:\n"); printLongLine(cat(" ", g_Statement[targetStmt].labelName, " $", chr(g_Statement[targetStmt].type), " ", nmbrCvtMToVString( g_Statement[targetStmt].mathString), NULL), " ", " "); j = nmbrLen(getStep.targetSubstsNmbr); if (j == 1) { printLongLine(cat( "The following substitution was made to the target hypothesis:", NULL),""," "); } else { printLongLine(cat( "The following substitutions were made to the target hypothesis:", NULL),""," "); } if (!j) { print2(" (None)\n"); } else { print2(" Variable Substituted with\n"); for (i = 0; i < j; i++) { printLongLine(cat(" ", g_MathToken[getStep.targetSubstsNmbr[i]].tokenName, " ", space(9 - (long)strlen( g_MathToken[getStep.targetSubstsNmbr[i]].tokenName)), nmbrCvtMToVString(getStep.targetSubstsPntr[i]), NULL), " ", " "); } } } cleanWrkProof(); getStep.stepNum = 0; /* Zero is flag for verifyProof to ignore getStep info */ /* Deallocate getStep contents */ j = pntrLen(getStep.sourceSubstsPntr); for (i = 0; i < j; i++) { nmbrLet((nmbrString **)(&getStep.sourceSubstsPntr[i]), NULL_NMBRSTRING); } j = pntrLen(getStep.targetSubstsPntr); for (i = 0; i < j; i++) { nmbrLet((nmbrString **)(&getStep.targetSubstsPntr[i]), NULL_NMBRSTRING); } nmbrLet(&getStep.sourceHyps, NULL_NMBRSTRING); pntrLet(&getStep.sourceSubstsPntr, NULL_PNTRSTRING); nmbrLet(&getStep.sourceSubstsNmbr, NULL_NMBRSTRING); pntrLet(&getStep.targetSubstsPntr, NULL_PNTRSTRING); nmbrLet(&getStep.targetSubstsNmbr, NULL_NMBRSTRING); /* Deallocate other strings */ let(&tmpStr, ""); let(&tmpStr1, ""); nmbrLet(&localLabels, NULL_NMBRSTRING); nmbrLet(&localLabelNames, NULL_NMBRSTRING); nmbrLet(&proof, NULL_NMBRSTRING); nmbrLet(&targetHyps, NULL_NMBRSTRING); } /* showDetailStep */ /* Summary of statements in proof for SHOW PROOF / STATEMENT_SUMMARY */ void proofStmtSumm(long statemNum, flag essentialFlag, flag texFlag) { long i, j, k, pos, stmt, plen, slen, step; char type; vstring statementUsedFlags = ""; /* 'Y'/'N' flag that statement is used */ vstring str1 = ""; vstring str2 = ""; vstring str3 = ""; nmbrString *statementList = NULL_NMBRSTRING; nmbrString *proof = NULL_NMBRSTRING; nmbrString *essentialFlags = NULL_NMBRSTRING; /* 10/10/02 This section is never called in HTML mode anymore. The code is left in though just in case we somehow get here and the user continues through the bug. */ if (texFlag && g_htmlFlag) bug(239); if (!texFlag) { print2("Summary of statements used in the proof of \"%s\":\n", g_Statement[statemNum].labelName); } else { g_outputToString = 1; /* Flag for print2 to add to g_printString */ if (!g_htmlFlag) { print2("\n"); print2("\\vspace{1ex} %%3\n"); printLongLine(cat("Summary of statements used in the proof of ", "{\\tt ", asciiToTt(g_Statement[statemNum].labelName), "}:", NULL), "", " "); } else { printLongLine(cat("Summary of statements used in the proof of ", "", asciiToTt(g_Statement[statemNum].labelName), ":", NULL), "", "\""); } g_outputToString = 0; fprintf(g_texFilePtr, "%s", g_printString); let(&g_printString, ""); } if (g_Statement[statemNum].type != p_) { print2(" This is not a provable ($p) statement.\n"); return; } /* 20-Oct-2013 nm Don't use bad proofs (incomplete proofs are ok) */ if (parseProof(statemNum) > 1) { /* The proof has an error, so use the empty proof */ nmbrLet(&proof, nmbrAddElement(NULL_NMBRSTRING, -(long)'?')); } else { nmbrLet(&proof, g_WrkProof.proofString); } plen = nmbrLen(proof); /* Get the essential step flags, if required */ if (essentialFlag) { nmbrLet(&essentialFlags, nmbrGetEssential(proof)); } for (step = 0; step < plen; step++) { if (essentialFlag) { if (!essentialFlags[step]) continue; /* Ignore floating hypotheses */ } stmt = proof[step]; if (stmt < 0) { continue; /* Ignore '?' and local labels */ } if (1) { /* Limit list to $a and $p only */ if (g_Statement[stmt].type != a_ && g_Statement[stmt].type != p_) { continue; } } /* Add this statement to the statement list if not already in it */ if (!nmbrElementIn(1, statementList, stmt)) { nmbrLet(&statementList, nmbrAddElement(statementList, stmt)); } } /* Next step */ /* Prepare the output */ /* First, fill in the statementUsedFlags char array. This allows us to sort the output by statement number without calling a sort routine. */ slen = nmbrLen(statementList); let(&statementUsedFlags, string(g_statements + 1, 'N')); /* Init. to 'no' */ for (pos = 0; pos < slen; pos++) { stmt = statementList[pos]; if (stmt > statemNum || stmt < 1) bug(210); statementUsedFlags[stmt] = 'Y'; } /* Next, build the output string */ for (stmt = 1; stmt < statemNum; stmt++) { if (statementUsedFlags[stmt] == 'Y') { assignStmtFileAndLineNum(stmt); /* 9-Jan-2018 nm */ let(&str1, cat(" is located on line ", str((double)(g_Statement[stmt].lineNum)), " of the file ", NULL)); if (!texFlag) { print2("\n"); printLongLine(cat("Statement ", g_Statement[stmt].labelName, str1, "\"", g_Statement[stmt].fileName, "\".",NULL), "", " "); } else { g_outputToString = 1; /* Flag for print2 to add to g_printString */ if (!g_htmlFlag) { print2("\n"); print2("\n"); print2("\\vspace{1ex} %%4\n"); printLongLine(cat("Statement {\\tt ", asciiToTt(g_Statement[stmt].labelName), "} ", str1, "{\\tt ", asciiToTt(g_Statement[stmt].fileName), "}.", NULL), "", " "); print2("\n"); } else { printLongLine(cat("Statement ", asciiToTt(g_Statement[stmt].labelName), " ", str1, " ", asciiToTt(g_Statement[stmt].fileName), " ", NULL), "", "\""); } g_outputToString = 0; fprintf(g_texFilePtr, "%s", g_printString); let(&g_printString, ""); } /* type = g_Statement[stmt].type; */ /* 18-Sep-2013 Not used */ let(&str1, ""); str1 = getDescription(stmt); if (str1[0]) { if (!texFlag) { printLongLine(cat("\"", str1, "\"", NULL), "", " "); } else { /* printTexComment(str1, 1); */ /* 17-Nov-2015 nm Added 3rd & 4th arguments */ printTexComment(str1, /* Sends result to g_texFilePtr */ 1, /* 1 = htmlCenterFlag */ PROCESS_EVERYTHING, /* actionBits */ /* 13-Dec-2018 nm */ 0 /* 1 = noFileCheck */); } } /* print2("Its mandatory hypotheses in RPN order are:\n"); */ j = nmbrLen(g_Statement[stmt].reqHypList); for (i = 0; i < j; i++) { k = g_Statement[stmt].reqHypList[i]; if (!essentialFlag || g_Statement[k].type != f_) { let(&str2, cat(" ",g_Statement[k].labelName, " $", chr(g_Statement[k].type), " ", NULL)); if (!texFlag) { printLongLine(cat(str2, nmbrCvtMToVString(g_Statement[k].mathString), " $.", NULL), " "," "); } else { let(&str3, space((long)strlen(str2))); printTexLongMath(g_Statement[k].mathString, str2, str3, 0, 0); } } } let(&str1, ""); type = g_Statement[stmt].type; if (type == p_) let(&str1, " $= ..."); let(&str2, cat(" ", g_Statement[stmt].labelName, " $",chr(type), " ", NULL)); if (!texFlag) { printLongLine(cat(str2, nmbrCvtMToVString(g_Statement[stmt].mathString), str1, " $.", NULL), " ", " "); } else { let(&str3, space((long)strlen(str2))); printTexLongMath(g_Statement[stmt].mathString, str2, str3, 0, 0); } } /* End if (statementUsedFlag[stmt] == 'Y') */ } /* Next stmt */ let(&statementUsedFlags, ""); /* 'Y'/'N' flag that statement is used */ let(&str1, ""); let(&str2, ""); let(&str3, ""); nmbrLet(&statementList, NULL_NMBRSTRING); nmbrLet(&proof, NULL_NMBRSTRING); nmbrLet(&essentialFlags, NULL_NMBRSTRING); } /* proofStmtSumm */ /* Traces back the statements used by a proof, recursively. */ /* Returns 1 if at least one label is printed (or would be printed in case testOnlyFlag=1); otherwise, returns 0 */ /* matchList suppresses all output except labels matching matchList */ /* testOnlyFlag prevents any printout; it is used to determine whether there is an unwanted axiom for MINIMIZE_WITH /FORBID. */ /* void traceProof(long statemNum, */ /* before 20-May-2013 */ flag traceProof(long statemNum, /* 20-May-2013 nm */ flag essentialFlag, flag axiomFlag, vstring matchList, /* 19-May-2013 nm */ vstring traceToList, /* 18-Jul-2015 nm */ flag testOnlyFlag /* 20-May-2013 nm */) { long stmt, pos; vstring statementUsedFlags = ""; /* y/n flags that statement is used */ vstring outputString = ""; nmbrString *unprovedList = NULL_NMBRSTRING; flag foundFlag = 0; /* Make sure we're calling this with $p statements only */ if (g_Statement[statemNum].type != (char)p_) bug(249); if (!testOnlyFlag) { /* 20-May-2013 nm */ if (axiomFlag) { print2( "Statement \"%s\" assumes the following axioms ($a statements):\n", g_Statement[statemNum].labelName); } else if (traceToList[0] == 0) { print2( "The proof of statement \"%s\" uses the following earlier statements:\n", g_Statement[statemNum].labelName); } else { print2( "The proof of statement \"%s\" traces back to \"%s\" via:\n", g_Statement[statemNum].labelName, traceToList); } } traceProofWork(statemNum, essentialFlag, traceToList, /* /TO argument of SHOW TRACE_BACK */ /* 18-Jul-2015 nm */ &statementUsedFlags, &unprovedList); if ((signed)(strlen(statementUsedFlags)) != g_statements + 1) bug(226); /* Build the output string */ let(&outputString, ""); for (stmt = 1; stmt < statemNum; stmt++) { if (statementUsedFlags[stmt] == 'Y') { /* 19-May-2013 nm - Added MATCH qualifier */ if (matchList[0]) { /* There is a list to match */ /* Don't include unmatched labels */ if (!matchesList(g_Statement[stmt].labelName, matchList, '*', '?')) continue; } /* 20-May-2013 nm Skip rest of scan in testOnlyFlag mode */ foundFlag = 1; /* At least one label would be printed */ if (testOnlyFlag) { goto TRACE_RETURN; } if (axiomFlag) { if (g_Statement[stmt].type == a_) { let(&outputString, cat(outputString, " ", g_Statement[stmt].labelName, NULL)); } } else { let(&outputString, cat(outputString, " ", g_Statement[stmt].labelName, NULL)); switch (g_Statement[stmt].type) { case a_: let(&outputString, cat(outputString, "($a)", NULL)); break; case e_: let(&outputString, cat(outputString, "($e)", NULL)); break; case f_: let(&outputString, cat(outputString, "($f)", NULL)); break; } } } /* End if (statementUsedFlag[stmt] == 'Y') */ } /* Next stmt */ /* 20-May-2013 nm Skip printing in testOnlyFlag mode */ if (testOnlyFlag) { goto TRACE_RETURN; } if (outputString[0]) { let(&outputString, cat(" ", outputString, NULL)); } else { let(&outputString, " (None)"); } /* Print the output */ printLongLine(outputString, " ", " "); /* Print any unproved statements */ if (nmbrLen(unprovedList)) { print2("Warning: The following traced statement(s) were not proved:\n"); let(&outputString, ""); for (pos = 0; pos < nmbrLen(unprovedList); pos++) { let(&outputString, cat(outputString, " ", g_Statement[unprovedList[ pos]].labelName, NULL)); } let(&outputString, cat(" ", outputString, NULL)); printLongLine(outputString, " ", " "); } TRACE_RETURN: /* Deallocate */ let(&outputString, ""); let(&statementUsedFlags, ""); nmbrLet(&unprovedList, NULL_NMBRSTRING); return foundFlag; } /* traceProof */ /* Traces back the statements used by a proof, recursively. Returns a nmbrString with a list of statements and unproved statements */ void traceProofWork(long statemNum, flag essentialFlag, vstring traceToList, /* /TO argument of SHOW TRACE_BACK */ /* 18-Jul-2015 nm */ vstring *statementUsedFlagsP, /* 'Y'/'N' flag that statement is used */ nmbrString **unprovedListP) { long pos, stmt, plen, slen, step; nmbrString *statementList = NULL_NMBRSTRING; nmbrString *proof = NULL_NMBRSTRING; nmbrString *essentialFlags = NULL_NMBRSTRING; vstring traceToFilter = ""; /* 18-Jul-2015 nm */ vstring str1 = ""; /* 18-Jul-2015 nm */ long j; /* 18-Jul-2015 nm */ /* 18-Jul-2015 nm */ /* Preprocess the "SHOW TRACE_BACK ... / TO" traceToList list if any */ if (traceToList[0] != 0) { let(&traceToFilter, string(g_statements + 1, 'N')); /* Init. to 'no' */ /* Wildcard match scan */ for (stmt = 1; stmt <= g_statements; stmt++) { if (g_Statement[stmt].type != (char)a_ && g_Statement[stmt].type != (char)p_) continue; /* Not a $a or $p statement; skip it */ /* Wildcard matching */ if (!matchesList(g_Statement[stmt].labelName, traceToList, '*', '?')) continue; let(&str1, ""); str1 = traceUsage(stmt /*g_showStatement*/, 1, /*recursiveFlag*/ statemNum /* cutoffStmt */); traceToFilter[stmt] = 'Y'; /* Include the statement we're showing usage of */ if (str1[0] == 'Y') { /* There is some usage */ for (j = stmt + 1; j <= g_statements; j++) { /* OR in the usage to the filter */ if (str1[j] == 'Y') traceToFilter[j] = 'Y'; } } } /* Next i (statement number) */ } /* if (traceToList[0] != 0) */ nmbrLet(&statementList, nmbrSpace(g_statements)); statementList[0] = statemNum; slen = 1; nmbrLet(&(*unprovedListP), NULL_NMBRSTRING); /* List of unproved statements */ let(&(*statementUsedFlagsP), string(g_statements + 1, 'N')); /* Init. to 'no' */ (*statementUsedFlagsP)[statemNum] = 'Y'; /* nm 22-Nov-2014 */ for (pos = 0; pos < slen; pos++) { if (g_Statement[statementList[pos]].type != p_) { continue; /* Not a $p */ } /* 20-Oct-2013 nm Don't use bad proofs (incomplete proofs are ok) */ if (parseProof(statementList[pos]) > 1) { /* The proof has an error, so use the empty proof */ nmbrLet(&proof, nmbrAddElement(NULL_NMBRSTRING, -(long)'?')); } else { nmbrLet(&proof, g_WrkProof.proofString); } plen = nmbrLen(proof); /* Get the essential step flags, if required */ if (essentialFlag) { nmbrLet(&essentialFlags, nmbrGetEssential(proof)); } for (step = 0; step < plen; step++) { if (essentialFlag) { if (!essentialFlags[step]) continue; /* Ignore floating hypotheses */ } stmt = proof[step]; if (stmt < 0) { if (stmt > -1000) { /* '?' */ if (!nmbrElementIn(1, *unprovedListP, statementList[pos])) { nmbrLet(&(*unprovedListP), nmbrAddElement(*unprovedListP, statementList[pos])); /* Add to list of unproved statements */ } } continue; /* Ignore '?' and local labels */ } if (1) { /* Limit list to $a and $p only */ if (g_Statement[stmt].type != a_ && g_Statement[stmt].type != p_) { continue; } } /* Add this statement to the statement list if not already in it */ if ((*statementUsedFlagsP)[stmt] == 'N') { /*(*statementUsedFlagsP)[stmt] = 'Y';*/ /* 18-Jul-2015 deleted */ /* 18-Jul-2015 nm */ if (traceToList[0] == 0) { statementList[slen] = stmt; slen++; (*statementUsedFlagsP)[stmt] = 'Y'; } else { /* TRACE_BACK / TO */ if (traceToFilter[stmt] == 'Y') { statementList[slen] = stmt; slen++; (*statementUsedFlagsP)[stmt] = 'Y'; } } } } /* Next step */ } /* Next pos */ /* Deallocate */ nmbrLet(&essentialFlags, NULL_NMBRSTRING); nmbrLet(&proof, NULL_NMBRSTRING); nmbrLet(&statementList, NULL_NMBRSTRING); let(&str1, ""); let(&str1, ""); return; } /* traceProofWork */ nmbrString *stmtFoundList = NULL_NMBRSTRING; long indentShift = 0; /* Traces back the statements used by a proof, recursively, with tree display.*/ void traceProofTree(long statemNum, flag essentialFlag, long endIndent) { if (g_Statement[statemNum].type != p_) { print2("Statement %s is not a $p statement.\n", g_Statement[statemNum].labelName); return; } printLongLine(cat("The proof tree traceback for statement \"", g_Statement[statemNum].labelName, "\" follows. The statements used by each proof are indented one level in,", " below the statement being proved. Hypotheses are not included.", NULL), "", " "); print2("\n"); nmbrLet(&stmtFoundList, NULL_NMBRSTRING); indentShift = 0; traceProofTreeRec(statemNum, essentialFlag, endIndent, 0); nmbrLet(&stmtFoundList, NULL_NMBRSTRING); } /* traceProofTree */ void traceProofTreeRec(long statemNum, flag essentialFlag, long endIndent, long recursDepth) { long i, pos, stmt, plen, slen, step; vstring outputStr = ""; nmbrString *localFoundList = NULL_NMBRSTRING; nmbrString *localPrintedList = NULL_NMBRSTRING; flag unprovedFlag = 0; nmbrString *proof = NULL_NMBRSTRING; nmbrString *essentialFlags = NULL_NMBRSTRING; let(&outputStr, ""); outputStr = getDescription(statemNum); /* Get statement comment */ let(&outputStr, edit(outputStr, 8 + 16 + 128)); /* Trim and reduce spaces */ slen = len(outputStr); for (i = 0; i < slen; i++) { /* Change newlines to spaces in comment */ if (outputStr[i] == '\n') { outputStr[i] = ' '; } } #define INDENT_INCR 3 #define MAX_LINE_LEN 79 if ((recursDepth * INDENT_INCR - indentShift) > (g_screenWidth - MAX_LINE_LEN) + 50) { indentShift = indentShift + 40 + (g_screenWidth - MAX_LINE_LEN); print2("****** Shifting indentation. Total shift is now %ld.\n", (long)indentShift); } if ((recursDepth * INDENT_INCR - indentShift) < 1 && indentShift != 0) { indentShift = indentShift - 40 - (g_screenWidth - MAX_LINE_LEN); print2("****** Shifting indentation. Total shift is now %ld.\n", (long)indentShift); } let(&outputStr, cat(space(recursDepth * INDENT_INCR - indentShift), g_Statement[statemNum].labelName, " $", chr(g_Statement[statemNum].type), " \"", edit(outputStr, 8 + 128), "\"", NULL)); if (len(outputStr) > MAX_LINE_LEN + (g_screenWidth - MAX_LINE_LEN)) { let(&outputStr, cat(left(outputStr, MAX_LINE_LEN + (g_screenWidth - MAX_LINE_LEN) - 3), "...", NULL)); } if (g_Statement[statemNum].type == p_ || g_Statement[statemNum].type == a_) { /* Only print assertions to reduce output bulk */ print2("%s\n", outputStr); } if (g_Statement[statemNum].type != p_) { let(&outputStr, ""); return; } if (endIndent) { /* An indentation level limit is set */ if (endIndent < recursDepth + 2) { let(&outputStr, ""); return; } } /* 20-Oct-2013 nm Don't use bad proofs (incomplete proofs are ok) */ if (parseProof(statemNum) > 1) { /* The proof has an error, so use the empty proof */ nmbrLet(&proof, nmbrAddElement(NULL_NMBRSTRING, -(long)'?')); } else { nmbrLet(&proof, g_WrkProof.proofString); } plen = nmbrLen(proof); /* Get the essential step flags, if required */ if (essentialFlag) { nmbrLet(&essentialFlags, nmbrGetEssential(proof)); } nmbrLet(&localFoundList, NULL_NMBRSTRING); nmbrLet(&localPrintedList, NULL_NMBRSTRING); for (step = 0; step < plen; step++) { if (essentialFlag) { if (!essentialFlags[step]) continue; /* Ignore floating hypotheses */ } stmt = proof[step]; if (stmt < 0) { if (stmt > -1000) { /* '?' */ unprovedFlag = 1; } continue; /* Ignore '?' and local labels */ } if (!nmbrElementIn(1, localFoundList, stmt)) { nmbrLet(&localFoundList, nmbrAddElement(localFoundList, stmt)); } if (!nmbrElementIn(1, stmtFoundList, stmt)) { traceProofTreeRec(stmt, essentialFlag, endIndent, recursDepth + 1); nmbrLet(&localPrintedList, nmbrAddElement(localPrintedList, stmt)); nmbrLet(&stmtFoundList, nmbrAddElement(stmtFoundList, stmt)); } } /* Next step */ /* See if there are any old statements printed previously */ slen = nmbrLen(localFoundList); let(&outputStr, ""); for (pos = 0; pos < slen; pos++) { stmt = localFoundList[pos]; if (!nmbrElementIn(1, localPrintedList, stmt)) { /* Don't include $f, $e in output */ if (g_Statement[stmt].type == p_ || g_Statement[stmt].type == a_) { let(&outputStr, cat(outputStr, " ", g_Statement[stmt].labelName, NULL)); } } } if (len(outputStr)) { printLongLine(cat(space(INDENT_INCR * (recursDepth + 1) - 1 - indentShift), outputStr, " (shown above)", NULL), space(INDENT_INCR * (recursDepth + 2) - indentShift), " "); } if (unprovedFlag) { printLongLine(cat(space(INDENT_INCR * (recursDepth + 1) - indentShift), "*** Statement ", g_Statement[statemNum].labelName, " has not been proved." , NULL), space(INDENT_INCR * (recursDepth + 2)), " "); } let(&outputStr, ""); nmbrLet(&localFoundList, NULL_NMBRSTRING); nmbrLet(&localPrintedList, NULL_NMBRSTRING); nmbrLet(&proof, NULL_NMBRSTRING); nmbrLet(&essentialFlags, NULL_NMBRSTRING); } /* traceProofTreeRec */ /* Called by SHOW TRACE_BACK
", "Colors of variables: ", g_htmlVarColor, "
Syntax hints: "); } /* 10/6/99 - Get the main symbol in the syntax */ /* This section can be deleted if not wanted - it is custom for set.mm and might not work with other .mm's */ let(&tmpStr1, ""); for (i = 1 /* Skip |- */; i < g_Statement[stmt].mathStringLen; i++) { if (g_MathToken[(g_Statement[stmt].mathString)[i]].tokenType == (char)con_) { /* Skip parentheses, commas, etc. */ if (strcmp(g_MathToken[(g_Statement[stmt].mathString)[i] ].tokenName, "(") && strcmp(g_MathToken[(g_Statement[stmt].mathString)[i] ].tokenName, ",") && strcmp(g_MathToken[(g_Statement[stmt].mathString)[i] ].tokenName, ")") && strcmp(g_MathToken[(g_Statement[stmt].mathString)[i] ].tokenName, ":") /* 14-Oct-2019 nm Use |-> rather than e. for cmpt, cmpt2 */ && !(!strcmp(g_MathToken[(g_Statement[stmt].mathString)[i] ].tokenName, "e.") && (!strcmp(g_Statement[stmt].labelName, "cmpt") || !strcmp(g_Statement[stmt].labelName, "cmpt2"))) ) { tmpStr1 = tokenToTex(g_MathToken[(g_Statement[stmt].mathString)[i] ].tokenName, stmt); /* 14-Jan-2016 nm */ let(&tmpStr1, cat( (g_altHtmlFlag ? cat("", NULL) : ""), /* 14-Jan-2016 nm */ tmpStr1, (g_altHtmlFlag ? "" : ""), NULL)); break; } } } /* Next i */ /* Special cases hard-coded for set.mm */ if (!strcmp(g_Statement[stmt].labelName, "wbr")) /* binary relation */ let(&tmpStr1, " class class class "); if (!strcmp(g_Statement[stmt].labelName, "cv")) let(&tmpStr1, "[set variable]"); /* 10/10/02 Let's don't do cv - confusing to reader */ if (!strcmp(g_Statement[stmt].labelName, "cv")) continue; if (!strcmp(g_Statement[stmt].labelName, "co")) /* operation */ let(&tmpStr1, "(class class class)"); let(&tmpStr, cat(tmpStr, "  ", tmpStr1, NULL)); /* End of 10/6/99 section - Get the main symbol in the syntax */ let(&tmpStr1, ""); tmpStr1 = pinkHTML(stmt); /******* 10/10/02 let(&tmpStr, cat(tmpStr, "", g_Statement[stmt].labelName, "   ", NULL)); *******/ let(&tmpStr, cat(tmpStr, "", g_Statement[stmt].labelName, "", tmpStr1, NULL)); } } if (tmpStr[0]) { let(&tmpStr, cat(tmpStr, "
This theorem was proved from axioms:"); } let(&tmpStr1, ""); tmpStr1 = pinkHTML(stmt); let(&tmpStr, cat(tmpStr, "  ", g_Statement[stmt].labelName, "", tmpStr1, NULL)); } } } /* next stmt */ if (tmpStr[0]) { let(&tmpStr, cat(tmpStr, "
This theorem depends on definitions:"); } let(&tmpStr1, ""); tmpStr1 = pinkHTML(stmt); let(&tmpStr, cat(tmpStr, "  ", g_Statement[stmt].labelName, "", tmpStr1, NULL)); } } } /* next stmt */ if (tmpStr[0]) { let(&tmpStr, cat(tmpStr, "
 ", "WARNING: This theorem has an incomplete proof.
 ", "WARNING: This proof depends on the following unproved theorem(s): ", NULL), "", "\""); let(&tmpStr, ""); for (i = 0; i < nmbrLen(unprovedList); i++) { let(&tmpStr, cat(tmpStr, " ", g_Statement[unprovedList[i]].labelName, "", NULL)); } printLongLine(cat(tmpStr, "