Add SearchDependRecursive command for transitive dependency analysis

Make_coq.local

@@ -52,6 +52,7 @@ TESTDIR=tests
 TESTS_SRC=$(TESTDIR)/Morph.v $(TESTDIR)/Test.v $(TESTDIR)/Polymorph.v \
 	  $(TESTDIR)/PrimitiveProjections.v\
 	  $(TESTDIR)/Morph.cmd $(TESTDIR)/Test.cmd $(TESTDIR)/search.cmd \
+	  $(TESTDIR)/search_recursive.cmd $(TESTDIR)/search_comparison.cmd \
           $(TESTDIR)/Polymorph.cmd $(TESTDIR)/PrimitiveProjections.cmd
 TESTS_DPD=$(TESTDIR)/graph.dpd $(TESTDIR)/graph2.dpd \
 	  $(TESTDIR)/Morph.dpd $(TESTDIR)/Morph_rw.dpd \
@@ -62,7 +63,8 @@ TESTS_DOT=$(TESTS_DPD:%.dpd=%.dot)
 TESTS_ERR_DPD=$(wildcard $(TESTDIR)/*.err.dpd)
 
 TESTS=$(TESTS_DPD) $(TESTS_DOT) $(TESTDIR)/graph.without.dot \
-      $(TESTDIR)/search  $(TESTDIR)/graph2.dpdusage \
+      $(TESTDIR)/search $(TESTDIR)/search_recursive $(TESTDIR)/search_comparison \
+      $(TESTDIR)/graph2.dpdusage \
       $(TESTS_ERR_DPD:%.dpd=%) $(TESTDIR)/file_not_found.err
 TESTS_LOG=$(TESTS:%=%.log)
 TESTS_ORACLE=$(TESTS:%=%.oracle)
@@ -144,6 +146,14 @@ $(TESTDIR)/search.log : $(TESTDIR)/Test.vo $(TESTDIR)/search.cmd $(DPDPLUGIN)
 	cd $(TESTDIR) ; coqtop $(TEST_INCLUDE) < search.cmd 2> /dev/null \
 	  | sed -e 's/Welcome to Rocq.*/Welcome to Rocq/' > ../$@
 
+$(TESTDIR)/search_recursive.log : $(TESTDIR)/Test.vo $(TESTDIR)/search_recursive.cmd $(DPDPLUGIN)
+	cd $(TESTDIR) ; coqtop $(TEST_INCLUDE) < search_recursive.cmd 2> /dev/null \
+	  | sed -e 's/Welcome to Rocq.*/Welcome to Rocq/' > ../$@
+
+$(TESTDIR)/search_comparison.log : $(TESTDIR)/Test.vo $(TESTDIR)/search_comparison.cmd $(DPDPLUGIN)
+	cd $(TESTDIR) ; coqtop $(TEST_INCLUDE) < search_comparison.cmd 2> /dev/null \
+	  | sed -e 's/Welcome to Rocq.*/Welcome to Rocq/' > ../$@
+
 %.dot : %.dpd  $(DPD2DOT)
 	$(DPD2DOT) $< > /dev/null
 

searchdepend.mlg

@@ -77,20 +77,52 @@ let collect_dependance opaque_access gref =
       let ca = indbody.Declarations.mind_user_lc in
         Array.fold_right (collect_long_names [fst i]) ca Data.empty
 
+let display_data d =
+  let pp gr n s =
+    Printer.pr_global gr ++ str "(" ++ int n ++ str ")" ++ spc() ++s
+  in
+  Feedback.msg_notice (str"[" ++ ((Data.fold pp) d (str "]")))
+
 let display_dependance ~opaque_access gref =
-  let display d =
-    let pp gr n s =
-      Printer.pr_global gr ++ str "(" ++ int n ++ str ")" ++ spc() ++s
-    in
-      Feedback.msg_notice (str"[" ++ ((Data.fold pp) d (str "]")))
-  in try let data = collect_dependance opaque_access gref in display data
+  try let data = collect_dependance opaque_access gref in display_data data
   with NoDef gref ->
     CErrors.user_err (Printer.pr_global gref ++ str " has no value")
 
+let collect_dependance_recursive ~opaque_access gref =
+  let rec aux visited acc gref =
+    if Names.GlobRef.Set.mem gref visited then (visited, acc)
+    else
+      let visited = Names.GlobRef.Set.add gref visited in
+      try
+        let deps = collect_dependance opaque_access gref in
+        let acc = Names.GlobRef.Map.fold
+          (fun dep_gref count acc ->
+            let n = try Names.GlobRef.Map.find dep_gref acc with Not_found -> 0 in
+            Names.GlobRef.Map.add dep_gref (n + count) acc)
+          deps acc
+        in
+        Names.GlobRef.Map.fold
+          (fun dep_gref _ (visited, acc) -> aux visited acc dep_gref)
+          deps (visited, acc)
+      with NoDef _ -> (visited, acc)
+  in
+  let _, result = aux Names.GlobRef.Set.empty Data.empty gref in
+  result
+
+let display_dependance_recursive ~opaque_access gref =
+  let data = collect_dependance_recursive ~opaque_access gref in
+  display_data data
+
 }
 
 VERNAC COMMAND EXTEND Searchdepend CLASSIFIED AS QUERY STATE opaque_access
 | ["SearchDepend" global(ref) ] ->
   {fun ~opaque_access ->
    display_dependance ~opaque_access (Nametab.global ref) }
 END
