Support infix functions and predicates with user-defined priorities
- Nov 23, 2022
-
-
Katja Goltsova authoredefc4b4a2
-
Katja Goltsova authoreddc41ccb8
-
Katja Goltsova authored4448bf98
-
Katja Goltsova authored
* Parser constructor takes the priority list of infix functions with the function's associativity (left-, right- or not associative), of infix predicates (any function has higher priority than any predicate: x + y < z), and the information about synonymous labels. * The pretty printer is now also a class whose constructor takes an instance of parser. * The default parser and printer are FOLParser and FOLPrinter. The only infix operation they handle is the equality predicate. They are also not aware of any synonyms. * In all places where the parser or printer object were used, the corresponding default is now used.
e485cc82 -
Katja Goltsova authored
To do so, introduce Termula type, which doesn't distinguish function application from predicate application. A string is parsed into a Termula, which then gets converted into a Formula or a Term, with the appropriate checks. Telling apart infix function and predicate application in LL1 parser does not appear feasible: consider two inputs, 1) (x + y) < z and 2) (a /\ b) /\ c. The parser is parsing a formula and observes '(' as the first token. It can either mean a subformula or a subterm with an infix operator, and this conflict seems fundamental. With the introduction of Termula, '(' corresponds to a start of subtermula, and the rest of the inputs is parsed either into a connector termula or an (infix) application termula.
d4443670 -
Katja Goltsova authoredd7454fd0
-