pvsio.in

#!/bin/sh
#
# pvsio.in
# Release: PVSio-7.1.0 (11/05/20)
#
# Contact: Cesar Munoz (cesar.a.munoz@nasa.gov)
# NASA Langley Research Center
# http://shemesh.larc.nasa.gov/people/cam/PVSio
#
# Copyright (c) 2011-2012 United States Government as represented by
# the National Aeronautics and Space Administration.  No copyright
# is claimed in the United States under Title 17, U.S.Code. All Other
# Rights Reserved.
#
# Script for batch proving several libraries in PVS 
#

PVSPATH=@PVSPATH@

#-------------------------------------------------
# Nothing below this line should need modification

export PVSIOTCCS=nil
export PVSIOVERB=nil
export PVSIOTIME=nil
export PVSIOPROMPTIN="<PVSio> "
export PVSIOPROMPTOUT="==>~%"

PACK=
DEBUG=

readVersion() {
    if ! type "$PVSPATH/pvs" > /dev/null 2>&1  || ! VERSION=$($PVSPATH/pvs -raw -E '(format t "~&~%PVSIOVERSION ~a~%~%" *pvsio-version*)(bye)' | grep PVSIOVERSION | sed 's/^.*PVSIOVERSION \(.*\)$/\1/g') ; then
	printf "PVS could not be located. Please double check PVS installation.\n"
	exit 1;
    fi
}

usage() {
    readVersion
    echo "PVSio $VERSION -- pvsio is a command-line utility to run the PVSio ground evaluator.

Usage: pvsio <option>* [<pvsfile>][@<theory>[:[<main>]]]
where <option> can be
  -h|--help                
   Print this message
  -p|--packages <P1>,..,<Pn>   
   Load packages (prelude libraries) <P1>,..,<Pn>
  -promptin <string>
   Change prompt \"$PVSIOPROMPTIN\" to <string>
  -promptout <string>
   Change prompt \"$PVSIOPROMPTOUT\" to <string>
  -t|--tccs                
   Generate TCCs     
  -T|--timing              
   Print timing information for each evaluation
  -v|--version             
   Print PVSio version
  -V|--verbose             
   Print typechecking information
  -l|--lisp allegro|cmulisp,sbclisp 
   Specify a particular PVS binary to execute PVSio. Use this option only 
   if you know what you are doing.

One-letter options can be combined.

Typical use:
  * pvsio <pvsfile.pvs>
    Load PVS file pvsfile.pvs and start PVSio read-and-eval loop
  * pvsio @<theory>
    Load PVS theory <theory> from file <theory>.pvs and start PVSio 
    read-and-eval loop
  * pvsio @<theory>:
    Load PVS theory <theory> from file <theory>.pvs and ground evaluate 
    function \"main\".
  * pvsio @<theory>:<f> <a1> ... <an>
    Load PVS theory <theory> from file <theory>.pvs and ground evaluate
    function f(a1,...,an) 
  * pvsio <file>@<theory>:<f> <a1> ... <an>
    Load PVS thoery <theory> from file <file>.pvs and ground evaluate
    function f(a1,...,an)
"  
}

while [ $# -gt 0 ]
do
  case $1 in
      -debug|--debug)
        DEBUG=yes;;
      -h|-help|--help)     
	  usage
	  exit 0;;
      -l|-lisp|--lisp)    
	  case $2 in
	      allegro) PVSLISP='-lisp allegro';;
	      cmulisp) PVSLISP='-lisp cmulisp';;
	      sbclisp) PVSLISP='-lisp sbclisp';;
	      *) echo "Only allegro, cmulisp, and sbclisp are currently available"
		  exit 1;;
	  esac
	  shift;;
      -p|-packages|--packages) 
	  if [ "$PACK" ]; then
  	    PACK="$PACK,$2"
          else
            PACK=$2
          fi
	  shift;;
      -promptin)
          PVSIOPROMPTIN="$2"
          shift;;
      -promptout)
          PVSIOPROMPTOUT="$2"
          shift;;
      -tccs|--tccs)        
	  PVSIOTCCS=t;;
      -timing|--timing) 
	  PVSIOTIME=t;;
      -verbose|--verbose)
	  PVSIOVERB=t;;
      -v|-version|--version)  
	  readVersion
	  printf "$VERSION\n"
	  exit 0;;
      -*)           
	  OPTS=`echo "$1" | sed -e s/-//g -e "s/\(.\)/\1 /g"`
	  for opt in $OPTS
	    do
	    case $opt in
		t)     
		    PVSIOTCCS=t;;
		T)   
		    PVSIOTIME=t;;
		V)   
		    PVSIOVERB=t;;
		*) 
		    usage
		    echo "Error: -$opt is not a valid option"
		    exit 1;;
	    esac
	  done;;  
      *)            
	  ARG="$1"
	  shift
	  if [ "$1" ]; then
            PARAM="$1"
	    shift
          fi
          while [ $# -gt 0 ]
          do
            PARAM="$PARAM,$1"
            shift
          done
	  break
  esac
  shift
done

if [ "$PACK" ]; then
    PACK=`echo "(\"$PACK\")" | sed -e "s/,/\" \"/g"`
else
    PACK=nil
fi

if [ -z "$ARG" ]; then
  echo "pvsio__ : THEORY BEGIN pvsio__ : void = TRUE END pvsio__" > /tmp/pvsio__.pvs
  ARG="/tmp/pvsio__"
fi

MAIN=

case $ARG in
  *@*) FILE=`echo $ARG | sed -e "s/\([^@]*\)@.*/\1/"`
       THMA=`echo $ARG | sed -e "s/[^@]*@//"`;;
  *)   FILE=$ARG
esac

case $THMA in
  *:*) THEORY=`echo $THMA | sed -e "s/\([^:]\):.*$/\1/"`
       MAIN=`echo $THMA | sed -e "s/[^:]*://"`
       if [ -z "$MAIN" ]; then
         MAIN="main"
       fi
       if [ "$PARAM" ]; then
         MAIN="$MAIN($PARAM)"
       fi;;
  *)   THEORY=$THMA
esac

if [ "$THMA" -a -z "$FILE" ]; then
  FILE=$THEORY
fi

DIR=`dirname $FILE`
if [ "$DIR" = "." ]; then
    DIR=`pwd -P`
fi
NAME=`basename $FILE .pvs`
FILE="$DIR/$NAME"

if [ ! -f "$FILE.pvs" ]; then
  echo Error: "File $FILE.pvs doesn't exist"
  exit 0
fi

if [ -z "$THEORY" ]; then
  THEORY=$NAME
fi

export PVSIOFILE=$FILE
export PVSIOTHEORY=$THEORY
export PVSIOPACK=$PACK
export PVSIOMAIN=$MAIN

if [ "$DEBUG" ]; then
  echo "*** PVSio Environment Variables"
  echo "\$PVSIOFILE=$PVSIOFILE"
  echo "\$PVSIOTHOERY=$PVSIOTHEORY"
  echo "\$PVSIOPACK=$PVSIOPACK"
  echo "\$PVSIOMAIN=$PVSIOMAIN"
fi

if [ "$PVSIOMAIN" -a "$PVSIOVERB" = nil ]; then
    $PVSPATH/pvs -raw $PVSLISP -E "(run-pvsio)" | awk '
BEGIN { beginpvsio = 0 }
/Starting pvsio script/ { beginpvsio = 1; getline }
beginpvsio == 1 { print }
END { }
'
else 
    $PVSPATH/pvs -raw $PVSLISP -E "(run-pvsio)"
fi