• The Theorem Loader provides a way to load theorems -- but not other Metamath objects -- into mmj2's current Logical System in memory and to write out those theorems in Metamath .mm format to a designated directory (folder).
• [Restrictions] New theorems are loaded into the Logical System global scope level, and must have all new logical hypotheses, they cannot share logical hypotheses with other theorems (i.e. shared scope, as is sometimes the case in set.mm with groups of lemmas and theorems.)  Existing theorems are also handled by the Theorem Loader, but only the proofs ('$=") and distinct variable restrictions ('$d') are updated. (As with the Proof Assistant GUI, variable and variable hypothesis declarations are not permitted in use with the TheoremLoader).
  
• Input to the Theorem Loader can be either a designated directory, containing one separate type ".mmt" (to avoid accidents involving ".mm" files :-) file for each theorem to be loaded. Or, a successfully unified mmj2 Proof Worksheet passed via a program "call" statement (incomplete and invalid Proof Worksheets are not "storable" using Theorem loader, but the Metamath "eimm" command may provide more support for importing from/exporting to Proof Worksheets involving incomplete or invalid proofs..)
  
• Output from the Theorem Loader consists of theorems written as ".mmt" type files in the Metamath .mm file format, as well as updates to mmj2's Logical System in memory.
• An additional primary benefit of the new Theorem Loader feature is that it provides a mechanism for the mmj2 Proof Assistant GUI to dynamically update the mmj2 Logical System presently in memory with new and newly-proven theorems. Dynamically stored new theorems and new proofs from the mmj2 Proof Assistant GUI are written out to a directory as individual ".mmt" files which can be read back in by the Theorem Loader, thus enabling a user to perform considerable amounts of work in one or multiple sessions before being forced to manually update the main .mm file (e.g. set.mm) -- without having to exit-and-restart mmj2!
  

I. Data Stores

A. Command Line Parms

B. .mm file(s)

C. .mmt folder

• Only files in the named directory itself -- not its sub-directories -- are loaded from the .mmt folder (directory). Thus, sub-directories of the .mmt folder could be used as archives or backup locations for work which has already been completed.
• For convenience -- especially because the Proof Assistant provides access to the Theorem Loader -- the user need not specify a .mmt Folder, either via RunParm or the Proof Assistant GUI prior to its actual use; this allows use of mmj2 without using the Theorem Loader, with no change to existing RunParm files or user practices. However, when processing requires a .mmt Folder and the .mmt Folder is "null" (not yet specified), an error message is output. There is no default setting for .mmt Folder, in other words (i.e. not to the "current directory" or any place else.)
  
• Only files with file type ".mmt" are loaded. Other files, such as ".mmp" (mmj2 Proof Worksheets) can be stored in the .mmt folder, which means that a single directory (folder) could be used as the .mmt folder and the "ProofAsstProofFolder" (see mmj2\mmj2jar\RunParms.txt) -- but this is not recommended (best to separate the two.)
  
• Only files whose filename -- minus the file type -- exactly matches the "$p" label inside each file are loaded (e.g. "syl.mmt" matches label "syl").
• Only files containing exactly one theorem are loaded.
• Files may contain only Metamath statements "${", "$}", "$(", "$)", "$d", "$e",  and "$p". Files containing any other statements are not loaded.
  
• Each "$(" (Begin Comment) must be followed by a "$)" (End Comment), and each "${" (Begin Scope) must be followed by a "$}" (End Scope).
• A maximum of one pair of Scope statements, "${" and "$}", is allowed. If "$d" or "$e" statements are used with the theorem a pair of Scope statements is mandatory.. If scope statements are used, Begin Scope, "${", must be the first Metamath statement in the file, and End Scope, "$}" must be the last Metamath statement in the file.
• If "$d" and/or "$e" statements are used with the theorem, these statements must precede the "$p" statement -- the $p statement is, of course, always mandatory.
  
• FYI, a Metamath comment statement should immediately precede the "$p" (e.g. "$( this is a comment $)  syl $p blah $=  ? $."). This is the only comment which Theorem Loaded will store in the Logical System. Any other comments are ignored.
  
• Only uncompressed proofs may be used -- compressed proofs will "error out" with a syntax error message.
• "Syntax theorems" cannot be input via the Theorem Loader -- the Type Code (i.e. 1st symbol of formula) on each Logical Hypothesis ('$e') and Theorem ('$p') statement must equal the "provable logic statement type code" in use with the input .mm file. For set.mm and ql.mm this is "|-" (see RunParm "ProvableLogicStmtType").
  
• For updates to existing theorems, the Logical Hypotheses and the Theorem formula must exactly match what is already present in the Logical System. New hypotheses cannot be added. Conversely, new Theorems cannot share Logical Hypotheses with other Theorems (i.e. it is not possible to insert a new Theorem into an existing local scope).
  

D. RunParms.txt

• "TheoremLoaderMMTFolder" is a constant
• "DirectoryPathname" specifies the default pathname of the .mm folder to be used by the Theorem Loader to write or load theorem .mmt files (via the Theorem Loader).

• "TheoremLoaderDjVarsOption" is a constant
• "DjVarsOption" specifies how $d statements in an existing theorem's extended frame are to be updated by an input .mmt file for that theorem; may be either "Replace" (means "replace old with new"), "Merge" (means "merge old with new"), or "NoUpdate" (the default, means "don't touch the old $d's!!!") Note: A new theorem's $d statements are set to the $d statement in the input .mmt file.

• "TheoremLoaderAuditMessages"  is a constant
• GenerateAuditMessages: may be "Yes", "No" or omitted. Default is "No". If set to "Yes" then audit messages about the load process are generated (for educational and testing purposes.)

• "LoadTheoremsFromMMTFolder" is a constant
• "LoadSpecification" equals either "*", meaning "Load the entire contents of the .mmt Folder" or is a theorem label, meaning to load the file "label.mmt" from the .mmt Folder.

• This RunParm can be located anywhere in the RunParms.txt file after the LoadFile command. It is most efficient to locate it immediately after the LoadFile command, prior to the "VerifyProof,*" and "Parse,*". For maximum ease of use however, the LoadTheoremsFromMMTFolder RunParm can be located after the "VerifyProof,*" and "Parse,*". This is because the source of any Verify errors will be more obvious. Newly loaded theorems are verified and parsed if the VerifyProof and Grammar objects are available, which is based on the current processing location in the RunParms file. It is possible for updated $d statements in existing theorems tol cause Verify Proof errors in subsequent theorems which have not been updated.
  
• Multiple LoadTheoremsFromMMTFolder RunParm commands can be input, but that would be an "advanced" scenario -- and perhaps troublesome in practice.
  
• If the RunParm options are invalid an error message is generated and processing terminates.
• If the RunParm is valid but one or more input .mmt files contain serious errors, error message(s) are output but the MMJ2Batch job continues processing RunParm.txt commands, and any updates made to the LogicalSystem are rolled back (undone).
  
• Informational messages are generated for successful .mmt file loads (Note: using RunParm "OutputVerbosity,0" will turn off informational messages in the output print stream.)
• The MObj.seq number -- the sequential, logical location within the Logical System -- of a new theorem is computed as follows: a) if the theorem's proof contains a "?" symbol then the theorem is added at the end of the Logical System but prior to any other new theorems being loaded which depend upon it in their own proofs; b) if the theorem's proof does not contain a "?" symbol then the MObj.seq is computed to be in the "gap", if present, following the highest MObj.seq of the assertions and logical hypotheses it uses in its proof. (MObj.seq numbers are assigned from 100 by 100, so "gap" refers to the range between two originally assigned MObj.seq numers -- for example the gap after MObj.seq 3600 is 3601 through 3699.) If the "gap" is full -- has no unused seq numbers, the theorem is added at the end of the Logical System but prior to any other new theorems being loaded which depend on it in their own proofs.
• Certain proof errors such as cyclic or forward references, or non-existent labels referenced in proofs are considered "severe" and result in not only harshly worded, cryptic error messages but termination of the LoadTheoremsFromMMTFolder RunParm's processing -- and "undo" of any updates that were made during the command's processing. However, a proof that is merely incomplete (contains "?" label) or incorrect -- does not prove the conclusion -- is reported with an error message and processing continues (this behavior is identical to the  "VerifyProofs,*" processing -- where proof errors in already loaded theorems are reported but do not terminate the entire BatchMMJ2 jobstream.)
• Only the "$d" and "$=" (Distinct Variable and Proof) data are updated using the contents of an input .mmt file which specifies a theorem already loaded into the Logical System. An error message is generated if any formulas in the existing theorem and its logical hypotheses are different from the input (this is a fail-safe double-check...)

