Re: [isabelle] antiquotations



Lucas Dixon wrote:
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Alexander Krauss wrote:
Since bind_thms is impure, it can only update some global reference
hanging around. This is incompatible with paralellism. At the moment it
may work sometimes, but it is guaranteed to break sooner or later.

I'm curious about this: is it really the case that references are
inherently incompatible with parallelism? Is there some reason why it
cannot update a thread-local reference?

I would expect that you can cut the Isar/ML cake both ways:
anti-quotations in Isar or quotations in ML. I feel there should be a
confluence proof there somewhere :)

So, is there some reason this is not possible? In particular, Isar is
executed in ML, so it seems rather strange to me that you cannot
replicate it's effect in ML, for example by pasting the function calls
used by Isar into the ML.

cheers,
lucas
Lucas / Alexander,

Well, yes, one would think so.

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 {* ... *} ?  If not, what exactly does happen ?

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

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 ?
Regards,

Jeremy






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