#!/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 "    -I           startup Isar interaction mode"

  echo "    -P           startup Proof General interaction mode"

  echo "    -S           secure mode -- disallow critical operations"

  echo "    -T ADDR      startup process wrapper, with socket address"

  echo "    -W IN:OUT    startup process wrapper, with input/output fifos"

  echo "    -X           startup PGIP interaction mode"

  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

ISAR=false

PROOFGENERAL=""

SECURE=""

WRAPPER_SOCKET=""

WRAPPER_FIFOS=""

PGIP=""

MLTEXT=""

MODES=""

TERMINATE=""

READONLY=""

NOWRITE=""

while getopts "IPST:W:Xe:fm:qruw" OPT

do

  case "$OPT" in

    I)

      ISAR=true

      ;;

    P)

      PROOFGENERAL=true

      ;;

    S)

      SECURE=true

      ;;

    T)

      WRAPPER_SOCKET="$OPTARG"

      ;;

    W)

      WRAPPER_FIFOS="$OPTARG"

      ;;

    X)

      PGIP=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=""

    splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")

    for DIR in "${PATHS[@]}"

    do

      DIR="$DIR/$ML_IDENTIFIER"

      ISA_PATH="$ISA_PATH  $DIR\n"

      [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"

    done

    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

  "")

    if [ -z "$READONLY" -a -w "$INFILE" ]; then

      perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"

    fi

    ;;

  */*)

    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="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT"

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

NICE="nice"

if [ -n "$WRAPPER_SOCKET" ]; then

  MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"

elif [ -n "$WRAPPER_FIFOS" ]; then

  splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")

  [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"

  [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"

  [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"

  MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"

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 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"