--- a/src/Doc/Codegen/Further.thy Mon Jul 03 14:25:07 2017 +0200
+++ b/src/Doc/Codegen/Further.thy Sun Jul 02 20:13:38 2017 +0200
@@ -215,121 +215,4 @@
short primer document.
\<close>
-
-subsection \<open>ML system interfaces \label{sec:ml}\<close>
-
-text \<open>
- Since the code generator framework not only aims to provide a nice
- Isar interface but also to form a base for code-generation-based
- applications, here a short description of the most fundamental ML
- interfaces.
-\<close>
-
-subsubsection \<open>Managing executable content\<close>
-
-text %mlref \<open>
- \begin{mldecls}
- @{index_ML Code.read_const: "theory -> string -> string"} \\
- @{index_ML Code.add_eqn: "Code.kind * bool -> thm -> theory -> theory"} \\
- @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
- @{index_ML Code_Preproc.map_pre: "(Proof.context -> Proof.context) -> theory -> theory"} \\
- @{index_ML Code_Preproc.map_post: "(Proof.context -> Proof.context) -> theory -> theory"} \\
- @{index_ML Code_Preproc.add_functrans: "
- string * (Proof.context -> (thm * bool) list -> (thm * bool) list option)
- -> theory -> theory"} \\
- @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
- @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
- @{index_ML Code.get_type: "theory -> string
- -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool"} \\
- @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"}
- \end{mldecls}
-
- \begin{description}
-
- \item @{ML Code.read_const}~@{text thy}~@{text s}
- reads a constant as a concrete term expression @{text s}.
-
- \item @{ML Code.add_eqn}~@{text "(kind, default)"}~@{text "thm"}~@{text "thy"} adds code equation
- @{text "thm"} to executable content.
-
- \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes code equation
- @{text "thm"} from executable content, if present.
-
- \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes
- the preprocessor simpset.
-
- \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
- function transformer @{text f} (named @{text name}) to executable content;
- @{text f} is a transformer of the code equations belonging
- to a certain function definition, depending on the
- current theory context. Returning @{text NONE} indicates that no
- transformation took place; otherwise, the whole process will be iterated
- with the new code equations.
-
- \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes
- function transformer named @{text name} from executable content.
-
- \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
- a datatype to executable content, with generation
- set @{text cs}.
-
- \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"}
- returns type constructor corresponding to
- constructor @{text const}; returns @{text NONE}
- if @{text const} is no constructor.
-
- \end{description}
-\<close>
-
-
-subsubsection \<open>Data depending on the theory's executable content\<close>
-
-text \<open>
- Implementing code generator applications on top of the framework set
- out so far usually not only involves using those primitive
- interfaces but also storing code-dependent data and various other
- things.
-
- Due to incrementality of code generation, changes in the theory's
- executable content have to be propagated in a certain fashion.
- Additionally, such changes may occur not only during theory
- extension but also during theory merge, which is a little bit nasty
- from an implementation point of view. The framework provides a
- solution to this technical challenge by providing a functorial data
- slot @{ML_functor Code_Data}; on instantiation of this functor, the
- following types and operations are required:
-
- \medskip
- \begin{tabular}{l}
- @{text "type T"} \\
- @{text "val empty: T"} \\
- \end{tabular}
-
- \begin{description}
-
- \item @{text T} the type of data to store.
-
- \item @{text empty} initial (empty) data.
-
- \end{description}
-
- \noindent An instance of @{ML_functor Code_Data} provides the
- following interface:
-
- \medskip
- \begin{tabular}{l}
- @{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\
- @{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"}
- \end{tabular}
-
- \begin{description}
-
- \item @{text change} update of current data (cached!) by giving a
- continuation.
-
- \item @{text change_yield} update with side result.
-
- \end{description}
-\<close>
-
end