Use both coercions and canonical projections to generate the diagram

1 files changed, 36 insertions, 16 deletions

diff --git a/etc/utils/hierarchy-diagram b/etc/utils/hierarchy-diagram
index 310c544..9e68b09 100755
--- a/etc/utils/hierarchy-diagram
+++ b/etc/utils/hierarchy-diagram
@@ -1,36 +1,56 @@
 #!/bin/bash
 
-rawgraph=$(tempfile)
+raw_coercions=$(tempfile -s .out | sed s/\.out$//)
+raw_canonicals=$(tempfile -s .out | sed s/\.out$//)
+parsed_coercions=$(tempfile)
+parsed_canonicals=$(tempfile)
 
-{
-coqtop -w none -R mathcomp mathcomp 2>/dev/null <<EOT
+coqtop -w none -R mathcomp mathcomp >/dev/null 2>&1 <<EOT
 Set Printing Width 4611686018427387903.
 Require Import all.all.
-Print Graph.
+Redirect "$raw_coercions" Print Graph.
+Redirect "$raw_canonicals" Print Canonical Projections.
 EOT
-} | \
-grep '^\[[^ ;]*\] : [a-zA-Z_\.]*\.type >-> [a-zA-Z_\.]*\.type$' | \
-while read -r line; do
-  echo $line | \
-  sed 's/^\[\([^]]*\)\] : \([a-zA-Z_\.]*\)\.type >-> \([a-zA-Z_\.]*\)\.type$/\2 \3 \1/'
-done > $rawgraph
+
+cat $raw_coercions.out \
+| sed -n 's/^\[\([^]]*\)\] : \([a-zA-Z_\.]*\)\.type >-> \([a-zA-Z_\.]*\)\.type$/\2 \3 \1/p' > $parsed_coercions
+
+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
 
 echo "digraph structures {"
 
-cat $rawgraph | while read -r from_module to_module coercion; do
+cat $parsed_coercions | while read -r from_module to_module coercion; do
+
+  grep "^$from_module " $parsed_coercions | ( while read -r _ middle_module _; do
+    if grep -q "^$middle_module $to_module " $parsed_coercions; then
+      exit 1
+    fi
+  done )
+  if [[ "$?" = "0" ]]; then
+    echo "\"$to_module\" -> \"$from_module\"[color=red];"
+  fi
+
+done
+
+cat $parsed_canonicals | while read -r from_module to_module proj_module projection; do
 
-  grep "^$from_module " $rawgraph | ( while read -r _ middle_module _; do
-    if grep -q "^$middle_module $to_module " $rawgraph; then
+  grep "^$from_module " $parsed_canonicals | ( while read -r _ middle_module _ _; do
+    if grep -q "^$middle_module $to_module " $parsed_canonicals; then
       exit 1
     fi
   done )
   if [[ "$?" = "0" ]]; then
-    echo "\"$from_module\" -> \"$to_module\";"
-    #echo "\"$from_module\" -> \"$to_module\" [label = \"$coercion\"];"
+    echo "\"$to_module\" -> \"$from_module\"[color=blue];"
   fi
 
 done
 
 echo "}"
 
-rm $rawgraph
+rm $raw_coercions.out $raw_canonicals.out $parsed_coercions $parsed_canonicals