From 9b14a9d3cf563093b264875fb185cea39e422baf Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sun, 31 Dec 2023 17:34:15 -0700 Subject: [PATCH] Add hypothesis and dv usage qualifiers to VERIFY PROOF /DISJOINT_VARS checks for unused non-dummy dvs /ALL_DISJOINT_VARS check for all unused dvs /ESSENTIAL checks for unused $e statements --- src/metamath.c | 22 ++++++---- src/mmcmdl.c | 2 +- src/mmcmds.c | 8 ++-- src/mmcmds.h | 13 +++++- src/mmhlpb.c | 10 ++++- src/mmveri.c | 109 ++++++++++++++++++++++++++++++++++++++++++++++--- src/mmveri.h | 61 +++++++++++++++++++++++++-- 7 files changed, 199 insertions(+), 26 deletions(-) diff --git a/src/metamath.c b/src/metamath.c index cb2199b2..6df17aa2 100644 --- a/src/metamath.c +++ b/src/metamath.c @@ -2063,9 +2063,9 @@ void command(int argc, char *argv[]) { readInput(); if (switchPos("VERIFY")) { - verifyProofs("*",1); // Parse and verify + verifyProofs("*",1,0); // Parse and verify } else { - // verifyProofs("*",0); // Parse only (for gross error checking) + // verifyProofs("*",0,0); // Parse only (for gross error checking) } if (g_sourceHasBeenRead == 1) { @@ -4064,7 +4064,7 @@ void command(int argc, char *argv[]) { parseProof(g_proveStatement); // Necessary to set RPN stack ptrs before calling cleanWrkProof(). - verifyProof(g_proveStatement); + verifyProof(g_proveStatement, 0); if (g_WrkProof.errorSeverity > 1) { print2( "The starting proof has a severe error. It will not be used.\n"); @@ -5354,7 +5354,7 @@ void command(int argc, char *argv[]) { parseProof(g_proveStatement); // Must be called even if error occurred in parseProof, // to init RPN stack for cleanWrkProof(). - verifyProof(g_proveStatement); + verifyProof(g_proveStatement, 0); // don't change proof if there is an error // (which could be pre-existing). i = (g_WrkProof.errorSeverity > 1); @@ -6313,11 +6313,15 @@ 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"); + j = 0; + if (switchPos("DISJOINT_VARS")) + j |= UNUSED_DVS; + if (switchPos("ALL_DISJOINT_VARS")) + j |= UNUSED_DVS | UNUSED_DUMMY_DVS; + if (switchPos("ESSENTIAL")) + j |= UNUSED_ESSENTIAL; + verifyProofs(g_fullArg[2], (flag)i, (flag)j); continue; } diff --git a/src/mmcmdl.c b/src/mmcmdl.c index 476a4233..299b6319 100644 --- a/src/mmcmdl.c +++ b/src/mmcmdl.c @@ -1192,7 +1192,7 @@ flag processCommandLine(void) { if (lastArgMatches("/")) { i++; if (!getFullArg(i, cat( - "SYNTAX_ONLY", + "SYNTAX_ONLY|DISJOINT_VARS|ALL_DISJOINT_VARS|ESSENTIAL", "|", NULL))) goto pclbad; } else { diff --git a/src/mmcmds.c b/src/mmcmds.c index 48446244..237d9ada 100644 --- a/src/mmcmds.c +++ b/src/mmcmds.c @@ -1408,7 +1408,7 @@ void typeProof(long statemNum, } return; // verifyProof() could crash } - verifyProof(g_showStatement); + verifyProof(g_showStatement, 0); } nmbrString_def(proof); @@ -2287,7 +2287,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, 0); nmbrLet(&proof, g_WrkProof.proofString); // The proof plen = nmbrLen(proof); @@ -4588,7 +4588,7 @@ void eraseSource(void) // ERASE command // If verify = 0, parse the proofs only for gross error checking. // If verify = 1, do the full verification. -void verifyProofs(vstring labelMatch, flag verifyFlag) { +void verifyProofs(vstring labelMatch, flag verifyFlag, flag unusedFlag) { vstring_def(emptyProofList); long i, k; long lineLen = 0; @@ -4637,7 +4637,7 @@ void verifyProofs(vstring labelMatch, flag verifyFlag) { if (k >= 2) errorFound = 1; if (k < 2) { // $p with no error if (verifyFlag) { - if (verifyProof(i) >= 2) errorFound = 1; + if (verifyProof(i, unusedFlag) >= 2) errorFound = 1; cleanWrkProof(); // Deallocate verifyProof storage } } diff --git a/src/mmcmds.h b/src/mmcmds.h index d1b2974e..544dd305 100644 --- a/src/mmcmds.h +++ b/src/mmcmds.h @@ -84,7 +84,18 @@ void fixUndefinedLabels(vstring extractNeeded, vstring *buf); void writeDict(void); void eraseSource(void); -void verifyProofs(vstring labelMatch, flag verifyFlag); + +/*! Verify proofs. + * \param labelMatch pattern matching names to verify + * \param verifyFlag 0 to parse the proofs only for gross error checking, + * 1 to do the full verification + * \param unusedFlag bitwise OR of \c UNUSED_* flags. If \c verifyFlag + * includes: + * - \c UNUSED_DVS: check for unused \c $d conditions on nondummy variables + * - \c VERIFY_DUMMY_DVS: check for all unused \c $d conditions + * - \c VERIFY_ESSENTIAL: check for unused \c $e statements + */ +void verifyProofs(vstring labelMatch, flag verifyFlag, flag unusedFlag); /*! If checkFiles = 0, do not open external files. If checkFiles = 1, check for presence of gifs and biblio file */ diff --git a/src/mmhlpb.c b/src/mmhlpb.c index 86e89e54..d5cf5bf9 100644 --- a/src/mmhlpb.c +++ b/src/mmhlpb.c @@ -627,7 +627,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]"); H(""); H("This command verifies the proofs of the specified statements."); H(" may contain * and ? wildcard characters to verify more than"); @@ -636,10 +637,15 @@ 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(""); 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 792740ff..db37a2eb 100644 --- a/src/mmveri.c +++ b/src/mmveri.c @@ -20,9 +20,9 @@ struct getStep_struct getStep = {0, 0, 0, 0, 0, // Verify proof of one statement in source file. Uses wrkProof structure. // Assumes that parseProof() has just been called for this statement. // 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) { +// returns 2 if error found; returns 3 if severe error found; +// returns 4 if not a $p statement. +char verifyProof(long statemNum, flag unusedFlag) { if (g_Statement[statemNum].type != p_) return 4; // Do nothing if not $p // Initialize pointers to math strings in RPN stack and vs. statement. @@ -39,6 +39,30 @@ char verifyProof(long statemNum) { nmbrString_def(bigSubstSchemeHyp); nmbrString_def(bigSubstInstHyp); + // The following 3 number strings contain only 0 or 1, where 0 indicates an + // unused element, and 1 a used element. + nmbrString_def(djRVar); /* Used when checking required $d conditions */ + nmbrString_def(djOVar); /* Used when checking optional $d conditions */ + nmbrString_def(essVar); /* Used when checking $e or $f statements */ + + if (unusedFlag & UNUSED_DVS) { + nmbrLet(&djRVar, nmbrSpace(nmbrLen(g_Statement[statemNum].reqDisjVarsA))); + if (unusedFlag & UNUSED_DUMMY_DVS) { + nmbrLet(&djOVar, nmbrSpace(nmbrLen(g_Statement[statemNum].optDisjVarsA))); + } + } + + // If checking for unused essential hypotheses, mark all floating hypotheses + // as used. + if (unusedFlag & UNUSED_ESSENTIAL) { + nmbrLet(&essVar, nmbrSpace(g_Statement[statemNum].numReqHyp)); + for (long i = 0; i < g_Statement[statemNum].numReqHyp; i++) { + if (g_Statement[g_Statement[statemNum].reqHypList[i]].type == f_) { + essVar[i] = 1; + } + } + } + char returnFlag = 0; for (long step = 0; step < g_WrkProof.numSteps; step++) { long stmt = g_WrkProof.proofString[step]; // Contents of proof string location @@ -88,6 +112,14 @@ char verifyProof(long statemNum) { g_WrkProof.mathStringPtrs[step] = g_Statement[stmt].mathString; + if (unusedFlag & UNUSED_ESSENTIAL) { + for (long i = 0; i < g_Statement[statemNum].numReqHyp; i++) { + if (stmt == g_Statement[statemNum].reqHypList[i]) { + essVar[i] = 1; + } + } + } + continue; } @@ -152,7 +184,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. nmbrString *nmbrTmpPtr = assignVar(bigSubstSchemeHyp, - bigSubstInstHyp, stmt, statemNum, step, unkHypFlag); + bigSubstInstHyp, stmt, statemNum, step, unkHypFlag, + unusedFlag, djRVar, djOVar); /*E*/if(db7)printLongLine(cat("step ", str((double)step+1), " res ", /*E*/ nmbrCvtMToVString(nmbrTmpPtr), NULL), "", " "); @@ -196,8 +229,68 @@ char verifyProof(long statemNum) { } g_WrkProof.errorCount++; } + + /* Check whether all of the $d conditions were used. */ + if (unusedFlag & UNUSED_DVS) { + flag warningPrinted = 0; + nmbrString *nmbrTmpPtrAS = g_Statement[statemNum].reqDisjVarsA; + nmbrString *nmbrTmpPtrBS = g_Statement[statemNum].reqDisjVarsB; + long dLen = nmbrLen(nmbrTmpPtrAS); + for (long 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 (unusedFlag & UNUSED_DUMMY_DVS) { + nmbrTmpPtrAS = g_Statement[statemNum].optDisjVarsA; + nmbrTmpPtrBS = g_Statement[statemNum].optDisjVarsB; + dLen = nmbrLen(nmbrTmpPtrAS); + for (long 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 (unusedFlag & UNUSED_ESSENTIAL) { + flag warningPrinted = 0; + for (long 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 essential 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); @@ -209,7 +302,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 unusedFlag, nmbrString *djRVar, nmbrString *djOVar) { nmbrString_def(result); // value returned nmbrString_def(bigSubstSchemeVars); @@ -635,6 +730,8 @@ nmbrString *assignVar(nmbrString *bigSubstSchemeAss, if (nmbrTmpPtrAIR[i] == aToken2) { if (nmbrTmpPtrBIR[i] == bToken2) { foundFlag = 1; + if (unusedFlag & UNUSED_DVS) + djRVar[i] = 1; break; } } @@ -646,6 +743,8 @@ nmbrString *assignVar(nmbrString *bigSubstSchemeAss, if (nmbrTmpPtrAIO[i] == aToken2) { if (nmbrTmpPtrBIO[i] == bToken2) { foundFlag = 1; + if (unusedFlag & UNUSED_DUMMY_DVS) + djOVar[i] = 1; break; } } diff --git a/src/mmveri.h b/src/mmveri.h index a32a9823..31bac127 100644 --- a/src/mmveri.h +++ b/src/mmveri.h @@ -11,14 +11,67 @@ #include "mmdata.h" -char verifyProof(long statemNum); +/* Flags for verifyProof */ +/*! Check that non-dummy distinct variable conditions ($d) are used. */ +#define UNUSED_DVS 1 +/*! Check that all distinct variable conditions ($d) are used. */ +#define UNUSED_DUMMY_DVS 2 +/*! Check that all essential hypotheses ($e) are used. */ +#define UNUSED_ESSENTIAL 4 -/*! assignVar() finds an assignment to substScheme variables that match - the assumptions specified in the reason string */ +/*! Verify proof of one statement in a source file. + * \param[in] statemNum number of the statement to verify + * \param[in] unusedFlag bitwise OR of \c UNUSED_* flags. If \c unusedFlag + * includes: + * - \c UNUSED_DVS: check for unused \c $d conditions on nondummy variables + * - \c UNUSED_DUMMY_DVS: check for all unused \c $d conditions + * - \c UNUSED_ESSENTIAL: check for unused \c $e statements + * \return + * - 0 if proof is OK + * - 1 if proof is incomplete (has '?' tokens) + * - 2 if error found + * - 3 if severe error found + * - 4 if not a $p statement + * \pre parseProof() must have already been called for the statement + */ +char verifyProof(long statemNum, flag unusedFlag); + +/*! Find an assignment to substScheme variables that match the assumptions + specified in the reason string + * \param[in] bigSubstSchemAss the hypotheses the scheme + * \param[in] bigSubstInstAss the instance hypotheses + * \param[in] substScheme number of the statement to use for substitution + * \param[in] statementNum number of the statement being verified + * \param[in] step number of the proof step being verified + * \param[in] unkHypFlag nonzero if there are unknown hypotheses, zero otherwise + * \param[in] unusedFlag bitwise OR of \c UNUSED_* flags; e.g., + * UNUSED_DVS|UNUSED_DUMMY_DVS + * \param[out] djRVar array with one element per non-dummy distinct variable + * condition, used to mark those that are used + * \param[out] djOVar array with one element per dummy distinct variable + * condition, used to mark those that are used + * \pre if \c UNUSED_DVS is set in \c unusedFlag, then the length of \c djRVar + * is at least as great as the length of + * \c g_Statement[statemNum].reqDisjVarsA and contains all zeroes + * \pre if \c UNUSED_DUMMY_DVS is set in \c unusedFlag, then the length of + * \c djOVar is at least as great as the length of + * \c g_Statement[statemNum].optDisjVarsA and contains all zeroes + * \post if \c UNUSED_DVS is set in \c unusedFlag, then for every integer \c i + * such that the variables \c g_Statement[statementNum].reqDisjVarsA[i] + * and \c g_Statement[statementNum].reqDisjVarsB[i] were checked for + * distinctness, \c djRVar[i] is nonzero + * \post if \c UNUSED_DUMMY_DVS is set in \c unusedFlag, then for every integer + * \c i such that the variables + * \c g_Statement[statementNum].optDisjVarsA[i] and + * \c g_Statement[statementNum].optDisjVarsB[i] were checked for + * distinctness, \c djOVar[i] is nonzero + */ 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 unusedFlag, 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