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
|
#!/bin/sh
# This scripts checks that the new grammar of Coq as defined in syntax-v8.tex
# is consistent in the sense that all invoked non-terminals are defined
defined_nt() {
grep "\\DEFNT{.*}" syntax-v8.tex | sed -e "s|.*DEFNT{\([^}]*\)}.*|\1|"|\
sort | sort -u
}
used_nt() {
cat syntax-v8.tex | tr \\\\ \\n | grep "^NT{.*}" |\
sed -e "s|^NT{\([^}]*\)}.*|\1|" | egrep -v ^\#1\|non-terminal | sort -u
}
used_term() {
cat syntax-v8.tex | tr \\\\ \\n | grep "^TERM{.*}" |\
sed -e "s|^TERM{\([^}]*\)}.*|\1|" -e "s|\\$||g" | egrep -v ^\#1\|terminal | sort -u
}
used_kwd() {
cat syntax-v8.tex | tr \\\\ \\n | grep "^KWD{.*}" |\
sed -e "s|^KWD{\([^}]*\)}.*|\1|" -e "s|\\$||g" | egrep -v ^\#1 | sort -u
}
defined_nt > def
used_nt > use
used_term > use-t
used_kwd > use-k
diff def use > df
###############################
echo
if grep ^\> df > /dev/null 2>&1 ; then
echo Undefined non-terminals:
echo ========================
echo
grep ^\> df | sed -e "s|^> ||"
echo
fi
if grep ^\< df > /dev/null 2>&1 ; then
echo Unused non-terminals:
echo =====================
echo
grep ^\< df | sed -e "s|^< ||"
echo
fi
#echo Used terminals:
#echo ===============
#echo
#cat use-t
|
