#!/bin/sh
java.lang.NullPointerException
# proveit.in
# Release: ProofLite-6.0.9 (3/14/14)
java.lang.NullPointerException
# Contact: Cesar Munoz (cesar.a.munoz@nasa.gov)
# NASA Langley Research Center
# http://shemesh.larc.nasa.gov/people/cam/ProofLite
java.lang.NullPointerException
# 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.
java.lang.NullPointerException
# Script for batch proving in PVS 
#  

PVSPATH=@PVSPATH@
VERSION="ProofLite-6.0.9 (3/14/14)"

export PROVEITVERSION="proveit - $VERSION"

#-------------------------------------------------
# Nothing below this line should need modification
java.lang.NullPointerException

# Extension for proof status summary file
EXT=.summary

# PVS directory of binary files
PVSBIN=pvsbin
LISPFORCE=t
LISPIMPORT=nil
LISPSCRIPTS=t
LISPTRACES=nil
LISPTXTPROOFS=nil
LISPTEXPROOFS=nil
LISPTYPECHECK=nil
LISPDEPENDENCIES=nil
PRELUDEXT=
DISABLE=
ENABLE=
CLEAN=
LOG=
QUIET=
DEBUG=
OUTDIR=
TOP=top
NOFILE=yes

reset_vars() {
  FILENOTFOUND=
  ARG=
  OPTS=  
  OUTFILE=
  LOGFILE=
  PVSCONTEXT=
  PVSFILE=
  THFS=
  THEORIES=  
  LISPDEPENDENCIES=nil
}

all_opt() {
  if [ -z "$FILENOTFOUND" ]; then
    QUIET=yes
    if [ -z "$CLEAN" ]; then
 CLEAN=yes
    fi
    if [ "$CLEAN" = "only" ]; then
 QUIET=
    fi
    LISPIMPORT=t
    LISPSCRIPTS=nil
  fi
}


# $ARG has the general form
# <dir> | <file>[.pvs] | [<dir>@]<thf1>,..,<thfn>, where 
# <thfi> has the form <th>[.<f1>:..:<fm>]

compile_infile_name() {
  # If <dir>, set context to <dir> and pvsfile to top.pvs
  if [ -d $ARG ]; then
    PVSCONTEXT=$ARG
    if [ -z "$OUTFILE" ]; then
      OUTFILE=$ARG$EXT
    fi
    PVSFILE=`basename $TOP .pvs`
    if [ -f $PVSCONTEXT/$PVSFILE.pvs ]; then
 all_opt
    else
 FILENOTFOUND="$PVSCONTEXT/$PVSFILE.pvs"
    fi
    LISPDEPENDENCIES=t
  # If  <file>, set context to its dirname and pvsfile to its base name
  else 
    PVSCONTEXT=`dirname $ARG`
    PVSFILE=`basename $ARG .pvs`
    if [ ! -f $PVSCONTEXT/$PVSFILE.pvs ]; then
 case $ARG in
     *@*) predir=`echo $ARG | sed -e "s/\([^@]*\)@.*/\1/"`
  THFS=`echo $ARG | sed -e "s/[^@]*@//"`
  if [ -z "$predir" ]; then
      PVSCONTEXT="."
  else 
      if [ -d "$predir" ]; then
   PVSCONTEXT=$predir
      else
   echo "Error: $predir is not a directory"
   exit 1
      fi
  fi
  if [ "$THFS" ]; then
      PVSFILE=$THFS
      THEORIES=`echo $THFS | sed -e "s/\..*,/,/g" -e "s/\..*//"`
  else
      echo "Error: At least one theory has to be specified in $ARG"
      exit 1
  fi;;
     *)  FILENOTFOUND="$PVSCONTEXT/$PVSFILE.pvs"
  if [ -z "$NOFILE" ]; then
      echo "Error: File $FILENOTFOUND not found"
      exit;
  fi;;
         
 esac
    fi
  fi
}

strip_ext() {
  echo "$1" | sed -e "s/\(.*\)\..*/\1/g" 
}

# If necessary, set the name of the output file
java.lang.NullPointerException
compile_outfile_names() {
    dir=$OUTDIR
    if [ -z "$OUTFILE" ]; then
 if [ -z "$dir" ]; then
     dir=$PVSCONTEXT
 fi
 OUTFILE=$PVSFILE$EXT
    else 
      if [ -z "$dir" ]; then
        dir=`dirname $OUTFILE`
      fi
    fi
    base=`basename $OUTFILE`
    BASEOUT=`strip_ext $base`
    if [ "$BASEOUT" = $base ]; then
      base=$BASEOUT$EXT
    fi
    OUTFILE=$dir/$base
    LOGFILE=$dir/$BASEOUT.log
    if [ "$LISPTYPECHECK" = "t" ]; then 
 OUTFILE=$OUTFILE-tc
 LOGFILE=$LOGFILE
    fi
}

