dropped obsolete external entrance point
authorhaftmann
Thu Feb 05 13:01:12 2015 +0100 (2015-02-05)
changeset 5948061d6d5cbbcd3
parent 59479 b36379a730f4
child 59481 74f638efffcb
dropped obsolete external entrance point
NEWS
etc/components
src/Tools/Code/code_target.ML
src/Tools/Code/etc/settings
src/Tools/Code/lib/Tools/codegen
     1.1 --- a/NEWS	Thu Feb 05 13:01:12 2015 +0100
     1.2 +++ b/NEWS	Thu Feb 05 13:01:12 2015 +0100
     1.3 @@ -68,6 +68,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Discontinued old-fashioned "codegen" tool.  Code generation can always
     1.8 +be externally triggered using an appropriate ROOT file plus a corresponding
     1.9 +theory.  Parametrization is possible using environment variables, or
    1.10 +ML snippets in the most extreme cases.  Minor INCOMPATIBILITY.
    1.11 +
    1.12  * Add NO_MATCH-simproc, allows to check for syntactic non-equality
    1.13  
    1.14  * Generalized and consolidated some theorems concerning divsibility:
     2.1 --- a/etc/components	Thu Feb 05 13:01:12 2015 +0100
     2.2 +++ b/etc/components	Thu Feb 05 13:01:12 2015 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  #hard-wired components
     2.5 -src/Tools/Code
     2.6  src/Tools/jEdit
     2.7  src/Tools/Graphview
     2.8  src/HOL/Mirabelle
     3.1 --- a/src/Tools/Code/code_target.ML	Thu Feb 05 13:01:12 2015 +0100
     3.2 +++ b/src/Tools/Code/code_target.ML	Thu Feb 05 13:01:12 2015 +0100
     3.3 @@ -53,8 +53,6 @@
     3.4    val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
     3.5      -> theory -> theory
     3.6    val add_reserved: string -> string -> theory -> theory
     3.7 -
     3.8 -  val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
     3.9  end;
    3.10  
    3.11  structure Code_Target : CODE_TARGET =
    3.12 @@ -661,18 +659,4 @@
    3.13    Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
    3.14      (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.context_of)));
    3.15  
    3.16 -
    3.17 -(** external entrance point -- for codegen tool **)
    3.18 -
    3.19 -fun codegen_tool thyname cmd_expr =
    3.20 -  let
    3.21 -    val thy = Thy_Info.get_theory thyname;
    3.22 -    val ctxt = Proof_Context.init_global thy;
    3.23 -    val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
    3.24 -      (filter Token.is_proper o Token.explode (Thy_Header.get_keywords thy) Position.none);
    3.25 -  in case parse cmd_expr
    3.26 -   of SOME f => (writeln "Now generating code..."; f ctxt)
    3.27 -    | NONE => error ("Bad directive " ^ quote cmd_expr)
    3.28 -  end;
    3.29 -
    3.30  end; (*struct*)
     4.1 --- a/src/Tools/Code/etc/settings	Thu Feb 05 13:01:12 2015 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,4 +0,0 @@
     4.4 -# -*- shell-script -*- :mode=shellscript:
     4.5 -
     4.6 -ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
     4.7 -
     5.1 --- a/src/Tools/Code/lib/Tools/codegen	Thu Feb 05 13:01:12 2015 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,64 +0,0 @@
     5.4 -#!/usr/bin/env bash
     5.5 -#
     5.6 -# Author: Florian Haftmann, TUM
     5.7 -#
     5.8 -# DESCRIPTION: issue code generation from shell
     5.9 -
    5.10 -
    5.11 -PRG="$(basename "$0")"
    5.12 -
    5.13 -function usage()
    5.14 -{
    5.15 -  echo
    5.16 -  echo "Usage: isabelle $PRG [OPTIONS] IMAGE THYNAME CMD"
    5.17 -  echo
    5.18 -  echo "  Options are:"
    5.19 -  echo "    -q    run in quick_and_dirty mode"
    5.20 -  echo
    5.21 -  echo "  Issues code generation using image IMAGE,"
    5.22 -  echo "  theory THYNAME,"
    5.23 -  echo "  with Isar command 'export_code CMD'"
    5.24 -  echo
    5.25 -  exit 1
    5.26 -}
    5.27 -
    5.28 -
    5.29 -## process command line
    5.30 -
    5.31 -QUICK_AND_DIRTY="false"
    5.32 -
    5.33 -while getopts "q" OPT
    5.34 -do
    5.35 -  case "$OPT" in
    5.36 -    q)
    5.37 -      QUICK_AND_DIRTY="true"
    5.38 -      ;;
    5.39 -    \?)
    5.40 -      usage
    5.41 -      ;;
    5.42 -  esac
    5.43 -done
    5.44 -
    5.45 -shift $(($OPTIND - 1))
    5.46 -
    5.47 -[ "$#" -ne 3 ] && usage
    5.48 -
    5.49 -IMAGE="$1"; shift
    5.50 -THYNAME="$1"; shift
    5.51 -CODE_EXPR=$(echo "$1" | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
    5.52 -
    5.53 -
    5.54 -## invoke code generation
    5.55 -
    5.56 -FORMAL_CMD="Runtime.toplevel_program (fn () => (use_thy thyname; ML_Context.eval_source_in \
    5.57 -    (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) \
    5.58 -    ML_Compiler.flags \
    5.59 -    {delimited=true, text=ml_cmd, pos=Position.none})) \
    5.60 -  handle _ => exit 1;"
    5.61 -
    5.62 -ACTUAL_CMD="val thyname = \"$THYNAME\"; \
    5.63 -  val cmd_expr = \"$CODE_EXPR\"; \
    5.64 -  val ml_cmd = \"Code_Target.codegen_tool thyname cmd_expr\"; \
    5.65 -  $FORMAL_CMD"
    5.66 -
    5.67 -"$ISABELLE_PROCESS" -r -q -o "quick_and_dirty=$QUICK_AND_DIRTY" -e "$ACTUAL_CMD" "$IMAGE" || exit 1