Fable tptp parser fixes#882
Open
quickbeam123 wants to merge 22 commits into
Open
Conversation
In endFormula(), when the token following an already-built formula is
'=' or '!=' (FOOL/TFX equality between boolean terms), the pending
binary connective `con` (and its conReverse flag, for =>/&/|) was
popped and then simply discarded, and no END_FORMULA state was
re-pushed. As a consequence:
- the connective and its other argument were silently dropped, leaving
the orphaned formula on _formulas and a stray -1 on _connectives, and
- connective parsing never resumed after the equality atom, so any rest
of the formula was silently swallowed by endFof's skipToRPAR().
Both directions lost parts of the input without any error:
printf 'tff(dp, type, p: $o).
tff(dq, type, q: $o).
tff(dr, type, r: $o).
tff(a, axiom, p & (q) = r).' | ./vampire --mode output
before: q = r ("p &" dropped!)
after: p & ((q = r))
printf 'tff(dp, type, p: $o).
tff(dr, type, r: $o).
tff(ds, type, s: $o).
tff(a, axiom, (p) = r & s).' | ./vampire --mode output
before: p = r ("& s" dropped!)
after: ((p = r)) & s
The fix restores the pending connective state (con, and conReverse for
IMP/AND/OR) and re-pushes END_FORMULA beneath the equality-parsing
states, so once the equality atom is built, parsing continues exactly
as after any simple formula.
Note: endHolFormula() has a similar-looking T_EQUAL/T_NEQ branch that
also drops `con`; the legacy HOL code path is left untouched here.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The lexer counted a line break for '\n' and '\r' independently, both in
the main whitespace skipper and inside the block-comment scanner, so
files with Windows CRLF line endings reported doubled line numbers in
parse errors:
printf 'fof(a1, axiom, p).\r\nfof(a2, axiom, q).\r\nfof(a3, axiom, r & ).\r\n' \
| ./vampire --mode output
before: parse error in "<stdin>", line 5: formula or term expected
after: parse error in "<stdin>", line 3: formula or term expected
Now a CRLF pair counts as a single line break; a lone \r (old Mac
style) still counts as one, and pure-LF files are unaffected. Since
detecting CRLF requires peeking one character ahead, the affected spots
must consume exactly the examined characters via shiftChars() rather
than clearing the whole buffer with resetChars(), which would eat the
peeked-at character (e.g. after a lone \r).
(The %-comment scanner counts only '\n' and was already correct.)
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The block-comment scanner, upon seeing a '*', read and unconditionally
consumed the following character while checking for '/'. If that
character was itself a '*', it could then no longer start the closing
'*/', so the comment silently swallowed the rest of the file:
printf '/* c1 */ fof(a1, axiom, p). /* c2 **/ fof(a2, axiom, q).' \
| ./vampire --mode output
before: only a1 is parsed; a2 is silently lost in the comment
after: both a1 and a2 are parsed
The fix consumes the character after '*' only when it is the closing
'/'; otherwise it is left in the buffer and re-examined from the top of
the loop. This also fixes a newline immediately following a '*' inside
a comment previously being consumed without counting, e.g.:
printf '/* c *\n*\n*/ fof(a1, axiom, r & ).' | ./vampire --mode output
now correctly reports the parse error on line 3
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Same defect class as the previous endFormula() fix, in the THF path:
when endHolFormula() had popped a pending connective `con` and then saw
'=' or '!=', it discarded `con` (and its conReverse flag) and pushed no
continuation state, silently losing parts of the input:
printf 'thf(dp, type, p: $o).
thf(dq, type, q: $o).
thf(dr, type, r: $o).
thf(a, axiom, p & (q) = r).' | ./vampire --mode output
before: q = r ("p &" dropped!)
after: ((q = r)) & p
Additionally, a pending application was dropped the same way, because
the branch equated the bare arguments instead of first completing the
application:
printf 'thf(df, type, f: $o > $o).
thf(dx, type, x: $o).
thf(dy, type, y: $o).
thf(a, axiom, f @ x = y).' | ./vampire --mode output
before: x = y ("f @" dropped!)
after: ((f @ x)) = y
The fix mirrors endFormula(): for con == APP, first finish building the
application (END_APP) and reconsider the not-yet-consumed '='/'!=' with
the enclosing connective; otherwise restore the pending connective
state and re-push END_HOL_FORMULA beneath the equality-parsing states,
so parsing continues after the equality atom is built.
Known remaining (pre-existing) THF deviations, postponed for now:
- the RHS of an equality is parsed greedily, so '(p) = r & s' groups as
'p = (r & s)' whereas THF mandates '((p) = r) & s' (equality binds
tighter than binary connectives);
- an unparenthesized application after a binary connective, e.g.
'p & f @ x', is rejected with "Non-boolean term f used in a formula
context" (the term-to-formula conversion fires before '@' is seen).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Function applications f(...) and tuples [...] share the ARGS/END_ARGS
parsing machinery, and endArgs() accepted ')' and ']' interchangeably
as the argument-list terminator. Malformed input was thus silently
accepted:
printf 'fof(a, axiom, p(a]).' | ./vampire --mode output
before: accepted, parses as p(a)
after: parse error: ) expected after an end of a term (text: ])
printf 'tff(da, type, a: $int).
tff(db, type, b: $int).
tff(x, axiom, [a, b) = [a, b]).' | ./vampire --newcnf on --mode output
before: accepted, parses as [a, b] = [a, b]
after: parse error: ] expected after an end of a term (text: ))
The two places in funApp() that push the ARGS state now also record the
expected closing delimiter on the _tags stack (T_RPAR for f(, T_RBRA
for [), and endArgs() pops and checks it when the closing token
arrives. Since parsing is properly nested, this preserves the LIFO
discipline _tags shares with the TAG states.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
readSort() detected an applied (polymorphic) type constructor by
peeking at the raw next character (getChar(0) == '('), so any
whitespace or comment between the constructor name and the opening
parenthesis defeated the detection and valid input was rejected:
printf 'tff(t1, type, list: $tType > $tType).
tff(t2, type, nil: !>[A: $tType]: list (A)).' | ./vampire --mode output
before: User error: Undeclared type constructor list/0
after: accepted, same as list(A)
TPTP allows arbitrary whitespace between tokens, and the term parser
(funApp) already uses a token peek for the same purpose and accepts
'p (a)'. readSort() now does the same: getTok(0).tag == T_LPAR.
Also, a malformed sort application such as list(A B) now raises a
proper parse error instead of a debug-only ASSERTION_VIOLATION (which
in release builds would have fallen through into an infinite loop).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The TPTP grammar has name ::= atomic_word | integer, and fof()/tff()
accordingly accept integers as unit names. The formula_selection list
of an include() directive, however, only accepted atomic words, so
selecting a unit with an integer name was a parse error:
cd $(mktemp -d)
printf 'fof(27, axiom, p).
fof(named, axiom, q).
fof(28, axiom, r).' > inc.p
printf "include('inc.p', [27, named]).
fof(main, axiom, m)." > main.p
./vampire --mode output main.p
before: parse error in main.p, line 1: formula name expected (text: 27)
after: units p, q and m are parsed (r correctly filtered out)
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
fof()/tff() set _containsConjecture as soon as they saw the
conjecture/question role, but endFof() may afterwards discard the unit
because of an include() directive's formula_selection list. A filtered
conjecture thus still influenced the SZS status classification:
cd $(mktemp -d)
printf 'fof(ax, axiom, p).
fof(c, conjecture, q).' > inc.p
printf "include('inc.p', [ax]).
fof(negp, axiom, ~p)." > main.p
./vampire main.p
before: % SZS status ContradictoryAxioms for main
(the flag claimed a conjecture exists, so the refutation not
using it was classified as contradictory axioms)
after: % SZS status Unsatisfiable for main
(the parsed problem contains no conjecture)
The flag is now set in endFof(), based on _lastInputType, only after
the unit has passed the allowedNames filter. Units whose role is
conjecture but which fall inside a vampire(model_check, model_start)
section keep being treated as model definitions, as before.
Also clean up the filtered-unit early return in endFof(): delete the
already-allocated SourceRecord (SourceRecord gains a virtual destructor
for this) and clear _curQuestionVarNames, whose stale entries would
otherwise pollute the variable-name map of the next parsed question.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
endIte() called Term::createITE() with the then-branch sort before
verifying that the else branch has the same sort, so on a mismatch a
malformed special term was constructed (and leaked) before the check
fired. Term::createITE performs no validation of its own today, so the
user-visible behavior is unchanged, but any future assertion inside
createITE would have preempted the intended friendly error. Now both
sorts are computed and compared first:
printf 'tff(dp, type, p: $o).
tff(a, axiom, $ite(p, 1, $true) = 2).' | ./vampire --mode output
(unchanged) User error: sort mismatch in the if-then-else
expression: 1 has the sort $int, whereas $true has the sort $o
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
findLetSymbol() took the scope (a Stack of names paired with symbol
references, containing std::strings and TermStacks) by value, and the
enclosing overload additionally iterated _letSymbols with
Stack::TopFirstIterator, whose next() also returns elements by value.
Every function/predicate application parsed inside a $let body thus
paid a deep copy of each enclosing scope.
Purely mechanical change: pass LetSymbolName and LetSymbols by const
reference and iterate the scope stack with Stack::ConstRefIterator
(same top-first order, but next() returns a const reference).
No behavior change; e.g.
printf 'tff(a, axiom, $let(f: $int > $int,
f(X) := $sum(X, 1), f(3)) = 4).' | ./vampire --mode output
parses identically to before.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A batch of small, behavior-neutral cleanups found during the parser
audit:
- skipToRBRA() reported ") not found" on EOF; it looks for ']'.
- tff()'s error for the unsupported roles assumption/unknown was cut
short: "Unsupported unit type 'unknown" -- now matches fof()'s
"Unsupported unit type 'unknown' found".
- unitList()'s error message did not mention tff() and thf() even
though both are accepted:
printf 'foo(a, axiom, p).' | ./vampire --mode output
now: cnf(), fof(), tff(), thf(), vampire() or include() expected
- fof() and tff() contained a dead 'tok = getTok(0);' self-assignment
right before name() (which fetches the token itself).
- createPredicateApplication()'s $distinct short-circuit for fewer than
two arguments returned without popping the argument off _termLists;
harmless (all stack operations are top-relative), but the residue
accumulated. '$distinct(c)' still parses as $true:
printf 'fof(a, axiom, $distinct(c) & p).' | ./vampire --mode output
- printStates()/printInts() were declared in TPTP.hpp under VDEBUG but
defined and used nowhere; declarations removed.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
endHolFormula() built a quantified/lambda formula over its body as soon
as the binder connective was popped, without looking at the next token.
A following '='/'!=' was therefore attached outside the binder,
although per the TPTP BNF (v9.2.1.4) the body of a binder is a
<thf_unit_formula>, which includes equalities (<thf_defined_infix>).
Real problems (e.g. Isabelle exports) rely on this reading:
printf 'thf(t1, type, tree_b: $tType).
thf(t2, type, e_b: tree_b).
thf(t3, type, heapIm229596387mpty_b: tree_b > $o).
thf(fact_0_hs__is__empty__def,axiom,
( heapIm229596387mpty_b
= ( ^ [T: tree_b] : T = e_b ) ) ).' | ./vampire --mode output
before: read as (^[T]: T) = e_b, dying with
"Cannot create equality between terms of different types"
after: heapIm...mpty_b = (^[X0 : tree_b] : ((X0 = e_b))),
identical to the explicitly parenthesized
^ [T: tree_b] : ( T = e_b )
The same held for the other binders, with especially confusing errors
for quantified boolean variables, where the misreading also moved the
variable out of its own scope:
printf 'thf(a, axiom, ! [X: $o] : X = X).' | ./vampire --mode output
before: read as (![X]: X) = X, where the second X is free and
defaults to $i: "Cannot create equality between terms of
different types: X0 is $i, ![X0 : $o] : X0 is $o"
after: ![X0 : $o] : ((X0 = X0))
The fix: when the popped connective is FORALL/EXISTS/LAMBDA and the
next token is '='/'!=', defer building the binder -- re-push the binder
connective and parse the equality first, using the same state pattern
as the connective-restoring '='/'!=' handling elsewhere in this
function. The bound variables stay bound while the equality's RHS is
parsed (UNBIND_VARIABLES is only scheduled when the binder is finally
built), as the equality lies inside the binder's scope. This also
composes with parenthesized applications:
^ [T: tree_b] : (g @ T) = e_b now yields ^[T]: ((g @ T) = e_b).
Deliberate behavior change: input that meant (^[X]: X) = y but omitted
the parentheses around the lambda was relying on the nonconforming
parse and is now read per the BNF.
Pre-existing and unchanged (postponed): an unparenthesized application
as a binder body, e.g. ^ [T: tree_b] : g @ T, still misparses as
(^[T]: g) @ T (the BNF requires the parentheses here anyway).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
holFormula() dispatches the tokens of binary connectives to holTerm()
so that sections like f @ (&) parse as applications of the internal
connective proxies, and holTerm()/convert() handle T_XOR (vXOR), but
T_XOR was missing from holFormula()'s dispatch list:
printf 'thf(df, type, f: ($o > $o > $o) > $o).
thf(a, axiom, f @ (<~>)).' | ./vampire --mode output
before: parse error: formula or term expected (text: <~>)
after: f @ <~>, analogous to f @ (&)
p <~> q as a formula is unaffected.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
holFormula()'s T_RPAR case exists for the (~) connective-as-term
section and merely asserted that the pending connective is NOT. On
malformed input such as an empty pair of parentheses, debug builds
died on the assertion, while release builds silently popped whatever
connective was pending and fabricated a vNOT term, desyncing the
parser's connective stack:
printf 'thf(df, type, f: ($o > $o) > $o).
thf(a, axiom, f @ ()).' | ./vampire --mode output
before: assertion violation (debug) / silent nonsense (release)
after: parse error: formula or term expected (text: ))
The (~) section itself keeps working:
printf 'thf(df, type, f: ($o > $o) > $o).
thf(a, axiom, f @ (~)).' | ./vampire --mode output
(unchanged) f @ ~
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The tokens ?* (T_THF_QUANT_SOME) and !> (T_TYPE_QUANT, outside type
declarations) fell through to holFormula()'s generic "formula or term
expected" parse error, giving no hint that the constructs are simply
not supported. They now get dedicated messages, in the style of the
existing one for the choice/description operators @+/@-:
printf 'thf(a, axiom, ?* [X: $o] : X).' | ./vampire --mode output
now: At the moment Vampire HOL cannot parse the ?* quantifier
printf 'thf(a, axiom, !> [A: $tType] : $true).' | ./vampire --mode output
now: At the moment Vampire HOL only supports type quantification
(!>) in type declarations, not in formulas
!> in type declarations is unaffected.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Behavior-neutral cleanups in the HOL parsing functions: - holTerm(): the T_BOOL_TYPE/T_DEFAULT_TYPE case called resetToks() a second time; the function already consumes the token right after fetching it at the top. (These cases are in fact unreachable, since holFormula() never dispatches those tokens to HOL_TERM; verified that e.g. 'f @ $o' errors identically before and after.) - endHolFormula(): the comment above the term-to-formula conversion claimed "APP and LAMBDA are the only connectives that can take terms"; rewritten to describe what the condition actually encodes (formula connectives below HOL_CONSTANTS_LOWER_BOUND need formulas; LAMBDA/APP/PI/SIGMA and the -1 context may operate on terms). - endHolFormula(): removed the unreachable 'case -2:' from the first connective switch; con == -2 is handled by the early return at the top of the function. - higherPrecedence(): the doc claimed "strictly higher", but APP is reported as higher than APP itself; documented that this is what makes application (@) left-associative. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Per the TPTP BNF, both sides of a THF equality are <thf_unitary_term>s
and an equality (<thf_defined_infix>) is a <thf_unit_formula>, i.e. the
operand granularity at which binary connectives attach. The parser
however parsed the right-hand side of '='/'!=' as a full formula,
greedily absorbing any following binary connectives:
printf 'thf(dp, type, p: $o).
thf(dr, type, r: $o).
thf(ds, type, s: $o).
thf(a, axiom, (p) = r & s).' | ./vampire --mode output
before: p = (r & s)
after: ((p = r)) & s
This was not just cosmetic: the two readings are semantically different
(e.g. p=false, r=true, s=false makes '(p = r) & s' false but
'p = (r & s)' true), so on BNF-conforming input Vampire could attack a
different formula than other systems. Note that this deliberately
changes the reading of common unparenthesized syntax:
thf(a, axiom, p = q & r).
before: p = (q & r)
after: (p = q) & r (per the BNF; parenthesize for the old one)
Mechanism: the two places in endHolFormula() that schedule parsing of
an equality RHS used the pseudo-connective -1 ("no pending connective",
which continues consuming connectives). They now push a new file-local
sentinel EQ_RHS (-3) instead, which endHolFormula() treats exactly like
-1 except at a binary logical connective token, where it returns
without consuming the token, leaving it to the enclosing context.
Concretely, EQ_RHS is (a) excluded from the term-to-formula conversion
(the RHS may be of any sort), (b) a no-op in the connective dispatch
switches like -1, (c) the new early return before connective
continuation, and (d) exempted from higherPrecedence() (only reachable
there with '@', which binds tighter than '=' and is still absorbed via
the connective push-back).
Behavior verified unchanged for: parenthesized RHS 'p = (r & s)';
chained 'p = q = r' (still right-associated); applications on either
side, 'f @ x = y' and 'p = f @ x'; binder bodies '^[T]: T = e_b' and
'! [X: $o]: X = X'. Newly correct groupings include:
p = f @ x & q -> (p = (f @ x)) & q
f @ x = y & q -> ((f @ x) = y) & q
p = q <=> r -> (p = q) <=> r
p = q & r = s -> (p = q) & (r = s)
! [X: s]: X = c & p -> (! [X: s]: (X = c)) & p
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… binder bodies
endHolFormula() finished the pending connective as soon as one unitary
item of its argument had been parsed, without checking whether an
application (@) -- which binds tighter than all formula connectives and
binders -- follows. Consequences:
- a binder closed over just the first unitary item:
printf 'thf(t1, type, tree_b: $tType).
thf(tg, type, g: tree_b > tree_b).
thf(tq, type, q: tree_b > tree_b).
thf(a, axiom, q = (^ [T: tree_b] : g @ T)).' | ./vampire --mode output
before: read as (^[T]: g) @ T, failing with
"unquantified variable detected" (T escaped its scope)
after: q = (^[X0 : tree_b] : ((g @ X0)))
- for quantifiers and unary/binary connectives, the argument term was
converted to a formula before the '@' was seen, giving a confusing
sort error:
printf 'thf(df, type, f: $o > $o).
thf(dx, type, x: $o).
thf(dp, type, p: $o).
thf(a, axiom, p & f @ x).' | ./vampire --mode output
before: User error: Non-boolean term f of sort ($o > $o) is used
in a formula context
after: (f @ x) & p
(likewise '! [X: tree_b] : p @ X', 'p => f @ x', '~ f @ x', ...)
The fix: when the popped connective is a formula connective
(NOT/AND/OR/IMP/IFF/XOR/FORALL/EXISTS, i.e. below
HOL_CONSTANTS_LOWER_BOUND) or LAMBDA, the last parsed item is a term,
and the next token is '@', defer the connective: re-push it and open an
EQ_RHS context (introduced in the previous commit) which absorbs the
whole application chain -- and, via its existing '='/'!=' handling, a
trailing equality -- and stops at binary logical connectives. The '@'
token is not consumed by the deferral itself. For IMP/AND/OR the
conReverse flag has not been popped at this point and simply stays on
_bools for the reconsideration. The combination makes the fully
unparenthesized Isabelle-style form work end to end:
thf(a, axiom, heap = ( ^ [T: tree_b] : f @ T = e_b ) ).
now: heap = (^[X0 : tree_b] : (((f @ X0) = e_b)))
Strictly, the TPTP BNF requires parentheses around an application used
as a <thf_unit_formula>, so all newly accepted inputs were previously
errors or misparses; no valid old readings change. Verified unchanged:
the whole equality-grouping matrix of the previous commit, application
chains at top level (f @ x & y), binder bodies with and without
equalities, and the (~) / (&) sections.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Per the TPTP BNF (v9.2.1.4), '~ p = q' is not legal THF at all: a
prefix-unary formula '~ p' is not a <thf_unitary_term> (so it cannot be
an equality side) and a bare <thf_defined_infix> 'p = q' is not a
<thf_preunit_formula> (so it cannot be the argument of '~'); conforming
input must write '(~ p) = q' or '~ (p = q)'. Vampire leniently accepts
the unparenthesized form, and until now invented the reading
'(~ p) = q' -- which contradicts the reading the BNF *mandates* for the
identical text in FOF/TFF (where 'p = q' is an atomic formula and
'~ (p = q)' is the only derivation), as well as the
equality-binds-tighter principle applied in the preceding commits.
printf 'thf(dp, type, p: $o).
thf(dq, type, q: $o).
thf(a, axiom, ~ p = q).' | ./vampire --mode output
before: (~ p) = q
after: ~ ((p = q)) (TFF parses the same text as p != q)
The fix simply adds NOT to the =/!= deferral in endHolFormula() that
already handles the binders: negation is deferred, the equality is
parsed first (its RHS in the EQ_RHS context, stopping at binary
connectives), and the negation is applied to the finished atom. Hence
also: '~ p != q' -> ~(p != q); '~ ~ p = q' -> ~(~(p = q));
'~ p = q & r' -> (~(p = q)) & r.
Explicitly parenthesized inputs are unaffected: '(~ p) = q' keeps the
old reading, '~ (p = q)' keeps working; likewise '~ p', '~ p & q',
'p = ~ q', '~ f @ x' and '! [X: $o] : ~ X = X' (now ![X]: ~(X = X)).
A follow-up task will add once-per-run warnings for all the lenient
readings of non-conforming input, including this one.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The preceding commits made the parser accept several forms that are not
legal per the TPTP BNF, silently inventing a (documented) reading. Such
leniency is now admitted to the user: the first time each kind of
non-conformity is encountered in a parser run, a warning is printed
with the file, line, an explanation of the chosen reading, and a note
that further occurrences of that kind will not be reported in this run.
Four kinds are distinguished (enum NonConformity, with a per-kind
once-per-run flag and the helper nonConformityWarning()):
1. NC_NOT_APPLIED_TO_EQUALITY: '~ p = q' read as '~ (p = q)'
2. NC_UNPARENTHESIZED_APPLICATION: 'p & f @ x' read as 'p & (f @ x)',
'^[X]: f @ X' as '^[X]: (f @ X)'
3. NC_NON_UNITARY_EQUALITY_ARGUMENT: 'p = ~ q' read as 'p = (~ q)',
'g = ^[X]: t' as 'g = (^[X]: t)'
4. NC_CHAINED_EQUALITY: 'p = q = r' read as 'p = (q = r)'
Detection points: (1) the NOT case of the =/!= binder deferral;
(2) the T_APP deferral block; (3) holFormula() seeing '~' or a binder
while the pending connective is the equality-RHS sentinel;
(4) endHolFormula() seeing '='/'!=' while the pending connective is the
equality-RHS sentinel.
For (4) to be sound, the application-absorption context introduced with
the T_APP deferral can no longer share the EQ_RHS sentinel: in
'p & f @ x = y' the '=' after the absorbed application is a first
equality, not a chained one. It gets its own sentinel APP_ABSORB (-4),
identical to EQ_RHS in all handling (shared via the tightContext()
helper) except at '='/'!='. While splitting this, the T_APP deferral
condition was also fixed to exclude the tight contexts themselves: it
previously matched APP_ABSORB (-4 passes 'con < HOL_CONSTANTS_LOWER_BOUND
&& con != -1 && con != EQ_RHS'), so 'p & f @ x @ y' would have
re-deferred without consuming '@' forever; it now parses as
'p & (f @ x @ y)'.
Example (each kind present twice; exactly four warnings, on the first
occurrence of each):
printf 'thf(dp, type, p: $o).
...
thf(a1, axiom, ~ p = q).
thf(a2, axiom, ~ q = p).
thf(b1, axiom, p & f @ x).
...' | ./vampire --mode output
% WARNING: non-conforming THF input in "<stdin>", line 7: '~'
applied to an unparenthesized (in)equality is not legal THF;
reading '~ s = t' as '~ (s = t)' (further occurrences of this kind
will not be reported in this run)
... (three more, one per kind)
Conforming input (parenthesized variants, equalities as binder bodies,
'(p) = r & s', ...) produces no warnings, and all invented readings are
unchanged.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
addUninterpretedConstant() unconditionally routed constants named vAND,
vOR, vIMP, vIFF, vXOR and vNOT to Vampire's internal HOL connective
proxy symbols, and TPTP::addFunction() did the same for vPI/vSIGMA.
These names are synthesized by the THF parsing functions
(holTerm/holFormula) and only meaningful there, but the routing fired
for every input dialect, hijacking innocent user symbols:
printf 'fof(a, axiom, p(vAND) & p(vNOT)).' | ./vampire --mode output
before: User error: ... The sort $o > ($o > $o) of the intended
term argument vAND (at index 0) is not an instance of $i
after: p(vAND) & p(vNOT) (ordinary constants)
printf 'tff(dc, type, c: $i).
tff(dv, type, vPI: $i > $i).
tff(a, axiom, vPI(c) = c).' | ./vampire --mode output
before: User error: The sort $i of type argument c is not $tType
as mandated by TF1 (vPI resolved to the pi proxy)
after: c = vPI(c)
The SMT-LIB parser reaches the same code through
TPTP::addUninterpretedConstant when declaring 0-ary functions, so e.g.
(declare-const vAND Bool) was affected as well -- and on the proxy path
the `added` output parameter was left uninitialized.
The fix moves the routing out of the static addUninterpretedConstant()
into createFunctionApplication() (for the 0-ary vAND/../vNOT) and
guards the vPI/vSIGMA case in TPTP::addFunction(), both conditional on
_isThf, i.e. active exactly where the names are synthesized. THF
behavior is unchanged: the (&)/(~) connective sections and the
!!/?? pi/sigma constants parse as before (verified), and all 97 unit
tests pass.
Remaining known limitation (old AYB TODO, now next to the routing): in
THF mode these names still capture identically named constants coming
from the input; fixing that requires making the internal names
impossible to write in TPTP syntax, a deeper change also touching how
Kernel/Signature registers the proxy symbols under plain names.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Small TPTP inputs under checks/parse/, one or two per recent parser
fix, each with a header comment documenting the expected behavior; the
corresponding commit messages hold the full stories. Three new sanity
helpers, in the spirit of check_exact_output but robust against
irrelevant output drift (e.g. symbol-table indices in --mode output):
- check_output_contains <substring> <args>: substring must appear in
stdout (positive tests, run with --mode output);
- check_output_contains_once: additionally exactly once (used for the
once-per-run non-conformity warnings);
- check_rejected: same grep, but named for tests where the expected
output is an error message. Parse errors and user errors go to
stdout, so run_vampire's stderr trap does not trip on them. These
tests pass --input_syntax tptp explicitly, since the auto mode
retries a failing TPTP parse as SMT-LIB and garbles the message.
The files and the fixes they exercise:
- eq-precedence.p =/!= after parenthesized formula (TFF/FOOL)
- crlf-line-numbers.p CRLF counted once (plus new .gitattributes
entry protecting its CRLF bytes)
- block-comment-star.p comments ending in '**/'
- mismatched-brackets.p p(a] rejected
- sort-app-space.p 'list (A)' with whitespace
- include-selection[-axioms].p integer names in formula selection
- include-filtered-conjecture.p filtered conjecture => Unsatisfiable,
via check_szs_status
- ite-sort-mismatch.p $ite branch sort error message
- bad-unit-kind.p unit-kind error message mentions tff/thf
- let-function-parse.p $let parsing
- thf-eq-truncation.p =/!= after formula/application (THF)
- thf-binder-eq.p equality inside binder bodies (the original
Isabelle heapIm... example verbatim)
- thf-eq-precedence.p equality binds tighter than connectives
- thf-app-absorb.p unparenthesized applications absorbed
(incl. the two-argument chain that once
risked an infinite loop) + kind-2 warning
- thf-not-eq.p '~ p = q' as '~ (p = q)'
- thf-non-conformity-warnings.p all 4 warning kinds, each twice,
each reported exactly once
- thf-xor-section.p (<~>) as a connective section
- thf-empty-parens.p 'f @ ()' rejected
- thf-quant-some.p, thf-type-quant-in-formula.p dedicated messages
for unsupported ?* and !>
- proxy-names.p vAND/vNOT/vPI as ordinary symbols in FOF/TFF
Verified: full 'checks/sanity build-debug/vampire' passes through the
whole parser section (the debug build then times out on the
pre-existing -t 1d arithmetic check DAT023_1.p, as it also does before
this branch; CI's release build is unaffected), all three helpers were
spot-checked to fail on wrong expectations, and every TPTP problem
referenced by sanity parses byte-identically to the pre-branch parser.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
I went on a parser fixing spree with Claude and this is the result.
Every commit is hopefully self-contained, so we don't need to accept all of them. And we could try to understand what's going on in each in isolation. (Rather than just reading the whole diff at once as we usually do.)
The commit messages usually contain little tptp inputs showcasing what's getting fixed. I could still ask to create some true tests, likely in sanity.
The code base is likely getting more complex thanks to this. But I couldn't say I understood the parser as a whole before, so the situation is not changing too much for me.
Obviously, we need to test this thoroughly. It might be that new strange things will start popping up due to us being more correct! In the last commit, I asked it to start issuing warnings for some parses we allow but actually should not according to the BNF.
Most importantly, this should fix #553 ;)