[isabelle-dev] I'd like to better understand some operations from Local_Theory.

[Thomas Sewell]

Hello Isabelle developers.

I'm doing an experiment in which I need to programmatically construct a locale. For simplicity I used the same operations that Michael Norrish was using in the l4.verified C code parser, Local_Theory.define and Local_Theory.notes. This led to some strange behaviour.

Suppose I set up ML actions for adding a definition "foo = True" to a locale and for getting the constant named "foo"

locale test = assumes True
begin

ML {*
val add_foo = Local_Theory.define ((@{binding foo}, NoSyn), (Attrib.empty_binding, @{term True}))
  #> snd;
fun get_foo ctxt = ProofContext.read_const ctxt false dummyT "foo";
*}
ML {*
val ctxt = @{context};
*}

If I run the add_foo operation with local_setup, get_foo tells me "foo" is now the constant "local.foo".

local_setup {* add_foo *}
ML {* get_foo @{context} *}

This looked promising for my experiment. However, performing these actions within a single ML block tells me "foo" is extracted by read_const as the free variable "foo" (with the correct type).

ML {* get_foo (add_foo ctxt) *}

That had me stumped for hours. It turns I can get the behaviour I want with judicious interspersing of Local_Theory.restore.

ML {* get_foo (Local_Theory.restore (add_foo ctxt)) *}

However I'm just reciting incantations at this point. Furthermore I had no idea where to go looking for this incantation other than to try a collection of uncommented functions from Local_Theory. I've been a bit negligent about reading the various manuals that have cropped up of late; would any of them have explained what is going on?

Also, the behaviour if one supplies a functional pattern to local_setup has to be seen to be believed:

local_setup {* fn _ => add_foo ctxt *}
ML {* get_foo @{context} *}
ML {* get_foo ctxt *}

Although in writing this email I finally understood: the context saved in @{context} when ctxt was being defined includes the local ML interpreter state, which is one in which ctxt isn't defined yet. I guess that's what I get for playing with setup/local_setup.

I'll rephrase my question: should I have been better informed about this, or are local definitions genuinely inscrutable?

Yours,
    Thomas.

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.