Skip to content

Commit

Permalink
Add hypothesis and dv usage qualifiers to VERIFY PROOF
Browse files Browse the repository at this point in the history 
/DISJOINT_VARS checks for unused non-dummy dvs
/ALL_DISJOINT_VARS check for all unused dvs
/ESSENTIAL checks for unused $e statements
  • Loading branch information
@jamesjer
jamesjer committed Jan 3, 2024
1 parent 8fedf16 commit 9b14a9d
Show file tree
Hide file tree
Showing 7 changed files with 199 additions and 26 deletions.
22 changes: 13 additions & 9 deletions src/metamath.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -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");
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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;
}

Expand Down
2 changes: 1 addition & 1 deletion src/mmcmdl.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1192,7 +1192,7 @@ flag processCommandLine(void) {
if (lastArgMatches("/")) {
i++;
if (!getFullArg(i, cat(
"SYNTAX_ONLY",
"SYNTAX_ONLY|DISJOINT_VARS|ALL_DISJOINT_VARS|ESSENTIAL",
"|<SYNTAX_ONLY>", NULL)))
goto pclbad;
} else {
Expand Down
8 changes: 4 additions & 4 deletions src/mmcmds.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1408,7 +1408,7 @@ void typeProof(long statemNum,
}
return; // verifyProof() could crash
}
verifyProof(g_showStatement);
verifyProof(g_showStatement, 0);
}

nmbrString_def(proof);
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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
}
}
Expand Down
13 changes: 12 additions & 1 deletion src/mmcmds.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 */
Expand Down
10 changes: 8 additions & 2 deletions src/mmhlpb.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -627,7 +627,8 @@ H("");
}

if (!strcmp(saveHelpCmd, "HELP VERIFY PROOF")) {
H("Syntax: VERIFY PROOF <label-match> [/ SYNTAX_ONLY]");
H("Syntax: VERIFY PROOF <label-match> [/ SYNTAX_ONLY] [/DISJOINT_VARS]");
H(" [/ALL_DISJOINT_VARS] [/ESSENTIAL]");
H("");
H("This command verifies the proofs of the specified statements.");
H("<label-match> may contain * and ? wildcard characters to verify more than");
Expand All @@ -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");
Expand Down
109 changes: 104 additions & 5 deletions src/mmveri.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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
Expand Down Expand Up @@ -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;
}

Expand Down Expand Up @@ -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), "", " ");

Expand Down Expand Up @@ -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);

Expand All @@ -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);
Expand Down Expand Up @@ -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;
}
}
Expand All @@ -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;
}
}
Expand Down
61 changes: 57 additions & 4 deletions src/mmveri.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.,
* <tt>UNUSED_DVS|UNUSED_DUMMY_DVS</tt>
* \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
Expand Down

0 comments on commit 9b14a9d

Please sign in to comment.