least common childen

1 files changed, 53 insertions, 16 deletions

diff --git a/etc/utils/hierarchy_test.py b/etc/utils/hierarchy_test.py
index 79e065c..b3c4dc1 100644
--- a/etc/utils/hierarchy_test.py
+++ b/etc/utils/hierarchy_test.py
@@ -4,34 +4,71 @@
 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))
+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 common_children(G):
+def least_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))
+            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_common_children_coq_check(G):
-    print("(** Generated by etc/utils/hierarchy_test.py *)")
-    print("From mathcomp Require Import all.")
+def print_least_common_children_coq_check(G):
+    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 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)
+    | _ => fail "There is no join of" t1 "and" t2
+  end;
+  let Tjoin :=
+    lazymatch T1 with
+      | _ ?Tjoin => constr: (Tjoin)
+      | ?Tjoin => constr: (Tjoin)
+    end
+  in
+  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.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.")
+    print ("Goal False.")
+    for (x, y,z) in least_common_children(G):
+        print ("check_join " + x + ".type " + y + ".type " + z + ".type.")
+    print ("Abort.")
 
 def main():
     parser = argparse.ArgumentParser(description='Generate a check .v file \
@@ -39,7 +76,7 @@ def main():
     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]))
+    print_least_common_children_coq_check(pgv.AGraph(args.dotfile[0]))
 
 if __name__ == "__main__":
     main()