#!/usr/bin/env bash
#
# Author: Florian Haftmann, TUM
#
# DESCRIPTION: issue code generation from shell
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [OPTIONS] IMAGE THYNAME CMD"
echo
echo " Options are:"
echo " -q run in quick'n'dirty mode"
echo
echo " Issues code generation using image IMAGE,"
echo " theory THYNAME,"
echo " with Isar command 'export_code CMD'"
echo
exit 1
}
## process command line
QUICK_AND_DIRTY="false"
while getopts "q" OPT
do
case "$OPT" in
q)
QUICK_AND_DIRTY="true"
;;
\?)
usage
;;
esac
done
shift $(($OPTIND - 1))
[ "$#" -ne 3 ] && usage
IMAGE="$1"; shift
THYNAME="$1"; shift
CODE_EXPR=$(echo "$1" | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
## invoke code generation
FORMAL_CMD="Toplevel.program (fn () => use_thy thyname; ML_Context.eval_text_in \
(SOME (ProofContext.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd) \
handle _ => OS.Process.exit OS.Process.failure;"
ACTUAL_CMD="val thyname = \"$THYNAME\"; \
val qnd = $QUICK_AND_DIRTY; \
val cmd_expr = \"$CODE_EXPR\"; \
val ml_cmd = \"Code_Target.codegen_tool thyname qnd cmd_expr\"; \
$FORMAL_CMD"
"$ISABELLE_PROCESS" -r -q -e "$ACTUAL_CMD" "$IMAGE" || exit 1