pvsio.in

#!/bin/sh
#
# pvsio.in
# Release: PVSio-6.0 (12/12/12)
#
# 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 PVSIOVERSION="PVSio-6.0 (12/12/12)"
export PVSIOPROMPTIN="<PVSio> "
export PVSIOPROMPTOUT="==>~%"

PACK=PVSio

usage() {
  echo "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.

  <pvsfile>@<theory>:<main>   
  Load <theory> from <pvsfile>, evaluate <main> and exit 

  One-letter options can be combined. If <theory> is not provided,
  it is assumed to have the same name as the name of the file. If <main> is
  not provided, PVSio starts a top level read-eval-loop.
"  
}

while [ $# -gt 0 ]
do
  case $1 in
      -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) 
	  PACK="$PACK,$2"
	  shift;;
      -promptin)
          PVSIOPROMPTIN="$2"
          shift;;
      -promptout)
          PVSIOPROMPTOUT="$2"
          shift;;
      -tccs|--tccs)        
	  PVSIOTCCS=t;;
      -timing|--timing) 
	  PVSIOTIME=t;;
      -verbose|--verbose)
	  PVSIOVERB=t;;
      -v|-version|--version)  
	  echo $PVSIOVERSION
	  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"
  esac
  shift
done

PACK=`echo "(\"$PACK\")" | sed -e "s/,/\" \"/g"`

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

DIR=`dirname $FILE`
NAME=`basename $FILE .pvs`
FILE="$DIR/$NAME"

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

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

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

if [ -z "$MAIN" ]
then MAIN=nil
else MAIN="\"$MAIN;\""
fi

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

$PVSPATH/pvs -raw $PVSLISP -E "(run-pvsio)"