First order formula parsers in Haskell (logic-TPTP and the one in Equinox)

[Ahn, Ki Yung]

Dear Daniel Schüssler and Koen Classen,

I've tried using both logic-TPTP and the parser in the Equinox theroem 
prover.  I wanted to list issues I had when I tried using the parsers.

logic-TPTP http://hackage.haskell.org/package/logic-TPTP is implemented 
with alex and happy, and it is very close to the specification to the 
TPTP syntax when you look at the happy source file.  So, I think it 
works very nice for the people who wants to work on source to source 
transformation from TPTP syntax.  It also comes with pretty printer and 
exporting to plain text TPTP syntax.  It seems to be tested against the 
TPTP problem set and also random testing with formulae generated from

One problem I had with logic-TPTP parser is about dealing with comments. 
The TPTP syntax specification states that comments can come in between 
any tokens.  Howerver, logic-TPTP assumes that it is only at the top 
level, and not in between the formlua.  As a result, it fails to parse 
such formulae, for example, the following one:

   fof(equality_reflexive, axiom,
         ! [X]  # for all X
         : X=X  # X is equal to itself
       ).

This is valid according to the TPTP syntax specification, and all the 
theorem provers I know (at least the ones in the TPTP world) accepts 
such formulae.

I believe that there is a reason Daniel's logic-TPTP keeps the comment 
since TPTP syntax specification also states that comment is not to be 
processed same as whitespace in case theorem prover implementation may 
use the content of the comment as extra information.  However, it is 
just not correct to reject valid formulae which contains comments inside.

For a quick fix, I would suggest either (1) provide another set of 
parsing functions parse' and parseFile' that ignores all comment (2) 
export the lexer so that the user can build such versions of parsing 
functions themselves which ignores all comment tokens.  (Maybe, in the 
long run, the happy syntax definition should allow comments between tokens?)


In contrast, the parser in Equinox 
http://www.cs.chalmers.se/~koen/folkung/ can parse the formulae above. 
It just seem to ignore all comments since Equinox internally does not 
make use of any comments.  However, the problem for me about the current 
parser implementation in Equinox is that it transforms the syntax tree 
into some normalized form.  For example the formula

     ! [X,Y] : ...

seem to be parsed as

    ! [X] : ! [Y] : ...

So, when one wants to maintain the original form during the
transformation the parser in Equinox would not be desirable for him.

--
Ahn, Ki Yung