Re: [isabelle] antiquotations



Makarius wrote:
If so, how does it work that in this case calls such as ML_Context.the_context () are safe to use ? (in general when are they safe and when not ?)

Here it is safe, because it runs in a critical section -- just for compile time. Later at run-time, where the actual work happens, eveything is purely functional and enables proper paralellism without further worries.


Makarius,

How do these critical sections work? Is it to do with the function CRITICAL which appears in the source code?
In terms of threads in general: When you're sitting at the terminal typing input into Isar, it gets executed in the context of a particular theory, doesn't it ? Obviously it manages to avoid any ambiguity (ie, it doesn't execute it in the context of some other theory which is currently developing in a different thread. How does it identify which is the relevant theory ?

It is determined from the context :-)
The question relates to what the system does. That is to say, when I am sitting at the terminal and type in ML {* val a = @{context} *} what is the ML code which the system evaluates ? I want to know what ML code I would put there which would achieve exactly the same effect.
Pointing your finger at a particular position in Isar source text, you determine a certain context once and for all. Any embedded ML code at that point will keep this as a first-class value (of type Proof.context) for later use at run-time; provided proper antiquotations are used. So this is just the well-known static closure principle applied to Isabelle/Isar + embedded ML.

In contrast, low-level access to global references buys you dynamic scoping in the best case, and erratic non-determinism in the worst case. This is why thm"foo", thms"foo", the_context() are all bad.


So what functions, _in ML_, are good, for these purposes?
Jeremy

	Makarius







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.