lib/Tools/codegen
author wenzelm
Sat Jul 25 10:31:27 2009 +0200 (2009-07-25)
changeset 32187 cca43ca13f4f
parent 30494 c150e6fa4e0d
permissions -rwxr-xr-x
renamed structure Display_Goal to Goal_Display;
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
## diagnostics
haftmann@21884
     9
haftmann@21884
    10
PRG="$(basename "$0")"
haftmann@21884
    11
haftmann@21884
    12
function usage()
haftmann@21884
    13
{
haftmann@21884
    14
  echo
wenzelm@28650
    15
  echo "Usage: isabelle $PRG IMAGE THY CMD"
haftmann@21884
    16
  echo
haftmann@21884
    17
  echo "  Issues code generation using image IMAGE,"
haftmann@21884
    18
  echo "  theory THY,"
haftmann@25611
    19
  echo "  with Isar command 'export_code CMD'"
haftmann@21884
    20
  echo
haftmann@21884
    21
  exit 1
haftmann@21884
    22
}
haftmann@21884
    23
haftmann@21884
    24
haftmann@21884
    25
## process command line
haftmann@21884
    26
haftmann@21884
    27
[ "$#" -lt 2 -o "$1" = "-?" ] && usage
haftmann@21884
    28
haftmann@21884
    29
IMAGE="$1"; shift
haftmann@21884
    30
THY="$1"; shift
haftmann@25611
    31
CMD="$1"
haftmann@21884
    32
haftmann@21884
    33
haftmann@21884
    34
## main
haftmann@21884
    35
haftmann@30494
    36
CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
haftmann@30494
    37
CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
haftmann@30494
    38
FULL_CMD="val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
haftmann@21884
    39
haftmann@30494
    40
"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1