Added new syntax definition

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4100 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 50 insertions, 0 deletions

diff --git a/doc/check-grammar b/doc/check-grammar
new file mode 100755
index 000000000..67da1bc51
--- /dev/null
+++ b/doc/check-grammar
@@ -0,0 +1,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
\ No newline at end of file