Stream: Coq devs & plugin devs

Topic: Faithful representation of case nodes


view this post on Zulip Pierre-Marie Pédrot (Feb 05 2022 at 18:00):

I was pondering recently about the mismatch between the internal representation of Case nodes and what we display to the user. Since the change of representation, the gap is much narrower, but there are still differences.

view this post on Zulip Pierre-Marie Pédrot (Feb 05 2022 at 18:00):

The only real difference is that we do not display parameters / universe instances of the return clause to the user.

view this post on Zulip Pierre-Marie Pédrot (Feb 05 2022 at 18:01):

In practice, we force syntactically parameters of the return clause to always be underscores.

view this post on Zulip Pierre-Marie Pédrot (Feb 05 2022 at 18:01):

But in hindsight this is a bit silly, because these things are there in the constr anyways.

view this post on Zulip Pierre-Marie Pédrot (Feb 05 2022 at 18:02):

What if we allowed the user to put arbitrary parameters there and preserve them until the kernel, instead of reinferring them?

view this post on Zulip Pierre-Marie Pédrot (Feb 05 2022 at 18:02):

We would also display them when going the other way around, leading to a 1:1 bijection.

view this post on Zulip Pierre-Marie Pédrot (Feb 05 2022 at 18:03):

(and similarly for the universe instance)

view this post on Zulip Pierre-Marie Pédrot (Feb 05 2022 at 18:04):

Does it sound like a reasonable idea?

view this post on Zulip Gaëtan Gilbert (Feb 05 2022 at 18:05):

try it and see how it goes

view this post on Zulip Pierre-Marie Pédrot (Feb 05 2022 at 18:08):

What is "how"?

view this post on Zulip Pierre-Marie Pédrot (Feb 05 2022 at 18:08):

I don't expect any trouble

view this post on Zulip Pierre-Marie Pédrot (Feb 05 2022 at 18:09):

rather it's a design choice that we want to expose this to the user

view this post on Zulip Pierre-Marie Pédrot (Feb 05 2022 at 18:09):

(it would also make explicit some pattern selection weirdnesses)

view this post on Zulip Hugo Herbelin (Feb 06 2022 at 09:29):

Is what makes you hesitating the difference of status that parameters and indices would have in the in clause (terms for the former, binders for the latter)? If so, an alternative would be to write things like in I (A:=nat) (x:=0) y. That's a bit cumbersome but if it is mostly expected for the Set Printing All mode, that could be acceptable.

Otherwise, why not in I nat 0 y as well if the difference of status between parameters and indices is clearly documented.

Side question: in constructors, that would remain _ I guess?

view this post on Zulip Gaëtan Gilbert (Feb 06 2022 at 12:47):

it should remain compatible with notations so that we can do in (x = y) so the := form may be too different

view this post on Zulip Matthieu Sozeau (Feb 06 2022 at 22:36):

I think we should do it, maybe subject to an optional Set Printing option


Last updated: Dec 05 2023 at 04:01 UTC