src/Tools/Code/lib/Tools/codegen
author Lars Noschinski <noschinl@in.tum.de>
Fri, 01 Aug 2014 13:59:34 +0200
changeset 57851 33b7372e87ad
parent 54563 7fa522b213a8
permissions -rwxr-xr-x
tuned, so codegen runs with current isabelle again
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21884
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
     1
#!/usr/bin/env bash
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
     2
#
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
     3
# Author: Florian Haftmann, TUM
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
     4
#
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
     5
# DESCRIPTION: issue code generation from shell
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
     6
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
     7
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
     8
PRG="$(basename "$0")"
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
     9
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
    10
function usage()
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
    11
{
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
    12
  echo
39646
64fdbee67135 improved and tuned external codegen tool
haftmann
parents: 39121
diff changeset
    13
  echo "Usage: isabelle $PRG [OPTIONS] IMAGE THYNAME CMD"
32483
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    14
  echo
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    15
  echo "  Options are:"
54563
7fa522b213a8 more official option;
wenzelm
parents: 52059
diff changeset
    16
  echo "    -q    run in quick_and_dirty mode"
21884
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
    17
  echo
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
    18
  echo "  Issues code generation using image IMAGE,"
39646
64fdbee67135 improved and tuned external codegen tool
haftmann
parents: 39121
diff changeset
    19
  echo "  theory THYNAME,"
25611
c0deb7307732 isatool codegen now returns exit value
haftmann
parents: 25451
diff changeset
    20
  echo "  with Isar command 'export_code CMD'"
21884
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
    21
  echo
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
    22
  exit 1
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
    23
}
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
    24
39646
64fdbee67135 improved and tuned external codegen tool
haftmann
parents: 39121
diff changeset
    25
21884
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
    26
## process command line
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
    27
39646
64fdbee67135 improved and tuned external codegen tool
haftmann
parents: 39121
diff changeset
    28
QUICK_AND_DIRTY="false"
32483
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    29
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    30
while getopts "q" OPT
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    31
do
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    32
  case "$OPT" in
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    33
    q)
39646
64fdbee67135 improved and tuned external codegen tool
haftmann
parents: 39121
diff changeset
    34
      QUICK_AND_DIRTY="true"
32483
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    35
      ;;
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    36
    \?)
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    37
      usage
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    38
      ;;
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    39
  esac
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    40
done
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    41
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    42
shift $(($OPTIND - 1))
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    43
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    44
[ "$#" -ne 3 ] && usage
21884
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
    45
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
    46
IMAGE="$1"; shift
39646
64fdbee67135 improved and tuned external codegen tool
haftmann
parents: 39121
diff changeset
    47
THYNAME="$1"; shift
64fdbee67135 improved and tuned external codegen tool
haftmann
parents: 39121
diff changeset
    48
CODE_EXPR=$(echo "$1" | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
21884
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
    49
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
    50
39646
64fdbee67135 improved and tuned external codegen tool
haftmann
parents: 39121
diff changeset
    51
## invoke code generation
21884
7df02627898e added isatool codegen
haftmann
parents:
diff changeset
    52
57851
33b7372e87ad tuned, so codegen runs with current isabelle again
Lars Noschinski <noschinl@in.tum.de>
parents: 54563
diff changeset
    53
FORMAL_CMD="Runtime.toplevel_program (fn () => (use_thy thyname; ML_Context.eval_source_in \
33b7372e87ad tuned, so codegen runs with current isabelle again
Lars Noschinski <noschinl@in.tum.de>
parents: 54563
diff changeset
    54
    (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) \
33b7372e87ad tuned, so codegen runs with current isabelle again
Lars Noschinski <noschinl@in.tum.de>
parents: 54563
diff changeset
    55
    ML_Compiler.flags \
33b7372e87ad tuned, so codegen runs with current isabelle again
Lars Noschinski <noschinl@in.tum.de>
parents: 54563
diff changeset
    56
    {delimited=true, text=ml_cmd, pos=Position.none})) \
51091
c007c6bf4a35 another attempt for a uniform abort on code generation errors
haftmann
parents: 48662
diff changeset
    57
  handle _ => exit 1;"
32483
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    58
39646
64fdbee67135 improved and tuned external codegen tool
haftmann
parents: 39121
diff changeset
    59
ACTUAL_CMD="val thyname = \"$THYNAME\"; \
64fdbee67135 improved and tuned external codegen tool
haftmann
parents: 39121
diff changeset
    60
  val cmd_expr = \"$CODE_EXPR\"; \
39750
c0099428ca7b consider quick_and_dirty option before loading theory
haftmann
parents: 39714
diff changeset
    61
  val ml_cmd = \"Code_Target.codegen_tool thyname cmd_expr\"; \
39646
64fdbee67135 improved and tuned external codegen tool
haftmann
parents: 39121
diff changeset
    62
  $FORMAL_CMD"
32483
522f04b719c8 added -q switch for run in qnd mode
haftmann
parents: 32482
diff changeset
    63
52059
2f970c7f722b proper option quick_and_dirty;
wenzelm
parents: 51091
diff changeset
    64
"$ISABELLE_PROCESS" -r -q -o "quick_and_dirty=$QUICK_AND_DIRTY" -e "$ACTUAL_CMD" "$IMAGE" || exit 1