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

[Makarius]

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