dependency-all

#!/bin/bash

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
  dependency-all $VERSION -- Generates the dependency graphs for the PVS libraries in the current folder.

SYNOPSIS

  dependency-all <options>

DESCRIPTION
  
  Applies dependencygraph over all the libraries in the current directory that are
  listed in the all-libraries file. 

  The option -no-iterate provokes the generation of a graph for the whole collection.
  If such option is not present, one graph is generated for each library in the
  collection. When in iterative mode, the scope of application can be controlled 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.

  This command also accepts all the parameters accepted by dependencygraph.

OPTIONS

  --dependencies  force regeneration of .dep files

  --no-iterate    generate graph for the whole collection instead of
  		  iterating on each library

  --zoomed        zoom into the current library when in iterative mode

  --after=<dir>   process all libraries after <dir>, exclusive
  --before=<dir>  process all libraries before <dir>, exclusive
  --but=<dir1>,..,<dirn>  does not process libraries <dir1>,...,<dirn>
  --do=<dir1>,..,<dirn>   process libraries <dir1>,...,<dirn>
  --from=<dir>    process all libraries from <dir>, inclusive
  --to=<dir>      process all libraries to <dir>, inclusive

  --dry-run       no action. Print call to dependencygraph

  -h|--help       prints this message
  --version       prints version information and exit

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

ADDITIONALARGS=
NOITERATE=
DRYRUN=
ZOOMORCENTER="--centered-at='%DIR%'"

while [ $# -gt 0 ]
do
  case $1 in
    -h|-help|--help) 
	usage
	exit 0;;
    -version|--version)
	readVersion
	echo $VERSION
	exit 0;;
    -dep|-d|--dependencies)
	FORCE=--dependencies;;
    --collection-label=*)
	COLLECTIONLABEL="$COLLECTIONLABEL $1";;
    -no-iterate|--no-iterate)
	NOITERATE=t;;
    -dry-run|--dry-run)
	DRYRUN="--dry-run";;
    -zoomed|--zoomed)
	ZOOMED=t
	ZOOMORCENTER="--do='%DIR%' --zoom='%DIR%'";;
    # valid options
    --after=*|-after=*\
    	|--before=*|-before=*\
    	|--but=*|-but=*\
    	|--do=*|-do=*\
    	|--from=*|-from=*\
    	|--to=*|-to=*)
    	ADDITIONALARGS="$ADDITIONALARGS $1";;	
    --after|-after\
    	|--before|-before\
    	|--but|-but\
    	|--do|-do\
    	|--from|-from\
    	|--to|-to)
    	if [[ $2 == -* ]]; then
    	    if [[ $1 =~ ^-[^-].*$ ]]; then
    		echo "Warning: missing values for $1 option (expected syntax is $1 <values>)"
    	    else
    		echo "Warning: missing values for $1 option (expected syntax is $1=<values>)"
    	    fi;
    	else
    	    ADDITIONALARGS="$ADDITIONALARGS $1 $2"
    	    shift
    	fi;;
    # # invalid options
    # *)
    # 	echo "Warning: omitting unrecognized option $1";;
    *)
	ADDITIONALDGARGS="$ADDITIONALDGARGS $1";;
  esac
  shift 
done

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

if [ "$provethem" ]; then
    NASALIBPATH=`./pvs-scripts/find-pvslib NASALib --strict --format "<dir>"`
    ( [ -z $PVS_LIBRARY_PATH ] || [ ! -d $NASALIBPATH ] ) && echo "Cannot find NASALib path" && exit 1;
    NASALIBDIR=$(echo $NASALIBPATH | sed -nE 's#^.*/([^/]+)$#\1#p')
    if [ $DRYRUN ]; then
	echo "-- Dry run --"
    fi
    if [ "$NOITERATE" ]; then
	if [ $DRYRUN ]; then
	    echo "$NASALIBPATH/pvs-scripts/dependencygraph $FORCE $COLLECTIONLABEL --svg --rankdir=TB --collection-label=\"$NASALIBDIR=NASALib\" --collection-label=\"lib=PVS Prelude\" --splines=polyline $ADDITIONALDGARGS $INPUT_FILE"
	else
	    $NASALIBPATH/pvs-scripts/dependencygraph $FORCE $COLLECTIONLABEL --svg --rankdir=TB --collection-label="$NASALIBDIR=NASALib" --collection-label="lib=PVS Prelude" --splines=polyline $ADDITIONALDGARGS $INPUT_FILE
	fi
    else
	if [ "$ZOOMED" ]; then
	    OUTPUTFILE='`echo %DIR%| sed "s#/#-#"`-zoomed'
	else
	    OUTPUTFILE='`echo %DIR%| sed "s#/#-#"`'
	fi
	$provethem $ADDITIONALARGS --execute "$NASALIBPATH/pvs-scripts/dependencygraph $FORCE $COLLECTIONLABEL $ZOOMORCENTER --svg --rankdir=TB --collection-label=\"$NASALIBDIR=NASALib\" --collection-label=\"lib=PVS Prelude\" --splines=polyline --out=$OUTPUTFILE $ADDITIONALDGARGS $INPUT_FILE && mv $OUTPUTFILE.svg %DIR%/" $DRYRUN --act="Plotting" $INPUT_FILE
    fi
else
  echo "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"
fi