From 2d31a42aa3c2dacabc0cf005b45fc7bb4e6383e9 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Tue, 30 Apr 2019 14:48:37 +0200
Subject: Reimplement the hierarchy related tools in OCaml

The functionalities of the structure hierarchy related tools `hierarchy-diagram`
and `hierarchy_test.py` are provided by an OCaml script `hierarchy.ml`.
`test_suite/hierarchy_test.v` is deleted. Now make can generate it.
---
 etc/utils/hierarchy-diagram | 154 --------------------------------------------
 1 file changed, 154 deletions(-)
 delete mode 100755 etc/utils/hierarchy-diagram

(limited to 'etc/utils/hierarchy-diagram')

diff --git a/etc/utils/hierarchy-diagram b/etc/utils/hierarchy-diagram
deleted file mode 100755
index e30bb87..0000000
--- a/etc/utils/hierarchy-diagram
+++ /dev/null
@@ -1,154 +0,0 @@
-#!/bin/bash
-
-usage(){
-cat <<EOT >&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 <module>.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_raw_inheritances=off
-opt_canonicals=on
-opt_coercions=off
-opt_libs=()
-opt_coqtopargs=()
-
-while [[ $# -gt 0 ]]
-do
-
-case "$1" in
-  -raw-inheritances)
-    opt_raw_inheritances=on
-    shift;
-  ;;
-  -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
-
-done
-
-[[ ${#opt_libs[@]} -eq 0 ]] && opt_libs=(all.all)
-
-coqtop -w none ${opt_coqtopargs[@]} >/dev/null 2>&1 <<EOT
-Set Printing Width 4611686018427387903.
-Require Import ${opt_libs[@]}.
-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 $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
-
-fi
-
-if [[ $opt_coercions != "off" ]]; then
-
-  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 "}"
-
-fi
-
-rm $raw_coercions.out $raw_canonicals.out $parsed_coercions $parsed_canonicals
-- 
cgit v1.2.3