haftmann@28213
|
1 |
theory "ML"
|
haftmann@28213
|
2 |
imports Setup
|
haftmann@28213
|
3 |
begin
|
haftmann@28213
|
4 |
|
haftmann@28419
|
5 |
section {* ML system interfaces \label{sec:ml} *}
|
haftmann@28419
|
6 |
|
haftmann@28419
|
7 |
text {*
|
haftmann@28419
|
8 |
Since the code generator framework not only aims to provide
|
haftmann@28419
|
9 |
a nice Isar interface but also to form a base for
|
haftmann@28419
|
10 |
code-generation-based applications, here a short
|
haftmann@28419
|
11 |
description of the most important ML interfaces.
|
haftmann@28419
|
12 |
*}
|
haftmann@28419
|
13 |
|
haftmann@28419
|
14 |
subsection {* Executable theory content: @{text Code} *}
|
haftmann@28419
|
15 |
|
haftmann@28419
|
16 |
text {*
|
haftmann@28419
|
17 |
This Pure module implements the core notions of
|
haftmann@28419
|
18 |
executable content of a theory.
|
haftmann@28419
|
19 |
*}
|
haftmann@28419
|
20 |
|
haftmann@28419
|
21 |
subsubsection {* Managing executable content *}
|
haftmann@28419
|
22 |
|
haftmann@28419
|
23 |
text %mlref {*
|
haftmann@28419
|
24 |
\begin{mldecls}
|
haftmann@28419
|
25 |
@{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
|
haftmann@28419
|
26 |
@{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
|
haftmann@31143
|
27 |
@{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\
|
haftmann@31143
|
28 |
@{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\
|
haftmann@31143
|
29 |
@{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
|
haftmann@28419
|
30 |
-> theory -> theory"} \\
|
haftmann@31143
|
31 |
@{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
|
haftmann@28419
|
32 |
@{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
|
haftmann@37208
|
33 |
@{index_ML Code.get_type: "theory -> string
|
haftmann@28419
|
34 |
-> (string * sort) list * (string * typ list) list"} \\
|
haftmann@37208
|
35 |
@{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"}
|
haftmann@28419
|
36 |
\end{mldecls}
|
haftmann@28419
|
37 |
|
haftmann@28419
|
38 |
\begin{description}
|
haftmann@28419
|
39 |
|
haftmann@28419
|
40 |
\item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function
|
haftmann@28419
|
41 |
theorem @{text "thm"} to executable content.
|
haftmann@28419
|
42 |
|
haftmann@28419
|
43 |
\item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes function
|
haftmann@28419
|
44 |
theorem @{text "thm"} from executable content, if present.
|
haftmann@28419
|
45 |
|
haftmann@31143
|
46 |
\item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes
|
haftmann@28419
|
47 |
the preprocessor simpset.
|
haftmann@28419
|
48 |
|
haftmann@31143
|
49 |
\item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
|
haftmann@28419
|
50 |
function transformer @{text f} (named @{text name}) to executable content;
|
haftmann@29560
|
51 |
@{text f} is a transformer of the code equations belonging
|
haftmann@28419
|
52 |
to a certain function definition, depending on the
|
haftmann@28419
|
53 |
current theory context. Returning @{text NONE} indicates that no
|
haftmann@28419
|
54 |
transformation took place; otherwise, the whole process will be iterated
|
haftmann@29560
|
55 |
with the new code equations.
|
haftmann@28419
|
56 |
|
haftmann@31143
|
57 |
\item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes
|
haftmann@28419
|
58 |
function transformer named @{text name} from executable content.
|
haftmann@28419
|
59 |
|
haftmann@28419
|
60 |
\item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
|
haftmann@28419
|
61 |
a datatype to executable content, with generation
|
haftmann@28419
|
62 |
set @{text cs}.
|
haftmann@28419
|
63 |
|
haftmann@37208
|
64 |
\item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"}
|
haftmann@28419
|
65 |
returns type constructor corresponding to
|
haftmann@28419
|
66 |
constructor @{text const}; returns @{text NONE}
|
haftmann@28419
|
67 |
if @{text const} is no constructor.
|
haftmann@28419
|
68 |
|
haftmann@28419
|
69 |
\end{description}
|
haftmann@28419
|
70 |
*}
|
haftmann@28419
|
71 |
|
haftmann@28419
|
72 |
subsection {* Auxiliary *}
|
haftmann@28419
|
73 |
|
haftmann@28419
|
74 |
text %mlref {*
|
haftmann@28419
|
75 |
\begin{mldecls}
|
haftmann@31999
|
76 |
@{index_ML Code.read_const: "theory -> string -> string"}
|
haftmann@28419
|
77 |
\end{mldecls}
|
haftmann@28419
|
78 |
|
haftmann@28419
|
79 |
\begin{description}
|
haftmann@28419
|
80 |
|
haftmann@31156
|
81 |
\item @{ML Code.read_const}~@{text thy}~@{text s}
|
haftmann@28419
|
82 |
reads a constant as a concrete term expression @{text s}.
|
haftmann@28419
|
83 |
|
haftmann@28419
|
84 |
\end{description}
|
haftmann@28419
|
85 |
|
haftmann@28419
|
86 |
*}
|
haftmann@28419
|
87 |
|
haftmann@28419
|
88 |
subsection {* Implementing code generator applications *}
|
haftmann@28419
|
89 |
|
haftmann@28419
|
90 |
text {*
|
haftmann@28419
|
91 |
Implementing code generator applications on top
|
haftmann@28419
|
92 |
of the framework set out so far usually not only
|
haftmann@28419
|
93 |
involves using those primitive interfaces
|
haftmann@28419
|
94 |
but also storing code-dependent data and various
|
haftmann@28419
|
95 |
other things.
|
haftmann@28419
|
96 |
*}
|
haftmann@28419
|
97 |
|
haftmann@28419
|
98 |
subsubsection {* Data depending on the theory's executable content *}
|
haftmann@28419
|
99 |
|
haftmann@28419
|
100 |
text {*
|
haftmann@28419
|
101 |
Due to incrementality of code generation, changes in the
|
haftmann@28419
|
102 |
theory's executable content have to be propagated in a
|
haftmann@28419
|
103 |
certain fashion. Additionally, such changes may occur
|
haftmann@28419
|
104 |
not only during theory extension but also during theory
|
haftmann@28419
|
105 |
merge, which is a little bit nasty from an implementation
|
haftmann@28419
|
106 |
point of view. The framework provides a solution
|
haftmann@28419
|
107 |
to this technical challenge by providing a functorial
|
haftmann@37208
|
108 |
data slot @{ML_functor Code_Data}; on instantiation
|
haftmann@28419
|
109 |
of this functor, the following types and operations
|
haftmann@28419
|
110 |
are required:
|
haftmann@28419
|
111 |
|
haftmann@28419
|
112 |
\medskip
|
haftmann@28419
|
113 |
\begin{tabular}{l}
|
haftmann@28419
|
114 |
@{text "type T"} \\
|
haftmann@28419
|
115 |
@{text "val empty: T"} \\
|
haftmann@28635
|
116 |
@{text "val purge: theory \<rightarrow> string list option \<rightarrow> T \<rightarrow> T"}
|
haftmann@28419
|
117 |
\end{tabular}
|
haftmann@28419
|
118 |
|
haftmann@28419
|
119 |
\begin{description}
|
haftmann@28419
|
120 |
|
haftmann@28419
|
121 |
\item @{text T} the type of data to store.
|
haftmann@28419
|
122 |
|
haftmann@28419
|
123 |
\item @{text empty} initial (empty) data.
|
haftmann@28419
|
124 |
|
haftmann@28419
|
125 |
\item @{text purge}~@{text thy}~@{text consts} propagates changes in executable content;
|
haftmann@28419
|
126 |
@{text consts} indicates the kind
|
haftmann@28419
|
127 |
of change: @{ML NONE} stands for a fundamental change
|
haftmann@28419
|
128 |
which invalidates any existing code, @{text "SOME consts"}
|
haftmann@28419
|
129 |
hints that executable content for constants @{text consts}
|
haftmann@28419
|
130 |
has changed.
|
haftmann@28419
|
131 |
|
haftmann@28419
|
132 |
\end{description}
|
haftmann@28419
|
133 |
|
haftmann@37208
|
134 |
\noindent An instance of @{ML_functor Code_Data} provides the following
|
haftmann@28419
|
135 |
interface:
|
haftmann@28419
|
136 |
|
haftmann@28419
|
137 |
\medskip
|
haftmann@28419
|
138 |
\begin{tabular}{l}
|
haftmann@28419
|
139 |
@{text "get: theory \<rightarrow> T"} \\
|
haftmann@28419
|
140 |
@{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\
|
haftmann@28419
|
141 |
@{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"}
|
haftmann@28419
|
142 |
\end{tabular}
|
haftmann@28419
|
143 |
|
haftmann@28419
|
144 |
\begin{description}
|
haftmann@28419
|
145 |
|
haftmann@28419
|
146 |
\item @{text get} retrieval of the current data.
|
haftmann@28419
|
147 |
|
haftmann@28419
|
148 |
\item @{text change} update of current data (cached!)
|
haftmann@28419
|
149 |
by giving a continuation.
|
haftmann@28419
|
150 |
|
haftmann@28419
|
151 |
\item @{text change_yield} update with side result.
|
haftmann@28419
|
152 |
|
haftmann@28419
|
153 |
\end{description}
|
haftmann@28419
|
154 |
*}
|
haftmann@28419
|
155 |
|
haftmann@28419
|
156 |
text {*
|
haftmann@28447
|
157 |
\bigskip
|
haftmann@28447
|
158 |
|
haftmann@28419
|
159 |
\emph{Happy proving, happy hacking!}
|
haftmann@28419
|
160 |
*}
|
haftmann@28213
|
161 |
|
haftmann@28213
|
162 |
end
|