Re: [isabelle] problem with local theories and the code generator



On Tue, 15 May 2012, Ondřej Kunčar wrote:

I've experienced the following problem with ML-level of Isabelle (namely with local theories and the code generator):

You should not use this confusing term "ML-level of Isabelle". Isabelle/ML and Isabelle/Isar are intertwined in a certain way, and there is no lower or upper level here. See also the recent thread https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-April/msg00066.html


My code is inside the command quotient_type and thus inside a local_theory context. In this context a new constant is defined (by Local_Theory.define) and it's called let's say "abs". Because I am inside a local_theory context, this constant is actually a fixed variable and not a real constant.

This is again a bit confusing. Local_Theory.define is for abstract term definitions. It depends on the local_theory target how this will be represented in the foundation, and integrated into the target for later use by the user. For a global theory it will become a constant, for a locale a constant that depends on locale parameters plus some abbreviations, for a completely different target something completely different.

A simple analogy is this: local_theory is the regular virtual memory view of a process address space that is now commonplace, probably even on tiny mobile devices. There are physical hardware addresses in the foundations somewhere, but you cannot count on that in your program code.


But now I want to call Code.add_datatype and thus say that "abs" is a code datatype constructor. I do it by the following command: Local_Theory.declaration {syntax = false, pervasive = true} (K (Context.mapping (Code.add_datatype [(name, type)]) I))

The "K" above is part of the problem. It disregards the morphism for the mapping, which is required to move things from one context to the other, before they can be applied to the concrete context in question.

Admittedly this is the difficult aspect of local theory declarations, but ignoring it is no solution. To make effective use of the Isabelle infrastructure, it is important to develop a habit to do things in "the canonical" way. Thus one does not have to revisit all the implementation details from the ground up over and over again.


But then the code generator complains that "abs" is not a constant. How can I solve this situation? It seems to me that I need either a) jump away from a local_theory context for a while and let "abs" get transformed to a real constant or b) I need something like a "localized" code generator package.

Generally, you can try to work with general declarations with proper use of morphisms, or make a reduced version that merely puts things into the background theory context. For that you transform the abstract term once to move it the global theory and then work with Local_Theort.background_theory etc.

I can't say anything about the possibility of a localied code generator. Florian Haftmann should comment on that.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.