5 section {* ML system interfaces \label{sec:ml} *}
8 Since the code generator framework not only aims to provide
9 a nice Isar interface but also to form a base for
10 code-generation-based applications, here a short
11 description of the most important ML interfaces.
14 subsection {* Executable theory content: @{text Code} *}
17 This Pure module implements the core notions of
18 executable content of a theory.
21 subsubsection {* Managing executable content *}
25 @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
26 @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
27 @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\
28 @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\
29 @{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
30 -> theory -> theory"} \\
31 @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
32 @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
33 @{index_ML Code.get_type: "theory -> string
34 -> (string * sort) list * (string * typ list) list"} \\
35 @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"}
40 \item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function
41 theorem @{text "thm"} to executable content.
43 \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes function
44 theorem @{text "thm"} from executable content, if present.
46 \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes
47 the preprocessor simpset.
49 \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
50 function transformer @{text f} (named @{text name}) to executable content;
51 @{text f} is a transformer of the code equations belonging
52 to a certain function definition, depending on the
53 current theory context. Returning @{text NONE} indicates that no
54 transformation took place; otherwise, the whole process will be iterated
55 with the new code equations.
57 \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes
58 function transformer named @{text name} from executable content.
60 \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
61 a datatype to executable content, with generation
64 \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"}
65 returns type constructor corresponding to
66 constructor @{text const}; returns @{text NONE}
67 if @{text const} is no constructor.
72 subsection {* Auxiliary *}
76 @{index_ML Code.read_const: "theory -> string -> string"}
81 \item @{ML Code.read_const}~@{text thy}~@{text s}
82 reads a constant as a concrete term expression @{text s}.
88 subsection {* Implementing code generator applications *}
91 Implementing code generator applications on top
92 of the framework set out so far usually not only
93 involves using those primitive interfaces
94 but also storing code-dependent data and various
98 subsubsection {* Data depending on the theory's executable content *}
101 Due to incrementality of code generation, changes in the
102 theory's executable content have to be propagated in a
103 certain fashion. Additionally, such changes may occur
104 not only during theory extension but also during theory
105 merge, which is a little bit nasty from an implementation
106 point of view. The framework provides a solution
107 to this technical challenge by providing a functorial
108 data slot @{ML_functor Code_Data}; on instantiation
109 of this functor, the following types and operations
115 @{text "val empty: T"} \\
116 @{text "val purge: theory \<rightarrow> string list option \<rightarrow> T \<rightarrow> T"}
121 \item @{text T} the type of data to store.
123 \item @{text empty} initial (empty) data.
125 \item @{text purge}~@{text thy}~@{text consts} propagates changes in executable content;
126 @{text consts} indicates the kind
127 of change: @{ML NONE} stands for a fundamental change
128 which invalidates any existing code, @{text "SOME consts"}
129 hints that executable content for constants @{text consts}
134 \noindent An instance of @{ML_functor Code_Data} provides the following
139 @{text "get: theory \<rightarrow> T"} \\
140 @{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\
141 @{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"}
146 \item @{text get} retrieval of the current data.
148 \item @{text change} update of current data (cached!)
149 by giving a continuation.
151 \item @{text change_yield} update with side result.
159 \emph{Happy proving, happy hacking!}