search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
282 stars 49 forks source link

parser fixes, thanks to Joe #558

Closed MichaelRawson closed 3 months ago

MichaelRawson commented 3 months ago

See #542. Fix some of the crashes reported there.

  1. When creating a tuple sort, we should call AtomicSort::create, not Term::create. I think it was probably fine data-wise, but we fail an assertion.
  2. We catch USER_ERRORS and wrap them as PARSE_ERRORS with a line number. I'm not sure how useful this is and it means we can't distinguish between "we parsed this but can't do anything with it" (e.g. HOL + theories), and "syntax error". Don't do that.
  3. Some PARSE_ERRORS should be USER_ERRORS.
quickbeam123 commented 3 months ago

Could we somehow propagate the lineNumber() even with the USER_ERRORs?

MichaelRawson commented 3 months ago

Right, this is what we lose - we can just add a field to UserErrorException, but I'm not sure I see the value. If e.g. the user supplies assumptions or mixes HOL and theories, it doesn't really matter where exactly.

quickbeam123 commented 3 months ago

The value is in being able to say "You are doing something stupid >AROUND HERE<." which is more informative than "You are doing something stupid in this 5 MB file of yours."

Not saying the current way is the best solution, but could we have this PR without 2. and think about it a bit more?

MichaelRawson commented 3 months ago

Ah, I see - some of the USER_ERRORs are more like a SEMANTIC_ERROR. OK, let's add a field to UserErrorException, it should not be so hard.

MichaelRawson commented 3 months ago

Done.