使用Python将AST形式的Coq术语转换为波兰语表示法

Question

假设我有一个任意的 Coq术语（使用s-expressions / sexp的AST格式），例如：

n = n + n

我想自动将其转换为：

= n + n n

通过遍历AST树（由于sexp，它是列表的嵌套列表）。Python中是否有可以执行此操作的标准库？

现在，如果我要写下要执行的算法/伪代码（假设我可以将sexp转换为某些实际的树对象）：

def ToPolish():
    '''
    "postfix" tree traversal
    '''
    text = ''
    for node in root.children:
        if node is atoms:
            text := text + node.text
        else:
            text := text + ToPolish(node,text)
    return text

我认为这很接近，但我认为某处存在一个小错误...

---

AST示例：

 (ObjList
  ((CoqGoal
    ((fg_goals
      (((name 4)
        (ty
         (App
          (Ind
           (((Mutind (MPfile (DirPath ((Id Logic) (Id Init) (Id Coq))))
              (DirPath ()) (Id eq))
             0)
            (Instance ())))
          ((Ind
            (((Mutind (MPfile (DirPath ((Id Datatypes) (Id Init) (Id Coq))))
               (DirPath ()) (Id nat))
              0)
             (Instance ())))
           (App
            (Const
             ((Constant (MPfile (DirPath ((Id Nat) (Id Init) (Id Coq))))
               (DirPath ()) (Id add))
              (Instance ())))
            ((Construct
              ((((Mutind
                  (MPfile (DirPath ((Id Datatypes) (Id Init) (Id Coq))))
                  (DirPath ()) (Id nat))
                 0)
                1)
               (Instance ())))
             (Var (Id n))))
           (Var (Id n)))))
        (hyp
         ((((Id n)) ()
           (Ind
            (((Mutind (MPfile (DirPath ((Id Datatypes) (Id Init) (Id Coq))))
               (DirPath ()) (Id nat))
              0)
             (Instance ())))))))))
     (bg_goals ()) (shelved_goals ()) (given_up_goals ())))))

以上就是：

 (ObjList
  ((CoqString  "\
              \n  n : nat\
              \n============================\
              \n0 + n = n"))))

要么

= n + n n

---

使用sexp解析器：

[Symbol('Answer'), 2, [Symbol('ObjList'), [[Symbol('CoqGoal'), [[Symbol('fg_goals'), [[[Symbol('name'), 4], [Symbol('ty'), [Symbol('App'), [Symbol('Ind'), [[[Symbol('Mutind'), [Symbol('MPfile'), [Symbol('DirPath'), [[Symbol('Id'), Symbol('Logic')], [Symbol('Id'), Symbol('Init')], [Symbol('Id'), Symbol('Coq')]]]], [Symbol('DirPath'), []], [Symbol('Id'), Symbol('eq')]], 0], [Symbol('Instance'), []]]], [[Symbol('Ind'), [[[Symbol('Mutind'), [Symbol('MPfile'), [Symbol('DirPath'), [[Symbol('Id'), Symbol('Datatypes')], [Symbol('Id'), Symbol('Init')], [Symbol('Id'), Symbol('Coq')]]]], [Symbol('DirPath'), []], [Symbol('Id'), Symbol('nat')]], 0], [Symbol('Instance'), []]]], [Symbol('App'), [Symbol('Const'), [[Symbol('Constant'), [Symbol('MPfile'), [Symbol('DirPath'), [[Symbol('Id'), Symbol('Nat')], [Symbol('Id'), Symbol('Init')], [Symbol('Id'), Symbol('Coq')]]]], [Symbol('DirPath'), []], [Symbol('Id'), Symbol('add')]], [Symbol('Instance'), []]]], [[Symbol('Construct'), [[[[Symbol('Mutind'), [Symbol('MPfile'), [Symbol('DirPath'), [[Symbol('Id'), Symbol('Datatypes')], [Symbol('Id'), Symbol('Init')], [Symbol('Id'), Symbol('Coq')]]]], [Symbol('DirPath'), []], [Symbol('Id'), Symbol('nat')]], 0], 1], [Symbol('Instance'), []]]], [Symbol('Var'), [Symbol('Id'), Symbol('n')]]]], [Symbol('Var'), [Symbol('Id'), Symbol('n')]]]]], [Symbol('hyp'), [[[[Symbol('Id'), Symbol('n')]], [], [Symbol('Ind'), [[[Symbol('Mutind'), [Symbol('MPfile'), [Symbol('DirPath'), [[Symbol('Id'), Symbol('Datatypes')], [Symbol('Id'), Symbol('Init')], [Symbol('Id'), Symbol('Coq')]]]], [Symbol('DirPath'), []], [Symbol('Id'), Symbol('nat')]], 0], [Symbol('Instance'), []]]]]]]]]], [Symbol('bg_goals'), []], [Symbol('shelved_goals'), []], [Symbol('given_up_goals'), []]]]]]]

Answer 1

恐怕我不知道有什么模块可以做你想做的事情，但如果我正确理解了你想要做的事情，并且正如你所确定的那样，你只需要遍历树即可。您的递归实现稍有偏差。这个怎么样？

class Node:
  def __init__(self, text, children=None):
    self.text = text
    self.children = children or []

  def is_atomic(self):
    return not self.children

def to_polish(root):
    ''' postfix tree traversal '''
    return root.text + ' ' + ''.join(to_polish(n) for n in root.children)

print(to_polish(
  Node('=', [
    Node('a', [
      Node('+', [
        Node('b'),
        Node('c')
      ])
    ])
  ])
))