aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/classops.ml
blob: 30d100af9fdf95032d9aeb0f77143a78dc6efee4 (plain)
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
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open CErrors
open Util
open Pp
open Flags
open Names
open Libnames
open Globnames
open Nametab
open Environ
open Libobject
open Term
open Termops
open Mod_subst

(* usage qque peu general: utilise aussi dans record *)

(* A class is a type constructor, its type is an arity whose number of
   arguments is cl_param (0 for CL_SORT and CL_FUN) *)

type cl_typ =
  | CL_SORT
  | CL_FUN
  | CL_SECVAR of variable
  | CL_CONST of constant
  | CL_IND of inductive
  | CL_PROJ of constant

type cl_info_typ = {
  cl_param : int
}

type coe_typ = global_reference

module CoeTypMap = Refmap_env

type coe_info_typ = {
  coe_value : constr;
  coe_type : types;
  coe_local : bool;
  coe_context : Univ.universe_context_set;
  coe_is_identity : bool;
  coe_is_projection : bool;
  coe_param : int }

let coe_info_typ_equal c1 c2 =
  eq_constr c1.coe_value c2.coe_value &&
    eq_constr c1.coe_type c2.coe_type &&
    c1.coe_local == c2.coe_local &&
    c1.coe_is_identity == c2.coe_is_identity &&
    c1.coe_is_projection == c2.coe_is_projection &&
    Int.equal c1.coe_param c2.coe_param

let cl_typ_ord t1 t2 = match t1, t2 with
  | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
  | CL_CONST c1, CL_CONST c2 -> con_ord c1 c2
  | CL_PROJ c1, CL_PROJ c2 -> con_ord c1 c2
  | CL_IND i1, CL_IND i2 -> ind_ord i1 i2
  | _ -> Pervasives.compare t1 t2 (** OK *)

module ClTyp = struct
  type t = cl_typ
  let compare = cl_typ_ord
end

module ClTypMap = Map.Make(ClTyp)

module IntMap = Map.Make(Int)

let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0

type coe_index = coe_info_typ

type inheritance_path = coe_index list

(* table des classes, des coercions et graphe d'heritage *)

module Bijint :
sig
  module Index :
  sig
    type t
    val compare : t -> t -> int
    val equal : t -> t -> bool
    val print : t -> std_ppcmds
  end
  type 'a t
  val empty : 'a t
  val mem : cl_typ -> 'a t -> bool
  val map : Index.t -> 'a t -> cl_typ * 'a
  val revmap : cl_typ -> 'a t -> Index.t * 'a
  val add : cl_typ -> 'a -> 'a t -> 'a t
  val dom : 'a t -> cl_typ list
end
=
struct

  module Index = struct include Int let print = Pp.int end

  type 'a t = { v : (cl_typ * 'a) IntMap.t; s : int; inv : int ClTypMap.t }
  let empty = { v = IntMap.empty; s = 0; inv = ClTypMap.empty }
  let mem y b = ClTypMap.mem y b.inv
  let map x b = IntMap.find x b.v
  let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (IntMap.find n b.v))
  let add x y b =
    { v = IntMap.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv }
  let dom b = List.rev (ClTypMap.fold (fun x _ acc -> x::acc) b.inv [])
end

type cl_index = Bijint.Index.t

let class_tab =
  ref (Bijint.empty : cl_info_typ Bijint.t)

let coercion_tab =
  ref (CoeTypMap.empty : coe_info_typ CoeTypMap.t)

module ClPairOrd =
struct
  type t = cl_index * cl_index
  let compare (i1, j1) (i2, j2) =
    let c = Bijint.Index.compare i1 i2 in
    if Int.equal c 0 then Bijint.Index.compare j1 j2 else c
end

module ClPairMap = Map.Make(ClPairOrd)

let inheritance_graph =
  ref (ClPairMap.empty : inheritance_path ClPairMap.t)

let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph)

let unfreeze (fcl,fco,fig) =
  class_tab:=fcl;
  coercion_tab:=fco;
  inheritance_graph:=fig

(* ajout de nouveaux "objets" *)

let add_new_class cl s =
  if not (Bijint.mem cl !class_tab) then
    class_tab := Bijint.add cl s !class_tab

let add_new_coercion coe s =
  coercion_tab := CoeTypMap.add coe s !coercion_tab

let add_new_path x y =
  inheritance_graph := ClPairMap.add x y !inheritance_graph

let init () =
  class_tab:= Bijint.empty;
  add_new_class CL_FUN  { cl_param = 0 };
  add_new_class CL_SORT { cl_param = 0 };
  coercion_tab:= CoeTypMap.empty;
  inheritance_graph:= ClPairMap.empty

