#!/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"