text: #!/usr/bin/env python3
  # Copyright (c) 2011 Qtrac Ltd. All rights reserved.
  # This program or module is free software: you can redistribute it and/or
  # modify it under the terms of the GNU General Public License as published
  # by the Free Software Foundation, either version 3 of the License, or
  # (at your option) any later version. It is provided for educational
  # purposes and is distributed in the hope that it will be useful, but
  # WITHOUT ANY WARRANTY; without even the implied warranty of
  # MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
  # General Public License for more details.
  
  """
  BNF
  
      FORMULA     ::= ('forall' | 'exists') SYMBOL ':' FORMULA
                   |  FORMULA '->' FORMULA      # right associative
                   |  FORMULA '|' FORMULA       # left associative
                   |  FORMULA '&' FORMULA       # left associative
                   |  '~' FORMULA
                   |  '(' FORMULA ')'
                   |  TERM '=' TERM
                   |  'true'
                   |  'false'
      TERM        ::= SYMBOL | SYMBOL '(' TERM_LIST ')'
      TERM_LIST   ::= TERM | TERM ',' TERM_LIST
      SYMBOL      ::= [a-zA-Z]\w*
  """
  
  import ply.lex
  import ply.yacc
  try:
      from pyparsing import (alphanums, alphas, delimitedList, Forward,
              Group, Keyword, Literal, opAssoc, operatorPrecedence,
              ParserElement, ParseException, ParseSyntaxException, Suppress,
              Word)
  except ImportError:
      from pyparsing_py3 import (alphanums, alphas, delimitedList, Forward,
              Group, Keyword, Literal, opAssoc, operatorPrecedence,
              ParserElement, ParseException, ParseSyntaxException, Suppress,
              Word)
  ParserElement.enablePackrat()
  
  
  def pyparsing_parse(text):
      """
      >>> formula = "a = b"
      >>> print(pyparsing_parse(formula))
      ['a', '=', 'b']
      >>> formula = "forall x: a = b"
      >>> print(pyparsing_parse(formula))
      ['forall', 'x', ['a', '=', 'b']]
      >>> formula = "a & b"
      >>> print(pyparsing_parse(formula))
      ['a', '&', 'b']
      >>> formula = "~true -> ~b = c"
      >>> print(pyparsing_parse(formula))
      [['~', 'true'], '->', ['~', ['b', '=', 'c']]]
      >>> formula = "~true -> ~(b = c)"
      >>> print(pyparsing_parse(formula))
      [['~', 'true'], '->', ['~', ['b', '=', 'c']]]
      >>> formula = "exists y: a -> b"
      >>> print(pyparsing_parse(formula))
      ['exists', 'y', ['a', '->', 'b']]
      >>> formula = "forall x: exists y: a = b"
      >>> print(pyparsing_parse(formula))
      ['forall', 'x', ['exists', 'y', ['a', '=', 'b']]]
      >>> formula = "forall x: exists y: a = b -> a = b & ~ a = b -> a = b"
      >>> print(pyparsing_parse(formula))
      ['forall', 'x', ['exists', 'y', [['a', '=', 'b'], '->', [[['a', '=', 'b'], '&', ['~', ['a', '=', 'b']]], '->', ['a', '=', 'b']]]]]
      >>> formula = "(forall x: exists y: a = b) -> a = b & ~ a = b -> a = b"
      >>> print(pyparsing_parse(formula))
      [['forall', 'x', ['exists', 'y', ['a', '=', 'b']]], '->', [[['a', '=', 'b'], '&', ['~', ['a', '=', 'b']]], '->', ['a', '=', 'b']]]
      >>> formula = "(forall x: exists y: true) -> true & ~ true -> true"
      >>> print(pyparsing_parse(formula))
      [['forall', 'x', ['exists', 'y', 'true']], '->', [['true', '&', ['~', 'true']], '->', 'true']]
      >>> formula = "a = b -> c = d & e = f"
      >>> result1 = pyparsing_parse(formula)
      >>> formula = "(a = b) -> (c = d & e = f)"
      >>> result2 = pyparsing_parse(formula)
      >>> result1 == result2
      True
      >>> result1
      [['a', '=', 'b'], '->', [['c', '=', 'd'], '&', ['e', '=', 'f']]]
      >>> formula = "forall x: exists y: true -> true & true | ~ true"
      >>> print(pyparsing_parse(formula))
      ['forall', 'x', ['exists', 'y', ['true', '->', [['true', '&', 'true'], '|', ['~', 'true']]]]]
      >>> formula = "~ true | true & true -> forall x: exists y: true"
      >>> print(pyparsing_parse(formula))
      [[['~', 'true'], '|', ['true', '&', 'true']], '->', ['forall', 'x', ['exists', 'y', 'true']]]
      >>> formula = "true & forall x: x = x"
      >>> print(pyparsing_parse(formula))
      ['true', '&', ['forall', 'x', ['x', '=', 'x']]]
      >>> formula = "true & (forall x: x = x)" # same as previous
      >>> print(pyparsing_parse(formula))
      ['true', '&', ['forall', 'x', ['x', '=', 'x']]]
      >>> formula = "forall x: x = x & true"
      >>> print(pyparsing_parse(formula))
      ['forall', 'x', [['x', '=', 'x'], '&', 'true']]
      >>> formula = "(forall x: x = x) & true" # different to previous
      >>> print(pyparsing_parse(formula))
      [['forall', 'x', ['x', '=', 'x']], '&', 'true']
      >>> formula = "forall x: = x & true"
      >>> print(pyparsing_parse(formula))
      Syntax error:
      forall x: = x & true
             ^
      []
      """
      left_parenthesis, right_parenthesis, colon = map(Suppress, "():")
      forall = Keyword("forall")
      exists = Keyword("exists")
      implies = Literal("->")
      or_ = Literal("|")
      and_ = Literal("&")
      not_ = Literal("~")
      equals = Literal("=")
      boolean = Keyword("false") | Keyword("true")
      symbol = Word(alphas, alphanums)
      term = Forward()
      term << (Group(symbol + Group(left_parenthesis +
                     delimitedList(term) + right_parenthesis)) | symbol)
      formula = Forward()
      forall_expression = Group(forall + symbol + colon + formula)
      exists_expression = Group(exists + symbol + colon + formula)
      operand = forall_expression | exists_expression | boolean | term
      formula << operatorPrecedence(operand, [
                                    (equals, 2, opAssoc.LEFT),
                                    (not_, 1, opAssoc.RIGHT),
                                    (and_, 2, opAssoc.LEFT),
                                    (or_, 2, opAssoc.LEFT),
                                    (implies, 2, opAssoc.RIGHT)])
      try:
          result = formula.parseString(text, parseAll=True)
          assert len(result) == 1
          return result[0].asList()
      except (ParseException, ParseSyntaxException) as err:
          print("Syntax error:\n{0.line}\n{1}^".format(err,
                " " * (err.column - 1)))
          return []
  
  
  def ply_parse(text):
      """
      >>> formula = "a = b"
      >>> print(ply_parse(formula))
      ['a', '=', 'b']
      >>> formula = "forall x: a = b"
      >>> print(ply_parse(formula))
      ['forall', 'x', ['a', '=', 'b']]
      >>> formula = "a & b"
      >>> print(ply_parse(formula))
      ['a', '&', 'b']
      >>> formula = "~true -> ~b = c"
      >>> print(ply_parse(formula))
      [['~', 'true'], '->', ['~', ['b', '=', 'c']]]
      >>> formula = "~true -> ~(b = c)"
      >>> print(ply_parse(formula))
      [['~', 'true'], '->', ['~', ['b', '=', 'c']]]
      >>> formula = "exists y: a -> b"
      >>> print(ply_parse(formula))
      ['exists', 'y', ['a', '->', 'b']]
      >>> formula = "forall x: exists y: a = b"
      >>> print(ply_parse(formula))
      ['forall', 'x', ['exists', 'y', ['a', '=', 'b']]]
      >>> formula = "forall x: exists y: a = b -> a = b & ~ a = b -> a = b"
      >>> print(ply_parse(formula))
      ['forall', 'x', ['exists', 'y', [['a', '=', 'b'], '->', [[['a', '=', 'b'], '&', ['~', ['a', '=', 'b']]], '->', ['a', '=', 'b']]]]]
      >>> formula = "(forall x: exists y: a = b) -> a = b & ~ a = b -> a = b"
      >>> print(ply_parse(formula))
      [['forall', 'x', ['exists', 'y', ['a', '=', 'b']]], '->', [[['a', '=', 'b'], '&', ['~', ['a', '=', 'b']]], '->', ['a', '=', 'b']]]
      >>> formula = "(forall x: exists y: true) -> true & ~ true -> true"
      >>> print(ply_parse(formula))
      [['forall', 'x', ['exists', 'y', 'true']], '->', [['true', '&', ['~', 'true']], '->', 'true']]
      >>> formula = "a = b -> c = d & e = f"
      >>> result1 = ply_parse(formula)
      >>> formula = "(a = b) -> (c = d & e = f)"
      >>> result2 = ply_parse(formula)
      >>> result1 == result2
      True
      >>> result1
      [['a', '=', 'b'], '->', [['c', '=', 'd'], '&', ['e', '=', 'f']]]
      >>> formula = "forall x: exists y: true -> true & true | ~ true"
      >>> print(ply_parse(formula))
      ['forall', 'x', ['exists', 'y', ['true', '->', [['true', '&', 'true'], '|', ['~', 'true']]]]]
      >>> formula = "~ true | true & true -> forall x: exists y: true"
      >>> print(ply_parse(formula))
      [[['~', 'true'], '|', ['true', '&', 'true']], '->', ['forall', 'x', ['exists', 'y', 'true']]]
      >>> formula = "true & forall x: x = x"
      >>> print(ply_parse(formula))
      ['true', '&', ['forall', 'x', ['x', '=', 'x']]]
      >>> formula = "true & (forall x: x = x)" # same as previous
      >>> print(ply_parse(formula))
      ['true', '&', ['forall', 'x', ['x', '=', 'x']]]
      >>> formula = "forall x: x = x & true"
      >>> print(ply_parse(formula))
      ['forall', 'x', [['x', '=', 'x'], '&', 'true']]
      >>> formula = "(forall x: x = x) & true" # different to previous
      >>> print(ply_parse(formula))
      [['forall', 'x', ['x', '=', 'x']], '&', 'true']
      >>> formula = "forall x: = x & true"
      >>> print(ply_parse(formula))
      Syntax error, line 2: EQUALS
      []
      """
      keywords = {"exists": "EXISTS", "forall": "FORALL",
                  "true": "TRUE", "false": "FALSE"}
      tokens = (["SYMBOL", "COLON", "COMMA", "LPAREN", "RPAREN",
                 "EQUALS", "NOT", "AND", "OR", "IMPLIES"] +
                list(keywords.values()))
  
      def t_SYMBOL(t):
          r"[a-zA-Z]\w*"
          t.type = keywords.get(t.value, "SYMBOL")
          return t
  
  
      t_EQUALS = r"="
      t_NOT = r"~"
      t_AND = r"&"
      t_OR = r"\|"
      t_IMPLIES = r"->"
      t_COLON = r":"
      t_COMMA = r","
      t_LPAREN = r"\("
      t_RPAREN = r"\)"
  
      t_ignore = " \t\n"
  
      def t_newline(t):
          r"\n+"
          t.lexer.lineno += len(t.value)
  
      def t_error(t):
          line = t.value.lstrip()
          i = line.find("\n")
          line = line if i == -1 else line[:i]
          raise ValueError("Syntax error, line {0}: {1}"
                           .format(t.lineno + 1, line))
      
      def p_formula_quantifier(p):
          """FORMULA : FORALL SYMBOL COLON FORMULA
                     | EXISTS SYMBOL COLON FORMULA"""
          p[0] = [p[1], p[2], p[4]]
  
      def p_formula_binary(p):
          """FORMULA : FORMULA IMPLIES FORMULA
                     | FORMULA OR FORMULA
                     | FORMULA AND FORMULA"""
          p[0] = [p[1], p[2], p[3]]
  
      def p_formula_not(p):
          "FORMULA : NOT FORMULA"
          p[0] = [p[1], p[2]]
  
      def p_formula_boolean(p):
          """FORMULA : FALSE
                     | TRUE"""
          p[0] = p[1]
  
      def p_formula_group(p):
          "FORMULA : LPAREN FORMULA RPAREN"
          p[0] = p[2]
  
      def p_formula_symbol(p):
          "FORMULA : SYMBOL"
          p[0] = p[1]
  
      def p_formula_equals(p):
          "FORMULA : TERM EQUALS TERM"
          p[0] = [p[1], p[2], p[3]]
  
      def p_term(p):
          """TERM : SYMBOL LPAREN TERMLIST RPAREN
                  | SYMBOL"""
          p[0] = p[1] if len(p) == 2 else [p[1], p[3]]
  
      def p_termlist(p):
          """TERMLIST : TERM COMMA TERMLIST
                      | TERM"""
          p[0] = p[1] if len(p) == 2 else [p[1], p[3]]
         
      def p_error(p):
          if p is None:
              raise ValueError("Unknown error")
          raise ValueError("Syntax error, line {0}: {1}".format(
                           p.lineno + 1, p.type))
  
  # from lowest to highest precedence!
      precedence = (("nonassoc", "FORALL", "EXISTS"),
                    ("right", "IMPLIES"),
                    ("left", "OR"),
                    ("left", "AND"),
                    ("right", "NOT"),
                    ("nonassoc", "EQUALS"))
  
      lexer = ply.lex.lex()
      parser = ply.yacc.yacc()
      try:
          return parser.parse(text, lexer=lexer)
      except ValueError as err:
          print(err)
          return []
      
  
  if __name__ == "__main__":
      import doctest
      doctest.testmod()
  