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
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
#!/usr/bin/python
# usage: hiearchy_test.py inputfile
import sys, argparse, collections
def print_hierarchy_test(G, test_cases):
print ("(** Generated by etc/utils/hierarchy_test.py *)")
print ("From mathcomp Require Import all.")
print ("""
(* `check_join t1 t2 tjoin` assert that the join of `t1` and `t2` is `tjoin`. *)
Tactic Notation "check_join"
open_constr(t1) open_constr(t2) open_constr(tjoin) :=
let T1 := open_constr:(_ : t1) in
let T2 := open_constr:(_ : t2) in
match tt with
| _ => unify ((id : t1 -> Type) T1) ((id : t2 -> Type) T2)
| _ => fail "There is no join of" t1 "and" t2
end;
let Tjoin :=
lazymatch T1 with
| _ (_ ?Tjoin) => constr: (Tjoin)
| _ ?Tjoin => constr: (Tjoin)
| ?Tjoin => constr: (Tjoin)
end
in
is_evar Tjoin;
let tjoin' := type of Tjoin in
lazymatch tjoin' with
| tjoin => lazymatch tjoin with
| tjoin' => idtac
| _ => idtac tjoin'
end
| _ => fail "The join of" t1 "and" t2 "is" tjoin'
"but is expected to be" tjoin
end.
""")
for x in G.keys():
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 _) (only parsing).")
print ("")
print ("Goal False.")
for (x,y,z) in test_cases:
print ("check_join " + x + ".type " + y + ".type " + z + ".type.")
print ("Abort.")
def compute_least_common_children(G):
tests=[]
for pa, ch_a in G.items():
for pb, ch_b in G.items():
ch_c = ({pa} | ch_a) & ({pb} | ch_b) # common children
for c in ch_c:
ch_c = ch_c - G[c]
if len(ch_c) == 1:
tests.append((pa, pb, ch_c.pop()))
elif 2 <= len(ch_c):
print (pa, "and", pb, "have more than two least common children:", ch_c, ".", file=sys.stderr)
sys.exit(1)
return tests
def main():
parser = argparse.ArgumentParser(description='Generate a check .v file \
for mathcomp structure hiearchies')
parser.add_argument('graph', metavar='<graph>', nargs=1,
help='a file representing the hierarchy')
args = parser.parse_args()
G = {}
with open(args.graph[0]) as f:
for line in f:
words = line.split()
p = words.pop(0)
G[p] = set(words)
G = collections.OrderedDict(sorted(G.items()))
print_hierarchy_test(G, compute_least_common_children(G))
if __name__ == "__main__":
main()
|
