/*****************************************************************************/ /* Copyright (C) 2006 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 texFileName */ #include "mmcmds.h" #include "mminou.h" #include "mmpars.h" #include "mmveri.h" #include "mmwtex.h" /* For htmlVarColors,... */ #include "mmpfas.h" /* vstring mainFileName = ""; */ /* 28-Dec-05 nm Obsolete */ flag printHelp = 0; /* For HTML output */ vstring printStringForReferencedBy = ""; /* For MIDI */ flag midiFlag = 0; vstring midiParam = ""; /* Type (i.e. print) a statement */ void typeStatement(long showStatement, flag briefFlag, flag commentOnlyFlag, flag texFlag, flag htmlFlag) { /* 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 htmlFlag=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 htmlFlag=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 */ 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 (!showStatement) bug(225); /* Must be 1 or greater */ if (!commentOnlyFlag && !briefFlag) { let(&str1, cat("Statement ", str(showStatement), " is located on line ", str(statement[showStatement].lineNum), " of the file ", NULL)); if (!texFlag) { printLongLine(cat(str1, "\"", statement[showStatement].fileName, "\".", /* 8-Feb-2007 nm Added HTML page info to SHOW STATEMENT ... /FULL */ (statement[showStatement].pinkNumber == 0) ? /* !=0 means $a or $p */ "" : cat(" Its statement number for HTML pages is ", str(statement[showStatement].pinkNumber), ".", NULL), NULL), "", " "); } else { if (!htmlFlag) let(&printString, ""); outputToString = 1; /* Flag for print2 to add to printString */ /* Note that printTexLongMathString resets it */ if (!(htmlFlag && texFlag)) { /* printLongLine(cat(str1, "{\\tt ", asciiToTt(statement[showStatement].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 (statement[showStatement].type == (char)p__) { subType = THEOREM; } else { /* Must be a__ due to filter in main() */ if (statement[showStatement].type != (char)a__) bug(228); if (strcmp("|-", mathToken[ (statement[showStatement].mathString)[0]].tokenName)) { subType = SYNTAX; } else { if (!strcmp("ax-", left(statement[showStatement].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(showStatement); printLongLine(cat("
", str1, " ", statement[showStatement].labelName, "", str2, "
", NULL), "", "\""); } /* (htmlFlag && texFlag) */ outputToString = 0; } /* texFlag */ } if (!briefFlag || commentOnlyFlag) { let(&str1, ""); str1 = getDescription(showStatement); if (!str1[0] /* No comment */ || (str1[0] == '[' && str1[strlen(str1) - 1] == ']') /* 7-Sep-04 Allow both "$([])$" and "$( [] )$" */ || (str1[1] == '[' && str1[strlen(str1) - 2] == ']')) { /* Date stamp from previous proof */ print2("?Warning: Statement \"%s\" has no comment\n", statement[showStatement].labelName); /*if (str1[0]) {*/ /*old*/ } else { 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 (htmlFlag && texFlag) { let(&str1, cat("
Description: ", str1, "

", NULL)); } *******/ if (!htmlFlag) { /* LaTeX */ /* 6-Dec-03 Add separation space between theorems */ let(&str1, cat("\n\\vspace{1ex}\n\n", str1, NULL)); } printTexComment(str1, 1); } } } if (commentOnlyFlag && !briefFlag) goto returnPoint; if ((briefFlag && !texFlag) || (htmlFlag && 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 (htmlFlag && 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 = statement[showStatement].reqDisjVarsA; nmbrTmpPtr2 = statement[showStatement].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 (!(htmlFlag && 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 (!(htmlFlag && 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; } } /* 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 (!(htmlFlag && texFlag)) { let(&str1, cat(str1, " ", mathToken[nmbrTmpPtr1[k]].tokenName, NULL)); } else { /* 12/23/01 */ if (htmlDistinctVarsCommaFlag) { let(&htmlDistinctVars, cat(htmlDistinctVars, ",", NULL)); } htmlDistinctVarsCommaFlag = 1; let(&str2, ""); str2 = tokenToTex(mathToken[nmbrTmpPtr1[k]].tokenName); /* 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 (!(htmlFlag && texFlag)) { let(&str1, cat(str1, " ", mathToken[nmbrTmpPtr2[k]].tokenName, NULL)); } else { /* 12/23/01 */ if (htmlDistinctVarsCommaFlag) { let(&htmlDistinctVars, cat(htmlDistinctVars, ",", NULL)); } htmlDistinctVarsCommaFlag = 1; let(&str2, ""); str2 = tokenToTex(mathToken[nmbrTmpPtr2[k]].tokenName); /* 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 (!(htmlFlag && 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 && htmlFlag)*/) { /* 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(statement[showStatement].reqHypList); k = 0; for (i = 0; i < j; i++) { /* Count the number of essential hypotheses */ if (statement[statement[showStatement].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 && htmlFlag)) { if (statement[statement[showStatement].reqHypList[i]].type == (char)f__) k++; } } if (k) { if (texFlag) { outputToString = 1; } if (texFlag && htmlFlag) { print2("
\n", (k == 1) ? "Hypothesis" : "Hypotheses"); print2("\n", (k == 1) ? "Hypothesis" : "Hypotheses"); print2("\n"); } for (i = 0; i < j; i++) { k = statement[showStatement].reqHypList[i]; if (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 && htmlFlag) && statement[k].type == (char)f__) ) continue; if (!texFlag) { let(&str2, cat(str(k), " ", NULL)); } else { let(&str2, " "); } let(&str2, cat(str2, statement[k].labelName, " $", chr(statement[k].type), " ", NULL)); if (!texFlag) { printLongLine(cat(str2, nmbrCvtMToVString(statement[k].mathString), " $.", NULL), " "," "); } else { if (!(htmlFlag && texFlag)) { let(&str3, space(strlen(str2))); printTexLongMath(statement[k].mathString, str2, str3, 0, 0); } else { outputToString = 1; print2("
%s
Ref\n"); print2("Expression
%s\n", statement[k].labelName); /* Print hypothesis */ printTexLongMath(statement[k].mathString, "", "", 0, 0); } } } /* next i */ if (texFlag && htmlFlag) { outputToString = 1; print2("
\n"); } } /* if k (#essential hyp) */ } let(&str1, ""); type = statement[showStatement].type; if (type == p__) let(&str1, " $= ..."); if (!texFlag) let(&str2, cat(str(showStatement), " ", NULL)); else let(&str2, " "); let(&str2, cat(str2, statement[showStatement].labelName, " $",chr(type), " ", NULL)); if (!texFlag) { printLongLine(cat(str2, nmbrCvtMToVString(statement[showStatement].mathString), str1, " $.", NULL), " ", " "); } else { if (!(htmlFlag && texFlag)) { let(&str3, space(strlen(str2))); /* 3rd argument of printTexLongMath cannot be temp allocated */ printTexLongMath(statement[showStatement].mathString, str2, str3, 0, 0); } else { outputToString = 1; print2("
\n"); print2("\n"); print2("\n"); printLongLine(cat( "
Assertion
Ref\n"); print2("Expression
", statement[showStatement].labelName, "", NULL), " ", " "); printTexLongMath(statement[showStatement].mathString, "", "", 0, 0); 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 && htmlFlag) { /* 6-Dec-03 */ outputToString = 1; print2("\n"); outputToString = 0; } /*if (!(htmlFlag && texFlag)) {*/ if (!texFlag) { /* 6-Dec-03 fix */ print2("Its mandatory hypotheses in RPN order are:\n"); } /*if (texFlag) outputToString = 0;*/ /* 6-Dec-03 */ j = nmbrLen(statement[showStatement].reqHypList); for (i = 0; i < j; i++) { k = statement[showStatement].reqHypList[i]; if (statement[k].type != (char)e__ && (!htmlFlag && texFlag)) continue; /* 9/2/99 Don't put $f's in LaTeX output */ let(&str2, cat(" ",statement[k].labelName, " $", chr(statement[k].type), " ", NULL)); if (!texFlag) { printLongLine(cat(str2, nmbrCvtMToVString(statement[k].mathString), " $.", NULL), " "," "); } else { if (!(htmlFlag && texFlag)) { /* LaTeX */ /*let(&str3, space(strlen(str2)));*/ /* 6-Dec-03 */ /* This clears out printString */ /*printTexLongMath(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 && htmlFlag) { /* 6-Dec-03 */ outputToString = 1; print2("\n"); outputToString = 0; } /*if (j == 0 && !(htmlFlag && texFlag)) print2(" (None)\n");*/ if (j == 0 && !texFlag) print2(" (None)\n"); /* 6-Dec-03 fix */ let(&str1, ""); nmbrTmpPtr1 = statement[showStatement].reqDisjVarsA; nmbrTmpPtr2 = statement[showStatement].reqDisjVarsB; i = nmbrLen(nmbrTmpPtr1); if (i) { for (k = 0; k < i; k++) { if (!texFlag) { let(&str1, cat(str1, ", <", mathToken[nmbrTmpPtr1[k]].tokenName, ",", mathToken[nmbrTmpPtr2[k]].tokenName, ">", NULL)); } else { if (htmlFlag && texFlag) { let(&str2, ""); str2 = tokenToTex(mathToken[nmbrTmpPtr1[k]].tokenName); /* tokenToTex allocates str2; we must deallocate it */ let(&str1, cat(str1, "   ", str2, NULL)); let(&str2, ""); str2 = tokenToTex(mathToken[nmbrTmpPtr2[k]].tokenName); let(&str1, cat(str1, ",", str2, NULL)); } } } if (!texFlag) printLongLine(cat( "Its mandatory disjoint variable pairs are: ", right(str1,3),NULL)," "," "); } if (type == p__ && nmbrLen(statement[showStatement].optHypList) && !texFlag) { printLongLine(cat( "Its optional hypotheses are: ", nmbrCvtRToVString( statement[showStatement].optHypList),NULL), " "," "); } nmbrTmpPtr1 = statement[showStatement].optDisjVarsA; nmbrTmpPtr2 = statement[showStatement].optDisjVarsB; i = nmbrLen(nmbrTmpPtr1); if (i && type == p__) { if (!texFlag) { let(&str1, ""); } else { if (htmlFlag && 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, ", <", mathToken[nmbrTmpPtr1[k]].tokenName, ",", mathToken[nmbrTmpPtr2[k]].tokenName, ">", NULL)); } else { if (htmlFlag && texFlag) { /* tokenToTex allocates str2; we must deallocate it */ /* 12/1/01 don't output dummy variables let(&str2, ""); str2 = tokenToTex(mathToken[nmbrTmpPtr1[k]].tokenName); let(&str1, cat(str1, "   ", str2, NULL)); let(&str2, ""); str2 = tokenToTex(mathToken[nmbrTmpPtr2[k]].tokenName); let(&str1, cat(str1, ",", str2, NULL)); */ } } } if (!texFlag) { printLongLine(cat( "Its optional disjoint variable pairs are: ", right(str1,3),NULL)," "," "); } } /* Before 12/23/01 ********** Future: once stable, take out redundant code producing str1 if (texFlag && htmlFlag && str1[0]) { outputToString = 1; printLongLine(cat("
Substitutions into these variable", " pairs may not have variables in common: ", str1, "
", NULL), "", " "); outputToString = 0; } ***********/ /* 12/23/01 */ if (texFlag && htmlFlag && htmlDistinctVars[0]) { outputToString = 1; printLongLine(cat( "
Distinct variable group", /* 11-Aug-2006 nm Determine whether "group" or "groups". */ distVarGrps > 1 ? "s" : "", /* 11-Aug-2006 */ ": ", htmlDistinctVars, "
", NULL), "", "\""); /* original code: printLongLine(cat( "
Distinct variable group(s): ", htmlDistinctVars, "
", NULL), "", "\""); */ outputToString = 0; } if (texFlag) { outputToString = 1; if (htmlFlag && texFlag) print2("
\n"); outputToString = 0; /* Restore normal output */ /* will be done automatically at closing fprintf(texFilePtr, "%s", printString); let(&printString, ""); */ break; } let(&str1, nmbrCvtMToVString( statement[showStatement].reqVarList)); if (!strlen(str1)) let(&str1, "(None)"); printLongLine(cat( "The statement and its hypotheses require the variables: ", str1, NULL), " ", " "); if (type == p__ && nmbrLen(statement[showStatement].optVarList)) { printLongLine(cat( "These additional variables are allowed in its proof: " ,nmbrCvtMToVString( statement[showStatement].optVarList),NULL)," ", " "); /*??? Add variables required by proof */ } /* Note: statement[].reqVarList is only stored for $a and $p statements, not for $e or $f. */ let(&str1, nmbrCvtMToVString( statement[showStatement].reqVarList)); if (!strlen(str1)) let(&str1, "(None)"); printLongLine(cat("The variables it contains are: ", str1, NULL), " ", " "); break; default: break; } /* End switch(type) */ if (texFlag) { outputToString = 0; /* will be done automatically at closing fprintf(texFilePtr, "%s", printString); let(&printString, ""); */ } /* Start of finding definition for syntax statement */ if (htmlFlag && 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 = showStatement + 1; i <= statements; i++) { if (statement[i].type == (char)a__) { if (!strcmp("|-", mathToken[ (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 < statement[showStatement].mathStringLen; k++) { if (mathToken[(statement[showStatement].mathString)[k]]. tokenType == (char)con__) { if (!nmbrElementIn(1, statement[i].mathString, (statement[showStatement].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 */ outputToString = 1; let(&str1, left(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 ", statement[i].labelName, "", str2, ".
", NULL), "", "\""); } else { printLongLine(cat( "
See definition ", statement[i].labelName, "", str2, " for more information.
", NULL), "", "\""); } /* 10/10/02 Moved here from mmwtex.c */ /*print2("Colors of variables:\n");*/ printLongLine(cat( "
", NULL), "", "\""); 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 < mathTokens; i++) { if (!strcmp("wff", mathToken[i].tokenName)) { wffToken = i; break; } } } if (wffToken >= 0) { /* Temporarily zap statement type from $a to $p */ if (statement[showStatement].type != (char)a__) bug(231); statement[showStatement].type = (char)p__; /* Temporarily zap statement with "wff" token in 1st position so parseProof will not give errors (in typeProof() call) */ zapStatement1stToken = (statement[showStatement].mathString)[0]; (statement[showStatement].mathString)[0] = wffToken; if (strcmp("|-", mathToken[zapStatement1stToken].tokenName)) bug(230); nmbrTmpPtr1 = NULL_NMBRSTRING; nmbrLet(&nmbrTmpPtr1, statement[showStatement].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*/, showStatement /*statemNum*/, 0 /*maxEDepth*/, 0, /*step - 0 = step 1 */ /*For messages*/ 0 /*not noDistinct*/); 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(statement[showStatement].proofSectionPtr, "")) bug(231); if (statement[showStatement].proofSectionLen != 0) bug(232); let(&str1, nmbrCvtRToVString(nmbrTmpPtr2)); /* Temporarily zap proof into the $a statement */ statement[showStatement].proofSectionPtr = str1; statement[showStatement].proofSectionLen = strlen(str1) - 1; /* Display the HTML proof of syntax breakdown */ typeProof(showStatement, 0 /*pipFlag*/, 0 /*startStep*/, 0 /*endStep*/, 0 /*startIndent*/, /* Not used */ 0 /*endIndent*/, 0 /*essentialFlag*/, /* <- also used as def flag in typeProof */ 1 /*renumberFlag*/, 0 /*unknownFlag*/, 0 /*notUnifiedFlag*/, 0 /*reverseFlag*/, 1 /*noIndentFlag*/, 0 /*splitColumn*/, 1 /*texFlag*/, /* Means either latex or html */ 1 /*htmlFlag*/); /* Restore the zapped statement structure */ statement[showStatement].proofSectionPtr = ""; statement[showStatement].proofSectionLen = 0; /* Deallocate storage */ let(&str1, ""); nmbrLet(&nmbrTmpPtr2, NULL_NMBRSTRING); } /* if (nmbrLen(nmbrTmpPtr2)) */ /* Restore the zapped statement structure */ statement[showStatement].type = (char)a__; (statement[showStatement].mathString)[0] = zapStatement1stToken; /* Deallocate storage */ nmbrLet(&nmbrTmpPtr1, NULL_NMBRSTRING); } /* if (wffToken >= 0) */ } /* if (subType == DEFINITION) */ } /* if (htmlFlag && texFlag) */ /* End of finding definition for syntax statement */ /* 10/6/99 - Start of creating used-by list for html page */ if (htmlFlag && texFlag) { /* 10/25/02 Clear out any previous printString accumulation for printStringForReferencedBy case below */ fprintf(texFilePtr, "%s", printString); let(&printString, ""); /* Start outputting to printString */ if (outputToString != 0) bug(242); outputToString = 1; if (subType != SYNTAX) { /* Only do this for definitions and axioms, not syntax statements */ let(&str1, ""); str1 = traceUsage(showStatement, 0 /* recursiveFlag */); if (str1[0]) { /* Used by at least one */ /* str1 will have a leading space before each label */ /* Convert usage list 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)); printLongLine(str2, "", "\""); } } 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 printString into a temporary global holding variable to print at the proper place inside of typeProof(). Ugly but necessary with present design. */ let(&printStringForReferencedBy, printString); let(&printString, ""); } /* Printing of the trailer in mmwtex.c will close out string later */ outputToString = 0; } /* if (htmlFlag && 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 (htmlFlag && texFlag) { /*** Output the html proof for $p statements ***/ /* Note that we also output the axiom and definition usage lists inside this function */ if (statement[showStatement].type == (char)p__) { typeProof(showStatement, 0 /*pipFlag*/, 0 /*startStep*/, 0 /*endStep*/, 0 /*startIndent*/, /* Not used */ 0 /*endIndent*/, 1 /*essentialFlag*/, 1 /*renumberFlag*/, 0 /*unknownFlag*/, 0 /*notUnifiedFlag*/, 0 /*reverseFlag*/, 1 /*noIndentFlag*/, 0 /*splitColumn*/, 1 /*texFlag*/, /* Means either latex or html */ 1 /*htmlFlag*/); } /* if (statement[showStatement].type == (char)p__) */ } /* if (htmlFlag && texFlag) */ /* End of html proof for $p statements */ /* typeProof should have cleared this out */ if (printStringForReferencedBy[0]) bug(243); returnPoint: /* Deallocate strings */ nmbrLet(&nmbrDDList, NULL_NMBRSTRING); let(&str1, ""); let(&str2, ""); let(&str3, ""); let(&str4, ""); let(&htmlDistinctVars, ""); } /* typeStatement */ /* 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 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 proofInProgress; statemNum must be proveStatement*/ long startStep, long endStep, long startIndent, 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, flag texFlag, flag htmlFlag /* htmlFlag added 6/27/99 */ /* flag 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. / NORMAL - The proof is displayed in normal format suitable for inclusion in a source file. May not be used with any other qualifier. / COMPRESSED - The proof is displayed in compressed format suitable for inclusion in a source file. May not be used with any other qualifier. / STATEMENT_SUMMARY - Summarizes all statements (like a brief SHOW STATEMENT) used by the proof. May not be used with any other qualifier except / ESSENTIAL. / DETAILED_STEP - Shows the details of what is happening at a specific proof step. May not be used with any other qualifier. / MIDI - 8/28/00 - puts out a midi sound file instead of a proof - determined by the global variable midiFlag, not by a parameter to typeProof() */ long i, plen, step, stmt, lens, lent, maxStepNum; vstring tmpStr = ""; vstring tmpStr1 = ""; vstring locLabDecl = ""; vstring tgtLabel = ""; vstring srcLabel = ""; vstring startPrefix = ""; vstring tgtPrefix = ""; vstring srcPrefix = ""; vstring userPrefix = ""; vstring contPrefix = ""; vstring statementUsedFlags = ""; nmbrString *proof = NULL_NMBRSTRING; nmbrString *localLabels = NULL_NMBRSTRING; nmbrString *localLabelNames = NULL_NMBRSTRING; nmbrString *indentationLevel = NULL_NMBRSTRING; nmbrString *targetHyps = NULL_NMBRSTRING; nmbrString *essentialFlags = NULL_NMBRSTRING; nmbrString *stepRenumber = NULL_NMBRSTRING; nmbrString *notUnifiedFlags = NULL_NMBRSTRING; nmbrString *unprovedList = NULL_NMBRSTRING; /* For traceProofWork() */ long maxLabelLen = 0; long maxStepNumLen = 1; char type; flag stepPrintFlag; long fromStep, toStep, byStep; vstring hypStr = ""; nmbrString *hypPtr; long hyp, hypStep; /* For statement syntax breakdown (see section below added 2/5/02 for better syntax hints), we declare the following 3 variables. */ 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 */ nmbrString *nmbrTmpPtr1; /* Pointer only; not allocated directly */ nmbrString *nmbrTmpPtr2; /* Pointer only; not allocated directly */ if (htmlFlag && texFlag) { outputToString = 1; /* Flag for print2 to add to printString */ print2("
", "Colors of variables: ", htmlVarColors, "
This ", str3, " is referenced by:", NULL)); /* Convert str1 to trailing space after each label */ let(&str1, cat(right(str1, 2), " ", NULL)); 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 (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)); } let(&str2, cat(str2, "
\n"); print2("", NULL), "", "\""); print2( "\n"); outputToString = 0; /* printTexLongMath in typeProof will do this fprintf(texFilePtr, "%s", printString); let(&printString, ""); */ } if (!pipFlag) { parseProof(showStatement); if (wrkProof.errorSeverity > 1) return; /* Display could crash */ verifyProof(showStatement); } if (!pipFlag) { nmbrLet(&proof, wrkProof.proofString); /* The proof */ if (midiFlag) { /* 8/28/00 */ /* Get the uncompressed version of the proof */ nmbrLet(&proof, nmbrUnsquishProof(proof)); } } else { nmbrLet(&proof, 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. */ if (htmlFlag && texFlag && !noIndentFlag /* Lemmon */) { /* Only Lemmon-style proofs are implemented for html */ bug(218); } if (htmlFlag && texFlag) { for (step = 0; step < plen; step++) { stmt = proof[step]; if (stmt < 0) continue; /* Unknown or label ref */ type = statement[stmt].type; if (type == f__ || type == e__ /* It's a hypothesis */ || 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 || 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 (midiFlag) { outputMidi(plen, indentationLevel, essentialFlags, midiParam, 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 (htmlFlag && texFlag && 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 */ } } /* 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++; } /* 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(proofInProgress.source[step])) { if (!nmbrEq(proofInProgress.target[step], proofInProgress.source[step])) notUnifiedFlags[step] = 1; } if (nmbrLen(proofInProgress.user[step])) { if (!nmbrEq(proofInProgress.target[step], proofInProgress.user[step])) notUnifiedFlags[step] = 1; } } } /* Get local labels and maximum label length */ /* lent = target length, lens = source length */ for (step = 0; step < plen; step++) { lent = strlen(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 = strlen(str(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 = strlen(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 && !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 (htmlFlag && texFlag) { if (stepRenumber[step] == 0) stepPrintFlag = 0; } /* 8/28/00 For MIDI files, ignore all qualifiers and process all steps */ if (midiFlag) stepPrintFlag = 1; if (!stepPrintFlag) continue; if (noIndentFlag) { let(&tgtLabel, ""); } else { let(&tgtLabel, statement[targetHyps[step]].labelName); } let(&locLabDecl, ""); /* Local label declaration */ stmt = proof[step]; if (stmt < 0) { if (stmt <= -1000) { stmt = -1000 - stmt; if (htmlFlag && texFlag) 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(localLabelNames[stmt]), NULL)); } else { let(&srcLabel, cat("=", str(localLabelNames[stmt]), NULL)); } type = 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 (!(htmlFlag && texFlag)) { /* No local label declaration is shown for html */ let(&locLabDecl, cat("@", str(localLabelNames[step]), ":", NULL)); } } else { let(&locLabDecl, cat(str(localLabelNames[step]), ":", NULL)); } } if (noIndentFlag) { let(&srcLabel, statement[stmt].labelName); /* For non-indented mode, add step numbers of hypotheses after label */ let(&hypStr, ""); hypStep = step - 1; hypPtr = statement[stmt].reqHypList; for (hyp = statement[stmt].numReqHyp - 1; hyp >=0; hyp--) { if (!essentialFlag || statement[hypPtr[hyp]].type == (char)e__) { i = stepRenumber[hypStep]; if (i == 0) { if (!(htmlFlag && texFlag)) 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(i)); } else { let(&hypStr, "?"); } } else { /* Put comma between more than one hypothesis reference */ if (i != -(long)'?') { let(&hypStr, cat(str(i), ",", hypStr, NULL)); } else { let(&hypStr, cat("?", ",", hypStr, NULL)); } } } if (hyp < 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("=", statement[stmt].labelName, NULL)); } type = statement[stmt].type; } #define PF_INDENT_INC 2 /* Print the proof line */ if (stepPrintFlag) { if (noIndentFlag) { let(&startPrefix, cat( space(maxStepNumLen - strlen(str(stepRenumber[step]))), str(stepRenumber[step]), " ", srcLabel, space(splitColumn - strlen(srcLabel) - strlen(locLabDecl) - 1 - maxStepNumLen - 1), " ", locLabDecl, NULL)); if (pipFlag) { let(&tgtPrefix, startPrefix); let(&srcPrefix, cat( space(maxStepNumLen - strlen(str(stepRenumber[step]))), space(strlen(str(stepRenumber[step]))), " ", space(splitColumn - 1 - maxStepNumLen), NULL)); let(&userPrefix, cat( space(maxStepNumLen - strlen(str(stepRenumber[step]))), space(strlen(str(stepRenumber[step]))), " ", "(User)", space(splitColumn - strlen("(User)") - 1 - maxStepNumLen), NULL)); } let(&contPrefix, space(strlen(startPrefix) + 4)); } else { /* not noIndentFlag */ let(&startPrefix, cat( space(maxStepNumLen - strlen(str(stepRenumber[step]))), str(stepRenumber[step]), " ", space(indentationLevel[step] * PF_INDENT_INC - strlen(locLabDecl)), locLabDecl, tgtLabel, srcLabel, space(maxLabelLen - strlen(tgtLabel) - strlen(srcLabel)), NULL)); if (pipFlag) { let(&tgtPrefix, cat( space(maxStepNumLen - strlen(str(stepRenumber[step]))), str(stepRenumber[step]), " ", space(indentationLevel[step] * PF_INDENT_INC - strlen(locLabDecl)), locLabDecl, tgtLabel, space(strlen(srcLabel)), space(maxLabelLen - strlen(tgtLabel) - strlen(srcLabel)), NULL)); let(&srcPrefix, cat( space(maxStepNumLen - strlen(str(stepRenumber[step]))), space(strlen(str(stepRenumber[step]))), " ", space(indentationLevel[step] * PF_INDENT_INC - strlen(locLabDecl)), space(strlen(locLabDecl)), space(strlen(tgtLabel)), srcLabel, space(maxLabelLen - strlen(tgtLabel) - strlen(srcLabel)), NULL)); let(&userPrefix, cat( space(maxStepNumLen - strlen(str(stepRenumber[step]))), space(strlen(str(stepRenumber[step]))), " ", space(indentationLevel[step] * PF_INDENT_INC - strlen(locLabDecl)), space(strlen(locLabDecl)), space(strlen(tgtLabel)), "=(User)", space(maxLabelLen - strlen(tgtLabel) - 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 (!midiFlag) { /* 8/28/00 */ printLongLine(cat(startPrefix," $", chr(type), " ", nmbrCvtMToVString(wrkProof.mathStringPtrs[step]), NULL), contPrefix, chr(1)); /* chr(1) is right-justify flag for printLongLine */ } } else { /* TeX or HTML */ printTexLongMath(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(proofInProgress.target[step], proofInProgress.source[step]) && nmbrLen(proofInProgress.source[step])) { if (!texFlag) { printLongLine(cat(tgtPrefix, " $", chr(type), " ", nmbrCvtMToVString(proofInProgress.target[step]), NULL), contPrefix, chr(1)); /* chr(1) is right-justify flag for printLongLine */ printLongLine(cat(srcPrefix," = ", nmbrCvtMToVString(proofInProgress.source[step]), NULL), contPrefix, chr(1)); /* chr(1) is right-justify flag for printLongLine */ } else { /* TeX or HTML */ printTexLongMath(proofInProgress.target[step], cat(tgtPrefix, " $", chr(type), " ", NULL), contPrefix, 0, 0); printTexLongMath(proofInProgress.source[step], cat(srcPrefix, " = ", NULL), contPrefix, 0, 0); } } else { if (!texFlag) { printLongLine(cat(startPrefix, " $", chr(type), " ", nmbrCvtMToVString(proofInProgress.target[step]), NULL), contPrefix, chr(1)); /* chr(1) is right-justify flag for printLongLine */ } else { /* TeX or HTML */ printTexLongMath(proofInProgress.target[step], cat(startPrefix, " $", chr(type), " ", NULL), contPrefix, 0, 0); } } if (nmbrLen(proofInProgress.user[step])) { if (!texFlag) { printLongLine(cat(userPrefix, " = ", nmbrCvtMToVString(proofInProgress.user[step]), NULL), contPrefix, chr(1)); /* chr(1) is right-justify flag for printLongLine */ } else { printTexLongMath(proofInProgress.user[step], cat(userPrefix, " = ", NULL), contPrefix, 0, 0); } } } } } /* Next step */ if (!pipFlag) { cleanWrkProof(); /* Deallocate verifyProof storage */ } if (htmlFlag && texFlag) { outputToString = 1; print2("
Proof of Theorem \n"); print2("Detailed syntax breakdown of Axiom \n"); print2("Detailed syntax breakdown of Definition ", asciiToTt(statement[statemNum].labelName), "
StepHypRef\n"); print2("Expression
\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(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 (statement[stmt].type == a__) { if (strcmp("|-", mathToken[ (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 < mathTokens; i++) { if (!strcmp("wff", 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 < 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 (statement[statemNum].type != (char)p__) bug(245); nmbrTmpPtr1 = NULL_NMBRSTRING; nmbrLet(&nmbrTmpPtr1, statement[statemNum].mathString); } else { /* Ignore $f */ if (statement[statement[statemNum].reqHypList[i]].type == (char)f__) continue; /* Must therefore be a $e */ if (statement[statement[statemNum].reqHypList[i]].type != (char)e__) bug(234); nmbrTmpPtr1 = NULL_NMBRSTRING; nmbrLet(&nmbrTmpPtr1, statement[statement[statemNum].reqHypList[i]].mathString); } if (strcmp("|-", 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*/); 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 (statement[stmt].type == a__) { if (strcmp("|-", mathToken[ (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 <= 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 */ if (printStringForReferencedBy[0]) { printLongLine(printStringForReferencedBy, "", "\""); let(&printStringForReferencedBy, ""); } /* Get list of axioms and definitions assumed by proof */ let(&statementUsedFlags, ""); traceProofWork(statemNum, 1 /*essentialFlag*/, &statementUsedFlags, /*&statementUsedFlags*/ &unprovedList /* &unprovedList */); if (strlen(statementUsedFlags) != statements + 1) bug(227); /* First get axioms */ let(&tmpStr, ""); for (stmt = 1; stmt <= statements; stmt++) { if (statementUsedFlags[stmt] == 'y' && statement[stmt].type == a__) { let(&tmpStr1, left(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 <= statements; stmt++) { if (statementUsedFlags[stmt] == 'y' && statement[stmt].type == a__) { let(&tmpStr1, left(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(statement[unprovedList[0]].labelName, 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 */ } /* if essentialFlag */ /* Printing of the trailer in mmwtex.c will close out string later */ 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, ""); 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); } /* 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(wrkProof.proofString); if (plen < detailStep || detailStep < 1) { printLongLine(cat("?The step number should be from 1 to ", str(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, 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(nextLocLabNum)); while (1) { voidPtr = (void *)bsearch(tmpStr, allLabelKeyBase, numAllLabelKeys, sizeof(long), labelSrchCmp); if (!voidPtr) break; /* It does not conflict */ nextLocLabNum++; /* Try the next one */ let(&tmpStr1,str(nextLocLabNum)); } localLabelNames[step] = nextLocLabNum; nextLocLabNum++; /* Prepare for next local label */ } } } /* Next step */ /* Print the step */ let(&tmpStr, 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(localLabelNames[stmt]), NULL)); type = 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(localLabelNames[detailStep - 1]), ":", NULL)); } let(&tmpStr, cat(tmpStr, "=", statement[stmt].labelName, NULL)); type = statement[stmt].type; } /* Print the proof line */ printLongLine(cat("Proof step ", str(detailStep), ": ", tmpStr1, tmpStr, " $", chr(type), " ", nmbrCvtMToVString(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(stmt), " (via local label reference \"", str(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 \"", statement[stmt].labelName, "\" ($", chr(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(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 \"", statement[targetStmt].labelName, "\" ($", chr(statement[targetStmt].type), ").", NULL)); } let(&tmpStr, cat(tmpStr, tmpStr1, NULL)); if (sourceStmt >= 0) { if (statement[sourceStmt].type == a__ || statement[sourceStmt].type == p__) { j = nmbrLen(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, "\"", statement[statement[sourceStmt].reqHypList[i]].labelName, "\" ($", chr(statement[statement[sourceStmt].reqHypList[i]].type), ", step ", str(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 \"", statement[getStep.targetParentStmt].labelName, "\" ($", chr(statement[getStep.targetParentStmt].type),", step ", str(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 (statement[sourceStmt].type == a__ || statement[sourceStmt].type == p__) { print2("The source assertion before substitution was:\n"); printLongLine(cat(" ", statement[sourceStmt].labelName, " $", chr(statement[sourceStmt].type), " ", nmbrCvtMToVString( 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(" ", mathToken[getStep.sourceSubstsNmbr[i]].tokenName," ", space(9 - strlen( mathToken[getStep.sourceSubstsNmbr[i]].tokenName)), nmbrCvtMToVString(getStep.sourceSubstsPntr[i]), NULL), " ", " "); } } } } if (detailStep < plen) { print2("The target hypothesis before substitution was:\n"); printLongLine(cat(" ", statement[targetStmt].labelName, " $", chr(statement[targetStmt].type), " ", nmbrCvtMToVString( 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(" ", mathToken[getStep.targetSubstsNmbr[i]].tokenName, " ", space(9 - strlen( 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); } /* Summary of statements in proof */ 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 && htmlFlag) bug(239); if (!texFlag) { print2("Summary of statements used in the proof of \"%s\":\n", statement[statemNum].labelName); } else { outputToString = 1; /* Flag for print2 to add to printString */ if (!htmlFlag) { print2("\n"); print2("\\vspace{1ex}\n"); printLongLine(cat("Summary of statements used in the proof of ", "{\\tt ", asciiToTt(statement[statemNum].labelName), "}:", NULL), "", " "); } else { printLongLine(cat("Summary of statements used in the proof of ", "", asciiToTt(statement[statemNum].labelName), ":", NULL), "", "\""); } outputToString = 0; fprintf(texFilePtr, "%s", printString); let(&printString, ""); } if (statement[statemNum].type != p__) { print2(" This is not a provable ($p) statement.\n"); return; } parseProof(statemNum); nmbrLet(&proof, wrkProof.proofString); /* The proof */ 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 (statement[stmt].type != a__ && 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(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') { let(&str1, cat(" is located on line ", str(statement[stmt].lineNum), " of the file ", NULL)); if (!texFlag) { print2("\n"); printLongLine(cat("Statement ", statement[stmt].labelName, str1, "\"", statement[stmt].fileName, "\".",NULL), "", " "); } else { outputToString = 1; /* Flag for print2 to add to printString */ if (!htmlFlag) { print2("\n"); print2("\n"); print2("\\vspace{1ex}\n"); printLongLine(cat("Statement {\\tt ", asciiToTt(statement[stmt].labelName), "} ", str1, "{\\tt ", asciiToTt(statement[stmt].fileName), "}.", NULL), "", " "); print2("\n"); } else { printLongLine(cat("Statement ", asciiToTt(statement[stmt].labelName), " ", str1, " ", asciiToTt(statement[stmt].fileName), " ", NULL), "", "\""); } outputToString = 0; fprintf(texFilePtr, "%s", printString); let(&printString, ""); } type = statement[stmt].type; let(&str1, ""); str1 = getDescription(stmt); if (str1[0]) { if (!texFlag) { printLongLine(cat("\"", str1, "\"", NULL), "", " "); } else { printTexComment(str1, 1); } } /* print2("Its mandatory hypotheses in RPN order are:\n"); */ j = nmbrLen(statement[stmt].reqHypList); for (i = 0; i < j; i++) { k = statement[stmt].reqHypList[i]; if (!essentialFlag || statement[k].type != f__) { let(&str2, cat(" ",statement[k].labelName, " $", chr(statement[k].type), " ", NULL)); if (!texFlag) { printLongLine(cat(str2, nmbrCvtMToVString(statement[k].mathString), " $.", NULL), " "," "); } else { let(&str3, space(strlen(str2))); printTexLongMath(statement[k].mathString, str2, str3, 0, 0); } } } let(&str1, ""); type = statement[stmt].type; if (type == p__) let(&str1, " $= ..."); let(&str2, cat(" ", statement[stmt].labelName, " $",chr(type), " ", NULL)); if (!texFlag) { printLongLine(cat(str2, nmbrCvtMToVString(statement[stmt].mathString), str1, " $.", NULL), " ", " "); } else { let(&str3, space(strlen(str2))); printTexLongMath(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); } /* Traces back the statements used by a proof, recursively. */ void traceProof(long statemNum, flag essentialFlag, flag axiomFlag) { long stmt, pos; vstring statementUsedFlags = ""; /* y/n flags that statement is used */ vstring outputString = ""; nmbrString *unprovedList = NULL_NMBRSTRING; if (axiomFlag) { print2( "Statement \"%s\" assumes the following axioms ($a statements):\n", statement[statemNum].labelName); } else { print2( "The proof of statement \"%s\" uses the following earlier statements:\n", statement[statemNum].labelName); } traceProofWork(statemNum, essentialFlag, &statementUsedFlags, &unprovedList); if (strlen(statementUsedFlags) != statements + 1) bug(226); /* Build the output string */ let(&outputString, ""); for (stmt = 1; stmt < statemNum; stmt++) { if (statementUsedFlags[stmt] == 'y') { if (axiomFlag) { if (statement[stmt].type == a__) { let(&outputString, cat(outputString, " ", statement[stmt].labelName, NULL)); } } else { let(&outputString, cat(outputString, " ", statement[stmt].labelName, NULL)); switch (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 */ 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, " ", statement[unprovedList[ pos]].labelName, NULL)); } let(&outputString, cat(" ", outputString, NULL)); printLongLine(outputString, " ", " "); } /* Deallocate */ let(&outputString, ""); let(&statementUsedFlags, ""); nmbrLet(&unprovedList, NULL_NMBRSTRING); } /* 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 *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; nmbrLet(&statementList, nmbrSpace(statements)); statementList[0] = statemNum; slen = 1; nmbrLet(&(*unprovedListP), NULL_NMBRSTRING); /* List of unproved statements */ let(&(*statementUsedFlagsP), string(statements + 1, 'n')); /* Init. to 'no' */ for (pos = 0; pos < slen; pos++) { if (statement[statementList[pos]].type != p__) { continue; /* Not a $p */ } parseProof(statementList[pos]); nmbrLet(&proof, wrkProof.proofString); /* The proof */ 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 (statement[stmt].type != a__ && statement[stmt].type != p__) { continue; } } /* Add this statement to the statement list if not already in it */ if ((*statementUsedFlagsP)[stmt] == 'n') { statementList[slen] = stmt; slen++; (*statementUsedFlagsP)[stmt] = 'y'; } } /* Next step */ } /* Next pos */ /* Deallocate */ nmbrLet(&essentialFlags, NULL_NMBRSTRING); nmbrLet(&proof, NULL_NMBRSTRING); nmbrLet(&statementList, NULL_NMBRSTRING); return; } 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 (statement[statemNum].type != p__) { print2("Statement %s is not a $p statement.\n", statement[statemNum].labelName); return; } printLongLine(cat("The proof tree traceback for statement \"", 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); } 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) > (screenWidth - MAX_LINE_LEN) + 50) { indentShift = indentShift + 40 + (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 - (screenWidth - MAX_LINE_LEN); print2("****** Shifting indentation. Total shift is now %ld.\n", (long)indentShift); } let(&outputStr, cat(space(recursDepth * INDENT_INCR - indentShift), statement[statemNum].labelName, " $", chr(statement[statemNum].type), " \"", edit(outputStr, 8 + 128), "\"", NULL)); if (len(outputStr) > MAX_LINE_LEN + (screenWidth - MAX_LINE_LEN)) { let(&outputStr, cat(left(outputStr, MAX_LINE_LEN + (screenWidth - MAX_LINE_LEN) - 3), "...", NULL)); } if (statement[statemNum].type == p__ || statement[statemNum].type == a__) { /* Only print assertions to reduce output bulk */ print2("%s\n", outputStr); } if (statement[statemNum].type != p__) { let(&outputStr, ""); return; } if (endIndent) { /* An indentation level limit is set */ if (endIndent < recursDepth + 2) { let(&outputStr, ""); return; } } parseProof(statemNum); nmbrLet(&proof, wrkProof.proofString); /* The proof */ 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 (statement[stmt].type == p__ || statement[stmt].type == a__) { let(&outputStr, cat(outputStr, " ", 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 ", 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); } /* Called by SHOW TRACE_BACK
", "Colors of variables: ", htmlVarColors, "
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 < statement[stmt].mathStringLen; i++) { if (mathToken[(statement[stmt].mathString)[i]].tokenType == (char)con__) { /* Skip parentheses, commas, etc. */ if (strcmp(mathToken[(statement[stmt].mathString)[i] ].tokenName, "(") && strcmp(mathToken[(statement[stmt].mathString)[i] ].tokenName, ",") && strcmp(mathToken[(statement[stmt].mathString)[i] ].tokenName, ")") && strcmp(mathToken[(statement[stmt].mathString)[i] ].tokenName, ":") ) { tmpStr1 = tokenToTex(mathToken[(statement[stmt].mathString)[i] ].tokenName); break; } } } /* Next i */ /* Special cases hard-coded for set.mm */ if (!strcmp(statement[stmt].labelName, "wbr")) /* binary relation */ let(&tmpStr1, " class class class "); if (!strcmp(statement[stmt].labelName, "cv")) let(&tmpStr1, "[set variable]"); /* 10/10/02 Let's don't do cv - confusing to reader */ if (!strcmp(statement[stmt].labelName, "cv")) continue; if (!strcmp(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, "", statement[stmt].labelName, "   ", NULL)); *******/ let(&tmpStr, cat(tmpStr, "", 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, "  ", 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, "  ", 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, " ", statement[unprovedList[i]].labelName, "", NULL)); } printLongLine(cat(tmpStr, "