Facilites pour le debogguage des univers.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1772 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 81 insertions, 0 deletions

diff --git a/dev/univdot b/dev/univdot
new file mode 100755
index 0000000000..bb0dd2c89b
--- /dev/null
+++ b/dev/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
diff --git a/dev/universes.txt b/dev/universes.txt
new file mode 100644
index 0000000000..65c1e522af
--- /dev/null
+++ b/dev/universes.txt
@@ -0,0 +1,32 @@
+How to debug universes?
+
+1. There is a command Dump Universes in Coq toplevel
+
+   Dump Universes.
+     prints the graph of universes in the form of constraints
+
+   Dump Universes "file".
+     produces the "file" containing universe constraints in the form
+       univ1 # univ2 ;
+     where # can be either > >= or =
+     
+   The file produced by the latter command can be transformed using
+   the script univdot to dot format.
+   For example
+
+   univdot file | dot -Tps > file.ps
+
+   produces a graph of universes in ps format. 
+   > arrows are red, >= blue, and = black.
+
+
+   *) for dot see http://www.research.att.com/sw/tools/graphviz/
+
+
+2. There is a printing option
+  
+   Termast.print_universes : bool ref
+
+   which, when set (in ocaml after Drop), makes all pretty-printed
+   Type's annotated with the name of the universe.
+