pytact.scripts.web

  1"""Generate a bird-eye-view visualization of (part of) a dataset with
  2Graphviz."""
  3
  4import graphviz
  5from pytact.data_reader import lowlevel_data_reader
  6import sys
  7import json
  8from pathlib import Path
  9from collections import Counter
 10import cmath
 11import colorsys
 12import math
 13
 14def get_node_id(gid, nid):
 15    prefix = f"{gid}-{nid}"
 16    return prefix
 17
 18def init_graph():
 19    g = graphviz.Graph(engine='sfdp')
 20    g.attr('node', shape='point', width='0.01', height='0.01')
 21    g.attr('edge', color="#0000ff10")
 22    g.attr(overlap='prism', outputorder='edgesfirst')
 23    g.attr(ratio='fill', size="20,10")
 24    return g
 25
 26def make_color(n, alpha):
 27    rgb = colorsys.hsv_to_rgb(n+(1/2), 1, 1)
 28    hexrgb = ["%0.2X"%int(v * 255) for v in list(rgb)+[alpha]]
 29    return f"#{hexrgb[0]}{hexrgb[1]}{hexrgb[2]}{hexrgb[3]}"
 30
 31def tooltip(n):
 32    if n.label.is_definition:
 33        return n.label.definition.name
 34    else:
 35        return n.label.which.name
 36
 37def main():
 38    with lowlevel_data_reader(Path(sys.argv[1])) as data:
 39
 40        subset = { p: gid for p, gid in data.graphid_by_filename.items()
 41                if Path('coq-tactician-stdlib.8.11.dev/theories/Init/') in p.parents }
 42
 43        # subset = { p: gid for p, gid in data.graphid_by_filename.items()
 44        #            if Path('coq-tactician-stdlib.8.11.dev/theories/Init/Logic.bin') == p }
 45
 46        print('Calculating node incoming count')
 47        incoming = Counter()
 48        for p, gid in subset.items():
 49            d = data[gid]
 50            for i, n in enumerate(d.graph.nodes):
 51                for ci in range(n.children_index, n.children_index + n.children_count):
 52                    target = d.graph.edges[ci].target
 53                    target_graph = data.local_to_global(gid, target.dep_index)
 54                    targetid = get_node_id(target_graph, target.node_index)
 55                    incoming[targetid] += 1
 56        incoming_max = incoming.most_common(1)[0][1]
 57
 58        print('Calculating node positions')
 59        g = init_graph()
 60        for p, gid in subset.items():
 61            d = data[gid]
 62            for i, n in enumerate(d.graph.nodes):
 63                sourceid = get_node_id(gid, i)
 64                g.node(sourceid, width=str(0.001*incoming[sourceid]), height=str(0.001*incoming[sourceid]))
 65                for ci in range(n.children_index, n.children_index + n.children_count):
 66                    target = d.graph.edges[ci].target
 67                    target_graph = data.local_to_global(gid, target.dep_index)
 68                    targetid = get_node_id(target_graph, target.node_index)
 69                    g.edge(sourceid, targetid)
 70                    # print(f"{sourceid},{targetid}")
 71        g.render(filename='web', format='json', view=False, cleanup=False)
 72
 73        print('Reading node positions')
 74        positions = dict()
 75        with open('web.json') as f:
 76            jsongraph = json.load(f)
 77            for node in jsongraph['objects']:
 78                position = node['pos'].split(',')
 79                position = complex(float(position[0]), float(position[1]))
 80                positions[node['name']] = position
 81
 82        print('Calculating largest distance')
 83        maxdist = 0
 84        for p, gid in subset.items():
 85            d = data[gid]
 86            for i, n in enumerate(d.graph.nodes):
 87                sourceid = get_node_id(gid, i)
 88                for ci in range(n.children_index, n.children_index + n.children_count):
 89                    target = d.graph.edges[ci].target
 90                    target_graph = data.local_to_global(gid, target.dep_index)
 91                    targetid = get_node_id(target_graph, target.node_index)
 92                    maxdist = max(maxdist, abs(positions[sourceid]-positions[targetid]))
 93        print(f'Max distance: {maxdist}')
 94
 95        print('Drawing final graph')
 96        g = init_graph()
 97        for p, gid in subset.items():
 98            d = data[gid]
 99            # print(p)
100            for i, n in enumerate(d.graph.nodes):
101                sourceid = get_node_id(gid, i)
102                g.node(sourceid, width=str(0.001*incoming[sourceid]), height=str(0.001*incoming[sourceid]),
103                    color=make_color((1/2)+(math.log(incoming[sourceid]+1)/math.log(incoming_max+1)), 1),
104                    tooltip=tooltip(n))
105                for ci in range(n.children_index, n.children_index + n.children_count):
106                    target = d.graph.edges[ci].target
107                    target_graph = data.local_to_global(gid, target.dep_index)
108                    targetid = get_node_id(target_graph, target.node_index)
109                    distance = abs(positions[sourceid]-positions[targetid])
110                    distance_norm = distance / maxdist
111                    g.edge(sourceid, targetid, color=make_color(distance_norm, 0.05))
112                    # print(f"{sourceid},{targetid}")
113        g.render(filename='web', format='svg', view=False, cleanup=False)
114
115# with data_reader(Path(sys.argv[1])) as data:
116
117#     g = graphviz.Graph(engine='sfdp')
118#     g.attr('node', shape='point', width='.1', height='.1')
119#     g.attr('edge', penwidth="0.1")
120#     g.attr(overlap='false')
121
122#     # print("source,target")
123
124#     for p, f in data.items():
125#         if Path('coq-tactician-stdlib.dev/theories/Init/') not in p.parents:
126#             continue
127#         for d in f:
128#             print(d.name)
129
130
131#     # g.render(filename='web', view=False, cleanup=False)
132
133if __name__ == "__main__":
134    exit(main())