Extract the vocabulary items (symbols) for MML articles.

vocab.pl

@@ -0,0 +1,65 @@
+#!/usr/bin/perl -w
+
+# Given a list ART_1, ART_2, ..., of article names, print out the list
+# of all the vocabulary items declared in these articles.
+#
+# TODO
+#
+# - if an article does not exist in the MML, search for the dict
+#   directory; if not found even there, issue a warning (or maybe die)
+
+
+my $grep_pipe = '';
+
+# build a pipe that ignores the lines, generated by listvoc, that
+# start like "Vocabulary: xboole_0".
+foreach my $i (0 .. $#ARGV) {
+  my $arg = $ARGV[$i];
+  if ($arg =~ /^[A-Za-z0-9_]{1,25}$/) {
+    $grep_pipe .= "grep --invert-match '^Vocabulary: $arg\$'";
+    if ($i != $#ARGV) {
+      $grep_pipe .= "| "
+    }
+  } else {
+    die ("Weird argument\n\n  $arg\n\nArguments must consist of alphanumeric characters and the underscore character _ only, cannot be empty, and must be at most 25 characters long (isn't that enough for you?).");
+  }
+}
+
+# sanity check: ensure that all the specified articles exist in the
+# MML.  We may want to loosen this condition later.  If we're working
+# only with MML articles, this check is sufficient.
+my $mml_lar = '/sw/share/mizar/mml.lar';
+foreach my $article (@ARGV) {
+  unless ($article =~ /^hidden$/i or $article =~ /^tarski$/i) {
+    system ('grep', '--silent', '--ignore-case', "$article", "$mml_lar");
+    unless ($? == 0) {
+      die ("The specified article\n\n  $article\n\ndoes not exist in the MML.");
+    }
+  }
+}
+
+# DEBUG
+# warn ("grep to be executed:\n\n  $grep_pipe\n");
+
+my $listvoc = "listvoc @ARGV";
+my $squeeze_extra_newlines = 'tr -s \'\n\'';
+my $ignore_first_three_lines = 'gsed -n -e \'3,\$p\'';
+my $first_before_space = 'cut -f 1 -d \' \'';
+my $ignore_first_character = 'gsed -e \'s/^[A-Z]//\'';
+my $uniqify = 'uniq'; # in case the same symbol has multiple syntactic roles
+
+my $big_pipe = "$listvoc | $squeeze_extra_newlines | $ignore_first_character | $grep_pipe | $first_before_space | $ignore_first_character | $uniqify";
+
+# DEBUG
+# warn ("full command to be executed:\n\n  $big_pipe\n");
+
+my @output = `$big_pipe`;
+if ($? eq 0) {
+  foreach my $line (@output) {
+    print ($line);
+  }
+  exit (0);
+} else {
+  warn ("The execution of the command\n\n  $big_pipe\n\ndid not terminate cleanly; the error was $!");
+  exit ($?);
+}