On Thu, 18 Jul 2013, Florian Haftmann wrote:
"Code generator: dropping subsumed code equation" by Auto Quickcheck
I guess it would be the task the tools to omit such outbursts and not
globally on the IDE side?
In principle Context_Position.is_visible should control that, and the
tools should observe it accordingly.
The canonical way to do that is
Context_Position.if_visible ctxt warning
but this does not work for code equations, because the operations of
src/Pure/Isar/code.ML act on a global theory, which is always "visible"
in that sense.
I have generalized the concept to allow changing the visibility of a
global theory context as well. This is observed by unify.ML, as a guard
to its many tracing options, find_theorems.ML then copies the
Proof.context visibility over to a copy of the background theory of the
goal state, so 'solve_direct' no longer produces spam from this source,
see Isabelle/d68fd63bf082.
Maybe Florian also has some ideas about codegen.
One answer would be to eliminate this meanwhile somehow ridiculous
warning entirely.
In principle you could refer to Context_Position.is_visible_global as
well, but it looks all a bit complicated: quickcheck would have to pass
down a modified theory, and code.ML would have to get all these lazy
theory_ref things right.
Note that I am presently experimenting with a purely value-oriented theory
type (Isabelle/38466f4f3483), where theory_ref is just an alias and
Theory.copy / Theory.checkpoint just the identity. So any mistakes in
rearanging the theory_ref management in code.ML won't be detected at
first, only if I have to backout 38466f4f3483 (e.g. due to resoure
problems).
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