let _ =
  Summary.declare_summary "inh_graph"
    { Summary.freeze_function = freeze;
      Summary.unfreeze_function = unfreeze;
      Summary.init_function = init }

let _ = init()

(* class_info : cl_typ -> int * cl_info_typ *)

let class_info cl = Bijint.revmap cl !class_tab

let class_exists cl = Bijint.mem cl !class_tab

(* class_info_from_index : int -> cl_typ * cl_info_typ *)

let class_info_from_index i = Bijint.map i !class_tab

let cl_fun_index = fst(class_info CL_FUN)

let cl_sort_index = fst(class_info CL_SORT)

(* coercion_info : coe_typ -> coe_info_typ *)

let coercion_info coe = CoeTypMap.find coe !coercion_tab

let coercion_exists coe = CoeTypMap.mem coe !coercion_tab

(* find_class_type : evar_map -> constr -> cl_typ * universe_list * constr list *)

let find_class_type sigma t =
  let t', args = Reductionops.whd_betaiotazeta_stack sigma t in
  match kind_of_term t' with
    | Var id -> CL_SECVAR id, Univ.Instance.empty, args
    | Const (sp,u) -> CL_CONST sp, u, args
    | Proj (p, c) when not (Projection.unfolded p) ->
      CL_PROJ (Projection.constant p), Univ.Instance.empty, c :: args
    | Ind (ind_sp,u) -> CL_IND ind_sp, u, args
    | Prod (_,_,_) -> CL_FUN, Univ.Instance.empty, []
    | Sort _ -> CL_SORT, Univ.Instance.empty, []
    |  _ -> raise Not_found


let subst_cl_typ subst ct = match ct with
    CL_SORT
  | CL_FUN
  | CL_SECVAR _ -> ct
  | CL_PROJ c ->
    let c',t = subst_con_kn subst c in
      if c' == c then ct else CL_PROJ c'
  | CL_CONST c ->
      let c',t = subst_con_kn subst c in
	if c' == c then ct else
         pi1 (find_class_type Evd.empty t)
  | CL_IND i ->
      let i' = subst_ind subst i in
	if i' == i then ct else CL_IND i'

(*CSC: here we should change the datatype for coercions: it should be possible
       to declare any term as a coercion *)
let subst_coe_typ subst t = subst_global_reference subst t

(* class_of : Term.constr -> int *)

let class_of env sigma t =
  let (t, n1, i, u, args) =
    try
      let (cl, u, args) = find_class_type sigma t in
      let (i, { cl_param = n1 } ) = class_info cl in
      (t, n1, i, u, args)
    with Not_found ->
      let t = Tacred.hnf_constr env sigma t in
      let (cl, u, args) = find_class_type sigma t in
      let (i, { cl_param = n1 } ) = class_info cl in
      (t, n1, i, u, args)
  in
  if Int.equal (List.length args) n1 then t, i else raise Not_found

let inductive_class_of ind = fst (class_info (CL_IND ind))

let class_args_of env sigma c = pi3 (find_class_type sigma c)

let string_of_class = function
  | CL_FUN -> "Funclass"
  | CL_SORT -> "Sortclass"
  | CL_CONST sp | CL_PROJ sp ->
      string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp))
  | CL_IND sp ->
      string_of_qualid (shortest_qualid_of_global Id.Set.empty (IndRef sp))
  | CL_SECVAR sp ->
      string_of_qualid (shortest_qualid_of_global Id.Set.empty (VarRef sp))

let pr_class x = str (string_of_class x)

(* lookup paths *)

let lookup_path_between_class (s,t) =
  ClPairMap.find (s,t) !inheritance_graph

let lookup_path_to_fun_from_class s =
  lookup_path_between_class (s,cl_fun_index)

let lookup_path_to_sort_from_class s =
  lookup_path_between_class (s,cl_sort_index)

(* advanced path lookup *)

let apply_on_class_of env sigma t cont =
  try
    let (cl,u,args) = find_class_type sigma t in
    let (i, { cl_param = n1 } ) = class_info cl in
    if not (Int.equal (List.length args) n1) then raise Not_found;
    t, cont i
  with Not_found ->
    (* Is it worth to be more incremental on the delta steps? *)
    let t = Tacred.hnf_constr env sigma t in
    let (cl, u, args) = find_class_type sigma t in
    let (i, { cl_param = n1 } ) = class_info cl in
    if not (Int.equal (List.length args) n1) then raise Not_found;
    t, cont i

let lookup_path_between env sigma (s,t) =
  let (s,(t,p)) =
    apply_on_class_of env sigma s (fun i ->
      apply_on_class_of env sigma t (fun j ->
	lookup_path_between_class (i,j))) in
  (s,t,p)

