Hi Makarius,
On 10.02.2015 18:30, Makarius wrote:
On Tue, 4 Nov 2014, Makarius wrote:
Strange hacks that work around the absence of proper options encumber
the introduction of them eventually. It is the usual bootstrap
problem for reforms.
I actually did start some work in the vicinity of resolve_tac with
proper context recently, but it will require more time to revisit
really ancient parts of the system, not to say ancient habits.
Here is an update on this pending thread: current
Isabelle/50b60f501b05 is the main move to proper context for
resolve_tac etc. After endless years of preparation to "localize" the
majority of Isabelle tools, it turned out a releatively small change.
What remains are slightly odd entry points without context:
resolve0_tac/rtac, eresolve_tac/etac, dresolve_tac/dtac. We could
probably remove them altogether, but there are a lot of remaining uses
in the new datatype implementation, which I don't want to change myself.
indeed approximately 2/3 of all usages of rtac in the Isabelle
distribution + AFP are in our BNF tactics (roughly 2000 occurrences).
Adding a context to each of them would make the tactics even harder to
read/maintain compared to their current state. The only decent way of
adding the context everywhere would be via some combinators à la
THEN'': (ctxt -> int -> tactic) * (ctxt -> int -> tactic) -> ctxt -> int
-> tactic
assuming that rtac has type "thm -> ctxt -> int -> tactic"
or reuse the polymorphism of THEN' and work with an uncurried version
of rtac: thm -> (ctxt, int) -> tactic (and other tactics). Needless to
say that I could do this only locally in the BNF package, but maybe this
is a general question of how tactics should look like.
Dmitriy
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
