public class ProofCompression
extends java.lang.Object
Constructor and Description |
---|
ProofCompression()
Constructor - default.
|
Modifier and Type | Method and Description |
---|---|
java.util.List<Stmt> |
compress(java.lang.String theoremLabel,
int width,
java.util.List<Hyp> mandHypArray,
java.util.List<VarHyp> optHypArray,
ParseTree.RPNStep[] rpnProof,
java.lang.StringBuilder letters) |
ParseTree.RPNStep[] |
decompress(java.lang.String theoremLabel,
int seq,
java.util.Map<java.lang.String,Stmt> stmtTbl,
Hyp[] mandHypArray,
Hyp[] optHypArray,
java.util.List<java.lang.String> otherRefList,
BlockList proofBlockList)
Decompress a single proof.
|
boolean |
isProofStepInExtendedFrame(Stmt proofStep)
Checks to see whether or not a proof step is contained in the Theorem's
Extended Frame.
|
boolean |
isProofStepInFrame(Stmt proofStep,
Hyp[] frame)
Checks to see whether or not a proof step is contained in the given
Frame.
|
public ParseTree.RPNStep[] decompress(java.lang.String theoremLabel, int seq, java.util.Map<java.lang.String,Stmt> stmtTbl, Hyp[] mandHypArray, Hyp[] optHypArray, java.util.List<java.lang.String> otherRefList, BlockList proofBlockList) throws LangException
theoremLabel
- Theorem's label, used in error messages that may be
generated during processing.seq
- the sequence number of the theoremstmtTbl
- Stmt lookup map for translating labels into Stmt object
references.mandHypArray
- The theorem's MandFrame.hypArray.optHypArray
- The theorem's OptFrame.optHypArray.otherRefList
- List of String containing labels of Stmt's provided
in the parenthesized portion of a compressed proof.proofBlockList
- List of String containing the compressed portion of
the proof.LangException
- if an error occurredpublic boolean isProofStepInFrame(Stmt proofStep, Hyp[] frame)
proofStep
- a Statement reference.frame
- the frame to checkpublic boolean isProofStepInExtendedFrame(Stmt proofStep)
Cloned this from mmj.lang.Theorem.java.
First checks to see if the proof step is in the MandFrame's hypArray. If not it checks the OptFrame's hypArray
proofStep
- a Statement reference.public java.util.List<Stmt> compress(java.lang.String theoremLabel, int width, java.util.List<Hyp> mandHypArray, java.util.List<VarHyp> optHypArray, ParseTree.RPNStep[] rpnProof, java.lang.StringBuilder letters)