# Translate a list l1,...,ln into (l1 .. ln)
list_to_lisp() {
  if [ -z "$1" ]
  then 
      echo nil
  else
      echo "(\"$1\")" | sed -e "s/,/\" \"/g"
  fi
}

# append e l = e,le. Check for the special case when l is empty
append() {
    if [ -z "$2" ]; then
 echo "$1"
    else
 echo "$2,$1"
    fi
}

# Take care of the optional cleaning
java.lang.NullPointerException
cleanup() {
  if [ "$CLEAN" ]
  then 
    if [ -z "$QUIET" ]
    then
      echo "Removing $PVSCONTEXT/.pvscontext $PVSCONTEXT/$PVSBIN/ $OUTFILE $LOGFILE"
    fi
    rm -r -f $PVSCONTEXT/.pvscontext $PVSCONTEXT/$PVSBIN/*.* $OUTFILE $LOGFILE
  fi
}

# Help print command
#
usage() {
    echo "NAME
  $PROVEITVERSION -- runs PVS in batch mode

SYNOPSIS

  proveit <option> ... <dir> | <file>[.pvs] | [<ctxt>]@<thf1>,..,<thfn> ...
     where <thfi> has the form  <th>[.<f1>:..:<fm>]

DESCRIPTION
  If directory <dir> is provided, prove all theories imported in
  <dir>/top.pvs. If a PVS <file> is provided, prove all theories
  defined in it. The proof status is saved in the working directory in
  a file that can be specified using the option -out. Otherwise, a
  default name of the form <dir>$EXT or <file>$EXT is used depending
  on the given options.
 
TYPICAL USE
  * If <dir> is a library, e.g., there is a file <dir>/top.pvs that 
    imports all other theories in <dir>, then type: \$proveit <dir>
  * If <file>.pvs is a regular PVS file, then type: \$proveit <file>
  * If <file>.pvs is a regular PVS file and want to reprove all
    formulas, including those in imported files, then type:
    \$proveit -a <file>

ADVANCED USE
  In the more general form, a context,  a list of theories, and a list of 
  formulas are specified using the syntax <[ctxt]@thf1,..,thfn>,  where <ctxt> 
  is a directory and each <thfi> has the form <th[.f1:..:fm]> with <th> being a 
  theory and <f1:..:fn> a list of formulas in <th>. Only formulas specified
  this way are proven by PVS. In this case, the proof status is saved
  in <th.f1:..:fm>$EXT in <ctxt>. For example, to prove formulas <f1> and 
  <f2> in theory <theory> in the current context, type: 
  \$proveit @<theory>.<f1>:<f2>


OPTIONS
  Options are processed in the order they appear. One letter options can be 
  combined.

   -a|--all            equivalent to -ciq -p Field
   -c|--clean          remove bin files and .pvscontext
   -C|--clean-only     clean but do not typecheck or prove the theory
   -d|--dir <dir>      use <dir> as default directory of summary files
   --dependencies      compute theory dependencies and save them in pvsbin/<outfile>.dep.
                       By default, dependencies are computed when proving a directory 
   --disable <o1,..,on> disable external oracles o1,...,on
   --disable-oracles   disable any external oracle
   --enable <o1,..,on> enable external oracles o1,..,on. Overwrite --disable
   .<ext>              use <ext> as default extension of summary files
   -f|--force          force proof reruns (default)
   ~f|--no-force       don't force proof reruns 
   -h|--help           print this message
   -i|--importchain    prove chain of imported theories (set --no-scripts)
   ~i|--no-importchain don't prove chain of imported theories (default)
   --lisp <lisp>       specify lisp version; <lisp> is one of allegro,cmulisp
   -l|--log            log all information generated by PVS in <outfile>.log
   ~l|--no-log         don't log PVS information (default)
   -o|--out <outfile>  save the proof status summary in <outfile> 
   -p|--prelude-ext <p1,..,pn> load prelude extensions p1,..,pn 
   ~p|--no-prelude-ext don't load any prelude extension
   -q|--quiet          print only untried and unfinished proofs per theory,
                       and grand total  
   -s|--scripts        install ProofLite scripts (default)
   ~s|--no-scripts     don't install ProofLite scripts
   --tex               generate LaTeX proof files in directory pvstex
   --no-tex            don't generate LaTeX proof files (default)
   --txt               generate text proof files in directory pvstxt
   --no-txt            don't generate text proof files (default)
   -t|--top <th>       use <th>.pvs instead of top.pvs when proving a directory
   --traces            include proof traces in log file
   --no-traces         don't include proof traces in log file (default)
   -T|--typecheck-only typecheck but do not prove the theory
   -v|--verbose        print proof status information per theory and grand 
                       total (default)
   --version           print version information and exit

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

# Print error output
error_output() {
    sed -i.bak -n -e '/^<pvserror/,/^<\/pvserror/p'\
-e '/^Restored .*/d'\
 -e '/^\*\*\* /p'\
 -e '/^Typechecking/h'\
 -e '/^Typechecking/ !{
                 /^Typecheck error/ {
                   p;g;p
                 }
                 /^Typecheck error/! {
                   /^PVS file .* is not/h
                   /^PVS file .* is not/!H
                 }
              }'\
 -e '/Proof summary/,/Grand Totals/p' $OUTFILE 
    if [ -z "$QUIET" ]; then
 cat $OUTFILE | \
     sed -e "s+^<pvserror msg=\"\(.*\)\">+\1 ($ARG)+" \
            -e 's/"//g' -e '/^<\/pvserror>/d' \
     -e '/^\*\*\*.*/d' 
    else
 cat $OUTFILE | \
     sed -n -e "s+^<pvserror msg=\"\(.*\)\">+\1 ($ARG)+p" \
                   -e "s/^\"\(.*\)\"$/\1/p" -e "/^Typecheck error/p"
    fi
    if [ "$LOG" ]; then
 mv -f $OUTFILE.bak $LOGFILE
    else
 rm $OUTFILE.bak
    fi
}

