From 25a1164023a46c035411d4fe3698d1a7c9912c4f Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 22 Feb 2019 15:22:46 +0100 Subject: Add a tool to draw the hierarchy diagram --- etc/utils/hierarchy-diagram | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100755 etc/utils/hierarchy-diagram diff --git a/etc/utils/hierarchy-diagram b/etc/utils/hierarchy-diagram new file mode 100755 index 0000000..ee96b8d --- /dev/null +++ b/etc/utils/hierarchy-diagram @@ -0,0 +1,20 @@ +#!/bin/bash + +echo "digraph structures {" + +{ +cat </dev/null | \ +grep '^\[[^ ;]*\] : [a-zA-Z_\.]*\.class_of >-> [a-zA-Z_\.]*\.class_of$' | \ +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"];/' +done + +echo "}" -- cgit v1.2.3 From 5d0af0cfb61b60a103456138577ec59b032e6133 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 22 Feb 2019 17:44:16 +0100 Subject: Reimplement hierarchy-diagram by using coercions between ".type" types --- etc/utils/hierarchy-diagram | 28 ++++++++++++++++++++++------ 1 file 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 </dev/null </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 -- cgit v1.2.3 From 059d01303184aaf5762bfca545c50d13ff988f6c Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Mon, 25 Feb 2019 16:38:52 +0100 Subject: Use both coercions and canonical projections to generate the diagram --- etc/utils/hierarchy-diagram | 52 +++++++++++++++++++++++++++++++-------------- 1 file 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 </dev/null 2>&1 <-> [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 -- cgit v1.2.3 From 45820be9a6bd339882d3fcb539a52cb7d26bdb66 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 7 Mar 2019 16:35:43 +0100 Subject: Put documentation and some command line options for hierarchy-diagram --- etc/utils/hierarchy-diagram | 144 ++++++++++++++++++++++++++++++++++---------- 1 file changed, 112 insertions(+), 32 deletions(-) diff --git a/etc/utils/hierarchy-diagram b/etc/utils/hierarchy-diagram index 9e68b09..845ecfa 100755 --- a/etc/utils/hierarchy-diagram +++ b/etc/utils/hierarchy-diagram @@ -1,55 +1,135 @@ #!/bin/bash +usage(){ +cat <&2 +Usage : hierarchy-diagram [OPTIONS] + +Description: + hierarchy-diagram is a small utility to draw hierarchy diagrams of + mathematical structures. This utility uses the coercion paths and the + canonical projections between .type types (typically in the MathComp + library) to draw the diagram. Indirect edges which can be composed of other + edges by transitivity are eliminated automatically for each kind of edges. + A diagram appears on the standard output in the DOT format which can be + converted to several image formats by Graphviz. + +Options: + -h, -help: + Output a usage message and exit. + + -canonicals (off|on|color): + Configure output of edges of canonical projections. The default value + is "on". + + -coercions (off|on|color): + Configure output of edges of coercions. The default value is "off". + The value given by this option must be different from that by + -canonical soption. + + -R dir coqdir: + This option is passed to coqtop: "recursively map physical dir to + logical coqdir". + + -lib library: + Specify a Coq library used to draw a diagram. This option can appear + repetitively. If not specified, all.all will be used. +EOT +} + raw_coercions=$(tempfile -s .out | sed s/\.out$//) raw_canonicals=$(tempfile -s .out | sed s/\.out$//) parsed_coercions=$(tempfile) parsed_canonicals=$(tempfile) +opt_canonicals=on +opt_coercions=off +opt_libs=() +opt_coqtopargs=() + +while [[ $# -gt 0 ]] +do + +case "$1" in + -canonicals) + opt_canonicals="$2" + shift; shift + ;; + -coercions) + opt_coercions="$2" + shift; shift + ;; + -R) + opt_coqtopargs+=("-R" "$2" "$3") + shift; shift; shift + ;; + -lib) + opt_libs+=("$2") + shift; shift + ;; + -h|-help) + usage; exit + ;; + *) + echo "ERROR: invalid option -- $1" >&2 + echo >&2 + usage; exit 1 + ;; +esac -coqtop -w none -R mathcomp mathcomp >/dev/null 2>&1 </dev/null 2>&1 <-> \([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 $parsed_coercions | while read -r from_module to_module coercion; do +if [[ $opt_canonicals != "off" ]]; then - grep "^$from_module " $parsed_coercions | ( while read -r _ middle_module _; do - if grep -q "^$middle_module $to_module " $parsed_coercions; then - exit 1 + 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 ) - if [[ "$?" = "0" ]]; then - echo "\"$to_module\" -> \"$from_module\"[color=red];" - fi + done > $parsed_canonicals -done + 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 + exit 1 + fi + done ) + if [[ "$?" = "0" ]]; then + echo -n "\"$to_module\" -> \"$from_module\"" + [[ $opt_canonicals == "on" ]] || echo -n "[color=$opt_canonicals]" + echo ";" + fi + done -cat $parsed_canonicals | while read -r from_module to_module proj_module projection; do +fi - 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 "\"$to_module\" -> \"$from_module\"[color=blue];" - 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 -done + 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 -n "\"$to_module\" -> \"$from_module\"" + [[ $opt_coercions == "on" ]] || echo -n "[color=$opt_coercions]" + echo ";" + fi + done +fi echo "}" -- cgit v1.2.3