diff --git a/src/mmcmdl.h b/src/mmcmdl.h index f997b770..733a4dca 100644 --- a/src/mmcmdl.h +++ b/src/mmcmdl.h @@ -8,7 +8,8 @@ #define METAMATH_MMCMDL_H_ /*! - * \file mmcmdl.h - includes for accessing the command line interpreter + * \file mmcmdl.h + * \brief includes for accessing the command line interpreter */ #include "mmvstr.h" @@ -27,7 +28,7 @@ extern pntrString *g_rawArgPntr; extern nmbrString *g_rawArgNmbr; extern long g_rawArgs; extern pntrString *g_fullArg; -extern vstring g_fullArgString; /* g_fullArg as one string */ +extern vstring g_fullArgString; /*!< g_fullArg as one string */ /*! * \var vstring g_commandPrompt * text displayed at the beginning of the line where a user is supposed to @@ -38,21 +39,22 @@ extern vstring g_commandLine; extern long g_showStatement; extern vstring g_logFileName; extern vstring g_texFileName; -extern flag g_PFASmode; /* Proof assistant mode, invoked by PROVE command */ -extern flag g_sourceChanged; /* Flag that user made some change to the source file*/ -extern flag g_proofChanged; /* Flag that user made some change to proof in progress*/ -extern flag g_commandEcho; /* Echo full command */ +extern flag g_PFASmode; /*!< Proof assistant mode, invoked by PROVE command */ +extern flag g_sourceChanged; /*!< Flag that user made some change to the source file*/ +extern flag g_proofChanged; /*!< Flag that user made some change to proof in progress*/ +extern flag g_commandEcho; /*!< Echo full command */ /*! - * \brief indicates whether the user has turned MEMORY STATUS on. + * \brief `MEMORY_STATUS` option: Always show memory * - * If the user issues SET MEMORY_STATUS ON this \a flag is set to 1. It is + * Indicates whether the user has turned MEMORY_STATUS on. + * If the user issues SET MEMORY_STATUS ON this \ref flag is set to 1. It is * reset to 0 again on a SET MEMORY_STATUS OFF command. When 1, certain * memory de/allocations are monitored - see \a db3. */ -extern flag g_memoryStatus; /* Always show memory */ +extern flag g_memoryStatus; -extern flag g_sourceHasBeenRead; /* 1 if a source file has been read in */ -extern vstring g_rootDirectory; /* Directory to use for included files */ +extern flag g_sourceHasBeenRead; /*!< 1 if a source file has been read in */ +extern vstring g_rootDirectory; /*!< Directory to use for included files */ #endif /* METAMATH_MMCMDL_H_ */ diff --git a/src/mmcmds.h b/src/mmcmds.h index 68d1ff7f..7d903655 100644 --- a/src/mmcmds.h +++ b/src/mmcmds.h @@ -7,18 +7,20 @@ #ifndef METAMATH_MMCMDS_H_ #define METAMATH_MMCMDS_H_ +/*! \file */ + #include "mmvstr.h" #include "mmdata.h" -/* Type (i.e. print) a statement */ +/*! Type (i.e. print) a statement */ void typeStatement(long statemNum, flag briefFlag, flag commentOnlyFlag, flag texFlag, flag htmlFlag); -/* Type (i.e. print) a proof */ +/*! Type (i.e. print) a proof */ void typeProof(long statemNum, - flag pipFlag, /* Type proofInProgress instead of source file proof */ + flag pipFlag, /*!< Type proofInProgress instead of source file proof */ long startStep, long endStep, long endIndent, flag essentialFlag, @@ -31,11 +33,11 @@ void typeProof(long statemNum, flag skipRepeatedSteps, flag texFlag, flag htmlFlag); -/* Show details of step */ +/*! Show details of step */ void showDetailStep(long statemNum, long detailStep); -/* Summary of statements in proof */ +/*! Summary of statements in proof */ void proofStmtSumm(long statemNum, flag essentialFlag, flag texFlag); -/* Traces back the statements used by a proof, recursively. */ +/*! Traces back the statements used by a proof, recursively. */ flag traceProof(long statemNum, flag essentialFlag, flag axiomFlag, @@ -45,18 +47,18 @@ flag traceProof(long statemNum, void traceProofWork(long statemNum, flag essentialFlag, vstring traceToList, - vstring *statementUsedFlagsP, /* 'y'/'n' flag that statement is used */ + vstring *statementUsedFlagsP, /*!< 'y'/'n' flag that statement is used */ nmbrString **unprovedListP); -/* Traces back the statements used by a proof, recursively, with tree display.*/ +/*! Traces back the statements used by a proof, recursively, with tree display.*/ void traceProofTree(long statemNum, flag essentialFlag, long endIndent); void traceProofTreeRec(long statemNum, flag essentialFlag, long endIndent, long recursDepth); -/* Counts the number of steps a completely exploded proof would require */ -/* (Recursive) */ -/* 0 is returned if some assertions have incomplete proofs. */ +/*! Counts the number of steps a completely exploded proof would require + (Recursive) + 0 is returned if some assertions have incomplete proofs. */ double countSteps(long statemNum, flag essentialFlag); -/* Traces what statements require the use of a given statement */ +/*! Traces what statements require the use of a given statement */ vstring traceUsage(long statemNum, flag recursiveFlag, long cutoffStmt /* if nonzero, stop scan there */); @@ -64,7 +66,7 @@ vstring htmlDummyVars(long showStmt); vstring htmlAllowedSubst(long showStmt); void readInput(void); -/* WRITE SOURCE command */ +/*! WRITE SOURCE command */ void writeSource( flag reformatFlag /* 1 = "/ FORMAT", 2 = "/REWRAP" */, flag splitFlag, /* /SPLIT - write out separate $[ $] includes */ @@ -73,7 +75,7 @@ void writeSource( when /SPIT is not specified */ vstring extractLabels); /* "" means write everything */ -/* Get info for WRITE SOURCE ... / EXTRACT */ +/*! Get info for WRITE SOURCE ... / EXTRACT */ void writeExtractedSource(vstring extractLabels, /* EXTRACT argument provided by user */ vstring fullOutput_fn, flag noVersioningFlag); @@ -84,7 +86,7 @@ void eraseSource(void); void verifyProofs(vstring labelMatch, flag verifyFlag); -/* If checkFiles = 0, do not open external files. +/*! If checkFiles = 0, do not open external files. If checkFiles = 1, check for presence of gifs and biblio file */ void verifyMarkup(vstring labelMatch, flag dateCheck, flag topDateCheck, flag fileCheck, @@ -95,51 +97,53 @@ void verifyMarkup(vstring labelMatch, flag dateCheck, flag topDateCheck, void processMarkup(vstring inputFileName, vstring outputFileName, flag processCss, long actionBits); -/* List "discouraged" statements with "(Proof modification is discouraged." +/*! List "discouraged" statements with "(Proof modification is discouraged." and "(New usage is discouraged.)" comment markup tags. */ void showDiscouraged(void); -/* Take a relative step FIRST, LAST, +nn, -nn (relative to the unknown +/*! Take a relative step FIRST, LAST, +nn, -nn (relative to the unknown essential steps) or ALL, and return the actual step for use by ASSIGN, IMPROVE, REPLACE, LET (or 0 in case of ALL, used by IMPROVE). In case stepStr is an unsigned integer nn, it is assumed to already be an actual step and is returned as is. If format is illegal, -1 is returned. */ -long getStepNum(vstring relStep, /* User's argument */ - nmbrString *pfInProgress, /* proofInProgress.proof */ - flag allFlag /* 1 = "ALL" is permissible */); +long getStepNum(vstring relStep, /*!< User's argument */ + nmbrString *pfInProgress, /*!< proofInProgress.proof */ + flag allFlag /*!< 1 = "ALL" is permissible */); -/* Convert the actual step numbers of an unassigned step to the relative +/*! Convert the actual step numbers of an unassigned step to the relative -1, -2, etc. offset for SHOW NEW_PROOF ... /UNKNOWN, to make it easier for the user to ASSIGN the relative step number. A 0 is returned for the last unknown step. The step numbers of known steps are - unchanged. */ -/* The caller must deallocate the returned nmbrString. */ + unchanged. + The caller must deallocate the returned nmbrString. */ nmbrString *getRelStepNums(nmbrString *pfInProgress); -/* This procedure finds the next statement number whose label matches +/*! This procedure finds the next statement number whose label matches stmtName. Wildcards are allowed. If uniqueFlag is 1, there must be exactly one match, otherwise an error message is printed, and -1 is returned. If uniqueFlag is 0, the next match is returned, or -1 if there are no more matches. No error messages are printed when uniqueFlag is 0, except for the special case of startStmt=1. For use by PROVE, REPLACE, ASSIGN. */ -long getStatementNum(vstring stmtName, /* Possibly with wildcards */ - long startStmt, /* Starting statement number (1 for full scan) */ - long maxStmt, /* Must be LESS THAN this statement number */ - flag aAllowed, /* 1 means $a is allowed */ - flag pAllowed, /* 1 means $p is allowed */ - flag eAllowed, /* 1 means $e is allowed */ - flag fAllowed, /* 1 means $f is allowed */ - flag efOnlyForMaxStmt, /* If 1, $e and $f must belong to maxStmt */ - flag uniqueFlag); /* If 1, match must be unique */ - -/* For HELP processing */ +long getStatementNum( + vstring stmtName, /*!< Possibly with wildcards */ + long startStmt, /*!< Starting statement number (1 for full scan) */ + long maxStmt, /*!< Must be LESS THAN this statement number */ + flag aAllowed, /*!< 1 means $a is allowed */ + flag pAllowed, /*!< 1 means $p is allowed */ + flag eAllowed, /*!< 1 means $e is allowed */ + flag fAllowed, /*!< 1 means $f is allowed */ + flag efOnlyForMaxStmt, /*!< If 1, $e and $f must belong to maxStmt */ + flag uniqueFlag /*!< If 1, match must be unique */ +); + +/*! For HELP processing */ extern flag g_printHelp; void H(vstring helpLine); -/* For MIDI files */ -extern flag g_midiFlag; /* Set to 1 if typeProof() is to output MIDI file */ -extern vstring g_midiParam; /* Parameter string for MIDI file */ +/*! For MIDI files */ +extern flag g_midiFlag; /*!< Set to 1 if typeProof() is to output MIDI file */ +extern vstring g_midiParam; /*!< Parameter string for MIDI file */ void outputMidi(long plen, nmbrString *indentationLevels, nmbrString *logicalFlags, vstring g_midiParameter, vstring statementLabel); diff --git a/src/mmdata.c b/src/mmdata.c index 91aa7a6c..f8129d10 100644 --- a/src/mmdata.c +++ b/src/mmdata.c @@ -2448,9 +2448,6 @@ temp_pntrString *pntrTempAlloc(long size) { } -/* Make string have temporary allocation to be released by next pntrLet() */ -/* Warning: after pntrMakeTempAlloc() is called, the pntrString may NOT be - assigned again with pntrLet() */ temp_pntrString *pntrMakeTempAlloc(pntrString *s) { if (g_pntrTempAllocStackTop>=(M_MAX_ALLOC_STACK-1)) { printf( @@ -2469,12 +2466,6 @@ temp_pntrString *pntrMakeTempAlloc(pntrString *s) { } -/* pntrString assignment */ -/* This function must ALWAYS be called to make assignment to */ -/* a pntrString in order for the memory cleanup routines, etc. */ -/* to work properly. If a pntrString has never been assigned before, */ -/* it is the user's responsibility to initialize it to NULL_PNTRSTRING (the */ -/* null string). */ void pntrLet(pntrString **target, const pntrString *source) { long targetLength,sourceLength; long targetAllocLen; diff --git a/src/mmdata.h b/src/mmdata.h index 48002cc7..24ef3896 100644 --- a/src/mmdata.h +++ b/src/mmdata.h @@ -4,13 +4,14 @@ /*****************************************************************************/ /*34567890123456 (79-character line to adjust editor window) 2345678901234567*/ -/*! - * \file mmdata.h - includes for some principal data structures and data-string - * handling */ - #ifndef METAMATH_MMDATA_H_ #define METAMATH_MMDATA_H_ +/*! + * \file mmdata.h + * \brief includes for some principal data structures and data-string handling + */ + #include "mmvstr.h" /* debugging flags & variables */ @@ -139,7 +140,7 @@ typedef nmbrString temp_nmbrString; * \typedef temp_pntrString * \brief a single \a pntrString element for use in a \ref stack "stack". * - * These elements are pushed onto and popped off a \ref stack + * These elements are pushed onto and popped off a \ref stack * "stack of temporary data". Special commands can free all pointers on and * after a particular one in such a stack. */ @@ -161,88 +162,90 @@ enum mTokenType { var_, con_ }; /* Global variables related to current statement */ extern int g_currentScope; +/*! The data associated with a statement in the file */ struct statement_struct { /* Array index is statement number, starting at 1 */ - long lineNum; /* Line number in file; 0 means not yet determined */ - vstring fileName; /* File statement is in; "" means not yet determined */ - vstring labelName; /* Label of statement */ - flag uniqueLabel; /* Flag that label is unique (future implementations may + long lineNum; /*!< Line number in file; 0 means not yet determined */ + vstring fileName; /*!< File statement is in; "" means not yet determined */ + vstring labelName; /*!< Label of statement */ + flag uniqueLabel; /*!< Flag that label is unique (future implementations may allow duplicate labels on hypotheses) */ - char type; /* 2nd character of keyword, e.g. 'e' for $e */ - int scope; /* Block scope level, increased by ${ and decreased by $}; + char type; /*!< 2nd character of keyword, e.g. 'e' for $e */ + int scope; /*!< Block scope level, increased by ${ and decreased by $}; ${ has scope _before_ the increase; $} has scope _before_ the decrease */ - long beginScopeStatementNum; /* statement of previous ${ ; 0 if we're in + long beginScopeStatementNum; /*!< statement of previous ${ ; 0 if we're in outermost block */ - long endScopeStatementNum; /* statement of next $} (populated for opening + long endScopeStatementNum; /*!< statement of next $} (populated for opening ${ only, 0 otherwise); g_statements+1 if we're in outermost block */ - vstring statementPtr; /* Pointer to end of (unmodified) label section used + vstring statementPtr; /*!< Pointer to end of (unmodified) label section used to determine file and line number for error or info messages about the statement */ - vstring labelSectionPtr; /* Source code before statement keyword + vstring labelSectionPtr; /*!< Source code before statement keyword - will be updated if labelSection changed */ long labelSectionLen; - char labelSectionChanged; /* Default is 0; if 1, labelSectionPtr points to an + char labelSectionChanged; /*!< Default is 0; if 1, labelSectionPtr points to an allocated vstring that must be freed by ERASE */ - vstring mathSectionPtr; /* Source code between keyword and $= or $. */ + vstring mathSectionPtr; /*!< Source code between keyword and $= or $. */ long mathSectionLen; - char mathSectionChanged; /* Default is 0; if 1, mathSectionPtr points to an + char mathSectionChanged; /*!< Default is 0; if 1, mathSectionPtr points to an allocated vstring that must be freed by ERASE */ - vstring proofSectionPtr; /* Source code between $= and $. */ + vstring proofSectionPtr; /*!< Source code between $= and $. */ long proofSectionLen; - char proofSectionChanged; /* Default is 0; if 1, proofSectionPtr points to an + char proofSectionChanged; /*!< Default is 0; if 1, proofSectionPtr points to an allocated vstring that must be freed by ERASE */ - nmbrString *mathString; /* Parsed mathSection */ + nmbrString *mathString; /*!< Parsed mathSection */ long mathStringLen; - nmbrString *proofString; /* Parsed proofSection (used by $p's only */ - nmbrString *reqHypList; /* Required hypotheses (excluding $d's) */ - nmbrString *optHypList; /* Optional hypotheses (excluding $d's) */ - long numReqHyp; /* Number of required hypotheses */ - nmbrString *reqVarList; /* Required variables */ - nmbrString *optVarList; /* Optional variables */ - nmbrString *reqDisjVarsA; /* Required disjoint variables, 1st of pair */ - nmbrString *reqDisjVarsB; /* Required disjoint variables, 2nd of pair */ - nmbrString *reqDisjVarsStmt; /* Req disjoint variables, statem number */ - nmbrString *optDisjVarsA; /* Optional disjoint variables, 1st of pair */ - nmbrString *optDisjVarsB; /* Optional disjoint variables, 2nd of pair */ - nmbrString *optDisjVarsStmt; /* Opt disjoint variables, statem number */ - long pinkNumber; /* The $a/$p sequence number for web pages */ - long headerStartStmt; /* # of stmt following previous $a, $p */ - }; - -/* Sort keys for statement labels (allocated by parseLabels) */ + nmbrString *proofString; /*!< Parsed proofSection (used by $p's only */ + nmbrString *reqHypList; /*!< Required hypotheses (excluding $d's) */ + nmbrString *optHypList; /*!< Optional hypotheses (excluding $d's) */ + long numReqHyp; /*!< Number of required hypotheses */ + nmbrString *reqVarList; /*!< Required variables */ + nmbrString *optVarList; /*!< Optional variables */ + nmbrString *reqDisjVarsA; /*!< Required disjoint variables, 1st of pair */ + nmbrString *reqDisjVarsB; /*!< Required disjoint variables, 2nd of pair */ + nmbrString *reqDisjVarsStmt; /*!< Req disjoint variables, statem number */ + nmbrString *optDisjVarsA; /*!< Optional disjoint variables, 1st of pair */ + nmbrString *optDisjVarsB; /*!< Optional disjoint variables, 2nd of pair */ + nmbrString *optDisjVarsStmt; /*!< Opt disjoint variables, statem number */ + long pinkNumber; /*!< The $a/$p sequence number for web pages */ + long headerStartStmt; /*!< # of stmt following previous $a, $p */ +}; + +/*! Sort keys for statement labels (allocated by parseLabels) */ extern long *g_labelKey; +/*! This structure holds all information related to $[ $] (include) statements + in the input source files, for error message processing. */ struct includeCall_struct { - /* This structure holds all information related to $[ $] (include) statements - in the input source files, for error message processing. */ - vstring source_fn; /* Name of the file where the + vstring source_fn; /*!< Name of the file where the inclusion source is located (= parent file for $( Begin $[... etc.) */ - vstring included_fn; /* Name of the file in the + vstring included_fn; /*!< Name of the file in the inclusion statement e.g. "$( Begin $[ included_fn..." */ - long current_offset; /* This is the starting + long current_offset; /*!< This is the starting character position of the included file w.r.t entire source buffer */ - long current_line; /* The line number + long current_line; /*!< The line number of the start of the included file (=1) or the continuation line of the parent file */ - flag pushOrPop; /* 0 means included file, 1 means continuation of parent */ - vstring current_includeSource; /* (Currently) assigned + flag pushOrPop; /*!< 0 means included file, 1 means continuation of parent */ + vstring current_includeSource; /*!< (Currently) assigned only if we may need it for a later Begin comparison */ - long current_includeLength; /* Length of the file + long current_includeLength; /*!< Length of the file to be included (0 if the file was previously included) */ - }; +}; +/*! The data associated with a math token. */ struct mathToken_struct { - vstring tokenName; /* may be used more than once at different scopes */ - long length; /* to speed up parsing scans */ - char tokenType; /* variable or constant - (char)var_ or (char)con_ */ - flag active; /* 1 if token is recognized in current scope */ - int scope; /* scope level token was declared at */ - long tmp; /* Temporary field use to speed up certain functions */ - long statement; /* Statement declared in */ - long endStatement; /* Statement of end of scope it was declared in */ - }; - -/* Sort keys for math tokens (allocated by parseMathDecl) */ + vstring tokenName; /*!< may be used more than once at different scopes */ + long length; /*!< to speed up parsing scans */ + char tokenType; /*!< variable or constant - (char)var_ or (char)con_ */ + flag active; /*!< 1 if token is recognized in current scope */ + int scope; /*!< scope level token was declared at */ + long tmp; /*!< Temporary field use to speed up certain functions */ + long statement; /*!< Statement declared in */ + long endStatement; /*!< Statement of end of scope it was declared in */ +}; + +/*! Sort keys for math tokens (allocated by parseMathDecl) */ extern long *g_mathKey; extern long g_MAX_STATEMENTS; @@ -250,7 +253,7 @@ extern long g_MAX_MATHTOKENS; extern struct statement_struct *g_Statement; /*Obs*/ /*extern struct label_struct *label;*/ -/* Warning: mathToken[i] is 0-based, not 1-based! */ +/*! \warning `mathToken[i]` is 0-based, not 1-based! */ extern struct mathToken_struct *g_MathToken; extern long g_statements, /*labels,*/ g_mathTokens; @@ -258,8 +261,8 @@ extern long g_MAX_INCLUDECALLS; extern struct includeCall_struct *g_IncludeCall; extern long g_includeCalls; -extern char *g_sourcePtr; /* Pointer to buffer in memory with input source */ -extern long g_sourceLen; /* Number of chars. in all inputs files combined (after includes)*/ +extern char *g_sourcePtr; /*!< Pointer to buffer in memory with input source */ +extern long g_sourceLen; /*!< Number of chars. in all inputs files combined (after includes)*/ /* For use by getMarkupFlag() */ #define PROOF_DISCOURAGED_MARKUP "(Proof modification is discouraged.)" @@ -295,7 +298,7 @@ void *poolFixedMalloc(long size /* bytes */); void *poolMalloc(long size /* bytes */); void poolFree(void *ptr); void addToUsedPool(void *ptr); -/* Purges reset memory pool usage */ +/*! Purges reset memory pool usage */ void memFreePoolPurge(flag untilOK); /* Statistics */ /*! @@ -325,13 +328,12 @@ void memFreePoolPurge(flag untilOK); */ void getPoolStats(long *freeAlloc, long *usedAlloc, long *usedActual); -/* Initial memory allocation */ +/*! Initial memory allocation */ void initBigArrays(void); -/* Find the number of free memory bytes */ +/*! Find the number of free memory bytes */ long getFreeSpace(long max); -/* Fatal memory allocation error */ /*! * \fn outOfMemory * \brief fatal memory allocation error. @@ -349,14 +351,14 @@ long getFreeSpace(long max); */ void outOfMemory(const char *msg); -/* Bug check error */ /*! * \fn bug + * Bug check error */ void bug(int bugNum); -/* Null nmbrString -- -1 flags the end of a nmbrString */ +/*! Null nmbrString -- -1 flags the end of a nmbrString */ struct nullNmbrStruct { long poolLoc; long allocSize; @@ -369,7 +371,9 @@ extern struct nullNmbrStruct g_NmbrNull; /*! * \struct nullPntrStruct - * describing a \ref block of \a pntrString containing only the null + * \brief Null pntrString -- NULL flags the end of a pntrString + * + * Describes a \ref block of \ref pntrString containing only the null * pointer. Besides this pointer it is accompanied with a header containing * the hidden administrative values of such \ref block "block". * @@ -379,32 +383,32 @@ extern struct nullNmbrStruct g_NmbrNull; * \bug The C standard does not require a long having the same size as a * void*. In fact there might be **no** integer type matching a pointer in size. */ -/* Null pntrString -- NULL flags the end of a pntrString */ struct nullPntrStruct { - /*! - * An instance of a nullPntrStruct is always standalone and never part of a - * larger pool. Indicated by the fixed value -1. - */ - long poolLoc; - /*! - * allocated size of the memory block containing the \a pntrString, - * excluding any hidden administrative data. - * Note: this is the number of bytes, not elements! Fixed to the size of a - * single void* instance. - */ - long allocSize; - /*! - * currently used size of the memory block containing the \a pntrString, - * excluding any hidden administrative data. - * Note: this is the number of bytes, not elements! Fixed to the size of a - * single pointer element. - */ - long actualSize; - /*! - * memory for a single void* instance, set and fixed to the null pointer. - * A null marks the end of the array. - */ - pntrString nullElement; }; + /*! + * An instance of a nullPntrStruct is always standalone and never part of a + * larger pool. Indicated by the fixed value -1. + */ + long poolLoc; + /*! + * allocated size of the memory block containing the \ref pntrString, + * excluding any hidden administrative data. + * Note: this is the number of bytes, not elements! Fixed to the size of a + * single void* instance. + */ + long allocSize; + /*! + * currently used size of the memory block containing the \ref pntrString, + * excluding any hidden administrative data. + * Note: this is the number of bytes, not elements! Fixed to the size of a + * single pointer element. + */ + long actualSize; + /*! + * memory for a single void* instance, set and fixed to the null pointer. + * A null marks the end of the array. + */ + pntrString nullElement; +}; /*! * \var g_PntrNull * Global instance of a memory block structured like a @@ -436,12 +440,12 @@ extern struct nullPntrStruct g_PntrNull; #define free_pntrString(x) pntrLet(&x, NULL_PNTRSTRING) -/* This function returns a 1 if any entry in a comma-separated list +/*! This function returns a 1 if any entry in a comma-separated list matches using the matches() function. */ flag matchesList(const char *testString, const char *pattern, char wildCard, char oneCharWildCard); -/* This function returns a 1 if the first argument matches the pattern of +/*! This function returns a 1 if the first argument matches the pattern of the second argument. The second argument may have 0-or-more and exactly-1 character match wildcards, typically '*' and '?'.*/ flag matches(const char *testString, const char *pattern, char wildCard, @@ -461,9 +465,9 @@ extern long g_nmbrStartTempAllocStack; /* Where to start freeing temporary allocation when nmbrLet() is called (normally 0, except for nested nmbrString functions) */ -/* Make string have temporary allocation to be released by next nmbrLet() */ -/* Warning: after nmbrMakeTempAlloc() is called, the nmbrString may NOT be - assigned again with nmbrLet() */ +/*! \brief Make string have temporary allocation to be released by next nmbrLet() + \warning after nmbrMakeTempAlloc() is called, the nmbrString may NOT be + assigned again with nmbrLet() */ temp_nmbrString *nmbrMakeTempAlloc(nmbrString *s); /* Make string have temporary allocation to be released by next nmbrLet() */ @@ -471,114 +475,118 @@ temp_nmbrString *nmbrMakeTempAlloc(nmbrString *s); /**************************************************/ -/* String assignment - MUST be used to assign vstrings */ +/*! String assignment - MUST be used to assign vstrings */ void nmbrLet(nmbrString **target, const nmbrString *source); -/* String concatenation - last argument MUST be NULL */ +/*! String concatenation - last argument MUST be NULL */ temp_nmbrString *nmbrCat(const nmbrString *string1,...); -/* Emulation of nmbrString functions similar to BASIC string functions */ +/*! Emulation of nmbrString functions similar to BASIC string functions */ temp_nmbrString *nmbrSeg(const nmbrString *sin, long p1, long p2); temp_nmbrString *nmbrMid(const nmbrString *sin, long p, long l); temp_nmbrString *nmbrLeft(const nmbrString *sin, long n); temp_nmbrString *nmbrRight(const nmbrString *sin, long n); -/* Allocate and return an "empty" string n "characters" long */ +/*! Allocate and return an "empty" string n "characters" long */ temp_nmbrString *nmbrSpace(long n); long nmbrLen(const nmbrString *s); long nmbrAllocLen(const nmbrString *s); void nmbrZapLen(nmbrString *s, long length); -/* Search for string2 in string 1 starting at start_position */ +/*! Search for string2 in string 1 starting at start_position */ long nmbrInstr(long start, const nmbrString *sin, const nmbrString *s); -/* Search for string2 in string 1 in reverse starting at start_position */ -/* (Reverse nmbrInstr) */ +/*! Search for string2 in string 1 in reverse starting at start_position + * (Reverse nmbrInstr) + */ long nmbrRevInstr(long start_position, const nmbrString *string1, const nmbrString *string2); -/* 1 if strings are equal, 0 otherwise */ +/*! 1 if strings are equal, 0 otherwise */ flag nmbrEq(const nmbrString *s, const nmbrString *t); -/* Converts mString to a vstring with one space between tokens */ +/*! Converts mString to a vstring with one space between tokens */ temp_vstring nmbrCvtMToVString(const nmbrString *s); -/* Converts rString to a vstring with one space between tokens */ +/*! Converts rString to a vstring with one space between tokens */ temp_vstring nmbrCvtRToVString(const nmbrString *s, flag explicitTargets, long statemNum); -/* Get step numbers in an rString - needed by cvtRToVString & elsewhere */ +/*! Get step numbers in an rString - needed by cvtRToVString & elsewhere */ nmbrString *nmbrGetProofStepNumbs(const nmbrString *reason); -/* Converts any nmbrString to an ASCII string of numbers corresponding +/*! Converts any nmbrString to an ASCII string of numbers corresponding to the .tokenNum field -- used for debugging only. */ temp_vstring nmbrCvtAnyToVString(const nmbrString *s); -/* Extract variables from a math token string */ +/*! Extract variables from a math token string */ temp_nmbrString *nmbrExtractVars(const nmbrString *m); -/* Determine if an element is in a nmbrString; return position if it is */ +/*! Determine if an element is in a nmbrString; return position if it is */ long nmbrElementIn(long start, const nmbrString *g, long element); -/* Add a single number to end of a nmbrString - faster than nmbrCat */ +/*! Add a single number to end of a nmbrString - faster than nmbrCat */ temp_nmbrString *nmbrAddElement(const nmbrString *g, long element); -/* Get the set union of two math token strings (presumably +/*! Get the set union of two math token strings (presumably variable lists) */ temp_nmbrString *nmbrUnion(const nmbrString *m1, const nmbrString *m2); -/* Get the set intersection of two math token strings (presumably +/*! Get the set intersection of two math token strings (presumably variable lists) */ temp_nmbrString *nmbrIntersection(const nmbrString *m1, const nmbrString *m2); -/* Get the set difference m1-m2 of two math token strings (presumably +/*! Get the set difference m1-m2 of two math token strings (presumably variable lists) */ temp_nmbrString *nmbrSetMinus(const nmbrString *m1,const nmbrString *m2); -/* This is a utility function that returns the length of a subproof that +/*! This is a utility function that returns the length of a subproof that ends at step */ long nmbrGetSubproofLen(const nmbrString *proof, long step); -/* This function returns a "squished" proof, putting in {} references +/*! This function returns a "squished" proof, putting in {} references to previous subproofs. */ temp_nmbrString *nmbrSquishProof(const nmbrString *proof); -/* This function un-squishes a "squished" proof, replacing {} references +/*! This function un-squishes a "squished" proof, replacing {} references to previous subproofs by the subproofs themselves. */ temp_nmbrString *nmbrUnsquishProof(const nmbrString *proof); -/* This function returns the indentation level vs. step number of a proof +/*! This function returns the indentation level vs. step number of a proof string. This information is used for formatting proof displays. The function calls itself recursively, but the first call should be with startingLevel = 0. */ temp_nmbrString *nmbrGetIndentation(const nmbrString *proof, long startingLevel); -/* This function returns essential (1) or floating (0) vs. step number of a +/*! This function returns essential (1) or floating (0) vs. step number of a proof string. This information is used for formatting proof displays. The function calls itself recursively, but the first call should be with startingLevel = 0. */ temp_nmbrString *nmbrGetEssential(const nmbrString *proof); -/* This function returns the target hypothesis vs. step number of a proof +/*! This function returns the target hypothesis vs. step number of a proof string. This information is used for formatting proof displays. The function calls itself recursively. statemNum is the statement being proved. */ temp_nmbrString *nmbrGetTargetHyp(const nmbrString *proof, long statemNum); -/* Converts a proof string to a compressed-proof-format ASCII string. - Normally, the proof string would be compacted with squishProof first, - although it's not a requirement. */ -/* The statement number is needed because required hypotheses are - implicit in the compressed proof. */ +/*! + * Converts a proof string to a compressed-proof-format ASCII string. + * Normally, the proof string would be compacted with squishProof first, + * although it's not a requirement. + * + * The statement number is needed because required hypotheses are + * implicit in the compressed proof. + */ temp_vstring compressProof(const nmbrString *proof, long statemNum, flag oldCompressionAlgorithm); -/* Gets length of the ASCII form of a compressed proof */ +/*! Gets length of the ASCII form of a compressed proof */ long compressedProofSize(const nmbrString *proof, long statemNum); @@ -602,20 +610,20 @@ extern long g_pntrStartTempAllocStack; /* Where to start freeing temporary allocation when pntrLet() is called (normally 0, except for nested pntrString functions) */ -/* Make string have temporary allocation to be released by next pntrLet() */ -/* Warning: after pntrMakeTempAlloc() is called, the pntrString may NOT be - assigned again with pntrLet() */ +/*! + * \brief Make string have temporary allocation to be released by next pntrLet() + * \warning after pntrMakeTempAlloc() is called, the pntrString may NOT be + * assigned again with pntrLet() + */ temp_pntrString *pntrMakeTempAlloc(pntrString *s); - /* Make string have temporary allocation to be - released by next pntrLet() */ /**************************************************/ -/* String assignment - MUST be used to assign vstrings */ +/*! String assignment - MUST be used to assign vstrings */ void pntrLet(pntrString **target, const pntrString *source); -/* String concatenation - last argument MUST be NULL */ +/*! String concatenation - last argument MUST be NULL */ temp_pntrString *pntrCat(const pntrString *string1,...); /* Emulation of pntrString functions similar to BASIC string functions */ @@ -624,14 +632,14 @@ temp_pntrString *pntrMid(const pntrString *sin, long p, long length); temp_pntrString *pntrLeft(const pntrString *sin, long n); temp_pntrString *pntrRight(const pntrString *sin, long n); -/* Allocate and return an "empty" string n "characters" long */ +/*! Allocate and return an "empty" string n "characters" long */ temp_pntrString *pntrSpace(long n); -/* Allocate and return an "empty" string n "characters" long +/*! Allocate and return an "empty" string n "characters" long initialized to nmbrStrings instead of vStrings */ temp_pntrString *pntrNSpace(long n); -/* Allocate and return an "empty" string n "characters" long +/*! Allocate and return an "empty" string n "characters" long initialized to pntrStrings instead of vStrings */ temp_pntrString *pntrPSpace(long n); @@ -665,76 +673,79 @@ long pntrLen(const pntrString *s); long pntrAllocLen(const pntrString *s); void pntrZapLen(pntrString *s, long length); -/* Search for string2 in string 1 starting at start_position */ +/*! Search for string2 in string 1 starting at start_position */ long pntrInstr(long start, const pntrString *sin, const pntrString *s); -/* Search for string2 in string 1 in reverse starting at start_position */ -/* (Reverse pntrInstr) */ +/*! Search for string2 in string 1 in reverse starting at start_position + (Reverse pntrInstr) */ long pntrRevInstr(long start_position, const pntrString *string1, const pntrString *string2); -/* 1 if strings are equal, 0 otherwise */ +/*! 1 if strings are equal, 0 otherwise */ flag pntrEq(const pntrString *sout, const pntrString *sin); -/* Add a single null string element to a pntrString - faster than pntrCat */ +/*! Add a single null string element to a pntrString - faster than pntrCat */ temp_pntrString *pntrAddElement(const pntrString *g); -/* Add a single null pntrString element to a pntrString - faster than pntrCat */ +/*! Add a single null pntrString element to a pntrString - faster than pntrCat */ temp_pntrString *pntrAddGElement(const pntrString *g); /* Utility functions */ -/* 0/1 knapsack algorithm */ +/*! 0/1 knapsack algorithm */ long knapsack01(long items, long *size, long *worth, long maxSize, char *itemIncluded /* output: 1 = item included, 0 = not included */); -/* 2D matrix allocation and deallocation */ +/*! 2D matrix allocation */ long **alloc2DMatrix(size_t xsize, size_t ysize); +/*! 2D matrix deallocation */ void free2DMatrix(long **matrix, size_t xsize /*, size_t ysize*/); -/* Returns the amount of indentation of a statement label. Used to +/*! Returns the amount of indentation of a statement label. Used to determine how much to indent a saved proof. */ long getSourceIndentation(long statemNum); -/* Returns any comment (description) that occurs just before a statement */ +/*! Returns any comment (description) that occurs just before a statement */ vstring getDescription(long statemNum); -/* Returns the label section of a statement with all comments except the +/*! Returns the label section of a statement with all comments except the last removed. */ vstring getDescriptionAndLabel(long statemNum); -/* Returns 1 if comment has an "is discouraged" markup tag */ +/*! Returns 1 if comment has an "is discouraged" markup tag */ flag getMarkupFlag(long statemNum, char mode); -/* Extract any contributors and dates from statement description. +/*! Extract any contributors and dates from statement description. If missing, the corresponding return string is blank. See GC_RESET etc. modes above. Caller must deallocate returned string. */ vstring getContrib(long stmtNum, char mode); -/* Extract up to 2 dates after a statement's proof. If no date is present, +/*! Extract up to 2 dates after a statement's proof. If no date is present, date1 will be blank. If no 2nd date is present, date2 will be blank. */ void getProofDate(long stmtNum, vstring *date1, vstring *date2); -/* Get date, month, year fields from a dd-mmm-yyyy date string, +/*! Get date, month, year fields from a dd-mmm-yyyy date string, where dd may be 1 or 2 digits, mmm is 1st 3 letters of month, and yyyy is 2 or 4 digits. A 1 is returned if an error was detected. */ flag parseDate(vstring dateStr, long *dd, long *mmm, long *yyyy); -/* Build date from numeric fields. mmm should be a number from 1 to 12. */ +/*! Build date from numeric fields. mmm should be a number from 1 to 12. */ void buildDate(long dd, long mmm, long yyyy, vstring *dateStr); -/* Compare two dates in the form dd-mmm-yyyy. -1 = date1 < date2, +/*! Compare two dates in the form dd-mmm-yyyy. -1 = date1 < date2, 0 = date1 = date2, 1 = date1 > date2. There is no error checking. */ flag compareDates(vstring date1, vstring date2); extern vstring g_qsortKey; - /* Used by qsortStringCmp; pointer only, do not deallocate */ -/* Comparison function for qsort */ +/*! + * \brief Comparison function for qsort + * \note Used by qsortStringCmp; pointer only, do not deallocate + */ int qsortStringCmp(const void *p1, const void *p2); -/* Call on exit to free memory */ +/*! Call on exit to free memory */ void freeData(void); #endif /* METAMATH_MMDATA_H_ */ diff --git a/src/mmhlpa.c b/src/mmhlpa.c index 816627ad..14189c07 100644 --- a/src/mmhlpa.c +++ b/src/mmhlpa.c @@ -17,7 +17,6 @@ #include "mmcmds.h" #include "mmhlpa.h" -/* help0 is mostly for TOOLS help */ void help0(vstring helpCmd) { vstring_def(saveHelpCmd); @@ -352,7 +351,6 @@ return; } /* help0 */ -/* Note: help1 should contain Metamath help */ void help1(vstring helpCmd) { vstring_def(saveHelpCmd); diff --git a/src/mmhlpa.h b/src/mmhlpa.h index ab65e07b..85d6a7c3 100644 --- a/src/mmhlpa.h +++ b/src/mmhlpa.h @@ -7,9 +7,13 @@ #ifndef METAMATH_MMHLPA_H_ #define METAMATH_MMHLPA_H_ +/*! \file */ + #include "mmvstr.h" +/*! help0 is mostly for TOOLS help */ void help0(vstring helpCmd); +/*! \note help1 should contain Metamath help */ void help1(vstring helpCmd); #endif /* METAMATH_MMHLPA_H_ */ diff --git a/src/mmhlpb.h b/src/mmhlpb.h index 87e8755f..c826640e 100644 --- a/src/mmhlpb.h +++ b/src/mmhlpb.h @@ -7,6 +7,8 @@ #ifndef METAMATH_MMHLPB_H_ #define METAMATH_MMHLPB_H_ +/*! \file */ + #include "mmvstr.h" void help2(vstring helpCmd); diff --git a/src/mminou.h b/src/mminou.h index f1789e82..e35cad20 100644 --- a/src/mminou.h +++ b/src/mminou.h @@ -4,35 +4,40 @@ /*****************************************************************************/ /*34567890123456 (79-character line to adjust editor window) 2345678901234567*/ -/*! - * \file - * Basic input and output interface. - */ - #ifndef METAMATH_MMINOU_H_ #define METAMATH_MMINOU_H_ +/*! + * \file mminou.h + * \brief Basic input and output interface. + */ + #include #include "mmvstr.h" #include "mmdata.h" -extern int g_errorCount; /* Total error count */ +extern int g_errorCount; /*!< Total error count */ /* Global variables used by print2() */ extern flag g_logFileOpenFlag; extern FILE *g_logFilePtr; + extern FILE *g_listFile_fp; -/* Global variables used by print2() */ + /*! * \var g_outputToString - * + * * Global variable redirecting the output of the function print2 from the * console ( = 0) to a string ( = 1). */ extern flag g_outputToString; + extern vstring g_printString; + + /* Global variables used by cmdInput() */ + /*! * \def MAX_COMMAND_FILE_NESTING * limits number of nested SUBMIT calls to 10. A SUBMIT redirects the input @@ -40,6 +45,7 @@ extern vstring g_printString; * so on. */ #define MAX_COMMAND_FILE_NESTING 10 + /*! * \var long g_commandFileNestingLevel * current level of nested SUBMIT commands. 0 is top level and refers to stdin @@ -49,25 +55,30 @@ extern vstring g_printString; extern long g_commandFileNestingLevel; extern FILE *g_commandFilePtr[MAX_COMMAND_FILE_NESTING + 1]; extern vstring g_commandFileName[MAX_COMMAND_FILE_NESTING + 1]; + extern flag g_commandFileSilent[MAX_COMMAND_FILE_NESTING + 1]; + /*! * \var g_commandFileSilentFlag * If set to 1, suppresses prompts on input. */ extern flag g_commandFileSilentFlag; /* For SUBMIT ... /SILENT */ -extern FILE *g_input_fp; /* File pointers */ -extern vstring g_input_fn, g_output_fn; /* File names */ -/* Warning: never call print2 with string longer than PRINTBUFFERSIZE - 1 */ -/* print2 returns 0 if the user has quit the printout. */ +extern FILE *g_input_fp; /*!< File pointers */ +extern vstring g_input_fn, g_output_fn; /*!< File names */ + +/*! print2 returns 0 if the user has quit the printout. + \warning: never call print2 with string longer than PRINTBUFFERSIZE - 1 */ flag print2(const char* fmt,...); -extern long g_screenHeight; /* Height of screen */ +extern long g_screenHeight; /*!< Height of screen */ /*! * \var long g_screenWidth + * \brief Width of screen + * * The minimum width of the display, measured in fixed width characters. */ -extern long g_screenWidth; /* Width of screen */ +extern long g_screenWidth; /*! * \def MAX_LEN * \brief Default width of screen @@ -77,8 +88,9 @@ extern long g_screenWidth; /* Width of screen */ * Graphical Displays on a notebook for example can display much more, but on * some mobile devices this may be reduced to 30-40 characters. */ -#define MAX_LEN 79 /* Default width of screen */ -#define SCREEN_HEIGHT 23 /* Lines on screen, minus 1 to account for prompt */ +#define MAX_LEN 79 +/*! Lines on screen, minus 1 to account for prompt */ +#define SCREEN_HEIGHT 23 /*! * \var flag g_scrollMode * \brief controls whether output stops after a full page is printed. @@ -87,15 +99,17 @@ extern long g_screenWidth; /* Width of screen */ * The command SET SCROLL controls this value. If followed by CONTINUOUS, this * flag is reset to 0. */ -extern flag g_scrollMode; /* Flag for continuous or prompted scroll */ +extern flag g_scrollMode; /*! * \var flag g_quitPrint + * \brief Flag that user typed 'q' to last scrolling prompt * The value 1 indicates the user entered a 'q' at the last scrolling prompt. */ -extern flag g_quitPrint; /* Flag that user typed 'q' to last scrolling prompt */ +extern flag g_quitPrint; -/* printLongLine automatically puts a newline \n in the output line. */ +/*! printLongLine automatically puts a newline \n in the output line. */ void printLongLine(const char *line, const char *startNextLine, const char *breakMatch); + /*! * \brief requests a line of text from the __stream__. * @@ -124,8 +138,8 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea * * 2. The user repetitively hits ENTER (only) while prompted in top level * context. The prompt is simply replayed as often. Entering an isolated 'b' - * or 'B' is first directed to case 1, and only if it cannot be served there, - * the routine exits, returning the b or B to the caller. + * or 'B' is first directed to case 1, and only if it cannot be served there, + * the routine exits, returning the b or B to the caller. * * No timeout is applied when waiting for user input from the console. * @@ -139,9 +153,9 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea * * A bug message need not result in an execution stop. * \param[in] stream (not null) source to read the line from. _stdin_ is - * common for user input from the console. + * common for user input from the console. * \param[in] ask prompt text displayed on the screen before __stream__ is - * read. This prompt is suppressed by either a NULL value, or setting + * read. This prompt is suppressed by either a NULL value, or setting * \a g_commandFileSilentFlag to 1. This prompt must be not NULL (empty is * fine!) outside of a SUBMIT call, where user is expected to enter input. * \n @@ -180,6 +194,7 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea * memory accesses beyond allocated buffers. */ vstring cmdInput(FILE *stream, const char *ask); + /*! * gets a line from either the terminal or the command file stream depending on * g_commandFileNestingLevel > 0. It calls cmdInput(). @@ -192,26 +207,27 @@ vstring cmdInput(FILE *stream, const char *ask); * \warning the calling program must deallocate the returned string. */ vstring cmdInput1(const char *ask); + flag cmdInputIsY(const char *ask); enum severity {notice_,warning_,error_,fatal_}; void errorMessage(vstring line, long lineNum, long column, long tokenLength, vstring error, vstring fileName, long statementNum, flag warnFlag); -/* Opens files with error message; opens output files with +/*! Opens files with error message; opens output files with backup of previous version. Mode must be "r" or "w". */ FILE *fSafeOpen(const char *fileName, const char *mode, flag noVersioningFlag); -/* Renames a file with backup of previous version. If non-zero +/*! Renames a file with backup of previous version. If non-zero is returned, there was an error. */ int fSafeRename(const char *oldFileName, const char *newFileName); -/* Finds the name of the first file of the form filePrefix + +/*! Finds the name of the first file of the form filePrefix + nnn + ".tmp" that does not exist. THE CALLER MUST DEALLOCATE THE RETURNED STRING. */ vstring fGetTmpName(const char *filePrefix); -/* This function returns a character string containing the entire contents of +/*! This function returns a character string containing the entire contents of an ASCII file, or Unicode file with only ASCII characters. On some systems it is faster than reading the file line by line. THE CALLER MUST DEALLOCATE THE RETURNED STRING. If a NULL is returned, the file @@ -219,12 +235,12 @@ vstring fGetTmpName(const char *filePrefix); problem. If verbose is 0, error and warning messages are suppressed. */ vstring readFileToString(const char *fileName, char verbose, long *charCount); -/* Returns total elapsed time in seconds since starting session (for the +/*! Returns total elapsed time in seconds since starting session (for the lcc compiler) or the CPU time used (for the gcc compiler). The argument is assigned the time since the last call to this function. */ double getRunTime(double *timeSinceLastCall); -/* Call before exiting to free memory allocated by this module */ +/*! Call before exiting to free memory allocated by this module */ void freeInOu(void); #endif /* METAMATH_MMINOU_H_*/ diff --git a/src/mmpars.h b/src/mmpars.h index 0dc02b43..0d53953b 100644 --- a/src/mmpars.h +++ b/src/mmpars.h @@ -7,6 +7,8 @@ #ifndef METAMATH_MMPARS_H_ #define METAMATH_MMPARS_H_ +/*! \file */ + #include "mmvstr.h" #include "mmdata.h" @@ -25,49 +27,49 @@ void mathTokenError(long tokenNum /* 0 is 1st one */, nmbrString *tokenList, long stmtNum, vstring errMsg); vstring shortDumpRPNStack(void); -/* Label comparison for qsort */ +/*! Label comparison for qsort */ int labelSortCmp(const void *key1, const void *key2); -/* Label comparison for bsearch */ +/*! Label comparison for bsearch */ int labelSrchCmp(const void *key, const void *data); -/* Math token comparison for qsort */ +/*! Math token comparison for qsort */ int mathSortCmp(const void *key1, const void *key2); -/* Math token label comparison for bsearch */ +/*! Math token label comparison for bsearch */ int mathSrchCmp(const void *key, const void *data); -/* Hypothesis and local label comparison for qsort */ +/*! Hypothesis and local label comparison for qsort */ int hypAndLocSortCmp(const void *key1, const void *key2); -/* Hypothesis and local label comparison for bsearch */ +/*! Hypothesis and local label comparison for bsearch */ int hypAndLocSrchCmp(const void *key, const void *data); -/* This function returns the length of the white space starting at ptr. +/*! This function returns the length of the white space starting at ptr. Comments are considered white space. ptr should point to the first character of the white space. If ptr does not point to a white space character, 0 is returned. If ptr points to a null character, 0 is returned. */ long whiteSpaceLen(char *ptr); /* For .mm file splitting */ -/* Like whiteSpaceLen except comments are not whitespace */ +/*! Like whiteSpaceLen except comments are not whitespace */ long rawWhiteSpaceLen(char *ptr); -/* This function returns the length of the token (non-white-space) starting at +/*! This function returns the length of the token (non-white-space) starting at ptr. Comments are considered white space. ptr should point to the first character of the token. If ptr points to a white space character, 0 is returned. If ptr points to a null character, 0 is returned. If ptr points to a keyword, 0 is returned. A keyword ends a token. */ long tokenLen(char *ptr); -/* Unlike tokenLen(), keywords are not treated as special. In particular: +/*! Unlike tokenLen(), keywords are not treated as special. In particular: if ptr points to a keyword, 0 is NOT returned (instead, 2 is returned), and a keyword does NOT end a token (which is a relic of days before whitespace surrounding a token was part of the spec, but still serves a useful purpose in token() for friendlier error detection). */ long rawTokenLen(char *ptr); -/* This function returns the length of the proof token starting at +/*! This function returns the length of the proof token starting at ptr. Comments are considered white space. ptr should point to the first character of the token. If ptr points to a white space character, 0 is returned. If ptr points to a null character, 0 is returned. If ptr @@ -75,128 +77,130 @@ long rawTokenLen(char *ptr); ":" is considered a token. */ long proofTokenLen(char *ptr); -/* Counts the number of \n between start for length chars. +/*! Counts the number of \n between start for length chars. If length = -1, then use end-of-string 0 to stop. If length >= 0, then scan at most length chars, but stop if end-of-string 0 is found. */ long countLines(const char *start, long length); -/* Array with sort keys for all possible labels, including the ones for - hypotheses (which may not always be active) */ -/* This array is used to see if any label is used anywhere, and is used +/*! \brief Array with sort keys for all possible labels, including the ones for + hypotheses (which may not always be active) + + This array is used to see if any label is used anywhere, and is used to make sure there are no conflicts when local labels inside of compact proofs are generated. */ extern long *g_allLabelKeyBase; extern long g_numAllLabelKeys; -/* Working structure for parsing proofs */ -/* This structure should be deallocated by the ERASE command. */ -extern long g_wrkProofMaxSize; /* Maximum size so far - it may grow */ + +extern long g_wrkProofMaxSize; /*!< Maximum size so far - it may grow */ struct sortHypAndLoc { /* Used for sorting hypAndLocLabel field */ long labelTokenNum; void *labelName; }; +/*! \brief Working structure for parsing proofs + \note This structure should be deallocated by the ERASE command. */ struct wrkProof_struct { - long numTokens; /* Number of tokens in proof */ - long numSteps; /* Number of steps in proof */ - long numLocalLabels; /* Number of local labels */ - long numHypAndLoc; /* Number of active hypotheses and local labels */ - char *localLabelPoolPtr; /* Next free location in local label pool */ - long RPNStackPtr; /* Offset of end of RPNStack */ - long errorCount; /* Errors in proof - used to suppress too many error msgs */ - flag errorSeverity; /* 0 = OK, 1 = unknown step, 2 = error, 3 = severe error, + long numTokens; /*!< Number of tokens in proof */ + long numSteps; /*!< Number of steps in proof */ + long numLocalLabels; /*!< Number of local labels */ + long numHypAndLoc; /*!< Number of active hypotheses and local labels */ + char *localLabelPoolPtr; /*!< Next free location in local label pool */ + long RPNStackPtr; /*!< Offset of end of RPNStack */ + long errorCount; /*!< Errors in proof - used to suppress too many error msgs */ + flag errorSeverity; /*!< 0 = OK, 1 = unknown step, 2 = error, 3 = severe error, 4 = not a $p statement */ /* The following pointers will always be allocated with g_wrkProofMaxSize entries. If a function needs more than g_wrkProofMaxSize, it must reallocate all of these and increase g_wrkProofMaxSize. */ - nmbrString *tokenSrcPtrNmbr; /* Source parsed into tokens vs. token number + nmbrString *tokenSrcPtrNmbr; /*!< Source parsed into tokens vs. token number - token size */ - pntrString *tokenSrcPtrPntr; /* Source parsed into tokens vs. token number + pntrString *tokenSrcPtrPntr; /*!< Source parsed into tokens vs. token number - token src ptrs */ - nmbrString *stepSrcPtrNmbr; /* Pointer to label token in source file + nmbrString *stepSrcPtrNmbr; /*!< Pointer to label token in source file vs. step number - label size */ - pntrString *stepSrcPtrPntr; /* Pointer to label token in source file + pntrString *stepSrcPtrPntr; /*!< Pointer to label token in source file vs. step number - label src ptrs */ - flag *localLabelFlag; /* 1 means step has a local label declaration */ + flag *localLabelFlag; /*!< 1 means step has a local label declaration */ + /*! Sorted ptrs to hyp and local label names + token# */ struct sortHypAndLoc *hypAndLocLabel; - /* Sorted ptrs to hyp and local label names + token# */ - char *localLabelPool; /* String pool to hold local labels */ - nmbrString *proofString; /* The proof in RPN - statement # if > 0 + char *localLabelPool; /*!< String pool to hold local labels */ + nmbrString *proofString; /*!< The proof in RPN - statement # if > 0 or -(step # + 1000) of local label decl if < -1 */ - pntrString *mathStringPtrs; /* Ptr to math string vs. each step */ - /* (Allocated in verifyProof() as needed by nmbrLet()) */ - nmbrString *RPNStack; /* Stack for RPN parsing */ + /*! Ptr to math string vs. each step (Allocated in verifyProof() as needed by nmbrLet()) */ + pntrString *mathStringPtrs; + nmbrString *RPNStack; /*!< Stack for RPN parsing */ /* For compressed proof parsing */ - nmbrString *compressedPfLabelMap; /* Map from compressed label to actual */ - long compressedPfNumLabels; /* Number of compressed labels */ - + nmbrString *compressedPfLabelMap; /*!< Map from compressed label to actual */ + long compressedPfNumLabels; /*!< Number of compressed labels */ }; extern struct wrkProof_struct g_WrkProof; -/* Converts an ASCII string to a nmbrString of math symbols. statemNum +/*! Converts an ASCII string to a nmbrString of math symbols. statemNum provides the context for the parse (to get correct active symbols) */ nmbrString *parseMathTokens(vstring userText, long statemNum); vstring outputStatement(long stmt, /*flag cleanFlag,*/ flag reformatFlag); -/* Caller must deallocate return string */ +/*! Caller must deallocate return string */ vstring rewrapComment(const char *comment); -/* Lookup $a or $p label and return statement number. +/*! Lookup $a or $p label and return statement number. Return -1 if not found. */ long lookupLabel(const char *label); /* For file splitting */ -/* Get the next real $[...$] or virtual $( Begin $[... inclusion */ -void getNextInclusion(char *fileBuf, long startOffset, /* inputs */ - /* outputs: */ +/*! Get the next real $[...$] or virtual $( Begin $[... inclusion */ +void getNextInclusion(char *fileBuf, long startOffset, /*!< inputs */ + /*! outputs: */ long *cmdPos1, long *cmdPos2, long *endPos1, long *endPos2, - char *cmdType, /* 'B' = "$( Begin [$..." through "$( End [$...", - 'I' = "[$...", - 'S' = "$( Skip [$...", - 'E' = Start missing matched End - 'N' = no include found */ - vstring *fileName /* name of included file */ + char *cmdType, /*!< 'B' = "$( Begin [$..." through "$( End [$...", + 'I' = "[$...", + 'S' = "$( Skip [$...", + 'E' = Start missing matched End + 'N' = no include found */ + vstring *fileName /*!< name of included file */ ); -/* This function transfers the content of the statement[] array +/*! This function transfers the content of the statement[] array to a linear buffer in preparation for creating the output file. */ vstring writeSourceToBuffer(void); -/* This function creates split files containing $[ $] inclusions, from - an unsplit source with $( Begin $[... etc. inclusions */ -/* Note that *fileBuf is assigned to the empty string upon return, to +/*! This function creates split files containing $[ $] inclusions, from + an unsplit source with $( Begin $[... etc. inclusions + \note that *fileBuf is assigned to the empty string upon return, to conserve memory */ void writeSplitSource(vstring *fileBuf, const char *fileName, flag noVersioningFlag, flag noDeleteFlag); -/* When "write source" does not have the "/split" qualifier, by default +/*! When "write source" does not have the "/split" qualifier, by default (i.e. without "/no_delete") the included modules are "deleted" (renamed to ~1) since their content will be in the main output file. */ void deleteSplits(vstring *fileBuf, flag noVersioningFlag); -/* Get file name and line number given a pointer into the read buffer */ -/* The user must deallocate the returned string (file name) */ -/* The globals includeCall structure and includeCalls are used */ +/*! \brief Get file name and line number given a pointer into the read buffer + * \note The user must deallocate the returned string (file name) + * \note The globals includeCall structure and includeCalls are used + */ vstring getFileAndLineNum(const char *buffPtr/*start of read buffer*/, const char *currentPtr/*place at which to get file name and line no*/, long *lineNum/*return argument*/); -/* statement[stmtNum].fileName and .lineNum are initialized to "" and 0. +/*! statement[stmtNum].fileName and .lineNum are initialized to "" and 0. To save CPU time, they aren't normally assigned until needed, but once assigned they can be reused without looking them up again. This function will assign them if they haven't been assigned yet. It just returns if - they have already been assigned. */ -/* The globals statement[] and sourcePtr are used */ + they have already been assigned. + \note The globals statement[] and sourcePtr are used */ void assignStmtFileAndLineNum(long stmtNum); -/* Initial read of source file */ +/*! Initial read of source file */ vstring readSourceAndIncludes(const char *inputFn, long *size); -/* Recursively expand the source of an included file */ +/*! Recursively expand the source of an included file */ vstring readInclude(const char *fileBuf, long fileBufOffset, /*vstring inclFileName,*/ const char *sourceFileName, long *size, long parentLineNum, flag *errorFlag); diff --git a/src/mmpfas.h b/src/mmpfas.h index 74a26b0d..59774398 100644 --- a/src/mmpfas.h +++ b/src/mmpfas.h @@ -7,189 +7,194 @@ #ifndef METAMATH_MMPFAS_H_ #define METAMATH_MMPFAS_H_ +/*! \file */ + #include "mmvstr.h" #include "mmdata.h" -extern long g_proveStatement; /* The statement to be proved */ -extern flag g_proofChangedFlag; /* Flag to push 'undo' stack */ +extern long g_proveStatement; /*!< The statement to be proved */ +extern flag g_proofChangedFlag; /*!< Flag to push 'undo' stack */ -extern long g_userMaxProveFloat; /* Upper limit for proveFloating */ +extern long g_userMaxProveFloat; /*!< Upper limit for proveFloating */ -extern long g_dummyVars; /* The number of dummy variables currently declared */ -extern long g_pipDummyVars; /* Number of dummy vars used by proof in progress */ +extern long g_dummyVars; /*!< The number of dummy variables currently declared */ +extern long g_pipDummyVars; /*!< Number of dummy vars used by proof in progress */ -/* Structure for holding a proof in progress. */ -/* This structure should be deallocated after use. */ +/*!< Structure for holding a proof in progress. + \note This structure should be deallocated after use. */ struct pip_struct { - nmbrString *proof; /* The proof itself */ - pntrString *target; /* Left hand side of = in display */ - pntrString *source; /* Right hand side of = in display */ - pntrString *user; /* User-specified math string assignments to step */ + nmbrString *proof; /*!< The proof itself */ + pntrString *target; /*!< Left hand side of = in display */ + pntrString *source; /*!< Right hand side of = in display */ + pntrString *user; /*!< User-specified math string assignments to step */ }; extern struct pip_struct g_ProofInProgress; -/* Interactively select statement assignments that match */ -/* maxEssential is the maximum number of essential hypotheses that a - statement may have in order to be included in the matched list. */ +/*! Interactively select statement assignments that match + \param maxEssential the maximum number of essential hypotheses that a + statement may have in order to be included in the matched list. */ void interactiveMatch(long step, long maxEssential); -/* Assign a statement to an unknown proof step */ +/*! Assign a statement to an unknown proof step */ void assignStatement(long statemNum, long step); -/* Find proof of formula by using the replaceStatement() algorithm i.e. +/*! Find proof of formula by using the replaceStatement() algorithm i.e. see if any statement matches current step AND each of its hypotheses matches a proof in progress hypothesis or some step already in the proof. If a proof is found, it is returned, otherwise an empty (length 0) proof is - returned. */ -/* The caller must deallocate the returned nmbrString. */ + returned. + \note The caller must deallocate the returned nmbrString. */ nmbrString *proveByReplacement(long prfStmt, - long prfStep, /* 0 means step 1 */ - flag noDistinct, /* 1 means don't try statements with $d's */ - flag dummyVarFlag, /* 0 means no dummy vars are in prfStmt */ - flag searchMethod, /* 1 means to try proveFloating on $e's also */ + long prfStep, /*!< 0 means step 1 */ + flag noDistinct, /*!< 1 means don't try statements with $d's */ + flag dummyVarFlag, /*!< 0 means no dummy vars are in prfStmt */ + flag searchMethod, /*!< 1 means to try proveFloating on $e's also */ long improveDepth, - flag overrideFlag, /* 1 means to override usage locks */ - flag mathboxFlag /* 1 means allow mathboxes */ + flag overrideFlag, /*!< 1 means to override usage locks */ + flag mathboxFlag /*!< 1 means allow mathboxes */ ); nmbrString *replaceStatement(long replStatemNum, long prfStep, long provStmtNum, - flag subProofFlag, /* If 1, then scan only subproof at prfStep to look for + flag subProofFlag, /*!< If 1, then scan only subproof at prfStep to look for matches, instead of whole proof, for faster speed (used by MINIMIZE_WITH) */ - flag noDistinct, /* 1 means don't try statements with $d's */ - flag searchMethod, /* 1 means to try proveFloating on $e's also */ + flag noDistinct, /*!< 1 means don't try statements with $d's */ + flag searchMethod, /*!< 1 means to try proveFloating on $e's also */ long improveDepth, - flag overrideFlag, /* 1 means to override usage locks */ - flag mathboxFlag /* 1 means allow mathboxes */ + flag overrideFlag, /*!< 1 means to override usage locks */ + flag mathboxFlag /*!< 1 means allow mathboxes */ ); -/* This function identifies all steps in the proof in progress that (1) are +/*! This function identifies all steps in the proof in progress that (1) are independent of step refStep, (2) have no dummy variables, (3) are not $f's or $e's, and (4) have subproofs that are complete (no unassigned steps). A "Y" is returned for each such step, and "N" is returned for all other steps. The "Y" steps can be used for scanning for useful subproofs outside of the subProof of refStep. - Note: The caller must deallocate the returned vstring. */ + \note The caller must deallocate the returned vstring. */ vstring getIndepKnownSteps(long proofStmt, long refStep); -/* This function classifies each proof step in g_ProofInProgress.proof +/*! This function classifies each proof step in g_ProofInProgress.proof as known or unknown ('K' or 'U' in the returned string) depending on whether the step has a completely known subproof. - Note: The caller must deallocate the returned vstring. */ + \note The caller must deallocate the returned vstring. */ vstring getKnownSubProofs(void); -/* Add a subproof in place of an unknown step to g_ProofInProgress. The +/*! Add a subproof in place of an unknown step to g_ProofInProgress. The .target, .source, and .user fields are initialized to empty (except .target of the deleted unknown step is retained). */ void addSubProof(const nmbrString *subProof, long step); -/* This function eliminates any occurrences of statement sourceStmtNum in the +/*! This function eliminates any occurrences of statement sourceStmtNum in the targetProof by substituting it with the proof of sourceStmtNum. An empty - nmbrString is returned if there was an error. */ -/* Normally, targetProof is the global g_ProofInProgress.proof. However, + nmbrString is returned if there was an error. + + Normally, targetProof is the global g_ProofInProgress.proof. However, we make it an argument in case in the future we'd like to do this - outside of the proof assistant. */ -/* Note: The caller must deallocate the returned nmbrString. */ + outside of the proof assistant. + \note The caller must deallocate the returned nmbrString. */ nmbrString *expandProof(const nmbrString *targetProof, long sourceStmtNum); -/* Delete a subproof starting (in reverse from) step. The step is replaced +/*! Delete a subproof starting (in reverse from) step. The step is replaced with an unknown step, and its .target field is retained. */ void deleteSubProof(long step); -/* Check to see if a statement will match the g_ProofInProgress.target (or .user) +/*! Check to see if a statement will match the g_ProofInProgress.target (or .user) of an unknown step. Returns 1 if match, 0 if not, 2 if unification timed out. */ char checkStmtMatch(long statemNum, long step); -/* Check to see if a (user-specified) math string will match the +/*! Check to see if a (user-specified) math string will match the g_ProofInProgress.target (or .user) of an step. Returns 1 if match, 0 if not, 2 if unification timed out. */ char checkMStringMatch(const nmbrString *mString, long step); -/* Find proof of formula or simple theorem (no new vars in $e's) */ -/* maxEDepth is the maximum depth at which statements with $e hypotheses are - considered. A value of 0 means none are considered. */ +/*! Find proof of formula or simple theorem (no new vars in $e's) + + \param maxEDepth the maximum depth at which statements with $e hypotheses are + considered. A value of 0 means none are considered. */ nmbrString *proveFloating(const nmbrString *mString, long statemNum, long maxEDepth, long step, flag noDistinct, - flag overrideFlag, /* 0 means respect usage locks + flag overrideFlag, /*!< 0 means respect usage locks 1 means to override usage locks 2 means override silently */ - flag mathboxFlag /* 1 means allow mathboxes */ + flag mathboxFlag /*!< 1 means allow mathboxes */ ); -/* This function does quick check for some common conditions that prevent +/*! This function does quick check for some common conditions that prevent a trial statement (scheme) from being unified with a given instance. Return value 0 means it can't be unified, 1 means it might be unifiable. */ char quickMatchFilter(long trialStmt, const nmbrString *mString, - long dummyVarFlag /* 0 if no dummy vars in mString */); + long dummyVarFlag /*!< 0 if no dummy vars in mString */); -/* Shorten proof by using specified statement. */ +/*! Shorten proof by using specified statement. */ void minimizeProof(long repStatemNum, long prvStatemNum, flag allowGrowthFlag); -/* Initialize g_ProofInProgress.source of the step, and .target of all +/*! Initialize g_ProofInProgress.source of the step, and .target of all hypotheses, to schemes using new dummy variables. */ void initStep(long step); -/* Look for completely known subproofs in g_ProofInProgress.proof and +/*! Look for completely known subproofs in g_ProofInProgress.proof and assign g_ProofInProgress.target and .source. Calls assignKnownSteps(). */ void assignKnownSubProofs(void); -/* This function assigns math strings to all steps (g_ProofInProgress.target and +/*! This function assigns math strings to all steps (g_ProofInProgress.target and .source fields) in a subproof with all known steps. */ void assignKnownSteps(long startStep, long sbProofLen); -/* Interactive unify a step. Calls interactiveUnify(). */ -/* If messageFlag is 1, a message will be issued if the +/*! \brief Interactive unify a step. Calls interactiveUnify(). + If messageFlag is 1, a message will be issued if the step is already unified. If messageFlag is 0, show the step # being unified. If messageFlag is 2, don't print step #, and do nothing if step is already unified. */ void interactiveUnifyStep(long step, char messageFlag); -/* Interactively select one of several possible unifications */ -/* Returns: 0 = no unification possible - 1 = unification was selected; held in stateVector - 2 = unification timed out - 3 = no unification was selected */ +/*! Interactively select one of several possible unifications + \returns * 0 = no unification possible + * 1 = unification was selected; held in stateVector + * 2 = unification timed out + * 3 = no unification was selected */ char interactiveUnify(const nmbrString *schemeA, const nmbrString *schemeB, pntrString **stateVector); -/* Automatically unify steps with unique unification */ +/*! Automatically unify steps with unique unification */ void autoUnify(flag congrats); -/* Make stateVector substitutions in all steps. The stateVector must +/*! Make stateVector substitutions in all steps. The stateVector must contain the result of a valid unification. */ void makeSubstAll(pntrString *stateVector); -/* Replace a dummy variable with a user-specified math string */ +/*! Replace a dummy variable with a user-specified math string */ void replaceDummyVar(long dummyVar, const nmbrString *mString); -/* Get subproof length of a proof, starting at endStep and going backwards */ +/*! Get subproof length of a proof, starting at endStep and going backwards */ long subproofLen(const nmbrString *proof, long endStep); -/* If testStep has no dummy variables, return 0; +/*! If testStep has no dummy variables, return 0; if testStep has isolated dummy variables (that don't affect rest of proof), return 1; if testStep has dummy variables used elsewhere in proof, return 2 */ -char checkDummyVarIsolation(long testStep); /* 0=1st step, 1=2nd, etc. */ +char checkDummyVarIsolation(long testStep /*!< 0=1st step, 1=2nd, etc. */); -/* Given a starting step, find its parent (the step it is a hypothesis of) */ -/* If the starting step is the last proof step, just return it */ -long getParentStep(long startStep); /* 0=1st step, 1=2nd, etc. */ +/*! Given a starting step, find its parent (the step it is a hypothesis of) -/* Adds a dummy variable to end of mathToken array */ -/* (Note: it now grows forever, but purging it might worsen fragmentation) */ + If the starting step is the last proof step, just return it */ +long getParentStep(long startStep /*!< 0=1st step, 1=2nd, etc. */); + +/*! Adds a dummy variable to end of mathToken array + \note it now grows forever, but purging it might worsen fragmentation */ void declareDummyVars(long numNewVars); -/* Copies the Proof Assistant proof state */ +/*! Copies the Proof Assistant proof state */ void copyProofStruct(struct pip_struct *outProofStruct, struct pip_struct inProofStruct); -/* Initializes the Proof Assistant proof state */ +/*! Initializes the Proof Assistant proof state */ void initProofStruct(struct pip_struct *proofStruct, const nmbrString *proof, long proveStatement); -/* Clears the Proof Assistant proof state */ +/*! Clears the Proof Assistant proof state */ void deallocProofStruct(struct pip_struct *proofStruct); /* Actions for processUndoStack() */ @@ -200,10 +205,11 @@ void deallocProofStruct(struct pip_struct *proofStruct); #define PUS_NEW_SIZE 5 #define PUS_GET_SIZE 6 #define PUS_GET_STATUS 7 -/* Handle the PUSH, UNDO, and REDO commands */ + +/*! Handle the PUSH, UNDO, and REDO commands */ long processUndoStack(struct pip_struct *proofStruct, char action, - vstring info, /* Info to print upon UNDO or REDO */ - long newStackSize); /* Used only by NEW_SIZE */ + vstring info, /*!< Info to print upon UNDO or REDO */ + long newStackSize /*!< Used only by NEW_SIZE */); #endif /* METAMATH_MMPFAS_H_ */ diff --git a/src/mmunif.h b/src/mmunif.h index 3fa28b6f..06facebd 100644 --- a/src/mmunif.h +++ b/src/mmunif.h @@ -7,15 +7,17 @@ #ifndef METAMATH_MMUNIF_H_ #define METAMATH_MMUNIF_H_ +/*! \file */ + #include "mmdata.h" -extern long g_minSubstLen; /* User-settable value - 0 or 1 */ +extern long g_minSubstLen; /*!< User-settable value - 0 or 1 */ extern long g_userMaxUnifTrials; - /* User-defined upper limit (# backtracks) for unification trials */ + /*!< User-defined upper limit (# backtracks) for unification trials */ extern long g_unifTrialCount; - /* 0 means don't time out; 1 means start counting trials */ -extern long g_unifTimeouts; /* Number of timeouts so far for this command */ -extern flag g_hentyFilter; /* Turns Henty filter on or off */ + /*!< 0 means don't time out; 1 means start counting trials */ +extern long g_unifTimeouts; /*!< Number of timeouts so far for this command */ +extern flag g_hentyFilter; /*!< Turns Henty filter on or off */ /* Global so eraseSource() (mmcmds.c) can clear them */ extern flag g_bracketMatchInit; @@ -28,13 +30,7 @@ nmbrString *makeSubstUnif(flag *newVarFlag, const nmbrString *trialScheme, pntrString *stateVector); -char unify( - const nmbrString *schemeA, - const nmbrString *schemeB, - /* nmbrString **unifiedScheme, */ /* stateVector[8] holds this */ - pntrString **stateVector, - long reEntryFlag); -/* This function unifies two math token strings, schemeA and +/*! This function unifies two math token strings, schemeA and schemeB. The result is contained in unifiedScheme. 0 is returned if no assignment is possible. If reEntryFlag is 1, the next possible set of assignments, if any, @@ -56,9 +52,15 @@ char unify( remain "unknown", and others may have assignments which include "unknown" variables. */ +char unify( + const nmbrString *schemeA, + const nmbrString *schemeB, + /* nmbrString **unifiedScheme, */ /* stateVector[8] holds this */ + pntrString **stateVector, + long reEntryFlag); -/* oneDirUnif() is like unify(), except that when reEntryFlag is 1, +/*! oneDirUnif() is like unify(), except that when reEntryFlag is 1, a new unification is returned ONLY if the assignments to the variables in schemeA have changed. This is used to speed up the program. */ @@ -69,7 +71,7 @@ flag oneDirUnif( long reEntryFlag); -/* uniqueUnif() is like unify(), but there is no reEntryFlag, and 3 possible +/*! uniqueUnif() is like unify(), but there is no reEntryFlag, and 3 possible values are returned: 0: no unification was possible. 1: exactly one unification was possible, and stateVector is valid. @@ -80,7 +82,7 @@ char uniqueUnif( const nmbrString *schemeB, pntrString **stateVector); -/* unifyH() is like unify(), except that when reEntryFlag is 1, +/*! unifyH() is like unify(), except that when reEntryFlag is 1, a new unification is returned ONLY if the normalized unification does not previously exist in the "Henty filter". This reduces ambiguous unifications. The values returned are the same as @@ -92,10 +94,10 @@ char unifyH( pntrString **stateVector, long reEntryFlag); -/* Cleans out a stateVector if not empty */ +/*! Cleans out a stateVector if not empty */ void purgeStateVector(pntrString **stateVector); -/* Prints the substitutions determined by unify for debugging purposes */ +/*! Prints the substitutions determined by unify for debugging purposes */ void printSubst(pntrString *stateVector); #endif /* METAMATH_MMUNIF_H_ */ diff --git a/src/mmveri.h b/src/mmveri.h index 106dbc1c..7aebfc43 100644 --- a/src/mmveri.h +++ b/src/mmveri.h @@ -7,27 +7,30 @@ #ifndef METAMATH_MMVERI_H_ #define METAMATH_MMVERI_H_ +/*! \file */ + #include "mmdata.h" char verifyProof(long statemNum); -/* assignVar() finds an assignment to substScheme variables that match +/*! assignVar() finds an assignment to substScheme variables that match the assumptions specified in the reason string */ nmbrString *assignVar(nmbrString *bigSubstSchemeAss, nmbrString *bigSubstInstAss, long substScheme, /* For error messages: */ long statementNum, long step, flag unkHypFlag); -/* Deallocate the math symbol strings assigned in g_WrkProof structure during +/*! Deallocate the math symbol strings assigned in g_WrkProof structure during proof verification. This should be called after verifyProof() and after the - math symbol strings have been used for proof printouts, etc. */ -/* Note that this does NOT free the other allocations in g_WrkProof. The + math symbol strings have been used for proof printouts, etc. + \note this does NOT free the other allocations in g_WrkProof. The ERASE command will do this. */ void cleanWrkProof(void); -/* Structure for getting info about a step for SHOW PROOF/STEP command */ -/* If getStep.stepNum is nonzero, we should get info about that step. */ -/* This structure should be deallocated after use. */ +/*! \brief Structure for getting info about a step for SHOW PROOF/STEP command + + If getStep.stepNum is nonzero, we should get info about that step. + \note This structure should be deallocated after use. */ struct getStep_struct { long stepNum; /* Step # to get info about */ long sourceStmt; /* Right side of = in proof display */ diff --git a/src/mmvstr.h b/src/mmvstr.h index 6957856c..d85eaec0 100644 --- a/src/mmvstr.h +++ b/src/mmvstr.h @@ -4,135 +4,133 @@ /*****************************************************************************/ /*34567890123456 (79-character line to adjust editor window) 2345678901234567*/ -/*! -\file mmvstr.h - VMS-BASIC variable length string library routines header -This is an emulation of the string functions available in VMS BASIC. -[VAX Basic](http://bitsavers.org/pdf/dec/vax/lang/basic/AA-HY16B-TE_VAX_BASIC_Reference_Manual_Feb90.pdf) -*/ - -/****************************************************************************** - -Variable-length string handler ------------------------------- - - This collection of string-handling functions emulate most of the -string functions of VMS BASIC. The objects manipulated by these -functions are strings of a special type called 'vstring' which have no -pre-defined upper length limit but are dynamically allocated and -deallocated as needed. To use the vstring functions within a program, -all vstrings must be initially set to the null string when declared or -before first used, for example: - - vstring_def(string1); - vstring stringArray[] = {"", "", ""}; - - vstring bigArray[100][10]; /- Must be initialized before using -/ - int i, j; - for (i = 0; i < 100; i++) - for (j = 0; j < 10; j++) - bigArray[i][j] = ""; /- Initialize -/ - - - After initialization, vstrings should be assigned with the 'let(&' -function only; for example the statements - - let(&string1, "abc"); - let(&string1, string2); - let(&string1, left(string2, 3)); - -all assign the second argument to 'string1'. The 'let(&' function must -_not_ be used to initialize a vstring the first time. - - Any local vstrings in a function must be deallocated before returning -from the function, otherwise there will be memory leakage and eventual -memory overflow. To deallocate, assign the vstring to "" with 'free_vstring': - - void abc(void) { - vstring_def(xyz); - ... - free_vstring(xyz); - } - - The 'cat' function emulates the '+' concatenation operator in BASIC. -It has a variable number of arguments, and the last argument should always -be NULL. For example, - - let(&string1,cat("abc","def",NULL)); - -assigns "abcdef" to 'string1'. Warning: 0 will work instead of NULL on the -VAX but not on the Macintosh, so always use NULL. - - All other functions are generally used exactly like their BASIC -equivalents. For example, the BASIC statement - - let string1$=left$("def",len(right$("xxx",2)))+"ghi"+string2$ - -is emulated in c as - - let(&string1,cat(left("def",len(right("xxx",2))),"ghi",string2,NULL)); - -Note that ANSI c does not allow "$" as part of an identifier -name, so the names in c have had the "$" suffix removed. - - The string arguments of the vstring functions may be either standard c -strings or vstrings (except that the first argument of the 'let(&' function -must be a vstring). The standard c string functions may use vstrings or -vstring functions as their string arguments, as long as the vstring variable -itself (which is a char * pointer) is not modified and no attempt is made to -increase the length of a vstring. Caution must be exercised when -assigning standard c string pointers to vstrings or the results of -vstring functions, as the memory space may be deallocated when the -'let(&' function is next executed. For example, - - char *stdstr; /- A standard c string pointer -/ - ... - stdstr=left("abc",2); - -will assign "ab" to 'stdstr', but this assignment will be lost when the -next 'let(&' function is executed. To be safe, use 'strcpy': - - char stdstr1[80]; /- A fixed length standard c string -/ - ... - strcpy(stdstr1,left("abc",2)); - -Here, of course, the user must ensure that the string copied to 'stdstr1' -does not exceed 79 characters in length. - - The vstring functions allocate temporary memory whenever they are called. -This temporary memory is deallocated whenever a 'let(&' assignment is -made. The user should be aware of this when using vstring functions -outside of 'let(&' assignments; for example - - for (i=0; i<10000; i++) - print2("%s\n",left(string1,70)); - -will allocate another 70 bytes or so of memory each pass through the loop. -If necessary, 'freeTempAlloc' can be used periodically to clear -this temporary memory: - - for (i=0; i<10000; i++) { - print2("%s\n",left(string1,70)); - freeTempAlloc(); - } - -It should be noted that the 'linput' function assigns its target string -with 'let(&' and thus has the same effect as 'let(&'. - -******************************************************************************/ - - #ifndef METAMATH_MMVSTR_H_ #define METAMATH_MMVSTR_H_ #include -/* A vstring is like a C string, but it contains a control block allowing -for memory allocation. New vstrings should always be constructed from the -`vstring_def` macro. */ +/**************************************************************************//** + * \file mmvstr.h + * \brief VMS-BASIC variable length string library routines header + * + * Variable-length string handler + * ------------------------------ + * + * This collection of string-handling functions emulate most of the + * string functions of [VMS BASIC][1]. The objects manipulated by these + * functions are strings of a special type called \ref vstring which have no + * pre-defined upper length limit but are dynamically allocated and + * deallocated as needed. To use the vstring functions within a program, + * all vstrings must be initially set to the null string when declared or + * before first used, for example: + * + * vstring_def(string1); + * vstring stringArray[] = {"", "", ""}; + * + * vstring bigArray[100][10]; /- Must be initialized before using -/ + * int i, j; + * for (i = 0; i < 100; i++) + * for (j = 0; j < 10; j++) + * bigArray[i][j] = ""; /- Initialize -/ + * + * + * After initialization, vstrings should be assigned with the `let(&` + * function only; for example the statements + * + * let(&string1, "abc"); + * let(&string1, string2); + * let(&string1, left(string2, 3)); + * + * all assign the second argument to `string1`. The \ref let function must + * _not_ be used to initialize a vstring the first time. + * + * Any local vstrings in a function must be deallocated before returning + * from the function, otherwise there will be memory leakage and eventual + * memory overflow. To deallocate, assign the vstring to "" with \ref free_vstring: + * + * void abc(void) { + * vstring_def(xyz); + * ... + * free_vstring(xyz); + * } + * + * The 'cat' function emulates the '+' concatenation operator in BASIC. + * It has a variable number of arguments, and the last argument should always + * be NULL. For example, + * + * let(&string1,cat("abc","def",NULL)); + * + * assigns "abcdef" to `string1`. Warning: 0 will work instead of NULL on the + * VAX but not on the Macintosh, so always use NULL. + * + * All other functions are generally used exactly like their BASIC + * equivalents. For example, the BASIC statement + * + * let string1$=left$("def",len(right$("xxx",2)))+"ghi"+string2$ + * + * is emulated in C as + * + * let(&string1,cat(left("def",len(right("xxx",2))),"ghi",string2,NULL)); + * + * Note that ANSI C does not allow "$" as part of an identifier + * name, so the names in C have had the "$" suffix removed. + * + * The string arguments of the vstring functions may be either standard C + * strings or vstrings (except that the first argument of the `let(&` function + * must be a vstring). The standard C string functions may use vstrings or + * vstring functions as their string arguments, as long as the vstring variable + * itself (which is a char * pointer) is not modified and no attempt is made to + * increase the length of a vstring. Caution must be exercised when + * assigning standard C string pointers to vstrings or the results of + * vstring functions, as the memory space may be deallocated when the + * `let(&` function is next executed. For example, + * + * char *stdstr; /- A standard c string pointer -/ + * ... + * stdstr=left("abc",2); + * + * will assign "ab" to 'stdstr', but this assignment will be lost when the + * next 'let(&' function is executed. To be safe, use 'strcpy': + * + * char stdstr1[80]; /- A fixed length standard c string -/ + * ... + * strcpy(stdstr1,left("abc",2)); + * + * Here, of course, the user must ensure that the string copied to `stdstr1` + * does not exceed 79 characters in length. + * + * The vstring functions allocate temporary memory whenever they are called. + * This temporary memory is deallocated whenever a `let(&` assignment is + * made. The user should be aware of this when using vstring functions + * outside of `let(&` assignments; for example + * + * for (i=0; i<10000; i++) + * print2("%s\n",left(string1,70)); + * + * will allocate another 70 bytes or so of memory each pass through the loop. + * If necessary, \ref freeTempAlloc can be used periodically to clear + * this temporary memory: + * + * for (i=0; i<10000; i++) { + * print2("%s\n",left(string1,70)); + * freeTempAlloc(); + * } + * + * It should be noted that the \ref linput function assigns its target string + * with `let(&` and thus has the same effect as `let(&`. + * + * [1]: http://bitsavers.org/pdf/dec/vax/lang/basic/AA-HY16B-TE_VAX_BASIC_Reference_Manual_Feb90.pdf + * + *****************************************************************************/ + /*! * \typedef vstring * \brief contains NUL terminated, character oriented data * + * A vstring is like a C string, but it contains a control block allowing + * for memory allocation. New vstrings should always be constructed from the + * `vstring_def` macro. + * * - A vstring is never NULL; * - If the text is empty, i.e. the pointer points to the terminating 0x00 * character, then its contents is not allocated memory and not mutable @@ -152,48 +150,9 @@ for memory allocation. New vstrings should always be constructed from the */ typedef char* vstring; -/* A vstring is allocated in temporary storage. These strings will be deallocated - after the next call to `let`. - - A `temp_vstring` should never be used as the first argument of a `let`. - This code is INCORRECT: - - temp_vstring foo = left("foobar", 3); - let(&foo, "bar"); // this will cause a double free - - It is okay (and quite common) to use a temp_vstring as the second argument, - however. It is best not to hold on to the value, though, because the `let` - will free it. This code is INCORRECT: - - vstring_def(x); - temp_vstring foobar = cat("foo", "bar"); - let(&x, foobar); // frees foobar - let(&x, foobar); // dangling reference - - There is a converse problem when `temp_vstring`s are used without `let`: - - for (int i = 0; i < 100000; i++) { - vstring_def(x); - if (strlen(space(i)) == 99999) break; - } - - We don't need to deallocate the string returned by `space()` directly, - because it returns a `temp_vstring`, but because there is no `let` in - this function, we end up allocating a bunch of temporaries and - effectively get a memory leak. (There is space for about 100 - temporaries so this loop will cause a crash.) To solve this problem, - we can either use a dummy `let()` statement in the loop, or call - `freeTempAlloc` directly: - - for (int i = 0; i < 100000; i++) { - vstring_def(x); - if (strlen(space(i)) == 99999) break; - freeTempAlloc(); - } - -*/ /*! - * \typedef temp_vstring + * \brief A vstring that is allocated in temporary storage. + * These strings will be deallocated after the next call to `let`. * * This alias for \a vstring is used to mark an entry in the \a tempAllocStack. * Entries in this stack are subject to automatic deallocation by \a let or @@ -203,7 +162,44 @@ typedef char* vstring; * If an empty string is generated as a temporary in the course of a * construction of a final \a vstring, it is allocated on the heap as usual. * - * If returned by a function, it is already pushed on the \a tempAllocStack. + * If returned by a function, it is already pushed on the \ref tempAllocStack. + * + * A `temp_vstring` should never be used as the first argument of a `let`. + * This code is INCORRECT: + * + * temp_vstring foo = left("foobar", 3); + * let(&foo, "bar"); // this will cause a double free + * + * It is okay (and quite common) to use a temp_vstring as the second argument, + * however. It is best not to hold on to the value, though, because the `let` + * will free it. This code is INCORRECT: + * + * vstring_def(x); + * temp_vstring foobar = cat("foo", "bar"); + * let(&x, foobar); // frees foobar + * let(&x, foobar); // dangling reference + * + * There is a converse problem when `temp_vstring`s are used without `let`: + * + * for (int i = 0; i < 100000; i++) { + * vstring_def(x); + * if (strlen(space(i)) == 99999) break; + * } + * + * We don't need to deallocate the string returned by `space()` directly, + * because it returns a `temp_vstring`, but because there is no `let` in + * this function, we end up allocating a bunch of temporaries and + * effectively get a memory leak. (There is space for about 100 + * temporaries so this loop will cause a crash.) To solve this problem, + * we can either use a dummy `let()` statement in the loop, or call + * `freeTempAlloc` directly: + * + * for (int i = 0; i < 100000; i++) { + * vstring_def(x); + * if (strlen(space(i)) == 99999) break; + * freeTempAlloc(); + * } + * */ typedef vstring temp_vstring; @@ -222,6 +218,7 @@ typedef vstring temp_vstring; * conformance with the semantics of a \a vstring. */ #define vstring_def(x) vstring x = "" + /*! * \def free_vstring * \brief deallocates a \a vstring variable and sets it to the empty string. @@ -234,7 +231,7 @@ typedef vstring temp_vstring; * * \param[in,out] x (not null) an initialized \a vstring variable. According to the * semantics of a \a vstring, __x__ is not deallocated, if it points to an - * empty string. + * empty string. * \pre * __x__ was declared and initialized before. * \post @@ -243,9 +240,6 @@ typedef vstring temp_vstring; */ #define free_vstring(x) let(&x, "") -/* Free space allocated for temporaries. This is normally called automatically - by let(), but it can also be called directly to avoid buildup of temporary - strings. */ /*! * \fn freeTempAlloc * \brief Free space allocated for temporary vstring instances. @@ -269,8 +263,6 @@ typedef vstring temp_vstring; */ void freeTempAlloc(void); -/* `source` must not point into `target` (but this is unlikely to arise if - `source` is calculated using `temp_vstring` operations from `target`). */ /*! * \fn let(vstring *target, const char *source) * \brief emulation of BASIC string assignment @@ -299,6 +291,8 @@ void freeTempAlloc(void); * this value, though. * \param[in] source (not null) NUL terminated string to be copied from. * + * \warning `source` must not point into `target` (but this is unlikely to arise if + * `source` is calculated using `temp_vstring` operations from `target`). * \pre * - \a g_startTempAllocStack contains the starting index of entries in * \a tempAllocStack, that is going to be deallocated. @@ -318,14 +312,14 @@ void freeTempAlloc(void); */ void let(vstring *target, const char *source); -/* Emulation of BASIC string concatenation - last argument MUST be NULL */ -/* vstring cat(vstring string1, ..., stringN, NULL); */ -/* e.g. 'let(&abc, cat("Hello", " ", left("worldx", 5), "!", NULL);' */ -/* Also the first string must not be `NULL`, i.e. `cat(NULL)` alone is invalid. */ /*! * \fn temp_vstring cat(const char * string1, ...) * \brief concatenates several NUL terminated strings to a single string. * + * \note last argument MUST be NULL, e.g. + * `let(&abc, cat("Hello", " ", left("worldx", 5), "!", NULL);` + * Also the first string must not be `NULL`, i.e. `cat(NULL)` alone is invalid. + * * Up to MAX_CAT_ARGS - 1 (49) NUL terminated strings submitted as parameters * are concatenated to form a single NUL terminated string. The parameters * terminate with a NULL pointer, a single NULL pointer is not allowed, though. @@ -341,21 +335,23 @@ void let(vstring *target, const char *source); */ temp_vstring cat(const char * string1, ...); -/* Emulation of BASIC linput (line input) statement; returns NULL if EOF */ -/* Note that linput assigns target string with let(&target,...) */ - /* - BASIC: linput "what";a$ - c: linput(NULL,"what?",&a); - - BASIC: linput #1,a$ (error trap on EOF) - c: if (!linput(file1,NULL,&a)) break; (break on EOF) - - */ -/* returns whether a (possibly empty) line was successfully read */ +/*! + * Emulation of BASIC linput (line input) statement; returns NULL if EOF + * \note linput assigns target string with `let(&target,...)` + * + * BASIC: linput "what";a$ + * c: linput(NULL,"what?",&a); + * + * BASIC: linput #1,a$ (error trap on EOF) + * c: if (!linput(file1,NULL,&a)) break; (break on EOF) + * + * \returns whether a (possibly empty) line was successfully read + */ int linput(FILE *stream, const char *ask, vstring *target); /* Emulation of BASIC string functions */ /* Indices are 1-based */ + /*! * \fn temp_vstring seg(const char *sin, long p1, long p2) * Extracts a substring from a source and pushes it on \a tempAllocStack. @@ -429,6 +425,7 @@ temp_vstring mid(const char *sin, long p, long l); * \bug a stack overflow of \a tempAllocStack is not handled correctly. */ temp_vstring left(const char *sin, long n); + /*! * \fn temp_vstring right(const char *sin, long n) * \brief Extract the substring starting with position n. @@ -454,6 +451,7 @@ temp_vstring left(const char *sin, long n); */ temp_vstring right(const char *sin, long n); temp_vstring edit(const char *sin, long control); + /*! * \fn temp_vstring space(long n) * pushes a NUL terminated string of __n__ characters onto @@ -466,6 +464,7 @@ temp_vstring edit(const char *sin, long control); * \bug a stack overflow of \a tempAllocStack is not handled correctly. */ temp_vstring space(long n); + /*! * \fn temp_vstring string(long n, char c) * pushes a NUL terminated string of __n__ characters __c__ onto @@ -481,6 +480,7 @@ temp_vstring space(long n); * \bug a stack overflow of \a tempAllocStack is not handled correctly. */ temp_vstring string(long n, char c); + /*! * \fn temp_vstring chr(long n) * \brief create a temporary string containing a single byte. @@ -502,24 +502,41 @@ temp_vstring string(long n, char c); * \bug a stack overflow of \a tempAllocStack is not handled correctly. */ temp_vstring chr(long n); + temp_vstring xlate(const char *sin, const char *table); + temp_vstring date(void); + temp_vstring time_(void); + temp_vstring num(double x); + temp_vstring num1(double x); + temp_vstring str(double x); + long len(const char *s); + long instr(long start, const char *string1, const char *string2); + long rinstr(const char *string1, const char *string2); + long ascii_(const char *c); + double val(const char *s); + /* Emulation of Progress 4GL string functions */ + temp_vstring entry(long element, const char *list); + long lookup(const char *expression, const char *list); + long numEntries(const char *list); + long entryPosition(long element, const char *list); + /* Routines may/may not be written (lowest priority): vstring place$(vstring sout); vstring prod$(vstring sout); @@ -565,13 +582,14 @@ extern long g_tempAllocStackTop; /* Top of stack for tempAlloc function */ extern long g_startTempAllocStack; /* Where to start freeing temporary allocation when let() is called (normally 0, except for nested vstring functions) */ -/* Make string have temporary allocation to be released by next let(). +/*! \brief Make string have temporary allocation to be released by next let(). + This function effectively changes the type of `s` from `vstring` (an owned pointer) to `temp_vstring` (a temporary to be freed by the next `let()`). See `temp_vstring` for information on what you can do with temporary strings. In particular, after makeTempAlloc() is called, the vstring may NOT be assigned again with let(). */ -temp_vstring makeTempAlloc(vstring s); /* Make string have temporary allocation to be - released by next let() */ +temp_vstring makeTempAlloc(vstring s); + #endif /* METAMATH_MMVSTR_H_ */ diff --git a/src/mmword.c b/src/mmword.c index ac9d6c8a..a068db4d 100644 --- a/src/mmword.c +++ b/src/mmword.c @@ -62,6 +62,12 @@ flag printedAtLeastOne; vstring reserve2_[MAX_BUF]; +/* These two functions emulate 2 GOSUBs in BASIC, that are part of a + translation of a very old BASIC program (by nm) that implemented a + difference algorithm (like Unix diff). */ +void gosub_7320(void); +void gosub_7330(void); + /* revise() is called by the UPDATE command of TOOLs. The idea is to keep all past history of a file in the file itself, in the form of comments. In mmcmds.c, see the parsing of the UPDATE command for a diff --git a/src/mmword.h b/src/mmword.h index b427e36b..d1da82bd 100644 --- a/src/mmword.h +++ b/src/mmword.h @@ -7,27 +7,24 @@ #ifndef METAMATH_MMWORD_H_ #define METAMATH_MMWORD_H_ +/*! \file */ + #include "mmvstr.h" -/* Tag file changes with revision number tags */ +/*! Tag file changes with revision number tags */ void revise(FILE *f1_fp, FILE *f2_fp, FILE *f3_fp, vstring addTag, long m); -/* Get the largest revision number tag in a file */ -/* Tags are assumed to be of format nn or #nn in comment at end of line */ -/* Used to determine default argument for tag question */ +/*! \brief Get the largest revision number tag in a file + + Tags are assumed to be of format nn or #nn in comment at end of line. + Used to determine default argument for tag question. */ long highestRevision(vstring fileName); -/* Get numeric revision from the tag on a line (returns 0 if none) */ -/* Tags are assumed to be of format nn or #nn in comment at end of line */ -long getRevision(vstring line); +/*! \brief Get numeric revision from the tag on a line (returns 0 if none) - -/* These two functions emulate 2 GOSUBs in BASIC, that are part of a - translation of a very old BASIC program (by nm) that implemented a - difference algorithm (like Unix diff). */ -void gosub_7320(void); -void gosub_7330(void); + Tags are assumed to be of format nn or #nn in comment at end of line */ +long getRevision(vstring line); #endif /* METAMATH_MMWORD_H_ */ diff --git a/src/mmwtex.h b/src/mmwtex.h index acd2ef1e..fb9f0576 100644 --- a/src/mmwtex.h +++ b/src/mmwtex.h @@ -7,90 +7,99 @@ #ifndef METAMATH_MMWTEX_H_ #define METAMATH_MMWTEX_H_ +/*! \file */ + #include "mmvstr.h" #include "mmdata.h" /* Colors for HTML pages. */ #define GREEN_TITLE_COLOR "\"#006633\"" #define MINT_BACKGROUND_COLOR "\"#EEFFFA\"" -#define PINK_NUMBER_COLOR "\"#FA8072\"" /* =salmon; was FF6666 */ +#define PINK_NUMBER_COLOR "\"#FA8072\"" + /* =salmon; was FF6666 */ #define PURPLISH_BIBLIO_COLOR "\"#FAEEFF\"" #define SANDBOX_COLOR "\"#FFFFD9\"" /* TeX flags */ -extern flag g_oldTexFlag; /* Use macros in output; obsolete; take out someday */ +extern flag g_oldTexFlag; /*!< Use macros in output; obsolete; take out someday */ /* HTML flags */ -extern flag g_htmlFlag; /* HTML flag: 0 = TeX, 1 = HTML */ -extern flag g_altHtmlFlag; /* Use "althtmldef" instead of "htmldef". This is +extern flag g_htmlFlag; /*!< HTML flag: 0 = TeX, 1 = HTML */ +extern flag g_altHtmlFlag; /*!< Use "althtmldef" instead of "htmldef". This is intended to allow the generation of pages with the old Symbol font instead of the individual GIF files. */ -extern flag g_briefHtmlFlag; /* Output statement only, for statement display +extern flag g_briefHtmlFlag; /*!< Output statement only, for statement display in other HTML pages, such as the Proof Explorer home page */ -extern long g_extHtmlStmt; /* At this statement and above, use the exthtmlxxx +extern long g_extHtmlStmt; /*!< At this statement and above, use the exthtmlxxx variables for title, links, etc. This was put in to allow proper generation of the Hilbert Space Explorer extension to the set.mm database. */ -extern vstring g_extHtmlTitle; /* Title of extended section if any; set by +extern vstring g_extHtmlTitle; /*!< Title of extended section if any; set by by exthtmltitle command in special $t comment of database source */ -extern vstring g_htmlVarColor; /* Set by htmlvarcolor commands */ -extern vstring g_htmlHome; /* Set by htmlhome command */ -extern vstring g_htmlBibliography; /* Optional; set by htmlbibliography command */ -extern vstring g_extHtmlBibliography; /* Optional; set by exthtmlbibliography +extern vstring g_htmlVarColor; /*!< Set by htmlvarcolor commands */ +extern vstring g_htmlHome; /*!< Set by htmlhome command */ +extern vstring g_htmlBibliography; /*!< Optional; set by htmlbibliography command */ +extern vstring g_extHtmlBibliography; /*!< Optional; set by exthtmlbibliography command */ -extern vstring g_htmlCSS; /* Set by htmlcss commands */ -extern vstring g_htmlFont; /* Optional; set by g_htmlFont command */ +extern vstring g_htmlCSS; /*!< Set by htmlcss commands */ +extern vstring g_htmlFont; /*!< Optional; set by g_htmlFont command */ -void eraseTexDefs(void); /* Undo readTexDefs() */ +/*! Undo readTexDefs() */ +void eraseTexDefs(void); /* TeX/HTML/ALT_HTML word-processor-specific routines */ -/* Returns 2 if there were severe parsing errors, 1 if there were warnings but - no errors, 0 if no errors or warnings */ -/* The GIF check ensures that for every 'htmldef' definition containing - `IMG SRC="bla.gif"`, `bla.gif` must exist. */ +/*! + \param gifCheck The GIF check ensures that for every 'htmldef' definition containing + `IMG SRC="bla.gif"`, `bla.gif` must exist. + \returns 2 if there were severe parsing errors, 1 if there were warnings but + no errors, 0 if no errors or warnings +*/ flag readTexDefs( - flag errorsOnly, /* 1 = suppress non-error messages */ - flag gifCheck /* 1 = check for missing GIFs */); + flag errorsOnly, /*!< 1 = suppress non-error messages */ + flag gifCheck /*!< 1 = check for missing GIFs */); extern flag g_texDefsRead; -struct texDef_struct { /* for "erase" */ - vstring tokenName; /* ASCII token */ - vstring texEquiv; /* Converted to TeX */ +/*! for "erase" */ +struct texDef_struct { + vstring tokenName; /*!< ASCII token */ + vstring texEquiv; /*!< Converted to TeX */ }; -extern struct texDef_struct *g_TexDefs; /* for "erase" */ +extern struct texDef_struct *g_TexDefs; /*!< for "erase" */ long texDefWhiteSpaceLen(char *ptr); long texDefTokenLen(char *ptr); -/* Token comparison for qsort */ +/*! Token comparison for qsort */ int texSortCmp(const void *key1, const void *key2); -/* Token comparison for bsearch */ +/*! Token comparison for bsearch */ int texSrchCmp(const void *key, const void *data); -/* Convert ascii to a string of \tt tex */ -/* (The caller must surround it by {\tt }) */ +/*! Convert ascii to a string of \tt tex + + (The caller must surround it by {\tt }) */ vstring asciiToTt(vstring s); vstring tokenToTex(vstring mtoken, long statemNum); -/* Converts a comment section in math mode to TeX. Each math token +/*! Converts a comment section in math mode to TeX. Each math token MUST be separated by white space. TeX "$" does not surround the output. */ vstring asciiMathToTex(vstring mathComment, long statemNum); -/* Gets the next section of a comment that is in the current mode (text, +/*! Gets the next section of a comment that is in the current mode (text, label, or math). If 1st char. is not "$", text mode is assumed. mode = 0 means end of comment reached. srcptr is left at 1st char. of start of next comment section. */ vstring getCommentModeSection(vstring *srcptr, char *mode); void printTexHeader(flag texHeaderFlag); -/* Prints an embedded comment in TeX. The commentPtr must point to the first +/*! Prints an embedded comment in TeX. The commentPtr must point to the first character after the "$(" in the comment. The printout ends when the first "$)" or null character is encountered. commentPtr must not be a temporary allocation. htmlCenterFlag, if 1, means to center the HTML and add a - "Description:" prefix.*/ + "Description:" prefix + \returns 1 if error/warning */ /* void printTexComment(vstring commentPtr, char htmlCenterFlag); */ -/* returns 1 if error/warning */ -flag printTexComment(vstring commentPtr, /* Sends result to g_texFilePtr */ - flag htmlCenterFlag, /* 1 = htmlCenterFlag */ - long actionBits, /* see indicators below */ - flag fileCheck /* 1 = fileCheck */); +flag printTexComment(vstring commentPtr, /*!< Sends result to g_texFilePtr */ + flag htmlCenterFlag, /*!< 1 = htmlCenterFlag */ + long actionBits, /*!< see indicators below */ + flag fileCheck /*!< 1 = fileCheck */); + /* Indicators for actionBits */ #define ERRORS_ONLY 1 #define PROCESS_SYMBOLS 2 @@ -111,7 +120,7 @@ void printTexLongMath(nmbrString *proofStep, vstring startPrefix, vstring contPrefix, long hypStmt, long indentationLevel); void printTexTrailer(flag texHeaderFlag); -/* Function implementing WRITE THEOREM_LIST / THEOREMS_PER_PAGE nn */ +/*! Function implementing WRITE THEOREM_LIST / THEOREMS_PER_PAGE nn */ void writeTheoremList(long theoremsPerPage, flag showLemmas, flag noVersioning); @@ -128,77 +137,81 @@ flag getSectionHeadings(long stmt, vstring *hugeHdrTitle, vstring *bigHdrComment, vstring *smallHdrComment, vstring *tinyHdrComment, - flag fineResolution, /* 0 = consider just successive $a/$p, 1 = all stmts */ - flag fullComment /* 1 = put $( + header + comment + $) into xxxHdrTitle */ + flag fineResolution, /*!< 0 = consider just successive $a/$p, 1 = all stmts */ + flag fullComment /*!< 1 = put $( + header + comment + $) into xxxHdrTitle */ ); /* TeX normal output */ extern flag g_texFileOpenFlag; extern FILE *g_texFilePtr; -/* Pink statement number HTML code for HTML pages */ -/* Warning: caller must deallocate returned string */ +/*! Pink statement number HTML code for HTML pages + \warning caller must deallocate returned string */ vstring pinkHTML(long statemNum); -/* Pink statement number range HTML code for HTML pages, separated by a "-" */ -/* Warning: caller must deallocate returned string */ +/*! Pink statement number range HTML code for HTML pages, separated by a "-" + \warning caller must deallocate returned string */ vstring pinkRangeHTML(long statemNum1, long statemNum2); #define PINK_NBSP " " /* Either "" or " " depending on taste, it is the separator between a statement href and its pink number */ -/* This function converts a "spectrum" color (1 to maxColor) to an +/*! This function converts a "spectrum" color (1 to maxColor) to an RBG value in hex notation for HTML. The caller must deallocate the returned vstring. color = 1 (red) to maxColor (violet). */ vstring spectrumToRGB(long color, long maxColor); -/* Returns the HTML code for GIFs (!g_altHtmlFlag) or Unicode (g_altHtmlFlag), +/*! Returns the HTML code for GIFs (!g_altHtmlFlag) or Unicode (g_altHtmlFlag), or LaTeX when !g_htmlFlag, for the math string (hypothesis or conclusion) that - is passed in. */ -/* Warning: The caller must deallocate the returned vstring. */ + is passed in. + \warning The caller must deallocate the returned vstring. */ vstring getTexLongMath(nmbrString *mathString, long statemNum); -/* Returns the TeX, or HTML code for GIFs (!g_altHtmlFlag) or Unicode +/*! Returns the TeX, or HTML code for GIFs (!g_altHtmlFlag) or Unicode (g_altHtmlFlag), for a statement's hypotheses and assertion in the form - hyp & ... & hyp => assertion */ -/* Warning: The caller must deallocate the returned vstring. */ + hyp & ... & hyp => assertion + \warning The caller must deallocate the returned vstring. */ vstring getTexOrHtmlHypAndAssertion(long statemNum); -/* For WRITE BIBLIOGRAPHY command and error checking by VERIFY MARKUP */ -/* Returns 0 if OK, 1 if error or warning found */ -/* In addition to checking for GIFs (see readTexDefs()), - the `fileCheck` flag controls whether to attempt to open and parse the - `htmlbibliograhy` or `exthtmlbibliograhy` file to search for anchors, - which can be used to verify the correctness of bibliography tags. */ +/*! + \brief For WRITE BIBLIOGRAPHY command and error checking by VERIFY MARKUP + + In addition to checking for GIFs (see readTexDefs()), + the `fileCheck` flag controls whether to attempt to open and parse the + `htmlbibliograhy` or `exthtmlbibliograhy` file to search for anchors, + which can be used to verify the correctness of bibliography tags. + + \returns 0 if OK, 1 if error or warning found */ flag writeBibliography(vstring bibFile, - vstring labelMatch, /* Normally "*" except by verifyMarkup() */ - flag errorsOnly, /* 1 = no output, just warning msgs if any */ - flag fileCheck); /* 1 = check external files (gifs and bib) */ + vstring labelMatch, /*!< Normally "*" except by verifyMarkup() */ + flag errorsOnly, /*!< 1 = no output, just warning msgs if any */ + flag fileCheck /*!< 1 = check external files (gifs and bib) */ +); -/* Globals to hold mathbox information. They should be re-initialized +/*! Globals to hold mathbox information. They should be re-initialized by the ERASE command (eraseSource()). g_mathboxStmt = 0 indicates it and the other variables haven't been initialized. */ extern long g_mathboxStmt; /* stmt# of "mathbox" label; statements+1 if none */ extern long g_mathboxes; /* # of mathboxes */ /* The following 3 "strings" are 0-based e.g. g_mathboxStart[0] is for mathbox #1 */ -extern nmbrString *g_mathboxStart; /* Start stmt vs. mathbox # */ -extern nmbrString *g_mathboxEnd; /* End stmt vs. mathbox # */ -extern pntrString *g_mathboxUser; /* User name vs. mathbox # */ +extern nmbrString *g_mathboxStart; /*!< Start stmt vs. mathbox # */ +extern nmbrString *g_mathboxEnd; /*!< End stmt vs. mathbox # */ +extern pntrString *g_mathboxUser; /*!< User name vs. mathbox # */ -/* Returns 1 if statements are in different mathboxes */ +/*! Returns 1 if statements are in different mathboxes */ flag inDiffMathboxes(long stmt1, long stmt2); -/* Returns the user of the mathbox that a statement is in, or "" - if the statement is not in a mathbox. */ -/* Caller should NOT deallocate returned string (it points directly to +/*! Returns the user of the mathbox that a statement is in, or "" + if the statement is not in a mathbox. + \attention Caller should NOT deallocate returned string (it points directly to g_mathboxUser[] entry); use directly in print2() messages */ vstring getMathboxUser(long stmt); -/* Returns the mathbox number (starting at 1) that stmt is in, or 0 if not +/*! Returns the mathbox number (starting at 1) that stmt is in, or 0 if not in a mathbox */ long getMathboxNum(long stmt); -/* Populates mathbox information */ +/*! Populates mathbox information */ void assignMathboxInfo(void); -/* Creates lists of mathbox starts and user names */ +/*! Creates lists of mathbox starts and user names */ long getMathboxLoc(nmbrString **mathboxStart, nmbrString **mathboxEnd, pntrString **mathboxUser);