summaryrefslogtreecommitdiff
path: root/dev/tools/univdot
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /dev/tools/univdot
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'dev/tools/univdot')
-rwxr-xr-xdev/tools/univdot49
1 files changed, 0 insertions, 49 deletions
diff --git a/dev/tools/univdot b/dev/tools/univdot
deleted file mode 100755
index bb0dd2c8..00000000
--- a/dev/tools/univdot
+++ /dev/null
@@ -1,49 +0,0 @@
-#!/bin/sh
-
-usage() {
- echo ""
- echo "usage: univdot [INPUT] [OUTPUT]"
- echo ""
- echo "takes the output of Dump Universes \"file\" command"
- echo "and transforms it to the dot format"
- echo ""
- echo "Coq> Dump Universes \"univ.raw\"."
- echo ""
- echo "user@host> univdot univ.raw | dot -Tps > univ.ps"
- echo ""
-}
-
-
-# these are dot edge attributes to draw arrows corresponding
-# to > >= and = edges of the universe graph
-
-GT="[color=red]"
-GE="[color=blue]"
-EQ="[color=black]"
-
-
-# input/output redirection
-case $# in
- 0) ;;
- 1) case $1 in
- -h|-help|--help) usage
- exit 0 ;;
- *) exec < $1 ;;
- esac ;;
- 2) exec < $1 > $2 ;;
- *) usage
- exit 0;;
-esac
-
-
-# dot header
-echo 'digraph G {\
- size="7.5,10" ;\
- rankdir = TB ;'
-
-sed -e "s/^\([^ =>]\+\) > \([^ =>]\+\)/\1 -> \2 $GT/" \
- -e "s/^\([^ =>]\+\) >= \([^ =>]\+\)/\1 -> \2 $GE/" \
- -e "s/^\([^ =>]\+\) = \([^ =>]\+\)/\1 -> \2 $EQ/" \
-| sed -e "s/\./_/g"
-
-echo "}" \ No newline at end of file