123 applications, they may serve as a tutorial for customising the code |
123 applications, they may serve as a tutorial for customising the code |
124 generator setup (see below \secref{sec:adaptation_mechanisms}). |
124 generator setup (see below \secref{sec:adaptation_mechanisms}). |
125 |
125 |
126 \begin{description} |
126 \begin{description} |
127 |
127 |
128 \item[@{theory "Code_Integer"}] represents @{text HOL} integers by |
128 \item[@{text "Code_Integer"}] represents @{text HOL} integers by |
129 big integer literals in target languages. |
129 big integer literals in target languages. |
130 |
130 |
131 \item[@{theory "Code_Char"}] represents @{text HOL} characters by |
131 \item[@{text "Code_Char"}] represents @{text HOL} characters by |
132 character literals in target languages. |
132 character literals in target languages. |
133 |
133 |
134 \item[@{theory "Code_Char_chr"}] like @{text "Code_Char"}, but |
134 \item[@{text "Code_Char_chr"}] like @{text "Code_Char"}, but |
135 also offers treatment of character codes; includes @{theory |
135 also offers treatment of character codes; includes @{text |
136 "Code_Char"}. |
136 "Code_Char"}. |
137 |
137 |
138 \item[@{theory "Efficient_Nat"}] \label{eff_nat} implements |
138 \item[@{text "Efficient_Nat"}] \label{eff_nat} implements |
139 natural numbers by integers, which in general will result in |
139 natural numbers by integers, which in general will result in |
140 higher efficiency; pattern matching with @{term "0\<Colon>nat"} / |
140 higher efficiency; pattern matching with @{term "0\<Colon>nat"} / |
141 @{const "Suc"} is eliminated; includes @{theory "Code_Integer"} |
141 @{const "Suc"} is eliminated; includes @{text "Code_Integer"} |
142 and @{theory "Code_Numeral"}. |
142 and @{text "Code_Numeral"}. |
143 |
143 |
144 \item[@{theory "Code_Numeral"}] provides an additional datatype |
144 \item[@{theory "Code_Numeral"}] provides an additional datatype |
145 @{typ index} which is mapped to target-language built-in |
145 @{typ index} which is mapped to target-language built-in |
146 integers. Useful for code setups which involve e.g.~indexing |
146 integers. Useful for code setups which involve e.g.~indexing |
147 of target-language arrays. |
147 of target-language arrays. Part of @{text "HOL-Main"}. |
148 |
148 |
149 \item[@{theory "String"}] provides an additional datatype @{typ |
149 \item[@{theory "String"}] provides an additional datatype @{typ |
150 String.literal} which is isomorphic to strings; @{typ |
150 String.literal} which is isomorphic to strings; @{typ |
151 String.literal}s are mapped to target-language strings. Useful |
151 String.literal}s are mapped to target-language strings. Useful |
152 for code setups which involve e.g.~printing (error) messages. |
152 for code setups which involve e.g.~printing (error) messages. |
|
153 Part of @{text "HOL-Main"}. |
153 |
154 |
154 \end{description} |
155 \end{description} |
155 |
156 |
156 \begin{warn} |
157 \begin{warn} |
157 When importing any of these theories, they should form the last |
158 When importing any of those theories which are not part of |
|
159 @{text "HOL-Main"}, they should form the last |
158 items in an import list. Since these theories adapt the code |
160 items in an import list. Since these theories adapt the code |
159 generator setup in a non-conservative fashion, strange effects may |
161 generator setup in a non-conservative fashion, strange effects may |
160 occur otherwise. |
162 occur otherwise. |
161 \end{warn} |
163 \end{warn} |
162 *} |
164 *} |