00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder#!/bin/bash
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder# ISABELLE_BIN_PATH (if isabelle is not located in PATH)
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederfunction path() {
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder if [ "${1%/*}" = "${1##*/}" ]; then
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo $(pwd -P)/$1
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder else
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder local P=`pwd`;
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder cd ${1%/*} &> /dev/null && echo $(pwd -P)/${1##*/};
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder local R=$?;
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder cd $P &> /dev/null;
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder return $R;
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder fi
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder}
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederSCRIPT=$(path $0)
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederSCRIPTPATH=`dirname "$SCRIPT"`
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederif [ -z $1 ]; then
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo "Nothing to translate!"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder exit 1
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederfi
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederif ! export TRANS=$(path $1); then
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo "Cannot find $1"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder exit 1
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederfi
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederTRANS_T=$(basename $TRANS .thy)
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederTRANS=$(dirname $TRANS)/$TRANS_T
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederif [ ! -r $TRANS.thy ]; then
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo "Cannot read file $TRANS.thy"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder exit 1
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederfi
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederif [ ! -z $ISABELLE_BIN_PATH ]; then
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder ISABELLE="$ISABELLE_BIN_PATH/isabelle"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder if [ ! -e $ISABELLE ]; then
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo "Cannot find isabelle executable. Maybe you didn't specify ISABELLE_BIN_PATH correctly?"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder exit 1
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder fi
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederelse
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder if which isabelle > /dev/null ; then
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder ISABELLE=`which isabelle`
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder else
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo "Cannot find isabelle executable. Maybe you need to specify ISABELLE_BIN_PATH?"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder exit 1
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder fi
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederfi
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederif [ ! -x $ISABELLE ]; then
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo "$ISABELLE is not executable"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder exit 1
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederfi
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederif which mktemp > /dev/null ; then
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder if uname | grep Darwin &> /dev/null ; then
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder TEMP_FILE=`mktemp isaexport.out`
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder else
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder TEMP_FILE=`mktemp`
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder fi
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederelse
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder TEMP_FILE="/tmp/isaexport.out"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederfi
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederecho "Starting Isabelle"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder(
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo "theory IsaExport
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederimports Datatype FunDef
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederbegin
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederML {*
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederuse \"$SCRIPTPATH/export_helper.ml\";
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederval s = File.read (Path.explode \"$TRANS.thy\");
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederval (th,err) = Parser.scan s |> Parser.test;
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von SchroederFile.write (Path.explode \"./test.out\") (Parser.scan s |> PolyML.makestring);
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder*}
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederend"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder) | ($ISABELLE tty) | tee $TEMP_FILE
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederif grep "*** Error" $TEMP_FILE &> /dev/null ; then
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo "Loading Theory failed"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder grep "\*\*\* " $TEMP_FILE | head -n-3
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder rm $TEMP_FILE
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder exit 1
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederfi
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederrm $TEMP_FILE