export.sh revision 067b7cf571968fe8e91212059da1590c2dfa741a
# ISABELLE_BIN_PATH (if isabelle is not located in PATH)
if [ -z $1 ]; then
echo "Nothing to translate!"
exit 1
fi
echo "Cannot read file $TRANS.thy"
exit 1
fi
if [ ! -z $ISABELLE_BIN_PATH ]; then
ISABELLE="$ISABELLE_BIN_PATH/isabelle"
if [ ! -e $ISABELLE ]; then
echo "Cannot find isabelle executable. Maybe you didn't specify ISABELLE_BIN_PATH correctly?"
fi
else
if [ ! $? ]; then
echo "Cannot find isabelle executable. Maybe you need to specify ISABELLE_BIN_PATH"
exit 1
fi
fi
if [ ! -x $ISABELLE ]; then
echo "$ISABELLE is not executable"
exit 1
fi
(
echo "theory IsaExport"
echo "imports \"$TRANS\""
echo "begin"
echo "ML {*"
echo "val T = Thy_Info.get_theory \"$TRANS_T\";
use \"$SCRIPTPATH/export_helper.ml\";
val types = ExportHelper.get_datatypes T;
val gths = ExportHelper.get_generated_theorems T types;
val consts = ExportHelper.get_consts T;
val axioms = ExportHelper.get_axioms T;
val theorems = ExportHelper.filter gths (ExportHelper.get_theorems T);
val num_consts = List.length consts;
val num_axioms = List.length axioms;
val num_theorems = List.length theorems;
val t1 = Option.valOf (Datatype.get_info T @{type_name type1});
val t2 = Option.valOf (Datatype.get_info T @{type_name type2});
(*val t1 = Option.valOf (#2 (List.hd types));
#alt_names t1;
#sorts t1;
Recdef.get_recdef T (Sign.intern_const T \"indicator\")*)"
echo "*}"
echo "end;"
#echo "ThyToOMDoc.ParseTheory \"$TRANS\";"