Fable tptp parser fixes - #882

Open

quickbeam123 wants to merge 23 commits into

fable-tptp-parser-fixes

Commits on Jul 17, 2026

Fix silent formula truncation at =/!= after a parenthesized formula

quickbeam123
and
claude
committed
06e98c3
Fix line numbers being counted twice for CRLF line endings

quickbeam123
and
claude
committed
42fe081
Fix block comments ending in '**/' never being closed

quickbeam123
and
claude
committed
338c77f
Fix silent truncation at =/!= in THF formulas (endHolFormula)

quickbeam123
and
claude
committed
c410342
Reject mismatched closing delimiters in argument lists

quickbeam123
and
claude
committed
db226aa
Allow whitespace between a type constructor and '(' in sort applications

quickbeam123
and
claude
committed
71555d8
Accept integer formula names in include() formula selection

quickbeam123
and
claude
committed
c7366a1
Do not count conjectures filtered out by include() formula selection

quickbeam123
and
claude
committed
15d38f9
Check $ite branch sorts before constructing the term

quickbeam123
and
claude
committed
dd01946
Avoid deep-copying $let scopes on every symbol lookup

quickbeam123
and
claude
committed
369575e
Parser cosmetics: error messages, dead code, stack hygiene

quickbeam123
and
claude
committed
bb5d2fd
Parse equalities inside THF binder bodies per the TPTP BNF

quickbeam123
and
claude
committed
d041420
Support (<~>) as a THF connective-as-term section

quickbeam123
and
claude
committed
2aa63eb
Reject empty () in THF instead of asserting / fabricating vNOT

quickbeam123
and
claude
committed
678247e
Explicit errors for ?* and !> in THF formula positions

quickbeam123
and
claude
committed
fb37eff
HOL parser cosmetics: dead code and misleading comments

quickbeam123
and
claude
committed
3d00c45
Make THF equality bind tighter than binary connectives on its RHS

quickbeam123
and
claude
committed
3829730
Absorb unparenthesized THF applications into connective arguments and binder bodies

quickbeam123
and
claude
committed
dbfaafe
Read THF '~ p = q' as '~ (p = q)', aligning with FOF/TFF

quickbeam123
and
claude
committed
5a502cc
Warn once per run about each kind of leniently accepted THF input

quickbeam123
and
claude
committed
04b4906

Commits on Jul 18, 2026

Do not capture user symbols named vAND, vNOT, ... outside THF

quickbeam123
and
claude
committed
f2c1a23
Add TPTP parser regression tests to checks/sanity

quickbeam123
and
claude
committed
49ae50d

Commits on Jul 25, 2026

Do not absorb '@' into binder bodies: a binder body is one thf_unit_formula

quickbeam123
and
claude
committed
f0288bf