let lookup_path_to_fun_from env sigma s =
  apply_on_class_of env sigma s lookup_path_to_fun_from_class

let lookup_path_to_sort_from env sigma s =
  apply_on_class_of env sigma s lookup_path_to_sort_from_class

let get_coercion_constructor env coe =
  let c, _ =
    Reductionops.whd_all_stack env Evd.empty coe.coe_value
  in
  match kind_of_term c with
  | Construct (cstr,u) ->
      (cstr, Inductiveops.constructor_nrealargs cstr -1)
  | _ ->
      raise Not_found

let lookup_pattern_path_between env (s,t) =
  let i = inductive_class_of s in
  let j = inductive_class_of t in
  List.map (get_coercion_constructor env) (ClPairMap.find (i,j) !inheritance_graph)

(* coercion_value : coe_index -> unsafe_judgment * bool *)

let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; 
		     coe_is_identity = b; coe_is_projection = b' } =
  let subst, ctx = Universes.fresh_universe_context_set_instance ctx in
  let c' = Vars.subst_univs_level_constr subst c 
  and t' = Vars.subst_univs_level_constr subst t in
    (make_judge c' t', b, b'), ctx

(* pretty-print functions are now in Pretty *)
(* rajouter une coercion dans le graphe *)

let path_printer = ref (fun _ -> str "<a class path>"
                        : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> std_ppcmds)

let install_path_printer f = path_printer := f

let print_path x = !path_printer x

let message_ambig l =
  (str"Ambiguous paths:" ++ spc () ++
   prlist_with_sep fnl (fun ijp -> print_path ijp) l)

(* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
                         coercion,source,target *)

let different_class_params i =
  let ci = class_info_from_index i in
    if (snd ci).cl_param > 0 then true
    else 
      match fst ci with
      | CL_IND i -> Global.is_polymorphic (IndRef i)
      | CL_CONST c -> Global.is_polymorphic (ConstRef c)
      | _ -> false
	
let add_coercion_in_graph (ic,source,target) =
  let old_inheritance_graph = !inheritance_graph in
  let ambig_paths =
    (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
  let try_add_new_path (i,j as ij) p =
    try
      if Bijint.Index.equal i j then begin
	if different_class_params i then begin
	  let _ = lookup_path_between_class ij in
          ambig_paths := (ij,p)::!ambig_paths
	end
      end else begin
        let _ = lookup_path_between_class ij in
        ambig_paths := (ij,p)::!ambig_paths
      end;
      false
    with Not_found -> begin
      add_new_path ij p;
      true
    end
  in
  let try_add_new_path1 ij p =
    let _ = try_add_new_path ij p in ()
  in
  if try_add_new_path (source,target) [ic] then begin
    ClPairMap.iter
      (fun (s,t) p ->
         if not (Bijint.Index.equal s t) then begin
	   if Bijint.Index.equal t source then begin
             try_add_new_path1 (s,target) (p@[ic]);
             ClPairMap.iter
	       (fun (u,v) q ->
                  if not (Bijint.Index.equal u v) && Bijint.Index.equal u target &&  not (List.equal coe_info_typ_equal p q) then
		    try_add_new_path1 (s,v) (p@[ic]@q))
               old_inheritance_graph
           end;
           if Bijint.Index.equal s target then try_add_new_path1 (source,t) (ic::p)
	 end)
      old_inheritance_graph
  end;
  let is_ambig = match !ambig_paths with [] -> false | _ -> true in
  if is_ambig && is_verbose () then
    Feedback.msg_info (message_ambig !ambig_paths)

type coercion = {
  coercion_type   : coe_typ;
  coercion_local  : bool;
  coercion_is_id  : bool;
  coercion_is_proj  : bool;
  coercion_source : cl_typ;
  coercion_target : cl_typ;
  coercion_params : int;
}

(* Computation of the class arity *)

let reference_arity_length ref =
  let t = Universes.unsafe_type_of_global ref in
  List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty t))

let projection_arity_length p =
  let len = reference_arity_length (ConstRef p) in
  let pb = Environ.lookup_projection (Projection.make p false) (Global.env ()) in 
    len - pb.Declarations.proj_npars

let class_params = function
  | CL_FUN | CL_SORT -> 0
  | CL_CONST sp -> reference_arity_length (ConstRef sp)
  | CL_PROJ sp -> projection_arity_length sp
  | CL_SECVAR sp -> reference_arity_length (VarRef sp)
  | CL_IND sp  -> reference_arity_length (IndRef sp)

(* add_class : cl_typ -> locality_flag option -> bool -> unit *)

