Paolo Giarrusso (Oct 13 2023 at 12:10): Paolo Giarrusso (Oct 13 2023 at 12:10):Debugging with @Janno and @Rodolphe Lepigre shows that vanilla elpi lenses don't generate calls to (folded) primitive projections proj r, only calls to _unfolded_ primitive projections match r with Mk proj => proj end. We've also failed to find APIs to build the unfolded folded primitive projection.
And since many tactics distinguish such projections, this leads to failures. Example:
From elpi.apps Require Export derive.
From elpi.apps Require Export derive.lens.
#[projections(primitive=yes)]
Record R := MkR {
proj : nat;
}.
#[only(lens)] derive R.
Lemma failing r :
proj r = 0 ->
view R__proj r = proj r.
Proof.
simpl.
intros Hpr.
rewrite Hpr.
Fail reflexivity.
Abort.
Lemma working r :
match r with MkR r_proj => r_proj end = 0 ->
view R__proj r = match r with MkR r_proj => r_proj end.
Proof.
simpl.
intros Hpr.
rewrite Hpr.
reflexivity.
Qed.
Its a bug indeed.
This PR makes it work as I intended it to work: https://github.com/LPCIC/coq-elpi/pull/521
It could receive some more testing.
Paolo Giarrusso (Oct 13 2023 at 13:11):forgot to mention: using a debug printer confirms that proj r produces Proj((primproj.proj),false,r) (a folded projection), while
view R__proj r produces Proj((primproj.proj),true,r)
message:(forall Hpr:(Ind(Coq.Init.Logic.eq,0) Ind(Coq.Init.Datatypes.nat,0)
Proj((bedrock.hw_models.primproj.proj),false,r)
Constr(Coq.Init.Datatypes.nat,0,1)),
(Ind(Coq.Init.Logic.eq,0) Ind(Coq.Init.Datatypes.nat,0)
Proj((bedrock.hw_models.primproj.proj),true,r)
Constr(Coq.Init.Datatypes.nat,0,1)))
@Enrico Tassi so now we can't write unfolded projections instead?
Paolo Giarrusso (Oct 13 2023 at 13:18):since elpi terms store primitive projections in primitive-value, it seems one could expose prim-proj-set-folded : primitive-value -> bool -> primitive-value, and use that when building projections. It probably should be done in the preferred APIs, but I'm not sure that should affect coq.build-match.
Paolo Giarrusso (Oct 13 2023 at 13:21):The key question is whether Elpi users need to control prim-proj folding. IMHO, the collective suffering from the compatibility layer suggests that yes, users need access and control over the actual terms — I think that's the moral from @Pierre-Marie Pédrot .
Paolo Giarrusso (Oct 13 2023 at 13:30):just an example of the duality:
Lemma failing' r : proj r = 0 -> match r with MkR r_proj => r_proj end = 0.
Proof. simpl. intros Hpr. Fail rewrite Hpr.
Lemma failing'_converse r : match r with MkR r_proj => r_proj end = 0 -> proj r = 0.
Proof. simpl. intros Hpr. Fail rewrite Hpr.
We could have an API like that, but I'd prefer to pretend primitive projects are folded in elpi.
I mean, calling Elpi on a goal/term with folded or unfolded primproj should do the same.
And internally I don't see the point of juggling with the flag.
Finally, it seems a nice invariant that the output of an elpi program has folded projections.
The only caveat is that if you implement idtac in elpi, well, it refolds primprojs.
At the border with ltac, one can call ltac's unfold to prepare the goal for a tactic which needs it.
Am I ruling out some use case in your opinion?
Janno (Oct 13 2023 at 14:01):It's does not seem generally possible to undo the effect of folding all primitive projection that make its way through elpi with something like ltac's unfold unless one can remember exactly the folded state of all projections and went into elpi. And what if one projection is used in the input and also generated by elpi code and the result is supposed to contain some folded and some unfolded occurrences?
Enrico Tassi (Oct 13 2023 at 14:07):Well, if you want to live in a world where some projections are folded and some are not, then yes, what I propose does not work.
At the same time I really don't get why one wants that, especially in a new code base.
The unfold flag was added so that old code (relying on unfold to expose a match) would continue to work even under the primproj option. That plan failed.
IMO in new code you should not call unfold on a primproj. Maybe you have no choice, and you have to call some old piece of code which leaves some occurrences unfolded. But IMO you should wrap that code and refold everything (again, in a new code base).
Can you explain why you need to have unfolded primproj around?
Paolo Giarrusso (Oct 13 2023 at 14:12):We'd have to port everything we use to satisfy this invariant, including vm_compute I guess?
Janno (Oct 13 2023 at 14:15):I don't have a specific use case in mind although I am sure our code base is full of places where projections end up unfolded, either accidentally or on purpose. I just generally don't think the coq ecosystem is in a state where anybody can reliably eliminate all unfolded primitive projections. Even coq's own elaborator generates them, after all.
Paolo Giarrusso (Oct 13 2023 at 14:15):Also, it's not enough that elpi tactics canonicalize all primitive projections. You need to fix all clients of elpi-generated definitions.
Enrico Tassi (Oct 13 2023 at 14:18):Hum, I guess I'm too optimisitc.
Let me summon @Gaëtan Gilbert and @Pierre-Marie Pédrot that know better.
Which piece of code could flip the boolean an unfold a primproj? (other than the unfold tactic).
And what is the plan in Ltac2? Do you want to expose this mess?
Enrico Tassi (Oct 13 2023 at 14:19):Paolo Giarrusso said:
Also, it's not enough that elpi tactics canonicalize all primitive projections. You need to fix all clients of elpi-generated definitions.
No, if they expect projections in folded state. Yes, if they expect them in unfolded state. So the question is which client is legit, and which one is legacy. If both are legit, then I don't see how we hope to get rid of this compat layer.
Paolo Giarrusso (Oct 13 2023 at 14:20):Which piece of code could flip the boolean an unfold a primproj? (other than the unfold tactic).
Normalizers must. So you'd proposing a world where elpi can't generate normal forms.
Paolo Giarrusso (Oct 13 2023 at 14:22):Without the compat layer you'd have _no_ flag at all, and then these problems disappear — you just have to port clients to sensible reduction rules, but at least those are canonical.
Enrico Tassi (Oct 13 2023 at 14:27):I'm looking at cClosure and I'm afraid reality is worse than what I tough, projections are put in unfolded form almost everywhere (when they are not reduced). I still don't get why, but it seems a catastrophe.
Gaëtan Gilbert (Oct 13 2023 at 14:30):The unfold flag was added so that old code (relying on unfold to expose a match) would continue to work even under the primproj option. That plan failed.
I am not sure that is actually true. I think there was some desire to control unfolding of projections and the flag is how it was done.
ie sometimes you want to mark a projection Opaque, and selectively use unfold for it
I'm looking at cClosure and I'm afraid reality is worse than what I tough, projections are put in unfolded form almost everywhere (when they are not reduced).
transparent projections are unfolded, and unfolded projections are put on the stack. Then the machine continues and if it finds a constructor it will further reduce.
Gaëtan Gilbert (Oct 13 2023 at 14:31):Which piece of code could flip the boolean an unfold a primproj? (other than the unfold tactic).
Basically anything that does delta reduction I think
Paolo Giarrusso (Oct 13 2023 at 14:32):if you just want Opaque you can use opacity on the constant, right?
Gaëtan Gilbert (Oct 13 2023 at 14:32):it's rather difficult to produce a term which contains the fully applied constant
Paolo Giarrusso (Oct 13 2023 at 14:33):still, you don't need the folded bit for that, do you?
Paolo Giarrusso (Oct 13 2023 at 14:33):The stated goal of the folded bit was that cbv delta [proj] won't reduce them, cbv beta delta [proj] will.
Paolo Giarrusso (Oct 13 2023 at 14:34):That matches non-primitive projections, but is not implementable without the folded bit IIRC.
Paolo Giarrusso (Oct 13 2023 at 14:34):and that's the "feature" many would be happy to drop
Enrico Tassi (Oct 13 2023 at 19:39):I've updated the PR up there, it should not match reality
Janno (Oct 17 2023 at 13:40):Will the new code refold unfolded projections that could appear in the record's parameters?
Paolo Giarrusso (Oct 17 2023 at 18:24):if you're right, it's probably hard to trigger here, but in general I'd also prefer "generate specified projection" rather than just a way to clear the statues
Last updated: Oct 13 2024 at 01:02 UTC