Merge pull request #963 from LPCIC/section-inspection

coq.env.section-contents (Fix #950)

Author: gares

Changelog.md

@@ -9,6 +9,8 @@
 ### API:
 - Fix `coq.sort.*` to not rely on puring algebraic universes that will become
   first class in Rocq 10
+- Rename `coq.env.section`, use `coq.env.section-variables`
+- New `coq.env.section-contents` listing the contents of sections.
 
 # [3.2.0] 19/09/2025
 

apps/tc/elpi/compiler1.elpi

@@ -11,7 +11,7 @@ namespace tc {
 
   func has-context-deps gref -> .
   has-context-deps GR :-
-    coq.env.section SectionVars,
+    coq.env.section-variables SectionVars,
     coq.env.dependencies GR _ Deps, 
     std.exists! SectionVars (x\ coq.gref.set.mem (const x) Deps).
 

apps/tc/elpi/tc_aux.elpi

@@ -63,7 +63,7 @@ namespace tc {
   instances-of-current-section InstsFiltered :-
     coq.env.current-section-path SectionPath,
     std.findall (tc.instance SectionPath _ _ _) Insts,
-    coq.env.section SectionVars,
+    coq.env.section-variables SectionVars,
     std.map-filter Insts (x\r\ sigma X\ tc.instance _ r _ _ = x, const X = r, not(std.mem SectionVars X)) InstsFiltered.
 
   func is-instance-gr gref ->.
@@ -182,7 +182,7 @@ namespace tc {
   % [section-var->decl L] decl representing seciton variables with their types
   func section-var->decl -> list prop.
   section-var->decl L :-
-    section-var->decl.aux {coq.env.section} L.
+    section-var->decl.aux {coq.env.section-variables} L.
 
   func time-is-active (func (list string) ->) ->.
   :name "time-is-active"

builtin-doc/coq-builtin.elpi

@@ -749,9 +749,21 @@ external func coq.env.module modpath -> list module-item.
 % type (does not recurse on submodules) *E*
 external func coq.env.module-type modtypath -> list id.
 
-% [coq.env.section GlobalObjects] lists the global objects that are marked
-% as to be abstracted at the end of the enclosing sections
-external func coq.env.section -> list constant.
+% [coq.env.section-variables ConstantsRepresentingVariables] lists all the
+% section variables, i.e. the global objects that are marked as to be
+% abstracted at the end of the enclosing sections
+external func coq.env.section-variables -> list constant.
+
+% [coq.env.section-contents GlobalObjects] lists the global objects that are
+% defined withing the current section
+external func coq.env.section-contents -> list gref.
+
+% Deprecated, use coq.env.section-variables
+  func coq.env.section -> list constant.
+  coq.env.section L :-
+    coq.warning "elpi.deprecated" "elpi.env.section" "use coq.env.section-variables in place of coq.env.section",
+    coq.env.section-variables L.
+  
 
 % [coq.env.dependencies GR MP Deps] Computes the direct dependencies of GR.
 % If MP is given, Deps only contains grefs from that module
@@ -1688,7 +1700,7 @@ external func coq.option.available? list string -> bool.
 % and for all in a .v file which your clients will load. Eg.
 % 
 %   Elpi Query lp:{{ coq.option.add ... }}.
-%   
+% 
 % 
 external func coq.option.add list string, coq.option, bool.
 

src/rocq_elpi_builtins.ml

@@ -1562,6 +1562,19 @@ let apply_proof ~name ~poly env tac pf =
 [%%endif]
 
 
+[%%if coq = "9.0"]
+let section_close_section x =
+  let a,b,_,_ = Section.close_section x in
+  a, b
+[%%elif coq = "9.1"]
+let section_close_section x =
+  let a,b,_,_,_ = Section.close_section x in
+  a, b
+[%%else]
+let section_close_section x =
+  let a,b,_,_ = Section.close_section x in
+  a, b
+[%%endif]
 
 
 
@@ -2135,14 +2148,45 @@ Supported attributes:
     !: (in_elpi_module_type (Environ.lookup_modtype mp env)))),
   DocAbove);
 
-  MLCode(Pred("coq.env.section",
-    Out(list constant, "GlobalObjects",
-    Read(unit_ctx, "lists the global objects that are marked as to be abstracted at the end of the enclosing sections")),
+  MLCode(Pred("coq.env.section-variables",
+    Out(list constant, "ConstantsRepresentingVariables",
+    Read(unit_ctx, "lists all the section variables, i.e. the global objects that are marked as to be abstracted at the end of the enclosing sections")),
   (fun _ ~depth _ _ state ->
      let { section } = mk_coq_context ~options:(default_options ()) state in
      !: (section |> List.map (fun x -> Variable x)) )),
   DocAbove);
 
+  MLCode(Pred("coq.env.section-contents",
+    Out(list (list gref), "GlobalObjects",
+    Read(unit_ctx, "lists the global objects that are defined withing the open sections. Inner section first.")),
+  (fun _ ~depth _ _ state ->
+     let l =
+      let safe_env = Global.safe_env () in
+      let section = Safe_typing.sections_of_safe_env safe_env in
+      let rec aux section =
+        match section with
+        | None -> []
+        | Some s ->
+            let section,l = section_close_section s in
+            List.concat_map (function
+              | Section.SecDefinition c -> [GlobRef.ConstRef c]
+              | Section.SecInductive m -> 
+                  let { Declarations.mind_packets } = Environ.lookup_mind m (Safe_typing.env_of_safe_env safe_env) in
+                  List.init (Array.length mind_packets) (fun i -> GlobRef.IndRef(m,i))
+              ) l :: aux section
+      in
+        aux section
+    in
+     !: l)),
+  DocAbove);
+
+  LPCode {|% Deprecated, use coq.env.section-variables
+  func coq.env.section -> list constant.
+  coq.env.section L :-
+    coq.warning "elpi.deprecated" "elpi.env.section" "use coq.env.section-variables in place of coq.env.section",
+    coq.env.section-variables L.
+  |};
+
   MLCode(Pred("coq.env.dependencies",
     In(gref, "GR",
     In(B.unspec modpath, "MP",

tests/test_API_section.v

@@ -12,7 +12,7 @@ Section SB.
 Variable b : nat.
 Let c := b.
 Elpi Query lp:{{
-  coq.env.section [CA, CB, CC],
+  coq.env.section-variables [CA, CB, CC],
   coq.locate "a" (const CA),
   coq.locate "b" (const CB),
   coq.locate "c" (const CC),
@@ -34,7 +34,7 @@ Elpi Query lp:{{
 }} lp:{{
   coq.env.begin-section "Foo",
   coq.env.add-section-variable "x" _ {{ nat }} X,
-  coq.env.section [X],
+  coq.env.section-variables [X],
   coq.env.add-const "fx" (global (const X)) _ _ _,
   coq.env.end-section.
 }}.
@@ -63,3 +63,28 @@ End Using.
 Check foo : nat.
 Check bar : bool -> nat.
 
+(* section inspection *)
+
+Section Foo.
+
+Variable x : nat.
+Definition a := x + 1.
+
+Section Bar.
+
+Definition b := a.
+Inductive C := .
+
+Elpi Query lp:{{
+  coq.env.section-contents L,
+  std.assert! (L = [ 
+    
+    [ {{:gref C_sind }}, {{:gref C_rec }}, {{:gref C_ind }}, {{:gref C_rect }}, {{:gref C }}, {{:gref b }}, ],
+    
+    [ {{:gref a }}]
+    
+    ]) "bad section listing".
+}}.
+
+End Bar.
+End Foo.