# Pretty print PVS output
pvs_output() {
    sed -i.bak -n -e '/File .*\.pvs typechecked/p'\
        -e '/^\*\*\* /p'\
        -e '/Proof summary/,/Grand Totals/p' $OUTFILE
    cat $OUTFILE | quiet_output
    if [ "$LOG" ]; then
 mv -f $OUTFILE.bak $LOGFILE
    else
 rm $OUTFILE.bak
    fi
}

# quiet output
quiet_output() {
    if [ -z "$QUIET" ]
    then
 sed -n -e '/File/p'\
               -e '/Proof summary/h'\
               -e '/Proof summary/ !{
                    /unfinished/H
                    /unchecked/H
                    /untried/H
                   }'\
               -e '/Theory totals/ { 
                    i\

                    x;p;g;p
                  }' \
               -e '/^Grand Totals:/ {
                    i\

                    p
                  }'
    else
 sed -n -e '/Proof summary/h'\
               -e '/Proof summary/ !{
                    /unfinished/H
                    /unchecked/H
                    /untried/H
                   }'\
               -e '/Theory totals/ {
                   H;g
                   /\.\.\.\./p
                  }'\
               -e '/^Grand Totals:/p' 
    fi
}

process_opts() {
  while [ $# -gt 0 ]
  do
    case $1 in
 -a|all|--all)  
     all_opt;;
 -c|-clean|--clean)   
     CLEAN=yes;;
 -C|-Clean|--Clean|-clean-only|--clean-only)
     QUIET=
     CLEAN=only;;
        ~c|-no-clean|--no-clean)
     CLEAN=;;
        -dep|--dep|-dependencies|--dependencies)
     LISPDEPENDENCIES=t;;
 -f|-force|--force)   
     LISPFORCE=t;;
 ~f|-no-force|--no-force)   
     LISPFORCE=nil;;
 -i|-importchain|--importchain) 
     LISPSCRIPTS=nil
     LISPIMPORT=t;;
        ~i|-no-importchain|--no-importchain)
     LISPIMPORT=nil;;
 -s|-scripts|--scripts)
     LISPSCRIPTS=t;;
 ~s|-no-scripts|--no-scripts)
     LISPSCRIPTS=nil;;
        -T|-Typecheck|--Typecheck|-typecheck-only|--typecheck-only)
     LISPTYPECHECK=t;;
 -traces|--traces) 
     LOG=yes
     LISPTRACES=t;;
 -no-traces|--no-traces) 
     LISPTRACES=nil;;
 -txt|--txt)
     LISPTXTPROOFS=t;;
 -no-txt|--no-txt)
     LISPTXTPROOFS=nil;;
 -tex|--tex)
     LISPTEXPROOFS=t;;
 -no-tex|--no-tex)
     LISPTEXPROOFS=nil;;
 -l|-log|--log)
     LOG=yes;;
 ~l|-no-log|--no-log)
     LOG=;;
 ~p|-no-prelude-ext|--no-prelude-ext)
     PRELUDEXT=;;
 -q|-quiet|--quiet)
     QUIET=yes;;
 -v|-verbose|--verbose)
     QUIET=;;
 --*)           
     usage
     echo "Error: $1 is not a valid option"
     exit 1;;
 -*)
     opts=`echo "$1" | sed -e s/-//g -e "s/\(.\)/\1 /g"`
     for opt in $opts; do
       case $opt in
    a)     
        all_opt;;
    c)   
        CLEAN=yes;;
    C)
        QUIET=
        CLEAN=only;;
    f)   
        LISPFORCE=t;;
    s)
        LISPSCRIPTS=t;;
    v)  
        QUIET=;;
    i) 
        LISPSCRIPTS=nil
        LISPIMPORT=t;;
    l)
        LOG=yes;;
    q)
        QUIET=yes;;
    T)
        LISPTYPECHECK=t;;
    *) 
        usage
        echo "Error: -$opt is not a valid option"
        exit 1;;
       esac
     done;;
 ~*)
     opts=`echo "$1" | sed -e s/~//g -e "s/\(.\)/\1 /g"`
     for opt in $opts; do
       case $opt in
    c)
        CLEAN=;;
    f)   
        LISPFORCE=nil;;
    i)
        LISPIMPORT=nil;;
    s)
        LISPSCRIPTS=nil;;
    l) 
        LOG=;;
    p)  
        PRELUDEXT=;;
    *) 
        usage
        echo "Error: ~$opt is not a valid option"
        exit 1;;
       esac
     done
    esac
    shift
  done
}

