Guillaume Melquiond (Feb 04 2022 at 14:41): Guillaume Melquiond (Feb 04 2022 at 14:41):The notation for refine is defined as
Ltac2 Notation refine := Control.refine.
As a consequence, the syntax differs from plain Ltac, while most tactics try to have the same syntax in both Ltac1 and Ltac2.
Is there a reason it is not defined as follows?
Ltac2 Notation refine c(thunk(open_constr)) := Control.refine c.
exact is defined like that and I think it is a mistake to make Ltac2 code look like Ltac1. I prefer refine '(my term) over refine (my term). (As a consequence I never use exact because it forces me to write exact $x when I have already let-bound my term to x. Which I almost always do anyway.)
Janno (Feb 04 2022 at 14:48):I do see the inconsistency, though. I guess my suggested solution would be to fix exact..
Pierre-Marie Pédrot (Feb 04 2022 at 15:08):Yeah, in general Ltac1 has hardwired support for parsing argument constrs, but in retrospective it's a bad idea.
Pierre-Marie Pédrot (Feb 04 2022 at 15:08):I agree that all constr-only Ltac2 functions shouldn't be declared through a notation.
Guillaume Melquiond (Feb 04 2022 at 15:09):But then you would not even be able to write refine x. You would have to fall back to refine (fun () => x), wouldn't you?
Pierre-Marie Pédrot (Feb 04 2022 at 15:10):Notation != syntactic alias.
Pierre-Marie Pédrot (Feb 04 2022 at 15:10):Syntactic aliases implicitly thunk their argument
Pierre-Marie Pédrot (Feb 04 2022 at 15:10):but it doesn't require adding a parsing rule
Pierre-Marie Pédrot (Feb 04 2022 at 15:11):so you write refine 'x and it's expanded to Control.refine (fun () => open_constr:(x))
Pierre-Marie Pédrot (Feb 04 2022 at 15:12):Syntax is not modular so every time you add a parsing rule you break some code out there
Guillaume Melquiond (Feb 04 2022 at 15:12):How does that work? Is that type-directed? If you write refine x, Coq checks the type of x and if it is not of type unit -> constr, it thunks it?
Pierre-Marie Pédrot (Feb 04 2022 at 15:12):it's a phase that occurs before type-checking
Pierre-Marie Pédrot (Feb 04 2022 at 15:12):it's just that some global definitions have a special status and are expanded syntactically
Pierre-Marie Pédrot (Feb 04 2022 at 15:12):nothing else
Guillaume Melquiond (Feb 04 2022 at 15:13):So, refine x systematically thunks its argument?
Pierre-Marie Pédrot (Feb 04 2022 at 15:13):yes
Pierre-Marie Pédrot (Feb 04 2022 at 15:14):in practice it's what you want most of the time (hence the fundamental dilemma of Ltac1 between forced values and lazy tactics)
Guillaume Melquiond (Feb 04 2022 at 15:15):Sure, but with this "in practice" argument, I also always want to pass an open constr to refine.
Pierre-Marie Pédrot (Feb 04 2022 at 15:15):no, because that one is a different grammar
Pierre-Marie Pédrot (Feb 04 2022 at 15:15):and it's not true
Pierre-Marie Pédrot (Feb 04 2022 at 15:15):sometimes you want to pass an Ltac2 variable
Guillaume Melquiond (Feb 04 2022 at 15:16):When I say "I", I mean "I".
Pierre-Marie Pédrot (Feb 04 2022 at 15:16):you never pass meta variables to refine?
Pierre-Marie Pédrot (Feb 04 2022 at 15:16):you're free to add a notation if you want
Pierre-Marie Pédrot (Feb 04 2022 at 15:17):but it shouldn't be exposed by default in Ltac2, that's it
Pierre-Marie Pédrot (Feb 04 2022 at 15:17):the less parsing rules, the more modular
Guillaume Melquiond (Feb 04 2022 at 15:17):Why would I pass a meta-variable to refine? What does it even achieve?
Pierre-Marie Pédrot (Feb 04 2022 at 15:17):Ltac foo := intro x; refine x?
Pierre-Marie Pédrot (Feb 04 2022 at 15:18):(meta as in Ltac variable, not a Meta as in the AST)
Guillaume Melquiond (Feb 04 2022 at 15:18):No, I would certainly use exact here.
Pierre-Marie Pédrot (Feb 04 2022 at 15:18):aha, but it doesn't use the same unification algo
Pierre-Marie Pédrot (Feb 04 2022 at 15:19):also it's very bad for HO stuff
Pierre-Marie Pédrot (Feb 04 2022 at 15:19):like, passing refine as an argument to a tactical is hell in Ltac1
Guillaume Melquiond (Feb 04 2022 at 15:20):And even if I were to use refine here, I would never write Ltac foo := let x := fresh in intro x; refine x. I would write Ltac foo := refine (fun x => x).
Pierre-Marie Pédrot (Feb 04 2022 at 15:21):whatever (and these two things are not equivalent)
Pierre-Marie Pédrot (Feb 04 2022 at 15:21):you're free to add your own notations in your devs
Pierre-Marie Pédrot (Feb 04 2022 at 15:21):but you'll have a hard time convincing me that we need more Ltac1-like crappy notations in Ltac2
Guillaume Melquiond (Feb 04 2022 at 15:22):You are absolutely right. That is why I will keep using Control.refine.
Last updated: Jun 10 2023 at 06:31 UTC