HOL Parsing Errors

[joe-hauns]

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]

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]

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.