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

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?


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.
isabelle-dev mailing list

Reply via email to