Re: [isabelle] Local_Theory.map_naming in locales



On Sun, 15 Feb 2015, Florian Haftmann wrote:

context begin
local_setup â Local_Theory.map_naming (Name_Space.mandatory_path "foo") â
lemma bar: "bar â True" ..
end

Unfortunately, this does not seem to work when I am inside a locale.

locale test = assumes *: True begin
context begin
local_setup â Local_Theory.map_naming (Name_Space.mandatory_path "foo") â
lemma bar: "bar â True" ..
end

Now, the theorem names "bar", "local.bar", and "test.foo.bar" are
available. I would have expected "foo.bar", "local.foo.bar", and
"test.foo.bar", but the first two do not exist.

Having a look at Local_Theory.map_naming this is quite obvious

fun map_naming f =
 map_top (fn (naming, operations, after_close, brittle, target) =>
   (f naming, operations, after_close, brittle, target));

I.e. only the topmost context in the stack of local theories is affected.

It is unclear to me what can be done in our current infrastructure to
achieve the desired effect.  I will spend some time to understand this
occasionally.

So far, the "naming" of a local_theory only refers to the background theory for foundation. There is still no provision for more name space control, but it is one of the important things in the pipeline for a very long time. Over many years, there were just important ingredients missing to move forward, e.g. unnamed context begin ... end blocks. There were also rather lame reasons like the inability to write "private definition ..." or "private theorem ..." with TTY/Proof General still around.


There is a whole complex around name space policies, but I don't recall all details on the spot. Here are some aspects to rekindle a discussion of what could be done eventually.

  * Some concrete syntax for bindings and namings (e.g. in context
    headers) to add name space qualification (with and without "mandatory"
    flag).

  * Likewise some syntax for certain flags, e.g. "concealed", "private",
    "hidden".

  * Reform of existing theories to eliminate all uses of "hide", "hide
    (open)", "map_naming" etc.

  * Session-qualified theory names.

  * Restoration of old tools that only cope with full names like
    "Theory.foo" or "Theory.local.foo" -- paradoxically, such "old" tools
    are sometimes only a few years old.


	Makarius


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