find-all

#!/usr/bin/env perl
use Getopt::Long;

$usageln = "find-all [--help | <option>* ] <regexpr>";

$provethempath = "$ENV{'PVS_DIR'}";

if (! -x $provethempath) {
  $provethempath = `which provethem`;
  $provethempath =~ s/\/[^\/]*$/\//;
}

die "Either define \$PVS_DIR to point to the PVS directory or add the PVS directory to the environment variable \$PATH\n" if !$provethempath;

sub readVersion() {
  $VERSION = `$provethempath/provethem --version;`;
  $VERSION =~ s/^(.*)[\r\n]*$/\1/;
}

sub usage() {
  readVersion;
  print <<EOF;
NAME
  find-all $VERSION -- searches strings matching a given regular expressions in PVS libraries.

SYNOPSIS

  $usageln

DESCRIPTION

  By default, it finds in all the libraries which are reachable from the current 
  directory. 

  A library is considered reachable in a given directory <dir> if it is one of its 
  direct subfolders and there is a text file named all-libraries in <dir> and
  the library is mentioned there. The scope of application of find-all can be 
  restricted using the options --after, --before, --but, --do, --from, and --to 
  detailed below. The order implicitly referred to by all these options is the one 
  induced by the applicable all-libraries file.

OPTIONS

  --pvs             find in .pvs files (default)
  --prf             find in .prf files 
  --strategies      find in pvs-strategies files
  --attachment      find in pvs-attachment files

  --after=<dir>     find <regexpr> in all libraries after <dir>, exclusive
  --before=<dir>    find <regexpr> in all libraries before <dir>, exclusive
  --but=<dir1>,..,<dirn>  exclude libraries <dir1>,...,<dirn>
  --do=<dir1>,..,<dirn>  find <regexpr> in libraries <dir1>,...,<dirn>
  --from=<dir>      find <regexpr> in libraries from <dir>, inclusive
  --to=<dir>        find <regexpr> in libraries upto <dir>, inclusive

  --help            print this message
EOF
    exit 0;
}

GetOptions('after=s'=>\$after,
           'before=s'=>\$before,
	   'but=s'=>\$but,
	   'do=s'=>\$do,
           'from=s'=>\$from,
           'to=s'=>\$to,
	   'help'=>\$help,
	   'prf'=>\$prf,
	   'pvs'=>\$pvs,
	   'strategies'=>\$strategies,
	   'attachments'=>\$attachments,
           'dry-run'=>\$dryrun,
           'version'=>\$version
    ) or exit 1;

if ($version) {
  readVersion;
  print "$VERSION\n";
  exit;
}

usage() if $help;

$what = shift;

die "$usageln\n" if !$what || shift; 

$options = "";
$options .= "--after=$after " if $after;
$options .= "--before=$before " if $before;
$options .= "--but=$but " if $but;
$options .= "--do=$do " if $do;
$options .= "--from=$from " if $from;
$options .= "--to=$to " if $to;
$options .= "--dry-run " if $dryrun;

$files = "";
$files .= " *.prf" if $prf;
$files .= " pvs-strategies" if $strategies;
$files .= " pvs-attachments" if $attachments;
$files .= " *.pvs" if !$files || $pvs;

$file='';
if ( -f "all-libraries" ) {
  $file='all-libraries';
} elsif ( -f "nasalib.all" ) {
  $file='nasalib.all';
} elsif ( -f "all-theories" ) {
  print "Warning: all-theories is no longer supported as default input file name, ",
    "please rename it to all-libraries.\n";
  $file='all-theories';
} else {
  die "Error: neither all-libraries nor nasalib.all file found.\n";
}

system("$provethempath/provethem --ret-val-label=\"1=NOT FOUND\" --ret-val-label=\"0=FOUND\" --act=\"Finding\" $options --execute \"cd %DIR%; ls $files 1> /dev/null 2>&1 && grep -n --exclude orphaned-proofs.prf -e '$what' $files\" $file");