why3 1.76 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
#!/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"
  echo "    -i NAME      interactive mode using interface NAME"
  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 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
  fi
}


## process command line

while getopts "bi:" OPT
do
  case "$OPT" in
    b)
      BATCH=true
      ;;
    i)
      INTERACTIVE=true
      INTERFACE="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done


## main

shift $(($OPTIND - 1))

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

NAME=`dirname "$1"`/`basename "$1" .xml`
73 74

if [ "$BATCH" = true ]; then
75
  "$ISABELLE_PROCESS" -e "use_thy \"$NAME\";" -rq Why3
76 77
elif [ "$INTERACTIVE" = true ]; then
  make_theory "$NAME"
78 79
  case "$INTERFACE" in
    emacs)
80
      "$ISABELLE_TOOL" emacs -L Why3 "${NAME}.thy"
81 82
      ;;
    jedit)
83 84 85 86
      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")"
87
      else
88
        "$ISABELLE_TOOL" jedit -l Why3 "${NAME}.thy"
89 90
      fi
      ;;
91 92 93
    *)
      fail "Unknown Isabelle interface: \"$INTERFACE\""
      ;;
94
  esac
95 96 97
else
  usage
fi