bin/isabelle

also support higher-order rules for Z3 proof reconstruction

#!/usr/bin/env bash
#
# Author: Markus Wenzel, TU Muenchen
#
# Isabelle tool wrapper.

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

splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}")


## diagnostics

function usage()
{
  echo
  echo "Usage: $PRG NAME [ARGS ...]"
  echo
  echo "  Start Isabelle tool NAME with ARGS; pass \"-?\" for tool specific help."
  echo
  echo "  Available tools are:"
  for DIR in "${TOOLS[@]}"
  do
    if [ -d "$DIR" ]; then
      for TOOL in "$DIR"/*
      do
        if [ -f "$TOOL" -a -x "$TOOL" ]; then
          NAME="$(basename "$TOOL")"
          DESCRLINE="$(fgrep DESCRIPTION: "$TOOL" | sed -e 's/^.*DESCRIPTION: *//')"
          echo "    $NAME - $DESCRLINE"
        fi
      done
    fi
  done
  exit 1
}

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


## args

[ "$#" -lt 1 -o "$1" = "-?" ] && usage

TOOLNAME="$1"
shift


## main

for DIR in "${TOOLS[@]}"
do
  TOOL="$DIR/$TOOLNAME"
  [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
done

fail "Unknown Isabelle tool: $TOOLNAME"