New test cases generation: corrent implementation of least common children

Add a new option `-raw-inheritances` to `hierarchy-diagram` to generate an
intermediate file for `hierarchy_test.py`. So the typical usage is:
$ python3.5 etc/utils/hierarchy_test.py \
    <(etc/utils/hierarchy-diagram -raw-inheritances -R mathcomp mathcomp) \
    > mathcomp/test_suite/hierarchy_test.v

1 files changed, 32 insertions, 35 deletions

diff --git a/etc/utils/hierarchy_test.py b/etc/utils/hierarchy_test.py
index b3c4dc1..b0a034c 100644
--- a/etc/utils/hierarchy_test.py
+++ b/etc/utils/hierarchy_test.py
@@ -1,33 +1,9 @@
 #!/usr/bin/python
 # usage: hiearchy_test.py inputfile
 
-import pygraphviz as pgv
-import sys, argparse
+import sys, argparse, collections
 
-def children(G,r):
-    res = []
-    new = list([r])
-    while new != []:
-        n = new.pop()
-        # replace with a correct implementation of a topological sort
-        ns = set(G.successors(n))
-        resp = list(filter(lambda x: x not in ns, res))
-        resn = list(filter(lambda x: x in ns, res))
-        res = resp + [n] + resn
-        new=(list(ns.difference(set(res))))+new
-    return res
-
-def least_common_children(G):
-    result = set()
-    for x in G.nodes():
-        for y in G.nodes():
-            if x < y:
-                z = next((n for n in children(G,x) if n in children(G,y)),None)
-                if z != None:
-                    result.add((x,y,z))
-    return result
-
-def print_least_common_children_coq_check(G):
+def print_hierarchy_test(G, test_cases):
     print ("(** Generated by etc/utils/hierarchy_test.py *)")
     print ("From mathcomp Require Import all.")
 
@@ -35,20 +11,20 @@ def print_least_common_children_coq_check(G):
 (* `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 f1 := open_constr:(id : t1 -> Type) in
-  let f2 := open_constr:(id : t2 -> Type) in
   let T1 := open_constr:(_ : t1) in
   let T2 := open_constr:(_ : t2) in
   match tt with
-    | _ => unify (f1 T1) (f2 T2)
+    | _ => 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
@@ -59,24 +35,45 @@ Tactic Notation "check_join"
                 "but is expected to be" tjoin
   end.
 """)
-    for x in G.nodes():
+    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 _).")
+            print ("Local Notation \"" + x + ".type\" := (" + x + ".type _) (only parsing).")
     print ("")
     print ("Goal False.")
-    for (x, y,z) in least_common_children(G):
+    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('dotfile', metavar='<dotfile>', nargs=1,
-                        help='a dotfile representing the hierarchy')
+    parser.add_argument('graph', metavar='<graph>', nargs=1,
+                        help='a file representing the hierarchy')
     args = parser.parse_args()
-    print_least_common_children_coq_check(pgv.AGraph(args.dotfile[0]))
+    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()