Re: [isabelle] antiquotations

On Thu, 14 Feb 2008, Jeremy Dawson wrote:

> Perusing the source code, I see a function called
> eval_antiquotes (to be exact, I used !ML_Context.eval_antiquotes_fn)
> which gives results like this:
> val eval_antiquotes = !ML_Context.eval_antiquotes_fn ;
> eval_antiquotes "val x = y ; val c = @{context} ; \
>  \ val a = b ; val cs = @{claset} ; val t = @{theory}" ;
> val eval_antiquotes = fn : string -> string * string
> > # val it =
>   ("structure Isabelle =\nstruct\nval context = ML_Context.the_local_context
> ();\nval claset = Classical.local_claset_of (ML_Context.the_local_context
> ());\nval thy = ML_Context.the_context ();\nend;",
>      "val x = y ; val c = Isabelle.context ;  val a = b ; val cs =
> Isabelle.claset ; val t = Isabelle.thy")
> : string * string
> Is this in fact used when the system encounters code such as
> ML {* val x = y ; val c = @{context} ; \
>  \ val a = b ; val cs = @{claset} ; val t = @{theory} *} ?
> Or to be exact, is this translated code executed when the system encounters
> the
> ML {* ... *} ?

Yes, here you see the compile time Isar context closure wrapped around ML 
text issued to the underlying platform.  Our previously mentioned paper 
about SML-antiquotations is explains this in a more abstract fashion.

> 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.

> 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 :-)

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.


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