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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
