1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: coqlib.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
19
(************************************************************************)
20
(* Generic functions to find Coq objects *)
24
let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
26
let find_reference locstr dir s =
27
let sp = Libnames.make_path (make_dir dir) (id_of_string s) in
29
Nametab.absolute_reference sp
31
anomaly (locstr^": cannot find "^(string_of_path sp))
33
let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
34
let coq_constant locstr dir s = constr_of_global (coq_reference locstr dir s)
36
let gen_reference = coq_reference
37
let gen_constant = coq_constant
39
let has_suffix_in_dirs dirs ref =
40
let dir = dirpath (sp_of_global ref) in
41
List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
43
let gen_constant_in_modules locstr dirs s =
44
let dirs = List.map make_dir dirs in
45
let id = id_of_string s in
46
let all = Nametab.locate_all (make_short_qualid id) in
47
let these = List.filter (has_suffix_in_dirs dirs) all in
49
| [x] -> constr_of_global x
51
anomalylabstrm "" (str (locstr^": cannot find "^s^
52
" in module"^(if List.length dirs > 1 then "s " else " ")) ++
53
prlist_with_sep pr_coma pr_dirpath dirs)
56
(str (locstr^": found more than once object of name "^s^
57
" in module"^(if List.length dirs > 1 then "s " else " ")) ++
58
prlist_with_sep pr_coma pr_dirpath dirs)
61
(* For tactics/commands requiring vernacular libraries *)
63
let check_required_library d =
64
let d' = List.map id_of_string d in
65
let dir = make_dirpath (List.rev d') in
66
if not (Library.library_is_loaded dir) then
67
(* Loading silently ...
68
let m, prefix = list_sep_last d' in
70
(dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
73
error ("Library "^(string_of_dirpath dir)^" has to be required first.")
75
(************************************************************************)
76
(* Specific Coq objects *)
78
let init_reference dir s = gen_reference "Coqlib" ("Init"::dir) s
80
let init_constant dir s = gen_constant "Coqlib" ("Init"::dir) s
82
let arith_dir = ["Coq";"Arith"]
83
let arith_modules = [arith_dir]
85
let narith_dir = ["Coq";"NArith"]
87
let zarith_dir = ["Coq";"ZArith"]
88
let zarith_base_modules = [narith_dir;zarith_dir]
90
let init_dir = ["Coq";"Init"]
92
init_dir@["Datatypes"];
95
init_dir@["Logic_Type"];
100
let coq_id = id_of_string "Coq"
101
let init_id = id_of_string "Init"
102
let arith_id = id_of_string "Arith"
103
let datatypes_id = id_of_string "Datatypes"
105
let logic_module_name = ["Coq";"Init";"Logic"]
106
let logic_module = make_dir logic_module_name
107
let logic_type_module = make_dir ["Coq";"Init";"Logic_Type"]
108
let datatypes_module = make_dir ["Coq";"Init";"Datatypes"]
109
let arith_module = make_dir ["Coq";"Arith";"Arith"]
111
(* TODO: temporary hack *)
112
let make_kn dir id = Libnames.encode_kn dir id
113
let make_con dir id = Libnames.encode_con dir id
117
let id = make_con datatypes_module (id_of_string "id")
118
let type_of_id = make_con datatypes_module (id_of_string "ID")
120
let _ = Cases.set_impossible_default_clause (mkConst id,mkConst type_of_id)
122
(** Natural numbers *)
123
let nat_kn = make_kn datatypes_module (id_of_string "nat")
124
let nat_path = Libnames.make_path datatypes_module (id_of_string "nat")
126
let glob_nat = IndRef (nat_kn,0)
128
let path_of_O = ((nat_kn,0),1)
129
let path_of_S = ((nat_kn,0),2)
130
let glob_O = ConstructRef path_of_O
131
let glob_S = ConstructRef path_of_S
134
let bool_kn = make_kn datatypes_module (id_of_string "bool")
136
let glob_bool = IndRef (bool_kn,0)
138
let path_of_true = ((bool_kn,0),1)
139
let path_of_false = ((bool_kn,0),2)
140
let glob_true = ConstructRef path_of_true
141
let glob_false = ConstructRef path_of_false
144
let eq_kn = make_kn logic_module (id_of_string "eq")
146
let glob_eq = IndRef (eq_kn,0)
148
type coq_sigma_data = {
155
type coq_bool_data = {
158
andb_true_intro : constr}
160
type 'a delayed = unit -> 'a
162
let build_bool_type () =
163
{ andb = init_constant ["Datatypes"] "andb";
164
andb_prop = init_constant ["Datatypes"] "andb_prop";
165
andb_true_intro = init_constant ["Datatypes"] "andb_true_intro" }
168
let build_sigma_set () = anomaly "Use build_sigma_type"
170
let build_sigma_type () =
171
{ proj1 = init_constant ["Specif"] "projT1";
172
proj2 = init_constant ["Specif"] "projT2";
173
elim = init_constant ["Specif"] "sigT_rec";
174
intro = init_constant ["Specif"] "existT";
175
typ = init_constant ["Specif"] "sigT" }
178
{ proj1 = init_constant ["Datatypes"] "fst";
179
proj2 = init_constant ["Datatypes"] "snd";
180
elim = init_constant ["Datatypes"] "prod_rec";
181
intro = init_constant ["Datatypes"] "pair";
182
typ = init_constant ["Datatypes"] "prod" }
185
type coq_leibniz_eq_data = {
189
rrec : constr option;
190
rect : constr option;
194
let lazy_init_constant dir id = lazy (init_constant dir id)
196
(* Equality on Set *)
197
let coq_eq_eq = lazy_init_constant ["Logic"] "eq"
198
let coq_eq_refl = lazy_init_constant ["Logic"] "refl_equal"
199
let coq_eq_ind = lazy_init_constant ["Logic"] "eq_ind"
200
let coq_eq_rec = lazy_init_constant ["Logic"] "eq_rec"
201
let coq_eq_rect = lazy_init_constant ["Logic"] "eq_rect"
202
let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal"
203
let coq_eq_sym = lazy_init_constant ["Logic"] "sym_eq"
204
let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2"
206
let build_coq_eq_data () =
207
let _ = check_required_library logic_module_name in {
208
eq = Lazy.force coq_eq_eq;
209
refl = Lazy.force coq_eq_refl;
210
ind = Lazy.force coq_eq_ind;
211
rrec = Some (Lazy.force coq_eq_rec);
212
rect = Some (Lazy.force coq_eq_rect);
213
congr = Lazy.force coq_eq_congr;
214
sym = Lazy.force coq_eq_sym }
216
let build_coq_eq () = Lazy.force coq_eq_eq
217
let build_coq_sym_eq () = Lazy.force coq_eq_sym
218
let build_coq_f_equal2 () = Lazy.force coq_f_equal2
221
let coq_sumbool = lazy_init_constant ["Specif"] "sumbool"
223
let build_coq_sumbool () = Lazy.force coq_sumbool
225
(* Equality on Type as a Type *)
226
let coq_identity_eq = lazy_init_constant ["Datatypes"] "identity"
227
let coq_identity_refl = lazy_init_constant ["Datatypes"] "refl_identity"
228
let coq_identity_ind = lazy_init_constant ["Datatypes"] "identity_ind"
229
let coq_identity_rec = lazy_init_constant ["Datatypes"] "identity_rec"
230
let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect"
231
let coq_identity_congr = lazy_init_constant ["Logic_Type"] "congr_id"
232
let coq_identity_sym = lazy_init_constant ["Logic_Type"] "sym_id"
234
let build_coq_identity_data () = {
235
eq = Lazy.force coq_identity_eq;
236
refl = Lazy.force coq_identity_refl;
237
ind = Lazy.force coq_identity_ind;
238
rrec = Some (Lazy.force coq_identity_rec);
239
rect = Some (Lazy.force coq_identity_rect);
240
congr = Lazy.force coq_identity_congr;
241
sym = Lazy.force coq_identity_sym }
243
(* The False proposition *)
244
let coq_False = lazy_init_constant ["Logic"] "False"
246
(* The True proposition and its unique proof *)
247
let coq_True = lazy_init_constant ["Logic"] "True"
248
let coq_I = lazy_init_constant ["Logic"] "I"
251
let coq_not = lazy_init_constant ["Logic"] "not"
252
let coq_and = lazy_init_constant ["Logic"] "and"
253
let coq_conj = lazy_init_constant ["Logic"] "conj"
254
let coq_or = lazy_init_constant ["Logic"] "or"
255
let coq_ex = lazy_init_constant ["Logic"] "ex"
258
let build_coq_True () = Lazy.force coq_True
259
let build_coq_I () = Lazy.force coq_I
261
let build_coq_False () = Lazy.force coq_False
262
let build_coq_not () = Lazy.force coq_not
263
let build_coq_and () = Lazy.force coq_and
264
let build_coq_conj () = Lazy.force coq_conj
265
let build_coq_or () = Lazy.force coq_or
266
let build_coq_ex () = Lazy.force coq_ex
268
(* The following is less readable but does not depend on parsing *)
269
let coq_eq_ref = lazy (init_reference ["Logic"] "eq")
270
let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
271
let coq_existS_ref = lazy (anomaly "use coq_existT_ref")
272
let coq_existT_ref = lazy (init_reference ["Specif"] "existT")
273
let coq_not_ref = lazy (init_reference ["Logic"] "not")
274
let coq_False_ref = lazy (init_reference ["Logic"] "False")
275
let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")
276
let coq_sig_ref = lazy (init_reference ["Specif"] "sig")
277
let coq_or_ref = lazy (init_reference ["Logic"] "or")
added
removed
interp/coqlib.ml
