blob: e30bb8762c26741d25eab20464614a6b94f3190b (
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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
#!/bin/bash
usage(){
cat <<EOT >&2
Usage : hierarchy-diagram [OPTIONS]
Description:
hierarchy-diagram is a small utility to draw hierarchy diagrams of
mathematical structures. This utility uses the coercion paths and the
canonical projections between <module>.type types (typically in the MathComp
library) to draw the diagram. Indirect edges which can be composed of other
edges by transitivity are eliminated automatically for each kind of edges.
A diagram appears on the standard output in the DOT format which can be
converted to several image formats by Graphviz.
Options:
-h, -help:
Output a usage message and exit.
-canonicals (off|on|color):
Configure output of edges of canonical projections. The default value
is "on".
-coercions (off|on|color):
Configure output of edges of coercions. The default value is "off".
The value given by this option must be different from that by
-canonical soption.
-R dir coqdir:
This option is passed to coqtop: "recursively map physical dir to
logical coqdir".
-lib library:
Specify a Coq library used to draw a diagram. This option can appear
repetitively. If not specified, all.all will be used.
EOT
}
raw_coercions=$(tempfile -s .out | sed s/\.out$//)
raw_canonicals=$(tempfile -s .out | sed s/\.out$//)
parsed_coercions=$(tempfile)
parsed_canonicals=$(tempfile)
opt_raw_inheritances=off
opt_canonicals=on
opt_coercions=off
opt_libs=()
opt_coqtopargs=()
while [[ $# -gt 0 ]]
do
case "$1" in
-raw-inheritances)
opt_raw_inheritances=on
shift;
;;
-canonicals)
opt_canonicals="$2"
shift; shift
;;
-coercions)
opt_coercions="$2"
shift; shift
;;
-R)
opt_coqtopargs+=("-R" "$2" "$3")
shift; shift; shift
;;
-lib)
opt_libs+=("$2")
shift; shift
;;
-h|-help)
usage; exit
;;
*)
echo "ERROR: invalid option -- $1" >&2
echo >&2
usage; exit 1
;;
esac
done
[[ ${#opt_libs[@]} -eq 0 ]] && opt_libs=(all.all)
coqtop -w none ${opt_coqtopargs[@]} >/dev/null 2>&1 <<EOT
Set Printing Width 4611686018427387903.
Require Import ${opt_libs[@]}.
Redirect "$raw_coercions" Print Graph.
Redirect "$raw_canonicals" Print Canonical Projections.
EOT
cat $raw_canonicals.out \
| sed -n 's/^\([a-zA-Z_\.]*\)\.sort <- \([a-zA-Z_\.]*\)\.sort ( \([a-zA-Z_\.]*\)\.\([a-zA-Z_]*\) )$/\1 \2 \3 \4/p' \
| while read -r from_module to_module proj_module projection; do
if [[ $from_module = $proj_module ]] || [[ $to_module = $proj_module ]]; then
echo $from_module $to_module $proj_module $projection
fi
done > $parsed_canonicals
cat $raw_coercions.out \
| sed -n 's/^\[\([^]]*\)\] : \([a-zA-Z_\.]*\)\.type >-> \([a-zA-Z_\.]*\)\.type$/\2 \3 \1/p' > $parsed_coercions
if [[ $opt_raw_inheritances != "off" ]]; then
cat $parsed_canonicals | sed 's/^\([^ ]*\) \([^ ]*\) .*$/\1\n\2/g' | sort | uniq \
| while read -r module; do
echo -n "$module "
sed -n "s/^\([^ ]*\) $module .*$/\1/p" $parsed_canonicals | sort | xargs
done
else
echo "digraph structures {"
if [[ $opt_canonicals != "off" ]]; then
cat $parsed_canonicals | while read -r from_module to_module proj_module projection; do
grep "^$from_module " $parsed_canonicals | ( while read -r _ middle_module _ _; do
if grep -q "^$middle_module $to_module " $parsed_canonicals; then
exit 1
fi
done )
if [[ "$?" = "0" ]]; then
echo -n "\"$to_module\" -> \"$from_module\""
[[ $opt_canonicals == "on" ]] || echo -n "[color=$opt_canonicals]"
echo ";"
fi
done
fi
if [[ $opt_coercions != "off" ]]; then
cat $parsed_coercions | while read -r from_module to_module coercion; do
grep "^$from_module " $parsed_coercions | ( while read -r _ middle_module _; do
if grep -q "^$middle_module $to_module " $parsed_coercions; then
exit 1
fi
done )
if [[ "$?" = "0" ]]; then
echo -n "\"$to_module\" -> \"$from_module\""
[[ $opt_coercions == "on" ]] || echo -n "[color=$opt_coercions]"
echo ";"
fi
done
fi
echo "}"
fi
rm $raw_coercions.out $raw_canonicals.out $parsed_coercions $parsed_canonicals
|
