why3 1.85 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
#!/usr/bin/env bash
#
# DESCRIPTION: process files generated by Why3


## diagnostics

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

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS] WHY3_FILE"
  echo
  echo "  Options are:"
  echo "    -b           batch mode"
Stefan Berghofer's avatar
Stefan Berghofer committed
17
  echo "    -i           interactive mode"
18
  echo
19
  echo "Process files generated by Why3."
20 21 22
  exit 1
}

23 24 25 26 27 28
function fail()
{
  echo "$1" >&2
  exit 2
}

29 30 31 32 33 34 35 36

## utilities

function make_theory()
{
  BNAME=`basename "$1"`

  if [ ! -e "$1.thy" ]; then
Stefan Berghofer's avatar
Stefan Berghofer committed
37
    echo -e "theory $BNAME\nimports Why3.Why3\nbegin\n\nwhy3_open \"$BNAME.xml\"\n" > "$1.thy"
38 39
    sed \
      -e 's/<lemma name="\([^"]*\)"[^>]*>/why3_vc \1\n\n/g' \
40 41 42
      -e 's/<[^l][^>]*>//g' \
      "$1.xml" >> "$1.thy"
    echo -e "why3_end\n\nend" >> "$1.thy"
43 44 45 46 47 48
  fi
}


## process command line

Stefan Berghofer's avatar
Stefan Berghofer committed
49
while getopts "bi" OPT
50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68
do
  case "$OPT" in
    b)
      BATCH=true
      ;;
    i)
      INTERACTIVE=true
      ;;
    \?)
      usage
      ;;
  esac
done


## main

shift $(($OPTIND - 1))

69 70 71
[ "$#" != 1 ] && usage

NAME=`dirname "$1"`/`basename "$1" .xml`
72

73 74 75 76 77 78 79 80 81 82 83 84
if [ "$ISABELLE_WHY3_SESSION" ]; then
  SESSION="$ISABELLE_WHY3_SESSION"
else
  SESSION=Why3
fi

if [ "$ISABELLE_WHY3_SESSION_DIR" ]; then
  SESSION_DIR=("-d" "$ISABELLE_WHY3_SESSION_DIR")
else
  SESSION_DIR=()
fi

85
if [ "$BATCH" = true ]; then
86 87 88 89 90
  if [ "$ISABELLE_ADDRESS" ]; then
    isabelle_client -t "$NAME"
  else
    "$ISABELLE_TOOL" process "${SESSION_DIR[@]}" -l "$SESSION" -T "$NAME"
  fi
91 92
elif [ "$INTERACTIVE" = true ]; then
  make_theory "$NAME"
Stefan Berghofer's avatar
Stefan Berghofer committed
93
  if [ -f "$JEDIT_SETTINGS/$WHY3_JEDIT_SERVER" ]; then
94 95 96
    "$ISABELLE_TOOL" java -jar "$(platform_path "$JEDIT_HOME/dist/jedit.jar")" \
      "-settings=$(platform_path "$JEDIT_SETTINGS")" "-server=$WHY3_JEDIT_SERVER" \
      -reuseview -wait "$(platform_path "${NAME}.thy")"
Stefan Berghofer's avatar
Stefan Berghofer committed
97
  else
98
    "$ISABELLE_TOOL" jedit "${SESSION_DIR[@]}" -l "$SESSION" "${NAME}.thy"
Stefan Berghofer's avatar
Stefan Berghofer committed
99
  fi
100 101 102
else
  usage
fi