Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add hypothesis and dv usage qualifiers to VERIFY PROOF #92

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Add hypothesis and dv usage qualifiers to VERIFY PROOF #92

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 13 additions & 9 deletions src/metamath.c
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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,
"", " ");
}
}
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indentation is out of order?

}
}

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
Open in desktop
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 */
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

When declaring new constants, comment their semantics at this point. All development environments I know of will automatically look up that lines and present an excerpt to the developer on request.

/*! 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
Loading