blob: 79e065c7a9dd9c8f1aab1c0d2c9cc22a87cb79e0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
#!/usr/bin/python
# usage: hiearchy_test.py inputfile
import pygraphviz as pgv
import sys, argparse
def children(G,n):
res = set()
new = set([n])
while new != set():
p = new.pop()
res.add(p)
new.update(set(G.successors(p)).difference(res))
return res
def common_children(G):
result = set()
for x in G.nodes():
for y in G.nodes():
if x < y and children(G,x).intersection(children(G,y)) != set():
result.add((x,y))
return result
def print_common_children_coq_check(G):
print("(** Generated by etc/utils/hierarchy_test.py *)")
print("From mathcomp Require Import all.")
for x in G.nodes():
if x.rfind("Lmod") >= 0 or x.rfind("Splitting") >= 0 or \
x.rfind("lgebra") >= 0 or x.rfind("FieldExt") >= 0 or \
x.rfind("Vector") >= 0:
print ("Local Notation \"" + x + ".type\" := (" + x + ".type _).")
print ("")
for (x, y) in common_children(G):
print ("Goal False. have := erefl : (_ : " + x + ".type) = (_ : " + y + ".type) :> Type. Abort.")
def main():
parser = argparse.ArgumentParser(description='Generate a check .v file \
for mathcomp structure hiearchies')
parser.add_argument('dotfile', metavar='<dotfile>', nargs=1,
help='a dotfile representing the hierarchy')
args = parser.parse_args()
print_common_children_coq_check(pgv.AGraph(args.dotfile[0]))
if __name__ == "__main__":
main()
|
