export.sh revision 6516023b9db74939c0a0f79fd6cc5bc7d9bab382
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder#!/bin/bash
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder# ISABELLE_BIN_PATH (if isabelle is not located in PATH)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von SchroederSCRIPT=$(readlink -f $0)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von SchroederSCRIPTPATH=`dirname $SCRIPT`
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederif [ -z $1 ]; then
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder echo "Nothing to translate!"
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder exit 1
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederfi
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von SchroederTRANS=$(readlink -f $1)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von SchroederTRANS_T=$(basename $TRANS .thy)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von SchroederTRANS=$(dirname $TRANS)/$TRANS_T
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederif [ ! -r $TRANS.thy ]; then
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder echo "Cannot read file $TRANS.thy"
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder exit 1
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederfi
067b7cf571968fe8e91212059da1590c2dfa741aJonathan 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
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder echo "Cannot find isabelle executable. Maybe you didn't specify ISABELLE_BIN_PATH correctly?"
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fi
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederelse
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder ISABELLE=`which isabelle`
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder if [ $? ]; then
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder echo "Cannot find isabelle executable. Maybe you need to specify ISABELLE_BIN_PATH"
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder exit 1
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fi
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederfi
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederif [ ! -x $ISABELLE ]; then
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder echo "$ISABELLE is not executable"
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder exit 1
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederfi
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroederecho $ISABELLE
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder(
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder echo "theory IsaExport"
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder echo "imports \"$TRANS\" Wellfounded"
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder echo "uses \"$SCRIPTPATH/export_helper.ml\""
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder echo "begin"
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder echo "ML {*"
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder echo "val T = Thy_Info.get_theory \"$TRANS_T\";
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroederval name = Context.theory_name T;
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederval types = ExportHelper.get_datatypes T;
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroederval consts = ExportHelper.filter (ExportHelper.get_gen_consts T name types)
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder (ExportHelper.get_consts T);
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroederval axioms = ExportHelper.filter (ExportHelper.get_gen_axioms T name types)
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder (ExportHelper.get_axioms T);
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroederval ths = ExportHelper.get_theorems T;
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroederval theorems = ExportHelper.filter (ExportHelper.get_gen_theorems T name types (List.map #1 ths))
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder ths;
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederval num_consts = List.length consts;
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederval num_axioms = List.length axioms;
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederval num_theorems = List.length theorems;
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder"
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder echo "*}"
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder echo "end;"
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder #echo "ThyToOMDoc.ParseTheory \"$TRANS\";"
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder) | ($ISABELLE tty -p "")