src/Tools/Code/lib/Tools/codegen
author haftmann
Wed Feb 13 13:38:52 2013 +0100 (2013-02-13)
changeset 51091 c007c6bf4a35
parent 48662 b171bcd5dd86
child 52059 2f970c7f722b
permissions -rwxr-xr-x
another attempt for a uniform abort on code generation errors
haftmann@21884
     1
#!/usr/bin/env bash
haftmann@21884
     2
#
haftmann@21884
     3
# Author: Florian Haftmann, TUM
haftmann@21884
     4
#
haftmann@21884
     5
# DESCRIPTION: issue code generation from shell
haftmann@21884
     6
haftmann@21884
     7
haftmann@21884
     8
PRG="$(basename "$0")"
haftmann@21884
     9
haftmann@21884
    10
function usage()
haftmann@21884
    11
{
haftmann@21884
    12
  echo
haftmann@39646
    13
  echo "Usage: isabelle $PRG [OPTIONS] IMAGE THYNAME CMD"
haftmann@32483
    14
  echo
haftmann@32483
    15
  echo "  Options are:"
haftmann@32483
    16
  echo "    -q    run in quick'n'dirty mode"
haftmann@21884
    17
  echo
haftmann@21884
    18
  echo "  Issues code generation using image IMAGE,"
haftmann@39646
    19
  echo "  theory THYNAME,"
haftmann@25611
    20
  echo "  with Isar command 'export_code CMD'"
haftmann@21884
    21
  echo
haftmann@21884
    22
  exit 1
haftmann@21884
    23
}
haftmann@21884
    24
haftmann@39646
    25
haftmann@21884
    26
## process command line
haftmann@21884
    27
haftmann@39646
    28
QUICK_AND_DIRTY="false"
haftmann@32483
    29
haftmann@32483
    30
while getopts "q" OPT
haftmann@32483
    31
do
haftmann@32483
    32
  case "$OPT" in
haftmann@32483
    33
    q)
haftmann@39646
    34
      QUICK_AND_DIRTY="true"
haftmann@32483
    35
      ;;
haftmann@32483
    36
    \?)
haftmann@32483
    37
      usage
haftmann@32483
    38
      ;;
haftmann@32483
    39
  esac
haftmann@32483
    40
done
haftmann@32483
    41
haftmann@32483
    42
shift $(($OPTIND - 1))
haftmann@32483
    43
haftmann@32483
    44
[ "$#" -ne 3 ] && usage
haftmann@21884
    45
haftmann@21884
    46
IMAGE="$1"; shift
haftmann@39646
    47
THYNAME="$1"; shift
haftmann@39646
    48
CODE_EXPR=$(echo "$1" | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
haftmann@21884
    49
haftmann@21884
    50
haftmann@39646
    51
## invoke code generation
haftmann@21884
    52
haftmann@39714
    53
FORMAL_CMD="Toplevel.program (fn () => (use_thy thyname; ML_Context.eval_text_in \
wenzelm@43328
    54
  (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \
haftmann@51091
    55
  handle _ => exit 1;"
haftmann@32483
    56
haftmann@39646
    57
ACTUAL_CMD="val thyname = \"$THYNAME\"; \
haftmann@39750
    58
  val _ = quick_and_dirty := $QUICK_AND_DIRTY; \
haftmann@39646
    59
  val cmd_expr = \"$CODE_EXPR\"; \
haftmann@39750
    60
  val ml_cmd = \"Code_Target.codegen_tool thyname cmd_expr\"; \
haftmann@39646
    61
  $FORMAL_CMD"
haftmann@32483
    62
haftmann@39646
    63
"$ISABELLE_PROCESS" -r -q -e "$ACTUAL_CMD" "$IMAGE" || exit 1