Ltac2 Quotation tutorial#123
Conversation
SkySkimmer
force-pushed
the
ltac2-quot
branch
from
f84baf4 to
2b7853f
Compare
thomas-lamiaux
left a comment
thomas-lamiaux
left a comment
There was a problem hiding this comment.
The content is clear to me.
However, it is more of an explanation than a tutorial since it is not much about doing.
A tutorial is a practical activity, in which the student learns by doing something meaningful, towards some achievable goal.
Would there be not trivial but simple enough examples that could be added to 2.1 and 2.4 to showcase how the need for quoting arises in practice, and how you choose constr, open_constr etc...
|
Reading the tutorial I don't get when we want to use |
This is not a sensible question. open_constr is syntax, econstr is a type. |
|
just curious you know |
|
Curious about what? I can only answer questions that I can understand. |
what about that ? |
|
IDK how often
open_constr is ltac2 syntax, econstr is a ocaml type, how could they be the same? |
|
My question is rather when should you use |
|
@SkySkimmer could you read section 2, and tells me if it looks good to you ? |
|
Also is |
|
Control.hyp is just a function. |
thomas-lamiaux
force-pushed
the
ltac2-quot
branch
from
e195055 to
e8f9f5e
Compare
| We can do so by: | ||
| 1. Recovering the type [?a] by matching the type of the hypothesis | ||
| 2. Creating a new existantial variables with [(_ :> a)], | ||
| 3. Quoting it [let e := '(_ :> ?a)] to get a Ltac2 expression we can manipulate |
There was a problem hiding this comment.
| 3. Quoting it [let e := '(_ :> ?a)] to get a Ltac2 expression we can manipulate | |
| 3. Quoting it [let e := '(_ :> $a)] to get a Ltac2 expression we can manipulate |
There was a problem hiding this comment.
also the let is not part of the quoting
and what we manipulate is the ltac value produced by evaluating the expression, not the expression itself
There was a problem hiding this comment.
your change does not adress my comment IMO
stop talking about manipulating expressions
| The reasons is that to solve existantial variables, opposite to [open_constr:], | ||
| [constr:] runs typeclass inference. |
There was a problem hiding this comment.
I don't think that's the reason, these evars are not typeclass evars.
There was a problem hiding this comment.
I think "instance" is just what we call a possible value for an evar
There was a problem hiding this comment.
The comment still incorrectly mentions TC inference.
| (** As an example, consider writing a small function [exists]. | ||
| If we write a notation for it naively, then it will fail when linked with | ||
| [;] with another tactic, because there will be two goals: | ||
| *) | ||
|
|
||
| Ltac2 exists0 (t : constr) := | ||
| unshelve (econstructor 1) > [exact $t |]. | ||
|
|
||
| Ltac2 Notation "exists" t(constr) := exists0 t. | ||
|
|
||
| Goal {n | n <= 0} * {n | n <= 0}. | ||
| Fail split; exists 0. | ||
| Abort. | ||
|
|
||
| (** We need to postpone typechecking to after focusing the goals. | ||
| We can do so by quoting a [preterm] rather than a [constr], then typechecking by hand. | ||
| *) | ||
|
|
||
| Ltac2 Notation "exists" t(preterm) := | ||
| Control.enter (fun () => exists0 (Constr.pretype t)). |
There was a problem hiding this comment.
I think the proper way to postpone typechecking is to thunk ie
Ltac2 Notation "exists" t(thunk(constr)) :=
Control.enter (fun () => exists0 (t ())).There was a problem hiding this comment.
last comment to adress, not sure what you mean. Are you saying this is a bad example ?
There was a problem hiding this comment.
yes, it's rather anti-idiomatic I think
in general if you're just going to call Constr.pretype there's no real need for preterm
you need to be changing flags or expected type somehow for preterm to be useful
There was a problem hiding this comment.
I am going to remove the example for now, and merge
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
thomas-lamiaux
force-pushed
the
ltac2-quot
branch
from
7e5e0b8 to
d0db0f1
Compare
| The grammar of names may be trivial but it still needs some syntax | ||
| to produce name constants in Ltac2 expression. | ||
|
|
||
| Identifiers are of type [ident], and can be create using [@x] |
There was a problem hiding this comment.
| Identifiers are of type [ident], and can be create using [@x] | |
| Identifiers are of type [ident], and can be created using [@x] |
| (** A term [t] is quoted in two steps: | ||
|
|
||
| 1. The term is internalized when the Ltac2 expression is typechecked. | ||
| This does several things like name resolution or interpreting notations. |
There was a problem hiding this comment.
May I suggest: notation unfolding and binding analysis (locally bound v.s. global reference).
|
|
||
| 2. When the Ltac2 expression is evaluated, the internalization of [t] | ||
| is typechecked in the current context, returning the elaborated term. | ||
| See " type inference" through the glossary index in the reference manual. |
There was a problem hiding this comment.
| See " type inference" through the glossary index in the reference manual. | |
| See "type inference" through the glossary index in the reference manual. |
| is typechecked in the current context, returning the elaborated term. | ||
| See " type inference" through the glossary index in the reference manual. | ||
|
|
||
| Note that ['] does not run typeclass inference. |
There was a problem hiding this comment.
This requires an example. Also the next sentence seems to be an example of this, which is not.
| hypotheses), it throws an error if more than one goal is focused. | ||
| For instance, the following fails as there are two goals after [split]: |
There was a problem hiding this comment.
pick two goals with different context, otherwise you are shooting yourself in the foot.
| Fail split; let _ := '(0) in (). | ||
| Abort. | ||
|
|
||
| (** Moreover, this error is "thrown", meaning it cannot be caught by "try" and |
There was a problem hiding this comment.
| (** Moreover, this error is "thrown", meaning it cannot be caught by "try" and | |
| (** Moreover, this error is fatal, meaning it cannot be caught by "try" and |
| [$(Control.hyp h)] or variation of that. It is only possible to unquote variables. | ||
| The reason is that functions like [Control.hyp] needs a goal, where [$] does not. | ||
| You hence need a [ltac2:()] wrapper, c.f. section 3. |
There was a problem hiding this comment.
This needs to be clarified further, since in the example above there is a context.
It is not clear to me why doing a let-elimination in the code above would result in a failure.
|
|
||
| (** We can also wrap it in a notation, to do the quoting for us *) | ||
|
|
||
| Ltac2 Notation "forward" h(ident) := forward h. |
There was a problem hiding this comment.
Maybe this should be used earlier as a method to avoid the various @ e co?
|
I'm sorry I did not realize the PR was already merged. |
|
Still useful I guess, maybe open issue to say they are stuff to improve and link the comments |
4 participants
Close #93