[isabelle-dev] copying contexts

[Makarius]

On Wed, 2 Dec 2009, Lucas Dixon wrote:

> I'm wondering what the right way to copy contexts is. I remember there 
> was some references lingering in theories, mostly as unique identifies 
> if I remember correctly, but it meant that copying needed to be an 
> explicit function. Is this the right way to copy a context:
>
> Context.map_theory Context.copy_thy
>
> and so copying a proof context would be:
>
> Context.proof_map (Context.map_theory Context.copy_thy)

(ML names below refer to the forthcoming Isabelle2009-1 release, e.g. see 
http://isabelle.in.tum.de/repos/isabelle-release/rev/6a973bd43949)

The theory type has indeed a double role of providing

   (1) formal certificates of a general background context,
   (2) default values for content of context data.

Any other formal entities (certified types, terms, theorems etc.) can 
maintain a back-reference to that using type theory_ref.  The theory 
referenced here can evolve monotonically later on.  This means we assume 
monotonicity of formal correctness wrt. the background context.  (This 
holds for the basic logical entities, but user concepts that are certified 
against theories need to observe this as well.)  The Theory.copy primitive 
is able to produce a detached side-branch of this linear/monotonic 
evolution of certificates.  Theory.checkpoint provides another way to 
produce a stable stepping stone that can be forked into independent 
developments later (the Isar toplevel already checkpoints theory states at 
transaction boundary, i.e. before and after each Isar command.)

Luckily, user code rarely has to care about any of this.  The reason: most 
of the time one works with a Proof.context, not a raw theory.  In this 
standard setup, user data is maintained via functor Generic_Data, 
sometimes Proof_Data, but hardly ever raw Theory_Data.

When working with Proof.context, the usual way of operation is to update 
that (purely functionally) on the surface.  The background theory 
certificate is still there, and might evolve monotonically without further 
notice, and usually you don't care.

There are some special situations, where updates on the background theory 
do need to be propagated to the surface context, notably in the 
implementation of local_theory mechanisms.  The ProofContext.theory and 
Local_Theory.theory combinators take care of the formal fiddling required 
in such situations.


> The reason I want to do this is that when proof planning proves new 
> theorems it creates some meta-data which gets stored in the context. I 
> want to be able to make a copy the context before I modify any such data 
> so that I can compare alternatives and do fair tests. I was previously 
> using my own generic context, but would like to cut down code 
> duplication.

I would say you merely need to use functor Generic_Data in the usual way: 
purely functional content, no copy operations ever.  See 
src/Pure/Tools/named_thms.ML for a typical example.


BTW, background theories still do support mutable content, which 
Theory.copy would take care of if the user data implements it accodingly. 
As of Isabelle2009-1 mutable data is essentially a legacy feature, though: 
due to performance reasons in an increasingly parallel and asynchronous 
environment, mutable state is very expensive.


 	Makarius