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
