Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

HOL Parsing Errors #645

Open
joe-hauns opened this issue Jan 15, 2025 · 2 comments
Open

HOL Parsing Errors #645

joe-hauns opened this issue Jan 15, 2025 · 2 comments

Comments

@joe-hauns
Copy link
Contributor

I found a class of parsing errors for thf problems. Some examples of this:

> vampire --input_syntax tptp $TPTP/Problems/SYO/SYO898^9.p
User error: Undeclared type constructor mworld/0 (detected at or around line 38)

> vampire --input_syntax tptp $TPTP/Problems/SEU/SEU976^5.p
User error: Undeclared type constructor a/0 (detected at or around line 35)

> vampire --input_syntax tptp $TPTP/Problems/SEV/SEV217^5.p
User error: Undeclared type constructor c/0 (detected at or around line 38)

> vampire --input_syntax tptp $TPTP/Problems/LCL/LCL942^2.p
User error: Undeclared type constructor mworld/0 (detected at or around line 38)

> vampire --input_syntax tptp $TPTP/Problems/SYO/SYO492^6.p
User error: Undeclared type constructor mu/0 (detected at or around line 62)

> vampire --input_syntax tptp $TPTP/Problems/SWW/SWW971^5.p
User error: Undeclared type constructor mworld/0 (detected at or around line 39)

> vampire --input_syntax tptp $TPTP/Problems/SEV/SEV133^5.p
User error: Undeclared type constructor atype/0 (detected at or around line 35)

> vampire --input_syntax tptp $TPTP/Problems/SEV/SEV211^5.p
User error: Undeclared type constructor a/0 (detected at or around line 35)

> vampire --input_syntax tptp $TPTP/Problems/SYO/SYO463^3.p
User error: Undeclared type constructor mu/0 (detected at or around line 63)

> vampire --input_syntax tptp $TPTP/Problems/DAT/DAT334^21.p
User error: Undeclared type constructor mworld/0 (detected at or around line 39)

I had a look and I think the issue is the use of Signature::addFunction instead of Signature::addTypeCon here.
This could be fixed easily but there is some witchery going on in TPTP::addUninterpretedConstant which I'm not quite sure how to nicely resolve.
I will have a look at this at some point as I'm planning some more tidying and optimization of the signature in general. But that propably won't happen too soon. So if someone feels like it I'm happy if they resolve it :)
For now i'll just add this as a "known issue". Practiaclly it doesn't make any difference right now anyways because if we fix the parsing we will die with the error message This version of Vampire is not yet HOLy anyways.

@joe-hauns
Copy link
Contributor Author

joe-hauns commented Jan 15, 2025

Thinking about it for a bit I think the special casing "vAND" & friends doesn't need to happen for type constructors anyways, so the fix should be quite simple. just pushed a branch thf-parser-fix. Does this look alright @ibnyusuf ?

@ibnyusuf
Copy link
Member

This looks reasonable, but I'm still struggling to understand why this wouldn't cause many more parsing errors? If we are storing every type constructor as a function symbol, I would expect many more such errors? I'll try and look into this a little more deeply when I have some time.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants