Gaëtan Gilbert (Feb 02 2024 at 13:23): Gaëtan Gilbert (Feb 02 2024 at 13:23):I'm looking into designing a set of APIs to look into modules. Something like the attached file:
Module.v
(no implementation yet, no point if we decide we don't want these APIs)
Most of it should be forward compatible except
Ltac2 Type module_field := [ Submodule (module_reference) | Reference (Std.reference) ].
Ltac2 @ external module_contents : module_reference -> module_field list option := ...
(** Returns [None] on functors and module types. *)
for instance https://github.com/coq/coq/pull/18038 adds a "rewrite rule block" field which I guess would add a constructor (currently with no useful APIs) to module_field.
I'm not sure there's a nice forward_compatible API though.
cc @Pierre-Marie Pédrot @Michael Soegtrop
Jason Gross (Feb 07 2024 at 22:04):You could make it forward-compatible by breaking up module_contents into a collection of functions submodules, references, etc.
Jason Gross (Feb 07 2024 at 22:04):It might be nice to also provide a is_global_module (or similar) which is false if the given module reference or any parent is a functor, bound, or a modtype. (Basically I want to know if constants inside a(n open) module will be accessible after the end of the current file.)
Gaëtan Gilbert (Feb 07 2024 at 22:10):Jason Gross said:
You could make it forward-compatible by breaking up
module_contentsinto a collection of functionssubmodules,references, etc.
only if we forget the order between submodules and references though
Jason Gross (Feb 07 2024 at 22:12):Oh, I see.
Jason Gross (Feb 07 2024 at 22:16):Not sure if this is a good idea, but you could Church-encode the module_field and uncurry the arguments into a record. That is, have a record of 'a module_field_handlers := { handle_submodule : module_reference -> 'a option ; handle_reference : Std.reference -> 'a option } and then make filter_map : 'a module_field_handlers -> module_reference -> ('a list) option. Then if you provide default_module_field_handlers that return None on everything, you can use record update syntax to support additions in a forward-compatible way.
Jason Gross (Feb 07 2024 at 22:18):Even if it will produce a functor or module type, it will be treated as a regular module for the APIs in this file.
Does this mean that module_contents (current_module ()) returns None? What about is_modtype (current_module ()), is_functor (current_module ())?
Gaëtan Gilbert (Feb 07 2024 at 22:21):Does this mean that module_contents (current_module ()) returns None?
no, it returns Some of whatever has been defined so far
current_module is treated as a regular module so not is_modtype, not is_functor
Gaëtan Gilbert (Feb 07 2024 at 22:25):I think it makes sense to have moule_contents be useful, and then I want the results of the other APIs to be consistent with that
but maybe it's worth having is_modtype & co return what they would return after the module is finished even if it means we lose properties like is_modtype foo = true -> module_contents foo = None
Jason Gross (Feb 07 2024 at 23:10):Yeah, I think is_modtype and is_functor should report accurately on the currently open module (rather than always returning false on it). Otherwise there's no way to access that information. I agree that module_contents should return Some on the currently open module, but I don't think is_modtype foo = true -> module_contents foo = None is particularly useful. (is_modtype foo || is_functor foo = false -> module_contents foo = Some seems like a more useful property to enforce)
Michael Soegtrop (Feb 08 2024 at 10:20):@Gaëtan Gilbert : this API would definitely be a great addition! My thoughts:
to_message - IMHO this fits nicer with the predefined of_xyz functions in Messages.vNone and Some [] is for module_contentsLast updated: Oct 12 2024 at 12:01 UTC