Parse formula expressed as string. Returns pair of parsed formula and table which maps atomic proposition's name in formula to atomic propositon expressed as PropLogicFormula after parsing.

The format of formula should be one of $, i.e. no parentheses can be omitted. When atomic propositions are required to get parse result, if atomic proposition corresponds to name in formula exists in nameToAtomicFormulae, nameToAtomicFormulae[name] is used. Othwewise, new atomic propositions are generated. For more details, see runnable example.

Note that This procedure uses very naive parsing method and does not construct any AST.

Example:

import propositionalLogic
import tables
import sets
import sequtils
import strutils

let
  p = generateAtomicProp()
  q = generateAtomicProp()
  formula = "((!p) => (q | r))"
  nameToAtomicFormulae = {
    "p": p,
    "q": q,
  }.toTable
  (parsedFormula, newNameToAtomicFormulae) = formula.parse(nameToAtomicFormulae)
  idToName = newNameToAtomicFormulae.pairs().toSeq().mapIt(($(it[1].getId()), it[0]))

assert formula.replace(" ", "") == ($parsedFormula).multiReplace(idToName)
## atomic proposition corresponds to `r` is generated automatically.
assert newNameToAtomicFormulae.keys().toSeq().toHashSet() == @["p", "q", "r"].toHashSet()