Make Cumulative, NonCumulative and Private attributes.

[Zimmi48]

Kind: feature

These are the last morally attributes which were not parsed as such.

Note that initially I wanted to make the new attributes universes(polymorphic(cumulative)) and universes(polymorphic(noncumulative) (since these attributes must be provided in a polymorphic context). But I didn't manage to find a solution that would be backward-compatible.

• Added / updated test-suite

• Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
• Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

[Zimmi48]

I'll wait for #11423 to be merged before I document this PR.

[Zimmi48]

@ppedrot This PR introduces the private attribute for private inductive types. If the notion of private inductive type is fundamentally different from private as in objects that are not exported from modules, then maybe the name for this attribute should be refined. WDYT?

[SkySkimmer]

I think it's fair enough to say that Private Inductive is about not exporting something from the module.

[maximedenes]

I think it's fair enough to say that Private Inductive is about not exporting something from the module.

I also think this is much more standard in CS than the abusive use of "private" in the HoTT community.

[Zimmi48]

OK, I don't know what the use of "private" in the HoTT community is, but if this Private Inductive feature truly is about a private thing in the sense of not exporting from the module, then there is no issue with this attribute and I simply misinterpreted @ppedrot's comment during the call.

[maximedenes]

I think there's a misunderstanding (but I'm not fully sure), so let's try to clarify: a private attribute should be about not being visible outside of a module. Private Inductive is something else (the type is exported but you can't match on its elements, you have to use the eliminators). I personally find the HoTT terminology confusing so I'd like to replace it with something else (also, the feature is not really implemented since it is not enforced by the kernel, I believe). What is less personal is that the other meaning of private (not being visible outside of a module) is very well established in CS, so please don't introduce a private attribute which has another meaning (such as the HoTT one).

[Zimmi48]

OK thank you very much for clearing things up. So private inductive types are a form of abstraction but more limited than the standard meaning of private. It is similar to types that are exported without their definition in OCaml. What about making the attribute private(constructors) or constructors(private)? Or do you have a suggestion for an entirely different word? The word sealed that we have talked about for opaque definitions could make sense for private inductive types as well somehow. WDYT?

[SkySkimmer]

private(constructors) or constructors(private)

It's the elimination which is restricted, not the construction.

[Zimmi48]

OK. Please advise a good name. nonmatchable comes to my mind but that's probably too obscure.

[SkySkimmer]

Private is fine imo

[Zimmi48]

But @maximedenes doesn't agree (and indeed using private here would prohibit giving it another meaning later). So @maximedenes do you have an alternative suggestion?

[maximedenes]

But @maximedenes doesn't agree (and indeed using private here would prohibit giving it another meaning later). So @maximedenes do you have an alternative suggestion?

Not at the moment, but please don't use private. Not only it will clash with private in the abstraction meaning, but it also clashes with the OCaml notion of private sum type, which ironically is the dual (they can be destructed but not constructed from outside).

[maximedenes]

I won't oppose to nonmatchable, in fact.

[Zimmi48]

New version uses nonmatchable.

Still need to write tests, doc, and a changelog entry.

[Zimmi48]

The documentation is still a work-in-progress (I still want to move the definition of the template and program attributes) but already gives a pretty good idea of the final result.

[Zimmi48]

@ppedrot Unfortunately, I couldn't make the Export modifier a proper legacy attribute because this syntax conflicts with the Export command. So the last commit in this PR does not change the parser but still interprets the Export modifier as an attribute, i.e. Export Set and #[ export ] Set become equivalent.

[Zimmi48]

@jfehrle The first commit of this PR 04adc1d might be of interest to you (so that you don't have to do it again in your own work).

[jfehrle]

The first commit of this PR 04adc1d might be of interest to you

Thanks. FWIW, I try to avoid DELETENT when I can because it's not too safe with respect to future grammar changes that add additional productions to the nonterminal. It's safer to delete each production explicitly with | DELETE ... in that a) the tool will complain if the production doesn't exist and b) any added production in the NT would likely show up as a change in the rsts.
But I've not followed this advice everywhere I could (future cleanup).

DELETE: [ ... ] is not too safe either, but what can you do?

This form is a bit safer (when applicable) because just by looking at it, you can easily verify that this doesn't alter the language accepted:

basequalid: [
| REPLACE ident fields
| WITH ident LIST0 field_ident
| DELETE ident
]

SPLICE and RENAME are always safe. Later on I'll look at improving the edits/edit operations to make them simpler/safer with respect to changes.

[ppedrot]

@Zimmi48 is that merely a parsing problem? In particular, could that be solved using some ad-hoc lookahead?

[Zimmi48]

@ppedrot I thought that lookaheads could help but I don't know how to use them.

[Zimmi48]

Everyone on Gitter seemed to prefer private(match) over nonmatchable.
Bad luck, match is a keyword so #[ private(match) ] does not actually parse.
Should I change the proposal to private(matching), hardcode the parsing of match in attribute syntax, or go back to nonmatchable?

[Zimmi48]

This is ready. Can I get an assignee?

[jfehrle]

I thought that lookaheads could help but I don't know how to use them.

You define a lookahead function and then use the function name in the production. The following example succeeds for the input "(" ident ":=" without consuming it. And fails otherwise.

let test_lpar_id_coloneq =
  let open Pcoq.Lookahead in
  to_entry "test_lpar_id_coloneq" begin
    lk_kw "(" >> lk_ident >> lk_kw ":="
  end


appl_arg:
    [ [ test_lpar_id_coloneq; "("; id = ident; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByName id)) }

[Zimmi48]

Thanks. I tried using a lookahead but didn't manage to fix the issue. But anyway, this wouldn't provide much advantage because Export followed by any other legacy attribute or any non-keyword command has to be assumed to be the Export command applied to modules of such names. Therefore, keeping things as they are in the current state of the PR looks like the best path to me.

[Zimmi48]

As this PR changes quite a lot of things in quite a number of places, I hope I won't have to wait for too long before it gets an assignee and eventually gets merged.

[ppedrot]

I didn't check the documentation changes thoroughly, but the changes to the code look OK to me. I am a bit surprised you managed to sort the parsing issues without breaking everything, but the CI seems to be fine, so that's probably correct.

[ppedrot]

Let's merge, this PR has been discussed viva voce already, I don't think there is much point in delaying it further.

[Zimmi48]

Thanks @ppedrot!