@Pierre-Marie Pédrot ; I can't figure out how to use the term id one can give in a context match. Syntactically it works, but whenever I use the id, I get a hard to digest error message:
Require Import Ltac2.Ltac2. Require Import Ltac2.Message. Ltac2 works ():= lazy_match! goal with | [ |- context [S ?n] ] => Message.print (Message.of_constr n) end. Ltac2 doesnt ():= lazy_match! goal with | [ |- context n [S _] ] => Message.print (Message.of_constr n) end.
For the latter I get:
This expression has type (((Pattern.match_kind * Pattern.t) list * (Pattern.match_kind * pattern)) * (ident array -> Pattern.context array -> constr array -> constr -> unit)) list but an expression was expected of type (((Pattern.match_kind * Pattern.t) list * (Pattern.match_kind * Pattern.t)) * (ident array -> Pattern.context array -> constr array -> Pattern.context -> 'a)) list
Am I doing something wrong or is this a bug?
I agree the error message is not very readable. I thought I had already written a patch to make it more palatable, but it seems not.
If you look carefully, the difference between the two types is constr vs. Pattern.context.
The reason is that a matching context is not a term, but a term with a hole.
You have to provide something to fill the context with to get a proper term.
See Pattern.instantiate for that.
OK, this works:
Ltac2 somehow ():= lazy_match! goal with | [ |- context n [S ?n'] ] => Message.print (Message.of_constr (Pattern.instantiate n n')) end.
But I don't quite see why it has to be like this - it reduces the usefulness of giving the complete context a name if I have to somehow put it together later anyway - I could just write
S n'. When the match is done, it should be clear how to fill in the whole.
Do you have uses cases in mind, where it would make sense to put in something else than the matched sub-term?
It could be a more complex context, though. For instance if you have variable capture and the like.
Sorry I still don't get it. In what case could I supply an argument for the holes in the context, Ltac2 couldn't figure out on this own?
I am not sure I see what you are asking for, actually.
In Ltac1 you also have to fill the context with a term to use it. It so happens that there is runtime trickery to cast it on the fly to a term but in general it's an ill-typed term.
e.g. this fails:
Goal 1 = 1. Proof. match goal with [ |- context c [S ?n] ] => pose c end.
variable c should be bound to a term.
The only case where you can use it is
idtac c AFAIU
(or explicit instantiation, obviously)
Sorry, I mixed this up with the
as name in Ltac1 - I didn't realize that the semantics of this is entirely different.
Last updated: Sep 28 2023 at 10:01 UTC