Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Prettyprint/produce proof tree #43

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Prev Previous commit
Next Next commit
lib/render-proof-tree: Small python script for extracting tree structure
nishantjr committed Apr 22, 2020
commit ec54f3667ae6ca5e47b19f3f6cc8eb43874dbee6
40 changes: 40 additions & 0 deletions prover/lib/render-proof-tree
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
#!/usr/bin/env python

from anytree import NodeMixin, Node, RenderTree
from collections import namedtuple
import textwrap
import fileinput
import re


class Goal(NodeMixin):
def __init__(self, id, parent_id):
self.id = id
self.name = id
self.parent_id = parent_id
self.claim = None

nodes = {}
roots = []

for line in fileinput.input():
match = re.search(' *active: \w*, id: (\w*\d*), parent: (\.|\w*\d*)', line)
if not match is None:
id = match.group(1)
parent = match.group(2)
node = Goal(id, parent)
nodes[id] = node
if parent == '.': roots += [node]
match = re.search('implies', line)
if not match is None:
node.claim = line

for id, node in nodes.items():
if node in roots: continue
node.parent = nodes[node.parent_id]

for pre, fill, node in RenderTree(roots[0]):
print(pre, 'id: ', node.id, 'x')
# if not node.claim is None:
# print(('\n' + fill).join(textwrap.wrap('claim: ' + node.claim)))