/*****************************************************************************/ /* Program name: metamath */ /* Copyright (C) 2021 NORMAN MEGILL nm at alum.mit.edu http://metamath.org */ /* License terms: GNU General Public License Version 2 or any later version */ /*****************************************************************************/ /*34567890123456 (79-character line to adjust editor window) 2345678901234567*/ /* Copyright notice: All code in this program that was written by Norman Megill is public domain. However, the project includes code contributions from other people which may be GPL licensed. For more details see: https://github.com/metamath/metamath-exe/issues/7#issuecomment-675555069 */ /* The overall functionality of the modules is as follows: metamath.c - Contains main(); executes or calls commands mmcmdl.c - Command line interpreter mmcmds.c - Extends metamath.c command() to execute SHOW and other commands; added after command() became too bloated (still is:) mmdata.c - Defines global data structures and manipulates arrays with functions similar to BASIC string functions; memory management; converts between proof formats mmhlpa.c - The help file, part 1. mmhlpb.c - The help file, part 2. mminou.c - Basic input and output interface mmmaci.c - THINK C Macintosh interface (obsolete) mmpars.c - Parses the source file mmpfas.c - Proof Assistant mmunif.c - Unification algorithm for Proof Assistant mmutil.c - Miscellaneous I/O utilities (reserved for future use) mmveri.c - Proof verifier for source file mmvstr.c - BASIC-like string functions mmwtex.c - LaTeX/HTML source generation mmword.c - File revision utility (for TOOLS> UPDATE) (not generally useful) */ /* Compilation instructions (gcc on Unix/Linus/Cygwin, lcc on Windows): 1. Make sure each .c file above is present in the compilation directory and that each .c file (except metamath.c) has its corresponding .h file present. 2. In the directory where these files are present, type: gcc m*.c -o metamath 3. For full error checking, use: gcc m*.c -o metamath -O2 -Wall -Wextra -Wmissing-prototypes \ -Wmissing-declarations -Wshadow -Wpointer-arith -Wcast-align \ -Wredundant-decls -Wnested-externs -Winline -Wno-long-long \ -Wconversion -Wstrict-prototypes -std=c99 -pedantic -Wunused-result Note: gcc 4.9.2 (on Debian) fails with "unknown type name `ssize_t'" if -std=c99 is used, so omit -std=c99 to work around this problem. 4. For faster runtime, use these gcc options: gcc m*.c -o metamath -O3 -funroll-loops -finline-functions \ -fomit-frame-pointer -Wall -std=c99 -pedantic -fno-strict-overflow 5. The Windows version in the download was compiled with lcc-win32 version 3.8: lc -O m*.c -o metamath.exe 6. On Linux, if you have autoconf, automake, and a C compiler, you can compile with the command "autoreconf -i && ./configure && make". See the README.TXT file for more information. */ #define MVERSION "0.198 7-Aug-2021" /* 0.198 nm 7-Aug-2021 mmpars.c - Fix cosmetic bug in WRITE SOURCE ... /REWRAP that prevented end of sentence (e.g. period) from appearing in column 79, thus causing some lines to be shorter than necessary. */ /* 0.197 nm 2-Aug-2021 mmpars.c - put two spaces between $c,v on same line in /rewrap; mmwtex.c mmhlpa.c mminou.c - minor edits */ /* 0.196 nm 31-Dec-2020 metamath.c mmpars.c - fix bug that deleted comments that were followed by ${, $}, $c, $v, $d on the same line */ /* 0.195 nm 30-Dec-2020 metamath.c - temporarily disable /REWRAP until bug fixed 27-Sep-2020 nm mmwtex.c - prevent "htmlexturl" links from wrapping */ /* 0.194 26-Dec-2020 nm mmwtex.c - add keyword "htmlexturl" to $t statement in .mm file */ /* 0.193 12-Sep-2020 nm mmcmds.c mmdata.c,h mmwtex.c,h mmhlpa.c - make the output of /EXTRACT stable in the sense that, with the same parameter, extract(extract(file)) = extract(file) except that the date stamp at the top will be updated. (The first extraction even if "*" will usually be different because it discards non-relevant content. Note that the include file directives "$( $[ Begin..." etc. and comments with "$j" are currently discarded.) */ /* 0.192 4-Sep-2020 nm metamath.c - fix bug */ /* 0.191 4-Sep-2020 nm metamath.c - add comment close */ /* 0.190 4-Sep-2020 nm mmcmds.c - fix bug in writeExtractedSource() */ /* 0.189 4-Sep-2020 nm mmhlpa.c - add help for WRITE SOURCE .. /EXTRACT ... 24-Aug-2020 nm metamath.c mmcmdl.c mmcmds.c,h mmdata.c,h mmhlpa.c mmpars.c mmpfas.c mmunif.c mmwtex.c,h - Added WRITE SOURCE ... /EXTRACT ... */ /* 0.188 23-Aug-2020 nm mmwtex.c, mmhlpa.c Added CONCLUSION FACT INTRODUCTION PARAGRAPH SCOLIA SCOLION SUBSECTION TABLE to [bib] keywords */ /* 0.187 15-Aug-2020 nm All m*.c, m*.h - put "g_" in front of all global variable names e.g. "statements" becomes "g_statements"; also capitalized 1st letter of original name in case of global structs e.g. "statement" becomes "g_Statement". 9-Aug-2020 nm mmcmdl.c, mmhlpa.c - add HELP BIBLIOGRAPHY */ /* 0.186 8-Aug-2020 nm mmwtex.c, mmhlpa.c - add CONJECTURE, RESULT to [bib] keywords 8-Aug-2020 nm mmpfas.c, metamath.c - print message when IMPROVE or MINIMIZE_WITH uses another mathbox */ /* 0.185 5-Aug-2020 nm metamath.c mmcmdl.c mmhlpb.c mmpfas.c,h mmcmds.c mmwtex.c,h - add /INCLUDE_MATHBOXES to to IMPROVE; notify user upon ASSIGN from another mathbox. 18-Jul-2020 nm mmcmds.c, mmdata.c, mmhlpb.c, metamath.c - "PROVE =" will now resume the previous MM-PA session if there was one; allow "~" to start/end with blank (meaning first/last statement); add "@1234" */ /* 0.184 17-Jul-2020 nm metamath.c mmcmdl.c mmcmds.c,h mmhlpb.c mmwtex.c,h - add checking for mathbox independence to VERIFY MARKUP; add /MATHBOX_SKIP 4-Jul-2020 nm mmwtex.c - correct error msg for missing althtmldef 3-Jul-2020 nm metamath.c, mmhlpa.c - allow space in TOOLS> BREAK */ /* 0.183 30-Jun-2020 30-Jun-2020 nm mmpars.c - refine prevention of WRITE SOURCE.../REWRAP from modifying comments containing "" (specifically, remove indentation alignment). 25-Jun-2020 nm metamath.c, mmcmds.c,h mmcmdl.c mmhlpb.c - add underscore checking in VERIFY MARKUP and add /UNDERSCORE_SKIP qualifier; also check for trailing space on lines. 20-Jun-2020 nm mmcmds.c - check for discouragement tags in *ALT, *OLD labels in VERIFY MARKUP. 19-Jun-2020 nm mminou.c,h, metamath.c, mmwtex.c - dynamically allocate buffer in print2() using vsnprintf() to calculate size needed 18-Jun-2020 nm mmpars.c - remove error check for $e <- $f assignments. See https://groups.google.com/d/msg/metamath/Cx_d84uorf8/0FrNYTM9BAAJ */ /* 0.182 12-Apr-2020 nm mmwtex.c, mmphlpa.c - add "Claim" to bib ref types */ /* 0.181 12-Feb-2020 nm (reported by David Starner) metamath.c - fix bug causing new axioms to be used by MINIMIZE_WITH */ /* 0.180 10-Dec-2019 nm (bj 13-Sep-2019) mmpars.c - fix "line 0" in error msg when label clashes with math symbol 8-Dec-2019 nm (bj 13-Oct-2019) mmhlpa.c - improve TOOLS> HELP INSERT, DELETE 8-Dec-2019 nm (bj 19-Sep-2019) mminou.c - change bug 1511 to error message 30-Nov-2019 nm (bj 12-Oct-2019) mmwtex.c - trigger Most Recent link on mmtheorems.html when there is a mathbox statement (currently set.mm and iset.mm). 30-Nov-2019 nm (bj 13-Sep-2019) mmhlpa.c - improve help for TOOLS> DELETE and SUBSTITUTE. 30-Nov-2019 nm (bj 13-Sep-2019) mmwtex.c - change "g_htmlHome" in warnings to "htmlhome". */ /* 0.179 29-Nov-2019 nm (bj 22-Sep-2019) metamath.c - MINIMIZE_WITH axiom trace now starts from current NEW_PROOF instead of SAVEd proof. 23-Nov-2019 nm (bj 4-Oct-2019) metamath.c - make sure traceback flags are cleared after MINIMIZE_WITH 20-Nov-2019 nm mmhlpa.c - add url pointer to HELP WRITE SOURCE /SPLIT 18-Nov-2019 nm mmhlpa.c - clarify HELP WRITE SOURCE /REWRAP 15-Oct-2019 nm mmdata.c - add bug check info for user 14-Oct-2019 nm mmcmds.c - use '|->' (not 'e.') as syntax hint for maps-to 14-Oct-2019 nm mmwtex.c - remove extraneous */ /* 0.178 10-Aug-2019 nm mminou.c - eliminate redundant fopen in fSafeOpen 6-Aug-2019 nm mmwtex.c,h, mmcmds.c - Add error check for >1 line section name or missing closing decoration line in getSectionHeadings() 4-Aug-2019 nm mmhlpb.c, mmcmdl.c, metamath.c - Add /ALLOW_NEW_AXIOMS, renamed /ALLOW_GROWTH to /MAY_GROW 17-Jul-2019 nm mmcmdl.c, mmhlpa.c, metamath.c - Add /NO_VERSIONING to WRITE THEOREM_LIST 17-Jul-2019 nm metamath.c - Change line of dashes between SHOW STATEMENT output from hardcoded 79 to current g_screenWidth */ /* 0.177 27-Apr-2019 nm mmcmds.c -"set" -> "setvar" in htmlAllowedSubst. mmhlpb.c - fix typos in HELP IMPROVE. */ /* 0.176 25-Mar-2019 nm metamath.c mmcmds.h mmcmds.c mmcmdl.c mmhlpb.c - add /TOP_DATE_SKIP to VERIFY MARKUP */ /* 0.175 8-Mar-2019 nm mmvstr.c - eliminate warning in gcc 8.3 (patch provided by David Starner) */ /* 0.174 22-Feb-2019 nm mmwtex.c - fix erroneous warning when using "[[" bracket escape in comment */ /* 0.173 3-Feb-2019 nm mmwtex.c - fix infinite loop when "[" was the first character in a comment */ /* 0.172 25-Jan-2019 nm mmwtex.c - comment out bug 2343 trap (not a bug) */ /* 0.171 13-Dec-2018 nm metamath.c, mmcmdl.c, mmhlpa.c, mmcmds.c,h, mmwtex.c,h - add fine-grained qualfiers to MARKUP command */ /* 0.170 12-Dec-2018 nm mmwtex.c - restore line accidentally deleted in 0.169 */ /* 0.169 10-Dec-2018 nm metamath.c, mmcmds.c,h, mmcmdl.c, mmpars.c, mmhlpa.c, mmwtex.c - Add MARKUP command. 9-Dec-2018 nm mmwtex.c - escape literal "[" with "[[" in comments. */ /* 0.168 8-Dec-2018 nm metamath.c - validate that /NO_REPEATED_STEPS is used only with /LEMMON. 8-Dec-2018 nm mmcmds.c - fix bug #256 reported by Jim Kingdon (https://github.com/metamath/set.mm/issues/497). */ /* 0.167 13-Nov-2018 nm mmcmds.c - SHOW TRACE_BACK .../COUNT now uses proof the way it's stored (previously, it always uncompressed the proof). The new step count (for compressed proofs) corresponds to the step count the user would see on the web pages. 12-Nov-2018 nm mmcmds.c - added unlimited precision arithmetic for SHOW TRACE_BACK .../COUNT/ESSENTIAL */ /* 0.166 31-Oct-2018 nm mmwtex.c - workaround Chrome anchor bug 30-Oct-2018 nm mmcmds.c - put "This theorem is referenced by" after axioms and definitions used in HTML; use "(None)" instead of suppressing line if nothing is referenced */ /* 0.165 20-Oct-2018 nm mmwtex.c - added ~ mmtheorems#abc type anchor in TOC details. mmwtex.c - fix bug (reported by Benoit Jubin) that changes "_" in labels to subscript. mmcmdl.c - remove unused COMPLETE qualifier from SHOW PROOF. mmwtex.c - enhance special cases of web page spacing identified by Benoit Jubin */ /* 0.164 5-Sep-2018 nm mmwtex.c, mmhlpb.c - added NOTE to bib keywords 14-Aug-2018 nm metamath.c - added defaultScrollMode to prevent SET SCROLL CONTINUOUS from reverting to PROMPTED after a SUBMIT command */ /* 0.163 4-Aug-2018 nm mmwtex.c - removed 2nd "sandbox:bighdr" anchor in mmtheorems.html; removed Firefox and IE references; changed breadcrumb font to be consistent with other pages; put asterisk next to TOC entries that have associated comments */ /* FOR FUTURE REFERENCE: search for "Thierry" in mmwtex.c to modify the link to tirix.org structured proof site */ /* 0.162-thierry 3-Jun-2018 nm mmwtex.c - add link to tirix.org structured proofs */ /* 0.162 3-Jun-2018 nm mmpars.c - re-enabled error check for $c not in outermost scope. mmhlpa.c mmhlpb.c- improve some help messages. mmwtex.c - added "OBSERVATION", "PROOF", AND "STATEMENT" keywords for WRITE BIBLIOGRAPHY */ /* 0.161 2-Feb-2018 nm mmpars.c,h mmcmds.c mmwtex.c - fix wrong file name and line number in error messages */ /* 0.160 24-Jan-2018 nm mmpars.c - fix bug introduced in version 0.158 */ /* 0.159 23-Jan-2018 nm mmpars.c - fix crash due to missing include file */ /* 0.158 22-Jan-2018 nm mminou.c - strip CRs from Windows SUBMIT files run on Linux */ /* 0.157 15-Jan-2018 nm Major rewrite of READ-related functions. Added HELP MARKUP. 9-Jan-2018 nm Track line numbers for error messages in included files 1-Jan-2018 nm Changed HOME_DIRECTORY to ROOT_DIRECTORY 31-Dec-2017 nm metamath.c mmcmdl.c,h mmpars.c,h mmcmds.c,h mminou.c,h mmwtex.c mmhlpb.c mmdata.h - add virtual includes "$( Begin $[...$] $)", $( End $[...$] $)", "$( Skip $[...$] $)" */ /* 0.156 8-Dec-2017 nm mmwtex.c - fix bug that incorrectly gave "verify markup" errors when there was a mathbox statement without an "extended" section */ /* 0.155 8-Oct-2017 nm mmcmdl.c - restore accidentally removed HELP HTML; mmhlpb.c mmwtex.c mmwtex.h,c mmcmds.c metamath.c - improve HELP and make other cosmetic changes per Benoit Jubin's suggestions */ /* 0.154 2-Oct-2017 nm mmunif.h,c mmcmds.c - add 2 more variables to ERASE; metamath.c mmcmdl.c - remove obsolete OPEN/CLOSE HTML; mmhlpa.c mmhlpb.c - fix typos reported by Benoit Jubin */ /* 0.153 1-Oct-2017 nm mmunif.c,h mmcmds.c - Re-initialize internal nmbrStrings in unify() after 'erase' command reported by Benoit Jubin */ /* 0.152 26-Sep-2017 nm mmcmds.c - change default links from mpegif to mpeuni; metamath.c - enforce minimum screen width = 3 to prevent crash reported by Benoit Jubin */ /* 0.151 20-Sep-2017 nm mmwtex.c - better matching to insert space between A and y in "E. x e. ran A y R x" to prevent spurious spaces in thms rncoeq, dfiun3g as reported by Benoit Jubin */ /* 0.150 26-Aug-2017 nm mmcmds.c,mmwtex.h - fix hyperlink for Distinct variable etc. lists so that it will point to mmset.html on other Explorers like NF. Move the "Dummy variables..." to print after the "Proof of Theorem..." line. */ /* 0.149 21-Aug-2017 nm mmwtex.c,h mmcmds.c mmhlpb.c - add a subsubsection "tiny" header with separator "-.-." to table of contents and theorem list; see HELP WRITE THEOREM_LIST 21-Aug-2017 nm mmcmds.c - remove bug check 255 19-Aug-2017 nm mmcmds.c - change mmset.html links to ../mpeuni/mmset.html so they will work in NF Explorer etc. */ /* 0.148 14-Aug-2017 nm mmcmds.c - hyperlink "Dummy variable(s)" */ /* 0.147 13-Aug-2017 nm mmcmds.c,h - add "Dummy variable x is distinct from all other variables." to proof web page */ /* 0.146 26-Jun-2017 nm mmwtex.c - fix handling of local labels in 'show proof.../tex' (bug 2341 reported by Eric Parfitt) */ /* 0.145 16-Jun-2017 nm metamath.c mmpars.c - fix bug 1741 during MINIMIZE_WITH; mmpfas.c - make duplicate bug numbers unique; mmhlpa.c mmhlpb.c - adjust to prevent lcc compiler "Function too big for the optimizer" 29-May-2017 nm mmwtex.c mmhlpa.c - take out extraneous ... markup tags in HTML output so w3c validator will pass */ /* 0.144 15-May-2017 nm metamath.c mmcmds.c - add "(Revised by..." tag for conversion of legacy .mm's if there is a 2nd date under the proof */ /* 0.143 14-May-2017 nm metamath.c mmdata.c,h mmcmdl.c mmcmds.c mmhlpb.c - added SET CONTRIBUTOR; for missing "(Contributed by..." use date below proof if it exists, otherwise use today's date, in order to update old .mm files. 14-May-2017 Ari Ferrera - mmcmds.c - fix memory leaks in ERASE */ /* 0.142 12-May-2017 nm metamath.c mmdata.c,h mmcmds.c - added "#define DATE_BELOW_PROOF" in mmdata.h that if uncommented, will enable use of the (soon-to-be obsolete) date below the proof 4-May-2017 Ari Ferrera - mmcmds.c metamath.c mmdata.c mmcmdl.c mminou.c mminou.h mmcmdl.h mmdata.h - fixed memory leaks and warnings found by valgrind. 3-May-2017 nm - metamath.c mmdata.c,h mmcmds.c,h mmpars.c,h mmhlpb.c mmcmdl.c mmwtex.c - added xxChanged flags to statement structure so that any part of the source can be changed; removed /CLEAN qualifier of WRITE SOURCE; automatically put "(Contributed by ?who?..." during SAVE NEW_PROOF or SAVE PROOF when it is missing; more VERIFY MARKUP checking. */ /* 0.141 2-May-2017 nm mmdata.c, metamath.c, mmcmds.c, mmhlpb.c - use getContrib() date for WRITE RECENT instead of date below proof. This lets us list recent $a's as well as $p's. Also, add caching to getContrib() for speedup. */ /* 0.140 1-May-2017 nm mmwtex.c, mmcmds.c, metamath.c - fix some LaTeX issues reported by Ari Ferrera */ /* 0.139 2-Jan-2017 nm metamath.c - print only one line for 'save proof * /compressed/fast' */ /* 0.138 26-Dec-2016 nm mmwtex.c - remove extraneous causing w3c validation failure; put space after 1st x in "F/ x x = x"; mmcmds.c - added checking for lines > 79 chars in VERIFY MARKUP; mmcmds.c, mmcmdl.c, metamath.c, mmhlpb.c, mmcmds.h - added /VERBOSE to VERIFY MARKUP */ /* 0.137 20-Dec-2016 nm mmcmds.c - check ax-XXX $a vs axXXX $p label convention in 'verify markup' 18-Dec-2016 nm mmwtex.c, mmpars.c, mmdata.h - use true "header area" between successive $a/$p for getSectionHeadings() mmcmds.c - add header comment checking 13-Dec-2016 nm mmdata.c,h - enhanced compareDates() to treat empty string as older date. 13-Dec-2016 nm metamath.c, mmcmds.c - moved mm* and Microsoft illegal file name label check to verifyMarkup() (the VERIFY MARKUP command) instead of checking on READ; added check of set.mm Version date to verifyMarkup(). 13-Dec-2016 nm mmwtex.c,h - don't treat bracketed description text with space as a bib label; add labelMatch parameter to writeBibliography() */ /* 0.136 10-Oct-2016 mminou.c - fix resource leak bug reported by David Binderman */ /* 0.135 11-Sep-2016, 14-Sep-2016 metamath.c, mmpfas.c,h, mmdata.c,h, mmpars.c,h mmcmds.c, mmcmdl.c, mmhlpb.c - added EXPAND command */ /* 0.134 16-Aug-2016 mmwtex.c - added breadcrumbs to theorem pages; metamath.c, mmcmdl.c, mmhlpb.c, mminou.c,.h - added /TIME to SAVE PROOF, SHOW STATEMENT.../[ALT}HTML, MINIMIZE_WITH */ /* 0.133 13-Aug-2016 mmwtex.c - improve mobile display with tag mmpars.c - use updated Macintosh information */ /* 0.132 10-Jul-2016 metamath.c, mmcmdl.c, mmcmds.c,.h, mmdata.c,.h, mmhlpb.c, mmpfas.c - change "restricted" to "discouraged" to match set.mm markup tags; add SET DISCOURAGEMENT OFF|ON (default ON) to turn off blocking for convenience of advanced users 6-Jul-2016 metamath.c - add "(void)" in front of "system(...)" to suppress -Wunused-result warning */ /* 0.131 10-Jun-2016 mminou.c - reverted change of 22-May-2016 because 'minimize_with' depends on error message in string to prevent DV violations. Todo: write a DV-checking routine for 'minimize_with', then revert the 22-May-2016 fix for bug 126 (which only occurs when writing web pages for .mm file with errors). 9-Jun-2016 mmcmdl.c, metamath.c - added _EXIT_PA for use with scripts that will give an error message outside of MM-PA> rather than exiting metamath */ /* 0.130 25-May-2016 mmpars.c - workaround clang warning about j = j; mmvstr.c - workaround gcc -Wstrict-overflow warning */ /* 0.129 24-May-2016 mmdata.c - fix bug 1393 */ /* 0.128 22-May-2016 mminou.c - fixed error message going to html page instead of to screen, triggering bug 126. */ /* 0.127 10-May-2016 metamath.c, mmcmdl.c, mmhlpb.c - added /OVERRIDE to PROVE */ /* 0.126 3-May-2016 metamath.c, mmdata.h, mmdata.c, mmcmds.h, mmcmds.c, mmcmdl.c, mmhlpb.c, mmpars.c - added getMarkupFlag() in mmdata.c; Added /OVERRIDE added to ASSIGN, REPLACE, IMPROVE, MINIMIZE_WITH, SAVE NEW_PROOF; PROVE gives warning about SAVE NEW_PROOF for locked proof. Added SHOW RESTRICTED command. 3-May-2016 m*.c - fix numerous conversion warnings provided by gcc 5.3.0 */ /* 0.125 10-Mar-2016 mmpars.c - fixed bug parsing /EXPLICIT/PACKED format 8-Mar-2016 nm mmdata.c - added "#nnn" to SHOW STATEMENT etc. to reference statement number e.g. SHOW STATEMENT #58 shows a1i in set.mm. 7-Mar-2016 nm mmwtex.c - added space between } and { in HTML output 6-Mar-2016 nm mmpars.c - disabled wrapping of formula lines in WRITE SOURCE.../REWRAP 2-Mar-2016 nm metamat.c, mmcmdl.c, mmhlpb.c - added /FAST to SAVE PROOF, SHOW PROOF */ /* 0.123 25-Jan-2016 nm mmpars.c, mmdata.h, mmdata.c, mmpfas.c, mmcmds., metamath.c, mmcmdl.c, mmwtex.c - unlocked SHOW PROOF.../PACKED, added SHOW PROOF.../EXPLICIT */ /* 0.122 14-Jan-2016 nm metamath.c, mmcmds.c, mmwtex.c, mmwtex.h - surrounded math HTML output with "...; added htmlcss and htmlfont $t commands 10-Jan-2016 nm mmwtex.c - delete duplicate -4px style; metamath.c - add   after char on mmascii.html 3-Jan-2016 nm mmwtex.c - fix bug when doing SHOW STATEMENT * /ALT_HTML after VERIFY MARKUP */ /* 0.121 17-Nov-2015 nm metamath.c, mmcmdl.h, mmcmdl.c, mmcmds.h, mmcmds.c, mmwtex.h, mmwtex.c, mmdata.h, mmdata.c - 1. Moved WRITE BIBLIOGRAPHY code from metamath.c to its own function in mmwtex.c; moved qsortStringCmp() from metamath.c to mmdata.c 2. Added $t, comment markup, and bibliography checking to VERIFY MARKUP 3. Added options to bug() bug-check interception to select aborting, stepping to next bug, or ignoring subsequent bugs 4. SHOW STATEMENT can now use both /HTML and /ALT_HTML in same session 5. Added /HTML, /ALT_HTML to WRITE THEOREM_LIST and WRITE RECENT_ADDITIONS */ /* 0.120 7-Nov-2015 nm metamath.c, mmcmdl.c, mmpars.c - add VERIFY MARKUP 4-Nov-2015 nm metamath.c, mmcmds.c/h, mmdata.c/h - move getDescription, getSourceIndentation from mmcmds.c to mmdata.c. metamath.c, mmdata.c - add and call parseDate() instead of in-line code; add getContrib(), getProofDate(), buildDate(), compareDates(). */ /* 0.119 18-Oct-2015 nm mmwtex.c - add summary TOC to Theorem List; improve math symbol GIF image alignment 2-Oct-2015 nm metamath.c, mmpfas.c, mmwtex.c - fix miscellaneous small bugs or quirks */ /* 0.118 18-Jul-2015 nm metamath.c, mmcmds.h, mmcmds.c, mmcmdl.c, mmhlpb.h, mmhlpb.c - added /TO qualifier to SHOW TRACE_BACK. See HELP SHOW TRACE_BACK. */ /* 0.117 30-May-2015 1. nm mmwtex.c - move of Theorem List pages */ /* 0.115 8-May-2015 nm mmwtex.c - added section header comments to WRITE THEOREM_LIST and broke out Table of Contents page 24-Apr-2015 nm metamath.c - add # bytes to end of "---Clip out the proof"; reverted to no blank lines there (see 0.113 item 3) */ /* 0.114 22-Apr-2015 nm mmcmds.c - put [-1], [-2],... offsets on 'show new_proof/unknown' */ /* 0.113 19-Apr-2015 so, nm metamath.c, mmdata.c 1. SHOW LABEL % will show statements with changed proofs 2. SHOW LABEL = will show the statement being proved in MM-PA 3. Added blank lines before, after "---------Clip out the proof" proof 4. Generate date only if the proof is complete */ /* 0.112 15-Apr-2015 nm metamath.c - fix bug 1121 (reported by S. O'Rear); mwtex.c - add "img { margin-bottom: -4px }" to CSS to align symbol GIFs; mwtex.c - remove some hard coding for set.mm, for use with new nf.mm; metamath.c - fix comment parsing in WRITE BIBLIOGRAPHY to ignore math symbols */ /* 0.111 22-Nov-2014 nm metamath.c, mmcmds.c, mmcmdl.c, mmhlpb.c - added /NO_NEW_AXIOMS_FROM qualifier to MINIMIZE_WITH; see HELP MINIMIZE_WITH. 21-Nov-2014 Stepan O'Rear mmdata.c, mmhlpb.c - added ~ label range specifier to wildcards; see HELP SEARCH */ /* 0.110 2-Nov-2014 nm mmcmds.c - fixed bug 1114 (reported by Stefan O'Rear); metamath.c, mmhlpb.c - added "SHOW STATEMENT =" to show the statement being proved in MM-PA (based on patch submitted by Stefan O'Rear) */ /* 0.109 20-Aug-2014 nm mmwtex.c - fix corrupted HTML caused by misinterpreting math symbols as comment markup (math symbols with _ [ ] or ~). Also, allow https:// as well as http:// in ~ label markup. 11-Jul-2014 wl mmdata.c - fix obscure crash in debugging mode db9 */ /* 0.108 25-Jun-2014 nm (1) metamath.c, mmcmdl.c, mmhlpb.c - MINIMIZE_WITH now checks the size of the compressed proof, prevents $d violations, and tries forward and reverse statment scanning order; /NO_DISTINCT, /BRIEF, /REVERSE qualifiers were removed. (2) mminou.c - prevent hard breaks (in the middle of a word) in too-long lines (e.g. long URLs) in WRITE SOURCE .../REWRAP; just overflow the screen width instead. (3) mmpfas.c - fixed memory leak in replaceStatement() (4) mmpfas.c - suppress inf. growth with MINIMIZE_WITH idi/ALLOW_GROWTH */ /* 0.107 21-Jun-2014 nm metamath.c, mmcmdl.c, mmhlpb.c - added /SIZE qualifier to SHOW PROOF; added SHOW ELAPSED_TIME; mmwtex.c - reformatted WRITE THEOREM_LIST output; now "$(", newline, "######" starts a "part" */ /* 0.106 30-Mar-2014 nm mmwtex.c - fix bug introduced by 0.105 that disabled hyperlinks on literature refs in HTML comment. metamath.c - improve messages */ /* 0.105 15-Feb-2014 nm mmwtex.c - prevented illegal LaTeX output for certain special characters in comments. */ /* 0.104 14-Feb-2014 nm mmwtex.c - fixed bug 2312, mmcmds.c - enhanced ASSIGN error message. */ /* 0.103 4-Jan-2014 nm mmcmds.c,h - added "Allowed substitution hints" below the "Distinct variable groups" list on generated web pages mmwtex.c - added "*" to indicate DV's occur in Statement List entries. */ /* 0.102 2-Jan-2014 nm mminou.c - made compressed proof line wrapping more uniform at start of compressed part of proof */ /* 0.101 27-Dec-2013 nm mmdata.h,c, mminou.c, mmcmdl.c, mmhlpb.c, mmvstr.c - Improved storage efficiency of /COMPRESSED proofs (but with 20% slower run time); added /OLD_COMPRESSION to specify old algorithm; removed end-of-line space after label list in old algorithm; fixed linput() bug */ /* 0.100 30-Nov-2013 nm mmpfas.c - reversed statement scan order in proveFloating(), to speed up SHOW STATEMENT df-* /HTML; metamath.c - remove the unknown date place holder in SAVE NEW_PROOF; Wolf Lammen mmvstr.c - some cleanup */ /* 0.07.99 1-Nov-2013 nm metamath.c, mmpfas.h,c, mmcmdl.h,c, mmhlpa.c, mmhlpb.c - added UNDO, REDO, SET UNDO commands (see HELP UNDO) */ /* 0.07.98 30-Oct-2013 Wolf Lammen mmvstr.c,h, mmiou.c, mmpars.c, mmdata.c - improve code style and program structure */ /* 0.07.97 20-Oct-2013 Wolf Lammen mmvstr.c,h, metamath.c - improved linput(); nm mmcmds.c, mmdata.c - tolerate bad proofs in SHOW TRACE_BACK etc. */ /* 0.07.96 20-Sep-2013 Wolf Lammen mmvstr.c - revised cat(); nm mmwtex.c, mminou.c - change a print2 to printLongLine to fix bug 1150 */ /* 0.07.95 18-Sep-2013 Wolf Lammen mmvstr.c - optimized cat(); nm metamath.c, mmcmds.c, mmdata.c, mmpars.c, mmpfas.c, mmvstr.c, mmwtex.c - suppress some clang warnings */ /* 0.07.94 28-Aug-2013 Alexey Merkulov mmcmds.c, mmpars.c - fixed several memory leaks found by valgrind --leak-check=full --show-possibly-lost=no */ /* 0.07.93 8-Jul-2013 Wolf Lammen mmvstr.c - simplified let() function; also many minor changes in m*.c and m*.h to assist future refactoring */ /* 0.07.92 28-Jun-2013 nm metamath.c mmcmds.c,h mmcmdl.c mmhlpb.c- added /NO_REPEATED_STEPS for /LEMMON mode of SHOW PROOF, SHOW NEW_PROOF. This reverts the /LEMMON mode default display change of 31-Jan-2010 and invokes it when desired via /NO_REPEATED_STEPS. */ /* 0.07.91 20-May-2013 nm metamath.c mmpfas.c,h mmcmds.c,h mmcmdl.c mmhlpb.c- added /FORBID qualifier to MINIMIZE_WITH */ /* 0.07.90 19-May-2013 nm metamath.c mmcmds.c mmcmdl.c mmhlpb.c - added /MATCH qualifier to SHOW TRACE_BACK */ /* 0.07.88 18-Nov-2012 nm mmcmds.c - fixed bug 243 */ /* 0.07.87 17-Nov-2012 nm mmwtex.c - fixed formatting problem when label markup ends a comment in SHOW PROOF ... /HTML */ /* 0.07.86 27-Oct-2012 nm mmcmds.c, mmwtex.c, mmwtex.h - fixed ERASE bug caused by imperfect re-initialization; reported by Wolf Lammen */ /* 0.07.85 10-Oct-2012 nm metamath.c, mmcmdl.c, mmwtex.c, mmwtex.h, mmhlpb.c - added /SHOW_LEMMAS to WRITE THEOREM_LIST to bypass lemma math suppression */ /* 0.07.84 9-Oct-2012 nm mmcmds.c - fixed bug in getStatementNum() */ /* 0.07.83 19-Sep-2012 nm mmwtex.c - fixed bug reported by Wolf Lammen */ /* 0.07.82 16-Sep-2012 nm metamath.c, mmpfas.c - fixed REPLACE infinite loop; improved REPLACE message for shared dummy variables */ /* 0.07.81 14-Sep-2012 nm metamath.c, mmcmds.c, mmcmds.h, mmcmdl.c, mmhlpb.c - added FIRST, LAST, +nn, -nn where missing from ASSIGN, REPLACE, IMPROVE, LET STEP. Wildcards are allowed for PROVE, ASSIGN, REPLACE labels provided there is a unique match. */ /* 0.07.80 4-Sep-2012 nm metamath.c, mmpfas.c, mmpfas.h, mmcmdl.c, mmhlpb.c - added / 1, / 2, / 3, / SUBPROOFS to IMPROVE to specify search level */ /* 0.07.79 31-Aug-2012 nm m*.c - clean up some gcc warnings */ /* 0.07.78 28-Aug-2012 nm mmpfas.c - fix bug in 0.07.77. */ /* 0.07.77 25-Aug-2012 nm metamath.c, mmpfas.c - Enhanced IMPROVE algorithm to allow non-shared dummy variables in unknown steps */ /* 0.07.76 22-Aug-2012 nm metamath.c, mmpfas.c, mmcmdl.c, mmhlpb.c - Enhanced IMPROVE algorithm to also try REPLACE algorithm */ /* 0.07.75 14-Aug-2012 nm metamath.c - MINIMIZE_WITH now checks current mathbox (but not other mathboxes) even if /INCLUDE_MATHBOXES is omitted */ /* 0.07.74 18-Mar-2012 nm mmwtex.c, mmcmds.c, metamath.c - improved texToken() error message */ /* 0.07.73 26-Dec-2011 nm mmwtex.c, mmpars.c - added ... in comments for passing through raw HTML code into HTML files generated with SHOw STATEMENT xxx / HTML */ /* 0.07.72 25-Dec-2011 nm (obsolete) */ /* 0.07.71 10-Nov-2011 nm metamath.c, mmcmdl.c - added /REV to MINIMIZE_WITH */ /* 0.07.70 6-Aug-2011 nm mmwtex.c - fix handling of double quotes inside of htmldef strings to match spec in Metamath book Appendix A p. 156 */ /* 0.07.69 9-Jul-2011 nm mmpars.c, mmvstr.c - Untab file in WRITE SOURCE ... /REWRAP */ /* 0.07.68 3-Jul-2011 nm metamath.c, mminou.h, mminou.c - Nested SUBMIT calls (SUBMIT calls inside of a SUBMIT command file) are now allowed. Also, mmdata.c - fix memory leak. */ /* 0.07.67 2-Jul-2011 nm metamath.c, mmcmdl.c, mmhlpa.c - Added TAG command to TOOLS. See HELP TAG under TOOLS. (The old special-purpose TAG command was renamed to UPDATE.) */ /* 0.07.66 1-Jul-2011 nm metamath.c, mmcmds.c, mmpars.c, mmpars.h - Added code to strip spurious "$( [?] $)" in WRITE SOURCE ... /CLEAN output */ /* 0.07.65 30-Jun-2011 nm mmwtex.c - Prevent processing [...] bibliography brackets inside of `...` math strings in comments. */ /* 0.07.64 28-Jun-2011 nm metamath.c, mmcmdl.c - Added /INCLUDE_MATHBOXES qualifier to MINIMIZE_WITH; without it, MINIMIZE_WITH * will skip checking user mathboxes. */ /* 0.07.63 26-Jun-2011 nm mmwtex.c - check that .gifs exist for htmldefs */ /* 0.07.62 18-Jun-2011 nm mmpars.c - fixed bug where redeclaration of active $v was not detected */ /* 0.07.61 12-Jun-2011 nm mmpfas.c, mmcmds.c, metamath.c, mmhlpb.c - added /FORMAT and /REWRAP qualifiers to WRITE SOURCE to format according to set.mm conventions - set HELP WRITE SOURCE */ /* 0.07.60 7-Jun-2011 nm mmpfas.c - fixed bug 1805 which occurred when doing MINIMIZE_WITH weq/ALLOW_GROWTH after DELETE DELETE FLOATING_HYPOTHESES */ /* 0.07.59 11-Dec-2010 nm mmpfas.c - increased default SET SEARCH_LIMIT from 10000 to 25000 to accomodate df-plig web page in set.mm */ /* 0.07.58 9-Dec-2010 nm mmpars.c - detect if same symbol is used with both $c and $v, in order to conform with Metamath spec */ /* 0.07.57 19-Oct-2010 nm mmpars.c - fix bug causing incorrect line count for error messages when non-ASCII character was found; mminou.h - increase SET WIDTH maximum from 999 to 9999 */ /* 0.07.56 27-Sep-2010 nm mmpars.c, mmpfas.c - check for $a's with one token e.g. "$a wff $."; if found, turn SET EMPTY_SUBSTITUTION ON automatically. (Suggested by Mel O'Cat; patent pending.) */ /* 0.07.55 26-Sep-2010 nm mmunif.c, mmcmds.c, mmunif.h - check for mismatched brackets in all $a's, so that if there are any, the bracket matching algorithm (for fewer ambiguous unifications) in mmunif.c will be turned off. */ /* 0.07.54 25-Sep-2010 nm mmpars.c - added $f checking to conform to the current Metamath spec, so footnote 2 on p. 92 of Metamath book is no longer applicable. */ /* 0.07.53 24-Sep-2010 nm mmveri.c - fixed bug(2106), reported by Michal Burger */ /* 0.07.52 14-Sep-2010 nm metamath.c, mmwtex.h, mmwtex.c, mmcmds.c, mmcmdl.c, mmhlpb.c - rewrote the LaTeX output for easier hand-editing and embedding in LaTeX documents. The old LaTeX output is still available with /OLD_TEX on OPEN TEX, SHOW STATEMENT, and SHOW PROOF, but it is obsolete and will be deleted eventually if no one objects. The new /TEX output also replaces the old /SIMPLE_TEX, which was removed. */ /* 0.07.51 9-Sep-2010 Stefan Allen mmwtex.c - put hyperlinks on hypothesis label references in SHOW STATEMENT * /HTML, ALT_HTML output */ /* 0.07.50 21-Feb-2010 nm mminou.c - "./metamath < empty", where "empty" is a 0-byte file, now exits metamath instead of producing an infinite loop. Also, ^D now exits metamath. Reported by Cai Yufei */ /* 0.07.49 31-Jan-2010 nm mmcmds.c - Lemmon-style proofs (SHOW PROOF xxx /LEMON/RENUMBER) no longer have steps with dummy labels; instead, steps are now the same as in HTML page proofs. (There is a line to comment out if you want to revert to old behavior.) */ /* 0.07.48 11-Sep-2009 nm mmpars.c, mm, mmvstr.c, mmdata.c - Added detection of non-whitespace around keywords (mmpars.c); small changes to eliminate warnings in gcc 3.4.4 (mmvstr.c, mmdata.c) */ /* 0.07.47 2-Aug-2009 nm mmwtex.c, mmwtex.h - added user name to mathbox pages */ /* 0.07.46 24-Jul-2009 nm metamath.c, mmwtex.c - changed name of sandbox to "mathbox" */ /* 0.07.45 15-Jun-2009 nm metamath.c, mmhlpb.c - put "!" before each line of SET ECHO ON output to make them easy to identity for creating scripts */ /* 0.07.44 12-May-2009 Stefan Allan, nm metamath.c, mmcmdl.c, mmwtex.c - added SHOW STATEMENT / MNEMONICS - see HELP SHOW STATEMENT */ /* 0.07.43 29-Aug-2008 nm mmwtex.c - workaround for Unicode huge font bug in FireFox 3 */ /* 0.07.42 8-Aug-2008 nm metamath.c - added sandbox, Hilbert Space colors to Definition List */ /* 0.07.41 29-Jul-2008 nm metamath.c, mmwtex.h, mmwtex.c - Added handling of sandbox section of Metamath Proof Explorer web pages */ /* 0.07.40 6-Jul-2008 nm metamath.c, mmcmdl.c, mmhlpa.c, mmhlpb.c - Added / NO_VERSIONING qualifier for SHOW STATEMENT, so website can be regenerated in place with less temporary space required. Also, the wildcard trigger for mmdefinitions.html, etc. is more flexible (see HELP HTML). */ /* 0.07.39 21-May-2008 nm metamath.c, mmhlpb.c - Added wildcard handling to statement label in SHOW TRACE_BACK. All wildcards now allow comma-separated lists [i.e. matchesList() instead of matches()] */ /* 0.07.38 26-Apr-2008 nm metamath.c, mmdata.h, mmdata.c, mmvstr.c, mmhlpb.c - Enhanced / EXCEPT qualifier for MINIMIZE_WITH to handle comma-separated wildcard list. */ /* 0.07.37 14-Apr-2008 nm metamath.c, mmcmdl.c, mmhlpb.c - Added / JOIN qualifier to SEARCH. */ /* 0.07.36 7-Jan-2008 nm metamath.c, mmcmdl.c, mmhlpb.c - Added wildcard handling for labels in SHOW USAGE. */ /* 0.07.35 2-Jan-2008 nm mmcmdl.c, metamath.c, mmhlpb.c - Changed keywords COMPACT to PACKED and COLUMN to START_COLUMN so that SAVE/SHOW proof can use C to abbreviate COMPRESSED. (PACKED format is supported but "unofficial," used mainly for debugging purposes, and is not listed in HELP SAVE PROOF.) */ /* 0.07.34 19-Nov-2007 nm mmwtex.c, mminou.c - Added tooltips to proof step hyperlinks in SHOW STATEMENT.../HTML,ALT_HTML output (suggested by Reinder Verlinde) */ /* 0.07.33 19-Jul-2007 nm mminou.c, mmvstr.c, mmdata.c, mmword.c - added fflush after each printf() call for proper behavior inside emacs (suggested by Frederic Line) */ /* 0.07.32 29-Apr-2007 nm mminou.c - fSafeOpen now stops at gap; e.g. if ~2 doesn't exist, ~1 will be renamed to ~2, but any ~3, etc. are not touched */ /* 0.07.31 5-Apr-2007 nm mmwtex.c - Don't make "_" in hyperlink a subscript */ /* 0.07.30 8-Feb-2007 nm mmcmds.c, mmwtex.c Added HTML statement number info to SHOW STATEMENT.../FULL; friendlier "Contents+1" link in mmtheorems*.html */ /* 0.07.29 6-Feb-2007 Jason Orendorff mmpfas.c - Patch to eliminate the duplicate "Exceeded trial limit at step n" messages */ /* 0.07.28 22-Dec-2006 nm mmhlpb.c - Added info on quotes to HELP LET */ /* 0.07.27 23-Oct-2006 nm metamath.c, mminou.c, mmhlpa.c, mmhlpb.c - Added / SILENT qualifier to SUBMIT command */ /* 0.07.26 12-Oct-2006 nm mminou.c - Fixed bug when SUBMIT file was missing a new-line at end of file (reported by Marnix Klooster) */ /* 0.07.25 10-Oct-2006 nm metamath.c - Fixed bug invoking TOOLS as a ./metamath command-line argument */ /* 0.07.24 25-Sep-2006 nm mmcmdl.c Fixed bug in SHOW NEW_PROOF/START_COLUMN nn/LEM */ /* 0.07.23 31-Aug-2006 nm mmwtex.c - Added Home and Contents links to bottom of WRITE THEOREM_LIST pages */ /* 0.07.22 26-Aug-2006 nm metamath.c, mmcmdl.c, mmhlpb.c - Changed 'IMPROVE STEP ' to 'IMPROVE ' for user convenience and to be consistent with ASSIGN */ /* 0.07.21 20-Aug-2006 nm mmwtex.c - Revised small colored numbers so that all colors have the same grayscale brightness.. */ /* 0.07.20 19-Aug-2006 nm mmpars.c - Made the error "Required hypotheses may not be explicitly declared" in a compressed proof non-severe, so that we can still SAVE the proof to reformat and recover it. */ /* 0.07.19 11-Aug-06 nm mmcmds.c - "Distinct variable group(s)" is now "group" or "groups" as appropriate. */ /* 0.07.18 31-Jul-06 nm mmwtex.c - added table to contents to p.1 of output of WRITE THEOREM_LIST command. */ /* 0.07.17 4-Jun-06 nm mmpars.c - do not allow labels to match math symbols (new spec proposed by O'Cat). mmwtex.c - made theorem name 1st in title, for readability in Firefox tabs. */ /* 0.07.16 16-Apr-06 nm metamath.c, mmcmdl.c, mmpfas.c, mmhlpb.c - allow step to be negative (relative to end of proof) for ASSIGN, UNIFY, and LET STEP (see their HELPs). Added INITIALIZE USER to delete LET STEP assignments (see HELP INITIALIZE). Fixed bug in LET STEP (mmpfas.c). */ /* 0.07.15 10-Apr-06 nm metamath.c, mmvstr.c - change dates from 2-digit to 4-digit year; make compatible with older 2-digit year. */ /* 0.07.14 21-Mar-06 nm mmpars.c - fix bug 1722 when compressed proof has "Z" at beginning of proof instead of after a proof step. */ /* 0.07.13 3-Feb-06 nm mmpfas.c - minor improvement to MINIMIZE_WITH */ /* 0.07.12 30-Jan-06 nm metamath.c, mmcmds.c, mmdata.c, mmdata.h, mmhlpa.c, mmhlpb.c - added "?" wildcard to match single character. See HELP SEARCH. */ /* 0.07.11 7-Jan-06 nm metamath.c, mmcmdl.c, mmhlpb.c - added EXCEPT qualifier to MINIMIZE_WITH */ /* 0.07.10 28-Dec-05 nm metamath.c, mmcmds.c - cosmetic tweaks */ /* 0.07.10 11-Dec-05 nm metamath.c, mmcmdl.c, mmhlpb.c - added ASSIGN FIRST and IMPROVE FIRST commands. Also enhanced READ error message */ /* 0.07.9 1-Dec-05 nm mmvstr.c - added comment on how to make portable */ /* 0.07.9 18-Nov-05 nm metamath.c, mminou.c, mminou.h, mmcmdl.c, mmhlpb.c - added SET HEIGHT command; changed SET SCREEN_WIDTH to SET WIDTH; changed SET HENTY_FILTER to SET JEREMY_HENTY_FILTER (to make H for HEIGHT unambiguous); added HELP for SET JEREMY_HENTY_FILTER */ /* 0.07.8 15-Nov-05 nm mmunif.c - now detects wrong order in bracket matching heuristic to further reduce ambiguous unifications in Proof Assistant */ /* 0.07.7 12-Nov-05 nm mmunif.c - add "[","]" and "[_","]_" bracket matching heuristic to reduce ambiguous unifications in Proof Assistant. mmwtex.c - added heuristic for HTML spacing after "sum_" token. */ /* 0.07.6 15-Oct-05 nm mmcmds.c,mmpars.c - fixed compressed proof algorithm to match spec in book (with new algorithm due to Marnix Klooster). Users are warned to convert proofs when the old compression is found. */ /* 0.07.5 6-Oct-05 nm mmpars.c - fixed bug that reset "severe error in proof" flag when a proof with severe error also had unknown steps */ /* 0.07.4 1-Oct-05 nm mmcmds.c - ignored bug 235, which could happen for non-standard logics */ /* 0.07.3 17-Sep-05 nm mmpars.c - reinstated duplicate local label checking to conform to strict spec */ /* 0.07.2 19-Aug-05 nm mmwtex.c - suppressed math content for lemmas in WRITE THEOREMS output */ /* 0.07.1 28-Jul-05 nm Added SIMPLE_TEX qualifier to SHOW STATEMENT */ /* 0.07: Official 0.07 22-Jun-05 corresponding to Metamath book */ /* 0.07x: Fixed to work with AMD64 with 64-bit longs by Waldek Hebisch; deleted unused stuff in mmdata.c */ /* 0.07w: .mm date format like "$( [7-Sep-04] $)" is now generated and permitted (old one is tolerated too for compatibility) */ /* Metamath Proof Verifier - main program */ /* See the book "Metamath" for description of Metamath and run instructions */ /*****************************************************************************/ /*----------------------------------------------------------------------*/ #include #include #include #include #include #include /* #include */ /* 21-Jun-2014 nm For ELAPSED_TIME */ #ifdef THINK_C #include #endif #include "mmutil.h" #include "mmvstr.h" #include "mmdata.h" #include "mmcmdl.h" #include "mmcmds.h" #include "mmhlpa.h" #include "mmhlpb.h" #include "mminou.h" #include "mmpars.h" #include "mmveri.h" #include "mmpfas.h" #include "mmunif.h" #include "mmword.h" #include "mmwtex.h" #ifdef THINK_C #include "mmmaci.h" #endif void command(int argc, char *argv[]); int main(int argc, char *argv[]) { /* argc is the number of arguments; argv points to an array containing them */ #ifdef THINK_C /* Set console attributes */ console_options.pause_atexit = 0; /* No pause at exit */ console_options.title = (unsigned char*)"\pMetamath"; #endif #ifdef THINK_C /* The standard stream triggers the console package to initialize the Macintosh Toolbox managers and use the console interface. cshow must be called before using our own window to prevent crashing (THINK C Standard Library Reference p. 43). */ cshow(stdout); /* Initialize MacIntosh interface */ /*ToolBoxInit(); */ /* cshow did this automatically */ /* Display opening window */ /* WindowInit(); DrawMyPicture(); */ /* Wait for mouse click or key */ /*while (!Button());*/ #endif /****** If g_listMode is set to 1 here, the startup will be Text Tools utilities, and Metamath will be disabled ***************************/ /* (Historically, this mode was used for the creation of a stand-alone "TOOLS>" utility for people not interested in Metamath. This utility was named "LIST.EXE", "tools.exe", and "tools" on VMS, DOS, and Unix platforms respectively. The UPDATE command of TOOLS (mmword.c) was custom-written in accordance with the version control requirements of a company that used it; it documents the differences between two versions of a program as C-style comments embedded in the newer version.) */ g_listMode = 0; /* Force Metamath mode as startup */ g_toolsMode = g_listMode; if (!g_listMode) { /*print2("Metamath - Version %s\n", MVERSION);*/ print2("Metamath - Version %s%s", MVERSION, space(27 - (long)strlen(MVERSION))); } /* if (argc < 2) */ print2("Type HELP for help, EXIT to exit.\n"); /* Allocate big arrays */ initBigArrays(); /* 14-May-2017 nm */ /* Set the default contributor */ let(&g_contributorName, DEFAULT_CONTRIBUTOR); /* Process a command line until EXIT */ command(argc, argv); /* Close logging command file */ if (g_listMode && g_listFile_fp != NULL) { fclose(g_listFile_fp); } return 0; } void command(int argc, char *argv[]) { /* Command line user interface -- this is an infinite loop; it fetches and processes a command; returns only if the command is 'EXIT' or 'QUIT' and never returns otherwise. */ long argsProcessed = 0; /* Number of argv initial command-line arguments processed so far */ long /*c,*/ i, j, k, m, l, n, p, q, r, s /*,tokenNum*/; long stmt, step; int subType = 0; #define SYNTAX 4 vstring str1 = "", str2 = "", str3 = "", str4 = "", str5= ""; nmbrString *nmbrTmpPtr; /* Pointer only; not allocated directly */ nmbrString *nmbrTmp = NULL_NMBRSTRING; nmbrString *nmbrSaveProof = NULL_NMBRSTRING; /*pntrString *pntrTmpPtr;*/ /* Pointer only; not allocated directly */ pntrString *pntrTmp = NULL_PNTRSTRING; pntrString *expandedProof = NULL_PNTRSTRING; flag tmpFlag; /* 1-Nov-2013 nm proofSavedFlag tells us there was at least one SAVE NEW_PROOF during the MM-PA session while the UNDO stack wasn't empty, meaning that "UNDO stack empty" is no longer a reliable indication that the proof wasn't changed. It is cleared upon entering MM-PA, and set by SAVE NEW_PROOF. */ flag proofSavedFlag = 0; /* Variables for SHOW PROOF */ flag pipFlag; /* Proof-in-progress flag */ long outStatement; /* Statement for SHOW PROOF or SHOW NEW_PROOF */ flag explicitTargets; /* For SAVE PROOF /EXPLICIT */ long startStep; long endStep; /* long startIndent; */ long endIndent; /* Also for SHOW TRACE_BACK */ flag essentialFlag; /* Also for SHOW TRACE_BACK */ flag renumberFlag; /* Flag to use essential step numbering */ flag unknownFlag; flag notUnifiedFlag; flag reverseFlag; long detailStep; flag noIndentFlag; /* Flag to use non-indented display */ long splitColumn; /* Column at which formula starts in nonindented display */ flag skipRepeatedSteps; /* NO_REPEATED_STEPS qualifier */ /* 28-Jun-2013 nm */ flag texFlag; /* Flag for TeX */ flag saveFlag; /* Flag to save in source */ flag fastFlag; /* Flag for SAVE PROOF.../FAST */ /* 2-Jan-2017 nm */ long indentation; /* Number of spaces to indent proof */ vstring labelMatch = ""; /* SHOW PROOF ", g_Statement[stmt].labelName, "", str4, "", NULL), /* Description */ /* 28-Dec-05 nm Added ALIGN=LEFT for IE */ " ", /* Start continuation line with space */ "\""); /* Don't break inside quotes e.g. "Arial Narrow" */ g_showStatement = stmt; /* For printTexComment */ g_outputToString = 0; /* For printTexComment */ g_texFilePtr = list2_fp; /* 18-Sep-03 ???Future - make this just return a string??? */ /* printTexComment(str3, 0); */ /* 17-Nov-2015 nm Added 3rd & 4th arguments */ printTexComment(str3, /* Sends result to g_texFilePtr */ 0, /* 1 = htmlCenterFlag */ PROCESS_EVERYTHING, /* actionBits */ /* 13-Dec-2018 nm */ 0 /* 1 = noFileCheck */ ); g_texFilePtr = NULL; g_outputToString = 1; /* Restore after printTexComment */ /* Get HTML hypotheses => assertion */ let(&str4, ""); str4 = getTexOrHtmlHypAndAssertion(stmt); /* In mmwtex.c */ printLongLine(cat("" : cat(" BGCOLOR=", PURPLISH_BIBLIO_COLOR, ">", NULL), */ /* 29-Jul-2008 nm Sandbox stuff */ (stmt < g_extHtmlStmt) ? ">" : (stmt < g_mathboxStmt) ? cat(" BGCOLOR=", PURPLISH_BIBLIO_COLOR, ">", NULL) : cat(" BGCOLOR=", SANDBOX_COLOR, ">", NULL), /*** old " ", str4, "", NULL), ****/ /* 27-Oct-03 nm */ "", str4, "", NULL), " ", /* Start continuation line with space */ "\""); /* Don't break inside quotes e.g. "Arial Narrow" */ g_outputToString = 0; fprintf(list2_fp, "%s", g_printString); let(&g_printString, ""); if (n >= i /*RECENT_COUNT*/) break; /* We're done */ /* 27-Oct-03 nm Put separator row if not last theorem */ g_outputToString = 1; printLongLine(cat("", " ", NULL), " ", /* Start continuation line with space */ "\""); /* Don't break inside quotes e.g. "Arial Narrow" */ /* 29-Jul-04 nm Put the previous, current, and next statement labels in HTML comments so a script can use them to update web site incrementally. This would be done by searching for "For script" and gather label between = and --> then regenerate just those statements. Previous and next labels are included to prevent dead links if they don't exist yet. */ /* This section can be deleted without side effects */ /* Find the previous statement with a web page */ j = 0; for (q = stmt - 1; q >= 1; q--) { if (g_Statement[q].type == (char)p_ || g_Statement[q].type == (char)a_ ) { j = q; break; } } /* 13-Dec-2018 nm This isn't used anywhere yet. But fix error in current label and also identify previous, current, next */ if (j) print2("\n", g_Statement[j].labelName); /* Current statement */ print2("\n", g_Statement[stmt].labelName); /* Find the next statement with a web page */ j = 0; for (q = stmt + 1; q <= g_statements; q++) { if (g_Statement[q].type == (char)p_ || g_Statement[q].type == (char)a_ ) { j = q; break; } } if (j) print2("\n", g_Statement[j].labelName); /* End of 29-Jul-04 section */ g_outputToString = 0; fprintf(list2_fp, "%s", g_printString); let(&g_printString, ""); } } /* Next stmt - statement number */ /* Decrement date */ if (k > 1) { k--; /* Decrement day */ } else { k = 31; /* Non-existent day 31's will never match, which is OK */ if (l > 1) { l--; /* Decrement month */ } else { l = 12; /* Dec */ m --; /* Decrement year */ } } } /* next while - Scan next date */ /* Discard the input file up to the special "" comment */ while (1) { if (!linput(list1_fp, NULL, &str1)) { print2( "?Error: Could not find \"\" line in input file \"%s\".\n", g_fullArg[2]); tmpFlag = 1; /* Error flag to recover input file */ break; } if (!strcmp(str1, "")) { fprintf(list2_fp, "%s\n", str1); break; } } if (tmpFlag) goto wrrecent_error; /* Transfer the rest of the input file */ while (1) { if (!linput(list1_fp, NULL, &str1)) { break; } /* Update the date stamp at the bottom of the HTML page. */ /* This is just a nicety; no error check is done. */ if (!strcmp("This page was last updated on ", left(str1, 30))) { let(&str1, cat(left(str1, 30), date(), ".", NULL)); } fprintf(list2_fp, "%s\n", str1); } print2("The %ld most recent theorem(s) were written.\n", n); wrrecent_error: fclose(list1_fp); fclose(list2_fp); if (tmpFlag) { /* Recover input files in case of error */ remove(g_fullArg[2]); /* Delete output file */ rename(cat(g_fullArg[2], "~1", NULL), g_fullArg[2]); /* Restore input file name */ print2("?The file \"%s\" was not modified.\n", g_fullArg[2]); } continue; } /* End of "WRITE RECENT_ADDITIONS" */ if (cmdMatches("SHOW LABELS")) { linearFlag = 0; if (switchPos("/ LINEAR")) linearFlag = 1; if (switchPos("/ ALL")) { m = 1; /* Include $e, $f statements */ print2( "The labels that match are shown with statement number, label, and type.\n"); } else { m = 0; /* Show $a, $p only */ print2( "The assertions that match are shown with statement number, label, and type.\n"); } j = 0; k = 0; let(&str2, ""); /* Line so far */ #define COL 20 /* Column width */ #define MIN_SPACE 2 /* At least this many spaces between columns */ for (i = 1; i <= g_statements; i++) { if (!g_Statement[i].labelName[0]) continue; /* No label */ if (!m && g_Statement[i].type != (char)p_ && g_Statement[i].type != (char)a_) continue; /* No /ALL switch */ /* 30-Jan-06 nm Added single-character-match wildcard argument */ if (!matchesList(g_Statement[i].labelName, g_fullArg[2], '*', '?')) { continue; } /* 2-Oct-2015 nm */ let(&str1, cat(str((double)i), " ", g_Statement[i].labelName, " $", chr(g_Statement[i].type), NULL)); if (!str2[0]) { j = 0; /* # of fields on line so far */ } k = ((long)strlen(str2) + MIN_SPACE > j * COL) ? (long)strlen(str2) + MIN_SPACE : j * COL; /* Position before new str1 starts */ if (k + (long)strlen(str1) > g_screenWidth || linearFlag) { if (j == 0) { /* In case of huge label, force it out anyway */ printLongLine(str1, "", " "); } else { /* Line width exceeded, postpone adding str1 */ print2("%s\n", str2); let(&str2, str1); j = 1; } } else { /* Add new field to line */ if (j == 0) { let(&str2, str1); /* Don't put space before 1st label on line */ } else { let(&str2, cat(str2, space(k - (long)strlen(str2)), str1, NULL)); } j++; } /* 2-Oct-2015 nm Deleted let(&str1,cat(str((double)i)," ", g_Statement[i].labelName," $",chr(g_Statement[i].type)," ",NULL)); #define COL 19 /@ Characters per column @/ if (j + (long)strlen(str1) > MAX_LEN || (linearFlag && j != 0)) { /@ j != 0 to suppress 1st CR @/ print2("\n"); j = 0; k = 0; } if (strlen(str1) > COL || linearFlag) { j = j + (long)strlen(str1); k = k + (long)strlen(str1) - COL; print2(str1); } else { if (k == 0) { j = j + COL; print2("%s%s",str1,space(COL - (long)strlen(str1))); } else { k = k - (COL - (long)strlen(str1)); if (k > 0) { print2(str1); j = j + (long)strlen(str1); } else { print2("%s%s",str1,space(COL - (long)strlen(str1))); j = j + COL; k = 0; } } } */ } /* next i */ /* print2("\n"); */ if (str2[0]) { print2("%s\n", str2); let(&str2, ""); } let(&str1, ""); continue; } if (cmdMatches("SHOW DISCOURAGED")) { /* was SHOW RESTRICTED */ showDiscouraged(); /* In mmcmds.c */ continue; } if (cmdMatches("SHOW SOURCE")) { /* 14-Sep-2012 nm */ /* Currently, SHOW SOURCE only handles one statement at a time, so use getStatementNum(). Eventually, SHOW SOURCE may become obsolete; I don't think anyone uses it. */ s = getStatementNum(g_fullArg[2], 1/*startStmt*/, g_statements + 1 /*maxStmt*/, 1/*aAllowed*/, 1/*pAllowed*/, 1/*eAllowed*/, 1/*fAllowed*/, 0/*efOnlyForMaxStmt*/, 1/*uniqueFlag*/); if (s == -1) { continue; /* Error msg was provided */ } g_showStatement = s; /* Update for future defaults */ /*********** 14-Sep-2012 replaced by getStatementNum() for (i = 1; i <= g_statements; i++) { if (!strcmp(g_fullArg[2],g_Statement[i].labelName)) break; } if (i > g_statements) { printLongLine(cat("?There is no statement with label \"", g_fullArg[2], "\". ", "Use SHOW LABELS for a list of valid labels.", NULL), "", " "); g_showStatement = 0; continue; } g_showStatement = i; ************** end 14-Sep-2012 *******/ let(&str1, ""); str1 = outputStatement(g_showStatement, /*0, 3-May-2017 */ /* cleanFlag */ 0 /* reformatFlag */); let(&str1,edit(str1,128)); /* Trim trailing spaces */ if (str1[strlen(str1)-1] == '\n') let(&str1, left(str1, (long)strlen(str1) - 1)); printLongLine(str1, "", ""); let(&str1,""); /* Deallocate vstring */ continue; } /* if (cmdMatches("SHOW SOURCE")) */ if (cmdMatches("SHOW STATEMENT") && ( switchPos("/ HTML") || switchPos("/ BRIEF_HTML") || switchPos("/ ALT_HTML") || switchPos("/ BRIEF_ALT_HTML"))) { /* Special processing for the / HTML qualifiers - for each matching statement, a .html file is opened, the statement is output, and depending on statement type a proof or other information is output. */ /* if (g_rawArgs != 5) { */ /* obsolete */ /* 16-Aug-2016 nm */ noVersioning = (switchPos("/ NO_VERSIONING") != 0); i = 5; /* # arguments with only / HTML or / ALT_HTML */ if (noVersioning) i = i + 2; if (switchPos("/ TIME")) i = i + 2; if (g_rawArgs != i) { printLongLine(cat("?The HTML qualifiers may not be combined with", " others except / NO_VERSIONING and / TIME.\n", NULL), " ", " "); continue; } /* 16-Aug-2016 nm */ printTime = 0; if (switchPos("/ TIME") != 0) { printTime = 1; } /*** 17-Nov-2014 nm This restriction has been removed. if (g_texDefsRead) { /@ Current limitation - can only read def's from .mm file once @/ if (!g_htmlFlag) { print2("?You cannot use both LaTeX and HTML in the same session.\n"); print2( "You must EXIT and restart Metamath to switch to the other.\n"); goto htmlDone; } else { if ((switchPos("/ ALT_HTML") || switchPos("/ BRIEF_ALT_HTML")) == (g_altHtmlFlag == 0)) { print2( "?You cannot use both HTML and ALT_HTML in the same session.\n"); print2( "You must EXIT and restart Metamath to switch to the other.\n"); goto htmlDone; } } } *** End 17-Nov-2014 deletion */ g_htmlFlag = 1; /* 17-Nov-2015 nm */ if (switchPos("/ BRIEF_HTML") || switchPos("/ BRIEF_ALT_HTML")) { if (strcmp(g_fullArg[2], "*")) { print2( "?For BRIEF_HTML or BRIEF_ALT_HTML, the label must be \"*\"\n"); goto htmlDone; } g_briefHtmlFlag = 1; } else { g_briefHtmlFlag = 0; } if (switchPos("/ ALT_HTML") || switchPos("/ BRIEF_ALT_HTML")) { g_altHtmlFlag = 1; } else { g_altHtmlFlag = 0; } q = 0; /* Special feature: if the match statement starts with "*", we will also output mmascii.html, mmtheoremsall.html, and mmdefinitions.html. So, with SHOW STATEMENT * / HTML these will be output plus all statements; with SHOW STATEMENT *! / HTML these will be output with no statements (since ! is illegal in a statement label); with SHOW STATEMENT ?* / HTML all statements will be output, but without mmascii.html etc. */ /* if (instr(1, g_fullArg[2], "*") || g_briefHtmlFlag) { */ /* obsolete */ if (((char *)(g_fullArg[2]))[0] == '*' || g_briefHtmlFlag) { /* 6-Jul-2008 nm */ s = -2; /* -2 is for ASCII table; -1 is for theorems; 0 is for definitions */ } else { s = 1; } for (s = s + 0; s <= g_statements; s++) { if (s > 0 && g_briefHtmlFlag) break; /* Only do summaries */ /* s = -2: mmascii.html s = -1: mmtheoremsall.html (used to be mmtheorems.html) s = 0: mmdefinitions.html s > 0: normal statement */ if (s > 0) { if (!g_Statement[s].labelName[0]) continue; /* No label */ /* 30-Jan-06 nm Added single-character-match wildcard argument */ if (!matchesList(g_Statement[s].labelName, g_fullArg[2], '*', '?')) continue; if (g_Statement[s].type != (char)a_ && g_Statement[s].type != (char)p_) continue; } q = 1; /* Flag that at least one matching statement was found */ if (s > 0) { g_showStatement = s; } else { /* We set it to 1 here so we will output the Metamath Proof Explorer and not the Hilbert Space Explorer header for definitions and theorems lists, when g_showStatement is compared to g_extHtmlStmt in printTexHeader in mmwtex.c */ g_showStatement = 1; } /*** Open the html file ***/ g_htmlFlag = 1; /* Open the html output file */ switch (s) { case -2: let(&g_texFileName, "mmascii.html"); break; case -1: let(&g_texFileName, "mmtheoremsall.html"); break; case 0: let(&g_texFileName, "mmdefinitions.html"); break; default: let(&g_texFileName, cat(g_Statement[g_showStatement].labelName, ".html", NULL)); } print2("Creating HTML file \"%s\"...\n", g_texFileName); g_texFilePtr = fSafeOpen(g_texFileName, "w", /* 17-Jul-2019 nm */ noVersioning /*noVersioningFlag*/); /****** old code before 17-Jul-2019 ******* if (switchPos("/ NO_VERSIONING") == 0) { g_texFilePtr = fSafeOpen(g_texFileName, "w", 0/@noVersioningFlag@/); } else { /@ 6-Jul-2008 nm Added / NO_VERSIONING @/ /@ Don't create the backup versions ~1, ~2,... @/ g_texFilePtr = fopen(g_texFileName, "w"); if (!g_texFilePtr) print2("?Could not open the file \"%s\".\n", g_texFileName); } ********* end of old code before 17-Jul-2019 *******/ if (!g_texFilePtr) goto htmlDone; /* Couldn't open it (err msg was provided) */ g_texFileOpenFlag = 1; printTexHeader((s > 0) ? 1 : 0 /*texHeaderFlag*/); if (!g_texDefsRead) { /* 9/6/03 If there was an error reading the $t xx.mm statement, g_texDefsRead won't be set, and we should close out file and skip further processing. Otherwise we will be attempting to process uninitialized htmldef arrays and such. */ print2("?HTML generation was aborted due to the error above.\n"); s = g_statements + 1; /* To force loop to exit */ goto ABORT_S; /* Go to end of loop where file is closed out */ } if (s <= 0) { g_outputToString = 1; if (s == -2) { printLongLine(cat("
", "Symbol to ASCII Correspondence for Text-Only Browsers", " (in order of appearance in $c and $v statements", " in the database)", "

