Skip to content

Support infix functions and predicates with user-defined priorities

Viktor Kuncak requested to merge github/fork/cache-nez/infix-priority into main

Created by: cache-nez

  1. 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, (x + y) < z and (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.

  2. Turn the parser into a class, which takes in its constructor the information about synonymous names, infix function names with associativity information in decreasing order of priority, and infix predicate names in decreasing order of priority.

  3. Create the parser and printer for first order logic, which are not aware of any synonyms nor infix functions and know of only one infix predicate: equality. Use those instances wherever the parser or printer objects used to be used.

Fixes #75

Merge request reports