[isabelle-dev] How to activate/de-activate unifier-trace from ML-level
traytel at in.tum.de
Wed Feb 11 09:35:08 CET 2015
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
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.
More information about the isabelle-dev