149 \<close> |
149 \<close> |
150 |
150 |
151 subsection \<open>Common adaptation applications \label{sec:common_adaptation}\<close> |
151 subsection \<open>Common adaptation applications \label{sec:common_adaptation}\<close> |
152 |
152 |
153 text \<open> |
153 text \<open> |
154 The @{theory HOL} @{theory Main} theory already provides a code |
154 The @{theory Main} theory of Isabelle/HOL already provides a code |
155 generator setup which should be suitable for most applications. |
155 generator setup which should be suitable for most applications. |
156 Common extensions and modifications are available by certain |
156 Common extensions and modifications are available by certain |
157 theories in \<^dir>\<open>~~/src/HOL/Library\<close>; beside being useful in |
157 theories in \<^dir>\<open>~~/src/HOL/Library\<close>; beside being useful in |
158 applications, they may serve as a tutorial for customising the code |
158 applications, they may serve as a tutorial for customising the code |
159 generator setup (see below \secref{sec:adaptation_mechanisms}). |
159 generator setup (see below \secref{sec:adaptation_mechanisms}). |
160 |
160 |
161 \begin{description} |
161 \begin{description} |
162 |
162 |
163 \item[@{theory "Code_Numeral"}] provides additional numeric |
163 \item[@{theory "HOL.Code_Numeral"}] provides additional numeric |
164 types @{typ integer} and @{typ natural} isomorphic to types |
164 types @{typ integer} and @{typ natural} isomorphic to types |
165 @{typ int} and @{typ nat} respectively. Type @{typ integer} |
165 @{typ int} and @{typ nat} respectively. Type @{typ integer} |
166 is mapped to target-language built-in integers; @{typ natural} |
166 is mapped to target-language built-in integers; @{typ natural} |
167 is implemented as abstract type over @{typ integer}. |
167 is implemented as abstract type over @{typ integer}. |
168 Useful for code setups which involve e.g.~indexing |
168 Useful for code setups which involve e.g.~indexing |
169 of target-language arrays. Part of @{text "HOL-Main"}. |
169 of target-language arrays. Part of @{text "HOL-Main"}. |
170 |
170 |
171 \item[@{theory "String"}] provides an additional datatype @{typ |
171 \item[@{theory "HOL.String"}] provides an additional datatype @{typ |
172 String.literal} which is isomorphic to lists of 7-bit (ASCII) characters; |
172 String.literal} which is isomorphic to lists of 7-bit (ASCII) characters; |
173 @{typ String.literal}s are mapped to target-language strings. |
173 @{typ String.literal}s are mapped to target-language strings. |
174 |
174 |
175 Literal values of type @{typ String.literal} can be written |
175 Literal values of type @{typ String.literal} can be written |
176 as @{text "STR ''\<dots>''"} for sequences of printable characters and |
176 as @{text "STR ''\<dots>''"} for sequences of printable characters and |
213 |
213 |
214 \item[@{text "Code_Target_Numeral"}] is a convenience theory |
214 \item[@{text "Code_Target_Numeral"}] is a convenience theory |
215 containing both @{text "Code_Target_Nat"} and |
215 containing both @{text "Code_Target_Nat"} and |
216 @{text "Code_Target_Int"}. |
216 @{text "Code_Target_Int"}. |
217 |
217 |
218 \item[@{theory "IArray"}] provides a type @{typ "'a iarray"} |
218 \item[@{theory "HOL-Library.IArray"}] provides a type @{typ "'a iarray"} |
219 isomorphic to lists but implemented by (effectively immutable) |
219 isomorphic to lists but implemented by (effectively immutable) |
220 arrays \emph{in SML only}. |
220 arrays \emph{in SML only}. |
221 |
221 |
222 \end{description} |
222 \end{description} |
223 \<close> |
223 \<close> |