let add_class cl =
  add_new_class cl { cl_param = class_params cl }

let automatically_import_coercions = ref false

open Goptions
let _ =
  declare_bool_option
    { optsync  = true;
      optdepr  = false;
      optname  = "automatic import of coercions";
      optkey   = ["Automatic";"Coercions";"Import"];
      optread  = (fun () -> !automatically_import_coercions);
      optwrite = (:=) automatically_import_coercions }

let cache_coercion (_, c) =
  let () = add_class c.coercion_source in
  let () = add_class c.coercion_target in
  let is, _ = class_info c.coercion_source in
  let it, _ = class_info c.coercion_target in
  let value, ctx = Universes.fresh_global_instance (Global.env()) c.coercion_type in
  let typ = Retyping.get_type_of (Global.env ()) Evd.empty value in
  let xf =
    { coe_value = value;
      coe_type = typ;
      coe_context = ctx;
      coe_local = c.coercion_local;
      coe_is_identity = c.coercion_is_id;
      coe_is_projection = c.coercion_is_proj;
      coe_param = c.coercion_params } in
  let () = add_new_coercion c.coercion_type xf in
  add_coercion_in_graph (xf,is,it)

let load_coercion _ o =
  if
    !automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2
  then
    cache_coercion o

let open_coercion i o =
  if Int.equal i 1 && not
    (!automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2)
  then
    cache_coercion o

let subst_coercion (subst, c) =
  let coe = subst_coe_typ subst c.coercion_type in
  let cls = subst_cl_typ subst c.coercion_source in
  let clt = subst_cl_typ subst c.coercion_target in
  if c.coercion_type == coe && c.coercion_source == cls && c.coercion_target == clt then c
  else { c with coercion_type = coe; coercion_source = cls; coercion_target = clt }

let discharge_cl = function
  | CL_CONST kn -> CL_CONST (Lib.discharge_con kn)
  | CL_IND ind -> CL_IND (Lib.discharge_inductive ind)
  | CL_PROJ p -> CL_PROJ (Lib.discharge_con p)
  | cl -> cl

let discharge_coercion (_, c) =
  if c.coercion_local then None
  else
    let n =
      try
        let ins = Lib.section_instance c.coercion_type in
        Array.length (snd ins)
      with Not_found -> 0
    in
    let nc = { c with
      coercion_type = Lib.discharge_global c.coercion_type;
      coercion_source = discharge_cl c.coercion_source;
      coercion_target = discharge_cl c.coercion_target;
      coercion_params = n + c.coercion_params;
    } in
    Some nc

let classify_coercion obj =
  if obj.coercion_local then Dispose else Substitute obj

let inCoercion : coercion -> obj =
  declare_object {(default_object "COERCION") with
    open_function = open_coercion;
    load_function = load_coercion;
    cache_function = cache_coercion;
    subst_function = subst_coercion;
    classify_function = classify_coercion;
    discharge_function = discharge_coercion }

let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps =
  let isproj = 
    match coef with
    | ConstRef c -> Environ.is_projection c (Global.env ())
    | _ -> false
  in
  let c = {
    coercion_type = coef;
    coercion_local = local;
    coercion_is_id = isid;
    coercion_is_proj = isproj;
    coercion_source = cls;
    coercion_target = clt;
    coercion_params = ps;
  } in
  Lib.add_anonymous_leaf (inCoercion c)

(* For printing purpose *)
let get_coercion_value v = v.coe_value

let pr_cl_index = Bijint.Index.print

let classes () = Bijint.dom !class_tab
let coercions () =
  List.rev (CoeTypMap.fold (fun _ y acc -> y::acc) !coercion_tab [])

let inheritance_graph () =
  ClPairMap.bindings !inheritance_graph

let coercion_of_reference r =
  let ref = Nametab.global r in
  if not (coercion_exists ref) then
    user_err ~hdr:"try_add_coercion"
      (Nametab.pr_global_env Id.Set.empty ref ++ str" is not a coercion.");
  ref

module CoercionPrinting =
  struct
    type t = coe_typ
    let compare = RefOrdered.compare
    let encode = coercion_of_reference
    let subst = subst_coe_typ
    let printer x = pr_global_env Id.Set.empty x
    let key = ["Printing";"Coercion"]
    let title = "Explicitly printed coercions: "
    let member_message x b =
      str "Explicit printing of coercion " ++ printer x ++
      str (if b then " is set" else " is unset")
    let synchronous = true
  end

module PrintingCoercion  = Goptions.MakeRefTable(CoercionPrinting)

let hide_coercion coe =
  if not (PrintingCoercion.active coe) then
    let coe_info = coercion_info coe in
    Some coe_info.coe_param
  else None