• "ExtractTheoremToMMTFolder" is a constant
• "TheoremLabel" specifies the label of a theorem ($p) statement already loaded into the Logical System.

• NOTE: This RunParm was added for use in system testing of mmj2 but is described here for the sake of completeness. (The Proof Assistant RunParm "ProofAsstExportToFile" outputs Proof Worksheets and this RunParm converts a Proof Worksheet to Metamath .mm file format and stores it in the .mmt Folder, thus allowing us to go full circle...)
• "UnifyAndStoreInLogSysAndMMTFolder" is a constant
• ProofWorksheetFileName may be a relative filename such as "syl.mmp" or an "absolute" name such as "c:\my\myproofs\syl.txt". If the "ProofAsstProofFolder" RunParm has been input, it is used with a relative filename.
• The input file is parsed and unified, then if the proof unifies successfully, the theorem is stored in the .mmt Folder and is loaded into the Logical System by the Theorem Loader.
• Note: this is technically a Theorem Loader RunParm but because it uses the Proof Assistant, this RunParm is affected by previously input Proof Assistant RunParms.
  

• NOTE: This RunParm was added for use in system testing of mmj2 but is described here for the sake of completeness. (The Proof Assistant RunParm "ProofAsstExportToFile" outputs Proof Worksheets and this RunParm converts a Proof Worksheet to Metamath .mm file format and stores it in the .mmt Folder, thus allowing us to go full circle...)
  
