Merge pull request #318 from CohenCyril/hierarchy_test

Least common childen

2 files changed, 90 insertions, 38 deletions

diff --git a/etc/utils/hierarchy-diagram b/etc/utils/hierarchy-diagram
index 845ecfa..e30bb87 100755
--- a/etc/utils/hierarchy-diagram
+++ b/etc/utils/hierarchy-diagram
@@ -40,6 +40,7 @@ raw_coercions=$(tempfile -s .out | sed s/\.out$//)
 raw_canonicals=$(tempfile -s .out | sed s/\.out$//)
 parsed_coercions=$(tempfile)
 parsed_canonicals=$(tempfile)
+opt_raw_inheritances=off
 opt_canonicals=on
 opt_coercions=off
 opt_libs=()
@@ -49,6 +50,10 @@ while [[ $# -gt 0 ]]
 do
 
 case "$1" in
+  -raw-inheritances)
+    opt_raw_inheritances=on
+    shift;
+  ;;
   -canonicals)
     opt_canonicals="$2"
     shift; shift
@@ -86,18 +91,31 @@ Redirect "$raw_coercions" Print Graph.
 Redirect "$raw_canonicals" Print Canonical Projections.
 EOT
 
+cat $raw_canonicals.out \
+| sed -n 's/^\([a-zA-Z_\.]*\)\.sort <- \([a-zA-Z_\.]*\)\.sort ( \([a-zA-Z_\.]*\)\.\([a-zA-Z_]*\) )$/\1 \2 \3 \4/p' \
+| while read -r from_module to_module proj_module projection; do
+  if [[ $from_module = $proj_module ]] || [[ $to_module = $proj_module ]]; then
+    echo $from_module $to_module $proj_module $projection
+  fi
+done > $parsed_canonicals
+
+cat $raw_coercions.out \
+| sed -n 's/^\[\([^]]*\)\] : \([a-zA-Z_\.]*\)\.type >-> \([a-zA-Z_\.]*\)\.type$/\2 \3 \1/p' > $parsed_coercions
+
+if [[ $opt_raw_inheritances != "off" ]]; then
+
+  cat $parsed_canonicals | sed 's/^\([^ ]*\) \([^ ]*\) .*$/\1\n\2/g' | sort | uniq \
+  | while read -r module; do
+    echo -n "$module "
+    sed -n "s/^\([^ ]*\) $module .*$/\1/p" $parsed_canonicals | sort | xargs
+  done
+
+else
+
 echo "digraph structures {"
 
 if [[ $opt_canonicals != "off" ]]; then
 
-  cat $raw_canonicals.out \
-  | sed -n 's/^\([a-zA-Z_\.]*\)\.sort <- \([a-zA-Z_\.]*\)\.sort ( \([a-zA-Z_\.]*\)\.\([a-zA-Z_]*\) )$/\1 \2 \3 \4/p' \
-  | while read -r from_module to_module proj_module projection; do
-    if [[ $from_module = $proj_module ]] || [[ $to_module = $proj_module ]]; then
-      echo $from_module $to_module $proj_module $projection
-    fi
-  done > $parsed_canonicals
-
   cat $parsed_canonicals | while read -r from_module to_module proj_module projection; do
     grep "^$from_module " $parsed_canonicals | ( while read -r _ middle_module _ _; do
       if grep -q "^$middle_module $to_module " $parsed_canonicals; then
@@ -114,8 +132,6 @@ if [[ $opt_canonicals != "off" ]]; then
 fi
 
 if [[ $opt_coercions != "off" ]]; then
-  cat $raw_coercions.out \
-  | sed -n 's/^\[\([^]]*\)\] : \([a-zA-Z_\.]*\)\.type >-> \([a-zA-Z_\.]*\)\.type$/\2 \3 \1/p' > $parsed_coercions
 
   cat $parsed_coercions | while read -r from_module to_module coercion; do
     grep "^$from_module " $parsed_coercions | ( while read -r _ middle_module _; do
@@ -133,4 +149,6 @@ fi
 
 echo "}"
 
+fi
+
 rm $raw_coercions.out $raw_canonicals.out $parsed_coercions $parsed_canonicals
diff --git a/etc/utils/hierarchy_test.py b/etc/utils/hierarchy_test.py
index 79e065c..b0a034c 100644
--- a/etc/utils/hierarchy_test.py
+++ b/etc/utils/hierarchy_test.py
@@ -1,45 +1,79 @@
 #!/usr/bin/python
 # usage: hiearchy_test.py inputfile
 
-import pygraphviz as pgv
-import sys, argparse
+import sys, argparse, collections
 
-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 print_hierarchy_test(G, test_cases):
+    print ("(** Generated by etc/utils/hierarchy_test.py *)")
+    print ("From mathcomp Require Import all.")
 
-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():
+    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 _).")
+            print ("Local Notation \"" + x + ".type\" := (" + x + ".type _) (only parsing).")
     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 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_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()