[api] coq.env.module precise description of contents

Author: gares

Changelog.md

@@ -6,6 +6,7 @@
   - Change `coq.env.module` and `coq.env.module-type` do not fail if the
     module (type) contains a mutual inductive. The resulting `gref` is going
     to me unusable with most APIs, though.
+  - Change `coq.env.module` returns a ADT describing the module contents
   - Change `coq.gref->path` and `coq.gref->id` do work on `gref` which point
     to mutual inductives.
   - New `coq.env.term-dependencies` computing all the `grefs` occurring in a term.

apps/locker/elpi/locker.elpi

@@ -106,7 +106,7 @@ make-key-unlockable ID DefBo Ty LockedDef Key :- std.do! [
 
 pred make-module-unlockable i:id, i:modpath.
 make-module-unlockable ID Module :- std.do! [
-  coq.env.module Module [_,UnlockEQ],
+  coq.env.module Module [_,gref UnlockEQ],
   coq.env.global UnlockEQ UnlockEQT,
   Unlock = {{ Unlockable lp:UnlockEQT }},
   make-unlockable ID Unlock,

coq-builtin.elpi

@@ -679,9 +679,17 @@ external pred coq.locate-module i:id, o:modpath.
 % error if ModName cannot be located. *E*
 external pred coq.locate-module-type i:id, o:modtypath.
 
+% Contents of a module
+kind module-item type.
+type submodule modpath -> list module-item -> module-item.
+type module-type modtypath -> module-item.
+type gref gref -> module-item.
+type module-functor modpath -> list modtypath -> module-item.
+type module-type-functor modtypath -> list modtypath -> module-item.
+
 % [coq.env.module MP Contents] lists the contents of a module (recurses on
 % submodules) *E*
-external pred coq.env.module i:modpath, o:list gref.
+external pred coq.env.module i:modpath, o:list module-item.
 
 % [coq.env.module-type MTP Entries] lists the items made visible by module
 % type (does not recurse on submodules) *E*

examples/example_reduction_surgery.v

@@ -14,7 +14,7 @@ gref->redflag (const C) (coq.redflags.const C).
 solve (goal _ _ Ty _ [str M] as G) GS :-
   coq.locate-module M MP,
   coq.env.module MP GREFS,
-  std.filter GREFS (x\x = const _) CONSTANTS,
+  std.map-filter GREFS (x\r\x = gref r, r = (const _)) CONSTANTS,
   std.map CONSTANTS (gr\r\ coq.env.transitive-dependencies gr _ r) DEPS,
   std.fold DEPS {coq.gref.set.empty} coq.gref.set.union ALLDEPS,
   std.append CONSTANTS {coq.gref.set.elements ALLDEPS} All,

src/coq_elpi_HOAS.ml

@@ -3413,15 +3413,32 @@ let lp2skeleton ~depth coq_ctx constraints state t =
 
 (* {{{  Declarations.module_body -> elpi ********************************** *)
 
-let rec in_elpi_module_item ~depth path state (name, item) = match item with
-  | Declarations.SFBconst _ ->
-      [GlobRef.ConstRef (Constant.make2 path name)]
-  | Declarations.SFBmind { Declarations.mind_packets } ->
-      CList.init (Array.length mind_packets) (fun i -> GlobRef.IndRef (MutInd.make2 path name,i))
-  | Declarations.SFBmodule mb -> in_elpi_module ~depth state mb
-  | Declarations.SFBmodtype _ -> []
-
-and in_elpi_module : 'a. depth:int -> API.Data.state -> 'a Declarations.generic_module_body -> GlobRef.t list =
+type module_item =
+  | Module of Names.ModPath.t * module_item list
+  | ModuleType of Names.ModPath.t
+  | Gref of Names.GlobRef.t
+  | Functor of Names.ModPath.t * Names.ModPath.t list
+  | FunctorType of Names.ModPath.t * Names.ModPath.t list
+
+let rec in_elpi_module_item ~depth path state (name, item) =
+  let open Declarations in
+  match item with
+  | SFBconst _ ->
+      [Gref (GlobRef.ConstRef (Constant.make2 path name))]
+  | SFBmind { mind_packets } ->
+      CList.init (Array.length mind_packets) (fun i -> Gref (GlobRef.IndRef (MutInd.make2 path name,i)))
+  | SFBmodule ({ mod_mp; mod_type = NoFunctor _ } as b) -> [Module (mod_mp,in_elpi_module ~depth state b) ]
+  | SFBmodule { mod_mp; mod_type = MoreFunctor _ as l } -> [Functor(mod_mp,functor_params l)]
+  | SFBmodtype { mod_mp; mod_type = NoFunctor _ }  -> [ModuleType mod_mp]
+  | SFBmodtype { mod_mp; mod_type = MoreFunctor _ as l }  -> [FunctorType (mod_mp,functor_params l)]
+
+and functor_params x =
+  let open Declarations in
+  match x with
+  | MoreFunctor(_,{ mod_type_alg = Some (NoFunctor (MEident mod_mp)) },rest) -> mod_mp :: functor_params rest
+  | _ -> [] (* XXX non trivial functors, eg P : X with type a = nat, are badly described (no params) *)
+
+and in_elpi_module : 'a. depth:int -> API.Data.state -> 'a Declarations.generic_module_body -> module_item list =
   fun ~depth state { Declarations.
   mod_mp;             (* Names.module_path *)
   mod_expr;           (* Declarations.module_implementation *)

src/coq_elpi_HOAS.mli

@@ -231,7 +231,14 @@ val modtypath : Names.ModPath.t Conversion.t
 val module_inline_default : Declaremods.inline Conversion.t
 val reduction_flags : CClosure.RedFlags.reds Conversion.t
 
-val in_elpi_module : depth:int -> State.t -> Declarations.module_body -> GlobRef.t list
+type module_item =
+  | Module of Names.ModPath.t * module_item list
+  | ModuleType of Names.ModPath.t
+  | Gref of Names.GlobRef.t
+  | Functor of Names.ModPath.t * Names.ModPath.t list
+  | FunctorType of Names.ModPath.t * Names.ModPath.t list
+
+val in_elpi_module : depth:int -> State.t -> Declarations.module_body -> module_item list
 val in_elpi_module_type : Declarations.module_type_body -> string list
 
 val coercion_status : coercion_status Conversion.t

src/coq_elpi_builtins.ml

@@ -616,6 +616,30 @@ let reduction_kind = let open API.AlgebraicData in let open CClosure.RedFlags in
   ]
 } |> CConv.(!<)
 
+
+let module_item = let open API.AlgebraicData in declare {
+  ty = Conv.TyName "module-item";
+  doc = "Contents of a module";
+  pp = (fun fmt a -> Format.fprintf fmt "TODO");
+  constructors = [
+    K("submodule","",A(modpath,C(CConv.(!>>) B.list,N)),
+      B (fun s l -> Module(s,l) ),
+      M (fun ~ok ~ko -> function Module(s,l) -> ok s l | _ -> ko ()));
+    K("module-type","",A(modtypath,N),
+      B (fun s -> ModuleType s),
+      M (fun ~ok ~ko -> function ModuleType s -> ok s | _ -> ko ()));
+    K("gref","",A(gref,N),
+      B (fun s -> Gref s),
+      M (fun ~ok ~ko -> function Gref x -> ok x | _ -> ko ()));
+    K("module-functor","",A(modpath,A(B.list modtypath,N)),
+      B (fun s a -> Functor(s,a)),
+      M (fun ~ok ~ko -> function Functor(s,a) -> ok s a | _ -> ko ()));
+    K("module-type-functor","",A(modtypath,A(B.list modtypath,N)),
+      B (fun s a -> FunctorType(s,a)),
+      M (fun ~ok ~ko -> function FunctorType(s,a) -> ok s a | _ -> ko ()));
+  ]
+} |> CConv.(!<)
+  
 let attribute a = let open API.AlgebraicData in declare {
   ty = Conv.TyName "attribute";
   doc = "Generic attribute";
@@ -1619,9 +1643,11 @@ Supported attributes:
     !:mp)),
   DocAbove);
 
+  MLData module_item;
+
   MLCode(Pred("coq.env.module",
     In(modpath, "MP",
-    Out(list gref, "Contents",
+    Out(list module_item, "Contents",
     Read(global, "lists the contents of a module (recurses on submodules) *E*"))),
   (fun mp _ ~depth {env} _ state ->
     let t = in_elpi_module ~depth state (Environ.lookup_module mp env) in

tests/test_API_module.v

@@ -18,12 +18,14 @@ End X.
 
 Elpi Query lp:{{
   coq.locate-module "X" MP,
-  coq.env.module MP [
-    (indt Xi), (const _), (const _), (const _), (const _),
-    (const _),
-    (indt XYi), (const XYr), (const _), (const _), (const _),
-    (const _)
-  ],
+  coq.env.module MP L,
+  std.assert! (L = [
+    gref (indt Xi), gref (const _), gref (const _), gref (const _), gref (const _),
+    gref (const _),
+    submodule _ [
+      gref (indt XYi), gref (const XYr), gref (const _), gref (const _), gref (const _),
+    gref (const _)]
+  ]) "bad module",
   coq.say {coq.gref->string (indt Xi)},
   rex_match "\\(Top.\\|.*test_API_module\\)\\.X\\.i$" {coq.gref->string (indt Xi)},
   rex_match "\\(Top.\\|.*test_API_module\\)\\.X\\.Y\\.i$" {coq.gref->string (indt XYi)},
@@ -43,7 +45,7 @@ End Y.
 
 Elpi Query lp:{{ 
     coq.locate-module "Y" MP,
-    coq.env.module MP [indt I, indt J, |_],
+    coq.env.module MP [gref (indt I), gref (indt J), |_],
     coq.gref->path (indt I) P,
     coq.gref->id (indt J) ID
 }}.
@@ -120,3 +122,40 @@ Elpi Query lp:{{
 
 Print ITA.
 
+
+Module R.
+  Module S.
+    Definition x := 3.
+  End S.
+  Module Type P1.
+    Parameter x : nat.
+  End P1.
+  Module Type P2.
+    Parameter y : nat.
+  End P2.
+  Module F(A : P1)(B : P2).
+    Definition z := A.x + B.y.
+  End F.
+  Module Type FT(A : P2)(B : P1).
+    Definition z := A.y + B.x.
+  End FT.
+  Definition a := 1.
+End R.
+
+Elpi Query lp:{{
+  coq.locate-module "R" R,
+  coq.locate-module "R.S" S,
+  coq.locate-module-type "R.P1" P1,
+  coq.locate-module-type "R.P2" P2,
+  coq.locate-module "R.F" F,
+  coq.locate-module-type "R.FT" FT,
+  coq.env.module R L,
+  std.assert! (L = [
+    submodule S [gref (const _)], 
+    module-type P1, 
+    module-type P2, 
+    module-functor F [P1,P2],
+    module-type-functor FT [P2,P1], 
+    gref (const _)
+  ]) "bad module"
+}}.