equal
deleted
inserted
replaced
8 PRG="$(basename "$0")" |
8 PRG="$(basename "$0")" |
9 |
9 |
10 function usage() |
10 function usage() |
11 { |
11 { |
12 echo |
12 echo |
13 echo "Usage: isabelle $PRG [OPTIONS] IMAGE THY CMD" |
13 echo "Usage: isabelle $PRG [OPTIONS] IMAGE THYNAME CMD" |
14 echo |
14 echo |
15 echo " Options are:" |
15 echo " Options are:" |
16 echo " -q run in quick'n'dirty mode" |
16 echo " -q run in quick'n'dirty mode" |
17 echo |
17 echo |
18 echo " Issues code generation using image IMAGE," |
18 echo " Issues code generation using image IMAGE," |
19 echo " theory THY," |
19 echo " theory THYNAME," |
20 echo " with Isar command 'export_code CMD'" |
20 echo " with Isar command 'export_code CMD'" |
21 echo |
21 echo |
22 exit 1 |
22 exit 1 |
23 } |
23 } |
24 |
24 |
|
25 |
25 ## process command line |
26 ## process command line |
26 |
27 |
27 QUICK_AND_DIRTY=0 |
28 QUICK_AND_DIRTY="false" |
28 |
29 |
29 while getopts "q" OPT |
30 while getopts "q" OPT |
30 do |
31 do |
31 case "$OPT" in |
32 case "$OPT" in |
32 q) |
33 q) |
33 QUICK_AND_DIRTY=1 |
34 QUICK_AND_DIRTY="true" |
34 ;; |
35 ;; |
35 \?) |
36 \?) |
36 usage |
37 usage |
37 ;; |
38 ;; |
38 esac |
39 esac |
41 shift $(($OPTIND - 1)) |
42 shift $(($OPTIND - 1)) |
42 |
43 |
43 [ "$#" -ne 3 ] && usage |
44 [ "$#" -ne 3 ] && usage |
44 |
45 |
45 IMAGE="$1"; shift |
46 IMAGE="$1"; shift |
46 THY="$1"; shift |
47 THYNAME="$1"; shift |
47 CMD="$1" |
48 CODE_EXPR=$(echo "$1" | perl -pe 's/\\/\\\\/g; s/"/\\\"/g') |
48 |
49 |
49 |
50 |
50 ## main |
51 ## invoke code generation |
51 |
52 |
52 CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g') |
53 FORMAL_CMD="Toplevel.program (fn () => ML_Context.eval_text_in \ |
|
54 (SOME (ProofContext.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd) \ |
|
55 handle _ => OS.Process.exit OS.Process.failure;" |
53 |
56 |
54 if [ "$QUICK_AND_DIRTY" -eq 1 ] |
57 ACTUAL_CMD="val thyname = \"$THYNAME\"; \ |
55 then |
58 val qnd = $QUICK_AND_DIRTY; \ |
56 QND_FLAG="true" |
59 val cmd_expr = \"$CODE_EXPR\"; \ |
57 else |
60 val ml_cmd = \"Code_Target.codegen_tool thyname qnd cmd_expr\"; \ |
58 QND_FLAG="false" |
61 $FORMAL_CMD" |
59 fi |
|
60 |
62 |
61 CTXT_CMD="ML_Context.eval_text_in (SOME (ProofContext.init_global (Thy_Info.get_theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";" |
63 "$ISABELLE_PROCESS" -r -q -e "$ACTUAL_CMD" "$IMAGE" || exit 1 |
62 |
|
63 FULL_CMD="quick_and_dirty := $QND_FLAG; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD" |
|
64 |
|
65 "$ISABELLE_PROCESS" -q -e "$FULL_CMD" "$IMAGE" || exit 1 |
|