From 045f398e6ad72d32199d77c9794f4b3e118f196a Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 6 Jun 2003 12:04:40 +0000
Subject: Added new syntax definition

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4100 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/check-grammar | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100755 doc/check-grammar

(limited to 'doc/check-grammar')

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
-- 
cgit v1.2.3