Isabelle/export/export.sh

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
0d295ebecb355c0f98d3f511619b14156d95e3d4Jonathan von Schroeder if uname | grep Darwin &> /dev/null ; 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
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroederimports Datatype FunDef Fixrec Domain
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);
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroederval v = fn s => out (1,\"Isabelle: \"^s);
baacb07fca6a4140974ce2a544edb755ede5a3c2Jonathan von Schroederval e = fn s => (out (0,s); OS.Process.exit OS.Process.failure)
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroederv \"Loading helper library\n\";
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederuse \"$SCRIPTPATH/parser.ml\";
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroederv \"Analyzing theory $TRANS_T\n\";
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder
90bbe729e1e28157a23bd04116e3856cba0b21b3Jonathan von Schroederval thys = Export.xml_of_theory v \"$TRANS.thy\"
90bbe729e1e28157a23bd04116e3856cba0b21b3Jonathan von Schroederhandle ex => e ((General.exnMessage ex)^\"\n\");
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroederval xml = XML.Elem ((\"Export\",[]),thys);
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroederv \"Writing theory information\n\";
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder(File.write (Path.explode \"$OUT_FILE\") (XML.string_of xml))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederhandle ex => e ((General.exnMessage ex)^\"\n\");
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder*}
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederend"
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder) | ($ISABELLE tty -l HOLCF) | tee $TEMP_FILE
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder
0d295ebecb355c0f98d3f511619b14156d95e3d4Jonathan von Schroederif grep "*** Error" $TEMP_FILE &> /dev/null ; 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