Isabelle/export/export.sh

	export.sh revision 6df4343f46cc159371dfa671c5943354480f4e1c
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich#!/bin/bash
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich# ISABELLE_BIN_PATH (if isabelle is not located in PATH)
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichfunction path() {
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich    if [ "${1%/*}" = "${1##*/}" ]; then
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich        echo $(pwd -P)/$1
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich        else
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich        local P=`pwd`;
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich        cd ${1%/*} &> /dev/null && echo $(pwd -P)/${1##*/};
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich        local R=$?;
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich        cd $P &> /dev/null;
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich        return $R;
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich        fi
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus LuettichSCRIPT=$(path $0)
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus LuettichSCRIPTPATH=`dirname "$SCRIPT"`
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichif [ ! -z $3 ]; then
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich COMM_FILE="$3"
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichelse
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich COMM_FILE="/dev/stdin"
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichfi
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichif [ -z $1 ]; then
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich echo "v0:Nothing to translate!" > $COMM_FILE
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich exit 1
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichfi
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichif ! export TRANS=$(path $1); then
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich echo "v0:Cannot find $1" > $COMM_FILE
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich exit 1
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichfi
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus LuettichTRANS_T=$(basename $TRANS .thy)
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus LuettichTRANS=$(dirname $TRANS)/$TRANS_T
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichif [ ! -r $TRANS.thy ]; then
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich echo "v0:Cannot read file $TRANS.thy" > $COMM_FILE
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich exit 1
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichfi
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichif [ ! -z $2 ]; then
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich OUT_FILE="$2"
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichelse
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich OUT_FILE="$TRANS.isa"
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichfi
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichif [ ! -z $ISABELLE_BIN_PATH ]; then
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich ISABELLE="$ISABELLE_BIN_PATH/isabelle"
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich if [ ! -e $ISABELLE ]; then
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich  echo "v0:Cannot find isabelle executable. Maybe you didn't specify ISABELLE_BIN_PATH correctly?" > $COMM_FILE
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich  exit 1
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich fi
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichelse
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich if which isabelle > /dev/null ; then
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich   ISABELLE=`which isabelle`
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich else
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich  echo "v0:Cannot find isabelle executable. Maybe you need to specify ISABELLE_BIN_PATH?" > $COMM_FILE
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich  exit 1
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich fi
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichfi
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichif [ ! -x $ISABELLE ]; then
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich echo "v0:$ISABELLE is not executable" > $COMM_FILE
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich exit 1
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichfi
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichif which mktemp > /dev/null ; then
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich if uname | grep Darwin &> /dev/null ; then
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich  TEMP_FILE=`mktemp isaexport.out`
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich else
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich  TEMP_FILE=`mktemp`
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich fi
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichelse
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich TEMP_FILE="/tmp/isaexport.out"
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichfi
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichecho "v1:Starting Isabelle" > $COMM_FILE
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich(
 echo "theory IsaExport
imports Datatype FunDef
begin
ML {*

val out' = fn (f,i,s') =>
 let val s = \"v\"^(Int.toString i)^\":\"^s'
 in case f of
   \"/dev/stdin\" => TextIO.output (TextIO.stdOut,s)
   | _ => File.write (Path.explode f) s
 end;
val out = fn (i,s) => out' (\"$COMM_FILE\",i,s);
val v = fn s => out (1,s);
val e = fn s => out (0,s);

v \"Isabelle: Loading helper library\n\";
use \"$SCRIPTPATH/parser.ml\";

v \"Isabelle: Analyzing theory\n\";

val thy = Parser.scan \"$TRANS.thy\" |> Parser.thy;

v \"Isabelle: Exporting theory information\n\";
(File.write (Path.explode \"$OUT_FILE\")
 (XML.string_of (Export.xml_of_theory thy)))
handle ex => e ((General.exnMessage ex)^\"\n\");
*}
end"
) | ($ISABELLE tty) | tee $TEMP_FILE

if grep "*** Error" $TEMP_FILE &> /dev/null ; then
 echo "v0:Loading Theory failed" > $COMM_FILE
 grep "\*\*\* " $TEMP_FILE | head -n-3 > $COMM_FILE
 rm $TEMP_FILE
 exit 1
fi

rm $TEMP_FILE