Stream: Coq devs & plugin devs

Topic: ✔ getting the list of constants in a module

Jason Gross (Feb 21 2023 at 21:13):

I'm looking at the code in MetaCoq for quoting modules:

let quote_module (qualid : qualid) : global_reference list =
  let mp = Nametab.locate_module qualid in
  let mb = Global.lookup_module mp in
  let rec aux mb =
    let open Declarations in
    let me = mb.mod_expr in
    let get_refs s =
      let body = Modops.destr_nofunctor mp s in
      let get_ref (label, field) =
        let open Names in
        match field with
        | SFBconst _ -> [GlobRef.ConstRef (Constant.make2 mp label)]
        | SFBmind _ -> [GlobRef.IndRef (MutInd.make2 mp label, 0)]
        | SFBmodule mb -> aux mb
        | SFBmodtype mtb -> []
      in
      CList.map_append get_ref body
    in
    match me with
    | Abstract -> []
    | Algebraic _ -> []
    | Struct s -> get_refs s
    | FullStruct -> get_refs mb.Declarations.mod_type
  in aux mb

Am I correct that the handling of Algebraic _ -> [] is what results in the empty list being returned for bound modules and bound aliases?

But what is responsible for the fact that this procedure sometimes returns duplicates?

Karl Palmskog (Feb 21 2023 at 21:18):

hmm, isn't this a MetaCoq question? Or are you asking about how MetaCoq-modeled stuff works in Coq itself?

Gaëtan Gilbert (Feb 21 2023 at 21:19):

the duplicates may be because of

        | SFBmodule mb -> aux mb

recursing in submodules without updating the module path mp
so f you have

Module Bla.
Module Bla'.
Definition t := ...
End Bla'.
Definition t := ...
End Bla.

quoting Bla will put Bla.t twice in the list instead of 1 Bla.t and 1 Bla.Bla'.t

Gaëtan Gilbert (Feb 21 2023 at 21:21):

Am I correct that the handling of Algebraic _ -> [] is what results in the empty list being returned for bound modules and bound aliases?

that sounds plausible
I'm not sure what the spec of this thing is but probably it should be looking at mb.mod_type all the time and ignore mb.mod_expr

Gaëtan Gilbert (Feb 21 2023 at 21:26):

basically I think it should be something like

let rec quote_module mb : GlobRef.t list =
  let open Declarations in
  match mb.mod_type with
  | MoreFunctor _ -> [] (* current version errors, not sure what is wanted *)
  | NoFunctor fields ->
    let get_ref (label, field) =
      let open Names in
      match field with
      | SFBconst _ -> [GlobRef.ConstRef (Constant.make2 mb.mod_mp label)]
      | SFBmind _ -> [GlobRef.IndRef (MutInd.make2 mb.mod_mp label, 0)]
      | SFBmodule mb -> quote_module mb
      | SFBmodtype mtb -> []
    in
    CList.map_append get_ref fields

let quote_module qualid = quote_module (Global.lookup_module (Nametab.locate_module qualid))

Gaëtan Gilbert (Feb 21 2023 at 21:27):

Karl Palmskog said:

hmm, isn't this a MetaCoq question? Or are you asking about how MetaCoq-modeled stuff works in Coq itself?

it can be considered a plugin dev question IMO

Jason Gross (Feb 21 2023 at 21:44):

nods Thank you! (Yes, I'm asking about how the stuff works in Coq itself.)

If we want the function to ignore inner modules (as the current one does), then SFBmodule mb -> quote_module mb should be replaced by SFBmodule _ -> []?

Gaëtan Gilbert (Feb 21 2023 at 21:44):

yes

Jason Gross (Feb 21 2023 at 21:45):

Oh, ew, the current one doesn't ignore inner modules but just fuses them without updating the modpath? (I had glossed over that before)

Gaëtan Gilbert (Feb 21 2023 at 21:45):

what do you mean the current one ignores inner modules? it's bugged on them not ignoring AFAICT

Notification Bot (Feb 21 2023 at 21:48):

Jason Gross has marked this topic as resolved.

Last updated: Dec 07 2023 at 14:02 UTC