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
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?
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?
The reference code for this is indeed Search
But why do you need to re-qualify the constant in the first place?
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
Ok yeah I'm going super deep :D
I'm afraid I can't comment on the module system in public XD
Here's an example: I am running this function after having loaded (and Require
d) 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:
Screen-Shot-2021-07-07-at-19.56.53.png
So yeah one is Coq.Arith.PeanoNat.succ_inj_wd
which is missing the module name Nat
.
The others -- I have no idea where they came from.
Oh, module inclusion maybe?
You have already noticed the UserName / Canonical name mess in the kernel
Is there a way to track this?
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
in the sense of the operations not respecting the quotient
what is a quotient? set of modules?
I need to look into it as to be of any help, sorry; and thanks for the example
quotient of names
so when including modules / using functors
an equivalence class of names is created, so you indeed equate A.foo
with B.C.foo
in some cases
but this was implemented, not very cleanly I'd say
oh ok; is there a way to know which one of them is the "original"?
I am surprised that I don't also get Numbers.NatInt.NZBase.succ_inj_wd
as one of the results.
There may be , but I am not familiar with it
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.
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.
Yes, I should definitely investigate the implementations of Search, Locate, About, etc.
Kernel names contain both the "user" and the "canonical" names.
morally, this is a hidden δ-step that is hidden (sometimes) in the upper layers
that is, internally we know that user := canonical
long story short, this was devised to make the tactic layer happy w.r.t. modules
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?
If I am not mistaken, for Y.ddd
that would be (user := Y.ddd, canonical := AAA.BBB.CCC.ddd)
similarly for X.ddd
for AAA.BBB.CCC.ddd
the two would coincide
(add a Test1
in front of everybody, I've just realized there was an enclosing module)
Thanks, I'll look into it!
Last updated: Sep 28 2023 at 11:01 UTC