bin/isabelle-process

Reintroduce set_interpreter for Collect and op :.
I removed them by accident when removing old code that dealt with the "set" type.
Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).

#!/usr/bin/env bash
#
# Author: Markus Wenzel, TU Muenchen
#
# Isabelle process startup script.

if [ -L "$0" ]; then
  TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
  exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
fi


## settings

PRG="$(basename "$0")"

ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2


## diagnostics

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
  echo
  echo "  Options are:"
  echo "    -C           tell ML system to copy output image"
  echo "    -I           startup Isar interaction mode"
  echo "    -P           startup Proof General interaction mode"
  echo "    -S           secure mode -- disallow critical operations"
  echo "    -X           startup PGIP interaction mode"
  echo "    -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream"
  echo "    -c           tell ML system to compress output image"
  echo "    -e MLTEXT    pass MLTEXT to the ML session"
  echo "    -f           pass 'Session.finish();' to the ML session"
  echo "    -m MODE      add print mode for output"
  echo "    -q           non-interactive session"
  echo "    -r           open heap file read-only"
  echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
  echo "    -w           reset write permissions on OUTPUT"
  echo
  echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
  echo "  These are either names to be searched in the Isabelle path, or"
  echo "  actual file names (containing at least one /)."
  echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

# options

COPYDB=""
ISAR=false
PROOFGENERAL=""
SECURE=""
WRAPPER_OUTPUT=""
PGIP=""
COMPRESS=""
MLTEXT=""
MODES=""
TERMINATE=""
READONLY=""
NOWRITE=""

while getopts "CIPSW:Xce:fm:qruw" OPT
do
  case "$OPT" in
    C)
      COPYDB=true
      ;;
    I)
      ISAR=true
      ;;
    P)
      PROOFGENERAL=true
      ;;
    S)
      SECURE=true
      ;;
    W)
      WRAPPER_OUTPUT="$OPTARG"
      ;;
    X)
      PGIP=true
      ;;
    c)
      COMPRESS=true
      ;;
    e)
      MLTEXT="$MLTEXT $OPTARG"
      ;;
    f)
      MLTEXT="$MLTEXT Session.finish();"
      ;;
    m)
      if [ -z "$MODES" ]; then
        MODES="\"$OPTARG\""
      else
        MODES="\"$OPTARG\", $MODES"
      fi
      ;;
    q)
      TERMINATE=true
      ;;
    r)
      READONLY=true
      ;;
    u)
      MLTEXT="$MLTEXT use\"ROOT.ML\";"
      ;;
    w)
      NOWRITE=true
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

INPUT=""
OUTPUT=""

if [ "$#" -ge 1 ]; then
  INPUT="$1"
  shift
fi

if [ "$#" -ge 1 ]; then
  OUTPUT="$1"
  shift
fi

[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }


## check ML system

[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."


## input heap file

[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"

case "$INPUT" in
  RAW_ML_SYSTEM)
    INFILE=""
    ;;
  */*)
    INFILE="$INPUT"
    [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
    ;;
  *)
    INFILE=""
    ISA_PATH=""

    ORIG_IFS="$IFS"
    IFS=":"
    for DIR in $ISABELLE_PATH
    do
      DIR="$DIR/$ML_IDENTIFIER"
      ISA_PATH="$ISA_PATH  $DIR\n"
      [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
    done
    IFS="$ORIG_IFS"

    if [ -z "$INFILE" ]; then
      echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
      echo -ne "$ISA_PATH" >&2
      exit 2
    fi
    ;;
esac


## output heap file

case "$OUTPUT" in
  "")
    [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
    ;;
  */*)
    OUTFILE="$OUTPUT"
    ;;
  *)
    mkdir -p "$ISABELLE_OUTPUT"
    OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
    ;;
esac


## prepare tmp directory

[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
ISABELLE_PID="$$"
ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
mkdir -p "$ISABELLE_TMP"


## run it!

ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)

[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"

[ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"

NICE="nice"
if [ -n "$WRAPPER_OUTPUT" ]; then
  [ "$WRAPPER_OUTPUT" = "-" -o -p "$WRAPPER_OUTPUT" ] || fail "Bad named pipe: $WRAPPER_OUTPUT"
  MLTEXT="$MLTEXT; IsabelleProcess.init \"$WRAPPER_OUTPUT\";"
elif [ -n "$PGIP" ]; then
  MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
elif [ -n "$PROOFGENERAL" ]; then
  MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
elif [ "$ISAR" = true ]; then
  MLTEXT="$MLTEXT; Isar.main();"
else
  NICE=""
fi

export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \
  ISABELLE_PID ISABELLE_TMP

if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
  $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
else
  $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
fi
RC="$?"

rmdir "$ISABELLE_TMP"

exit "$RC"