Monadic Predicate Logic with Some Modal Operators

I have a new version of the monadic predicate logic program that I posted a while ago.  It has operators for possibility and necessity (<> and [], respectively).  They bind to sub-expressions the same way negation (~) does; they bind to the nearest existential or universal quantifier to the right, or, failing that, the nearest predication to the right, so <>Px&Py is equivalent to (<>Px)&(Py) but not <>(Px&Py).  <>x,Px&Py is equivalent to <>(x,Px&Py) but not (<>x,Px)&Py.  I'm posting it and its source code, now that I have written a parser that I'm not ashamed of.  The one downside is that it no longer supports the "old school" dot grouping.  If any one wants to use it, tell me and I'll add it back in.  If anyone uses this program at all, tell me!

• Download mpl.exe and some example logic files.
• Download the source code.