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
- /FLOATING checks for unused $f statements
- /HYPOTHESES is /ESSENTIAL and /FLOATING combined
  • Loading branch information
@jamesjer
jamesjer committed Jun 27, 2022
1 parent adb9bec commit a7b6967
Show file tree
Hide file tree
Showing 6 changed files with 171 additions and 33 deletions.
31 changes: 19 additions & 12 deletions src/metamath.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -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");
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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;
}

Expand Down
4 changes: 2 additions & 2 deletions src/mmcmdl.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1206,8 +1206,8 @@ flag processCommandLine(void) {
if (lastArgMatches("/")) {
i++;
if (!getFullArg(i, cat(
"SYNTAX_ONLY",
"|<SYNTAX_ONLY>", NULL)))
"SYNTAX_ONLY|DISJOINT_VARS|ALL_DISJOINT_VARS",
"|ESSENTIAL|FLOATING|HYPOTHESES|<SYNTAX_ONLY>", NULL)))
goto pclbad;
} else {
break;
Expand Down
27 changes: 16 additions & 11 deletions src/mmcmds.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1491,7 +1491,7 @@ void typeProof(long statemNum,
}
return; /* verifyProof() could crash */
}
verifyProof(g_showStatement);
verifyProof(g_showStatement, VERIFY_NONE);
}

if (!pipFlag) {
Expand Down Expand Up @@ -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 */
Expand Down Expand Up @@ -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;
Expand All @@ -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);
Expand All @@ -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++;
Expand All @@ -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) {
Expand All @@ -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 */
}
}
Expand All @@ -4738,7 +4743,7 @@ void verifyProofs(vstring labelMatch, flag verifyFlag) {
NULL));
}
}
if (verifyFlag) {
if (verifyFlag & VERIFY_FULL) {
print2("\n");
}

Expand All @@ -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));
Expand Down
12 changes: 10 additions & 2 deletions src/mmhlpb.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -648,7 +648,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] [/FLOATING] [/HYPOTHESES]");
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 @@ -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");
Expand Down
116 changes: 112 additions & 4 deletions src/mmveri.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 */
Expand All @@ -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 */

Expand All @@ -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];
Expand Down Expand Up @@ -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;
}

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

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

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

0 comments on commit a7b6967

Please sign in to comment.