diff --git a/src/metamath.c b/src/metamath.c index ed7c206d..355ba311 100644 --- a/src/metamath.c +++ b/src/metamath.c @@ -2074,9 +2074,9 @@ void command(int argc, char *argv[]) { readInput(); if (switchPos("/ VERIFY")) { - verifyProofs("*",1); /* Parse and verify */ + verifyProofs("*",VERIFY_FULL); /* Parse and verify */ } else { - /* verifyProofs("*",0); */ /* Parse only (for gross error checking) */ + /* verifyProofs("*",VERIFY_NONE); */ /* Parse only (for gross error checking) */ } if (g_sourceHasBeenRead == 1) { @@ -4104,8 +4104,8 @@ void command(int argc, char *argv[]) { nmbrLen(g_ProofInProgress.proof) != 0 */ parseProof(g_proveStatement); - verifyProof(g_proveStatement); /* Necessary to set RPN stack ptrs - before calling cleanWrkProof() */ + verifyProof(g_proveStatement, VERIFY_NONE); /* Necessary to set RPN stack + ptrs before calling cleanWrkProof() */ if (g_WrkProof.errorSeverity > 1) { print2( "The starting proof has a severe error. It will not be used.\n"); @@ -5417,9 +5417,9 @@ void command(int argc, char *argv[]) { the proof, and deallocate the g_WrkProof structure. Either none of them or all of them must be called. */ parseProof(g_proveStatement); - verifyProof(g_proveStatement); /* Must be called even if error - occurred in parseProof, to init RPN stack - for cleanWrkProof() */ + verifyProof(g_proveStatement, VERIFY_NONE); /* Must be called + even if error occurred in parseProof, to init + RPN stack for cleanWrkProof() */ /* don't change proof if there is an error (which could be pre-existing). */ i = (g_WrkProof.errorSeverity > 1); @@ -6405,11 +6405,18 @@ void command(int argc, char *argv[]) { } if (cmdMatches("VERIFY PROOF")) { - if (switchPos("/ SYNTAX_ONLY")) { - verifyProofs(g_fullArg[2],0); /* Parse only */ - } else { - verifyProofs(g_fullArg[2],1); /* Parse and verify */ - } + i = (switchPos("/ SYNTAX_ONLY") != 0) ? VERIFY_NONE : VERIFY_FULL; + if (switchPos("/ DISJOINT_VARS") != 0) + i |= VERIFY_DVS; + if (switchPos("/ ALL_DISJOINT_VARS") != 0) + i |= VERIFY_DVS | VERIFY_DUMMY_DVS; + if (switchPos("/ ESSENTIAL") != 0) + i |= VERIFY_ESSENTIAL; + if (switchPos("/ FLOATING") != 0) + i |= VERIFY_FLOATING; + if (switchPos("/ HYPOTHESES") != 0) + i |= VERIFY_ESSENTIAL | VERIFY_FLOATING; + verifyProofs(g_fullArg[2], (flag)i); continue; } diff --git a/src/mmcmdl.c b/src/mmcmdl.c index 031ce93e..fe59e4fd 100644 --- a/src/mmcmdl.c +++ b/src/mmcmdl.c @@ -1206,8 +1206,8 @@ flag processCommandLine(void) { if (lastArgMatches("/")) { i++; if (!getFullArg(i, cat( - "SYNTAX_ONLY", - "|", NULL))) + "SYNTAX_ONLY|DISJOINT_VARS|ALL_DISJOINT_VARS", + "|ESSENTIAL|FLOATING|HYPOTHESES|", NULL))) goto pclbad; } else { break; diff --git a/src/mmcmds.c b/src/mmcmds.c index 2a1b9494..14de0616 100644 --- a/src/mmcmds.c +++ b/src/mmcmds.c @@ -1491,7 +1491,7 @@ void typeProof(long statemNum, } return; /* verifyProof() could crash */ } - verifyProof(g_showStatement); + verifyProof(g_showStatement, VERIFY_NONE); } if (!pipFlag) { @@ -2357,7 +2357,7 @@ void showDetailStep(long statemNum, long detailStep) { /* 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); + verifyProof(statemNum, VERIFY_NONE); nmbrLet(&proof, g_WrkProof.proofString); /* The proof */ @@ -4674,8 +4674,13 @@ void eraseSource(void) /* ERASE command */ } /* eraseSource */ -/* If verify = 0, parse the proofs only for gross error checking. - If verify = 1, do the full verification. */ +/* If verifyFlag = VERIFY_NONE, parse the proofs only for gross error checking. + If verifyFlag includes VERIFY_FULL, do the full verification. + If verifyFlag includes VERIFY_DVS, check for unused $d conditions on nondummy + variables. + If verifyFlag includes VERIFY_DUMMY_DVS, check for all unused $d conditions. + If verifyFlag includes VERIFY_ESSENTIAL, check for unused $e statements. + If verifyFlag includes VERIFY_FLOATING, check for unused $f statements. */ void verifyProofs(vstring labelMatch, flag verifyFlag) { vstring_def(emptyProofList); long i, k; @@ -4697,7 +4702,7 @@ void verifyProofs(vstring labelMatch, flag verifyFlag) { #ifdef CLOCKS_PER_SEC clockStart = clock(); /* Retrieve start time */ #endif - if (!strcmp("*", labelMatch) && verifyFlag) { + if (!strcmp("*", labelMatch) && (verifyFlag & VERIFY_FULL)) { /* Use status bar */ let(&header, "0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100%"); print2("%s\n", header); @@ -4706,7 +4711,7 @@ void verifyProofs(vstring labelMatch, flag verifyFlag) { errorFound = 0; for (i = 1; i <= g_statements; i++) { - if (!strcmp("*", labelMatch) && verifyFlag) { + if (!strcmp("*", labelMatch) && (verifyFlag & VERIFY_FULL)) { while (lineLen < (50 * i) / g_statements) { print2("."); lineLen++; @@ -4715,7 +4720,7 @@ void verifyProofs(vstring labelMatch, flag verifyFlag) { if (g_Statement[i].type != p_) continue; if (!matchesList(g_Statement[i].labelName, labelMatch, '*', '?')) continue; - if (strcmp("*",labelMatch) && verifyFlag) { + if (strcmp("*",labelMatch) && (verifyFlag & VERIFY_FULL)) { /* If not *, print individual labels */ lineLen = lineLen + (long)strlen(g_Statement[i].labelName) + 1; if (lineLen > 72) { @@ -4728,8 +4733,8 @@ void verifyProofs(vstring labelMatch, flag verifyFlag) { k = parseProof(i); if (k >= 2) errorFound = 1; if (k < 2) { /* $p with no error */ - if (verifyFlag) { - if (verifyProof(i) >= 2) errorFound = 1; + if (verifyFlag & VERIFY_FULL) { + if (verifyProof(i, verifyFlag) >= 2) errorFound = 1; cleanWrkProof(); /* Deallocate verifyProof storage */ } } @@ -4738,7 +4743,7 @@ void verifyProofs(vstring labelMatch, flag verifyFlag) { NULL)); } } - if (verifyFlag) { + if (verifyFlag & VERIFY_FULL) { print2("\n"); } @@ -4748,7 +4753,7 @@ void verifyProofs(vstring labelMatch, flag verifyFlag) { right(emptyProofList,3), NULL)," "," "); } if (!emptyProofList[0] && !errorFound && !strcmp("*", labelMatch)) { - if (verifyFlag) { + if (verifyFlag & VERIFY_FULL) { #ifdef CLOCKS_PER_SEC print2("All proofs in the database were verified in %1.2f s.\n", (double)((1.0 * (double)(clock() - clockStart)) / CLOCKS_PER_SEC)); diff --git a/src/mmhlpb.c b/src/mmhlpb.c index 85c5ba03..35988858 100644 --- a/src/mmhlpb.c +++ b/src/mmhlpb.c @@ -648,7 +648,8 @@ H(""); if (!strcmp(saveHelpCmd, "HELP VERIFY PROOF")) { -H("Syntax: VERIFY PROOF [/ SYNTAX_ONLY]"); +H("Syntax: VERIFY PROOF [/ SYNTAX_ONLY] [/DISJOINT_VARS]"); +H(" [/ALL_DISJOINT_VARS] [/ESSENTIAL] [/FLOATING] [/HYPOTHESES]"); H(""); H("This command verifies the proofs of the specified statements."); H(" may contain * and ? wildcard characters to verify more than"); @@ -657,10 +658,17 @@ H("\"abc\" followed by any single character followed by \"def\"."); H("VERIFY PROOF * will verify all proofs in the database."); H("See HELP SEARCH for complete wildcard matching rules."); H(""); -H("Optional qualifier:"); +H("Optional qualifiers:"); H(" / SYNTAX_ONLY - This qualifier will perform a check of syntax and RPN"); H(" stack violations only. It will not verify that the proof is"); H(" correct."); +H(" / DISJOINT_VARS - List disjoint variable conditions for non-dummy"); +H(" variables not used by the verifier."); +H(" / ALL_DISJOINT_VARS - List all disjoint variable conditions not used"); +H(" by the verifier."); +H(" / ESSENTIAL - List essential hypotheses not used by the verifier."); +H(" / FLOATING - List floating hypotheses not used by the verifier."); +H(" / HYPOTHESES - List all hypotheses not used by the verifier."); H(""); H("Note: READ, followed by VERIFY PROOF *, will ensure the database is free"); H("from errors in Metamath language but will not check the markup language"); diff --git a/src/mmveri.c b/src/mmveri.c index a2c8ec85..07bfda02 100644 --- a/src/mmveri.c +++ b/src/mmveri.c @@ -18,11 +18,16 @@ struct getStep_struct getStep = {0, 0, 0, 0, 0, NULL_PNTRSTRING}; /* Verify proof of one statement in source file. Uses wrkProof structure. - Assumes that parseProof() has just been called for this statement. */ + Assumes that parseProof() has just been called for this statement. + If verifyFlag includes VERIFY_DVS, check for unused $d conditions on nondummy + variables. + If verifyFlag includes VERIFY_DUMMY_DVS, check for all unused $d conditions. + If verifyFlag includes VERIFY_ESSENTIAL, check for unused $e statements. + If verifyFlag includes VERIFY_FLOATING, check for unused $f statements. */ /* Returns 0 if proof is OK; 1 if proof is incomplete (has '?' tokens); returns 2 if error found; returns 3 if not severe error found; returns 4 if not a $p statement */ -char verifyProof(long statemNum) +char verifyProof(long statemNum, flag verifyFlag) { long stmt; /* Contents of proof string location */ @@ -38,6 +43,9 @@ char verifyProof(long statemNum) nmbrString_def(bigSubstInstHyp); flag unkHypFlag; nmbrString_def(nmbrTmp); /* Used to force tmp stack dealloc */ + nmbrString_def(djRVar); /* Check use of required $d conditions */ + nmbrString_def(djOVar); /* Check use of optional $d conditions */ + nmbrString_def(essVar); /* Check use of $e statements */ if (g_Statement[statemNum].type != p_) return (4); /* Do nothing if not $p */ @@ -54,6 +62,31 @@ char verifyProof(long statemNum) if (g_WrkProof.numSteps == 0) return (2); /* Empty proof caused by error found by in parseProof */ + if (verifyFlag & VERIFY_DVS) { + nmbrLet(&djRVar, nmbrSpace(nmbrLen(g_Statement[statemNum].reqDisjVarsA))); + if (verifyFlag & VERIFY_DUMMY_DVS) { + nmbrLet(&djOVar, nmbrSpace(nmbrLen(g_Statement[statemNum].optDisjVarsA))); + } + } + + if (verifyFlag & (VERIFY_ESSENTIAL | VERIFY_FLOATING)) { + nmbrLet(&essVar, nmbrSpace(g_Statement[statemNum].numReqHyp)); + if (!(verifyFlag & VERIFY_ESSENTIAL)) { + for (i = 0; i < g_Statement[statemNum].numReqHyp; i++) { + if (g_Statement[g_Statement[statemNum].reqHypList[i]].type == e_) { + essVar[i] = 1; + } + } + } + if (!(verifyFlag & VERIFY_FLOATING)) { + for (i = 0; i < g_Statement[statemNum].numReqHyp; i++) { + if (g_Statement[g_Statement[statemNum].reqHypList[i]].type == f_) { + essVar[i] = 1; + } + } + } + } + for (step = 0; step < g_WrkProof.numSteps; step++) { stmt = g_WrkProof.proofString[step]; @@ -103,6 +136,14 @@ char verifyProof(long statemNum) g_WrkProof.mathStringPtrs[step] = g_Statement[stmt].mathString; + if (verifyFlag & VERIFY_ESSENTIAL) { + for (i = 0; i < g_Statement[statemNum].numReqHyp; i++) { + if (stmt == g_Statement[statemNum].reqHypList[i]) { + essVar[i] = 1; + } + } + } + continue; } @@ -168,7 +209,8 @@ char verifyProof(long statemNum) (due to proof being debugged or previous error) we will try to unify anyway; if the result is unique, we will use it. */ nmbrTmpPtr = assignVar(bigSubstSchemeHyp, - bigSubstInstHyp, stmt, statemNum, step, unkHypFlag); + bigSubstInstHyp, stmt, statemNum, step, unkHypFlag, + verifyFlag, djRVar, djOVar); /*E*/if(db7)printLongLine(cat("step ", str((double)step+1), " res ", /*E*/ nmbrCvtMToVString(nmbrTmpPtr), NULL), "", " "); @@ -216,8 +258,68 @@ char verifyProof(long statemNum) } g_WrkProof.errorCount++; } + + /* Check whether all of the $d conditions were used. */ + if (verifyFlag & VERIFY_DVS) { + flag warningPrinted = 0; + nmbrString *nmbrTmpPtrAS = g_Statement[statemNum].reqDisjVarsA; + nmbrString *nmbrTmpPtrBS = g_Statement[statemNum].reqDisjVarsB; + long dLen = nmbrLen(nmbrTmpPtrAS); + for (i = 0; i < dLen; i++) { + if (djRVar[i] == 0) { + if (warningPrinted == 0) { + warningPrinted = 1; + printLongLine(cat("Statement ", g_Statement[statemNum].labelName, + " has unused $d conditions: ", NULL), "", " "); + } + printLongLine(cat("$d ", + g_MathToken[nmbrTmpPtrAS[i]].tokenName, + " ", + g_MathToken[nmbrTmpPtrBS[i]].tokenName, + " $. ", NULL), "", " "); + } + } + if (verifyFlag & VERIFY_DUMMY_DVS) { + nmbrTmpPtrAS = g_Statement[statemNum].optDisjVarsA; + nmbrTmpPtrBS = g_Statement[statemNum].optDisjVarsB; + dLen = nmbrLen(nmbrTmpPtrAS); + for (i = 0; i < dLen; i++) { + if (djOVar[i] == 0) { + if (warningPrinted == 0) { + warningPrinted = 1; + printLongLine(cat("Statement ", g_Statement[statemNum].labelName, + " has unused $d conditions: ", NULL), "", " "); + } + printLongLine(cat("$d ", + g_MathToken[nmbrTmpPtrAS[i]].tokenName, + " ", + g_MathToken[nmbrTmpPtrBS[i]].tokenName, + " $. ", NULL), "", " "); + } + } + } + } + + /* Check whether all of the $e statements were used. */ + if (verifyFlag & (VERIFY_ESSENTIAL | VERIFY_FLOATING)) { + flag warningPrinted = 0; + for (i = 0; i < g_Statement[statemNum].numReqHyp; i++) { + if (essVar[i] == 0) { + if (warningPrinted == 0) { + warningPrinted = 1; + printLongLine(cat("Statement ", g_Statement[statemNum].labelName, + " has unused hypotheses: ", NULL), "", " "); + } + printLongLine(g_Statement[g_Statement[statemNum].reqHypList[i]].labelName, + "", " "); + } + } + } } + free_nmbrString(essVar); + free_nmbrString(djRVar); + free_nmbrString(djOVar); free_nmbrString(bigSubstSchemeHyp); free_nmbrString(bigSubstInstHyp); @@ -233,7 +335,9 @@ char verifyProof(long statemNum) nmbrString *assignVar(nmbrString *bigSubstSchemeAss, nmbrString *bigSubstInstAss, long substScheme, /* For error messages: */ - long statementNum, long step, flag unkHypFlag) + long statementNum, long step, flag unkHypFlag, + /* For unused distinct variable checking: */ + flag verifyFlag, nmbrString *djRVar, nmbrString *djOVar) { nmbrString_def(bigSubstSchemeVars); nmbrString_def(substSchemeFrstVarOcc); @@ -705,6 +809,8 @@ nmbrString *assignVar(nmbrString *bigSubstSchemeAss, if (nmbrTmpPtrAIR[i] == aToken2) { if (nmbrTmpPtrBIR[i] == bToken2) { foundFlag = 1; + if (verifyFlag & VERIFY_DVS) + djRVar[i] = 1; break; } } @@ -716,6 +822,8 @@ nmbrString *assignVar(nmbrString *bigSubstSchemeAss, if (nmbrTmpPtrAIO[i] == aToken2) { if (nmbrTmpPtrBIO[i] == bToken2) { foundFlag = 1; + if (verifyFlag & VERIFY_DUMMY_DVS) + djOVar[i] = 1; break; } } diff --git a/src/mmveri.h b/src/mmveri.h index 7aebfc43..f349d869 100644 --- a/src/mmveri.h +++ b/src/mmveri.h @@ -11,14 +11,24 @@ #include "mmdata.h" -char verifyProof(long statemNum); +/* Flags for verifyProof */ +#define VERIFY_NONE 0 +#define VERIFY_FULL 1 +#define VERIFY_DVS 2 +#define VERIFY_DUMMY_DVS 4 +#define VERIFY_ESSENTIAL 8 +#define VERIFY_FLOATING 16 + +char verifyProof(long statemNum, flag verifyFlag); /*! assignVar() finds an assignment to substScheme variables that match the assumptions specified in the reason string */ nmbrString *assignVar(nmbrString *bigSubstSchemeAss, nmbrString *bigSubstInstAss, long substScheme, /* For error messages: */ - long statementNum, long step, flag unkHypFlag); + long statementNum, long step, flag unkHypFlag, + /* For checking for unused $d conditions: */ + flag verifyFlag, nmbrString *djRVar, nmbrString *djOVar); /*! Deallocate the math symbol strings assigned in g_WrkProof structure during proof verification. This should be called after verifyProof() and after the