Reimplement hierarchy-diagram by using coercions between "<module>.type" types

1 files changed, 22 insertions, 6 deletions

diff --git a/etc/utils/hierarchy-diagram b/etc/utils/hierarchy-diagram
index ee96b8d..310c544 100755
--- a/etc/utils/hierarchy-diagram
+++ b/etc/utils/hierarchy-diagram
@@ -1,20 +1,36 @@
 #!/bin/bash
 
-echo "digraph structures {"
+rawgraph=$(tempfile)
 
 {
-cat <<EOT
+coqtop -w none -R mathcomp mathcomp 2>/dev/null <<EOT
 Set Printing Width 4611686018427387903.
 Require Import all.all.
 Print Graph.
 EOT
 } | \
-coqtop -w none -R mathcomp mathcomp 2>/dev/null | \
-grep '^\[[^ ;]*\] : [a-zA-Z_\.]*\.class_of >-> [a-zA-Z_\.]*\.class_of$' | \
+grep '^\[[^ ;]*\] : [a-zA-Z_\.]*\.type >-> [a-zA-Z_\.]*\.type$' | \
 while read -r line; do
   echo $line | \
-  sed 's/^\[\([^]]*\)\] : \([a-zA-Z_\.]*\)\.class_of >-> \([a-zA-Z_\.]*\)\.class_of$/"\2" -> "\3";/'
-  #sed 's/^\[\([^]]*\)\] : \([a-zA-Z_\.]*\)\.class_of >-> \([a-zA-Z_\.]*\)\.class_of$/"\2" -> "\3" [label="\1"];/'
+  sed 's/^\[\([^]]*\)\] : \([a-zA-Z_\.]*\)\.type >-> \([a-zA-Z_\.]*\)\.type$/\2 \3 \1/'
+done > $rawgraph
+
+echo "digraph structures {"
+
+cat $rawgraph | while read -r from_module to_module coercion; do
+
+  grep "^$from_module " $rawgraph | ( while read -r _ middle_module _; do
+    if grep -q "^$middle_module $to_module " $rawgraph; then
+      exit 1
+    fi
+  done )
+  if [[ "$?" = "0" ]]; then
+    echo "\"$from_module\" -> \"$to_module\";"
+    #echo "\"$from_module\" -> \"$to_module\" [label = \"$coercion\"];"
+  fi
+
 done
 
 echo "}"
+
+rm $rawgraph