", NULL), "", "\""); } /* 13-Oct-2006 nm todo - still appears - where is it? */ if (!g_briefHtmlFlag) print2("

\n"); print2("\n"); break; case -1: print2("SUMMARY=\"List of theorems\">\n"); break; case 0: print2("SUMMARY=\"List of syntax, axioms and definitions\">\n"); break; } switch (s) { case -2: print2("\n"); m = 0; /* Statement number map */ let(&str3, ""); /* For storing ASCII token list in s=-2 mode */ let(&bgcolor, MINT_BACKGROUND_COLOR); /* 8-Aug-2008 nm Initialize */ for (i = 1; i <= g_statements; i++) { /* 8-Aug-2008 nm Commented out: */ /* if (i == g_extHtmlStmt && s != -2) { / * Print a row that identifies the start of the extended database (e.g. Hilbert Space Explorer) * / printLongLine(cat( "", NULL), "", "\""); } */ /* 8-Aug-2008 nm */ if (s != -2 && (i == g_extHtmlStmt || i == g_mathboxStmt)) { /* Print a row that identifies the start of the extended database (e.g. Hilbert Space Explorer) or the user sandboxes */ if (i == g_extHtmlStmt) { let(&bgcolor, PURPLISH_BIBLIO_COLOR); } else { let(&bgcolor, SANDBOX_COLOR); } printLongLine(cat("", NULL), "", "\""); } if (g_Statement[i].type == (char)p_ || g_Statement[i].type == (char)a_ ) m++; if ((s == -1 && g_Statement[i].type != (char)p_) || (s == 0 && g_Statement[i].type != (char)a_) || (s == -2 && g_Statement[i].type != (char)c_ && g_Statement[i].type != (char)v_) ) continue; switch (s) { case -2: /* Print symbol to ASCII table entry */ /* It's a $c or $v statement, so each token generates a table row */ for (j = 0; j < g_Statement[i].mathStringLen; j++) { let(&str1, g_MathToken[(g_Statement[i].mathString)[j]].tokenName); /* Output each token only once in case of multiple decl. */ if (!instr(1, str3, cat(" ", str1, " ", NULL))) { let(&str3, cat(str3, " ", str1, " ", NULL)); let(&str2, ""); str2 = tokenToTex(g_MathToken[(g_Statement[i].mathString)[j] ].tokenName, i/*stmt# for error msgs*/); /* 2/9/02 Skip any tokens (such as |- in QL Explorer) that may be suppressed */ if (!str2[0]) continue; /* Convert special characters to HTML entities */ for (k = 0; k < (signed)(strlen(str1)); k++) { if (str1[k] == '&') { let(&str1, cat(left(str1, k), "&", right(str1, k + 2), NULL)); k = k + 4; } if (str1[k] == '<') { let(&str1, cat(left(str1, k), "<", right(str1, k + 2), NULL)); k = k + 3; } if (str1[k] == '>') { let(&str1, cat(left(str1, k), ">", right(str1, k + 2), NULL)); k = k + 3; } } /* next k */ printLongLine(cat("", NULL), "", "\""); } } /* next j */ /* Close out the string now to prevent memory overflow */ fprintf(g_texFilePtr, "%s", g_printString); let(&g_printString, ""); break; case -1: /* Falls through to next case */ case 0: /* Count the number of essential hypotheses k */ /* Not needed anymore??? since getTexOrHtmlHypAndAssertion() */ /* k = 0; j = nmbrLen(g_Statement[i].reqHypList); for (n = 0; n < j; n++) { if (g_Statement[g_Statement[i].reqHypList[n]].type == (char)e_) { k++; } } */ let(&str1, ""); if (s == 0 || g_briefHtmlFlag) { let(&str1, ""); /* 18-Sep-03 Get HTML hypotheses => assertion */ str1 = getTexOrHtmlHypAndAssertion(i); /* In mmwtex.c */ let(&str1, cat(str1, "", NULL)); } /* 13-Oct-2006 nm Made some changes to BRIEF_HTML/_ALT_HTML to use its mmtheoremsall.html output for the Palm PDA */ if (g_briefHtmlFlag) { /* Get page number in mmtheorems*.html of WRITE THEOREMS */ k = ((g_Statement[i].pinkNumber - 1) / THEOREMS_PER_PAGE) + 1; /* Page # */ let(&str2, cat("", NULL)); printLongLine(str1, "", "\""); } /* Close out the string now to prevent overflow */ fprintf(g_texFilePtr, "%s", g_printString); let(&g_printString, ""); break; } /* end switch */ } /* next i (statement number) */ /* print2("
\n"); break; case -1: print2( "
List of Theorems
\n"); break; case 0: printLongLine(cat( /*"
List of Syntax (not |- ), ",*/ /* 2/9/02 (in case |- suppressed) */ "List of Syntax, ", "Axioms (ax-) and", " Definitions (df-)", "
", NULL), "", "\""); break; } switch (s) { case -2: print2("SymbolASCII\n"); break; case -1: print2( "RefDescription\n"); break; case 0: printLongLine(cat( "Ref", "Expression (see link for any distinct variable requirements)", NULL), "", "\""); break; } print2("
", "The list of syntax, axioms (ax-) and definitions (df-) for", " the ", g_extHtmlTitle, " starts here
", "The list of syntax, axioms (ax-) and definitions (df-) for", " the ", (i == g_extHtmlStmt) ? g_extHtmlTitle : /*"User Sandboxes",*/ /* 24-Jul-2009 nm Changed name of sandbox to "mathbox" */ "User Mathboxes", " starts here
", (g_altHtmlFlag ? cat("", NULL) : ""), /* 14-Jan-2016 nm */ str2, (g_altHtmlFlag ? "" : ""), /* 14-Jan-2016 nm */ " ", /* 10-Jan-2016 nm This will prevent a -4px shifted image from overlapping the lower border of the table cell */ "", str1, "
", /*"",*/ "", str((double)(g_Statement[i].pinkNumber)), " ", "", g_Statement[i].labelName, "", NULL)); let(&str1, cat(str2, " ", str1, NULL)); } else { /* Get little pink (or rainbow-colored) number */ let(&str4, ""); str4 = pinkHTML(i); let(&str2, cat("
", g_Statement[i].labelName, "", str4, NULL)); let(&str1, cat(str2, "", str1, NULL)); } /* End of 13-Oct-2006 changed section */ print2("\n"); /* New line for HTML source readability */ printLongLine(str1, "", "\""); if (s == 0 || g_briefHtmlFlag) { /* Set s == 0 here for Web site version, s == s for symbol version of theorem list */ /* The below has been replaced by getTexOrHtmlHypAndAssertion(i) above. */ /*printTexLongMath(g_Statement[i].mathString, "", "", 0, 0);*/ /*g_outputToString = 1;*/ /* Is reset by printTexLongMath */ } else { /* Theorems are listed w/ description; otherwise file is too big for convenience */ let(&str1, ""); str1 = getDescription(i); if (strlen(str1) > 29) let(&str1, cat(left(str1, 26), "...", NULL)); let(&str1, cat(str1, "
\n"); */ /* 8/8/03 Removed - already done somewhere else, causing validator.w3.org to fail */ g_outputToString = 0; /* closing will write out the string */ let(&bgcolor, ""); /* Deallocate (to improve fragmentation) */ } else { /* s > 0 */ /* 16-Aug-2016 nm */ if (printTime == 1) { getRunTime(&timeIncr); /* This call just resets the time */ } /*** Output the html statement body ***/ typeStatement(g_showStatement, 0 /*briefFlag*/, 0 /*commentOnlyFlag*/, 1 /*texFlag*/, /* means latex or html */ 1 /*g_htmlFlag*/); /* 16-Aug-2016 nm */ if (printTime == 1) { getRunTime(&timeIncr); print2("SHOW STATEMENT run time = %6.2f sec for \"%s\"\n", timeIncr, g_texFileName); } } /* if s <= 0 */ ABORT_S: /*** Close the html file ***/ printTexTrailer(1 /*texHeaderFlag*/); fclose(g_texFilePtr); g_texFileOpenFlag = 0; let(&g_texFileName,""); } /* next s */ if (!q) { /* No matching statement was found */ printLongLine(cat("?There is no statement whose label matches \"", g_fullArg[2], "\". ", "Use SHOW LABELS for a list of valid labels.", NULL), "", " "); continue; } /* Complete the command processing to bypass normal SHOW STATEMENT (non-html) below. */ htmlDone: continue; } /* if (cmdMatches("SHOW STATEMENT") && switchPos("/ HTML")...) */ /******* Section for / MNEMONICS added 12-May-2009 by Stefan Allan *****/ /* Write mnemosyne.txt */ if (cmdMatches("SHOW STATEMENT") && switchPos("/ MNEMONICS")) { /*** 17-Nov-2015 nm Deleted - removed g_htmlFlag, g_altHtmlFlag change prohibition if (!g_texDefsRead) { g_htmlFlag = 1; /@ Use HTML, not TeX section @/ g_altHtmlFlag = 1; /@ Use Unicode, not GIF @/ print2("Reading definitions from $t statement of %s...\n", g_input_fn); if (2/@error@/ == readTexDefs(0 /@ 1 = check errors only @/, 0 /@ 1 = no GIF file existence check @/ )) { print2( "?There was an error in the $t comment's LaTeX/HTML definitions.\n"); print2("?HTML generation was aborted due to the error above.\n"); continue; /@ An error occurred @/ } } else { /@ Current limitation - can only read def's from .mm file once @/ if (!g_htmlFlag) { print2("?You cannot use both LaTeX and HTML in the same session.\n"); print2( "You must EXIT and restart Metamath to switch to the other.\n"); continue; } else { if (!g_altHtmlFlag) { print2( "?You cannot use both HTML and ALT_HTML in the same session.\n"); print2( "You must EXIT and restart Metamath to switch to the other.\n"); continue; } } } *** end of 17-Nov-2015 deletion */ g_htmlFlag = 1; /* Use HTML, not TeX section */ g_altHtmlFlag = 1; /* Use Unicode, not GIF */ /* readTexDefs() rereads based on changes to g_htmlFlag, g_altHtmlFlag */ if (2/*error*/ == readTexDefs(0 /* 1 = check errors only */, 0 /* 1 = no GIF file existence check */ )) { continue; /* An error occurred */ } let(&g_texFileName, "mnemosyne.txt"); g_texFilePtr = fSafeOpen(g_texFileName, "w", 0/*noVersioningFlag*/); if (!g_texFilePtr) { /* Couldn't open file; error message was provided by fSafeOpen */ continue; } print2("Creating Mnemosyne file \"%s\"...\n", g_texFileName); for (s = 1; s <= g_statements; s++) { g_showStatement = s; /* if (strcmp("|-", g_MathToken[ (g_Statement[g_showStatement].mathString)[0]].tokenName)) { subType = SYNTAX; } */ if (!g_Statement[s].labelName[0]) continue; /* No label */ /* 30-Jan-06 nm Added single-character-match wildcard argument */ if (!matchesList(g_Statement[s].labelName, g_fullArg[2], '*', '?')) continue; if (g_Statement[s].type != (char)a_ && g_Statement[s].type != (char)p_) continue; let(&str1, cat("
", " ", g_Statement[g_showStatement].labelName, "", "
", NULL)); fprintf(g_texFilePtr, "%s", str1); let(&str1, cat("",NULL)); fprintf(g_texFilePtr, "%s", str1); j = nmbrLen(g_Statement[g_showStatement].reqHypList); for (i = 0; i < j; i++) { k = g_Statement[g_showStatement].reqHypList[i]; if (g_Statement[k].type != (char)e_ && !(subType == SYNTAX && g_Statement[k].type == (char)f_)) continue; let(&str1, cat("", str1); } let(&str1, "
", g_Statement[k].labelName, "", NULL)); fprintf(g_texFilePtr, "%s", str1); /* Print hypothesis */ let(&str1, ""); /* Free any previous allocation to str1 */ /* getTexLongMath does not return a temporary allocation; must assign str1 directly, not with let(). It will be deallocated with the next let(&str1,...). */ str1 = getTexLongMath(g_Statement[k].mathString, k/*stmt# for err msgs*/); fprintf(g_texFilePtr, "%s
"); fprintf(g_texFilePtr, "%s", str1); let(&str1, "
What is the conclusion?"); fprintf(g_texFilePtr, "%s\n", str1); let(&str1, ""); fprintf(g_texFilePtr, "%s", str1); let(&str1, ""); /* Free any previous allocation to str1 */ /* getTexLongMath does not return a temporary allocation */ str1 = getTexLongMath(g_Statement[s].mathString, s); fprintf(g_texFilePtr, "%s", str1); let(&str1, ""); fprintf(g_texFilePtr, "%s\n",str1); } /* for(s=1;s j-3) { print2("At least %ld bytes of memory are free.\n",j); } else { print2("%ld bytes of memory are free.\n",i); } continue; } /* 21-Jun-2014 */ if (cmdMatches("SHOW ELAPSED_TIME")) { timeTotal = getRunTime(&timeIncr); print2( "Time since last SHOW ELAPSED_TIME command = %6.2f s; total = %6.2f s\n", timeIncr, timeTotal); continue; } /* if (cmdMatches("SHOW ELAPSED_TIME")) */ if (cmdMatches("SHOW TRACE_BACK")) { /* Pre-21-May-2008 for (i = 1; i <= g_statements; i++) { if (!strcmp(g_fullArg[2],g_Statement[i].labelName)) break; } if (i > g_statements) { printLongLine(cat("?There is no statement with label \"", g_fullArg[2], "\". ", "Use SHOW LABELS for a list of valid labels.", NULL), "", " "); g_showStatement = 0; continue; } */ essentialFlag = 0; axiomFlag = 0; endIndent = 0; i = switchPos("/ ESSENTIAL"); if (i) essentialFlag = 1; /* Limit trace to essential steps only */ i = switchPos("/ ALL"); if (i) essentialFlag = 0; i = switchPos("/ AXIOMS"); if (i) axiomFlag = 1; /* Limit trace printout to axioms */ i = switchPos("/ DEPTH"); /* Limit depth of printout */ if (i) endIndent = (long)val(g_fullArg[i + 1]); /* 19-May-2013 nm */ i = switchPos("/ COUNT_STEPS"); countStepsFlag = (i != 0 ? 1 : 0); i = switchPos("/ TREE"); treeFlag = (i != 0 ? 1 : 0); i = switchPos("/ MATCH"); matchFlag = (i != 0 ? 1 : 0); if (matchFlag) { let(&matchList, g_fullArg[i + 1]); } else { let(&matchList, ""); } i = switchPos("/ TO"); if (i != 0) { let(&traceToList, g_fullArg[i + 1]); } else { let(&traceToList, ""); } if (treeFlag) { if (axiomFlag) { print2( "(Note: The AXIOMS switch is ignored in TREE mode.)\n"); } if (countStepsFlag) { print2( "(Note: The COUNT_STEPS switch is ignored in TREE mode.)\n"); } if (matchFlag) { print2( "(Note: The MATCH list is ignored in TREE mode.)\n"); } } else { if (endIndent != 0) { print2( "(Note: The DEPTH is ignored if the TREE switch is not used.)\n"); } if (countStepsFlag) { if (matchFlag) { print2( "(Note: The MATCH list is ignored in COUNT_STEPS mode.)\n"); } } } /* 21-May-2008 nm Added wildcard handling */ g_showStatement = 0; for (i = 1; i <= g_statements; i++) { if (g_Statement[i].type != (char)p_) continue; /* Not a $p statement; skip it */ /* Wildcard matching */ if (!matchesList(g_Statement[i].labelName, g_fullArg[2], '*', '?')) continue; g_showStatement = i; /*** start of 19-May-2013 deletion j = switchPos("/ TREE"); if (j) { if (axiomFlag) { print2( "(Note: The AXIOMS switch is ignored in TREE mode.)\n"); } if (switchPos("/ COUNT_STEPS")) { print2( "(Note: The COUNT_STEPS switch is ignored in TREE mode.)\n"); } traceProofTree(g_showStatement, essentialFlag, endIndent); } else { if (endIndent != 0) { print2( "(Note: The DEPTH is ignored if the TREE switch is not used.)\n"); } j = switchPos("/ COUNT_STEPS"); if (j) { countSteps(g_showStatement, essentialFlag); } else { traceProof(g_showStatement, essentialFlag, axiomFlag); } } *** end of 19-May-2013 deletion */ /* 19-May-2013 nm - move /TREE and /COUNT_STEPS to outside loop, assigning new variables, for cleaner code. */ if (treeFlag) { traceProofTree(g_showStatement, essentialFlag, endIndent); } else { if (countStepsFlag) { countSteps(g_showStatement, essentialFlag); } else { traceProof(g_showStatement, essentialFlag, axiomFlag, matchList, /* 19-May-2013 nm */ traceToList, /* 18-Jul-2015 nm */ 0 /* testOnlyFlag */ /* 20-May-2013 nm */); } } /* 21-May-2008 nm Added wildcard handling */ } /* next i */ if (g_showStatement == 0) { printLongLine(cat("?There are no $p labels matching \"", g_fullArg[2], "\". ", "See HELP SHOW TRACE_BACK for matching rules.", NULL), "", " "); } let(&matchList, ""); /* Deallocate memory */ let(&traceToList, ""); /* Deallocate memory */ continue; } /* if (cmdMatches("SHOW TRACE_BACK")) */ if (cmdMatches("SHOW USAGE")) { /* 7-Jan-2008 nm Added / ALL qualifier */ if (switchPos("/ ALL")) { m = 1; /* Always include $e, $f statements */ } else { m = 0; /* If wildcards are used, show $a, $p only */ } g_showStatement = 0; for (i = 1; i <= g_statements; i++) { /* 7-Jan-2008 */ /* 7-Jan-2008 nm Added wildcard handling */ if (!g_Statement[i].labelName[0]) continue; /* No label */ if (!m && g_Statement[i].type != (char)p_ && g_Statement[i].type != (char)a_ /* A wildcard-free user-specified statement is always matched even if it's a $e, i.e. it overrides omission of / ALL */ && (instr(1, g_fullArg[2], "*") || instr(1, g_fullArg[2], "?"))) continue; /* No /ALL switch and wildcard and not $p, $a */ /* Wildcard matching */ if (!matchesList(g_Statement[i].labelName, g_fullArg[2], '*', '?')) continue; g_showStatement = i; recursiveFlag = 0; j = switchPos("/ RECURSIVE"); if (j) recursiveFlag = 1; /* Recursive (indirect) usage */ j = switchPos("/ DIRECT"); if (j) recursiveFlag = 0; /* Direct references only */ let(&str1, ""); str1 = traceUsage(g_showStatement, recursiveFlag, 0 /* cutoffStmt */); /************* 18-Jul-2015 nm Start of deleted code ************/ /* /@ Count the number of statements = # of spaces @/ k = (long)strlen(str1) - (long)strlen(edit(str1, 2)); if (!k) { printLongLine(cat("Statement \"", g_Statement[g_showStatement].labelName, "\" is not referenced in the proof of any statement.", NULL), "", " "); } else { if (recursiveFlag) { let(&str2, "\" directly or indirectly affects"); } else { let(&str2, "\" is directly referenced in"); } if (k == 1) { printLongLine(cat("Statement \"", g_Statement[g_showStatement].labelName, str2, " the proof of ", str((double)k), " statement:", NULL), "", " "); } else { printLongLine(cat("Statement \"", g_Statement[g_showStatement].labelName, str2, " the proofs of ", str((double)k), " statements:", NULL), "", " "); } } if (k) { let(&str1, cat(" ", str1, NULL)); } else { let(&str1, " (None)"); } /@ Print the output @/ printLongLine(str1, " ", " "); */ /********* 18-Jul-2015 nm End of deleted code ****************/ /************* 18-Jul-2015 nm Start of new code ************/ /* 18-Jul-2015 nm */ /* str1[0] will be 'Y' or 'N' depending on whether there are any statements. str1[i] will be 'Y' or 'N' depending on whether g_Statement[i] uses g_showStatement. */ /* Count the number of statements k = # of 'Y' */ k = 0; if (str1[0] == 'Y') { /* There is at least one statement using g_showStatement */ for (j = g_showStatement + 1; j <= g_statements; j++) { if (str1[j] == 'Y') { k++; } else { if (str1[j] != 'N') bug(1124); /* Must be 'Y' or 'N' */ } } } else { if (str1[0] != 'N') bug(1125); /* Must be 'Y' or 'N' */ } if (k == 0) { printLongLine(cat("Statement \"", g_Statement[g_showStatement].labelName, "\" is not referenced in the proof of any statement.", NULL), "", " "); } else { if (recursiveFlag) { let(&str2, "\" directly or indirectly affects"); } else { let(&str2, "\" is directly referenced in"); } if (k == 1) { printLongLine(cat("Statement \"", g_Statement[g_showStatement].labelName, str2, " the proof of ", str((double)k), " statement:", NULL), "", " "); } else { printLongLine(cat("Statement \"", g_Statement[g_showStatement].labelName, str2, " the proofs of ", str((double)k), " statements:", NULL), "", " "); } } if (k != 0) { let(&str3, " "); /* Line buffer */ for (j = g_showStatement + 1; j <= g_statements; j++) { if (str1[j] == 'Y') { /* Since the output list could be huge, don't build giant string (very slow) but output it line by line */ if ((long)strlen(str3) + 1 + (long)strlen(g_Statement[j].labelName) > g_screenWidth) { /* Output and reset the line buffer */ print2("%s\n", str3); let(&str3, " "); } let(&str3, cat(str3, " ", g_Statement[j].labelName, NULL)); } } if (strlen(str3) > 1) print2("%s\n", str3); let(&str3, ""); } else { print2(" (None)\n"); } /* if (k != 0) */ /********* 18-Jul-2015 nm End of new code ****************/ } /* next i (statement matching wildcard list) */ if (g_showStatement == 0) { printLongLine(cat("?There are no labels matching \"", g_fullArg[2], "\". ", "See HELP SHOW USAGE for matching rules.", NULL), "", " "); } continue; } /* if cmdMatches("SHOW USAGE") */ if (cmdMatches("SHOW PROOF") || cmdMatches("SHOW NEW_PROOF") || cmdMatches("SAVE PROOF") || cmdMatches("SAVE NEW_PROOF") || cmdMatches("MIDI")) { if (switchPos("/ HTML")) { print2("?HTML qualifier is obsolete - use SHOW STATEMENT * / HTML\n"); continue; } /* 3-May-2016 nm */ if (cmdMatches("SAVE NEW_PROOF") && getMarkupFlag(g_proveStatement, PROOF_DISCOURAGED)) { if (switchPos("/ OVERRIDE") == 0 && g_globalDiscouragement == 1) { /* print2("\n"); */ /* Enable for more emphasis */ print2( ">>> ?Error: Attempt to overwrite a proof whose modification is discouraged.\n"); print2( ">>> Use SAVE NEW_PROOF ... / OVERRIDE if you really want to do this.\n"); /* print2("\n"); */ /* Enable for more emphasis */ continue; } else { /* print2("\n"); */ /* Enable for more emphasis */ print2( ">>> ?Warning: You are overwriting a proof whose modification is discouraged.\n"); /* print2("\n"); */ /* Enable for more emphasis */ } } if (cmdMatches("SHOW PROOF") || cmdMatches("SAVE PROOF")) { pipFlag = 0; } else { pipFlag = 1; /* Proof-in-progress (NEW_PROOF) flag */ } if (cmdMatches("SHOW")) { saveFlag = 0; } else { saveFlag = 1; /* The command is SAVE PROOF */ } /* 16-Aug-2016 nm */ printTime = 0; if (switchPos("/ TIME") != 0) { /* / TIME legal in SAVE mode only */ printTime = 1; } /* 27-Dec-2013 nm */ i = switchPos("/ OLD_COMPRESSION"); if (i) { if (!switchPos("/ COMPRESSED")) { print2("?/ OLD_COMPRESSION must be accompanied by / COMPRESSED.\n"); continue; } } /* 2-Mar-2016 nm */ i = switchPos("/ FAST"); if (i) { if (!switchPos("/ COMPRESSED") && !switchPos("/ PACKED")) { print2("?/ FAST must be accompanied by / COMPRESSED or / PACKED.\n"); continue; } fastFlag = 1; } else { fastFlag = 0; } /* 2-Mar-2016 nm */ if (switchPos("/ EXPLICIT")) { if (switchPos("/ COMPRESSED")) { print2("?/ COMPRESSED and / EXPLICIT may not be used together.\n"); continue; } else if (switchPos("/ NORMAL")) { print2("?/ NORMAL and / EXPLICIT may not be used together.\n"); continue; } } if (switchPos("/ NORMAL")) { if (switchPos("/ COMPRESSED")) { print2("?/ NORMAL and / COMPRESSED may not be used together.\n"); continue; } } /* Establish defaults for omitted qualifiers */ startStep = 0; endStep = 0; /* startIndent = 0; */ /* Not used */ endIndent = 0; /*essentialFlag = 0;*/ essentialFlag = 1; /* 10/9/99 - friendlier default */ renumberFlag = 0; unknownFlag = 0; notUnifiedFlag = 0; reverseFlag = 0; detailStep = 0; noIndentFlag = 0; splitColumn = DEFAULT_COLUMN; skipRepeatedSteps = 0; /* 28-Jun-2013 nm */ texFlag = 0; i = switchPos("/ FROM_STEP"); if (i) startStep = (long)val(g_fullArg[i + 1]); i = switchPos("/ TO_STEP"); if (i) endStep = (long)val(g_fullArg[i + 1]); i = switchPos("/ DEPTH"); if (i) endIndent = (long)val(g_fullArg[i + 1]); /* 10/9/99 - ESSENTIAL is retained for downwards compatibility, but is now the default, so we ignore it. */ /* i = switchPos("/ ESSENTIAL"); if (i) essentialFlag = 1; */ i = switchPos("/ ALL"); if (i) essentialFlag = 0; if (i && switchPos("/ ESSENTIAL")) { print2("?You may not specify both / ESSENTIAL and / ALL.\n"); continue; } i = switchPos("/ RENUMBER"); if (i) renumberFlag = 1; i = switchPos("/ UNKNOWN"); if (i) unknownFlag = 1; i = switchPos("/ NOT_UNIFIED"); /* pip mode only */ if (i) notUnifiedFlag = 1; i = switchPos("/ REVERSE"); if (i) reverseFlag = 1; i = switchPos("/ LEMMON"); if (i) noIndentFlag = 1; i = switchPos("/ START_COLUMN"); if (i) splitColumn = (long)val(g_fullArg[i + 1]); i = switchPos("/ NO_REPEATED_STEPS"); /* 28-Jun-2013 nm */ if (i) skipRepeatedSteps = 1; /* 28-Jun-2013 nm */ /* 8-Dec-2018 nm */ /* If NO_REPEATED_STEPS is specified, indentation (tree) mode will be misleading because a hypothesis assignment will be suppressed if the same assignment occurred earlier, i.e. it is no longer a "tree". */ if (skipRepeatedSteps == 1 && noIndentFlag == 0) { print2("?You must specify / LEMMON with / NO_REPEATED_STEPS\n"); continue; } i = switchPos("/ TEX") || switchPos("/ HTML") /* 14-Sep-2010 nm Added OLDE_TEX */ || switchPos("/ OLD_TEX"); if (i) texFlag = 1; /* 14-Sep-2010 nm Added OLD_TEX */ g_oldTexFlag = 0; if (switchPos("/ OLD_TEX")) g_oldTexFlag = 1; if (cmdMatches("MIDI")) { /* 8/28/00 */ g_midiFlag = 1; pipFlag = 0; saveFlag = 0; let(&labelMatch, g_fullArg[1]); i = switchPos("/ PARAMETER"); /* MIDI only */ if (i) { let(&g_midiParam, g_fullArg[i + 1]); } else { let(&g_midiParam, ""); } } else { g_midiFlag = 0; if (!pipFlag) let(&labelMatch, g_fullArg[2]); } if (texFlag) { if (!g_texFileOpenFlag) { print2( "?You have not opened a %s file. Use the OPEN %s command first.\n", g_htmlFlag ? "HTML" : "LaTeX", g_htmlFlag ? "HTML" : "TEX"); continue; } /**** this is now done after outputting print2("The %s source was written to \"%s\".\n", g_htmlFlag ? "HTML" : "LaTeX", g_texFileName); */ } i = switchPos("/ DETAILED_STEP"); /* non-pip mode only */ if (i) { detailStep = (long)val(g_fullArg[i + 1]); if (!detailStep) detailStep = -1; /* To use as flag; error message will occur in showDetailStep() */ } /*??? Need better warnings for switch combinations that don't make sense */ /* 2-Jan-2017 nm */ /* Print a single message for "/compressed/fast" */ if (switchPos("/ COMPRESSED") && fastFlag && !strcmp("*", labelMatch)) { print2( "Reformatting and saving (but not recompressing) all proofs...\n"); } q = 0; /* Flag that at least one matching statement was found */ for (stmt = 1; stmt <= g_statements; stmt++) { /* If pipFlag (NEW_PROOF), we will iterate exactly once. This loop of course will be entered because there is a least one statement, and at the end of the s loop we break out of it. */ /* If !pipFlag, get the next statement: */ if (!pipFlag) { if (g_Statement[stmt].type != (char)p_) continue; /* Not $p */ /* 30-Jan-06 nm Added single-character-match wildcard argument */ if (!matchesList(g_Statement[stmt].labelName, labelMatch, '*', '?')) continue; g_showStatement = stmt; } q = 1; /* Flag that at least one matching statement was found */ if (detailStep) { /* Show the details of just one step */ showDetailStep(g_showStatement, detailStep); continue; } if (switchPos("/ STATEMENT_SUMMARY")) { /* non-pip mode only */ /* Just summarize the statements used in the proof */ proofStmtSumm(g_showStatement, essentialFlag, texFlag); continue; } /* 21-Jun-2014 */ if (switchPos("/ SIZE")) { /* non-pip mode only */ /* Just print the size of the stored proof and continue */ let(&str1, space(g_Statement[g_showStatement].proofSectionLen)); memcpy(str1, g_Statement[g_showStatement].proofSectionPtr, (size_t)(g_Statement[g_showStatement].proofSectionLen)); n = instr(1, str1, "$."); if (n == 0) { /* The original source truncates the proof before $. */ n = g_Statement[g_showStatement].proofSectionLen; } else { /* If a proof is saved, it includes the $. (Should we revisit or document better how/why this is done?) */ n = n - 1; } print2("The proof source for \"%s\" has %ld characters.\n", g_Statement[g_showStatement].labelName, n); continue; } if (switchPos("/ PACKED") || switchPos("/ NORMAL") || switchPos("/ COMPRESSED") || switchPos("/ EXPLICIT") || saveFlag) { /*??? Add error msg if other switches were specified. (Ignore them.)*/ /* 16-Aug-2016 nm */ if (saveFlag) { if (printTime == 1) { getRunTime(&timeIncr); /* This call just resets the time */ } } if (!pipFlag) { outStatement = g_showStatement; } else { outStatement = g_proveStatement; } explicitTargets = (switchPos("/ EXPLICIT") != 0) ? 1 : 0; /* Get the amount to indent the proof by */ indentation = 2 + getSourceIndentation(outStatement); if (!pipFlag) { parseProof(g_showStatement); /* Prints message if severe error */ if (g_WrkProof.errorSeverity > 1) { /* 21-Aug-04 nm */ /* Prevent bugtrap in nmbrSquishProof -> */ /* nmbrGetSubProofLen if proof corrupted */ print2( "?The proof has a severe error and cannot be displayed or saved.\n"); continue; } /* verifyProof(g_showStatement); */ /* Not necessary */ if (fastFlag) { /* 2-Mar-2016 nm */ /* 2-Mar-2016 nm */ /* Use the proof as is */ nmbrLet(&nmbrSaveProof, g_WrkProof.proofString); } else { /* Make sure the proof is uncompressed */ nmbrLet(&nmbrSaveProof, nmbrUnsquishProof(g_WrkProof.proofString)); } } else { nmbrLet(&nmbrSaveProof, g_ProofInProgress.proof); } if (switchPos("/ PACKED") || switchPos("/ COMPRESSED")) { if (!fastFlag) { /* 2-Mar-2016 nm */ nmbrLet(&nmbrSaveProof, nmbrSquishProof(nmbrSaveProof)); } } if (switchPos("/ COMPRESSED")) { let(&str1, compressProof(nmbrSaveProof, outStatement, /* g_showStatement or g_proveStatement based on pipFlag */ (switchPos("/ OLD_COMPRESSION")) ? 1 : 0 /* 27-Dec-2013 nm */ )); } else { let(&str1, nmbrCvtRToVString(nmbrSaveProof, /* 25-Jan-2016 nm */ explicitTargets, /*explicitTargets*/ outStatement /*statemNum, used only if explicitTargets*/)); } if (saveFlag) { /* ??? This is a problem when mixing html and save proof */ if (g_printString[0]) bug(1114); let(&g_printString, ""); /* Set flag for print2() to put output in g_printString instead of displaying it on the screen */ g_outputToString = 1; } else { if (!print2("Proof of \"%s\":\n", g_Statement[outStatement].labelName)) break; /* Break for speedup if user quit */ print2( "---------Clip out the proof below this line to put it in the source file:\n"); /* 19-Apr-2015 so */ /* 24-Apr-2015 nm Reverted */ /*print2("\n");*/ /* Add a blank line to make clipping easier */ } if (switchPos("/ COMPRESSED")) { printLongLine(cat(space(indentation), str1, " $.", NULL), space(indentation), "& "); /* "&" is special flag to break compressed part of proof anywhere */ } else { printLongLine(cat(space(indentation), str1," $.", NULL), space(indentation), " "); } /* 24-Apr-2015 nm */ l = (long)(strlen(str1)); /* Save length for printout below */ /* 3-May-2017 nm Rewrote the if block below */ /* 12-Jun-2011 nm Removed pipFlag condition so that a date stamp will always be created if it doesn't exist */ if /*(pipFlag)*/ (1 /* Add the date proof was created */ /* 19-Apr-2015 so */ /* SOREAR Only generate date if the proof looks complete. This is not intended as a grading mechanism, just trying to avoid premature output */ && !nmbrElementIn(1, nmbrSaveProof, -(long)'?')) { /* 3-May-2017 nm */ /* Add a "(Contributed by...)" date if it isn't there */ let(&str2, ""); str2 = getContrib(outStatement, CONTRIBUTOR); if (str2[0] == 0) { /* The is no contributor, so add one */ /* 14-May-2017 nm */ /* See if there is a date below the proof (for converting old .mm files). Someday this will be obsolete, with str3 and str4 always returned as "". */ getProofDate(outStatement, &str3, &str4); /* If there are two dates below the proof, the first on is the revision date and the second the "Contributed by" date. */ if (str4[0] != 0) { /* There are 2 dates below the proof */ let(&str5, str3); /* 1st date is Revised by... */ let(&str3, str4); /* 2nd date is Contributed by... */ } else { let(&str5, ""); } /* If there is no date below proof, use today's date */ if (str3[0] == 0) let(&str3, date()); let(&str4, cat("\n", space(indentation + 1), /*"(Contributed by ?who?, ", date(), ".) ", NULL));*/ "(Contributed by ", g_contributorName, ", ", str3, ".) ", NULL)); /* 14-May-2017 nm */ /* If there is a 2nd date below proof, add a "(Revised by..." tag */ if (str5[0] != 0) { /* Use the DEFAULT_CONTRIBUTOR ?who? because we don't know the reviser name (using the contributor name may be incorrect). Also, this will trigger a warning in VERIFY MARKUP since it may be a proof shortener rather than a reviser. */ let(&str4, cat(str4, "\n", space(indentation + 1), "(Revised by ", DEFAULT_CONTRIBUTOR, ", ", str5, ".) ", NULL)); /* 15-May-2017 nm */ } let(&str3, space(g_Statement[outStatement].labelSectionLen)); /* str3 will have the statement's label section w/ comment */ memcpy(str3, g_Statement[outStatement].labelSectionPtr, (size_t)(g_Statement[outStatement].labelSectionLen)); i = rinstr(str3, "$)"); /* The last "$)" occurrence */ if (i != 0 /* A description comment exists */ && saveFlag) { /* and we are saving the proof */ /* This isn't a perfect wrapping but we assume 'write source .../rewrap' will be done eventually. */ /* str3 will have the updated comment */ let(&str3, cat(left(str3, i - 1), str4, right(str3, i), NULL)); if (g_Statement[outStatement].labelSectionChanged == 1) { /* Deallocate old comment if not original source */ let(&str4, ""); /* Deallocate any previous str4 content */ str4 = g_Statement[outStatement].labelSectionPtr; let(&str4, ""); /* Deallocate the old content */ } /* Set flag that this is not the original source */ g_Statement[outStatement].labelSectionChanged = 1; g_Statement[outStatement].labelSectionLen = (long)strlen(str3); /* We do a direct assignment instead of let(&...) because labelSectionPtr may point to the middle of the giant input file buffer, which we don't want to deallocate */ g_Statement[outStatement].labelSectionPtr = str3; /* Reset str3 without deallocating with let(), since it was assigned to labelSectionPtr */ str3 = ""; /* Reset the cache for this statement in getContrib() */ str3 = getContrib(outStatement, GC_RESET_STMT); } /* if i != 0 */ #ifdef DATE_BELOW_PROOF /* 12-May-2017 nm */ /* Add a date below the proof. It actually goes in the label section of the next statement; the proof section is not changed. */ /* (This will become obsolete eventually) */ let(&str3, space(g_Statement[outStatement + 1].labelSectionLen)); /* str3 will have the next statement's label section w/ comment */ memcpy(str3, g_Statement[outStatement + 1].labelSectionPtr, (size_t)(g_Statement[outStatement + 1].labelSectionLen)); let(&str5, ""); /* We need to guarantee this for the screen printout later */ if (instr(1, str3, "$( [") == 0) { /* There is no date below proof (if there is, don't do anything; if it is wrong, 'verify markup' will check it) */ /* Save str5 for screen printout later! */ let(&str5, cat(space(indentation), "$( [", date(), "] $)", NULL)); /* str4 will be used for the screen printout later */ if (saveFlag) { /* save proof, not show proof */ if (g_Statement[outStatement + 1].labelSectionChanged == 1) { /* Deallocate old comment if not original source */ let(&str4, ""); /* Deallocate any previous str4 content */ str4 = g_Statement[outStatement + 1].labelSectionPtr; let(&str4, ""); /* Deallocate the old content */ } /* str3 starts after the "$." ending the proof, and should start with "\n" */ let(&str3, edit(str3, 8/* Discard leading spaces and tabs */)); if (str3[0] != '\n') let(&str3, cat("\n", str3, NULL)); /* Add the date after the proof */ let(&str3, cat("\n", str5, str3, NULL)); /* Set flag that this is not the original source */ g_Statement[outStatement + 1].labelSectionChanged = 1; g_Statement[outStatement + 1].labelSectionLen = (long)strlen(str3); /* We do a direct assignment instead of let(&...) because labelSectionPtr may point to the middle of the giant input file buffer, which we don't want to deallocate */ g_Statement[outStatement + 1].labelSectionPtr = str3; /* Reset str3 without deallocating with let(), since it was assigned to labelSectionPtr */ str3 = ""; /* Reset the cache for this statement in getContrib() */ str3 = getContrib(outStatement + 1, GC_RESET_STMT); } /* if saveFlag */ } /* if (instr(1, str3, "$( [") == 0) */ #endif /* end #ifdef DATE_BELOW_PROOF */ /* 12-May-2017 nm */ } /* if str2[0] == 0 */ /* At this point, str4 contains the "$( [date] $)" comment if it would have been added to the saved proof, for use by "show proof" */ /********* deleted 3-May-2017 - date below proof is obsolete /@ 12-Jun-2011 nm Removed pipFlag condition so that a date stamp will always be created if it doesn't exist @/ if ( /@ pipFlag && @/ !instr(1, str2, "$([") /@ 7-Sep-04 Allow both "$([])$" and "$( [] )$" @/ /@ 19-Apr-2015 so @/ /@ SOREAR Only generate date if the proof looks complete. This is not intended as a grading mechanism, just trying to avoid premature output @/ && !nmbrElementIn(1, nmbrSaveProof, -(long)'?') && !instr(1, str2, "$( [")) { /@ 6/13/98 end @/ /@ No date stamp existed before. Create one for today's date. Note that the characters after "$." at the end of the proof normally go in the labelSection of the next statement, but a special mode in outputStatement() (in mmpars.c) will output the date stamp characters for a saved proof. @/ /@ print2("%s$([%s]$)\n", space(indentation), date()); @/ /@ 4/23/04 nm Initialize with a "?" date followed by today's date. The "?" date can be edited by the user when the proof is becomes "official." @/ /@print2("%s$([?]$) $([%s]$)\n", space(indentation), date());@/ /@ 7-Sep-04 Put space around "[]" @/ /@print2("%s$( [?] $) $( [%s] $)\n", space(indentation), date());@/ /@ 30-Nov-2013 remove the unknown date placeholder @/ print2("%s$( [%s] $)\n", space(indentation), date()); } else { if (saveFlag && (instr(1, str2, "$([") /@ 7-Sep-04 Allow both "$([])$" and "$( [] )$" @/ || instr(1, str2, "$( ["))) { /@ An old date stamp existed, and we're saving the proof to the output file. Make sure the indentation of the old date stamp (which exists in the labelSection of the next statement) matches the indentation of the saved proof. To do this, we "delete" the indentation spaces on the old date in the labelSection of the next statement, and we put the actual required indentation spaces at the end of the saved proof. This is done because the labelSectionPtr of the next statement does not point to an isolated string that can be allocated/deallocated but rather to a place in the input source buffer. @/ /@ Correct the indentation on old date @/ while ((g_Statement[outStatement + 1].labelSectionPtr)[0] != '$') { /@ "Delete" spaces before old date (by moving source buffer pointer forward), and also "delete" the \n that comes before those spaces @/ /@ If the proof is saved a 2nd time, this loop will not be entered because the pointer will already be at the "$". @/ (g_Statement[outStatement + 1].labelSectionPtr)++; (g_Statement[outStatement + 1].labelSectionLen)--; } if (!g_outputToString) bug(1115); /@ The final \n will not appear in final output (done in outputStatement() in mmpars.c) because the proofSectionLen below is adjusted to omit it. This will allow the space(indentation) to appear before the old date without an intervening \n. @/ print2("%s\n", space(indentation)); } } ******** end of deletion 3-May-2017 ******/ } /* if / *(pipFlag)* / (1) */ if (saveFlag) { g_sourceChanged = 1; g_proofChanged = 0; if (processUndoStack(NULL, PUS_GET_STATUS, "", 0)) { /* The UNDO stack may not be empty */ proofSavedFlag = 1; /* UNDO stack empty no longer reliably indicates that proof hasn't changed */ } /******** deleted 3-May-2017 nm (before proofSectionChanged added) /@ ASCII 1 is a flag that string was allocated and not part of original source file text buffer @/ let(&g_printString, cat(chr(1), "\n", g_printString, NULL)); if (g_Statement[outStatement].proofSectionPtr[-1] == 1) { /@ Deallocate old proof if not original source @/ let(&str1, ""); /@ Deallocate any previous str1 content @/ str1 = g_Statement[outStatement].proofSectionPtr - 1; let(&str1, ""); /@ Deallocate the proof section @/ } g_Statement[outStatement].proofSectionPtr = g_printString + 1; /@ Subtr 1 char for ASCII 1 at beg, 1 char for "\n" at the end (which is the first char of next statement's labelSection) @/ g_Statement[outStatement].proofSectionLen = (long)strlen(g_printString) - 2; /@ Reset g_printString without deallocating @/ g_printString = ""; g_outputToString = 0; **********/ /* 3-May-2017 nm */ /* Add an initial \n which will go after the "$=" and the beginning of the proof */ let(&g_printString, cat("\n", g_printString, NULL)); if (g_Statement[outStatement].proofSectionChanged == 1) { /* Deallocate old proof if not original source */ let(&str1, ""); /* Deallocate any previous str1 content */ str1 = g_Statement[outStatement].proofSectionPtr; let(&str1, ""); /* Deallocate the proof section */ } /* Set flag that this is not the original source */ g_Statement[outStatement].proofSectionChanged = 1; if (strcmp(" $.\n", right(g_printString, (long)strlen(g_printString) - 3))) { bug(1128); } /* Note that g_printString ends with "$.\n", but those 3 characters should not be in the proofSection. (The "$." keyword is added between proofSection and next labelSection when the output is written by writeOutput.) Thus we subtract 3 from the length. But there is no need to truncate the string; later deallocation will take care of the whole string. */ g_Statement[outStatement].proofSectionLen = (long)strlen(g_printString) - 3; /* We do a direct assignment instead of let(&...) because proofSectionPtr may point to the middle of the giant input file string, which we don't want to deallocate */ g_Statement[outStatement].proofSectionPtr = g_printString; /* Reset g_printString without deallocating with let(), since it was assigned to proofSectionPtr */ g_printString = ""; g_outputToString = 0; if (!pipFlag) { if (!(fastFlag && !strcmp("*", labelMatch))) { printLongLine( cat("The proof of \"", g_Statement[outStatement].labelName, "\" has been reformatted and saved internally.", NULL), "", " "); } } else { printLongLine(cat("The new proof of \"", g_Statement[outStatement].labelName, "\" has been saved internally.", NULL), "", " "); } /* 16-Aug-2016 nm */ if (printTime == 1) { getRunTime(&timeIncr); print2("SAVE PROOF run time = %6.2f sec for \"%s\"\n", timeIncr, g_Statement[outStatement].labelName); } } else { #ifdef DATE_BELOW_PROOF /* 12-May-2017 nm */ /* Print the date on the screen if it would be added to the file */ if (str5[0] != 0) print2("%s\n", str5); #endif /*#ifdef DATE_BELOW_PROOF*/ /* 12-May-2017 nm */ /* 19-Apr-2015 so */ /* 24-Apr-2015 nm Reverted */ /*print2("\n");*/ /* Add a blank line to make clipping easier */ print2(cat( "---------The proof of \"", g_Statement[outStatement].labelName, /* "\" to clip out ends above this line.\n",NULL)); */ /* 24-Apr-2015 nm */ "\" (", str((double)l), " bytes) ends above this line.\n", NULL)); } /* End if saveFlag */ nmbrLet(&nmbrSaveProof, NULL_NMBRSTRING); if (pipFlag) break; /* Only one iteration for NEW_PROOF stuff */ continue; /* to next s iteration */ } /* end if (switchPos("/ PACKED") || switchPos("/ NORMAL") || switchPos("/ COMPRESSED") || switchPos("/ EXPLICIT") || saveFlag) */ if (saveFlag) bug(1112); /* Shouldn't get here */ if (!pipFlag) { outStatement = g_showStatement; } else { outStatement = g_proveStatement; } if (texFlag) { g_outputToString = 1; /* Flag for print2 to add to g_printString */ if (!g_htmlFlag) { if (!g_oldTexFlag) { /* 14-Sep-2010 nm */ print2("\\begin{proof}\n"); print2("\\begin{align}\n"); } else { print2("\n"); print2("\\vspace{1ex} %%1\n"); printLongLine(cat("Proof of ", "{\\tt ", asciiToTt(g_Statement[outStatement].labelName), "}:", NULL), "", " "); print2("\n"); print2("\n"); } } else { /* g_htmlFlag */ bug(1118); /*???? The code below is obsolete - now down in show statement*/ /* print2("
\n", MINT_BACKGROUND_COLOR); print2("", NULL), "", "\""); print2( "\n"); */ } g_outputToString = 0; /* 8/26/99: Obsolete: */ /* printTexLongMath in typeProof will do this fprintf(g_texFilePtr, "%s", g_printString); let(&g_printString, ""); */ /* 8/26/99: printTeXLongMath now clears g_printString in LaTeX mode before starting its output, so we must put out the g_printString ourselves here */ fprintf(g_texFilePtr, "%s", g_printString); let(&g_printString, ""); /* We'll clr it anyway */ } else { /* !texFlag */ /* Terminal output - display the statement if wildcard is used */ if (!pipFlag) { /* 30-Jan-06 nm Added single-character-match wildcard argument */ if (instr(1, labelMatch, "*") || instr(1, labelMatch, "?")) { if (!print2("Proof of \"%s\":\n", g_Statement[outStatement].labelName)) break; /* Break for speedup if user quit */ } } } if (texFlag) print2("Outputting proof of \"%s\"...\n", g_Statement[outStatement].labelName); typeProof(outStatement, pipFlag, startStep, endStep, endIndent, essentialFlag, /* 1-May-2017 nm */ /* In SHOW PROOF xxx /TEX, we use renumber steps mode so that the first step is step 1. The step number is checked for step 1 in mmwtex.c to prevent a spurious \\ (newline) at the start of the proof. Note that SHOW PROOF is not available in HTML mode, so texFlag will always mean LaTeX mode here. */ (texFlag ? 1 : renumberFlag), /*was: renumberFlag,*/ unknownFlag, notUnifiedFlag, reverseFlag, /* 1-May-2017 nm */ /* In SHOW PROOF xxx /TEX, we use Lemmon mode so that the hypothesis reference list will be available. Note that SHOW PROOF is not available in HTML mode, so texFlag will always mean LaTeX mode here. */ (texFlag ? 1 : noIndentFlag), /*was: noIndentFlag,*/ splitColumn, skipRepeatedSteps, /* 28-Jun-2013 nm */ texFlag, g_htmlFlag); if (texFlag) { if (!g_htmlFlag) { /* 14-Sep-2010 nm */ if (!g_oldTexFlag) { g_outputToString = 1; print2("\\end{align}\n"); print2("\\end{proof}\n"); print2("\n"); g_outputToString = 0; fprintf(g_texFilePtr, "%s", g_printString); let(&g_printString, ""); } else { } } else { /* g_htmlFlag */ g_outputToString = 1; print2("
Proof of Theorem ", asciiToTt(g_Statement[outStatement].labelName), "
StepHypRef\n"); print2("Expression
\n"); print2("
\n"); /* print trailer will close out string later */ g_outputToString = 0; } } /*???CLEAN UP */ /*nmbrLet(&g_WrkProof.proofString, nmbrSaveProof);*/ /*E*/ if (0) { /* for debugging: */ printLongLine(nmbrCvtRToVString(g_WrkProof.proofString, /* 25-Jan-2016 nm */ 0, /*explicitTargets*/ 0 /*statemNum, used only if explicitTargets*/)," "," "); print2("\n"); nmbrLet(&nmbrSaveProof, nmbrSquishProof(g_WrkProof.proofString)); printLongLine(nmbrCvtRToVString(nmbrSaveProof, /* 25-Jan-2016 nm */ 0, /*explicitTargets*/ 0 /*statemNum, used only if explicitTargets*/)," "," "); print2("\n"); nmbrLet(&nmbrTmp, nmbrUnsquishProof(nmbrSaveProof)); printLongLine(nmbrCvtRToVString(nmbrTmp, /* 25-Jan-2016 nm */ 0, /*explicitTargets*/ 0 /*statemNum, used only if explicitTargets*/)," "," "); nmbrLet(&nmbrTmp, nmbrGetTargetHyp(nmbrSaveProof,g_showStatement)); printLongLine(nmbrCvtAnyToVString(nmbrTmp)," "," "); print2("\n"); nmbrLet(&nmbrTmp, nmbrGetEssential(nmbrSaveProof)); printLongLine(nmbrCvtAnyToVString(nmbrTmp)," "," "); print2("\n"); cleanWrkProof(); /* Deallocate verifyProof storage */ } /* end debugging */ if (pipFlag) break; /* Only one iteration for NEW_PROOF stuff */ } /* Next stmt */ if (!q) { /* No matching statement was found */ printLongLine(cat("?There is no $p statement whose label matches \"", (cmdMatches("MIDI")) ? g_fullArg[1] : g_fullArg[2], "\". ", "Use SHOW LABELS to see list of valid labels.", NULL), "", " "); } else { if (saveFlag) { print2("Remember to use WRITE SOURCE to save changes permanently.\n"); } if (texFlag) { print2("The LaTeX source was written to \"%s\".\n", g_texFileName); /* 14-Sep-2010 nm Added OLD_TEX */ g_oldTexFlag = 0; } } continue; } /* if (cmdMatches("SHOW/SAVE [NEW_]PROOF" or" MIDI") */ /*E*/ /*???????? DEBUG command for debugging only */ if (cmdMatches("DBG")) { print2("DEBUGGING MODE IS FOR DEVELOPER'S USE ONLY!\n"); print2("Argument: %s\n", g_fullArg[1]); nmbrLet(&nmbrTmp, parseMathTokens(g_fullArg[1], g_proveStatement)); for (j = 0; j < 3; j++) { print2("Trying depth %ld\n", j); nmbrTmpPtr = proveFloating(nmbrTmp, g_proveStatement, j, 0, 0, 1/*overrideFlag*/, 1/*mathboxFlag*/); if (nmbrLen(nmbrTmpPtr)) break; } print2("Result: %s\n", nmbrCvtRToVString(nmbrTmpPtr, /* 25-Jan-2016 nm */ 0, /*explicitTargets*/ 0 /*statemNum, used only if explicitTargets*/)); nmbrLet(&nmbrTmpPtr, NULL_NMBRSTRING); continue; } /*E*/ /*???????? DEBUG command for debugging only */ if (cmdMatches("PROVE")) { /* 14-Sep-2012 nm */ /* Get the unique statement matching the g_fullArg[1] pattern */ i = getStatementNum(g_fullArg[1], 1/*startStmt*/, g_statements + 1 /*maxStmt*/, 0/*aAllowed*/, 1/*pAllowed*/, 0/*eAllowed*/, 0/*fAllowed*/, 0/*efOnlyForMaxStmt*/, 1/*uniqueFlag*/); if (i == -1) { continue; /* Error msg was provided if not unique */ } g_proveStatement = i; /* 10-May-2016 nm */ /* 1 means to override usage locks */ overrideFlag = ( (switchPos("/ OVERRIDE")) ? 1 : 0) || g_globalDiscouragement == 0; if (getMarkupFlag(g_proveStatement, PROOF_DISCOURAGED)) { if (overrideFlag == 0) { /* print2("\n"); */ /* Enable for more emphasis */ print2( ">>> ?Error: Modification of this statement's proof is discouraged.\n" ); print2( ">>> You must use PROVE ... / OVERRIDE to work on it.\n"); /* print2("\n"); */ /* Enable for more emphasis */ continue; } } /*********** 14-Sep-2012 replaced by getStatementNum() /@??? Make sure only $p statements are allowed. @/ for (i = 1; i <= g_statements; i++) { if (!strcmp(g_fullArg[1],g_Statement[i].labelName)) break; } if (i > g_statements) { printLongLine(cat("?There is no statement with label \"", g_fullArg[1], "\". ", "Use SHOW LABELS for a list of valid labels.", NULL), "", " "); g_proveStatement = 0; continue; } g_proveStatement = i; if (g_Statement[g_proveStatement].type != (char)p_) { printLongLine(cat("?Statement \"", g_fullArg[1], "\" is not a $p statement.", NULL), "", " "); g_proveStatement = 0; continue; } ************** end of 14-Sep-2012 deletion ************/ print2( "Entering the Proof Assistant. HELP PROOF_ASSISTANT for help, EXIT to exit.\n"); /* Obsolete: print2("You will be working on the proof of statement %s:\n", g_Statement[g_proveStatement].labelName); printLongLine(cat(" $p ", nmbrCvtMToVString( g_Statement[g_proveStatement].mathString), NULL), " ", " "); */ g_PFASmode = 1; /* Set mode for commands here and in mmcmdl.c */ /* Note: Proof Assistant mode can equivalently be determined by: nmbrLen(g_ProofInProgress.proof) != 0 */ parseProof(g_proveStatement); verifyProof(g_proveStatement); /* 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"); nmbrLet(&nmbrSaveProof, nmbrAddElement(NULL_NMBRSTRING, -(long)'?')); } else { nmbrLet(&nmbrSaveProof, g_WrkProof.proofString); } cleanWrkProof(); /* Deallocate verifyProof storage */ /* 11-Sep-2016 nm */ /* Initialize the structure needed for the Proof Assistant */ initProofStruct(&g_ProofInProgress, nmbrSaveProof, g_proveStatement); /****** 11-Sep-2016 nm Replaced by initProofStruct() /@ Right now, only non-packed proofs are handled. @/ nmbrLet(&nmbrSaveProof, nmbrUnsquishProof(nmbrSaveProof)); /@ Assign initial proof structure @/ if (nmbrLen(g_ProofInProgress.proof)) bug(1113); /@ Should've been deall.@/ nmbrLet(&g_ProofInProgress.proof, nmbrSaveProof); i = nmbrLen(g_ProofInProgress.proof); pntrLet(&g_ProofInProgress.target, pntrNSpace(i)); pntrLet(&g_ProofInProgress.source, pntrNSpace(i)); pntrLet(&g_ProofInProgress.user, pntrNSpace(i)); nmbrLet((nmbrString @@)(&((g_ProofInProgress.target)[i - 1])), g_Statement[g_proveStatement].mathString); g_pipDummyVars = 0; /@ Assign known subproofs @/ assignKnownSubProofs(); /@ Initialize remaining steps @/ for (j = 0; j < i/@proof length@/; j++) { if (!nmbrLen((g_ProofInProgress.source)[j])) { initStep(j); } } /@ Unify whatever can be unified @/ autoUnify(0); /@ 0 means no "congrats" message @/ **** end of 11-Sep-2016 deletion ************/ /* print2( "Periodically save your work with SAVE NEW_PROOF and WRITE SOURCE.\n"); print2( "There is no UNDO command yet. You can OPEN LOG to track what you've done.\n"); */ /* Show the user the statement to be proved */ print2("You will be working on statement (from \"SHOW STATEMENT %s\"):\n", g_Statement[g_proveStatement].labelName); typeStatement(g_proveStatement /*g_showStatement*/, 1 /*briefFlag*/, 0 /*commentOnlyFlag*/, 0 /*texFlag*/, 0 /*g_htmlFlag*/); if (!nmbrElementIn(1, g_ProofInProgress.proof, -(long)'?')) { print2( "Note: The proof you are starting with is already complete.\n"); } else { print2( "Unknown step summary (from \"SHOW NEW_PROOF / UNKNOWN\"):\n"); /* 6/14/98 - Automatically display new unknown steps ???Future - add switch to enable/defeat this */ typeProof(g_proveStatement, 1 /*pipFlag*/, 0 /*startStep*/, 0 /*endStep*/, 0 /*endIndent*/, 1 /*essentialFlag*/, 0 /*renumberFlag*/, 1 /*unknownFlag*/, 0 /*notUnifiedFlag*/, 0 /*reverseFlag*/, 0 /*noIndentFlag*/, 0 /*splitColumn*/, 0 /*skipRepeatedSteps*/, /* 28-Jun-2013 nm */ 0 /*texFlag*/, 0 /*g_htmlFlag*/); /* 6/14/98 end */ } /* 3-May-2016 nm */ if (getMarkupFlag(g_proveStatement, PROOF_DISCOURAGED)) { /* print2("\n"); */ /* Enable for more emphasis */ print2( ">>> ?Warning: Modification of this statement's proof is discouraged.\n" ); /* print2( ">>> You must use SAVE NEW_PROOF ... / OVERRIDE to save it.\n"); */ /* print2("\n"); */ /* Enable for more emphasis */ } processUndoStack(NULL, PUS_INIT, "", 0); /* Optional? */ /* Put the initial proof into the UNDO stack; we don't need the info string since it won't be undone */ processUndoStack(&g_ProofInProgress, PUS_PUSH, "", 0); continue; } /* 1-Nov-2013 nm Added UNDO */ if (cmdMatches("UNDO")) { processUndoStack(&g_ProofInProgress, PUS_UNDO, "", 0); g_proofChanged = 1; /* Maybe make this more intelligent some day */ /* 6/14/98 - Automatically display new unknown steps ???Future - add switch to enable/defeat this */ typeProof(g_proveStatement, 1 /*pipFlag*/, 0 /*startStep*/, 0 /*endStep*/, 0 /*endIndent*/, 1 /*essentialFlag*/, 0 /*renumberFlag*/, 1 /*unknownFlag*/, 0 /*notUnifiedFlag*/, 0 /*reverseFlag*/, 0 /*noIndentFlag*/, 0 /*splitColumn*/, 0 /*skipRepeatedSteps*/, /* 28-Jun-2013 nm */ 0 /*texFlag*/, 0 /*g_htmlFlag*/); /* 6/14/98 end */ continue; } /* 1-Nov-2013 nm Added REDO */ if (cmdMatches("REDO")) { processUndoStack(&g_ProofInProgress, PUS_REDO, "", 0); g_proofChanged = 1; /* Maybe make this more intelligent some day */ /* 6/14/98 - Automatically display new unknown steps ???Future - add switch to enable/defeat this */ typeProof(g_proveStatement, 1 /*pipFlag*/, 0 /*startStep*/, 0 /*endStep*/, 0 /*endIndent*/, 1 /*essentialFlag*/, 0 /*renumberFlag*/, 1 /*unknownFlag*/, 0 /*notUnifiedFlag*/, 0 /*reverseFlag*/, 0 /*noIndentFlag*/, 0 /*splitColumn*/, 0 /*skipRepeatedSteps*/, /* 28-Jun-2013 nm */ 0 /*texFlag*/, 0 /*g_htmlFlag*/); /* 6/14/98 end */ continue; } if (cmdMatches("UNIFY")) { m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ g_proofChangedFlag = 0; if (cmdMatches("UNIFY STEP")) { s = (long)val(g_fullArg[2]); /* Step number */ if (s > m || s < 1) { print2("?The step must be in the range from 1 to %ld.\n", m); continue; } interactiveUnifyStep(s - 1, 1); /* 2nd arg. means print msg if already unified */ /* (The interactiveUnifyStep handles all messages.) */ /* print2("... */ autoUnify(1); if (g_proofChangedFlag) { g_proofChanged = 1; /* Cumulative flag */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } continue; } /* "UNIFY ALL" */ if (!switchPos("/ INTERACTIVE")) { autoUnify(1); if (!g_proofChangedFlag) { print2("No new unifications were made.\n"); } else { print2( "Steps were unified. SHOW NEW_PROOF / NOT_UNIFIED to see any remaining.\n"); g_proofChanged = 1; /* Cumulative flag */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } } else { q = 0; while (1) { /* Repeat the unifications over and over until done, since a later unification may improve the ability of an aborted earlier one to be done without timeout */ g_proofChangedFlag = 0; /* This flag is set by autoUnify() and interactiveUnifyStep() */ autoUnify(0); for (s = m - 1; s >= 0; s--) { interactiveUnifyStep(s, 0); /* 2nd arg. means no msg if already unified */ } autoUnify(1); /* 1 means print congratulations if complete */ if (!g_proofChangedFlag) { if (!q) { print2("No new unifications were made.\n"); } else { /* If q=1, then we are in the 2nd or later pass, which means there was a change in the 1st pass. */ print2( "Steps were unified. SHOW NEW_PROOF / NOT_UNIFIED to see any remaining.\n"); g_proofChanged = 1; /* Cumulative flag */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } break; /* while (1) */ } else { q = 1; /* Flag that we're starting a 2nd or later pass */ } } /* End while (1) */ } /* 6/14/98 - Automatically display new unknown steps ???Future - add switch to enable/defeat this */ typeProof(g_proveStatement, 1 /*pipFlag*/, 0 /*startStep*/, 0 /*endStep*/, 0 /*endIndent*/, 1 /*essentialFlag*/, 0 /*renumberFlag*/, 1 /*unknownFlag*/, 0 /*notUnifiedFlag*/, 0 /*reverseFlag*/, 0 /*noIndentFlag*/, 0 /*splitColumn*/, 0 /*skipRepeatedSteps*/, /* 28-Jun-2013 nm */ 0 /*texFlag*/, 0 /*g_htmlFlag*/); /* 6/14/98 end */ continue; } if (cmdMatches("MATCH")) { maxEssential = -1; /* Default: no maximum */ i = switchPos("/ MAX_ESSENTIAL_HYP"); if (i) maxEssential = (long)val(g_fullArg[i + 1]); if (cmdMatches("MATCH STEP")) { s = (long)val(g_fullArg[2]); /* Step number */ m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ if (s > m || s < 1) { print2("?The step must be in the range from 1 to %ld.\n", m); continue; } if ((g_ProofInProgress.proof)[s - 1] != -(long)'?') { print2( "?Step %ld is already assigned. Only unknown steps can be matched.\n", s); continue; } interactiveMatch(s - 1, maxEssential); n = nmbrLen(g_ProofInProgress.proof); /* New proof length */ if (n != m) { if (s != m) { printLongLine(cat("Steps ", str((double)s), ":", str((double)m), " are now ", str((double)(s - m + n)), ":", str((double)n), ".", NULL), "", " "); } else { printLongLine(cat("Step ", str((double)m), " is now step ", str((double)n), ".", NULL), "", " "); } } autoUnify(1); g_proofChanged = 1; /* Cumulative flag */ /* 1-Nov-2013 nm Why is g_proofChanged set unconditionally above? Do we need the processUndoStack() call? */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); continue; } /* End if MATCH STEP */ if (cmdMatches("MATCH ALL")) { m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ k = 0; g_proofChangedFlag = 0; if (switchPos("/ ESSENTIAL")) { nmbrLet(&nmbrTmp, nmbrGetEssential(g_ProofInProgress.proof)); } for (s = m; s > 0; s--) { /* Match only unknown steps */ if ((g_ProofInProgress.proof)[s - 1] != -(long)'?') continue; /* Match only essential steps if specified */ if (switchPos("/ ESSENTIAL")) { if (!nmbrTmp[s - 1]) continue; } interactiveMatch(s - 1, maxEssential); if (g_proofChangedFlag) { k = s; /* Save earliest step changed */ g_proofChangedFlag = 0; } print2("\n"); } if (k) { g_proofChangedFlag = 1; /* Restore it */ g_proofChanged = 1; /* Cumulative flag */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); print2("Steps %ld and above have been renumbered.\n", k); } autoUnify(1); continue; } /* End if MATCH ALL */ } if (cmdMatches("LET")) { g_errorCount = 0; nmbrLet(&nmbrTmp, parseMathTokens(g_fullArg[4], g_proveStatement)); if (g_errorCount) { /* Parsing issued error message(s) */ g_errorCount = 0; continue; } if (cmdMatches("LET VARIABLE")) { if (((vstring)(g_fullArg[2]))[0] != '$') { print2( "?The target variable must be of the form \"$\", e.g. \"$23\".\n"); continue; } n = (long)val(right(g_fullArg[2], 2)); if (n < 1 || n > g_pipDummyVars) { print2("?The target variable must be between $1 and $%ld.\n", g_pipDummyVars); continue; } replaceDummyVar(n, nmbrTmp); autoUnify(1); g_proofChangedFlag = 1; /* Flag to push 'undo' stack */ g_proofChanged = 1; /* Cumulative flag */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } if (cmdMatches("LET STEP")) { /* 14-Sep-2012 nm */ s = getStepNum(g_fullArg[2], g_ProofInProgress.proof, 0 /* ALL not allowed */); if (s == -1) continue; /* Error; message was provided already */ /************** 14-Sep-2012 replaced by getStepNum() s = (long)val(g_fullArg[2]); /@ Step number @/ /@ 16-Apr-06 nm Added LET STEP n where n <= 0: 0 = last, -1 = penultimate, etc. _unknown_ step @/ /@ Unlike ASSIGN LAST/FIRST and IMPROVE LAST/FIRST, it probably doesn't make sense to add LAST/FIRST to LET STEP since known steps can also be LET. The main purpose of LET STEP n, n<=0, is to use with scripting for mmj2 imports. @/ offset = 0; if (s <= 0) { offset = - s + 1; s = 1; /@ Temp. until we figure out which step @/ } /@ End of 16-Apr-06 @/ m = nmbrLen(g_ProofInProgress.proof); /@ Original proof length @/ if (s > m || s < 1) { print2("?The step must be in the range from 1 to %ld.\n", m); continue; } /@ 16-Apr-06 nm Added LET STEP n where n <= 0: 0 = last, 1 = penultimate, etc. _unknown_ step @/ if (offset > 0) { /@ step <= 0 @/ /@ Get the essential step flags @/ s = 0; /@ Use as flag that step was found @/ nmbrLet(&essentialFlags, nmbrGetEssential(g_ProofInProgress.proof)); /@ Scan proof backwards until last essential unknown step found @/ /@ 16-Apr-06 - count back 'offset' unknown steps @/ j = offset; for (i = m; i >= 1; i--) { if (essentialFlags[i - 1] && (g_ProofInProgress.proof)[i - 1] == -(long)'?') { j--; if (j == 0) { /@ Found it @/ s = i; break; } } } /@ Next i @/ if (s == 0) { if (offset == 1) { print2("?There are no unknown essential steps.\n"); } else { print2("?There are not at least %ld unknown essential steps.\n", offset); } continue; } } /@ if offset > 0 @/ /@ End of 16-Apr-06 @/ ******************** end 14-Sep-2012 deletion ********/ /* Check to see if the statement selected is allowed */ if (!checkMStringMatch(nmbrTmp, s - 1)) { printLongLine(cat("?Step ", str((double)s), " cannot be unified with \"", nmbrCvtMToVString(nmbrTmp),"\".", NULL), " ", " "); continue; } /* Assign the user string */ nmbrLet((nmbrString **)(&((g_ProofInProgress.user)[s - 1])), nmbrTmp); autoUnify(1); g_proofChangedFlag = 1; /* Flag to push 'undo' stack */ g_proofChanged = 1; /* Cumulative flag */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } /* 6/14/98 - Automatically display new unknown steps ???Future - add switch to enable/defeat this */ typeProof(g_proveStatement, 1 /*pipFlag*/, 0 /*startStep*/, 0 /*endStep*/, 0 /*endIndent*/, 1 /*essentialFlag*/, 0 /*renumberFlag*/, 1 /*unknownFlag*/, 0 /*notUnifiedFlag*/, 0 /*reverseFlag*/, 0 /*noIndentFlag*/, 0 /*splitColumn*/, 0 /*skipRepeatedSteps*/, /* 28-Jun-2013 nm */ 0 /*texFlag*/, 0 /*g_htmlFlag*/); /* 6/14/98 end */ continue; } if (cmdMatches("ASSIGN")) { /* 10/4/99 - Added LAST - this means the last unknown step shown with SHOW NEW_PROOF/ESSENTIAL/UNKNOWN */ /* 11-Dec-05 nm - Added FIRST - this means the first unknown step shown with SHOW NEW_PROOF/ESSENTIAL/UNKNOWN */ /* 16-Apr-06 nm - Handle nonpositive step number: 0 = last, -1 = penultimate, etc.*/ /* 14-Sep-2012 nm All the above now done by getStepNum() */ s = getStepNum(g_fullArg[1], g_ProofInProgress.proof, 0 /* ALL not allowed */); if (s == -1) continue; /* Error; message was provided already */ /* 3-May-2016 nm */ /* 1 means to override usage locks */ overrideFlag = ( (switchPos("/ OVERRIDE")) ? 1 : 0) || g_globalDiscouragement == 0; /****** replaced by getStepNum() nm 14-Sep-2012 offset = 0; /@ 16-Apr-06 @/ let(&str1, g_fullArg[1]); /@ To avoid void pointer problems with g_fullArg @/ if (toupper((unsigned char)(str1[0])) == 'L' || toupper((unsigned char)(str1[0])) == 'F') { /@ "ASSIGN LAST" or "ASSIGN FIRST" @/ /@ 11-Dec-05 nm @/ s = 1; /@ Temporary until we figure out which step @/ offset = 1; /@ 16-Apr-06 @/ } else { s = (long)val(g_fullArg[1]); /@ Step number @/ if (strcmp(g_fullArg[1], str((double)s))) { print2("?Expected either a number or FIRST or LAST after ASSIGN.\n"); /@ 11-Dec-05 nm @/ continue; } if (s <= 0) { /@ 16-Apr-06 @/ offset = - s + 1; /@ 16-Apr-06 @/ s = 1; /@ Temporary until we figure out which step @/ /@ 16-Apr-06 @/ } /@ 16-Apr-06 @/ } ******************** end 14-Sep-2012 deletion ********/ /* 14-Sep-2012 nm */ /* Get the unique statement matching the g_fullArg[2] pattern */ k = getStatementNum(g_fullArg[2], 1/*startStmt*/, g_proveStatement /*maxStmt*/, 1/*aAllowed*/, 1/*pAllowed*/, 1/*eAllowed*/, 1/*fAllowed*/, 1/*efOnlyForMaxStmt*/, 1/*uniqueFlag*/); if (k == -1) { continue; /* Error msg was provided if not unique */ } /*********** 14-Sep-2012 replaced by getStatementNum() for (i = 1; i <= g_statements; i++) { if (!strcmp(g_fullArg[2], g_Statement[i].labelName)) { /@ If a $e or $f, it must be a hypothesis of the statement being proved @/ if (g_Statement[i].type == (char)e_ || g_Statement[i].type == (char)f_){ if (!nmbrElementIn(1, g_Statement[g_proveStatement].reqHypList, i) && !nmbrElementIn(1, g_Statement[g_proveStatement].optHypList, i)) continue; } break; } } if (i > g_statements) { printLongLine(cat("?The statement with label \"", g_fullArg[2], "\" was not found or is not a hypothesis of the statement ", "being proved. ", "Use SHOW LABELS for a list of valid labels.", NULL), "", " "); continue; } k = i; if (k >= g_proveStatement) { print2( "?You must specify a statement that occurs earlier the one being proved.\n"); continue; } ***************** end of 14-Sep-2012 deletion ************/ /* 3-May-2016 nm */ if (getMarkupFlag(k, USAGE_DISCOURAGED)) { if (overrideFlag == 0) { /* print2("\n"); */ /* Enable for more emphasis */ print2( ">>> ?Error: Attempt to assign a statement whose usage is discouraged.\n"); print2( ">>> Use ASSIGN ... / OVERRIDE if you really want to do this.\n"); /* print2("\n"); */ /* Enable for more emphasis */ continue; } else { /* print2("\n"); */ /* Enable for more emphasis */ print2( ">>> ?Warning: You are assigning a statement whose usage is discouraged.\n"); /* print2("\n"); */ /* Enable for more emphasis */ } } m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ /****** replaced by getStepNum() nm 14-Sep-2012 if (s > m || s < 1) { print2("?The step must be in the range from 1 to %ld.\n", m); continue; } /@ 10/4/99 - For ASSIGN FIRST/LAST command, figure out the last unknown essential step @/ /@ 11-Dec-05 nm - Added LAST @/ /@if (toupper(str1[0]) == 'L' || toupper(str1[0]) == 'F') {@/ /@ "ASSIGN LAST or FIRST" @/ /@ 11-Dec-05 nm @/ if (offset > 0) { /@ LAST, FIRST, or step <= 0 @/ /@ 16-Apr-06 @/ /@ Get the essential step flags @/ s = 0; /@ Use as flag that step was found @/ nmbrLet(&essentialFlags, nmbrGetEssential(g_ProofInProgress.proof)); /@ if (toupper((unsigned char)(str1[0])) == 'L') { @/ if (toupper((unsigned char)(str1[0])) != 'F') { /@ 16-Apr-06 @/ /@ Scan proof backwards until last essential unknown step is found @/ /@ 16-Apr-06 - count back 'offset' unknown steps @/ j = offset; /@ 16-Apr-06 @/ for (i = m; i >= 1; i--) { if (essentialFlags[i - 1] && (g_ProofInProgress.proof)[i - 1] == -(long)'?') { j--; /@ 16-Apr-06 @/ if (j == 0) { /@ 16-Apr-06 @/ /@ Found it @/ s = i; break; } /@ 16-Apr-06 @/ } } /@ Next i @/ } else { /@ 11-Dec-05 nm Added ASSIGN FIRST @/ /@ Scan proof forwards until first essential unknown step is found @/ for (i = 1; i <= m; i++) { if (essentialFlags[i - 1] && (g_ProofInProgress.proof)[i - 1] == -(long)'?') { /@ Found it @/ s = i; break; } } /@ Next i @/ } if (s == 0) { if (offset == 1) { /@ 16-Apr-06 @/ print2("?There are no unknown essential steps.\n"); } else { /@ 16-Apr-06 @/ print2("?There are not at least %ld unknown essential steps.\n", offset); /@ 16-Apr-06 @/ } /@ 16-Apr-06 @/ continue; } } ******************** end 14-Sep-2012 deletion ********/ /* Check to see that the step is an unknown step */ if ((g_ProofInProgress.proof)[s - 1] != -(long)'?') { print2( "?Step %ld is already assigned. You can only assign unknown steps.\n" , s); continue; } /* Check to see if the statement selected is allowed */ if (!checkStmtMatch(k, s - 1)) { print2("?Statement \"%s\" cannot be unified with step %ld.\n", g_Statement[k].labelName, s); continue; } assignStatement(k /*statement#*/, s - 1 /*step*/); n = nmbrLen(g_ProofInProgress.proof); /* New proof length */ autoUnify(1); /* Automatically interact with user if step not unified */ /* ???We might want to add a setting to defeat this if user doesn't like it */ /* 8-Apr-05 nm Since ASSIGN LAST is often run from a commmand file, don't interact if / NO_UNIFY is specified, so response is predictable */ if (switchPos("/ NO_UNIFY") == 0) { interactiveUnifyStep(s - m + n - 1, 2); /* 2nd arg. means print msg if already unified */ } /* if NO_UNIFY flag not set */ /******* 8-Apr-05 nm Commented out: if (m == n) { print2("Step %ld was assigned statement %s.\n", s, g_Statement[k].labelName); } else { if (s != m) { printLongLine(cat("Step ", str((double)s), " was assigned statement ", g_Statement[k].labelName, ". Steps ", str((double)s), ":", str((double)m), " are now ", str((double)(s - m + n)), ":", str((double)n), ".", NULL), "", " "); } else { printLongLine(cat("Step ", str((double)s), " was assigned statement ", g_Statement[k].labelName, ". Step ", str((double)m), " is now step ", str((double)n), ".", NULL), "", " "); } } *********/ /* 8-Apr-05 nm Added: */ /* 1-Nov-2013 nm No longer needed because of UNDO printLongLine(cat("To undo the assignment, DELETE STEP ", str((double)(s - m + n)), " and if needed INITIALIZE, UNIFY.", NULL), "", " "); */ /* 5-Aug-2020 nm */ /* See if it's in another mathbox; if so, let user know */ assignMathboxInfo(); if (k > g_mathboxStmt && g_proveStatement > g_mathboxStmt) { if (k < g_mathboxStart[getMathboxNum(g_proveStatement) - 1]) { printLongLine(cat("\"", g_Statement[k].labelName, "\" is in the mathbox for ", g_mathboxUser[getMathboxNum(k) - 1], ".", NULL), "", " "); } } /* 6/14/98 - Automatically display new unknown steps ???Future - add switch to enable/defeat this */ typeProof(g_proveStatement, 1 /*pipFlag*/, 0 /*startStep*/, 0 /*endStep*/, 0 /*endIndent*/, 1 /*essentialFlag*/, 0 /*renumberFlag*/, 1 /*unknownFlag*/, 0 /*notUnifiedFlag*/, 0 /*reverseFlag*/, 0 /*noIndentFlag*/, 0 /*splitColumn*/, 0 /*skipRepeatedSteps*/, /* 28-Jun-2013 nm */ 0 /*texFlag*/, 0 /*g_htmlFlag*/); /* 6/14/98 end */ g_proofChangedFlag = 1; /* Flag to push 'undo' stack (future) */ g_proofChanged = 1; /* Cumulative flag */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); continue; } /* cmdMatches("ASSIGN") */ if (cmdMatches("REPLACE")) { /* s = (long)val(g_fullArg[1]); obsolete */ /* Step number */ /* 3-May-2016 nm */ /* 1 means to override usage locks */ overrideFlag = ( (switchPos("/ OVERRIDE")) ? 1 : 0) || g_globalDiscouragement == 0; /* 14-Sep-2012 nm */ step = getStepNum(g_fullArg[1], g_ProofInProgress.proof, 0 /* ALL not allowed */); if (step == -1) continue; /* Error; message was provided already */ /* This limitation is due to the assignKnownSteps call below which does not tolerate unknown steps. */ /******* 10/20/02 Limitation removed if (nmbrElementIn(1, g_ProofInProgress.proof, -(long)'?')) { print2("?The proof must be complete before you can use REPLACE.\n"); continue; } *******/ /* 14-Sep-2012 nm */ /* Get the unique statement matching the g_fullArg[2] pattern */ stmt = getStatementNum(g_fullArg[2], 1/*startStmt*/, g_proveStatement /*maxStmt*/, 1/*aAllowed*/, 1/*pAllowed*/, 0/*eAllowed*/, /* Not implemented (yet?) */ 0/*fAllowed*/, /* Not implemented (yet?) */ 1/*efOnlyForMaxStmt*/, 1/*uniqueFlag*/); if (stmt == -1) { continue; /* Error msg was provided if not unique */ } /*********** 14-Sep-2012 replaced by getStatementNum() for (i = 1; i <= g_statements; i++) { if (!strcmp(g_fullArg[2], g_Statement[i].labelName)) { /@ If a $e or $f, it must be a hypothesis of the statement being proved @/ if (g_Statement[i].type == (char)e_ || g_Statement[i].type == (char)f_){ if (!nmbrElementIn(1, g_Statement[g_proveStatement].reqHypList, i) && !nmbrElementIn(1, g_Statement[g_proveStatement].optHypList, i)) continue; } break; } } if (i > g_statements) { printLongLine(cat("?The statement with label \"", g_fullArg[2], "\" was not found or is not a hypothesis of the statement ", "being proved. ", "Use SHOW LABELS for a list of valid labels.", NULL), "", " "); continue; } k = i; if (k >= g_proveStatement) { print2( "?You must specify a statement that occurs earlier the one being proved.\n"); continue; } ****************************** end of 14-Sep-2012 deletion *********/ /* 3-May-2016 nm */ if (getMarkupFlag(stmt, USAGE_DISCOURAGED)) { if (overrideFlag == 0) { /* print2("\n"); */ /* Enable for more emphasis */ print2( ">>> ?Error: Attempt to assign a statement whose usage is discouraged.\n"); print2( ">>> Use REPLACE ... / OVERRIDE if you really want to do this.\n"); /* print2("\n"); */ /* Enable for more emphasis */ continue; } else { /* print2("\n"); */ /* Enable for more emphasis */ print2( ">>> ?Warning: You are assigning a statement whose usage is discouraged.\n"); /* print2("\n"); */ /* Enable for more emphasis */ } } m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ /************** 14-Sep-2012 replaced by getStepNum() if (s > m || s < 1) { print2("?The step must be in the range from 1 to %ld.\n", m); continue; } ************* end of 14-Sep-2012 deletion **************/ /* Check to see that the step is a known step */ /* 22-Aug-2012 nm This check was deleted because it is unnecessary */ /* if ((g_ProofInProgress.proof)[s - 1] == -(long)'?') { print2( "?Step %ld is unknown. You can only replace known steps.\n" , s); continue; } */ /* 10/20/02 Set a flag that proof has unknown steps (for autoUnify() call below) */ if (nmbrElementIn(1, g_ProofInProgress.proof, -(long)'?')) { p = 1; } else { p = 0; } /* Check to see if the statement selected is allowed */ if (!checkStmtMatch(stmt, step - 1)) { print2("?Statement \"%s\" cannot be unified with step %ld.\n", g_Statement[stmt].labelName, step); continue; } /* 16-Sep-2012 nm */ /* Check dummy variable status of step */ /* For use in message later */ dummyVarIsoFlag = checkDummyVarIsolation(step - 1); /* 0=no dummy vars, 1=isolated dummy vars, 2=not isolated*/ /* Do the replacement */ nmbrTmpPtr = replaceStatement(stmt /*statement#*/, step - 1 /*step*/, g_proveStatement, 0,/*scan whole proof to maximize chance of a match*/ 0/*noDistinct*/, 1/* try to prove $e's */, 1/*improveDepth*/, overrideFlag, /* 3-May-2016 nm */ /* Currently REPLACE (not often used) allows other mathboxes silently; TODO: we may want to notify user like for ASSIGN */ 1/*mathboxFlag*/ /* 5-Aug-2020 nm */ ); if (!nmbrLen(nmbrTmpPtr)) { print2( "?Hypotheses of statement \"%s\" do not match known proof steps.\n", g_Statement[stmt].labelName); continue; } /* Get the subproof at step s */ q = subproofLen(g_ProofInProgress.proof, step - 1); deleteSubProof(step - 1); addSubProof(nmbrTmpPtr, step - q); /* 10/20/02 Replaced "assignKnownSteps" with code from entry of PROVE command so REPLACE can be done in partial proofs */ /*assignKnownSteps(s - q, nmbrLen(nmbrTmpPtr));*/ /* old code */ /* Assign known subproofs */ assignKnownSubProofs(); /* Initialize remaining steps */ i = nmbrLen(g_ProofInProgress.proof); for (j = 0; j < i; j++) { if (!nmbrLen((g_ProofInProgress.source)[j])) { initStep(j); } } /* Unify whatever can be unified */ /* If proof wasn't complete before (p = 1), but is now, print congrats for user */ autoUnify((char)p); /* 0 means no "congrats" message */ /* end 10/20/02 */ nmbrLet(&nmbrTmpPtr, NULL_NMBRSTRING); /* Deallocate memory */ n = nmbrLen(g_ProofInProgress.proof); /* New proof length */ if (nmbrElementIn(1, g_ProofInProgress.proof, -(long)'?')) { /* The proof is not complete, so print step numbers that changed */ if (m == n) { print2("Step %ld was replaced with statement %s.\n", step, g_Statement[stmt].labelName); } else { if (step != m) { printLongLine(cat("Step ", str((double)step), " was replaced with statement ", g_Statement[stmt].labelName, ". Steps ", str((double)step), ":", str((double)m), " are now ", str((double)(step - m + n)), ":", str((double)n), ".", NULL), "", " "); } else { printLongLine(cat("Step ", str((double)step), " was replaced with statement ", g_Statement[stmt].labelName, ". Step ", str((double)m), " is now step ", str((double)n), ".", NULL), "", " "); } } } /*autoUnify(1);*/ /************ delete 19-Sep-2012 nm - not needed for REPLACE ******* /@ Automatically interact with user if step not unified @/ /@ ???We might want to add a setting to defeat this if user doesn't like it @/ if (1 /@ ???Future setting flag @/) { interactiveUnifyStep(step - m + n - 1, 2); /@ 2nd arg. means print msg if already unified @/ } *************** end 19-Sep-2012 deletion ********************/ g_proofChangedFlag = 1; /* Flag to push 'undo' stack */ g_proofChanged = 1; /* Cumulative flag */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); /* 16-Sep-2012 nm */ /* if (dummyVarIsoFlag == 2 && g_proofChangedFlag) { printLongLine(cat( "Assignments to shared working variables ($nn) are guesses. If " "incorrect, to undo DELETE STEP ", str((double)(step - m + n)), ", INITIALIZE, UNIFY, then assign them manually with LET ", "and try REPLACE again.", NULL), "", " "); } */ /* 25-Feb-2014 nm */ if (dummyVarIsoFlag == 2 && g_proofChangedFlag) { printLongLine(cat( "Assignments to shared working variables ($nn) are guesses. If " "incorrect, UNDO then assign them manually with LET ", "and try REPLACE again.", NULL), "", " "); } /* 14-Sep-2012 nm - Automatically display new unknown steps ???Future - add switch to enable/defeat this */ if (g_proofChangedFlag) typeProof(g_proveStatement, 1 /*pipFlag*/, 0 /*startStep*/, 0 /*endStep*/, 0 /*endIndent*/, 1 /*essentialFlag*/, 0 /*renumberFlag*/, 1 /*unknownFlag*/, 0 /*notUnifiedFlag*/, 0 /*reverseFlag*/, 0 /*noIndentFlag*/, 0 /*splitColumn*/, 0 /*skipRepeatedSteps*/, /* 28-Jun-2013 nm */ 0 /*texFlag*/, 0 /*g_htmlFlag*/); /* 14-Sep-2012 end */ continue; } /* REPLACE */ if (cmdMatches("IMPROVE")) { improveDepth = 0; /* Depth */ i = switchPos("/ DEPTH"); if (i) improveDepth = (long)val(g_fullArg[i + 1]); if (switchPos("/ NO_DISTINCT")) p = 1; else p = 0; /* p = 1 means don't try to use statements with $d's */ /* 22-Aug-2012 nm Added */ searchAlg = 1; /* Default */ if (switchPos("/ 1")) searchAlg = 1; if (switchPos("/ 2")) searchAlg = 2; if (switchPos("/ 3")) searchAlg = 3; /* 4-Sep-2012 nm Added */ searchUnkSubproofs = 0; if (switchPos("/ SUBPROOFS")) searchUnkSubproofs = 1; mathboxFlag = (switchPos("/ INCLUDE_MATHBOXES") != 0); /* 5-Aug-2020 */ /* 5-Aug-2020 nm */ assignMathboxInfo(); /* In case it hasn't been assigned yet */ if (g_proveStatement > g_mathboxStmt) { /* We're in a mathbox */ i = getMathboxNum(g_proveStatement); if (i <= 0) bug(1130); thisMathboxStartStmt = g_mathboxStart[i - 1]; } else { thisMathboxStartStmt = g_mathboxStmt; } /* 3-May-2016 nm */ /* 1 means to override usage locks */ overrideFlag = ( (switchPos("/ OVERRIDE")) ? 1 : 0) || g_globalDiscouragement == 0; /* 14-Sep-2012 nm */ s = getStepNum(g_fullArg[1], g_ProofInProgress.proof, 1 /* 1 = "ALL" is permissible; returns 0 */); if (s == -1) continue; /* Error; message was provided already */ if (s != 0) { /* s=0 means ALL */ /**************** 14-Sep-2012 nm replaced with getStepNum() /@ 26-Aug-2006 nm Changed 'IMPROVE STEP ' to 'IMPROVE ' @/ let(&str1, g_fullArg[1]); /@ To avoid void pointer problems with g_fullArg @/ if (toupper((unsigned char)(str1[0])) != 'A') { /@ 16-Apr-06 nm - Handle nonpositive step number: 0 = last, -1 = penultimate, etc.@/ offset = 0; /@ 16-Apr-06 @/ /@ 10/4/99 - Added LAST - this means the last unknown step shown with SHOW NEW_PROOF/ESSENTIAL/UNKNOWN @/ if (toupper((unsigned char)(str1[0])) == 'L' || toupper((unsigned char)(str1[0])) == 'F') { /@ 'IMPROVE LAST' or 'IMPROVE FIRST' @/ s = 1; /@ Temporary until we figure out which step @/ offset = 1; /@ 16-Apr-06 @/ } else { if (toupper((unsigned char)(str1[0])) == 'S') { print2( "?\"IMPROVE STEP \" is obsolete. Use \"IMPROVE \".\n"); continue; } s = (long)val(g_fullArg[1]); /@ Step number @/ if (strcmp(g_fullArg[1], str((double)s))) { print2( "?Expected a number or FIRST or LAST or ALL after IMPROVE.\n"); continue; } if (s <= 0) { /@ 16-Apr-06 @/ offset = - s + 1; /@ 16-Apr-06 @/ s = 1; /@ Temporary until we figure out step @/ /@ 16-Apr-06 @/ } /@ 16-Apr-06 @/ } /@ End of 26-Aug-2006 change @/ /@ ------- Old code before 26-Aug-2006 ------- if (cmdMatches("IMPROVE STEP") || cmdMatches("IMPROVE LAST") || cmdMatches("IMPROVE FIRST")) { /# 11-Dec-05 nm #/ /# 16-Apr-06 nm - Handle nonpositive step number: 0 = last, -1 = penultimate, etc.#/ offset = 0; /# 16-Apr-06 #/ /# 10/4/99 - Added LAST - this means the last unknown step shown with SHOW NEW_PROOF/ESSENTIAL/UNKNOWN #/ if (cmdMatches("IMPROVE LAST") || cmdMatches("IMPROVE FIRST")) { /# "IMPROVE LAST or FIRST" #/ /# 11-Dec-05 nm #/ s = 1; /# Temporary until we figure out which step #/ offset = 1; /# 16-Apr-06 #/ } else { s = val(g_fullArg[2]); /# Step number #/ if (s <= 0) { /# 16-Apr-06 #/ offset = - s + 1; /# 16-Apr-06 #/ s = 1; /# Temp. until we figure out which step #/ /# 16-Apr-06 #/ } /# 16-Apr-06 #/ } ------- End of old code ------- @/ **************** end of 14-Sep-2012 nm ************/ m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ /**************** 14-Sep-2012 nm replaced with getStepNum() if (s > m || s < 1) { print2("?The step must be in the range from 1 to %ld.\n", m); continue; } /@ 10/4/99 - For IMPROVE FIRST/LAST command, figure out the last unknown essential step @/ /@ 11-Dec-05 nm - Added FIRST @/ /@if (cmdMatches("IMPROVE LAST") || cmdMatches("IMPROVE FIRST")) {@/ /@ IMPROVE LAST or FIRST @/ /@ 11-Dec-05 nm @/ if (offset > 0) { /@ LAST, FIRST, or step <= 0 @/ /@ 16-Apr-06 @/ /@ Get the essential step flags @/ s = 0; /@ Use as flag that step was found @/ nmbrLet(&essentialFlags, nmbrGetEssential(g_ProofInProgress.proof)); /@if (cmdMatches("IMPROVE LAST")) {@/ /@if (!cmdMatches("IMPROVE FIRST")) {@/ /@ 16-Apr-06 @/ if (toupper((unsigned char)(str1[0])) != 'F') { /@ 26-Aug-2006 @/ /@ Scan proof backwards until last essential unknown step found @/ /@ 16-Apr-06 - count back 'offset' unknown steps @/ j = offset; /@ 16-Apr-06 @/ for (i = m; i >= 1; i--) { if (essentialFlags[i - 1] && (g_ProofInProgress.proof)[i - 1] == -(long)'?') { j--; /@ 16-Apr-06 @/ if (j == 0) { /@ 16-Apr-06 @/ /@ Found it @/ s = i; break; } /@ 16-Apr-06 @/ } } /@ Next i @/ } else { /@ 11-Dec-05 nm Added IMPROVE FIRST @/ /@ Scan proof forwards until first essential unknown step found @/ for (i = 1; i <= m; i++) { if (essentialFlags[i - 1] && (g_ProofInProgress.proof)[i - 1] == -(long)'?') { /@ Found it @/ s = i; break; } } /@ Next i @/ } if (s == 0) { if (offset == 1) { /@ 16-Apr-06 @/ print2("?There are no unknown essential steps.\n"); } else { /@ 16-Apr-06 @/ print2("?There are not at least %ld unknown essential steps.\n", offset); /@ 16-Apr-06 @/ } /@ 16-Apr-06 @/ continue; } } /@ if offset > 0 @/ **************** end of 14-Sep-2012 nm ************/ /* Get the subproof at step s */ q = subproofLen(g_ProofInProgress.proof, s - 1); nmbrLet(&nmbrTmp, nmbrSeg(g_ProofInProgress.proof, s - q + 1, s)); /*???Shouldn't this be just known?*/ /* Check to see that the subproof has an unknown step. */ if (!nmbrElementIn(1, nmbrTmp, -(long)'?')) { print2( "?Step %ld already has a proof and cannot be improved.\n", s); continue; } /* 25-Aug-2012 nm */ /* Check dummy variable status of step */ dummyVarIsoFlag = checkDummyVarIsolation(s - 1); /* 0=no dummy vars, 1=isolated dummy vars, 2=not isolated*/ if (dummyVarIsoFlag == 2) { print2( "?Step %ld target has shared dummy variables and cannot be improved.\n", s); continue; /* Don't try to improve dummy variables that aren't isolated */ } /********* Deleted old code 25-Aug-2012 nm /@ Check to see that the step has no dummy variables. @/ j = 0; /@ Break flag @/ for (i = 0; i < nmbrLen((g_ProofInProgress.target)[s - 1]); i++) { if (((nmbrString @)((g_ProofInProgress.target)[s - 1]))[i] > mathTokens) { j = 1; break; } } if (j) { print2( "?Step %ld target has dummy variables and cannot be improved.\n", s); continue; } ********/ if (dummyVarIsoFlag == 0) { /* No dummy vars */ /* 25-Aug-2012 nm */ /* Only use proveFloating if no dummy vars */ nmbrTmpPtr = proveFloating((g_ProofInProgress.target)[s - 1], g_proveStatement, improveDepth, s - 1, (char)p/*NO_DISTINCT*/, overrideFlag, /* 3-May-2016 nm */ mathboxFlag /* 5-Aug-2020 nm */ ); } else { nmbrTmpPtr = NULL_NMBRSTRING; /* Initialize */ /* 25-Aug-2012 nm */ } if (!nmbrLen(nmbrTmpPtr)) { /* A proof for the step was not found with proveFloating(). */ /* 22-Aug-2012 nm Next, try REPLACE algorithm */ if (searchAlg == 2 || searchAlg == 3) { nmbrTmpPtr = proveByReplacement(g_proveStatement, s - 1/*prfStep*/, /* 0 means step 1 */ (char)p/*NO_DISTINCT*/, /* 1 means don't try stmts with $d's */ dummyVarIsoFlag, (char)(searchAlg - 2), /*0=proveFloat for $fs, 1=$e's also */ improveDepth, /* 4-Sep-2012 */ overrideFlag, /* 3-May-2016 nm */ mathboxFlag /* 5-Aug-2020 nm */ ); } if (!nmbrLen(nmbrTmpPtr)) { print2("A proof for step %ld was not found.\n", s); /* REPLACE algorithm also failed */ continue; } } /* If q=1, subproof must be an unknown step, so don't bother to delete it */ /*???Won't q always be 1 here?*/ if (q > 1) deleteSubProof(s - 1); addSubProof(nmbrTmpPtr, s - q); assignKnownSteps(s - q, nmbrLen(nmbrTmpPtr)); nmbrLet(&nmbrTmpPtr, NULL_NMBRSTRING); n = nmbrLen(g_ProofInProgress.proof); /* New proof length */ if (m == n) { print2("A 1-step proof was found for step %ld.\n", s); } else { if (s != m || q != 1) { printLongLine(cat("A ", str((double)(n - m + 1)), "-step proof was found for step ", str((double)s), ". Steps ", str((double)s), ":", str((double)m), " are now ", str((double)(s - q + 1 - m + n)), ":", str((double)n), ".", NULL), "", " "); } else { printLongLine(cat("A ", str((double)(n - m + 1)), "-step proof was found for step ", str((double)s), ". Step ", str((double)m), " is now step ", str((double)n), ".", NULL), "", " "); } } autoUnify(1); /* To get 'congrats' message if proof complete */ g_proofChanged = 1; /* Cumulative flag */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); /* End if s != 0 i.e. not IMPROVE ALL */ /* 14-Sep-2012 nm */ } else { /* Here, getStepNum() returned 0, meaning ALL */ /* 14-Sep-2012 nm */ /*if (cmdMatches("IMPROVE ALL")) {*/ /* obsolete */ if (!nmbrElementIn(1, g_ProofInProgress.proof, -(long)'?')) { print2("The proof is already complete.\n"); continue; } n = 0; /* Earliest step that changed */ g_proofChangedFlag = 0; for (improveAllIter = 1; improveAllIter <= 4; improveAllIter++) { /* 25-Aug-2012 nm */ if (improveAllIter == 1 && (searchAlg == 2 || searchAlg == 3)) print2("Pass 1: Trying to match cut-free statements...\n"); if (improveAllIter == 2) { if (searchAlg == 2) { print2("Pass 2: Trying to match all statements...\n"); } else { print2( "Pass 2: Trying to match all statements, with cut-free hypothesis matches...\n" ); } } if (improveAllIter == 3 && searchUnkSubproofs) print2("Pass 3: Trying to replace incomplete subproofs...\n"); if (improveAllIter == 4) { if (searchUnkSubproofs) { print2("Pass 4: Repeating pass 1...\n"); } else { print2("Pass 3: Repeating pass 1...\n"); } } /* improveAllIter = 1: run proveFloating only */ /* improveAllIter = 2: run proveByReplacement on unknown steps */ /* improveAllIter = 3: run proveByReplacement on steps with incomplete subproofs */ /* improveAllIter = 4: if something changed, run everything again */ if (improveAllIter == 3 && !searchUnkSubproofs) continue; m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ for (s = m; s > 0; s--) { proofStepUnk = ((g_ProofInProgress.proof)[s - 1] == -(long)'?') ? 1 : 0; /* 25-Aug-2012 nm Added for clearer code */ /* 22-Aug-2012 nm I think this is really too conservative, even with the old algorithm, but keep it to imitate the old one */ if (improveAllIter == 1 || searchAlg == 1) { /* 22-Aug-2012 nm */ /* If the step is known and unified, don't do it, since nothing would be accomplished. */ if (!proofStepUnk) { if (nmbrEq((g_ProofInProgress.target)[s - 1], (g_ProofInProgress.source)[s - 1])) continue; } } /* Get the subproof at step s */ q = subproofLen(g_ProofInProgress.proof, s - 1); if (proofStepUnk && q != 1) { bug(1120); /* 25-Aug-2012 nm Consistency check */ } nmbrLet(&nmbrTmp, nmbrSeg(g_ProofInProgress.proof, s - q + 1, s)); /* Improve only subproofs with unknown steps */ if (!nmbrElementIn(1, nmbrTmp, -(long)'?')) continue; nmbrLet(&nmbrTmp, NULL_NMBRSTRING); /* No longer needed - dealloc */ /* 25-Aug-2012 nm */ /* Check dummy variable status of step */ dummyVarIsoFlag = checkDummyVarIsolation(s - 1); /* 0=no dummy vars, 1=isolated dummy vars, 2=not isolated*/ if (dummyVarIsoFlag == 2) continue; /* Don't try to improve dummy variables that aren't isolated */ /********* Deleted old code now done by checkDummyVarIsolation() 25-Aug-2012 nm /@ Check to see that the step has no dummy variables. @/ j = 0; /@ Break flag @/ for (i = 0; i < nmbrLen((g_ProofInProgress.target)[s - 1]); i++) { if (((nmbrString @)((g_ProofInProgress.target)[s - 1]))[i] > mathTokens) { j = 1; break; } } if (j) { /@ Step has dummy variables and cannot be improved. @/ continue; } ********/ if (dummyVarIsoFlag == 0 && (improveAllIter == 1 || improveAllIter == 4)) { /* No dummy vars */ /* 25-Aug-2012 nm */ /* Only use proveFloating if no dummy vars */ nmbrTmpPtr = proveFloating((g_ProofInProgress.target)[s - 1], g_proveStatement, improveDepth, s - 1, (char)p/*NO_DISTINCT*/, overrideFlag, /* 3-May-2016 nm */ mathboxFlag /* 5-Aug-2020 nm */ ); } else { nmbrTmpPtr = NULL_NMBRSTRING; /* Init */ /* 25-Aug-2012 nm */ } if (!nmbrLen(nmbrTmpPtr)) { /* A proof for the step was not found with proveFloating(). */ /* 22-Aug-2012 nm Next, try REPLACE algorithm */ if ((searchAlg == 2 || searchAlg == 3) && ((improveAllIter == 2 && proofStepUnk) || (improveAllIter == 3 && !proofStepUnk) /*|| improveAllIter == 4*/)) { nmbrTmpPtr = proveByReplacement(g_proveStatement, s - 1/*prfStep*/, /* 0 means step 1 */ (char)p/*NO_DISTINCT*/, /* 1 means don't try stmts w/ $d's */ dummyVarIsoFlag, (char)(searchAlg - 2),/*searchMethod: 0 or 1*/ improveDepth, /* 4-Sep-2012 */ overrideFlag, /* 3-May-2016 nm */ mathboxFlag /* 5-Aug-2020 nm */ ); } if (!nmbrLen(nmbrTmpPtr)) { /* REPLACE algorithm also failed */ continue; } } /* If q=1, subproof must be an unknown step, so don't bother to delete it */ if (q > 1) deleteSubProof(s - 1); addSubProof(nmbrTmpPtr, s - q); assignKnownSteps(s - q, nmbrLen(nmbrTmpPtr)); print2("A proof of length %ld was found for step %ld.\n", nmbrLen(nmbrTmpPtr), s); if (nmbrLen(nmbrTmpPtr) || q != 1) n = s - q + 1; /* Save earliest step changed */ nmbrLet(&nmbrTmpPtr, NULL_NMBRSTRING); g_proofChangedFlag = 1; s = s - q + 1; /* Adjust step position to account for deleted subpr */ } /* Next step s */ if (g_proofChangedFlag) { autoUnify(0); /* 0 = No 'Congrats' if done */ } if (!g_proofChangedFlag && ( (improveAllIter == 2 && !searchUnkSubproofs) || improveAllIter == 3 || searchAlg == 1)) { print2("No new subproofs were found.\n"); break; /* out of improveAllIter loop */ } if (g_proofChangedFlag) { g_proofChanged = 1; /* Cumulative flag */ } if (!nmbrElementIn(1, g_ProofInProgress.proof, -(long)'?')) { break; /* Proof is complete */ } if (searchAlg == 1) break; /* Old algorithm does just 1st pass */ } /* Next improveAllIter */ if (g_proofChangedFlag) { if (n > 0) { /* n is the first step number changed. It will be 0 if the numbering didn't change e.g. a $e was assigned to an unknown step. */ print2("Steps %ld and above have been renumbered.\n", n); } processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } if (!nmbrElementIn(1, g_ProofInProgress.proof, -(long)'?')) { /* This is a redundant call; its purpose is just to give the message if the proof is complete */ autoUnify(1); /* 1 = 'Congrats' if done */ } } /* End if IMPROVE ALL */ /* 6/14/98 - Automatically display new unknown steps ???Future - add switch to enable/defeat this */ if (g_proofChangedFlag) typeProof(g_proveStatement, 1 /*pipFlag*/, 0 /*startStep*/, 0 /*endStep*/, 0 /*endIndent*/, 1 /*essentialFlag*/, 0 /*renumberFlag*/, 1 /*unknownFlag*/, 0 /*notUnifiedFlag*/, 0 /*reverseFlag*/, 0 /*noIndentFlag*/, 0 /*splitColumn*/, 0 /*skipRepeatedSteps*/, /* 28-Jun-2013 nm */ 0 /*texFlag*/, 0 /*g_htmlFlag*/); /* 6/14/98 end */ continue; } /* cmdMatches("IMPROVE") */ if (cmdMatches("MINIMIZE_WITH")) { /* 16-Aug-2016 nm */ printTime = 0; if (switchPos("/ TIME") != 0) { printTime = 1; } if (printTime == 1) { getRunTime(&timeIncr); /* This call just resets the time */ } /* q = 0; */ /* Line length */ /* 25-Jun-2014 deleted */ prntStatus = 0; /* Status flag to help determine messages 0 = no statement was matched during scan (mainly for error message if user typo in label field) 1 = a statement was matched but no shorter proof 2 = shorter proof found */ /* verboseMode = (switchPos("/ BRIEF") == 0); */ /* Non-verbose mode */ /* 4-Feb-2013 nm VERBOSE is now default */ verboseMode = (switchPos("/ VERBOSE") != 0); /* Verbose mode */ /* 30-Jan-06 nm Added single-character-match wildcard argument */ if (!(instr(1, g_fullArg[1], "*") || instr(1, g_fullArg[1], "?"))) i = 1; /* 16-Feb-05 If no wildcard was used, switch to non-verbose mode since there is no point to it and an annoying extra blank line results */ mayGrowFlag = (switchPos("/ MAY_GROW") != 0); /* Mode to replace even if it doesn't reduce proof length */ /* 25-Jun-2014 nm /NO_DISTINCT is obsolete noDistinctFlag = (switchPos("/ NO_DISTINCT") != 0); */ /* Skip trying statements with $d */ exceptPos = switchPos("/ EXCEPT"); /* Statement match to skip */ /* 7-Jan-06 */ /* 4-Aug-2019 nm */ allowNewAxiomsMatchPos = switchPos("/ ALLOW_NEW_AXIOMS"); if (allowNewAxiomsMatchPos != 0) { let(&allowNewAxiomsMatchList, g_fullArg[allowNewAxiomsMatchPos + 1]); } else { let(&allowNewAxiomsMatchList, ""); } /* 20-May-2013 nm */ noNewAxiomsMatchPos = switchPos("/ NO_NEW_AXIOMS_FROM"); if (noNewAxiomsMatchPos != 0) { let(&noNewAxiomsMatchList, g_fullArg[noNewAxiomsMatchPos + 1]); } else { let(&noNewAxiomsMatchList, ""); } /* 20-May-2013 nm */ forbidMatchPos = switchPos("/ FORBID"); if (forbidMatchPos != 0) { let(&forbidMatchList, g_fullArg[forbidMatchPos + 1]); } else { let(&forbidMatchList, ""); } mathboxFlag = (switchPos("/ INCLUDE_MATHBOXES") != 0); /* 28-Jun-2011 */ /* 25-Jun-2014 nm /REVERSE is obsolete forwFlag = (switchPos("/ REVERSE") != 0); /@ 10-Nov-2011 nm @/ */ /****** 5-Aug-2020 nm Replaced w/ assignMathboxInfo() below if (g_mathboxStmt == 0) { /@ Look up "mathbox" label if it hasn't been @/ g_mathboxStmt = lookupLabel("mathbox"); if (g_mathboxStmt == -1) g_mathboxStmt = g_statements + 1; /@ Default beyond db end if none @/ } *******/ /* 3-May-2016 nm */ /* Flag to override any "usage locks" placed in the comment markup */ overrideFlag = (switchPos("/ OVERRIDE") != 0) || g_globalDiscouragement == 0; /* 25-Jun-2014 nm */ /* If a single statement is specified, don't bother to do certain actions or print some of the messages */ /* 18-Jul-2020 nm New code*/ hasWildCard = 0; /* (Note strpbrk warning in mmpars.c) */ /*if (strpbrk(g_fullArg[1], "*?=~%#@,") != NULL) {*/ /* Set hasWildCard only when there are potentially > 1 matches */ if (strpbrk(g_fullArg[1], "*?~%,") != NULL) { /* (See matches() function for processing of these) "*" 0 or more char match "?" 1 char match "=" Most recent PROVE command statement = one statement match "~" Statement range "%" List of modified statements "#" Internal statement number = one statement match "@" Web page statement number = one statement match "," Comma-separated fields */ hasWildCard = 1; } /****** 18-Jul-2020 nm Deleted old code: hasWildCard = (instr(1, g_fullArg[1], "*") || instr(1, g_fullArg[1], "?") || instr(1, g_fullArg[1], ",") || instr(1, g_fullArg[1], "~") /@ 3-May-2014 nm label~label range @/ ); ********/ g_proofChangedFlag = 0; /* Added 14-Aug-2012 nm */ /* Always scan statements in current mathbox, even if "/ INCLUDE_MATHBOXES" is omitted */ /* 5-Aug-2020 nm */ assignMathboxInfo(); /* In case it hasn't been assigned yet */ if (g_proveStatement > g_mathboxStmt) { /* We're in a mathbox */ i = getMathboxNum(g_proveStatement); if (i <= 0) bug(1130); thisMathboxStartStmt = g_mathboxStart[i - 1]; } else { thisMathboxStartStmt = g_mathboxStmt; } /****** 5-Aug-2020 deleted old code thisMathboxStartStmt = g_mathboxStmt; /@ Will become start of current (g_proveStatement's) mathbox @/ if (g_proveStatement > g_mathboxStmt) { /@ We're in a mathbox @/ for (k = g_proveStatement; k >= g_mathboxStmt; k--) { let(&str1, left(g_Statement[k].labelSectionPtr, g_Statement[k].labelSectionLen)); /@ Heuristic to match beginning of mathbox @/ if (instr(1, str1, "Mathbox for") != 0) { /@ Found beginning of current mathbox @/ thisMathboxStartStmt = k; break; } } } **************/ /* 25-Jun-2014 nm */ copyProofStruct(&saveOrigProof, g_ProofInProgress); /* 12-Sep-2016 nm TODO replace this w/ compressedProofSize */ /* 25-Jun-2014 nm Get the current (original) compressed proof length to compare it when a shorter non-compressed proof is found, to see if the compressed proof also decreased in size */ nmbrLet(&nmbrSaveProof, g_ProofInProgress.proof); /* Redundant? */ nmbrLet(&nmbrSaveProof, nmbrSquishProof(g_ProofInProgress.proof)); /* We only care about length; str1 will be discarded */ let(&str1, compressProof(nmbrSaveProof, g_proveStatement, /* statement being proved */ 0 /* Normal (not "fast") compression */ )); origCompressedLength = (long)strlen(str1); print2( "Bytes refer to compressed proof size, steps to uncompressed length.\n"); /* 25-Jun-2014 nm forwRevPass outer loop added */ /* Scan forward, then reverse, then pick best result */ for (forwRevPass = 1; forwRevPass <= 2; forwRevPass++) { /* 25-Jun-2014 nm */ if (forwRevPass == 1) { if (hasWildCard) print2("Scanning forward through statements...\n"); forwFlag = 1; } else { /* If growth allowed, don't bother with reverse pass */ if (mayGrowFlag) break; /* If nothing was found on forward pass, don't bother with rev pass */ if (!g_proofChangedFlag) break; /* If only one statement was specified, don't bother with rev pass */ if (!hasWildCard) break; print2("Scanning backward through statements...\n"); forwFlag = 0; /* Save proof and length from 1st pass; re-initialize */ copyProofStruct(&save1stPassProof, g_ProofInProgress); forwardLength = nmbrLen(g_ProofInProgress.proof); forwardCompressedLength = oldCompressedLength; /* Start over from original proof */ copyProofStruct(&g_ProofInProgress, saveOrigProof); } /* 20-May-2013 nm */ /* if (forbidMatchList[0]) { /@ User provided a /FORBID list @/ /@ Save the proof structure in case we have to revert a forbidden match. @/ copyProofStruct(&saveProofForReverting, g_ProofInProgress); } */ /* 25-Jun-2014 nm */ copyProofStruct(&saveProofForReverting, g_ProofInProgress); oldCompressedLength = origCompressedLength; /* for (k = 1; k < g_proveStatement; k++) { */ /* 10-Nov-2011 nm */ /* If forwFlag is 0, scan from g_proveStatement-1 to 1 If forwFlag is 1, scan from 1 to g_proveStatement-1 */ for (k = forwFlag ? 1 : (g_proveStatement - 1); k * (forwFlag ? 1 : -1) < (forwFlag ? g_proveStatement : 0); k = k + (forwFlag ? 1 : -1)) { /* 28-Jun-2011 */ /* Scan mathbox statements only if INCLUDE_MATHBOXES specified */ /*if (!mathboxFlag && k >= g_mathboxStmt) continue;*/ /* 14-Aug-2012 nm */ if (!mathboxFlag && k >= g_mathboxStmt && k < thisMathboxStartStmt) { continue; } if (g_Statement[k].type != (char)p_ && g_Statement[k].type != (char)a_) continue; /* 30-Jan-06 nm Added single-character-match wildcard argument */ if (!matchesList(g_Statement[k].labelName, g_fullArg[1], '*', '?')) continue; /* 25-Jun-2014 nm /NO_DISTINCT is obsolete if (noDistinctFlag) { /@ Skip the statement if it has a $d requirement. This option prevents illegal minimizations that would violate $d requirements since MINIMIZE_WITH does not check for $d violations. @/ if (nmbrLen(g_Statement[k].reqDisjVarsA)) { /@ 30-Jan-06 nm Added single-character-match wildcard argument @/ if (!(instr(1, g_fullArg[1], "@") || instr(1, g_fullArg[1], "?"))) print2("?\"%s\" has a $d requirement\n", g_fullArg[1]); continue; } } */ /* 7-Jan-06 nm - Added EXCEPT switch */ if (exceptPos != 0) { /* Skip any match to the EXCEPT argument */ /* 30-Jan-06 nm Added single-character-match wildcard argument */ if (matchesList(g_Statement[k].labelName, g_fullArg[exceptPos + 1], '*', '?')) continue; } /* 20-May-2013 nm */ if (forbidMatchList[0]) { /* User provided a /FORBID list */ /* First, we check to make sure we're not trying a statement in the forbidMatchList directly (traceProof() won't find this) */ if (matchesList(g_Statement[k].labelName, forbidMatchList, '*', '?')) continue; } /* 3-May-2016 nm */ /* Check to see if statement comment specified a usage restriction */ if (!overrideFlag) { if (getMarkupFlag(k, USAGE_DISCOURAGED)) { continue; } } /* Print individual labels */ if (prntStatus == 0) prntStatus = 1; /* Matched at least one */ /* 25-Jun-2014 nm Don't list matched statements anymore if (verboseMode) { q = q + (long)strlen(g_Statement[k].labelName) + 1; if (q > 72) { q = (long)strlen(g_Statement[k].labelName) + 1; print2("\n"); } print2("%s ",g_Statement[k].labelName); } */ m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ nmbrLet(&nmbrTmp, g_ProofInProgress.proof); minimizeProof(k /* trial statement */, g_proveStatement /* statement being proved in MM-PA */, (char)mayGrowFlag /* mayGrowFlag */); n = nmbrLen(g_ProofInProgress.proof); /* New proof length */ if (!nmbrEq(nmbrTmp, g_ProofInProgress.proof)) { /* The proof got shorter (or it changed if MAY_GROW) */ /* 20-May-2013 nm Because of the slow speed of traceBack(), we only want to check the /FORBID list in the relatively rare case where a minimization occurred. If the FORBID list is matched, we then need to revert back to the original proof. */ if (forbidMatchList[0]) { /* User provided a /FORBID list */ if (g_Statement[k].type == (char)p_) { /* We only care about tracing $p statements */ /* See if the TRACE_BACK list includes a match to the /FORBID argument */ if (traceProof(k, 0, /*essentialFlag*/ 0, /*axiomFlag*/ forbidMatchList, "", /*traceToList*/ /* 18-Jul-2015 nm */ 1 /* testOnlyFlag */)) { /* Yes, a forbidden statement occurred in traceProof() */ /* Revert the proof to before minimization */ copyProofStruct(&g_ProofInProgress, saveProofForReverting); /* Skip further printout and flag setting */ continue; /* Continue at 'Next k' loop end below */ } } } /* 22-Nov-2014 nm Because of the slow speed of traceBack(), we only want to check the /NO_NEW_AXIOMS_FROM list in the relatively rare case where a minimization occurred. If the NO_NEW_AXIOMS_FROM condition applies, we then need to revert back to the original proof. */ /* 4-Aug-2019 nm */ if (n == n + 0) { /* By default, no new axioms are permitted */ /*if (noNewAxiomsMatchList[0]) {*/ /* User provided /NO_NEW_AXIOMS_FROM */ /* If we haven't called trace yet for the theorem being proved, do it now. */ if (traceProofFlags[0] == 0) { /******** start of 29-Nov-2019 nm ************/ /* traceProofWork() was written to use the SAVEd proof and not the proof in progress. In order to use the proof in progress, we temporarily put the proof in progress into the (SAVEd) statement structure to trick traceProofWork() into using the proof in progress instead of the SAVEd proof */ /* Bad code line between 4-Aug-2019 and 12-Feb-2020: */ /*nmbrLet(&nmbrSaveProof, nmbrSquishProof(g_ProofInProgress.proof));*/ /* Bad! */ /* 12-Feb-2020 nm */ /* Use the version of the proof in progress that existed *before* the MINIMIZE_WITH command was invoked */ nmbrLet(&nmbrSaveProof, nmbrSquishProof(saveProofForReverting.proof)); let(&str1, compressProof(nmbrSaveProof, g_proveStatement, /* statement being proved in MM-PA */ 0 /* Normal (not "fast") compression */ )); saveZappedProofSectionPtr = g_Statement[g_proveStatement].proofSectionPtr; saveZappedProofSectionLen = g_Statement[g_proveStatement].proofSectionLen; saveZappedProofSectionChanged = g_Statement[g_proveStatement].proofSectionChanged; /* Set flag that this is not the original source */ g_Statement[g_proveStatement].proofSectionChanged = 1; /* str1 has the new compressed trial proof after minimization */ /* Put space before and after to satisfy "space around token" requirement, to prevent possible error messages, and also add "$." since parseCompressedProof() expects it */ let(&str1, cat(" ", str1, " $.", NULL)); /* Don't include the "$." in the length */ g_Statement[g_proveStatement].proofSectionLen = (long)strlen(str1) - 2; /* We don't deallocate previous proofSectionPtr content because we will recover it after the verifyProof() */ g_Statement[g_proveStatement].proofSectionPtr = str1; /******** end of 29-Nov-2019 nm ************/ traceProofWork(g_proveStatement, 1 /*essentialFlag*/, "", /*traceToList*/ /* 18-Jul-2015 nm */ &traceProofFlags, /* y/n list of flags */ &nmbrTmp /* unproved list - ignored */); nmbrLet(&nmbrTmp, NULL_NMBRSTRING); /* Discard */ /******** start of 29-Nov-2019 nm ************/ /* Restore the SAVEd proof */ g_Statement[g_proveStatement].proofSectionPtr = saveZappedProofSectionPtr; g_Statement[g_proveStatement].proofSectionLen = saveZappedProofSectionLen; g_Statement[g_proveStatement].proofSectionChanged = saveZappedProofSectionChanged; /* 16-Jun-2017 nm */ /******** end of 29-Nov-2019 nm ************/ } let(&traceTrialFlags, ""); traceProofWork(k, /* The trial statement */ 1 /*essentialFlag*/, "", /*traceToList*/ /* 18-Jul-2015 nm */ &traceTrialFlags, /* Y/N list of flags */ &nmbrTmp /* unproved list - ignored */); nmbrLet(&nmbrTmp, NULL_NMBRSTRING); /* Discard */ j = 1; /* 1 = ok to use trial statement */ for (i = 1; i < g_proveStatement; i++) { if (g_Statement[i].type != (char)a_) continue; /* Not $a */ if (traceProofFlags[i] == 'Y') continue; /* If the axiom is already used by the proof, we don't care if the trial statement depends on it */ if (matchesList(g_Statement[i].labelName, allowNewAxiomsMatchList, '*', '?') == 1 && matchesList(g_Statement[i].labelName, noNewAxiomsMatchList, '*', '?') != 1) { /* 4-Aug-2019 nm */ /* If the axiom is in the list to allow and not in the list to disallow, we don't care if the trial statement depends on it */ continue; } /* if (matchesList(g_Statement[i].labelName, noNewAxiomsMatchList, '@', '?') != 1) { /@ If the axiom isn't in the list to avoid, we don't care if the trial statement depends on it @/ continue; } */ if (traceTrialFlags[i] == 'Y') { /* The trial statement uses an axiom that the current proof should avoid, so we abort it */ j = 0; /* 0 = don't use trial statement */ break; } } /* next i */ if (j == 0) { /* A forbidden axiom is used by the trial proof */ /* Revert the proof to before minimization */ copyProofStruct(&g_ProofInProgress, saveProofForReverting); /* Skip further printout and flag setting */ continue; /* Continue at 'Next k' loop end below */ } } /* end if (true) */ /* 25-Jun-2014 nm Make sure the compressed proof length decreased, otherwise revert. Also, we will use the compressed proof for the $d check next */ if (nmbrLen(g_Statement[k].reqDisjVarsA) || !mayGrowFlag) { nmbrLet(&nmbrSaveProof, g_ProofInProgress.proof); nmbrLet(&nmbrSaveProof, nmbrSquishProof(g_ProofInProgress.proof)); let(&str1, compressProof(nmbrSaveProof, g_proveStatement, /* statement being proved in MM-PA */ 0 /* Normal (not "fast") compression */ )); newCompressedLength = (long)strlen(str1); if (!mayGrowFlag && newCompressedLength > oldCompressedLength) { /* The compressed proof length increased, so don't use it. (If it stayed the same, we will use it because the uncompressed length did decrease.) */ /* Revert the proof to before minimization */ if (verboseMode) { print2( "Reverting \"%s\": Uncompressed steps: old = %ld, new = %ld\n", g_Statement[k].labelName, m, n ); print2( " but compressed size: old = %ld bytes, new = %ld bytes\n", oldCompressedLength, newCompressedLength); } copyProofStruct(&g_ProofInProgress, saveProofForReverting); /* Skip further printout and flag setting */ continue; /* Continue at 'Next k' loop end below */ } } /* if (nmbrLen(g_Statement[k].reqDisjVarsA) || !mayGrowFlag) */ /* 25-Jun-2014 nm */ /* Make sure there are no $d violations, otherwise revert */ /* This requires the str1 from above */ if (nmbrLen(g_Statement[k].reqDisjVarsA)) { /* There is currently no way to verify a proof that doesn't read and parse the source directly. This should be changed in the future to make the program more modular. But for now, we temporarily zap the source with new compressed proof and see if there are any $d violations by looking at the error message output */ saveZappedProofSectionPtr = g_Statement[g_proveStatement].proofSectionPtr; saveZappedProofSectionLen = g_Statement[g_proveStatement].proofSectionLen; /****** Obsolete due to 3-May-2017 update /@ (search for "chr(1)" above for explanation) @/ let(&str1, cat(chr(1), "\n", str1, " $.\n", NULL)); g_Statement[g_proveStatement].proofSectionPtr = str1 + 1; /@ Compressed proof generated above @/ g_Statement[g_proveStatement].proofSectionLen = newCompressedLength + 4; *******/ /******** start of 16-Jun-2017 nm ************/ saveZappedProofSectionChanged = g_Statement[g_proveStatement].proofSectionChanged; /* Set flag that this is not the original source */ g_Statement[g_proveStatement].proofSectionChanged = 1; /* str1 has the new compressed trial proof after minimization */ /* Put space before and after to satisfy "space around token" requirement, to prevent possible error messages, and also add "$." since parseCompressedProof() expects it */ let(&str1, cat(" ", str1, " $.", NULL)); /* Don't include the "$." in the length */ g_Statement[g_proveStatement].proofSectionLen = (long)strlen(str1) - 2; /* We don't deallocate previous proofSectionPtr content because we will recover it after the verifyProof() */ g_Statement[g_proveStatement].proofSectionPtr = str1; /******** end of 16-Jun-2017 nm ************/ g_outputToString = 1; /* Suppress error messages */ /* i = parseProof(g_proveStatement); */ /* if (i != 0) bug(1121); */ /* i = verifyProof(g_proveStatement); */ /* if (i != 0) bug(1122); */ /* 15-Apr-2015 nm parseProof, verifyProof, cleanWkrProof must be called in sequence to assign the g_WrkProof structure, verify 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() */ /* 15-Apr-2015 nm - don't change proof if there is an error (which could be pre-existing). */ i = (g_WrkProof.errorSeverity > 1); /**** Here we look at the screen output sent to a string. This is rather crude, and someday the ability to check proofs and $d violations should be modularized *****/ j = instr(1, g_printString, "There is a disjoint variable ($d) violation"); g_outputToString = 0; /* Restore to normal output */ let(&g_printString, ""); /* Clear out the stored error messages */ cleanWrkProof(); /* Deallocate verifyProof storage */ g_Statement[g_proveStatement].proofSectionPtr = saveZappedProofSectionPtr; g_Statement[g_proveStatement].proofSectionLen = saveZappedProofSectionLen; g_Statement[g_proveStatement].proofSectionChanged = saveZappedProofSectionChanged; /* 16-Jun-2017 nm */ if (i != 0 || j != 0) { /* There was a verify proof error (j!=0) or $d violation (i!=0) so don't used minimized proof */ /* Revert the proof to before minimization */ copyProofStruct(&g_ProofInProgress, saveProofForReverting); /* Skip further printout and flag setting */ continue; /* Continue at 'Next k' loop end below */ } } /* if (nmbrLen(g_Statement[k].reqDisjVarsA)) */ /* 25-Jun-2014 nm - not needed since trials now suppressed */ /* if (verboseMode) { print2("\n"); } */ /*if (nmbrLen(g_Statement[k].reqDisjVarsA) || !mayGrowFlag) {*/ /* 3-May-2016 nm */ /* Warn user if a discouraged statement is overridden */ if (getMarkupFlag(k, USAGE_DISCOURAGED)) { if (!overrideFlag) bug(1126); /* print2("\n"); */ /* Enable for more emphasis */ print2( ">>> ?Warning: Overriding discouraged usage of \"%s\".\n", g_Statement[k].labelName); /* print2("\n"); */ /* Enable for more emphasis */ } if (!mayGrowFlag) { /* Note: this is the length BEFORE indentation and wrapping, so it is less than SHOW PROOF ... /SIZE */ if (newCompressedLength < oldCompressedLength) { print2( "Proof of \"%s\" decreased from %ld to %ld bytes using \"%s\".\n", g_Statement[g_proveStatement].labelName, oldCompressedLength, newCompressedLength, g_Statement[k].labelName); } else { if (newCompressedLength > oldCompressedLength) bug(1123); print2( "Proof of \"%s\" stayed at %ld bytes using \"%s\".\n", g_Statement[g_proveStatement].labelName, oldCompressedLength, g_Statement[k].labelName); print2( " (Uncompressed steps decreased from %ld to %ld).\n", m, n ); } /* (We don't care about compressed length if MAY_GROW) */ oldCompressedLength = newCompressedLength; } if (n < m && (mayGrowFlag || verboseMode)) { print2( "%sProof of \"%s\" decreased from %ld to %ld steps using \"%s\".\n", (mayGrowFlag ? "" : " "), g_Statement[g_proveStatement].labelName, m, n, g_Statement[k].labelName); } /* MAY_GROW possibility */ if (m < n) print2( "Proof of \"%s\" increased from %ld to %ld steps using \"%s\".\n", g_Statement[g_proveStatement].labelName, m, n, g_Statement[k].labelName); /* MAY_GROW possibility */ if (m == n) print2( "Proof of \"%s\" remained at %ld steps using \"%s\".\n", g_Statement[g_proveStatement].labelName, m, g_Statement[k].labelName); /* Distinct variable warning (obsolete) */ /* if (nmbrLen(g_Statement[k].reqDisjVarsA)) { printLongLine(cat("Note: \"", g_Statement[k].labelName, "\" has $d constraints.", " SAVE NEW_PROOF then VERIFY PROOF to check them.", NULL), "", " "); } */ /* q = 0; */ /* Line length for label list */ /* 25-Jun-2014 del */ /* 8-Aug-2020 nm */ /* See if it's in another mathbox; if so, let user know */ assignMathboxInfo(); if (k > g_mathboxStmt && g_proveStatement > g_mathboxStmt) { if (k < g_mathboxStart[getMathboxNum(g_proveStatement) - 1]) { printLongLine(cat("\"", g_Statement[k].labelName, "\" is in the mathbox for ", g_mathboxUser[getMathboxNum(k) - 1], ".", NULL), " ", " "); } } prntStatus = 2; /* Found one */ g_proofChangedFlag = 1; /* deleted 25-Jun-2014: /@ 20-May-2012 nm @/ if (forbidMatchList[0]) { /@ User provided a /FORBID list @/ /@ Save the changed proof in case we have to restore it later @/ copyProofStruct(&saveProofForReverting, g_ProofInProgress); } */ /* 25-Jun-2014 nm */ /* Save the changed proof in case we have to restore it later */ copyProofStruct(&saveProofForReverting, g_ProofInProgress); } } /* Next k (statement) */ /* 25-Jun-2014 nm - not needed since trials now suppressed */ /* if (verboseMode) { if (prntStatus) print2("\n"); } */ if (g_proofChangedFlag && forwRevPass == 2) { /* 25-Jun-2014 nm */ /* Check whether the reverse pass found a better proof than the forward pass */ if (verboseMode) { print2( "Forward vs. backward: %ld vs. %ld bytes; %ld vs. %ld steps\n", forwardCompressedLength, oldCompressedLength, forwardLength, nmbrLen(g_ProofInProgress.proof)); } if (oldCompressedLength < forwardCompressedLength || (oldCompressedLength == forwardCompressedLength && nmbrLen(g_ProofInProgress.proof) < forwardLength)) { /* The reverse pass was better */ print2("The backward scan results were used.\n"); } else { copyProofStruct(&g_ProofInProgress, save1stPassProof); print2("The forward scan results were used.\n"); } } } /* next forwRevPass */ if (prntStatus == 1 && !mayGrowFlag) print2("No shorter proof was found.\n"); if (prntStatus == 1 && mayGrowFlag) print2("The proof was not changed.\n"); if (!prntStatus /* && !noDistinctFlag */) print2("?No earlier %s$p or $a label matches \"%s\".\n", (overrideFlag ? "" : "(allowed) "), /* 3-May-2016 nm */ g_fullArg[1]); /* 25-Jun-2014 nm /NO_DISTINCT is obsolete if (!prntStatus && noDistinctFlag) { /@ 30-Jan-06 nm Added single-character-match wildcard argument @/ if (instr(1, g_fullArg[1], "@") || instr(1, g_fullArg[1], "?")) print2("?No earlier $p or $a label (without $d) matches \"%s\".\n", g_fullArg[1]); } */ /* 28-Jun-2011 nm */ if (!mathboxFlag && g_proveStatement >= g_mathboxStmt) { print2( "(Other mathboxes were not checked. Use / INCLUDE_MATHBOXES to include them.)\n"); } /* 16-Aug-2016 nm */ if (printTime == 1) { getRunTime(&timeIncr); print2("MINIMIZE_WITH run time = %7.2f sec for \"%s\"\n", timeIncr, g_Statement[g_proveStatement].labelName); } /* 23-Nov-2019 nm */ let(&str1, ""); /* Deallocate memory */ nmbrLet(&nmbrSaveProof, NULL_NMBRSTRING); /* Deallocate memory */ /* 23-Nov-2019 nm */ /* Clear these Y/N trace strings unconditionally since new axioms are no longer allowed by default, so they may become set regardless of qualifiers */ let(&traceProofFlags, ""); /* Deallocate memory */ let(&traceTrialFlags, ""); /* Deallocate memory */ /* 4-Aug-2019 nm */ if (allowNewAxiomsMatchList[0]) { /* User provided /NO_NEW_AXIOMS_FROM list */ let(&allowNewAxiomsMatchList, ""); /* Deallocate memory */ } /* 22-Nov-2014 nm */ if (noNewAxiomsMatchList[0]) { /* User provided /ALLOW_NEW_AXIOMS list */ let(&noNewAxiomsMatchList, ""); /* Deallocate memory */ } /* 20-May-2013 nm */ if (forbidMatchList[0]) { /* User provided a /FORBID list */ /*deallocProofStruct(&saveProofForReverting);*/ /* Deallocate memory */ let(&forbidMatchList, ""); /* Deallocate memory */ } /* 25-Jun-2014 nm */ deallocProofStruct(&saveProofForReverting); /* Deallocate memory */ deallocProofStruct(&saveOrigProof); /* Deallocate memory */ deallocProofStruct(&save1stPassProof); /* Deallocate memory */ if (g_proofChangedFlag) { g_proofChanged = 1; /* Cumulative flag */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } continue; } /* End if MINIMIZE_WITH */ /* 11-Sep-2016 nm Added EXPAND command */ if (cmdMatches("EXPAND")) { g_proofChangedFlag = 0; nmbrLet(&nmbrSaveProof, g_ProofInProgress.proof); s = compressedProofSize(nmbrSaveProof, g_proveStatement); for (i = g_proveStatement - 1; i >= 1; i--) { if (g_Statement[i].type != (char)p_) continue; /* Not a $p */ /* 30-Jan-06 nm Added single-character-match wildcard argument */ if (!matchesList(g_Statement[i].labelName, g_fullArg[1], '*', '?')) { continue; } sourceStatement = i; nmbrTmp = expandProof(nmbrSaveProof, sourceStatement /*, g_proveStatement*/); if (!nmbrEq(nmbrTmp, nmbrSaveProof)) { g_proofChangedFlag = 1; n = compressedProofSize(nmbrTmp, g_proveStatement); printLongLine(cat("Proof of \"", g_Statement[g_proveStatement].labelName, "\" ", (s == n ? cat("stayed at ", str((double)s), NULL) : cat((s < n ? "increased from " : " decreased from "), str((double)s), " to ", str((double)n), NULL)), " bytes after expanding \"", g_Statement[sourceStatement].labelName, "\".", NULL), " ", " "); s = n; nmbrLet(&nmbrSaveProof, nmbrTmp); } } if (g_proofChangedFlag) { g_proofChanged = 1; /* Cumulative flag */ /* Clear the existing proof structure */ deallocProofStruct(&g_ProofInProgress); /* Then rebuild proof structure from new proof nmbrTmp */ initProofStruct(&g_ProofInProgress, nmbrTmp, g_proveStatement); /* Save the new proof structure on the undo stack */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } else { print2("No expansion occurred. The proof was not changed.\n"); } nmbrLet(&nmbrSaveProof, NULL_NMBRSTRING); nmbrLet(&nmbrTmp, NULL_NMBRSTRING); continue; } /* EXPAND */ if (cmdMatches("DELETE STEP") || (cmdMatches("DELETE ALL"))) { if (cmdMatches("DELETE STEP")) { s = (long)val(g_fullArg[2]); /* Step number */ } else { s = nmbrLen(g_ProofInProgress.proof); } if ((g_ProofInProgress.proof)[s - 1] == -(long)'?') { print2("?Step %ld is unknown and cannot be deleted.\n", s); continue; } m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ if (s > m || s < 1) { print2("?The step must be in the range from 1 to %ld.\n", m); continue; } deleteSubProof(s - 1); n = nmbrLen(g_ProofInProgress.proof); /* New proof length */ if (m == n) { print2("Step %ld was deleted.\n", s); } else { if (n > 1) { printLongLine(cat("A ", str((double)(m - n + 1)), "-step subproof at step ", str((double)s), " was deleted. Steps ", str((double)s), ":", str((double)m), " are now ", str((double)(s - m + n)), ":", str((double)n), ".", NULL), "", " "); } else { print2("The entire proof was deleted.\n"); } } /* 6/14/98 - Automatically display new unknown steps ???Future - add switch to enable/defeat this */ typeProof(g_proveStatement, 1 /*pipFlag*/, 0 /*startStep*/, 0 /*endStep*/, 0 /*endIndent*/, 1 /*essentialFlag*/, 0 /*renumberFlag*/, 1 /*unknownFlag*/, 0 /*notUnifiedFlag*/, 0 /*reverseFlag*/, 0 /*noIndentFlag*/, 0 /*splitColumn*/, 0 /*skipRepeatedSteps*/, /* 28-Jun-2013 nm */ 0 /*texFlag*/, 0 /*g_htmlFlag*/); /* 6/14/98 end */ g_proofChanged = 1; /* Cumulative flag */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); continue; } if (cmdMatches("DELETE FLOATING_HYPOTHESES")) { /* Get the essential step flags */ nmbrLet(&nmbrTmp, nmbrGetEssential(g_ProofInProgress.proof)); m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ n = 0; /* Earliest step that changed */ g_proofChangedFlag = 0; for (s = m; s > 0; s--) { /* Skip essential steps and unknown steps */ if (nmbrTmp[s - 1] == 1) continue; /* Not floating */ if ((g_ProofInProgress.proof)[s - 1] == -(long)'?') continue; /* Unknown */ /* Get the subproof length at step s */ q = subproofLen(g_ProofInProgress.proof, s - 1); deleteSubProof(s - 1); n = s - q + 1; /* Save earliest step changed */ g_proofChangedFlag = 1; s = s - q + 1; /* Adjust step position to account for deleted subpr */ } /* Next step s */ if (g_proofChangedFlag) { print2("All floating-hypothesis steps were deleted.\n"); if (n) { print2("Steps %ld and above have been renumbered.\n", n); } /* 6/14/98 - Automatically display new unknown steps ???Future - add switch to enable/defeat this */ typeProof(g_proveStatement, 1 /*pipFlag*/, 0 /*startStep*/, 0 /*endStep*/, 0 /*endIndent*/, 1 /*essentialFlag*/, 0 /*renumberFlag*/, 1 /*unknownFlag*/, 0 /*notUnifiedFlag*/, 0 /*reverseFlag*/, 0 /*noIndentFlag*/, 0 /*splitColumn*/, 0 /*skipRepeatedSteps*/, /* 28-Jun-2013 nm */ 0 /*texFlag*/, 0 /*g_htmlFlag*/); /* 6/14/98 end */ g_proofChanged = 1; /* Cumulative flag */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } else { print2("?There are no floating-hypothesis steps to delete.\n"); } continue; } /* End if DELETE FLOATING_HYPOTHESES */ if (cmdMatches("INITIALIZE")) { if (cmdMatches("INITIALIZE ALL")) { i = nmbrLen(g_ProofInProgress.proof); /* Reset the dummy variable counter (all will be refreshed) */ g_pipDummyVars = 0; /* Initialize all steps */ for (j = 0; j < i; j++) { initStep(j); } /* Assign known subproofs */ assignKnownSubProofs(); print2("All steps have been initialized.\n"); g_proofChanged = 1; /* Cumulative flag */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); continue; } /* Added 16-Apr-06 nm */ if (cmdMatches("INITIALIZE USER")) { i = nmbrLen(g_ProofInProgress.proof); /* Delete all LET STEP assignments */ for (j = 0; j < i; j++) { nmbrLet((nmbrString **)(&((g_ProofInProgress.user)[j])), NULL_NMBRSTRING); } print2( "All LET STEP user assignments have been initialized (i.e. deleted).\n"); g_proofChanged = 1; /* Cumulative flag */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); continue; } /* End 16-Apr-06 */ /* cmdMatches("INITIALIZE STEP") */ s = (long)val(g_fullArg[2]); /* Step number */ if (s > nmbrLen(g_ProofInProgress.proof) || s < 1) { print2("?The step must be in the range from 1 to %ld.\n", nmbrLen(g_ProofInProgress.proof)); continue; } initStep(s - 1); /* Also delete LET STEPs, per HELP INITIALIZE */ /* 16-Apr-06 */ nmbrLet((nmbrString **)(&((g_ProofInProgress.user)[s - 1])), /* 16-Apr-06 */ NULL_NMBRSTRING); /* 16-Apr-06 */ print2( "Step %ld and its hypotheses have been initialized.\n", s); g_proofChanged = 1; /* Cumulative flag */ processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); continue; } if (cmdMatches("SEARCH")) { if (switchPos("/ ALL")) { m = 1; /* Include $e, $f statements */ } else { m = 0; /* Show $a, $p only */ } /* 14-Apr-2008 nm added */ if (switchPos("/ JOIN")) { joinFlag = 1; /* Join $e's to $a,$p for matching */ } else { joinFlag = 0; /* Search $a,$p by themselves */ } if (switchPos("/ COMMENTS")) { n = 1; /* Search comments */ } else { n = 0; /* Search statement math symbols */ } let(&str1, g_fullArg[2]); /* String to match */ if (n) { /* COMMENTS switch */ /* Trim leading, trailing spaces; reduce white space to space; convert to upper case */ let(&str1, edit(str1, 8 + 16 + 128 + 32)); } else { /* No COMMENTS switch */ /* Trim leading, trailing spaces; reduce white space to space */ let(&str1, edit(str1, 8 + 16 + 128)); /* Change all spaces to double spaces */ q = (long)strlen(str1); let(&str3, space(q + q)); s = 0; for (p = 0; p < q; p++) { str3[p + s] = str1[p]; if (str1[p] == ' ') { s++; str3[p + s] = str1[p]; } } let(&str1, left(str3, q + s)); /* 30-Jan-06 nm Added single-character-match wildcard argument "$?" (or "?" for convenience). Use ASCII 3 for the exactly-1-char wildcard character. This is a single-character match, not a single-token match: we need "??" to match "ph". */ while (1) { p = instr(1, str1, "$?"); if (!p) break; let(&str1, cat(left(str1, p - 1), chr(3), right(str1, p + 2), NULL)); } /* Allow just "?" for convenience. */ while (1) { p = instr(1, str1, "?"); if (!p) break; let(&str1, cat(left(str1, p - 1), chr(3), right(str1, p + 1), NULL)); } /* End of 30-Jan-06 addition */ /* Change wildcard to ASCII 2 (to be different from printable chars) */ /* 1/3/02 (Why are we matching with and without space? I'm not sure.)*/ /* 30-Jan-06 nm Answer: We need the double-spacing, and the removal of space in the "with spaces" case, so that "ph $ ph" will match "ph ph" (0-token case) - "ph $ ph" won't match this in the (character-based, not token-based) matches(). The "with spaces" case is for matching whole tokens, whereas the "without spaces" case is for matching part of a token. */ while (1) { p = instr(1, str1, " $* "); if (!p) break; /* This removes the space before and after the $* */ let(&str1, cat(left(str1, p - 1), chr(2), right(str1, p + 4), NULL)); } while (1) { p = instr(1, str1, "$*"); if (!p) break; /* This simply replaces $* with chr(2) */ let(&str1, cat(left(str1, p - 1), chr(2), right(str1, p + 2), NULL)); } /* 1/3/02 Also allow a plain $ as a wildcard, for convenience. */ while (1) { p = instr(1, str1, " $ "); if (!p) break; /* 30-Jan-06 nm Bug fix - changed "2" to "3" below in order to properly match 0 tokens */ let(&str1, cat(left(str1, p - 1), chr(2), right(str1, p + 3), NULL)); } while (1) { /* Note: the "$" shortcut must be done last to avoid picking up "$*" and "$?". */ p = instr(1, str1, "$"); if (!p) break; let(&str1, cat(left(str1, p - 1), chr(2), right(str1, p + 1), NULL)); } /* Add wildcards to beginning and end to match middle of any string */ let(&str1, cat(chr(2), " ", str1, " ", chr(2), NULL)); } /* End no COMMENTS switch */ for (i = 1; i <= g_statements; i++) { if (!g_Statement[i].labelName[0]) continue; /* No label */ if (!m && g_Statement[i].type != (char)p_ && g_Statement[i].type != (char)a_) { continue; /* No /ALL switch */ } /* 30-Jan-06 nm Added single-character-match wildcard argument */ if (!matchesList(g_Statement[i].labelName, g_fullArg[1], '*', '?')) continue; if (n) { /* COMMENTS switch */ let(&str2, ""); str2 = getDescription(i); /* str2 must be deallocated here */ /* Strip linefeeds and reduce spaces; cvt to uppercase */ j = instr(1, edit(str2, 4 + 8 + 16 + 128 + 32), str1); if (!j) { /* No match */ let(&str2, ""); continue; } /* Strip linefeeds and reduce spaces */ let(&str2, edit(str2, 4 + 8 + 16 + 128)); j = j + ((long)strlen(str1) / 2); /* Center of match location */ p = g_screenWidth - 7 - (long)strlen(str((double)i)) - (long)strlen(g_Statement[i].labelName); /* Longest comment portion that will fit in one line */ q = (long)strlen(str2); /* Length of comment */ if (q <= p) { /* Use entire comment */ let(&str3, str2); } else { if (q - j <= p / 2) { /* Use right part of comment */ let(&str3, cat("...", right(str2, q - p + 4), NULL)); } else { if (j <= p / 2) { /* Use left part of comment */ let(&str3, cat(left(str2, p - 3), "...", NULL)); } else { /* Use middle part of comment */ let(&str3, cat("...", mid(str2, j - p / 2, p - 6), "...", NULL)); } } } print2("%s\n", cat(str((double)i), " ", g_Statement[i].labelName, " $", chr(g_Statement[i].type), " \"", str3, "\"", NULL)); let(&str2, ""); } else { /* No COMMENTS switch */ let(&str2,nmbrCvtMToVString(g_Statement[i].mathString)); /* 14-Apr-2008 nm JOIN flag */ tmpFlag = 0; /* Flag that $p or $a is already in string */ if (joinFlag && (g_Statement[i].type == (char)p_ || g_Statement[i].type == (char)a_)) { /* If $a or $p, prepend $e's to string to match */ k = nmbrLen(g_Statement[i].reqHypList); for (j = k - 1; j >= 0; j--) { p = g_Statement[i].reqHypList[j]; if (g_Statement[p].type == (char)e_) { let(&str2, cat("$e ", nmbrCvtMToVString(g_Statement[p].mathString), tmpFlag ? "" : cat(" $", chr(g_Statement[i].type), NULL), " ", str2, NULL)); tmpFlag = 1; /* Flag that a $p or $a was added */ } } } /* Change all spaces to double spaces */ q = (long)strlen(str2); let(&str3, space(q + q)); s = 0; for (p = 0; p < q; p++) { str3[p + s] = str2[p]; if (str2[p] == ' ') { s++; str3[p + s] = str2[p]; } } let(&str2, left(str3, q + s)); let(&str2, cat(" ", str2, " ", NULL)); /* 30-Jan-06 nm Added single-character-match wildcard argument */ /* We should use matches() and not matchesList() here, because commas can be legal token characters in math symbols */ if (!matches(str2, str1, 2/* ascii 2 0-or-more-token match char*/, 3/* ascii 3 single-token-match char*/)) continue; let(&str2, edit(str2, 8 + 16 + 128)); /* Trim leading, trailing spaces; reduce white space to space */ printLongLine(cat(str((double)i)," ", g_Statement[i].labelName, tmpFlag ? "" : cat(" $", chr(g_Statement[i].type), NULL), " ", str2, NULL), " ", " "); } /* End no COMMENTS switch */ } /* Next i */ continue; } if (cmdMatches("SET ECHO")) { if (cmdMatches("SET ECHO ON")) { g_commandEcho = 1; /* 15-Jun-2009 nm Added "!" (see 15-Jun-2009 note above) */ print2("!SET ECHO ON\n"); print2("Command line echoing is now turned on.\n"); } else { g_commandEcho = 0; print2("Command line echoing is now turned off.\n"); } continue; } if (cmdMatches("SET MEMORY_STATUS")) { if (cmdMatches("SET MEMORY_STATUS ON")) { print2("Memory status display has been turned on.\n"); print2("This command is intended for debugging purposes only.\n"); g_memoryStatus = 1; } else { g_memoryStatus = 0; print2("Memory status display has been turned off.\n"); } continue; } if (cmdMatches("SET JEREMY_HENTY_FILTER")) { if (cmdMatches("SET JEREMY_HENTY_FILTER ON")) { print2("The unification equivalence filter has been turned on.\n"); print2("This command is intended for debugging purposes only.\n"); g_hentyFilter = 1; } else { print2("This command is intended for debugging purposes only.\n"); print2("The unification equivalence filter has been turned off.\n"); g_hentyFilter = 0; } continue; } if (cmdMatches("SET EMPTY_SUBSTITUTION")) { if (cmdMatches("SET EMPTY_SUBSTITUTION ON")) { g_minSubstLen = 0; print2("Substitutions with empty symbol sequences is now allowed.\n"); continue; } if (cmdMatches("SET EMPTY_SUBSTITUTION OFF")) { g_minSubstLen = 1; printLongLine(cat("The ability to substitute empty expressions", " for variables has been turned off. Note that this may", " make the Proof Assistant too restrictive in some cases.", NULL), "", " "); continue; } } if (cmdMatches("SET SEARCH_LIMIT")) { s = (long)val(g_fullArg[2]); /* Timeout value */ print2("IMPROVE search limit has been changed from %ld to %ld\n", g_userMaxProveFloat, s); g_userMaxProveFloat = s; continue; } if (cmdMatches("SET WIDTH")) { /* 18-Nov-85 nm Was SCREEN_WIDTH */ s = (long)val(g_fullArg[2]); /* Screen width value */ /************ 19-Jun-2020 nm printBuffer is now dynamically allocated if (s >= PRINTBUFFERSIZE - 1) { print2( "?Maximum screen width is %ld. Recompile with larger PRINTBUFFERSIZE in\n", (long)(PRINTBUFFERSIZE - 2)); print2("mminou.h if you need more.\n"); continue; } *************/ /* 26-Sep-2017 nm */ /* TODO: figure out why s=2 crashes program! */ if (s < 3) s = 3; /* Less than 3 may cause a segmentation fault */ i = g_screenWidth; g_screenWidth = s; /* 26-Sep-2017 nm - print with new screen width */ print2("Screen width has been changed from %ld to %ld.\n", i, s); continue; } if (cmdMatches("SET HEIGHT")) { /* 18-Nov-05 nm Added */ s = (long)val(g_fullArg[2]); /* Screen height value */ if (s < 2) s = 2; /* Less than 2 makes no sense */ i = g_screenHeight; g_screenHeight = s - 1; print2("Screen height has been changed from %ld to %ld.\n", i + 1, s); /* g_screenHeight is one less than the physical screen to account for the prompt line after pausing. */ continue; } /* 10-Jul-2016 nm */ if (cmdMatches("SET DISCOURAGEMENT")) { if (!strcmp(g_fullArg[2], "ON")) { g_globalDiscouragement = 1; print2("\"(...is discouraged.)\" markup tags are now honored.\n"); } else if (!strcmp(g_fullArg[2], "OFF")) { print2( "\"(...is discouraged.)\" markup tags are no longer honored.\n"); /* print2("\n"); */ /* Enable for more emphasis */ print2( ">>> ?Warning: This setting is intended for advanced users only. Please turn\n"); print2( ">>> it back ON if you are not intimately familiar with this database.\n"); /* print2("\n"); */ /* Enable for more emphasis */ g_globalDiscouragement = 0; } else { bug(1129); } continue; } /* 14-May-2017 nm */ if (cmdMatches("SET CONTRIBUTOR")) { print2("\"Contributed by...\" name was changed from \"%s\" to \"%s\"\n", g_contributorName, g_fullArg[2]); let(&g_contributorName, g_fullArg[2]); continue; } /* 31-Dec-2017 nm */ if (cmdMatches("SET ROOT_DIRECTORY")) { let(&str1, g_rootDirectory); /* Save previous one */ let(&g_rootDirectory, edit(g_fullArg[2], 2/*discard spaces,tabs*/)); if (g_rootDirectory[0] != 0) { /* Not an empty directory path */ /* Add trailing "/" to g_rootDirectory if missing */ if (instr(1, g_rootDirectory, "\\") != 0 || instr(1, g_input_fn, "\\") != 0 || instr(1, g_output_fn, "\\") != 0 ) { /* Using Windows-style path (not really supported, but at least make full path consistent) */ if (g_rootDirectory[strlen(g_rootDirectory) - 1] != '\\') { let(&g_rootDirectory, cat(g_rootDirectory, "\\", NULL)); } } else { if (g_rootDirectory[strlen(g_rootDirectory) - 1] != '/') { let(&g_rootDirectory, cat(g_rootDirectory, "/", NULL)); } } } if (strcmp(str1, g_rootDirectory)){ print2("Root directory was changed from \"%s\" to \"%s\"\n", str1, g_rootDirectory); } let(&str1, ""); continue; } /* 1-Nov-2013 nm Added UNDO */ if (cmdMatches("SET UNDO")) { s = (long)val(g_fullArg[2]); /* Maximum UNDOs */ if (s < 0) s = 0; /* Less than 0 UNDOs makes no sense */ /* Reset the stack size if it changed */ if (processUndoStack(NULL, PUS_GET_SIZE, "", 0) != s) { print2( "The maximum number of UNDOs was changed from %ld to %ld\n", processUndoStack(NULL, PUS_GET_SIZE, "", 0), s); processUndoStack(NULL, PUS_NEW_SIZE, "", s); if (g_PFASmode == 1) { /* If we're in the Proof Assistant, assign the first stack entry with the current proof (the stack was erased) */ processUndoStack(&g_ProofInProgress, PUS_PUSH, "", 0); } } else { print2("The maximum number of UNDOs was not changed.\n"); } continue; } if (cmdMatches("SET UNIFICATION_TIMEOUT")) { s = (long)val(g_fullArg[2]); /* Timeout value */ print2("Unification timeout has been changed from %ld to %ld\n", g_userMaxUnifTrials,s); g_userMaxUnifTrials = s; continue; } if (cmdMatches("OPEN LOG")) { /* Open a log file */ let(&g_logFileName, g_fullArg[2]); g_logFilePtr = fSafeOpen(g_logFileName, "w", 0/*noVersioningFlag*/); if (!g_logFilePtr) continue; /* Couldn't open it (err msg was provided) */ g_logFileOpenFlag = 1; print2("The log file \"%s\" was opened %s %s.\n",g_logFileName, date(),time_()); continue; } if (cmdMatches("CLOSE LOG")) { /* Close the log file */ if (!g_logFileOpenFlag) { print2("?Sorry, there is no log file currently open.\n"); } else { print2("The log file \"%s\" was closed %s %s.\n",g_logFileName, date(),time_()); fclose(g_logFilePtr); g_logFileOpenFlag = 0; } let(&g_logFileName,""); continue; } if (cmdMatches("OPEN TEX")) { /* 2-Oct-2017 nm OPEN HTML is very obsolete, no need to warn anymore if (cmdMatches("OPEN TEX") || cmdMatches("OPEN HTML") ) { if (cmdMatches("OPEN HTML")) { print2("?OPEN HTML is obsolete - use SHOW STATEMENT * / HTML\n"); continue; } */ /* 17-Nov-2015 TODO: clean up mixed LaTeX/HTML attempts (check g_texFileOpenFlag when switching to HTML & close LaTeX file) */ if (g_texDefsRead) { /* Current limitation - can only read .def once */ /* 2-Oct-2017 nm OPEN HTML is obsolete */ /*if (cmdMatches("OPEN HTML") != g_htmlFlag) {*/ if (g_htmlFlag) { /* Actually it isn't clear to me this is still the case, but to be safe I left it in */ print2("?You cannot use both LaTeX and HTML in the same session.\n"); print2( "?You must EXIT and restart Metamath to switch to the other.\n"); continue; } } /* 2-Oct-2017 nm OPEN HTML is obsolete */ /*g_htmlFlag = cmdMatches("OPEN HTML");*/ /* Open a TeX file */ let(&g_texFileName,g_fullArg[2]); if (switchPos("/ NO_HEADER")) { texHeaderFlag = 0; } else { texHeaderFlag = 1; } /* 14-Sep-2010 nm Added OLD_TEX */ if (switchPos("/ OLD_TEX")) { g_oldTexFlag = 1; } else { g_oldTexFlag = 0; } g_texFilePtr = fSafeOpen(g_texFileName, "w", 0/*noVersioningFlag*/); if (!g_texFilePtr) continue; /* Couldn't open it (err msg was provided) */ g_texFileOpenFlag = 1; /* 2-Oct-2017 nm OPEN HTML is obsolete */ print2("Created %s output file \"%s\".\n", g_htmlFlag ? "HTML" : "LaTeX", g_texFileName); printTexHeader(texHeaderFlag); g_oldTexFlag = 0; continue; } /* 2-Oct-2017 nm CLOSE HTML is obsolete */ /****** if (cmdMatches("CLOSE TEX") || cmdMatches("CLOSE HTML")) { if (cmdMatches("CLOSE HTML")) { print2("?CLOSE HTML is obsolete - use SHOW STATEMENT @ / HTML\n"); continue; } /@ Close the TeX file @/ if (!g_texFileOpenFlag) { print2("?Sorry, there is no %s file currently open.\n", g_htmlFlag ? "HTML" : "LaTeX"); } else { print2("The %s output file \"%s\" has been closed.\n", g_htmlFlag ? "HTML" : "LaTeX", g_texFileName); printTexTrailer(texHeaderFlag); fclose(g_texFilePtr); g_texFileOpenFlag = 0; } let(&g_texFileName,""); continue; } *****/ if (cmdMatches("CLOSE TEX")) { /* Close the TeX file */ if (!g_texFileOpenFlag) { print2("?Sorry, there is no LaTeX file currently open.\n"); } else { print2("The LaTeX output file \"%s\" has been closed.\n", g_texFileName); printTexTrailer(texHeaderFlag); fclose(g_texFilePtr); g_texFileOpenFlag = 0; } let(&g_texFileName,""); continue; } /* Similar to Unix 'more' */ if (cmdMatches("MORE")) { list1_fp = fSafeOpen(g_fullArg[1], "r", 0/*noVersioningFlag*/); if (!list1_fp) continue; /* Couldn't open it (error msg was provided) */ while (1) { if (!linput(list1_fp, NULL, &str1)) break; /* End of file */ /* Print a line on the screen */ if (!print2("%s\n", str1)) break; /* User typed Q */ } fclose(list1_fp); continue; } /* end MORE */ if (cmdMatches("FILE SEARCH")) { /* Search the contents of a file and type on the screen */ type_fp = fSafeOpen(g_fullArg[2], "r", 0/*noVersioningFlag*/); if (!type_fp) continue; /* Couldn't open it (error msg was provided) */ fromLine = 0; toLine = 0; searchWindow = 0; i = switchPos("/ FROM_LINE"); if (i) fromLine = (long)val(g_fullArg[i + 1]); i = switchPos("/ TO_LINE"); if (i) toLine = (long)val(g_fullArg[i + 1]); i = switchPos("/ WINDOW"); if (i) searchWindow = (long)val(g_fullArg[i + 1]); /*??? Implement SEARCH /WINDOW */ if (i) print2("Sorry, WINDOW has not be implemented yet.\n"); let(&str2, g_fullArg[3]); /* Search string */ let(&str2, edit(str2, 32)); /* Convert to upper case */ tmpFlag = 0; /* Search window buffer */ pntrLet(&pntrTmp, pntrSpace(searchWindow)); j = 0; /* Line # */ m = 0; /* # matches */ while (linput(type_fp, NULL, &str1)) { j++; if (j > toLine && toLine != 0) break; if (j >= fromLine || fromLine == 0) { let(&str3, edit(str1, 32)); /* Convert to upper case */ if (instr(1, str3, str2)) { /* Match occurred */ if (!tmpFlag) { tmpFlag = 1; print2( "The line number in the file is shown before each line.\n"); } m++; if (!print2("%ld: %s\n", j, left(str1, MAX_LEN - (long)strlen(str((double)j)) - 3))) break; } } for (k = 1; k < searchWindow; k++) { let((vstring *)(&pntrTmp[k - 1]), pntrTmp[k]); } if (searchWindow > 0) let((vstring *)(&pntrTmp[searchWindow - 1]), str1); } if (!tmpFlag) { print2("There were no matches.\n"); } else { if (m == 1) { print2("There was %ld matching line in the file %s.\n", m, g_fullArg[2]); } else { print2("There were %ld matching lines in the file %s.\n", m, g_fullArg[2]); } } fclose(type_fp); /* Deallocate search window buffer */ for (i = 0; i < searchWindow; i++) { let((vstring *)(&pntrTmp[i]), ""); } pntrLet(&pntrTmp, NULL_PNTRSTRING); continue; } if (cmdMatches("SET UNIVERSE") || cmdMatches("ADD UNIVERSE") || cmdMatches("DELETE UNIVERSE")) { /*continue;*/ /* ???Not implemented */ } /* end if xxx UNIVERSE */ if (cmdMatches("SET DEBUG FLAG")) { print2("Notice: The DEBUG mode is intended for development use only.\n"); print2("The printout will not be meaningful to the user.\n"); i = (long)val(g_fullArg[3]); if (i == 4) db4 = 1; /* Not used */ if (i == 5) db5 = 1; /* mmpars.c statistics; mmunif.c overview */ if (i == 6) db6 = 1; /* mmunif.c details */ if (i == 7) db7 = 1; /* mmunif.c more details; mmveri.c */ if (i == 8) db8 = 1; /* mmpfas.c unification calls */ if (i == 9) db9 = 1; /* memory */ /* use SET MEMORY_STATUS ON instead */ continue; } if (cmdMatches("SET DEBUG OFF")) { db4 = 0; db5 = 0; db6 = 0; db7 = 0; db8 = 0; db9 = 0; print2("The DEBUG mode has been turned off.\n"); continue; } if (cmdMatches("ERASE")) { if (g_sourceChanged) { print2("Warning: You have not saved changes to the source.\n"); str1 = cmdInput1("Do you want to ERASE anyway (Y, N) ? "); if (str1[0] != 'y' && str1[0] != 'Y') { print2("Use WRITE SOURCE to save the changes.\n"); continue; } g_sourceChanged = 0; } eraseSource(); g_sourceHasBeenRead = 0; /* Global variable */ /* 31-Dec-2017 nm */ g_showStatement = 0; g_proveStatement = 0; print2("Metamath has been reset to the starting state.\n"); continue; } if (cmdMatches("VERIFY PROOF")) { if (switchPos("/ SYNTAX_ONLY")) { verifyProofs(g_fullArg[2],0); /* Parse only */ } else { verifyProofs(g_fullArg[2],1); /* Parse and verify */ } continue; } /* 7-Nov-2015 nm New */ /* 17-Nov-2015 nm Updated */ /* 25-Jun-2020 nm Added UNDERSCORE_SKIP */ /* 17-Jul-2020 nm Added MATHBOX_SKIP */ if (cmdMatches("VERIFY MARKUP")) { i = (switchPos("/ DATE_SKIP") != 0) ? 1 : 0; j = (switchPos("/ TOP_DATE_SKIP") != 0) ? 1 : 0; k = (switchPos("/ FILE_SKIP") != 0) ? 1 : 0; l = (switchPos("/ UNDERSCORE_SKIP") != 0) ? 1 : 0; m = (switchPos("/ MATHBOX_SKIP") != 0) ? 1 : 0; n = (switchPos("/ VERBOSE") != 0) ? 1 : 0; if (i == 1 && j == 1) { printf( "?Only one of / DATE_SKIP and / TOP_DATE_SKIP may be specified.\n"); continue; } verifyMarkup(g_fullArg[2], (flag)i, /* 1 = skip checking date consistency */ (flag)j, /* 1 = skip checking top date only */ (flag)k, /* 1 = skip checking external files GIF, mmset.html,... */ (flag)l, /* 1 = skip checking labels for underscores */ (flag)m, /* 1 = skip checking mathbox cross-references */ (flag)n); /* 1 = verbose mode */ /* 26-Dec-2016 nm */ continue; } /* 10-Dec-2018 nm Added */ if (cmdMatches("MARKUP")) { g_htmlFlag = 1; g_altHtmlFlag = (switchPos("/ ALT_HTML") != 0); if ((switchPos("/ HTML") != 0) == (switchPos("/ ALT_HTML") != 0)) { print2("?Please specify exactly one of / HTML and / ALT_HTML.\n"); continue; } i = 0; i = ((switchPos("/ SYMBOLS") != 0) ? PROCESS_SYMBOLS : 0) + ((switchPos("/ LABELS") != 0) ? PROCESS_LABELS : 0) + ((switchPos("/ NUMBER_AFTER_LABEL") != 0) ? ADD_COLORED_LABEL_NUMBER : 0) + ((switchPos("/ BIB_REFS") != 0) ? PROCESS_BIBREFS : 0) + ((switchPos("/ UNDERSCORES") != 0) ? PROCESS_UNDERSCORES : 0); processMarkup(g_fullArg[1], /* Input file */ g_fullArg[2], /* Output file */ (switchPos("/ CSS") != 0), i); /* Action bits */ continue; } print2("?This command has not been implemented.\n"); continue; } } /* command */