Sometimes it is necessary to convert an Ltac
to a Tactic Notation
, e.g. when one needs an argument to be parsed a certain way and ltac doesn't provide another way of forcing the right parsing (see https://github.com/coq/coq/issues/18111).
But which parsing "category" do I need to set for general ltac terms / ltac thunks? Let's say I have a tactic like this
Ltac run_tac tac := tac ().
How do I make that a notation? I tried this but it doesn't work:
Ltac run_tac tac := tac ().
Tactic Notation "run_tac2" tactic(tac) := tac.
Goal forall n : nat, True.
Proof.
intros n.
run_tac ltac:(fun _ => destruct n as [|n']).
Undo.
run_tac2 ltac:(fun _ => destruct n as [|n']).
(* Error: An unnamed user-defined tactic was not fully applied: There is a missing argument for variable _,
no arguments at all were provided. *)
I've looked through the table at https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#coq:cmd.Tactic-Notation but none of the categories seem to fit
but also the table is incomplete, e.g. open_constr
is missing, so maybe there are other things missing as well
I am not sure I understand the question. You are passing an ltac fun
to both run_tac
and run_tac2
but only run_tac
actually supplies the unit argument. If you change run_tac2
to tac ()
it seems to work.
You can also use ltac:(idtac; ..)
to thunk tactics and that way you can skip fun _ =>
and the unit argument
do you actually need thunk/idtac
for tactics passed to Tactic Notation
? The stdpp tactics don't seem to
Tactic Notation "run_tac2" tactic(tac) := tac.
bewaretactic
is probably almost always the wrong precedence, run_tac2 a; b; c
would parse as run_tac2 (a; b; c)
.
You have tactic0
to tactic4
, matching ltac_expr0
to ltac_expr4
in the ltac grammar: https://coq.inria.fr/refman/proof-engine/ltac.html#syntax. I've recommended tactic3
in the past for stdpp, but I suspect tactic1
would make more sense.
Janno said:
I am not sure I understand the question. You are passing an ltac
fun
to bothrun_tac
andrun_tac2
but onlyrun_tac
actually supplies the unit argument. If you changerun_tac2
totac ()
it seems to work.
oh I am stupid, you are right.
I had some very strange trouble porting an existing Ltac
to a Tactic Notation
that lead to the same error and then made this fatal mistake while minimizing...
I wonder now if my original issue was a similar typo or something deeper. sadly the error doesn't say where arguments failed to be provided.
Paolo Giarrusso said:
You have
tactic0
totactic4
, matchingltac_expr0
toltac_expr4
in the ltac grammar: https://coq.inria.fr/refman/proof-engine/ltac.html#syntax. I've recommendedtactic3
in the past for stdpp, but I suspecttactic1
would make more sense.
yeah I know, this is just for demonstration. I never know which number to pick, I just know the default is bad...
Paolo Giarrusso said:
do you actually need thunk/
idtac
for tactics passed toTactic Notation
? The stdpp tactics don't seem to
probably not but we always use thunks since it is the only way to be sure
There's at least no visible thunking with naive_solver eauto with foo
.
All tactic arguments are delayed by default unless they are headed by match, lazymatch, multimatch, or let
Paolo Giarrusso said:
There's at least no visible thunking with
naive_solver eauto with foo
.
ah sure yes we avoid the thunks to get a nicer UI. I meant in the implementation. we have to use CPS for tons of stuff anyway so the few additional closures for thunking barely stick out^^
Last updated: Oct 13 2024 at 01:02 UTC