Re: [isabelle] antiquotations



On Fri, 15 Feb 2008, Jeremy Dawson wrote:

> How do these critical sections work?  Is it to do with the function 
> CRITICAL which appears in the source code?

See appendix A.2 of the fragmentary Isabelle/Isar implementation manual. 
It explains the programming model for multithreaded Isabelle; the short 
and simple message is: do it purely functionally and in accord with the 
official concepts of context (as a plain value).

In rare situations, user code may also have to synchronize things 
explicitly, but well-behaved programs should only do this for tiny amounts 
of time, i.e. refrain from any real computations / proof search inside a 
critical section.


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

You can look at the Isar implementation to find out the details, just for 
curiosity.  It is of course out of question to attempt to interfere with 
the existing infrastructure in user ML code.


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

Basically none.  You can refer to the compile time context using 
@{context}, or get a runtime context as explicit functional argument from 
somewhere else.  For example, a proof method is essentially a function 
Proof.context -> args -> tactic, and your implementation will be something 
like (fn ctxt => fn args => ...), so you get the context ``by induction 
hypothesis'' over the structure of your program.

Concerning theorem lookup, ProofContext.get_thm: Proof.context -> thmref
-> thm enables to retrieve named facts from a given context, but it is
rarely useful within abstract code, because the name spacing rules behind 
this are quite delicate.  Better refer to proper theorem *values* 
directly, either via @{thm ...} at compile time, or by using well-typed 
interfaces to derived context data, such as DatatypePackage.the_datatype 
or similar operations of whatever tool you build yourself.

The general idea of strongly-typed context data is explained in section 
1.1 in the Isabelle/Isar implementation manual.


	Makarius





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