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.
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
