why3 1.49 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
37
    echo -e "theory $BNAME\nimports 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

if [ "$BATCH" = true ]; then
74
  "$ISABELLE_PROCESS" -e "use_thy \"$NAME\";" -rq Why3
75 76
elif [ "$INTERACTIVE" = true ]; then
  make_theory "$NAME"
Stefan Berghofer's avatar
Stefan Berghofer committed
77 78 79 80 81 82 83
  if [ -f "$JEDIT_SETTINGS/$WHY3_JEDIT_SERVER" ]; then
    "$ISABELLE_TOOL" java -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
      "-settings=$(jvmpath "$JEDIT_SETTINGS")" "-server=$WHY3_JEDIT_SERVER" \
      -reuseview -wait "$(jvmpath "${NAME}.thy")"
  else
    "$ISABELLE_TOOL" jedit -l Why3 "${NAME}.thy"
  fi
84 85 86
else
  usage
fi