#!/usr/bin/env bash

 #

 # $Id$

 # Author: Markus Wenzel, TU Muenchen

 #

 # DESCRIPTION: build object-logic or run examples

 ## diagnostics

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

 function usage()

 {

   echo

   echo "Usage: $PRG [OPTIONS] LOGIC NAME"

   echo

   echo "  Options are:"

   echo "    -C BOOL      copy existing document directory to -D PATH (default true)"

   echo "    -D PATH      dump generated document sources into PATH"

   echo "    -M MAX       multithreading: maximum number of worker threads (default 1)"

   echo "    -P PATH      set path for remote theory browsing information"

   echo "    -T LEVEL     multithreading: trace level (default 0)"

   echo "    -V VERSION   declare alternative document VERSION"

   echo "    -b           build mode (output heap image, using current dir)"

   echo "    -c BOOL      tell ML system to compress output image (default true)"

   echo "    -d FORMAT    build document as FORMAT (default false)"

   echo "    -f NAME      use ML file NAME (default ROOT.ML)"

   echo "    -g BOOL      generate session graph image for document (default false)"

   echo "    -i BOOL      generate HTML and graph browser information (default false)"

   echo "    -m MODE      add print mode for output"

   echo "    -p LEVEL     set level of detail for proof objects"

   echo "    -r           reset session path"

   echo "    -s NAME      override session NAME"

   echo "    -v BOOL      be verbose (default false)"

   echo

   echo "  Build object-logic or run examples. Also creates browsing"

   echo "  information (HTML etc.) according to settings."

   echo

   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"

   echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"

   echo

   exit 1

 }

 function fail()

 {

   echo "$1" >&2

   exit 2

 }

 function check_bool()

 {

   [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\""

 }

 function check_number()

 {

   [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""

 }

 ## process command line

 # options

 COPY_DUMP=true

 DUMP=""

 MAXTHREADS="1"

 RPATH=""

 TRACETHREADS="0"

 DOCUMENT_VERSIONS=""

 BUILD=""

 COMPRESS=true

 DOCUMENT=false

 ROOT_FILE="ROOT.ML"

 DOCUMENT_GRAPH=false

 INFO=false

 MODES=""

 RESET=false

 SESSION=""

 PROOFS=0

 VERBOSE=false

 function getoptions()

 {

   OPTIND=1

   while getopts "C:D:M:P:T:V:bc:d:f:g:i:m:p:rs:v:" OPT

   do

     case "$OPT" in

       C)

         check_bool "$OPTARG"

         COPY_DUMP="$OPTARG"

         ;;

       D)

         DUMP="$OPTARG"

         ;;

       M)

         check_number "$OPTARG"

         MAXTHREADS="$OPTARG"

         ;;

       P)

         RPATH="$OPTARG"

         ;;

       T)

         check_number "$OPTARG"

         TRACETHREADS="$OPTARG"

         ;;

       V)

         if [ -z "$DOCUMENT_VERSIONS" ]; then

           DOCUMENT_VERSIONS="\"$OPTARG\""

         else

           DOCUMENT_VERSIONS="$DOCUMENT_VERSIONS, \"$OPTARG\""

         fi

         ;;

       b)

         BUILD=true

         ;;

       c)

         check_bool "$OPTARG"

         COMPRESS="$OPTARG"

         ;;

       d)

         DOCUMENT="$OPTARG"

         ;;

       f)

         ROOT_FILE="$OPTARG"

         ;;

       g)

         check_bool "$OPTARG"

         DOCUMENT_GRAPH="$OPTARG"

         ;;

       i)

         check_bool "$OPTARG"

         INFO="$OPTARG"

         ;;

       m)

         if [ -z "$MODES" ]; then

           MODES="\"$OPTARG\""

         else

           MODES="\"$OPTARG\", $MODES"

         fi

         ;;

       p)

         check_number "$OPTARG"

         PROOFS="$OPTARG"

         ;;

       r)

         RESET=true

         ;;

       s)

         SESSION="$OPTARG"

         ;;

       v)

         check_bool "$OPTARG"

         VERBOSE="$OPTARG"

         ;;

       \?)

         usage

         ;;

     esac

   done

 }

 getoptions $ISABELLE_USEDIR_OPTIONS

 getoptions "$@"

 shift $(($OPTIND - 1))

 # args

 [ "$#" -ne 2 ] && usage

 LOGIC="$1"; shift

 NAME="$1"; shift

 [ -z "$SESSION" ] && SESSION=$(basename "$NAME")

 ## main

 # prepare browser info dir

 if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then

   mkdir -p "$ISABELLE_BROWSER_INFO"

   cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"

   cp "$ISABELLE_HOME/lib/html/index.html" "$ISABELLE_BROWSER_INFO/index.html"

 fi

 # prepare log dir

 LOGDIR="$ISABELLE_OUTPUT/log"

 mkdir -p "$LOGDIR"

 # run isabelle

 PARENT=$(basename "$LOGIC")

 if [ -z "$BUILD" ]; then

   cd "$NAME" || fail "Bad session directory '$NAME'"

 fi

 if [ "$DOCUMENT" != false ]; then

   DOC="$DOCUMENT"

 else

   DOC=""

 fi

 . "$ISABELLE_HOME/lib/scripts/timestart.bash"

 if [ -n "$BUILD" ]; then

   ITEM="$SESSION"

   echo "Building $ITEM ..." >&2

   LOG="$LOGDIR/$ITEM"

   OPT_C=""

   [ "$COMPRESS" = true ] && OPT_C="-c"

   "$ISABELLE" \

     -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS;" \

     $OPT_C -q -w $LOGIC $NAME > "$LOG"

   RC="$?"

 else

   ITEM=$(basename "$LOGIC")-"$SESSION"

   echo "Running $ITEM ..." >&2

   LOG="$LOGDIR/$ITEM"

   "$ISABELLE" \

     -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS; quit();" \

     -r -q "$LOGIC" > "$LOG"

   RC="$?"

   cd ..

 fi

 . "$ISABELLE_HOME/lib/scripts/timestop.bash"

 # exit status

 if [ "$RC" -eq 0 ]; then

   echo "Finished $ITEM ($TIMES_REPORT)" >&2

   gzip --force "$LOG"

 else

   { echo "$ITEM FAILED";

     echo "(see also $LOG)";

     echo; tail "$LOG"; echo; } >&2

 fi

 exit "$RC"