• "UnifyAndStoreInLogSysAndMMTFolder" is a constant
• ProofWorksheetFileName may be a relative filename such as "syl.mmp" or an "absolute" name such as "c:\my\myproofs\syl.txt". If the "ProofAsstProofFolder" RunParm has been input, it is used with a relative filename.
• The input file is parsed and unified, then if the proof unifies successfully, the theorem is stored in the .mmt Folder.
• Note: this is technically a Theorem Loader RunParm but because it uses the Proof Assistant, this RunParm is affected by previously input Proof Assistant RunParms.
  

II. Processes

A. mmj2 Service "Caller"

• In mmj2 Service Caller mode, a user program creates an object satisfying the new mmj2 "SvcCallback" interface and then passes a reference to that object in its call to BatchMMJ2.generateSvcCallback() -- also passing the necessary BatchMMJ2 Command Line Parms which specify the RunParms file to be used by mmj2.
• BatchMMJ2 then performs the normal processing, which involves calling BatchFramework, which processes the RunParms.txt file.
• Inside the RunParms.txt file various "Svc*" RunParms may be specified, including the executable RunParm,"SvcCall".
• When BatchFramework executes the "SvcCall" RunParm it invokes the "go()" method in the designated SvcCallback interface object.
• The "go()" method is passed arguments providing access to the main mmj2 objects, including ProofAsst.
• The Caller program simply needs to exit the "go()" method to terminate mmj2's callback, at which point the user's Caller program remains in control and may continue processing as it pleases.
  

B. BatchMMJ2

C. BatchFramework

D. SvcCallback

E. LogicalSystem

