On Wed, 11 Feb 2015, Dmitriy Traytel wrote:
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.
There is indeed a general question in the background what tactics should
look like, for a few decades already.
The most compact (or rather hermetic) way you be to put the context into
the goal state, but in recent decades the direction of movement has been
the opposite. The context is the static part and the goal state the
dynamic part. The subgoal address is somehow in the middle. So the
canonical argument order for that came out as follows:
context --> arguments --> subgoal_address -> tactic
For Eisbach the distinction of static vs. dynamic part has become very
relevant again, and not all questions are answered, especially concerning
"arguments" in some cases.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
