Merge pull request #28 from Azumabashi/support-parsing

Support parsing

src/propositionalLogic.nim

@@ -24,7 +24,8 @@ import
   propositionalLogic/evalUtils,
   propositionalLogic/interpretationUtils,
   propositionalLogic/simplification,
-  propositionalLogic/hashUtils
+  propositionalLogic/hashUtils,
+  propositionalLogic/parse
 
 # List of types/procs/iterators to be exported
 export
@@ -35,4 +36,5 @@ export
   isSat, getModels, isTautology, isContradiction, iff,
   Interpretation, interpretations, getModels, getNumberOfInterpretations,
   simplification,
-  hash
+  hash,
+  parse

src/propositionalLogic/constants.nim

@@ -11,6 +11,14 @@ proc isOperator*(x: string): bool =
   ## `false` otherwise.
   x == andSymbol or x == orSymbol or x == notSymbol or x == impliesSymbol
 
+proc isOperator*(x: char): bool =
+  ## Proc `isOperator`'s wrapper for `char`.
+  ($x).isOperator()
+
 proc isParen*(x: string): bool =
   ## Returns `true` is `x` is left paren or right paren, and `false` otherwise.
-  x == leftParen and x == rightParen
+  x == leftParen or x == rightParen
+
+proc isParen*(x: char): bool =
+  ## Proc `isParen`'s wrapper for `char`.
+  ($x).isParen()

src/propositionalLogic/parse.nim

@@ -0,0 +1,126 @@
+import constants
+import formulae
+import deques
+import strutils
+import algorithm
+import tables
+import sequtils
+import math
+
+proc toReversePolishNotation(formula: string): seq[string] =
+  var 
+    operatorLevelPairs: seq[(string, int)]
+    level = 0
+    i = 0
+
+  while i < formula.len:
+    var token = $(formula[i])
+    if token == leftParen:
+      level += 1
+    elif token == rightParen:
+      level -= 1
+    elif token.isOperator() or token == "=":
+      if token == "=":
+        i += 1
+        assert formula[i] == '>', "Unknown token: =" & formula[i]
+        token = "=>"
+      if operatorLevelPairs.len > 0 and operatorLevelPairs[^1][1] > level:
+        for operatorLevelPair in operatorLevelPairs.reversed:
+          result.add(operatorLevelPair[0])
+        operatorLevelPairs = @[]
+      operatorLevelPairs.add((token, level))
+    elif token != " ":
+      var j = i + 1
+      while j < formula.len and not (
+        formula[j] == '=' or isOperator(formula[j]) or isParen(formula[j])
+      ):
+        j += 1
+      result.add(formula[i..<j].strip())
+      i = j - 1
+    i += 1
+
+  for operatorLevelPair in operatorLevelPairs.reversed:
+    result.add(operatorLevelPair[0])
+
+proc parse*(
+  formula: string, 
+  nameToAtomicFormulae: Table[string, PropLogicFormula]
+): (PropLogicFormula, Table[string, PropLogicFormula]) =
+  ## 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.
+  runnableExamples:
+    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()
+
+  let 
+    logicalConnectiveCount = @[andSymbol, orSymbol, notSymbol, impliesSymbol].mapIt(formula.count(it)).sum()
+    leftParenCount = formula.count(leftParen)
+    rightParenCount = formula.count(rightParen)
+
+  # simple syntax check
+  assert logicalConnectiveCount == leftParenCount, "number of logical connectives and left parenthesis is different"
+  assert logicalConnectiveCount == rightParenCount, "number of logical connectives and right parenthesis is different"
+
+  let reversePolishNotation = formula.toReversePolishNotation()
+  var 
+    deque = initDeque[PropLogicFormula]()
+    newNameToAtomicFormulae = nameToAtomicFormulae
+  for token in reversePolishNotation:
+    if token.isOperator():
+      case token
+      of andSymbol:
+        let
+          right = deque.popLast()
+          left = deque.popLast()
+        deque.addLast(left & right)
+      of orSymbol:
+        let
+          right = deque.popLast()
+          left = deque.popLast()
+        deque.addLast(left | right)
+      of notSymbol:
+        let subFormula = deque.popLast()
+        deque.addLast(!subFormula)
+      of impliesSymbol:
+        let
+          consequent = deque.popLast()
+          antecedent = deque.popLast()
+        deque.addLast(antecedent => consequent)
+      else:
+        assert false, "No procedure for " & token & " exists!"
+    elif not token.isParen():
+      if not newNameToAtomicFormulae.hasKey(token):
+        newNameToAtomicFormulae[token] = generateAtomicProp()
+      deque.addLast(newNameToAtomicFormulae[token])
+    else:
+      assert false, "Unknown token: " & token
+  assert deque.len == 1, "Parse result is not single formula: " & $deque
+  let parseResult = deque.popLast()
+  return (parseResult, newNameToAtomicFormulae)

tests/testStringifyAndParsing.nim

@@ -0,0 +1,46 @@
+import unittest
+import strformat
+import tables
+import sets
+import sequtils
+import strutils
+
+import propositionalLogic
+
+suite "Stringify and restoring":
+  let 
+    p = generateAtomicProp()
+    q = generateAtomicProp()
+    r = generateAtomicProp()
+    formula = !p => (p | (q & r))
+    pId = p.getId()
+    qId = q.getId()
+    rId = r.getId()
+    nameToAtomicProps = {
+      $pId: p,
+      $qId: q,
+      $rId: r
+    }.toTable()
+
+  test "stringify":
+    assert $formula == fmt"((!{pId})=>({pId}|({qId}&{rId})))"
+
+  test "restoring":
+    let (restored, newNameToAtomicProps) = ($formula).parse(nameToAtomicProps)
+    assert $restored == $formula
+    assert newNameToAtomicProps.keys().toSeq().toHashSet() == nameToAtomicProps.keys().toSeq().toHashSet()
+
+  test "parse formula which includes atomic propositions which name is non-number":
+    var currentNameToAtomicProps = nameToAtomicProps
+    # generate atomic proposition corresponds to p before parsing
+    currentNameToAtomicProps["p"] = generateAtomicProp()
+    let 
+      formulaContainsNonNumber = "((p => (!(q & p))) | r)"
+      (restored, newNameToAtomicProps) = formulaContainsNonNumber.parse(currentNameToAtomicProps)
+      idToNamePair = newNameToAtomicProps.pairs().toSeq().mapIt(($(it[1].getId()), it[0]))
+    # remove spaces
+    assert ($restored).multiReplace(idToNamePair.concat(@[(" ", "")])) == formulaContainsNonNumber.replace(" ", "")
+    assert nameToAtomicProps.keys().toSeq().toHashSet() < newNameToAtomicProps.keys().toSeq().toHashSet()
+    assert newNameToAtomicProps.hasKey("p")
+    assert newNameToAtomicProps.hasKey("q")
+    assert newNameToAtomicProps.hasKey("r")