On Sat, 20 Jul 2013, Florian Haftmann wrote:
I stumbled over a problem with
http://isabelle.in.tum.de/repos/isabelle/rev/9ec2d47de6a7 and static
code conversions.
In static code conversions, it happens routinely that the cterm to which
the conversion is applied to stems from a different (but subsequent)
theory than the theory from the context of its construction. See the
attached theory for a minimal example which actually only invokes pre-
and postprocessor.
This breaks in #9ec2d47de6a7 with »rewrite_cterm: bad background theory«.
That change belongs to the full localization of the Simplifier that I did
some weeks ago. There is no longer anything special about type simpset
from the past -- you just invoke the Simplifier with "the" context, i.e.
the one you have at run-time of a certain tool. So it should be a context
from a super-theory of everything involved in the process.
I was half expecting problems with codegen side-entries to the Simplifier,
but it should work out nonetheless. You need to avoid hard-wired
(Simplifier.global_context thy) -- it would have to transferred to the
run-time theory before invoking simplification.
Instead of transfer, it is usually easier not to store such a Simplifier
context at all, but only its inner data content, which is accessible via
simpset_of and put_simpset. E.g. see this example here:
http://isabelle.in.tum.de/repos/isabelle/annotate/06653152ea8b/src/HOL/HOL.thy#l1997
The idea is as follows:
* use the compile-time @{context} to build up a certain simpset
(the full context is required for operations like addsimps to work);
* store its simpset_of;
* at tool run-time put_simpset that into "the" context;
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
