src/Tools/Code/lib/Tools/codegen

modernized structure ProofContext;

#!/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 (Proof_Context.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 _ = quick_and_dirty := $QUICK_AND_DIRTY; \
  val cmd_expr = \"$CODE_EXPR\"; \
  val ml_cmd = \"Code_Target.codegen_tool thyname cmd_expr\"; \
  $FORMAL_CMD"

"$ISABELLE_PROCESS" -r -q -e "$ACTUAL_CMD" "$IMAGE" || exit 1