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: classops.ml 11897 2009-02-09 19:28:02Z barras $ *)
26
(* usage qque peu general: utilise aussi dans record *)
28
(* A class is a type constructor, its type is an arity whose number of
29
arguments is cl_param (0 for CL_SORT and CL_FUN) *)
34
| CL_SECVAR of variable
35
| CL_CONST of constant
42
type coe_typ = global_reference
47
coe_strength : locality;
48
coe_is_identity : bool;
53
type coe_index = coe_info_typ
55
type inheritance_path = coe_index list
57
(* table des classes, des coercions et graphe d'heritage *)
59
module Bijint = struct
60
type ('a,'b) t = { v : ('a * 'b) array; s : int; inv : ('a,int) Gmap.t }
61
let empty = { v = [||]; s = 0; inv = Gmap.empty }
62
let mem y b = Gmap.mem y b.inv
63
let map x b = if 0 <= x & x < b.s then b.v.(x) else raise Not_found
64
let revmap y b = let n = Gmap.find y b.inv in (n, snd (b.v.(n)))
67
if b.s = Array.length b.v then
68
(let v = Array.make (b.s + 8) (x,y) in Array.blit b.v 0 v 0 b.s; v)
70
v.(b.s) <- (x,y); { v = v; s = b.s+1; inv = Gmap.add x b.s b.inv }
72
let v = Array.copy b.v in v.(n) <- (x,y); { b with v = v }
73
let dom b = Gmap.dom b.inv
77
ref (Bijint.empty : (cl_typ, cl_info_typ) Bijint.t)
80
ref (Gmap.empty : (coe_typ, coe_info_typ) Gmap.t)
82
let inheritance_graph =
83
ref (Gmap.empty : (cl_index * cl_index, inheritance_path) Gmap.t)
85
let freeze () = (!class_tab, !coercion_tab, !inheritance_graph)
87
let unfreeze (fcl,fco,fig) =
90
inheritance_graph:=fig
92
(* ajout de nouveaux "objets" *)
94
let add_new_class cl s =
95
if not (Bijint.mem cl !class_tab) then
96
class_tab := Bijint.add cl s !class_tab
98
let add_new_coercion coe s =
99
coercion_tab := Gmap.add coe s !coercion_tab
101
let add_new_path x y =
102
inheritance_graph := Gmap.add x y !inheritance_graph
105
class_tab:= Bijint.empty;
106
add_new_class CL_FUN { cl_param = 0 };
107
add_new_class CL_SORT { cl_param = 0 };
108
coercion_tab:= Gmap.empty;
109
inheritance_graph:= Gmap.empty
112
Summary.declare_summary "inh_graph"
113
{ Summary.freeze_function = freeze;
114
Summary.unfreeze_function = unfreeze;
115
Summary.init_function = init;
116
Summary.survive_module = false;
117
Summary.survive_section = false }
121
(* class_info : cl_typ -> int * cl_info_typ *)
123
let class_info cl = Bijint.revmap cl !class_tab
125
let class_exists cl = Bijint.mem cl !class_tab
127
(* class_info_from_index : int -> cl_typ * cl_info_typ *)
129
let class_info_from_index i = Bijint.map i !class_tab
131
let cl_fun_index = fst(class_info CL_FUN)
133
let cl_sort_index = fst(class_info CL_SORT)
135
(* coercion_info : coe_typ -> coe_info_typ *)
137
let coercion_info coe = Gmap.find coe !coercion_tab
139
let coercion_exists coe = Gmap.mem coe !coercion_tab
141
let coercion_params coe_info = coe_info.coe_param
143
(* find_class_type : env -> evar_map -> constr -> cl_typ * int *)
145
let find_class_type env sigma t =
146
let t', args = Reductionops.whd_betaiotazeta_stack sigma t in
147
match kind_of_term t' with
148
| Var id -> CL_SECVAR id, args
149
| Const sp -> CL_CONST sp, args
150
| Ind ind_sp -> CL_IND ind_sp, args
151
| Prod (_,_,_) -> CL_FUN, []
152
| Sort _ -> CL_SORT, []
153
| _ -> raise Not_found
156
let subst_cl_typ subst ct = match ct with
161
let kn',t = subst_con subst kn in
162
if kn' == kn then ct else
163
fst (find_class_type (Global.env()) Evd.empty t)
165
let kn' = subst_kn subst kn in
166
if kn' == kn then ct else
169
(*CSC: here we should change the datatype for coercions: it should be possible
170
to declare any term as a coercion *)
171
let subst_coe_typ subst t = fst (subst_global subst t)
173
(* class_of : Term.constr -> int *)
175
let class_of env sigma t =
176
let (t, n1, i, args) =
178
let (cl,args) = find_class_type env sigma t in
179
let (i, { cl_param = n1 } ) = class_info cl in
182
let t = Tacred.hnf_constr env sigma t in
183
let (cl, args) = find_class_type env sigma t in
184
let (i, { cl_param = n1 } ) = class_info cl in
187
if List.length args = n1 then t, i else raise Not_found
189
let inductive_class_of ind = fst (class_info (CL_IND ind))
191
let class_args_of env sigma c = snd (find_class_type env sigma c)
193
let string_of_class = function
194
| CL_FUN -> "Funclass"
195
| CL_SORT -> "Sortclass"
197
string_of_qualid (shortest_qualid_of_global Idset.empty (ConstRef sp))
199
string_of_qualid (shortest_qualid_of_global Idset.empty (IndRef sp))
201
string_of_qualid (shortest_qualid_of_global Idset.empty (VarRef sp))
203
let pr_class x = str (string_of_class x)
207
let lookup_path_between_class (s,t) =
208
Gmap.find (s,t) !inheritance_graph
210
let lookup_path_to_fun_from_class s =
211
lookup_path_between_class (s,cl_fun_index)
213
let lookup_path_to_sort_from_class s =
214
lookup_path_between_class (s,cl_sort_index)
216
(* advanced path lookup *)
218
let apply_on_class_of env sigma t cont =
220
let (cl,args) = find_class_type env sigma t in
221
let (i, { cl_param = n1 } ) = class_info cl in
222
if List.length args <> n1 then raise Not_found;
225
(* Is it worth to be more incremental on the delta steps? *)
226
let t = Tacred.hnf_constr env sigma t in
227
let (cl, args) = find_class_type env sigma t in
228
let (i, { cl_param = n1 } ) = class_info cl in
229
if List.length args <> n1 then raise Not_found;
232
let lookup_path_between env sigma (s,t) =
234
apply_on_class_of env sigma s (fun i ->
235
apply_on_class_of env sigma t (fun j ->
236
lookup_path_between_class (i,j))) in
239
let lookup_path_to_fun_from env sigma s =
240
apply_on_class_of env sigma s lookup_path_to_fun_from_class
242
let lookup_path_to_sort_from env sigma s =
243
apply_on_class_of env sigma s lookup_path_to_sort_from_class
245
let get_coercion_constructor coe =
247
Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty coe.coe_value
249
match kind_of_term c with
251
(cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1)
255
let lookup_pattern_path_between (s,t) =
256
let i = inductive_class_of s in
257
let j = inductive_class_of t in
258
List.map get_coercion_constructor (Gmap.find (i,j) !inheritance_graph)
260
(* coercion_value : coe_index -> unsafe_judgment * bool *)
262
let coercion_value { coe_value = c; coe_type = t; coe_is_identity = b } =
265
(* pretty-print functions are now in Pretty *)
266
(* rajouter une coercion dans le graphe *)
268
let path_printer = ref (fun _ -> str "<a class path>"
269
: (int * int) * inheritance_path -> std_ppcmds)
271
let install_path_printer f = path_printer := f
273
let print_path x = !path_printer x
275
let message_ambig l =
276
(str"Ambiguous paths:" ++ spc () ++
277
prlist_with_sep pr_fnl (fun ijp -> print_path ijp) l)
279
(* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
280
coercion,source,target *)
282
let different_class_params i j =
283
(snd (class_info_from_index i)).cl_param > 0
285
let add_coercion_in_graph (ic,source,target) =
286
let old_inheritance_graph = !inheritance_graph in
288
(ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
289
let try_add_new_path (i,j as ij) p =
292
if different_class_params i j then begin
293
let _ = lookup_path_between_class ij in
294
ambig_paths := (ij,p)::!ambig_paths
297
let _ = lookup_path_between_class (i,j) in
298
ambig_paths := (ij,p)::!ambig_paths
301
with Not_found -> begin
306
let try_add_new_path1 ij p =
307
let _ = try_add_new_path ij p in ()
309
if try_add_new_path (source,target) [ic] then begin
313
if t = source then begin
314
try_add_new_path1 (s,target) (p@[ic]);
317
if u<>v & (u = target) & (p <> q) then
318
try_add_new_path1 (s,v) (p@[ic]@q))
319
old_inheritance_graph
321
if s = target then try_add_new_path1 (source,t) (ic::p)
323
old_inheritance_graph
325
if (!ambig_paths <> []) && is_verbose () then
326
ppnl (message_ambig !ambig_paths)
328
type coercion = coe_typ * locality * bool * cl_typ * cl_typ * int
330
(* Calcul de l'arit� d'une classe *)
332
let reference_arity_length ref =
333
let t = Global.type_of_global ref in
334
List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty t))
336
let class_params = function
337
| CL_FUN | CL_SORT -> 0
338
| CL_CONST sp -> reference_arity_length (ConstRef sp)
339
| CL_SECVAR sp -> reference_arity_length (VarRef sp)
340
| CL_IND sp -> reference_arity_length (IndRef sp)
342
(* add_class : cl_typ -> locality_flag option -> bool -> unit *)
345
add_new_class cl { cl_param = class_params cl }
347
let load_coercion i (_,(coe,stre,isid,cls,clt,ps)) =
350
let is,_ = class_info cls in
351
let it,_ = class_info clt in
353
{ coe_value = constr_of_global coe;
354
coe_type = Global.type_of_global coe;
356
coe_is_identity = isid;
358
add_new_coercion coe xf;
359
add_coercion_in_graph (xf,is,it)
361
let cache_coercion o =
364
let subst_coercion (_,subst,(coe,stre,isid,cls,clt,ps as obj)) =
365
let coe' = subst_coe_typ subst coe in
366
let cls' = subst_cl_typ subst cls in
367
let clt' = subst_cl_typ subst clt in
368
if coe' == coe && cls' == cls & clt' == clt then obj else
369
(coe',stre,isid,cls',clt',ps)
371
let discharge_cl = function
372
| CL_CONST kn -> CL_CONST (Lib.discharge_con kn)
373
| CL_IND ind -> CL_IND (Lib.discharge_inductive ind)
376
let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) =
377
if stre = Local then None else
378
let n = try Array.length (Lib.section_instance coe) with Not_found -> 0 in
379
Some (Lib.discharge_global coe,
386
let (inCoercion,outCoercion) =
387
declare_object {(default_object "COERCION") with
388
load_function = load_coercion;
389
cache_function = cache_coercion;
390
subst_function = subst_coercion;
391
classify_function = (fun (_,x) -> Substitute x);
392
discharge_function = discharge_coercion;
393
export_function = (function x -> Some x) }
395
let declare_coercion coef stre ~isid ~src:cls ~target:clt ~params:ps =
396
Lib.add_anonymous_leaf (inCoercion (coef,stre,isid,cls,clt,ps))
398
let coercion_strength v = v.coe_strength
399
let coercion_identity v = v.coe_is_identity
401
(* For printing purpose *)
402
let get_coercion_value v = v.coe_value
404
let pr_cl_index n = int n
406
let classes () = Bijint.dom !class_tab
407
let coercions () = Gmap.rng !coercion_tab
408
let inheritance_graph () = Gmap.to_list !inheritance_graph
410
let coercion_of_reference r =
411
let ref = Nametab.global r in
412
if not (coercion_exists ref) then
413
errorlabstrm "try_add_coercion"
414
(Nametab.pr_global_env Idset.empty ref ++ str" is not a coercion.");
417
module CoercionPrinting =
420
let encode = coercion_of_reference
421
let subst = subst_coe_typ
422
let printer x = pr_global_env Idset.empty x
423
let key = Goptions.SecondaryTable ("Printing","Coercion")
424
let title = "Explicitly printed coercions: "
425
let member_message x b =
426
str "Explicit printing of coercion " ++ printer x ++
427
str (if b then " is set" else " is unset")
428
let synchronous = true
431
module PrintingCoercion = Goptions.MakeRefTable(CoercionPrinting)
433
let hide_coercion coe =
434
if not (PrintingCoercion.active coe) then
435
let coe_info = coercion_info coe in
436
Some coe_info.coe_param
added
removed
pretyping/classops.ml