• mmj.pa.ProofUnifier.unifySearchList is sorted by MObj.seq. When commit() is communicated to ProofAsst -- which is passed an object containing a MObj.seq list of containing new theorems added to LogicalSystem.stmtTbl, the new theorems will be merged into unifySearchList in a single pass through the list. If this operation fails for any reason whatsoever then processing in mmj2 is terminated abruptly with a fatal IllegalArgumentException -- therefore, the restore() communique to the TheoremLoadListeners requires no processing.
• mmj.pa.StepSelectorSearch.assrtArray is sorted by Assrt.NBR_LOG_HYP_SEQ.. The assrtArray will be changed to be an ArrayList called assrtList -- and StepSelectorSearch modified accordingly -- so that insertions can be made without recreating the array (we look forward to the day when Metamath's set.mm has 1,000,000 theorems :-) Then when commit() is communicated to ProofAsst -- which is passed an object containing a MObj.seq list of new theorems added to LogicalSystem.stmtTbl, the list of new theorems will be first sorted by Assrt.NBR_LOG_HYP_SEQ and then merged into unifySearchList in a single pass through the list. If this operation fails for any reason whatsoever then processing in mmj2 is terminated abruptly with a fatal IllegalArgumentException -- therefore, the restore() communique to the TheoremLoadListeners requires no processing.
• The initial capacity of mmj.pa.ProofUnifier.unifySearchList and StepSelectorSearch.assrtList will be set at LogicalSystem.stmtTbl.size() * 105% so that TheoremLoader inserts do not require resizing unless rather large additions are made.
• mmj.lang.BookManager keeps track of Chapters and Sections, and maintains the following fields in MObj: MObj.chapterNbr, MObj.sectionNbr, and MObj.sectionMObjNbr. The key idea of BookManager is that each MObj is assigned to a Section, and MObj.sectionMObjNbr is assigned from 1 by 1 within the current Section, thus allowing unlimited inserts at the end of a Section. When commit() is communicated to BookManager -- which is passed an object containing a MObj.seq list of new theorems added to LogicalSystem.stmtTbl, the new theorems will be assigned BookManager chapter, section and sectionMObj numbers. If this operation fails for any reason whatsoever then processing in mmj2 is terminated abruptly with a fatal IllegalArgumentException -- therefore, the restore() communique to the BookManager requires no processing. Note that the input list of theorems contains for each new theorem, a "located after" reference to an existing MObj -- this is used to determine the BookManager Chapter and Section of the new theorem: the new theorem is assigned to the Chapter and Section of the "located after" MObj (adjusted for the fact that Section is adjusted for the type of MObj, so if the "located after" MObj happens to be an axiom, then the theorem's Section will be one greater than the "located after" MObj's section. Note also -- this is important -- if the input theorem list contains an update to an existing theorem's proof and the revised proof uses a new theorem in the same BookManager Section, then the MObj.sectionMObjNbr's will need to be resequenced following the initial assignment (to eliminate the severely erroneous forward reference.)
  

F. ProofAsst

• Theorem Loader DjVars Option: Identical to function of TheoremLoaderDjVarsOption RunParm. Specifies how $d statements in an existing theorem's extended frame are to be updated by an input .mmt file for that theorem; may be either "Replace" (means "replace old with new"), "Merge" (means "merge old with new"), or "NoUpdate" (the default, means "don't touch the old $d's!!!") Note: A new theorem's $d statements are set to the $d statement in the input .mmt file.
  
• Theorem Loader MMT Folder: Identical to function of TheoremLoaderMMTFolder RunParm. Specifies the pathname of the directory to be used for storing or retrieving .mmt files with the Theorem Loader.
• Theorem Loader Audit Messages: Identical to function of TheoremLoaderAuditMessages RunParm. May be "Yes", "No" or omitted. Default is "No". If set to "Yes" then audit messages about the load process are generated (for educational and testing purposes.)
• Load Theorems From MMT Folder: identical to function of LoadTheoremsFromMMTFolder RunParm.

• Extract Theorem To MMT Folder: identical to function of ExtractTheoremToMMTFolder RunParm.
  
• Unify + Store in MMT Folder: Unifies the Proof Worksheet, and if the proof unifies successfully, a .mmt file is created in the current .mmt Folder for the Proof Worksheet's theorem. Note: if the Proof Worksheet has been modified since the last File/Save, the user is prompted to save before proceeding.

• Unify + Store in LogSys and MMT Folder: Unifies the Proof Worksheet, and if the proof unifies successfully, a .mmt file is created in the current .mmt Folder for the Proof Worksheet's theorem. Then, if there are no errors, the newly stored .mmt file is loaded into the Logical System using the same processed used by LoadTheoremsFromMMTFolder RunParm, except that only a single .mmt file is loaded. Note: if the Proof Worksheet has been modified since the last File/Save, the user is prompted to save before proceeding. Also note that if the theorem is new and the LOC_AFTER field has been used in the Proof Worksheet header, the user will need to erase the LOC_AFTER location manually if another Unify function is attempted (because the theorem is no longer new and LOC_AFTER applies only to new theorems.)
  
• Verify All Proofs: This operates identically to the "VerifyProof,*" RunParm -- except that if the "LoadProofs,no" RunParm was used during initial file loading, something like 10,000 error messages will be returned (subject to the "MaxErrorMessages" RunParm limitation :-) Proof Verification using the Metamath proof verification algorithm is equivalent, in theory, to the mmj2 Unification algorithm. However, if Theorem Loader has been used to update the $d specifications of an existing theorem, other theorems which refer to that theorem in their proofs may become "invalid" as a result of the Theorem Loader's update -- which is precisely the reason that this function will be useful in the mmj2 Proof Assistant GUI.

G. TheoremLoader