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: class.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
30
let strength_min l = if List.mem Local l then Local else Global
32
let id_of_varid c = match kind_of_term c with
34
| _ -> anomaly "class__id_of_varid"
38
type coercion_error_kind =
41
| NoSource of cl_typ option
42
| ForbiddenSourceClass of cl_typ
45
| WrongTarget of cl_typ * cl_typ
46
| NotAClass of global_reference
47
| NotEnoughClassArgs of cl_typ
49
exception CoercionError of coercion_error_kind
51
let explain_coercion_error g = function
53
(Printer.pr_global g ++ str" is already a coercion")
55
(Printer.pr_global g ++ str" is not a function")
56
| NoSource (Some cl) ->
57
(str "Cannot recognize " ++ pr_class cl ++ str " as a source class of "
58
++ Printer.pr_global g)
60
(str ": cannot find the source class of " ++ Printer.pr_global g)
61
| ForbiddenSourceClass cl ->
62
pr_class cl ++ str " cannot be a source class"
64
(Printer.pr_global g ++
65
str" does not respect the inheritance uniform condition");
67
(str"Cannot find the target class")
68
| WrongTarget (clt,cl) ->
69
(str"Found target class " ++ pr_class cl ++
70
str " instead of " ++ pr_class clt)
72
(str "Type of " ++ Printer.pr_global ref ++
73
str " does not end with a sort")
74
| NotEnoughClassArgs cl ->
75
(str"Wrong number of parameters for " ++ pr_class cl)
77
(* Verifications pour l'ajout d'une classe *)
79
let check_reference_arity ref =
80
if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global ref)) then
81
raise (CoercionError (NotAClass ref))
83
let check_arity = function
84
| CL_FUN | CL_SORT -> ()
85
| CL_CONST cst -> check_reference_arity (ConstRef cst)
86
| CL_SECVAR id -> check_reference_arity (VarRef id)
87
| CL_IND kn -> check_reference_arity (IndRef kn)
91
(* check that the computed target is the provided one *)
92
let check_target clt = function
93
| Some cl when cl <> clt -> raise (CoercionError (WrongTarget(clt,cl)))
96
(* condition d'heritage uniforme *)
98
let uniform_cond nargs lt =
99
let rec aux = function
101
| (n,t::l) -> (strip_outer_cast t = mkRel n) & (aux ((n-1),l))
106
let id_of_cl = function
107
| CL_FUN -> id_of_string "FUNCLASS"
108
| CL_SORT -> id_of_string "SORTCLASS"
109
| CL_CONST kn -> id_of_label (con_label kn)
111
let (_,mip) = Global.lookup_inductive ind in
115
let class_of_global = function
116
| ConstRef sp -> CL_CONST sp
117
| IndRef sp -> CL_IND sp
118
| VarRef id -> CL_SECVAR id
119
| ConstructRef _ as c ->
120
errorlabstrm "class_of_global"
121
(str "Constructors, such as " ++ Printer.pr_global c ++
122
str ", cannot be used as a class.")
125
lp est la liste (inverse'e) des arguments de la coercion
126
ids est le nom de la classe source
127
sps_opt est le sp de la classe source dans le cas des structures
130
nbre d'arguments de la classe
131
le constr de la class
132
la liste des variables dont depend la classe source
133
l'indice de la classe source dans la liste lp
136
let get_source lp source =
141
| [] -> raise Not_found
142
| t1::_ -> find_class_type (Global.env()) Evd.empty t1
146
let rec aux = function
147
| [] -> raise Not_found
150
let cl1,lv1 = find_class_type (Global.env()) Evd.empty t1 in
151
if cl = cl1 then cl1,lv1,(List.length lt+1)
153
with Not_found -> aux lt
156
let get_target t ind =
160
fst (find_class_type (Global.env()) Evd.empty t)
163
let rec aux acc d = match kind_of_term d with
164
| Prod (_,c1,c2) -> aux (c1::acc) c2
165
| Cast (c,_,_) -> aux acc c
170
let strength_of_cl = function
171
| CL_CONST kn -> Global
172
| CL_SECVAR id -> Local
175
let get_strength stre ref cls clt =
176
let stres = strength_of_cl cls in
177
let stret = strength_of_cl clt in
178
let stref = strength_of_global ref in
179
strength_min [stre;stres;stret;stref]
181
let ident_key_of_class = function
182
| CL_FUN -> "Funclass"
183
| CL_SORT -> "Sortclass"
184
| CL_CONST sp -> string_of_label (con_label sp)
185
| CL_IND (sp,_) -> string_of_label (label sp)
186
| CL_SECVAR id -> string_of_id id
188
(* coercion identit� *)
190
let error_not_transparent source =
191
errorlabstrm "build_id_coercion"
192
(pr_class source ++ str " must be a transparent constant.")
194
let build_id_coercion idf_opt source =
195
let env = Global.env () in
196
let vs = match source with
197
| CL_CONST sp -> mkConst sp
198
| _ -> error_not_transparent source in
199
let c = match constant_opt_value env (destConst vs) with
201
| None -> error_not_transparent source in
202
let lams,t = Sign.decompose_lam_assum c in
205
(mkLambda (Name (id_of_string "x"),
206
applistc vs (extended_rel_list 0 lams),
212
(mkProd (Anonymous, applistc vs (extended_rel_list 0 lams), lift 1 t))
215
(* juste pour verification *)
218
(Reductionops.is_conv_leq env Evd.empty
219
(Typing.type_of env Evd.empty val_f) typ_f)
221
errorlabstrm "" (strbrk
222
"Cannot be defined as coercion (maybe a bad number of arguments).")
228
let cl,_ = find_class_type (Global.env()) Evd.empty t in
229
id_of_string ("Id_"^(ident_key_of_class source)^"_"^
230
(ident_key_of_class cl))
232
let constr_entry = (* Cast is necessary to express [val_f] is identity *)
234
{ const_entry_body = mkCast (val_f, DEFAULTcast, typ_f);
235
const_entry_type = Some typ_f;
236
const_entry_opaque = false;
237
const_entry_boxed = Flags.boxed_definitions()} in
238
let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in
241
let check_source = function
242
| Some (CL_FUN|CL_SORT as s) -> raise (CoercionError (ForbiddenSourceClass s))
246
nom de la fonction coercion
248
nom de la classe source (optionnel)
249
sp de la classe source (dans le cas des structures)
250
nom de la classe target (optionnel)
251
booleen "coercion identite'?"
253
lorque source est None alors target est None aussi.
256
let add_new_coercion_core coef stre source target isid =
258
let t = Global.type_of_global coef in
259
if coercion_exists coef then raise (CoercionError AlreadyExists);
260
let tg,lp = prods_of t in
261
let llp = List.length lp in
262
if llp = 0 then raise (CoercionError NotAFunction);
267
raise (CoercionError (NoSource source))
269
check_source (Some cls);
270
if not (uniform_cond (llp-ind) lvs) then
271
raise (CoercionError NotUniform);
276
raise (CoercionError NoTarget)
278
check_target clt target;
281
let stre' = get_strength stre coef cls clt in
282
declare_coercion coef stre' isid cls clt (List.length lvs)
284
let try_add_new_coercion_core ref b c d e =
285
try add_new_coercion_core ref b c d e
286
with CoercionError e ->
287
errorlabstrm "try_add_new_coercion_core"
288
(explain_coercion_error ref e ++ str ".")
290
let try_add_new_coercion ref stre =
291
try_add_new_coercion_core ref stre None None false
293
let try_add_new_coercion_subclass cl stre =
294
let coe_ref = build_id_coercion None cl in
295
try_add_new_coercion_core coe_ref stre (Some cl) None true
297
let try_add_new_coercion_with_target ref stre ~source ~target =
298
try_add_new_coercion_core ref stre (Some source) (Some target) false
300
let try_add_new_identity_coercion id stre ~source ~target =
301
let ref = build_id_coercion (Some id) source in
302
try_add_new_coercion_core ref stre (Some source) (Some target) true
304
let try_add_new_coercion_with_source ref stre ~source =
305
try_add_new_coercion_core ref stre (Some source) None false
307
let add_coercion_hook stre ref =
308
try_add_new_coercion ref stre;
309
Flags.if_verbose message
310
(string_of_qualid (shortest_qualid_of_global Idset.empty ref)
311
^ " is now a coercion")
313
let add_subclass_hook stre ref =
314
let cl = class_of_global ref in
315
try_add_new_coercion_subclass cl stre
added
removed
toplevel/class.ml
