From e24d8149c3aefd11b03458b6f9b3e38ca454b07a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 23 May 2006 21:51:59 +0000
Subject: Restructuration dossier dev et mise à jour de certaines
 documentations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8856 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/tools/univdot | 49 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)
 create mode 100755 dev/tools/univdot

(limited to 'dev/tools/univdot')

diff --git a/dev/tools/univdot b/dev/tools/univdot
new file mode 100755
index 0000000000..bb0dd2c89b
--- /dev/null
+++ b/dev/tools/univdot
@@ -0,0 +1,49 @@
+#!/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
-- 
cgit v1.2.3