search

epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Parser failing on single argument Or/And formula #60

Closed lighthea closed 2 years ago

lighthea commented 2 years ago

When printing a ConnectorFormula (I tested And and Or) with a single argument, the parser fails with error (this does not seems to be a problem with a no argument ConnectorFormula): 

lisa.utils.Parser$PrintFailedException: Printing of ConnectorFormula(And,List(PredicateFormula(SchematicPredicateLabel(phi,0),ArraySeq()))) failed unexpectedly

for the formula phi() |- phi(). Minimal code to reproduce : 

 val phi = SchematicPredicateLabel("phi", 0)
 println(Printer.prettyFormula(sequentToFormula((phi()) |- (phi()))))
cache-nez commented 2 years ago

I am not entirely sure that it's the parser's job to print and / or connector formulas with 1 arguments, because there is never a string that is parsed into such formulas. #65 proposes one parser-level solution but it has side effects (see tests where Implies(and(a), or(a)) is printed as (a) => (a) rather than a => a).

On a separate point, why is the example converted into an and of one argument at all rather than being a predicate formula with no arguments?

lighthea commented 2 years ago

Sorry I incriminated the parser only because of the error. It is surely the printer that fails here. For your last question, sequentToFormula definition transforms a sequent into a formula by taking the intersection of the left side implying the union of the right side not accounting for the number of arguments.

cache-nez commented 2 years ago

The parser and the printer are basically the same thing (there is some freedom at unlexing (tokens -> strings) level but besides we are very limited in what unparseable behaviours we can support in the printer) so I meant to use them interchangeably. An alternative to handling the issue at the parser/printer level (which is done in #65) would be a normalization phase that precedes printing.