1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
(* This file is part of the DpdGraph tools. *)
(* Copyright (C) 2009-2015 Anne Pacalet (Anne.Pacalet@free.fr) *)
(* and Yves Bertot (Yves.Bertot@inria.fr) *)
(* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
(* This file is distributed under the terms of the *)
(* GNU Lesser General Public License Version 2.1 *)
(* (see the enclosed LICENSE file for mode details) *)
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
DECLARE PLUGIN "coq-dpdgraph.plugin"
{
open Pp
open Stdarg
module Data = struct
type t = int Names.GlobRef.Map.t
let empty = Names.GlobRef.Map.empty
let add gref d =
let n = try Names.GlobRef.Map.find gref d with Not_found -> 0 in
Names.GlobRef.Map.add gref (n+1) d
(* [f gref n acc] *)
let fold f d acc = Names.GlobRef.Map.fold f d acc
end
let add_identifier (x:Names.Id.t)(d:Data.t) =
failwith
("SearchDep does not expect to find plain identifiers :" ^
Names.Id.to_string x)
let add_sort (s:Sorts.t)(d:Data.t) = d
let add_constant (cst:Names.Constant.t)(d:Data.t) =
Data.add (Names.GlobRef.ConstRef cst) d
let add_inductive ((k,i):Names.inductive)(d:Data.t) =
Data.add (Names.GlobRef.IndRef (k, i)) d
let add_constructor(((k,i),j):Names.constructor)(d:Data.t) =
Data.add (Names.GlobRef.ConstructRef ((k,i),j)) d
let collect_long_names avoid (c:Constr.t) (acc:Data.t) =
let rec add acc c =
let open Constr in
match kind c with
| Var x -> add_identifier x acc
| Sort s -> add_sort s acc
| Const cst -> add_constant (UVars.out_punivs cst) acc
| Ind (i,_) when not (List.exists (Names.MutInd.CanOrd.equal (fst i)) avoid) -> add_inductive i acc
| Construct (cnst,_) when not (List.exists (Names.MutInd.CanOrd.equal (fst (fst cnst))) avoid) -> add_constructor cnst acc
| Case({ci_ind=i},_,_,_,_,_,_) ->
add_inductive i (Constr.fold add acc c)
| _ -> Constr.fold add acc c
in add acc c
exception NoDef of Names.GlobRef.t
let collect_dependance gref =
(* This will change to Names.GlobRef in 8.10 *)
let open Names in
let open GlobRef in
match gref with
| VarRef _ -> assert false
| ConstRef cst ->
let cb = Environ.lookup_constant cst (Global.env()) in
let cl = match Global.body_of_constant_body Library.indirect_accessor cb with
Some (e,_,_) -> [e]
| None -> [] in
let cl = cb.Declarations.const_type :: cl in
List.fold_right (collect_long_names []) cl Data.empty
| IndRef i | ConstructRef (i,_) ->
let _, indbody = Global.lookup_inductive i in
let ca = indbody.Declarations.mind_user_lc in
Array.fold_right (collect_long_names [fst i]) ca Data.empty
let display_dependance 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 gref in display data
with NoDef gref ->
CErrors.user_err (Printer.pr_global gref ++ str " has no value")
}
VERNAC COMMAND EXTEND Searchdepend CLASSIFIED AS QUERY
| ["SearchDepend" global(ref) ] -> { display_dependance (Nametab.global ref) }
END
|
