Michael Soegtrop (Oct 11 2022 at 10:48): Michael Soegtrop (Oct 11 2022 at 10:48):I was exploring the module API based on the coq-elpi test file test_API_module.v.
I modified it to print a different module but get an error:
From elpi Require Import elpi.
Require Import compcert.cfrontend.Clight.
Elpi Command modules.
(* module *)
Print Module Datatypes.
Elpi Query lp:{{ coq.locate-module "Datatypes" MP, coq.env.module MP L }}.
Print Module Clight.
Elpi Query lp:{{ coq.locate-module "Clight" MP, coq.env.module MP L }}.
The second query results in "Not Yet Implemented: HOAS SFBmind" while the first query (from the original file) works.
Michael Soegtrop (Oct 11 2022 at 10:49):It seems to find the module:
Print Module Clight.
Elpi Query lp:{{ coq.locate-module "Clight" MP }}.
=>
Query assignments:
MP = «compcert.cfrontend.Clight»
since that error comes from src/coq_elpi_HOAS.ml, I suspect the module interface uses some construct that can't be reified in Elpi yet
Paolo Giarrusso (Oct 11 2022 at 11:26):comparing this against kernel/declarations.ml suggests the limitation is on mutual inductives with more than one branch?
| Declarations.SFBmind { Declarations.mind_packets = [| _ |] } ->
[GlobRef.IndRef (MutInd.make2 path name, 0)]
| Declarations.SFBmind _ -> nYI "HOAS SFBmind"
Yes, I tried to document what Elpi does not support yet here:
coq.env.module gives you a list of handles to the objects in the module, since mutual inductives are not supported yet, you get this error (which sure could be improved).
Enrico Tassi (Oct 11 2022 at 11:50):The best I can do is to make this API not fail, but only list the objects it can actually handle. But that would be confusing too :-/
Enrico Tassi (Oct 11 2022 at 11:51):@Michael Soegtrop which application do you have in mind?
Michael Soegtrop (Oct 11 2022 at 11:57):I am working on speeding up VST by replacing simpl with cbv with explicit delta list. The difference is quite dramatic - in many cases milliseconds instead of minutes. Also it should be more robust.
In that I am working on managing the involved largish (few 100) symbol lists. What I would like to have is a way to add all defined symbols in a module to a list of symbols I can use with cbv.
Originally I wanted to do it in Ltac2, but Ltac2 does not have an API to list the contents of a module. Not sure if @Pierre-Marie Pédrot made progress with this.
This is essentially what I was talking about in the working group meeting in June.
Michael Soegtrop (Oct 11 2022 at 12:00):One question: is the problem with coq.env.module as such, or is the problem with printing the result?
Paolo Giarrusso (Oct 11 2022 at 12:05):AFAICT, the problem is not with printing but with coq.env.module. And really, it's a limitation of the coq-elpi type of Coq terms:
coq.env.module returns a coq-elpi AST, so it must translate the Coq AST into a coq-elpi one, and but the translation fails here
Michael Soegtrop (Oct 11 2022 at 12:15):I wonder if there is an API to just get the identifiers defined in the module - in the end I just want to have the identifiers.
Enrico Tassi (Oct 11 2022 at 12:45):I'm looking at the code, and I this I was too strict. I could give you a handle to all objects, including mutual inductive. The rest of the APIs would then complain nYI, but it would make coq.env.module "future proof" in some sense.
Enrico Tassi (Oct 11 2022 at 12:48):But the API is already ugly (see the "E") marker for experimental. For example I'm not sure recursing on submodules is what one wants.
So, I don't mind changing it for a better one. But I need use cases and here you can help.
Enrico Tassi (Oct 11 2022 at 12:48):So, to answer your question, I don't have an API to do what you need out of the box, but I'm happy to improve that one.
Enrico Tassi (Oct 11 2022 at 12:50):To me an API like coq.env.dependencies seems more appropriate, maybe binding coq.search would also do (imagine flags like you have in Search).
In your use case, after having the list of ids in a module, what do you have to do? How do you filter them?
Michael Soegtrop (Oct 11 2022 at 13:07):As far as I can tell it would do to take all transparent definitions of a module. This are usually modules of VST or CompCert handling certain aspects. Usually one wants this fully expanded, while everything from the user domain (the topic the C code is about) shall remain untouched.
Enrico Tassi (Oct 11 2022 at 13:10):So the recursive traversal coq.env.module does suits you, right?
Michael Soegtrop (Oct 11 2022 at 13:11):I don't think "coq.env.dependencies" or "coq.search" would be very effective. I usually treat a module as a certain abstraction level or aspect and want to keep it or want it reduced.
A typical example from outside VST: when I work with rationals, I frequently want all the rational stuff removed and everything reduced to the ZArith level. The easiest and most reliable way to do this is to cbv delta [<all functions in QArith>].
Michael Soegtrop (Oct 11 2022 at 13:12):So the recursive traversal coq.env.module does suits you, right?
You mean recursive inclusion of submodules? I would think it would be best to make this optional - if I have to choose I would make ti non recursive and do the recusion manually.
Michael Soegtrop (Oct 11 2022 at 13:12):E.g. it does happen that I want all submodules of module X except X.Y and X.Z.
Michael Soegtrop (Oct 11 2022 at 13:14):If the question was "do you want module traversal" the answer is yes, this is what I want, since modules are a reasonable abstraction of abstraction levels of aspects in Coq.
Michael Soegtrop (Oct 11 2022 at 13:15):Btw.: can I get a list of fully qualified IDs - it shouldn't matter than what the definition is.
Enrico Tassi (Oct 11 2022 at 14:09):This is what you get today, a gref is a "kernel name", you have API to get the id part, but also the path as a list of strings.
Look for gref->id and gref->path.
So I have the impression that making it "not fail" on mutual inductives would already enable you to do what you want.
(well, we don'have a Coq database yet you can write to this list, but that is orthogonal)
Michael Soegtrop (Oct 11 2022 at 15:30):Maybe I can somehow put it together with Ltac2 ...
Michael Soegtrop (Oct 11 2022 at 15:30):You have a commit for me?
Enrico Tassi (Oct 11 2022 at 15:52):Sorry, I don't have it today, I can open a PR tomorrow.
Enrico Tassi (Oct 11 2022 at 15:53):Michael Soegtrop said:
Maybe I can somehow put it together with Ltac2 ...
Are you saying that Ltac2 has already the API to register a set of names to be used as a cbv argument?
Michael Soegtrop (Oct 11 2022 at 15:57):Yes, this is easy in Ltac2. The reduction functions take an argument of type "red_flags" which contains a reference list used for delta reductions. See red_flags
Michael Soegtrop (Oct 11 2022 at 15:59):One can use a computed rConst list.
Michael Soegtrop (Oct 11 2022 at 16:01):The cbv tactic in Ltac2 is just a notation for this using a built in parser which produces red_flags structures from the usual syntax. See cbv
Michael Soegtrop (Oct 11 2022 at 16:03):The idea is to upfront compute red_flags structures for specific purposes e.g. from a list of modules.
Last updated: Jun 06 2023 at 22:01 UTC