|
#!/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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
