summaryrefslogtreecommitdiff
path: root/dev/univdot
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 "}"