Stream: Coq devs & plugin devs

Topic: determining if a functor is open

Jason Gross (Oct 31 2022 at 16:43):

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)?

Gaëtan Gilbert (Oct 31 2022 at 17:11):

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

Gaëtan Gilbert (Oct 31 2022 at 17:11):

I'm not sure the info is available anywhere else

Jason Gross (Oct 31 2022 at 17:32):

Should I open an issue for exposing this information as an OCaml interface?

Last updated: Apr 19 2024 at 18:01 UTC