Stream: jsCoq

Topic: `Inspect` in the presence of modules

Shachar Itzhaky (Jul 07 2021 at 16:35):

Hi @Emilio Jesús Gallego Arias, I need some advice w.r.t collecting all the global symbols in a loaded library.
So far I have used this code to get a list of global constants and their qualified names:

let full_path_of_kn kn =
  let mp, l = Names.KerName.repr kn in
  Libnames.make_path (Lib.dp_of_mp mp) (Names.Label.to_id l)

let full_path_of_constant c = full_path_of_kn (Names.Constant.user c)

(* Get constants in global scope *)
let inspect_globals ~env () =
  let global_consts = List.to_seq @@
      Environ.fold_constants (fun name _ l -> name :: l) env [] in
  Seq.map full_path_of_constant global_consts

Shachar Itzhaky (Jul 07 2021 at 16:36):

However, when the constant is defined in a module, it seems that Lib.dp_of_mp throws away the ModPath. There are several data structures in the Coq codebase that seem targeted to storing both the DirPath and the ModPath (e.g. Nametab.object_prefix); which is the canonical representation and how do I get it?

Emilio Jesús Gallego Arias (Jul 07 2021 at 16:44):

Wow what a question XDDD as far as I know that's a super mess, can you provide me a pair of input / expected output so I have a look?

Emilio Jesús Gallego Arias (Jul 07 2021 at 16:44):

The reference code for this is indeed Search

Emilio Jesús Gallego Arias (Jul 07 2021 at 16:45):

But why do you need to re-qualify the constant in the first place?

Emilio Jesús Gallego Arias (Jul 07 2021 at 16:46):

IIANW it should already contain the full path, I'm gonna invoke @Pierre-Marie Pédrot @Gaëtan Gilbert and @Hugo Herbelin and they are more knowledgeable about this stuff than myself

Shachar Itzhaky (Jul 07 2021 at 16:52):

Ok yeah I'm going super deep :D

Emilio Jesús Gallego Arias (Jul 07 2021 at 16:53):

I'm afraid I can't comment on the module system in public XD

Shachar Itzhaky (Jul 07 2021 at 16:56):

Here's an example: I am running this function after having loaded (and Required) all of the Coq standard library. Now there is this lemma succ_inj_wd. The About command tells me that it is known as Coq.Arith.PeanoNat.Nat.succ_inj_wd. (btw how is that so? It is defined in NZBase.v.) In the list of symbols, however, it is listed as these:

Shachar Itzhaky (Jul 07 2021 at 16:57):

Screen-Shot-2021-07-07-at-19.56.53.png

Shachar Itzhaky (Jul 07 2021 at 16:57):

So yeah one is Coq.Arith.PeanoNat.succ_inj_wd which is missing the module name Nat.

Shachar Itzhaky (Jul 07 2021 at 16:58):

The others -- I have no idea where they came from.

Emilio Jesús Gallego Arias (Jul 07 2021 at 16:58):

Oh, module inclusion maybe?

Emilio Jesús Gallego Arias (Jul 07 2021 at 16:58):

You have already noticed the UserName / Canonical name mess in the kernel

Shachar Itzhaky (Jul 07 2021 at 16:59):

Is there a way to track this?

Emilio Jesús Gallego Arias (Jul 07 2021 at 16:59):

actually due to the module system having an alias mechanism to do name quotienting, but the last time we looked into it, we were horrified

Emilio Jesús Gallego Arias (Jul 07 2021 at 16:59):

in the sense of the operations not respecting the quotient

Shachar Itzhaky (Jul 07 2021 at 16:59):

what is a quotient? set of modules?

Emilio Jesús Gallego Arias (Jul 07 2021 at 16:59):

I need to look into it as to be of any help, sorry; and thanks for the example

Emilio Jesús Gallego Arias (Jul 07 2021 at 17:00):

quotient of names

Emilio Jesús Gallego Arias (Jul 07 2021 at 17:00):

so when including modules / using functors

Emilio Jesús Gallego Arias (Jul 07 2021 at 17:00):

an equivalence class of names is created, so you indeed equate A.foo with B.C.foo in some cases

Emilio Jesús Gallego Arias (Jul 07 2021 at 17:00):

but this was implemented, not very cleanly I'd say

Shachar Itzhaky (Jul 07 2021 at 17:01):

oh ok; is there a way to know which one of them is the "original"?

Shachar Itzhaky (Jul 07 2021 at 17:02):

I am surprised that I don't also get Numbers.NatInt.NZBase.succ_inj_wd as one of the results.

Emilio Jesús Gallego Arias (Jul 07 2021 at 17:17):

There may be , but I am not familiar with it

Clément Pit-Claudel (Aug 05 2021 at 14:50):

If I'm following correctly, there should be a way to go back to the "canonical" name, because the "Locate" command knows how to do it: it prints alias of … after printing the name of a constant.

Clément Pit-Claudel (Aug 05 2021 at 14:53):

Module Test1.
  Module AAA.
    Module BBB.
      Module CCC.
        Definition ddd := 1.
      End CCC.
    End BBB.
  End AAA.

  Module X.
    Include AAA.BBB.CCC.
  End X.

  Module Y.
    Include X.
  End Y.

  About Y.ddd. (* Expands to: Constant test.Test1.Y.ddd *)
  Locate test.Test1.Y.ddd. (* alias of AAA.BBB.CCC.ddd *)
  About AAA.BBB.CCC.ddd. (* Expands to: Constant test.Test1.AAA.BBB.CCC.ddd *)
  Locate test.Test1.AAA.BBB.CCC.ddd. (* no more aliases *)
End Test1.

Shachar Itzhaky (Aug 05 2021 at 16:22):

Yes, I should definitely investigate the implementations of Search, Locate, About, etc.

Pierre-Marie Pédrot (Aug 05 2021 at 16:24):

Kernel names contain both the "user" and the "canonical" names.

Pierre-Marie Pédrot (Aug 05 2021 at 16:25):

morally, this is a hidden δ-step that is hidden (sometimes) in the upper layers

Pierre-Marie Pédrot (Aug 05 2021 at 16:25):

that is, internally we know that user := canonical

Pierre-Marie Pédrot (Aug 05 2021 at 16:26):

long story short, this was devised to make the tactic layer happy w.r.t. modules

Shachar Itzhaky (Aug 05 2021 at 21:15):

What is the semantics of "user" vs. "canonical"? E.g. what would be the user and canonical names of the various occurrences of ddd in @Clément Pit-Claudel's example above?

Pierre-Marie Pédrot (Aug 05 2021 at 21:22):

If I am not mistaken, for Y.ddd that would be (user := Y.ddd, canonical := AAA.BBB.CCC.ddd)

Pierre-Marie Pédrot (Aug 05 2021 at 21:22):

similarly for X.ddd

Pierre-Marie Pédrot (Aug 05 2021 at 21:22):

for AAA.BBB.CCC.ddd the two would coincide

Pierre-Marie Pédrot (Aug 05 2021 at 21:23):

(add a Test1 in front of everybody, I've just realized there was an enclosing module)

Shachar Itzhaky (Aug 06 2021 at 18:55):

Thanks, I'll look into it!

Last updated: May 31 2023 at 04:01 UTC