# Main Function
proveit() {
  compile_infile_name
  if [ "$CLEAN" = "only" ]; then
      cleanup
  else
      process_opts $OPTS
      if [ "$DEBUG" ]; then
   QUIET=
   LOG=y
      fi
      compile_outfile_names
      cleanup
      
      if [ "$FILENOTFOUND" ]; then
   if [ -z "$CLEAN" ]; then
       echo "Error: File $FILENOTFOUND not found"
   fi
   exit 1
      fi
      
      echo Processing $PVSCONTEXT/$PVSFILE.pvs. Writing output to file $OUTFILE
      if [ "$LOG" ]; then
   echo "Logging PVS information in $LOGFILE"
      fi
      if [ -z "$QUIET" ]; then
   if [ "$PRELUDEXT" ]; then
       echo "Loading prelude extensions: $PRELUDEXT"
   fi
   if [ "$DISABLE" ]; then
       if [ "$DISABLE" = "_" ]; then
                  echo "Disabling any external oracle"
              else
     echo "Disabling oracles: $DISABLE"
       fi
   fi
   if [ "$ENABLE" ]; then
        echo "Enabling oracles: $ENABLE"
   fi
   if [ "$LISPIMPORT" = "t" ]; then
       echo "Proving chain of imported theories"
   fi 
   if [ "$LISPDEPENDENCIES" ]; then
       echo "Saving theory dependencies in directory pvsbin"
   fi
   if [ "$LISPSCRIPTS" != "t" ]; then
       echo "ProofLite scripts won't be installed"
   fi 
   if [ "$LISPFORCE" != "t" ]; then
       echo "Proofs won't be forced"
   fi
   if [ "$LISPTRACES" = "t" ]; then
       echo "Including proof traces in output file"
   fi
   if [ "$LISPTXTPROOFS" = "t" ]; then
       echo "Generating text proof files in directory pvstxt"
   fi
   if [ "$LISPTEXPROOFS" = "t" ]; then
       echo "Generating LaTeX proof files in directory pvstex"
   fi
      fi
      
      export PROVEITPVSCONTEXT="$PVSCONTEXT"
      export PROVEITPVSFILE="$PVSFILE"
      export PROVEITBASEOUT="$BASEOUT"
      export PROVEITLISPIMPORT="$LISPIMPORT"
      export PROVEITLISPSCRIPTS="$LISPSCRIPTS"
      export PROVEITLISPTRACES="$LISPTRACES"
      export PROVEITLISPFORCE="$LISPFORCE"
      export PROVEITLISPTYPECHECK="$LISPTYPECHECK"
      export PROVEITLISPTXTPROOFS="$LISPTXTPROOFS"
      export PROVEITLISPTEXPROOFS="$LISPTEXPROOFS"
      export PROVEITLISPDEPENDENCIES="$LISPDEPENDENCIES"
      export PROVEITLISPPRELUDEXT="`list_to_lisp $PRELUDEXT`"
      export PROVEITLISPDISABLE="`list_to_lisp $DISABLE`"
      export PROVEITLISPENABLE="`list_to_lisp $ENABLE`"
      export PROVEITLISPTHFS="`list_to_lisp $THFS`"
      export PROVEITLISPTHEORIES="`list_to_lisp $THEORIES`"
      
      if [ "$DEBUG" ]; then
   echo "PROVEITVERSION: $PROVEITVERSION"
   echo "OUTFILE: $OUTFILE"
   echo "LOGFILE: $LOGFILE"
   echo "PROVEITPVSCONTEXT: $PROVEITPVSCONTEXT"
   echo "PROVEITPVSFILE: $PROVEITPVSFILE"
   echo "PROVEITBASEOUT: $PROVEITBASEOUT"
   echo "PROVEITLISPIMPORT: $PROVEITLISPIMPORT"
   echo "PROVEITLISPSCRIPTS: $PROVEITLISPSCRIPTS"
   echo "PROVEITLISPTRACES: $PROVEITLISPTRACES"
   echo "PROVEITLISPFORCE: $PROVEITLISPFORCE" 
   echo "PROVEITLISPTYPECHECK: $PROVEITLISPTYPECHECK"
   echo "PROVEITLISPTXTPROOFS: $PROVEITLISPTXTPROOFS"
   echo "PROVEITLISPTEXPROOFS: $PROVEITLISPTEXPROOFS"
   echo "PROVEITLISPDEPENDENCIES: $PROVEITLISPDEPENDENCIES"
   echo "PROVEITLISPPRELUDEXT: $PROVEITLISPPRELUDEXT"
   echo "PROVEITLISPDISABLE: $PROVEITLISPDISABLE"
   echo "PROVEITLISPENABLE: $PROVEITLISPENABLE"
   echo "PROVEITLISPTHFS: $PROVEITLISPTHFS"
   echo "PROVEITLISPTHEORIES: $PROVEITLISPTHEORIES"
      fi
      
      $PVSPATH/pvs -raw $PVSLISP -E "(proveit)" > $OUTFILE
      
      if [ $? = 0 ]; then
   error_output
   exit 1
      fi
      pvs_output
  fi
  reset_vars
}

