blob: bb0dd2c89b1ccba0246adc1f6c4cae6591e57697 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
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 "}"
|
