public class ProofConstants
extends java.lang.Object
VerifyProofs uses fixed size arrays that are reused from one proof to the next. This is much faster than reallocating everything for each proof, but it means that each instance of VerifyProofs requires massive storage and can only work on one proof at a time. It also means that Metamath databases like set.mm can overflow the arrays (set.mm is unbelievable!) Therefore, VerifyProofs dynamically reallocates its array after an overflow, up to a point; it throws an exception if a predetermined maximum size is exceeded, based on the idea that a bug in the code is more likely than a work formula having 32,000 symbols. The numbers can be changed here, in ProofConstants, up or down (have fun :).
Each mmj message begins with a code, such as this:
E-LA-0007
where the format of the code is X-YY-9999
X
: error level
E
= Error
I
= Information
A
= Abort (processing terminates, usually a bug).
YY
: source code
GM
= mmj.gmff package (see GMFFConstants
)
GR
= mmj.verify.Grammar and related code (see
GrammarConstants
)
IO
= mmj.mmio package (see MMIOConstants
)
LA
= mmj.lang package (see GMFFConstants
)
PA
= mmj.pa package (proof assistant) (see PaConstants
)
PR
= mmj.verify.VerifyProof and related code (see
ProofConstants
)
TL
= mmj.tl package (Theorem Loader).
TM
= mmj.tmff.AlignColumn and related code
UT
= mmj.util package. (see UtilConstants
)
TR
= mmj.transforms package (proof assistant) (see
TrConstants
)
9999
: sequential number within the source code, 0001 through
9999.
Constructor and Description |
---|
ProofConstants() |
public static final int PROOF_ABSOLUTE_MAX_RETRIES
public static final int PROOF_PSTACK_INIT_LEN
public static final int PROOF_PSTACK_HARD_FAILURE_LEN
public static final int PROOF_WEXPR_INIT_LEN
public static final int PROOF_WEXPR_HARD_FAILURE_LEN
public static final int PROOF_SUBST_INIT_LEN
public static final int PROOF_SUBST_HARD_FAILURE_LEN
public static final java.lang.String QED_STEP_NBR
public static final ErrorCode ERRMSG_PSTACK_ARRAY_OVERFLOW
public static final ErrorCode ERRMSG_WEXPR_ARRAY_OVERFLOW
public static final ErrorCode ERRMSG_SUBST_ARRAY_OVERFLOW
public static final ErrorCode ERRMSG_PROOF_STEP_INCOMPLETE
public static final ErrorCode ERRMSG_PROOF_HAS_ZERO_STEPS
public static final ErrorCode ERRMSG_PROOF_STACK_GT_1_AT_END
public static final ErrorCode ERRMSG_FINAL_STACK_ENTRY_UNEQUAL
public static final ErrorCode ERRMSG_HYP_TYP_MISMATCH_STACK_TYP
public static final ErrorCode ERRMSG_SUBST_TO_VARS_MATCH
public static final ErrorCode ERRMSG_SUBST_TO_VARS_NOT_DJ
public static final ErrorCode ERRMSG_STEP_LOG_HYP_SUBST_UNEQUAL
public static final ErrorCode ERRMSG_RPN_VERIFY_AS_PROOF_FAILURE
public static final ErrorCode ERRMSG_PROOF_STACK_UNDERFLOW
public static final ErrorCode ERRMSG_PROOF_ABS_MAX_RETRY_EXCEEDED
public static final ErrorCode ERRMSG_DERIV_STEP_PROOF_FAILURE
public static final ErrorCode ERRMSG_RPN_TO_FORMULA_CONV_FAILURE
public static final ErrorCode ERRMSG_BOGUS_PROOF_LOGHYP_STMT
public static final ErrorCode ERRMSG_LOGHYP_STACK_DEFICIENT
public static final ErrorCode ERRMSG_FINAL_STACK_ENTRY_UNEQUAL2
public static final ErrorCode ERRMSG_NO_DERIV_STEPS_CREATED
public static final ErrorCode ERRMSG_STACK_SIZE_MISMATCH_FOR_STEP_HYPS
public static final ErrorCode ERRMSG_PROOF_STEP_RANGE
public static final ErrorCode ERRMSG_PROOF_NULL
public static final ErrorCode ERRMSG_PROOF_SQUISH_FAIL