# ... and go!
java.lang.NullPointerException

reset_vars
while [ $# -gt 0 ]
do
  case $1 in
    --debug)
      DEBUG=yes;;
    -h|-help|--help)    
   usage
   exit 0;;
    -version|--version)     
   echo $PROVEITVERSION
   exit 0;;
    .*) 
      EXT=$1;;
    -lisp|--lisp)    
   case $2 in
       allegro) 
    LISP='allegro';;
       cmulisp) 
    LISP='cmulisp'
    PVSBIN='PVSBIN';;
       sbclisp)
    LISP='sbclisp'
    PVSBIN='PVSBIN';;
       *) 
    echo "Error: Only allegro, cmulisp, and sbcl are currently available"
    exit 1;;
   esac
   if [ "$LISP" ]; then
       PVSLISP="-lisp $LISP"
   fi
   shift;;
    -d|-dir|--dir)           
   if [ -d "$2" ]; then
       OUTDIR=$2
          else
        echo "Error: $2 is not a directory"
       exit 1
   fi
   shift;;
    -t|-top|--top)           
   TOP=$2
   shift;;
    -C|-Clean|--Clean|-clean-only|--clean-only)
   QUIET=
   CLEAN=only;;
    -o|-out|--out)           
   if [ -d "$2" ]; then
       echo "Error: $2 is a directory"
       exit 1
          else
        OUTFILE=$2
   fi
   shift;;
    -p|-prelude-ext|--prelude-ext) 
   PRELUDEXT=`append $2 $PRELUDEXT`
   shift;;
    -disable|--disable) 
   DISABLE=`append $2 $DISABLE`
   shift;;
    -disable-oracles|--disable-oracles) 
   DISABLE="_";;
    -enable|--enable) 
   ENABLE=`append $2 $ENABLE`
   shift;;
    -*|~*) OPTS="$OPTS $1";;
    *)     ARG=$1
     NOFILE=
           proveit
  esac
  shift 
done 
if [ "$NOFILE" ]; then
  ARG=$TOP.pvs
  if [ -f $ARG -o "$CLEAN" = "only" ]; then
    proveit
  else
    echo "Usage: proveit [--help | <option> ...] <file>.pvs"
  fi
fi

exit 0