Stream: Coq devs & plugin devs

Topic: Constant/MutInd API

Hugo Herbelin (Dec 20 2021 at 19:03):

Am I the only ones having troubles to remember what Constant.make, Constant.make1, Constant.make2 are doing? What about the following alternatives:

• Scheme 1 ( to follow the model of KerName.make):
  • Constant.make2 -> Constant.make (with an optional ~user:modpath)
  • Constant.make1 -> Constant.of_kn (with an optional ~user:modpath, or optional ~user:kn)
  • Constant.make -> subsumed by Constant.of_kn ~user:modpath

• Scheme 2 ( to follow the model of KerName.make, but less disruptive):

  • Constant.make2 -> Constant.make
  • Constant.make1 -> Constant.of_kn
  • Constant.make -> Constant.of_kn2 (or Constant.of_kn_pair)
    But risk that we don't realize that we have to think about whether we want different user/canonical parts. But to the but: this is anyway low-level and somehow to be used only in the kernel.

• Scheme 3 (to suggest that make1/make2 are building a canonical name):

  • Constant.make2 -> Constant.make_canonical
  • Constant.make1 -> Constant.make_canonical_of_kn
  • Constant.make -> Constant.make_pair (or unchanged)
    But risk of confusion between a canonical name and the canonical part of a name?

• Scheme 4 (to oppose buiding a pair of different or same names):

  • Constant.make2 -> Constant.make_same
  • Constant.make1 -> Constant.make_same_of_kn
  • Constant.make -> Constant.make_pair (or unchanged)

Additionally, when looking at when these functions are used, one can see that it is often to do low-level manipulation to implement higher-level functionalities such as is_canonical : Constant.t -> bool, or canonize : Constant.t -> Constant.t. So, I'm considering providing those too. Any opinion? In particular, by doing so, the need for another cryptic name, Constant.repr2, disappears.

Same for MutInd of course.

Gaëtan Gilbert (Dec 20 2021 at 19:48):

I like n°3 best

Emilio Jesús Gallego Arias (Dec 20 2021 at 22:24):

Would it make sense to have somethin glike Constant.Canonical.t ?

Gaëtan Gilbert (Dec 20 2021 at 22:33):

what would that be?

Emilio Jesús Gallego Arias (Dec 21 2021 at 00:18):

A projection?

Hugo Herbelin (Dec 21 2021 at 09:20):

For the record #15391 implements scheme 1 and this branch implements scheme 3. Also, a variant for scheme 1 would be to have not ~user but ~canonical optional.

Last updated: Oct 08 2024 at 16:02 UTC