On Thu, 7 Apr 2011, Thomas Sewell wrote:
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} *}
Looks fine so far, although ProofContext.read_const is a bit unusual. I
had to do a hypersearch on the whole sources myself to get an idea of what
is its point. A quick glance at its typicaly uses confirms its exotic
nature. Plain Syntax.read_term should do the job in most situations.
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.
You could have spend the time studying chapter 7 in the implementation
manual and the two papers being cited there.
What you have encountered here is the hypothetical entity within the
auxiliary context of the local theory target. These are very important
concepts. Thus the details of the actual target mechanisms are hidden
from a definitional package, i.e. it will work uniformly for global
theories, locales, type classes etc.
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)) *}
Thus you pretend to be on a package boundary. Normally you don't want
this, although there are rare situations where there is no better
workaround. Again a hypersearch on the sources reveals that
Local_Theory.restore is hardly ever used in practice.
It is important to read the sources the proper way.
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.
As usual when there is a surprise there are two main possibilities:
(1) unexpectedly general types being inferred for some terms
(2) working with an unexpected context
The local setup above ignores the current context and returns to an update
of an earlier one. There should be no surprise that the ML toplevel
environment is part of the context -- everything in Isabelle is part of
the context. (There are a few corner cases where this rule is violated,
and these should be the surprising ones.)
BTW, Poly/ML is a native code compiler, not an interpreter.
BTW2, the Poly/ML runtime state is *not* saved, i.e. mutable content is
not subject to the context. Since mutable content is hardly ever used
these days, one can mostly forget about it.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