+
+VERNAC COMMAND EXTEND SearchdependRecursive CLASSIFIED AS QUERY STATE opaque_access
+| ["SearchDependRecursive" global(ref) ] ->
+  {fun ~opaque_access ->
+   display_dependance_recursive ~opaque_access (Nametab.global ref) }
+END

tests/search_comparison.cmd

@@ -0,0 +1,16 @@
+Require Import dpdgraph.dpdgraph.
+
+Require Import Test.
+
+(* Test to demonstrate the difference between SearchDepend and SearchDependRecursive *)
+
+(* Direct dependencies only *)
+SearchDepend Test.app_ass.
+
+(* All transitive dependencies *)
+SearchDependRecursive Test.app_ass.
+
+(* Another example *)
+SearchDepend Test.in_cons.
+
+SearchDependRecursive Test.in_cons.

tests/search_comparison.oracle

@@ -0,0 +1,8 @@
+Welcome to Rocq
+[Loading ML file coq-dpdgraph.plugin ... done]
+[Loading ML file rocq-runtime.plugins.ring ... done]
+Fetching opaque proofs from disk for dpdgraph.tests.Test
+[cons(5) nil(2) eq_refl(2) list(18) eq(6) app(29) eq_ind(1) list_ind(1) ]
+[cons(8) nil(4) eq_refl(2) list(36) eq(9) app(29) eq_ind(1) list_ind(1) ]
+[cons(2) or_intror(1) list(3) eq(1) In(6) ]
+[cons(2) or_intror(1) list(7) False(1) or(1) eq(2) In(6) ]

tests/search_recursive.cmd

@@ -0,0 +1,5 @@
+Require Import dpdgraph.dpdgraph.
+
+Require Import Test.
+
+SearchDependRecursive Test.Permutation_app_swap.

tests/search_recursive.oracle

@@ -0,0 +1,8 @@
+Welcome to Rocq
+[Loading ML file coq-dpdgraph.plugin ... done]
+[Loading ML file rocq-runtime.plugins.ring ... done]
+Fetching opaque proofs from disk for dpdgraph.tests.Test
+[cons(95) nil(31) eq_refl(4) perm_trans(2) perm_swap(2) perm_skip(5)
+perm_nil(2) list(127) eq(17) Permutation(37) app(52) Permutation_trans(3)
+eq_ind_r(1) eq_sym(1) eq_ind(4) list_ind(4) Permutation_refl(2)
+app_comm_cons(1) app_nil_end(2) Permutation_sym(3) Permutation_ind(1) ]