Skip navigation links
mmj.pa

Class ProofWorksheet

    • Field Detail

      • proofTextTokenizer

        public Tokenizer proofTextTokenizer
      • tmffFormulaSB

        public java.lang.StringBuilder tmffFormulaSB
      • structuralErrors

        public boolean structuralErrors
      • nbrDerivStepsReadyForUnify

        public int nbrDerivStepsReadyForUnify
      • hasWorkVarsOrDerives

        public boolean hasWorkVarsOrDerives
      • newTheorem

        public boolean newTheorem
      • locAfter

        public Stmt locAfter
      • maxSeq

        public int maxSeq
      • comboVarMap

        public java.util.Map<java.lang.String,Var> comboVarMap
      • proofWorkStmtList

        public java.util.List<ProofWorkStmt> proofWorkStmtList
      • greatestStepNbr

        public int greatestStepNbr
      • dvStmtCnt

        public int dvStmtCnt
      • hypStepCnt

        public int hypStepCnt
      • proofSoftDjVarsErrorList

        public java.util.List<java.util.List<DjVars>> proofSoftDjVarsErrorList
      • stepsWithLocalRefs

        public java.util.List<DerivationStep> stepsWithLocalRefs
    • Constructor Detail

      • ProofWorksheet

        public ProofWorksheet(ProofAsstPreferences proofAsstPreferences,
                              Messages messages,
                              boolean structuralErrors,
                              ProofAsstCursor proofCursor)
        Constructor for skeletal ProofWorksheet. This constructor is used in ProofAsst.updateWorksheetWithException(). to create a worksheet that has "structuralErrors". When the GUI displays a worksheet with structural errors it does not update its proofTextArea, and thus, the original user input is left untouched.
        Parameters:
        proofAsstPreferences - variable settings
        messages - the mmj.lang.Messages object used to store error and informational messages.
        structuralErrors - indicates whether or not the ProofWorksheet has severe/fatal validation errors.
        proofCursor - ProofAsstCursor set to position of error.
      • ProofWorksheet

        public ProofWorksheet(Tokenizer proofTextTokenizer,
                              ProofAsstPreferences proofAsstPreferences,
                              LogicalSystem logicalSystem,
                              Grammar grammar,
                              Messages messages,
                              MacroManager macroManager)
        Constructor creating empty ProofWorksheet to be loaded using a Tokenizer. This constructor is used by ProofWorksheetParser.next().
        Parameters:
        proofTextTokenizer - the mmj.mmio.Tokenizer input stream parser.
        proofAsstPreferences - variable settings
        logicalSystem - the loaded Metamath data
        grammar - the mmj.verify.Grammar object
        messages - the mmj.lang.Messages object used to store error and informational messages.
        macroManager - the mmj.pa.MacroManager object
      • ProofWorksheet

        public ProofWorksheet(java.lang.String newTheoremLabel,
                              ProofAsstPreferences proofAsstPreferences,
                              LogicalSystem logicalSystem,
                              Grammar grammar,
                              Messages messages)
        Constructor creating a ProofWorksheet initialized for a new proof for a specific theorem label This constructor is used by ProofAsst.startNewProof(). Note: the ProofWorksheet created here is not a fully populated object -- it is destined for a one-way trip to the output screen via the GUI.
        Parameters:
        newTheoremLabel - Theorem label String.
        proofAsstPreferences - variable settings
        logicalSystem - the loaded Metamath data
        grammar - the mmj.verify.Grammar object
        messages - the mmj.lang.Messages object used to store error and informational messages.
      • ProofWorksheet

        public ProofWorksheet(Theorem theorem,
                              java.util.List<ProofDerivationStepEntry> proofDerivationStepList,
                              boolean deriveFormulas,
                              ProofAsstPreferences proofAsstPreferences,
                              LogicalSystem logicalSystem,
                              Grammar grammar,
                              Messages messages)
        Constructor used for exporting a Proof Worksheet containing a completed proof. Note: the worksheet created by this constructor is "skeletal" in the sense that it is destined for output only. This constructor is used by ProofAsst.exportToFile().
        Parameters:
        theorem - to be used to create ProofWorksheet.
        proofDerivationStepList - List of mmj.verify.ProofDerivationStepEntry created by VerifyProofs
        deriveFormulas - if true, derive formulas during creation
        proofAsstPreferences - variable settings
        logicalSystem - the loaded Metamath data
        grammar - the mmj.verify.Grammar object
        messages - the mmj.lang.Messages object used to store error and informational messages.
    • Method Detail

      • getVarHypFromComboFrame

        public VarHyp getVarHypFromComboFrame(Var v)
      • hasStructuralErrors

        public boolean hasStructuralErrors()
        Gets structuralErrors switch for ProofWorksheet. A "structural error" means that the Proof Worksheet contains one or more validation errors that prevent Unification. An example would be any individual field error or a parse error, theorem label not found, etc. When ProofWorksheet is done validating a proof it must be *clean* for ProofUnifier (or else bad things would happen.)
        Returns:
        boolean structuralErrors
      • setStructuralErrors

        public void setStructuralErrors(boolean structuralErrors)
        Sets structuralErrors switch for ProofWorksheet.

        See hasStructuralErrors() for more info.

        Parameters:
        structuralErrors - boolean, true or false.
      • getNbrDerivStepsReadyForUnify

        public int getNbrDerivStepsReadyForUnify()
        Gets the number of proof derivation steps that are ready for Unification.

        Note: a derivation step with a "?" in its Hyp field is not ready for unification, but interestingly, a subsequent step that refers to that step as one of its Hyps, can be unified (it just can't be "proved".)

        Returns:
        number of derivation steps in the proof that are ready for Unification.
      • incNbrDerivStepsReadyForUnify

        public void incNbrDerivStepsReadyForUnify()
      • isNewTheorem

        public boolean isNewTheorem()
        Returns the isNewTheorem boolean value indicating whether the theorem is new or is already in the Metamath file that was loaded.
        Returns:
        boolean isNewTheorem, which if true means that the theorem being proved is not already in the Metamath database that was loaded.
      • setNewTheorem

        public void setNewTheorem(boolean newTheorem)
      • getTheorem

        public Theorem getTheorem()
        Returns the ProofWorksheet's Theorem reference.
        Returns:
        Theorem may be null if new theorem or errors in ProofWorksheet!
      • getMaxSeq

        public int getMaxSeq()
        Returns the ProofWorksheet theorem maxSeq value.

        For an existing theorem (in the loaded database), maxSeq is just the MObj.seq number of the theorem itself. For a new theorem the LocAfter statement label defines the maxSeq (maxSeq = locAfter.seq + 1)

        The maxSeq value sets a boundary for parsing, proofs, formulas, etc. A Metamath statement cannot legitimately use or refer to another Metamath statement with a sequence number >= its own (no recursive references.)

        Returns:
        maxSeq number in use for the current proof.
      • setMaxSeq

        public void setMaxSeq(int maxSeq)
      • getComboFrame

        public ScopeFrame getComboFrame()
        Returns the proof theorem's "comboFrame".

        "comboFrame" and comboVarMap combine the optional and mandatory frame entries for the theorem, including any $d statements added as part of the proof.

        For an existing theorem this just means merging the Assrt.mandFrame, Theorem.optFrame and any proof $d's, and then deriving the comboVarMap from the set of VarHyp's in the comboFrame.

        For a new theorem this means constructing comboFrame using (ScopeDef)(LogicalSystem.getScopeDefList()).get(0) to obtain the sets of globally active Var's, VarHyp's and DjVars (new Theorems in ProofAsst can only use global scope Var's and VarHyp's) and adding in any $d's from the proof.

        The REASON why the optional and mandatory frames can be combined in this way is a little bit subtle: they only need to be separate if the new theorem is going to be referred to in later theorems' proofs, and ProofAsst does not provide that capability at this time.

        The REASON why we want to combine the optional and mandatory frames is to simplify handling of derivation steps within the proof. Variables used in the intermediate steps would normally be part of the optional frame, if not used in the theorem's formula or its LogHyp formulas. That would create more work, especially at grammatical parse time, when we need to match each Var to its active VarHyp. Soooo...instead of building a mandatory frame for each intermediate step we just build a combo frame for use in every step (and note that DjVars apply to every step regardless of the location of the $d ProofWorkStmt within the Proof Text area.

        Returns:
        MandFrame combined with OptFrame values for the theorem.
      • getHypStepCnt

        public int getHypStepCnt()
        Gets the hypStepCnt counter of the number of HypothesisStep statements in the ProofWorksheet.
        Returns:
        the hypStepCnt.
      • getHypothesisStepFromList

        public HypothesisStep getHypothesisStepFromList(LogHyp h)
        Returns a given HypothesisStep from the ProofWorkStmtList.
        Parameters:
        h - the LogHyp sought in the ProofWorkStmtList.
        Returns:
        the HypothesisStep if found, or null.
      • buildProofWorksheetWorkVarSet

        public java.util.Set<WorkVar> buildProofWorksheetWorkVarSet()
      • getProofWorkStmtList

        public java.lang.Iterable<ProofWorkStmt> getProofWorkStmtList()
        Returns an Iterable over the ProofWorksheet ProofWorkStmt ArrayList.
        Returns:
        Iterable over ProofWorkStmtList.
      • getProofWorkStmtListCnt

        public int getProofWorkStmtListCnt()
        Returns the count of items in the ProofWorksheet ProofWorkStmt ArrayList.
        Returns:
        count of items in ProofWorkStmtList.
      • computeProofWorkStmtLineNbr

        public int computeProofWorkStmtLineNbr(ProofWorkStmt x)
        Computes the line number of a ProofWorkStmt on the screen text area.

        This algorithm requires that we know in advance how many lines are occupied by each ProofWorkStmt. The computation is then simple: just total the previous lineCnt's and add 1. (But if lineCnt is wrong, then we are doomed -- note that TMFF went to a lot of trouble to obtain lineCnt, and lineCnt is computed during parsing of an input ProofWorksheet!)

        Parameters:
        x - the owner ProofWorkStmt
        Returns:
        line number in ProofWorksheet text area.
      • computeProofWorkStmtOfLineNbr

        public ProofWorkStmt computeProofWorkStmtOfLineNbr(int n)
        Determines which ProofWorkStmt is located at a given line number of the screen text area.
        Parameters:
        n - the line number
        Returns:
        ProofWorkStmt at the input line number, or null.
      • computeTotalLineCnt

        public int computeTotalLineCnt()
        Computes the total number of text area lines required to display all ProofWorkStmt objects in the ProofWorksheet.
        Returns:
        total number of lines required for ProofWorkStmt's.
      • getFooterStmt

        public FooterStmt getFooterStmt()
        Returns the ProofWorksheet FooterStmt object.
        Returns:
        FooterStmt of ProofWorksheet.
      • getQedStep

        public DerivationStep getQedStep()
        Returns the QED step of the proof, which is the final derivation step.

        Note: the nomenclature here "qed step" is something made up for ProofAssistant to make things easier to explain.

        Returns:
        the final DerivationStep in the ProofWorksheet.
      • getQedStepProofRPN

        public ParseTree.RPNStep[] getQedStepProofRPN()
        Returns the proof RPN of the QED step of the proof.

        Note that each DerivationStep will have its own proof -- if the proof is valid -- but the QED step's proof is the proof of the theorem itself!

        Returns:
        the RPN proof of the final DerivationStep in the ProofWorksheet.
      • getProofCursor

        public ProofAsstCursor getProofCursor()
        Get the ProofWorksheet ProofCursor object.
        Returns:
        ProofCursor object for ProofWorksheet.
      • setProofCursor

        public void setProofCursor(ProofAsstCursor proofCursor)
        Set the ProofWorksheet ProofCursor object.
        Parameters:
        proofCursor - object for ProofWorksheet.
      • posCursorAtQedStmt

        public void posCursorAtQedStmt()
        Positions the cursor at the 'qed' step if the cursor is not already set.
      • posCursorAtLastIncompleteStmt

        public boolean posCursorAtLastIncompleteStmt(boolean beforeCursor)
        Positions the ProofWorksheet ProofCursor at the last ProofWorkStmt with status = incomplete and sets the cursor at the start of the Ref sub-field.
        Parameters:
        beforeCursor - true if the search starts at the cursor
        Returns:
        true if the cursor was set
      • posCursorAtFirstIncompleteStmt

        public boolean posCursorAtFirstIncompleteStmt(boolean afterCursor)
        Positions the ProofWorksheet ProofCursor at the first ProofWorkStmt with status = incomplete and sets the cursor at the start of the Ref sub-field.
        Parameters:
        afterCursor - true if the search starts at the cursor
        Returns:
        true if the cursor was set
      • incompleteStepCursorPositioning

        public void incompleteStepCursorPositioning()
      • outputCursorInstrumentationIfEnabled

        public void outputCursorInstrumentationIfEnabled()
      • getErrorLabelIfPossible

        public java.lang.String getErrorLabelIfPossible()
      • getErrorLabelIfPossible

        public static java.lang.String getErrorLabelIfPossible(ProofWorksheet proofWorksheet)
      • getTheoremLabel

        public java.lang.String getTheoremLabel()
        Returns the theorem label, if present.
        Returns:
        String containing theorem label, may be null;
      • getLocAfterLabel

        public java.lang.String getLocAfterLabel()
      • getRPNProofLeftCol

        public int getRPNProofLeftCol()
      • findMatchingStepFormula

        public ProofStepStmt findMatchingStepFormula(Formula searchFormula,
                                                     ProofStepStmt exclusiveEndpointStep)
        Searches up to an exclusive endpoint in the proofWorkStmtList for a step whose formula matches the input formula.
        Parameters:
        searchFormula - Formula we're looking for
        exclusiveEndpointStep - Exclusive endpoint of the search (return null as soon as this step is reached, even if its formula matches.)
        Returns:
        ProofStepStmt matching the formula or null if Not Found.
      • renumberProofSteps

        public void renumberProofSteps(int renumberStart,
                                       int renumberInterval)
        Renumbers each ProofWorkStmt according to an input renumberInterval and alters each Hyp reference to conform to the new step numbers.
        Parameters:
        renumberStart - is the number to start at. Commonly equal to 1.
        renumberInterval - is the number to add to each new step number. Commonly equal to 1.
      • tmffReformat

        public void tmffReformat(boolean inputCursorStep)
        Reformats all or just one ProofStepStmt using TMFF.
        Parameters:
        inputCursorStep - set to true to reformat just the proof step underneath the cursor.
      • doubleSpaceQedStep

        public void doubleSpaceQedStep()
        Add extra newline to end of qed step so that the footer step has a blank line before it.
      • addDerivStepForDeriveFeature

        public DerivationStep addDerivStepForDeriveFeature(java.util.List<WorkVar> workVarList,
                                                           Formula formula,
                                                           ParseTree formulaParseTree,
                                                           DerivationStep derivStep)
        Generates a DerivationStep and adds it to the proofWorkStmtList ArrayList on behalf of ProofUnifier.

        If !workVarList.isEmpty() then the new step is marked incomplete and given a Hyp = "?" -- no unification need be attempted. Otherwise, unification can be attempted using no Hyps. If this fails then because the step is marked "generated", the step can be updated to show Hyp "?" (this is a helpful feature for the users, going the extra mile...)

        Parameters:
        workVarList - List of Work Vars in formula.
        formula - Formula of new step.
        formulaParseTree - ParseTree of new Formula
        derivStep - insert point for new step.
        Returns:
        DerivationStep added to the ProofWorksheet.
      • generateNewDerivedStepNbr

        public int generateNewDerivedStepNbr()
        Generates the next value of greatestStepNbr for use in the ProofUnifier Derive feature and returns the new value.
        Returns:
        value of new greatestStepNbr.
      • loadWorksheet

        public java.lang.String loadWorksheet(java.lang.String nextToken,
                                              int inputCursorPos,
                                              StepRequest stepRequestIn)
                                       throws java.io.IOException,
                                              MMIOException,
                                              ProofAsstException
        Load the ProofWorksheet starting with the input token.

        • - The first token of each statement must start in column 1. this means that ((nextToken.length - proofTextTokenizer.getCurrentColumnNbr()) == 0) must be true -->else throw ProofAsstException!
        • - First statement must be a Header, so Load Header using input nextToken If error, throw ProofAsstException.
        • - Loads proof text statements until footer reached or end of file, discarding any generated proof statements along the way: - reject a 2nd Header, if found;
        • - After loading each statement makes sure that worksheet: - begins with a header statement; - contains a "qed" proof step; - ends with a footer statement; If missing footer, qed step or header step, throw ProofAsstException to terminate the parse
        • - If no errors so far, performs remaining "relational" edits on worksheet statements.
        • - During processing here and in any subroutines, a thrown ProofAsstException indicates that the parse is terminated completely.

        Otherwise, return the nextToken value which should be the first token of the next ProofWorksheet or null if EOF. (Each routine that loads a statement will return the next token after the end of the statement's input text.)

        Parameters:
        nextToken - the first token to be loaded.
        inputCursorPos - offset plus one of Caret in Proof TextArea or -1 if not available.
        stepRequestIn - may be null, or StepSelector Search or Choice request and will be loaded into the ProofWorksheet.
        Returns:
        String token starting the next ProofWorksheet or null.
        Throws:
        java.io.IOException - if an error occurred
        MMIOException - if an error occurred
        ProofAsstException - if an error occurred
      • makeLocalRefRevisionsToWorksheet

        public void makeLocalRefRevisionsToWorksheet()
      • loadWorksheetProofLevelNumbers

        public void loadWorksheetProofLevelNumbers()
        Initial load of proof worksheet step level numbers. Note: this assumes that each ProofStepStmt.proofLevel is pre-initialized to zero.
      • getOutputMessageText

        public java.lang.String getOutputMessageText()
        Obtain output message text from ProofWorksheet.

        Note: this is a key function used by ProofAsstGUI.

        Note: with word wrap 'on', newlines are ignored in JTextArea, so we insert spacer lines.

        Returns:
        Proof Error Message Text area as String.
      • getOutputMessageText

        public static java.lang.String getOutputMessageText(Messages messages)
        Obtain output message text from ProofWorksheet.

        Note: this is a key function used by ProofAsstGUI.

        Note: with word wrap 'on', newlines are ignored in JTextArea, so we insert spacer lines.

        Parameters:
        messages - Messages object.
        Returns:
        Proof Error Message Text area as String.
      • getOutputMessageTextAbbrev

        public static java.lang.String getOutputMessageTextAbbrev(Messages m)
      • getOutputProofText

        public java.lang.String getOutputProofText()
        Obtain output proof text from ProofWorksheet.

        Note: this is a key function used by ProofAsstGUI.

        Note: with word wrap 'on', newlines are ignored in JTextArea, so we insert spacer lines.

        Returns:
        Proof Text area as String.
      • addGeneratedProofStmt

        public void addGeneratedProofStmt(ParseTree.RPNStep[] rpnProof)
        Insert a GeneratedProofStmt into the ProofWorksheet

        Note: this is used by ProofAsst after successful unification.

        Parameters:
        rpnProof - Proof Stmt array.
      • addGeneratedProofStmt

        public void addGeneratedProofStmt(java.util.List<Stmt> parenList,
                                          java.lang.String letters)
      • getGeneratedProofStmt

        public GeneratedProofStmt getGeneratedProofStmt()
        Returns the GeneratedProofStmt from the ProofWorksheet

        Note: returns null if unification unsuccessful or not yet performed.

        Returns:
        generatedProofStmt or null if not unified successfully.
      • getDvStmtArray

        public DistinctVariablesStmt[] getDvStmtArray()
        Returns the DistinctVariablesStmt array from the ProofWorksheet.

        Note: may return null.

        Returns:
        DistinctVariablesStmt array or null if there are none.
      • generateAndAddDjVarsStmts

        public void generateAndAddDjVarsStmts()
        Generate DistinctVariablesStmt set for soft DjVars errors.

        Input is ProofWorksheet.proofSoftDjVarsErrorList and ProofAsstPreferences, which determines whether a full replacement set of DistinctVariableStmt's must be created, or only the differences to what is already on the theorem in the .mm database.

        Note that the ProofWorksheet's dvStmtArray, dvStmtCnt and comboFrame are updated -- even though at this time there is no known use of these data items after this point in the processing (which is just prior to displaying the fully-unified proof on the GUI screen). However, there may be a use for the updated data items in testing, and in any case it is best no to leave loose ends dangling.

      • getProvableLogicStmtTyp

        public Cnst getProvableLogicStmtTyp()
      • findFirstMatchingRefOrStep

        public ProofWorkStmt findFirstMatchingRefOrStep(java.lang.String localRef)
      • findMatchingStepNbr

        public ProofWorkStmt findMatchingStepNbr(java.lang.String newStepNbr)
      • loadComboFrameAndVarMap

        public void loadComboFrameAndVarMap()
        Load the combo frame and var array object for use throughout the ProofWorksheet. For new theorems uses global ScopeDef from logical system, pruned by eliminating MObj's with seq >= maxSeq. For existing theorems, merges MandFrame and OptFrame. comboVarMap always built using MandFrame for simplicity and reliability even though it would, theoretically be possible to derive it for new theorems using the ScopeDef (curiously, MandFrame/OptFrame do not directly store Var's -- probably because each VarHyp *has* an associated Var and it would be redundant.)
      • runCallback

        public void runCallback(MacroManager.CallbackType c)
        Run a macro callback.
        Parameters:
        c - The type of callback (event trigger)