forked from coq-community/coq-dpdgraph
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsearchdepend.ml4
101 lines (86 loc) · 3.68 KB
/
searchdepend.ml4
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
96
97
98
99
100
101
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
(* This file is part of the DpdGraph tools. *)
(* Copyright (C) 2009-2015 Anne Pacalet ([email protected]) *)
(* and Yves Bertot ([email protected]) *)
(* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
(* 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) *)
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
open Pp
open Stdarg
module Data = struct
type t = int Globnames.Refmap.t
let empty = Globnames.Refmap.empty
let add gref d =
let n = try Globnames.Refmap.find gref d with Not_found -> 0 in
Globnames.Refmap.add gref (n+1) d
(* [f gref n acc] *)
let fold f d acc = Globnames.Refmap.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 (Globnames.ConstRef cst) d
let add_inductive ((k,i):Names.inductive)(d:Data.t) =
Data.add (Globnames.IndRef (k, i)) d
let add_constructor(((k,i),j):Names.constructor)(d:Data.t) =
Data.add (Globnames.ConstructRef ((k,i),j)) d
let collect_long_names (c:Constr.t) (acc:Data.t) =
let rec add c acc =
let open Constr in
match kind c with
Rel _ -> acc
| Var x -> add_identifier x acc
| Meta _ -> assert false
| Evar _ -> assert false
| Sort s -> add_sort s acc
| Cast(c,_,t) -> add c (add t acc)
| Prod(n,t,c) -> add t (add c acc)
| Lambda(n,t,c) -> add t (add c acc)
| LetIn(_,v,t,c) -> add v (add t (add c acc))
| App(c,ca) -> add c (Array.fold_right add ca acc)
| Const cst -> add_constant (Univ.out_punivs cst) acc
| Ind i -> add_inductive (Univ.out_punivs i) acc
| Construct cnst -> add_constructor (Univ.out_punivs cnst) acc
| Case({ci_ind=i},c,t,ca) ->
add_inductive i (add c (add t (Array.fold_right add ca acc)))
| Fix(_,(_,ca,ca')) ->
Array.fold_right add ca (Array.fold_right add ca' acc)
| CoFix(_,(_,ca,ca')) ->
Array.fold_right add ca (Array.fold_right add ca' acc)
| Proj(p, c) ->
add c acc
in add c acc
exception NoDef of Names.global_reference
let collect_dependance gref =
(* This will change to Names.GlobRef in 8.10 *)
let open Globnames 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 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 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