Isabelle/export/export.sh

	export.sh revision 11bed5e9b739f03c810e816ddcbeb865aff352f3
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder#!/bin/bash
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder# ISABELLE_BIN_PATH (if isabelle is not located in PATH)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederfunction path() {
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder    if [ "${1%/*}" = "${1##*/}" ]; then
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder        echo $(pwd -P)/$1
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder        else
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder        local P=`pwd`;
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder        cd ${1%/*} &> /dev/null && echo $(pwd -P)/${1##*/};
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder        local R=$?;
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder        cd $P &> /dev/null;
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder        return $R;
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder        fi
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder}
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von SchroederSCRIPT=$(path $0)
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von SchroederSCRIPTPATH=`dirname "$SCRIPT"`
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederif [ ! -z $3 ]; then
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder COMM_FILE="$3"
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederelse
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder COMM_FILE="/dev/stdin"
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederfi
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederif [ -z $1 ]; then
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder echo "v0:Nothing to translate!" > $COMM_FILE
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder exit 1
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederfi
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederif ! export TRANS=$(path $1); then
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder echo "v0:Cannot find $1" > $COMM_FILE
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder exit 1
7bbfb15142ab4286dfc6fcde2fc94a5512297e41Jonathan von Schroederfi
7bbfb15142ab4286dfc6fcde2fc94a5512297e41Jonathan von Schroeder
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von SchroederTRANS_T=$(basename $TRANS .thy)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von SchroederTRANS=$(dirname $TRANS)/$TRANS_T
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederif [ ! -r $TRANS.thy ]; then
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder echo "v0:Cannot read file $TRANS.thy" > $COMM_FILE
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder exit 1
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederfi
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederif [ ! -z $2 ]; then
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder OUT_FILE="$2"
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederelse
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder OUT_FILE="$TRANS.isa"
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederfi
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederif [ ! -z $ISABELLE_BIN_PATH ]; then
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder ISABELLE="$ISABELLE_BIN_PATH/isabelle"
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder if [ ! -e $ISABELLE ]; then
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder  echo "v0:Cannot find isabelle executable. Maybe you didn't specify ISABELLE_BIN_PATH correctly?" > $COMM_FILE
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder  exit 1
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fi
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederelse
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder if which isabelle > /dev/null ; then
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder   ISABELLE=`which isabelle`
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder else
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder  echo "v0:Cannot find isabelle executable. Maybe you need to specify ISABELLE_BIN_PATH?" > $COMM_FILE
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder  exit 1
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fi
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederfi
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederif [ ! -x $ISABELLE ]; then
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder echo "v0:$ISABELLE is not executable" > $COMM_FILE
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder exit 1
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederfi
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederif which mktemp > /dev/null ; then
11bed5e9b739f03c810e816ddcbeb865aff352f3Jonathan von Schroeder if uname | grep -q Darwin ; then
11bed5e9b739f03c810e816ddcbeb865aff352f3Jonathan von Schroeder  TEMP_FILE=`mktemp isaexport.out`
11bed5e9b739f03c810e816ddcbeb865aff352f3Jonathan von Schroeder else
11bed5e9b739f03c810e816ddcbeb865aff352f3Jonathan von Schroeder  TEMP_FILE=`mktemp`
11bed5e9b739f03c810e816ddcbeb865aff352f3Jonathan von Schroeder fi
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederelse
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder TEMP_FILE="/tmp/isaexport.out"
7bbfb15142ab4286dfc6fcde2fc94a5512297e41Jonathan von Schroederfi
7bbfb15142ab4286dfc6fcde2fc94a5512297e41Jonathan von Schroeder
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederecho "v1:Starting Isabelle" > $COMM_FILE
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder(
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder echo "theory IsaExport
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederimports Datatype
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederbegin
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von SchroederML {*
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederval out' = fn (f,i,s') =>
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder let val s = \"v\"^(Int.toString i)^\":\"^s'
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder in case f of
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder   \"/dev/stdin\" => TextIO.output (TextIO.stdOut,s)
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder   | _ => File.write (Path.explode f) s
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder end;
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederval out = fn (i,s) => out' (\"$COMM_FILE\",i,s);
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederval v = fn s => out (1,s);
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederval e = fn s => (out (0,s); exit 1);
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederv \"Isabelle: Loading theory $TRANS\n\";
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederuse_thy \"$TRANS\";
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederv \"Isabelle: Loading helper library\n\";
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederuse \"$SCRIPTPATH/export_helper.ml\";
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederval T = Thy_Info.get_theory \"$TRANS_T\";
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederv \"Isabelle: Exporting theory information\n\";
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder(File.write (Path.explode \"$OUT_FILE\")
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder (XML.string_of (ExportHelper.tinfo2xml T \"$TRANS_T\"
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder  (ExportHelper.theory_info T))))
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederhandle ExportHelper.ExportError msg => e msg;
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder*}
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederend"
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder) | ($ISABELLE tty) | tee $TEMP_FILE
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederif grep -q "*** Error" $TEMP_FILE; then
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder echo "v0:Loading Theory failed" > $COMM_FILE
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder grep "\*\*\* " $TEMP_FILE | head -n-3 > $COMM_FILE
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder rm $TEMP_FILE
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder exit 1
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederfi
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederrm $TEMP_FILE