223 |
223 |
224 FIXME: calling the ML-compiler |
224 FIXME: calling the ML-compiler |
225 |
225 |
226 *} |
226 *} |
227 |
227 |
228 section {* Managing Name Spaces (TBD) *} |
228 section {* What Is In an Isabelle Name? (TBD) *} |
|
229 |
|
230 text {* |
|
231 On the ML-level of Isabelle, you often have to work with qualified names. |
|
232 These are strings with some additional information, such as positional |
|
233 information and qualifiers. Such qualified names can be generated with the |
|
234 antiquotation @{text "@{binding \<dots>}"}. For example |
|
235 |
|
236 @{ML_response [display,gray] |
|
237 "@{binding \"name\"}" |
|
238 "name"} |
|
239 |
|
240 An example where a qualified name is needed is the function |
|
241 @{ML_ind define in Local_Theory}. This function is used below to define |
|
242 the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}. |
|
243 *} |
|
244 |
|
245 local_setup %gray {* |
|
246 Local_Theory.define ((@{binding "TrueConj"}, NoSyn), |
|
247 (Attrib.empty_binding, @{term "True \<and> True"})) #> snd *} |
|
248 |
|
249 text {* |
|
250 Now querying the definition you obtain: |
|
251 |
|
252 \begin{isabelle} |
|
253 \isacommand{thm}~@{text "TrueConj_def"}\\ |
|
254 @{text "> "}~@{thm TrueConj_def} |
|
255 \end{isabelle} |
|
256 |
|
257 \begin{readmore} |
|
258 The basic operations on bindings are implemented in |
|
259 @{ML_file "Pure/General/binding.ML"}. |
|
260 \end{readmore} |
|
261 |
|
262 \footnote{\bf FIXME give a better example why bindings are important} |
|
263 \footnote{\bf FIXME give a pointer to \isacommand{local\_setup}; if not, then explain |
|
264 why @{ML snd} is needed.} |
|
265 \footnote{\bf FIXME: There should probably a separate section on binding, long-names |
|
266 and sign.} |
|
267 |
|
268 *} |
|
269 |
229 |
270 |
230 ML {* Sign.intern_type @{theory} "list" *} |
271 ML {* Sign.intern_type @{theory} "list" *} |
231 ML {* Sign.intern_const @{theory} "prod_fun" *} |
272 ML {* Sign.intern_const @{theory} "prod_fun" *} |
232 |
273 |
|
274 text {* |
|
275 \footnote{\bf FIXME: Explain the following better; maybe put in a separate |
|
276 section and link with the comment in the antiquotation section.} |
|
277 |
|
278 Occasionally you have to calculate what the ``base'' name of a given |
|
279 constant is. For this you can use the function @{ML_ind "Sign.extern_const"} or |
|
280 @{ML_ind Long_Name.base_name}. For example: |
|
281 |
|
282 @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} |
|
283 |
|
284 The difference between both functions is that @{ML extern_const in Sign} returns |
|
285 the smallest name that is still unique, whereas @{ML base_name in Long_Name} always |
|
286 strips off all qualifiers. |
|
287 |
|
288 \begin{readmore} |
|
289 Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"}; |
|
290 functions about signatures in @{ML_file "Pure/sign.ML"}. |
|
291 \end{readmore} |
|
292 *} |
233 |
293 |
234 text {* |
294 text {* |
235 @{ML_ind "Binding.str_of"} returns the string with markup; |
295 @{ML_ind "Binding.str_of"} returns the string with markup; |
236 @{ML_ind "Binding.name_of"} returns the string without markup |
296 @{ML_ind "Binding.name_of"} returns the string without markup |
237 |
297 |