2020-02-07 22:56:54 (GMT)
Guillaume Bury, who wrote archsat (a solver) and dolmen (a library for parsing) among other things, would like the native Zipperposition format to get simpler, by forbidding quantifiers that are not type annotated. I think it's reasonable to ask for that, and we do have a big-ish development using Zipperposition for B set theory that specifies all types this way. It would simplify the parser a bit, and the type inference quite a bit, I think.
In parallel, I think it'd be nice to have the pretty-printer always display type arguments. I'm not sure if y'all deal with polymorphic problems regularly, but whereas terms are smaller when types are omitted, it's also less clear what is going on. There is an option for printing types but I think the default could be reversed, and an option provided to hide types. Anyone has objections to that?
2020-02-08 17:44:6 (GMT)
I've just pushed this change on master; one can hide type arguments with --hide-ty-args if required. I think displaying type arguments is the sane default.
2020-02-15 15:4:57 (GMT)
As said by @Simon Cruanes , the dolmen parser library could be useful. Great care was taken to write parsers that conform as much as possible to the specification of each language. For more information, you can look at the repo , the documentation for the parsing library, the small tutorial , or simply ask me, ^^
Additionally, I've just pushed an experimental LSP server implemented using dolmen, you can take a look at its documentation .
2020-02-15 20:22:40 (GMT)
The LSP server is pretty cool, I've already started using it. Its support for .zf files is a bit imperfect for now, but it works well for SMT-Lib 2.6.
2020-02-15 20:49:29 (GMT)
So maybe we could use this in Zipperposition to parse TPTP more reliably?
2020-02-15 21:15:58 (GMT)
That's the idea indeed. Also it would make it possible to parse SMTLIB 2.6 directly, which is full of interesting problems (although none/few of them involve HO at the moment, afaik).
We'd keep Zipperposition's current typechecker, though, this is purely for parsers.