why3 1.49 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 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 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
#!/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
  echo "  Process files generated by Why3"
  exit 1
}


## utilities

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

  if [ ! -e "$1.thy" ]; then
    sed \
      -e "s/<theory[^>]*>/theory $BNAME\nimports Why3\nbegin\n\nwhy3_open \"$BNAME\.xml\"\n\n/g" \
      -e 's/<lemma name="\([^"]*\)"[^>]*>/why3_vc \1\n\n/g' \
      -e 's/<\/theory>/why3_end\n\nend\n/g' \
      -e 's/<[^tl\/][^>]*>//g' \
      -e 's/<type[^>]*>//g' \
      -e 's/<tvar[^>]*>//g' \
      -e 's/<\/[^t][^>]*>//g' \
      -e 's/<\/type[^>]*>//g' \
      -e 's/<\/tvar[^>]*>//g' \
      "$1.xml" > "$1.thy"
  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))

if [ "$1" = "" ]; then
  usage
else
  NAME=`dirname "$1"`/`basename "$1" .xml`
fi

if [ "$BATCH" = true ]; then
  $ISABELLE_PROCESS -e "use_thy \"$NAME\";" -rq Why3
elif [ "$INTERACTIVE" = true ]; then
  if [ "$INTERFACE" = emacs ]; then
    LOGIC="-L"
  else
    LOGIC="-l"
  fi
  make_theory "$NAME"
  $ISABELLE_TOOL $INTERFACE $LOGIC Why3 "$NAME.thy"
else
  usage
fi