diff --git a/Make_coq.local b/Make_coq.local index 3fb8f8296..e883799a3 100644 --- a/Make_coq.local +++ b/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 diff --git a/searchdepend.mlg b/searchdepend.mlg index 8497ac433..c2ae07ada 100644 --- a/searchdepend.mlg +++ b/searchdepend.mlg @@ -77,16 +77,42 @@ 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 @@ -94,3 +120,9 @@ VERNAC COMMAND EXTEND Searchdepend CLASSIFIED AS QUERY STATE opaque_access {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 diff --git a/tests/search_comparison.cmd b/tests/search_comparison.cmd new file mode 100644 index 000000000..cec4bdc6b --- /dev/null +++ b/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. diff --git a/tests/search_comparison.oracle b/tests/search_comparison.oracle new file mode 100644 index 000000000..aa71a618e --- /dev/null +++ b/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) ] diff --git a/tests/search_recursive.cmd b/tests/search_recursive.cmd new file mode 100644 index 000000000..415a3e6ed --- /dev/null +++ b/tests/search_recursive.cmd @@ -0,0 +1,5 @@ +Require Import dpdgraph.dpdgraph. + +Require Import Test. + +SearchDependRecursive Test.Permutation_app_swap. diff --git a/tests/search_recursive.oracle b/tests/search_recursive.oracle new file mode 100644 index 000000000..491d1ad19 --- /dev/null +++ b/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) ]