[isabelle-dev] Advice for replacing @{simpset} with @{context}.

[Makarius]

On Fri, 13 Sep 2013, David Greenaway wrote:

> On 13/09/13 04:17, Makarius wrote:
>> The NEWS file explains what will happen in the coming release with
>> simpset vs. Proof.context -- the Simplifier was one of the last
>> hold-outs of non-localized tools, so after long delays we are mostly
>> through with it.
>
> Sorry, I should have mentioned that I read the NEWS file; I understood 
> that the simplifier now accepted a context instead of a simpset, and 
> that "addsimps" operated on contexts instead of simpsets.

The relevant text from NEWS is this:

* Simplifier tactics and tools use proper Proof.context instead of
historic type simpset.  Old-style declarations like addsimps,
addsimprocs etc. operate directly on Proof.context.  Raw type simpset
retains its use as snapshot of the main Simplifier context, using
simpset_of and put_simpset on Proof.context.  INCOMPATIBILITY -- port
old tools by making them depend on (ctxt : Proof.context) instead of
(ss : simpset), then turn (simpset_of ctxt) into ctxt.


As usual it needs to be studied and digested carefully, the absorb as much 
of the meaning as possible.  Superficially, the text also gives certain 
main entry points into the sources, like "simpset_of" or "put_simpset". If 
you look a bit around how that is usually used (e.g. via hypersearch in 
Isabelle/jEdit), and how it is defined in src/Pure/raw_simplifier.ML, you 
should get some ideas about it.  Moreover, looking in the vicinity of it, 
you see the less frequently used simpset_map combinator.  Searching for 
uses of that in the sources, you will see some examples of updating a 
separate simpset in the context (e.g. in src/HOL/Tools/record.ML).

None of this is rocket-science -- just elementary techniques of reading 
things carefully.


> My question was instead related to the best way to perform operations on 
> long-lived simpsets which need to be mutated over time

Once again a note on proper terminlogy: Isabelle context data is never 
*mutated*, which would mean destructive in-place change.  It has required 
many years to overcome that old habit, which was once considered an 
"optimization", but avoiding it makes the performance of parallel Isabelle 
today.

All Isabelle context data is pure, and it is *updated* in an immutable 
manner.  The coming release even gets rid of the last bits of mutablility 
at the bottom of the implementation of context data (for the theory 
stamps).

Coq still has a lot of mutability left over from the old times, which 
prevents it from using current hardware efficiently.


> Florian's reply was helpful in pointing out some code (the code
> generator) which also had this problem, and its solution to this which
> amounts to: (i) taking your old simpset; (ii) putting it into a dummy
> context; (iii) performing your "addsimp"/"addcong"/etc operation; (iv)
> extract the simpset out again.

This sounds right, and is probably close to Simplifier.simpset_map. The 
auxiliary context should normally be "the context" that you have from 
somewhere already.


 	Makarius