summaryrefslogtreecommitdiff
path: root/dev/v8-syntax/check-grammar
blob: 67da1bc51336525095ede332ab75df8aa2ddc198 (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
#!/bin/bash
# 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