typecheck-all

#!/bin/sh

if [ ! -z "$PVS_DIR" ]; then
    provethem="$PVS_DIR/provethem"
else
    provethem=`which provethem`
    if [ ! $provethem  ]; then
	printf "The script 'provethem' could not be located. Either define \$PVS_DIR to point to the PVS directory or add the PVS directory to the environment variable \$PATH.\n"
	exit 1;
    fi
fi

readVersion() {
    if ! type "$provethem" > /dev/null 2>&1  || ! VERSION=$($provethem --version) ; then
	printf "The script 'provethem' could not be located. Either define \$PVS_DIR to point to the PVS directory or add the PVS directory to the environment variable \$PATH.\n"
	exit 1;
    fi
}

usage() {
    readVersion
    
    echo "NAME
  typecheck-all $VERSION -- Typechecks the PVS libraries in the current folder.

SYNOPSIS

  typecheck-all <options>

DESCRIPTION
  This script wraps provethem to provide a specific kind of run. By default, it removes 
  .pvscontext and the binary files from the pvsbin folder in each library directory, replaces 
  the pvs library path by the current directory, and typechecks the libraries listed in the 
  nasalib.all file. 

  To supersede this particular configuration, the same options accepted by provethem can
  be used on this script.

  The list of libraries to be processed is read from the file 'all-libraries' if there is no
  'nasalib.all' file in the current folder.

SEE ALSO
  provethem -- for iterating proveit on a list of directories
"
}

for opt in "$@"
do
    if [ $opt = "--help" -o $opt = "-help" -o $opt = "-h" ]; then
	usage
	exit 0
    fi
done

all_theories_file="nasalib.all"
if [ ! -f $all_theories_file ]; then 
    all_theories_file="all-libraries";
    if [ ! -f $all_theories_file ]; then 
	all_theories_file="all-theories";
	if [ -f $all_theories_file ]; then
	    echo "Warning: all-theories is no longer supported as default input file name, please rename it to all-libraries."
	else
	    echo "Error: input file not found.";
	    exit 1;
	fi;
    fi
fi

if [ "$provethem" ]; then
  $provethem --clean-only --action-name="Cleaning" "$@" $all_theories_file
  $provethem  --action-name="Typechecking" --clearpath --addpath --force --typecheck "$@" $all_theories_file
fi