src/Doc/Codegen/Further.thy
changeset 66251 cd935b7cb3fb
parent 65981 e2c25346b156
child 66453 cc19f7ca2ed6
     1.1 --- a/src/Doc/Codegen/Further.thy	Mon Jul 03 14:25:07 2017 +0200
     1.2 +++ b/src/Doc/Codegen/Further.thy	Sun Jul 02 20:13:38 2017 +0200
     1.3 @@ -215,121 +215,4 @@
     1.4    short primer document.
     1.5  \<close>
     1.6  
     1.7 -
     1.8 -subsection \<open>ML system interfaces \label{sec:ml}\<close>
     1.9 -
    1.10 -text \<open>
    1.11 -  Since the code generator framework not only aims to provide a nice
    1.12 -  Isar interface but also to form a base for code-generation-based
    1.13 -  applications, here a short description of the most fundamental ML
    1.14 -  interfaces.
    1.15 -\<close>
    1.16 -
    1.17 -subsubsection \<open>Managing executable content\<close>
    1.18 -
    1.19 -text %mlref \<open>
    1.20 -  \begin{mldecls}
    1.21 -  @{index_ML Code.read_const: "theory -> string -> string"} \\
    1.22 -  @{index_ML Code.add_eqn: "Code.kind * bool -> thm -> theory -> theory"} \\
    1.23 -  @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
    1.24 -  @{index_ML Code_Preproc.map_pre: "(Proof.context -> Proof.context) -> theory -> theory"} \\
    1.25 -  @{index_ML Code_Preproc.map_post: "(Proof.context -> Proof.context) -> theory -> theory"} \\
    1.26 -  @{index_ML Code_Preproc.add_functrans: "
    1.27 -    string * (Proof.context -> (thm * bool) list -> (thm * bool) list option)
    1.28 -      -> theory -> theory"} \\
    1.29 -  @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
    1.30 -  @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
    1.31 -  @{index_ML Code.get_type: "theory -> string
    1.32 -    -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool"} \\
    1.33 -  @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"}
    1.34 -  \end{mldecls}
    1.35 -
    1.36 -  \begin{description}
    1.37 -
    1.38 -  \item @{ML Code.read_const}~@{text thy}~@{text s}
    1.39 -     reads a constant as a concrete term expression @{text s}.
    1.40 -
    1.41 -  \item @{ML Code.add_eqn}~@{text "(kind, default)"}~@{text "thm"}~@{text "thy"} adds code equation
    1.42 -     @{text "thm"} to executable content.
    1.43 -
    1.44 -  \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes code equation
    1.45 -     @{text "thm"} from executable content, if present.
    1.46 -
    1.47 -  \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes
    1.48 -     the preprocessor simpset.
    1.49 -
    1.50 -  \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
    1.51 -     function transformer @{text f} (named @{text name}) to executable content;
    1.52 -     @{text f} is a transformer of the code equations belonging
    1.53 -     to a certain function definition, depending on the
    1.54 -     current theory context.  Returning @{text NONE} indicates that no
    1.55 -     transformation took place;  otherwise, the whole process will be iterated
    1.56 -     with the new code equations.
    1.57 -
    1.58 -  \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes
    1.59 -     function transformer named @{text name} from executable content.
    1.60 -
    1.61 -  \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
    1.62 -     a datatype to executable content, with generation
    1.63 -     set @{text cs}.
    1.64 -
    1.65 -  \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"}
    1.66 -     returns type constructor corresponding to
    1.67 -     constructor @{text const}; returns @{text NONE}
    1.68 -     if @{text const} is no constructor.
    1.69 -
    1.70 -  \end{description}
    1.71 -\<close>
    1.72 -
    1.73 -
    1.74 -subsubsection \<open>Data depending on the theory's executable content\<close>
    1.75 -
    1.76 -text \<open>
    1.77 -  Implementing code generator applications on top of the framework set
    1.78 -  out so far usually not only involves using those primitive
    1.79 -  interfaces but also storing code-dependent data and various other
    1.80 -  things.
    1.81 -
    1.82 -  Due to incrementality of code generation, changes in the theory's
    1.83 -  executable content have to be propagated in a certain fashion.
    1.84 -  Additionally, such changes may occur not only during theory
    1.85 -  extension but also during theory merge, which is a little bit nasty
    1.86 -  from an implementation point of view.  The framework provides a
    1.87 -  solution to this technical challenge by providing a functorial data
    1.88 -  slot @{ML_functor Code_Data}; on instantiation of this functor, the
    1.89 -  following types and operations are required:
    1.90 -
    1.91 -  \medskip
    1.92 -  \begin{tabular}{l}
    1.93 -  @{text "type T"} \\
    1.94 -  @{text "val empty: T"} \\
    1.95 -  \end{tabular}
    1.96 -
    1.97 -  \begin{description}
    1.98 -
    1.99 -  \item @{text T} the type of data to store.
   1.100 -
   1.101 -  \item @{text empty} initial (empty) data.
   1.102 -
   1.103 -  \end{description}
   1.104 -
   1.105 -  \noindent An instance of @{ML_functor Code_Data} provides the
   1.106 -  following interface:
   1.107 -
   1.108 -  \medskip
   1.109 -  \begin{tabular}{l}
   1.110 -  @{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\
   1.111 -  @{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"}
   1.112 -  \end{tabular}
   1.113 -
   1.114 -  \begin{description}
   1.115 -
   1.116 -  \item @{text change} update of current data (cached!) by giving a
   1.117 -    continuation.
   1.118 -
   1.119 -  \item @{text change_yield} update with side result.
   1.120 -
   1.121 -  \end{description}
   1.122 -\<close>
   1.123 -
   1.124  end