Stream: jsCoq

Topic: `Inspect` in the presence of modules


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 16:44):

The reference code for this is indeed Search

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 16:52):

Ok yeah I'm going super deep :D

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 16:57):

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

view this post on Zulip 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.

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 16:58):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 16:58):

Oh, module inclusion maybe?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 16:58):

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

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 16:59):

Is there a way to track this?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 16:59):

in the sense of the operations not respecting the quotient

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 16:59):

what is a quotient? set of modules?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 17:00):

quotient of names

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 17:00):

so when including modules / using functors

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 17:00):

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

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 17:01):

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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 17:17):

There may be , but I am not familiar with it

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Shachar Itzhaky (Aug 05 2021 at 16:22):

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

view this post on Zulip Pierre-Marie Pédrot (Aug 05 2021 at 16:24):

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

view this post on Zulip Pierre-Marie Pédrot (Aug 05 2021 at 16:25):

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

view this post on Zulip Pierre-Marie Pédrot (Aug 05 2021 at 16:25):

that is, internally we know that user := canonical

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Pierre-Marie Pédrot (Aug 05 2021 at 21:22):

similarly for X.ddd

view this post on Zulip Pierre-Marie Pédrot (Aug 05 2021 at 21:22):

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

view this post on Zulip 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)

view this post on Zulip Shachar Itzhaky (Aug 06 2021 at 18:55):

Thanks, I'll look into it!


Last updated: Sep 28 2023 at 11:01 UTC