I'd like a way to determine (in MetaCoq, ultimately) if a constant will eventually be removed from the nametab. Is there a way (in Ltac, Ltac2, or MetaCoq, or even a convenient way in OCaml, I guess, which I can export to MetaCoq) to determine if a given module path contains any functors in it, or, as an approximation to this, a way to determine whether or not there's currently an open functor (importantly, we must be able to distinguish between open argumentless module/module type, and open functor/functor type)?
you may have to look at the safe_typing modvariant field to tell if an open module is a functor, together with the current modpath
something like
let rec is_open_functor senv mp =
match senv.modvariant with
| NONE | LIBRARY -> false
| (STRUCT (params, senv') | SIG (params, senv')) ->
if ModPath.equal mp senv.modpath then not (List.is_empty params)
else is_open_functor senv' mp
but modvariant is internal to safe_typing
I'm not sure the info is available anywhere else
Should I open an issue for exposing this information as an OCaml interface?
Last updated: Oct 13 2024 at 01:02 UTC