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?
hmm, isn't this a MetaCoq question? Or are you asking about how MetaCoq-modeled stuff works in Coq itself?
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
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
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))
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
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 _ -> []
?
yes
Oh, ew, the current one doesn't ignore inner modules but just fuses them without updating the modpath? (I had glossed over that before)
what do you mean the current one ignores inner modules? it's bugged on them not ignoring AFAICT
Jason Gross has marked this topic as resolved.
Last updated: Jun 09 2023 at 04:01 UTC