Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: check-grammar Sprache: Isabelle

Original von: Coq^©

#!/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.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.