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
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
module DefMap = CString.Map
module Error = struct
type t =
| Ill_formed of string
| Outdated
let to_string = function
| Ill_formed s -> "Ill-formed file: " ^ s
| Outdated -> "Outdated .glob file"
end
module Info = struct
type t =
{ kind : string
; offset : int * int
}
end
module Coq = struct
module Entry_type = struct
type t =
| Library
| Module
| Definition
| Inductive
| Constructor
| Lemma
| Record
| Projection
| Instance
| Class
| Method
| Variable
| Axiom
| TacticDefinition
| Abbreviation
| Notation
| Section
| Binder
let of_string = function
| "def"
| "coe"
| "subclass"
| "canonstruc"
| "fix"
| "cofix"
| "ex"
| "scheme" -> Definition
| "prf" | "thm" -> Lemma
| "ind" | "variant" | "coind" -> Inductive
| "constr" -> Constructor
| "indrec" | "rec" | "corec" -> Record
| "proj" -> Projection
| "class" -> Class
| "meth" -> Method
| "inst" -> Instance
| "var" -> Variable
| "defax" | "prfax" | "ax" -> Axiom
| "abbrev" | "syndef" -> Abbreviation
| "not" -> Notation
| "lib" -> Library
| "mod" | "modtype" -> Module
| "tac" -> TacticDefinition
| "sec" -> Section
| "binder" -> Binder
| s -> invalid_arg ("type_of_string:" ^ s)
end
let read_dp ic =
let line = input_line ic in
let n = String.length line in
match line.[0] with
| 'F' ->
let lib_name = String.sub line 1 (n - 1) in
Ok lib_name
| _ -> Error (Error.Ill_formed "lib name not found in header")
let correct_file vfile ic =
let s = input_line ic in
if String.length s < 7 || String.sub s 0 7 <> "DIGEST " then
Error (Error.Ill_formed "DIGEST ill-formed")
else
let s = String.sub s 7 (String.length s - 7) in
match (vfile, s) with
| None, "NO" -> read_dp ic
| Some _, "NO" -> Error (Ill_formed "coming from .v file but no digest")
| None, _ -> Error (Ill_formed "digest but .v source file not available")
| Some vfile, s ->
if s = Digest.to_hex (Digest.file vfile) then
read_dp ic
else Error Outdated
let parse_ref line =
try
if false then
let add_ref _ _ _ _ _ = () in
Scanf.sscanf line "R%d:%d %s %s %s %s" (fun loc1 loc2 lib_dp sp id ty ->
for loc = loc1 to loc2 do
add_ref loc lib_dp sp id (Entry_type.of_string ty);
ignore
(List.fold_right
(fun thisPiece priorPieces ->
let newPieces =
match priorPieces with
| "" -> thisPiece
| _ -> thisPiece ^ "." ^ priorPieces
in
add_ref loc "" "" newPieces Entry_type.Library;
newPieces)
(Str.split (Str.regexp_string ".") lib_dp)
"")
done)
with _ -> ()
let parse_def line : _ Result.t =
try
Scanf.sscanf line "%s %d:%d %s %s"
(fun kind loc1 loc2 section_path name ->
Ok (name, section_path, kind, (loc1, loc2)))
with Scanf.Scan_failure err -> Error err
let process_line dp map line =
match line.[0] with
| 'R' ->
let _reference = parse_ref line in
map
| _ -> (
match parse_def line with
| Error _ -> map
| Ok (name, section_path, kind, offset) ->
let section_path =
if String.equal "<>" section_path then "" else section_path ^ "."
in
let name = dp ^ "." ^ section_path ^ name in
let info = { Info.kind; offset } in
DefMap.add name info map)
let read_glob vfile inc =
match correct_file vfile inc with
| Error e -> Error (Error.to_string e)
| Ok dp -> (
let map = ref DefMap.empty in
try
while true do
let line = input_line inc in
let n = String.length line in
if n > 0 then map := process_line dp !map line
done;
assert false
with End_of_file -> Ok !map)
end
type t = Info.t DefMap.t
let open_file file =
if Sys.file_exists file then
let vfile = Filename.remove_extension file ^ ".v" in
Compat.Ocaml_414.In_channel.with_open_text file (Coq.read_glob (Some vfile))
else Error (Format.asprintf "Cannot open file: %s" file)
let get_info map name = DefMap.find_opt name map