package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file coercionops.ml

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
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open CErrors
open Util
open Pp
open Names
open Constr
open Libnames
open Globnames
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.t
  | CL_IND of inductive
  | CL_PROJ of Projection.Repr.t

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 -> Constant.CanOrd.compare c1 c2
  | CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2
  | CL_IND i1, CL_IND i2 -> Ind.CanOrd.compare i1 i2
  | _ -> pervasives_compare t1 t2 (** OK *)

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

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

module ClTypSet = Set.Make(ClTyp)
module ClTypMap = Map.Make(ClTyp)

type cl_info_typ = {
  (* The number of parameters of the coercion class. *)
  cl_param : int;
  (* The sets of coercion classes respectively reachable from and to the
     coercion class. *)
  cl_reachable_from : ClTypSet.t;
  cl_reachable_to : ClTypSet.t;
  (* The representative class of the strongly connected component. *)
  cl_repr : cl_typ;
}

type coe_typ = GlobRef.t

module CoeTypMap = GlobRef.Map_env

type coe_info_typ = {
  coe_value : GlobRef.t;
  coe_typ : Constr.t;
  coe_local : bool;
  coe_reversible : bool;
  coe_is_identity : bool;
  coe_is_projection : Projection.Repr.t option;
  coe_source : cl_typ;
  coe_target : cl_typ;
  coe_param : int;
}

type inheritance_path = coe_info_typ list

let init_class_tab =
  let open ClTypMap in
  let cl_info params cl =
    let cl_singleton = ClTypSet.singleton cl in
    { cl_param = params;
      cl_reachable_from = cl_singleton;
      cl_reachable_to = cl_singleton;
      cl_repr = cl }
  in
  add CL_FUN (cl_info 0 CL_FUN) (add CL_SORT (cl_info 0 CL_SORT) empty)

let class_tab =
  Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ ClTypMap.t)

let coercion_tab =
  Summary.ref ~name:"coercion_tab" (CoeTypMap.empty : coe_info_typ CoeTypMap.t)

let reachable_from cl =
  try (ClTypMap.find cl !class_tab).cl_reachable_from
  with Not_found -> ClTypSet.empty

module ClGraph :
sig
  type t
  val empty : t
  val add : cl_typ -> cl_typ -> inheritance_path -> t -> t
  val find : cl_typ -> cl_typ -> t -> inheritance_path
  val src : cl_typ -> t -> inheritance_path ClTypMap.t
  val dst : cl_typ -> t -> inheritance_path ClTypMap.t
  val bindings : t -> ((cl_typ * cl_typ) * inheritance_path) list
end =
struct
  type map = inheritance_path ClTypMap.t ClTypMap.t
  type t = map * map
  (* Doubly-indexed map in both directions *)
  let empty = ClTypMap.empty, ClTypMap.empty
  let add0 x y p m =
    let n = try ClTypMap.find x m with Not_found -> ClTypMap.empty in
    ClTypMap.add x (ClTypMap.add y p n) m
  let add x y p (ml, mr) = (add0 x y p ml, add0 y x p mr)
  let find x y (m, _) = ClTypMap.find y (ClTypMap.find x m)
  let src x (m, _) = try ClTypMap.find x m with Not_found -> ClTypMap.empty
  let dst x (_, m) = try ClTypMap.find x m with Not_found -> ClTypMap.empty

  let bindings (m, _) =
    let fold s n accu =
      let fold t p accu = ((s, t), p) :: accu in
      ClTypMap.fold fold n accu
    in
    List.rev (ClTypMap.fold fold m [])
end

let inheritance_graph =
  Summary.ref ~name:"inheritance_graph" ClGraph.empty

(* ajout de nouveaux "objets" *)

let add_new_class cl s =
  class_tab := ClTypMap.add cl s !class_tab

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

let add_path (x, y) p =
  inheritance_graph := ClGraph.add x y p !inheritance_graph

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

let class_info cl = ClTypMap.find cl !class_tab

let class_nparams cl = (class_info cl).cl_param

let class_exists cl = ClTypMap.mem cl !class_tab

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 env sigma t =
  let open EConstr in
  let t', args = Reductionops.whd_betaiotazeta_stack env sigma t in
  match EConstr.kind sigma t' with
    | Var id -> CL_SECVAR id, EInstance.empty, args
    | Const (sp,u) -> CL_CONST sp, u, args
    | Proj (p, c) when not (Projection.unfolded p) ->
      let revparams =
        let open Inductiveops in
        let t = Retyping.get_type_of env sigma c in
        let IndType (fam,_) = find_rectype env sigma t in
        let _, params = dest_ind_family fam in
        List.rev_map EConstr.of_constr params
      in
      CL_PROJ (Projection.repr p), EInstance.empty, (List.rev_append revparams (c :: args))
    | Ind (ind_sp,u) -> CL_IND ind_sp, u, args
    | Prod _ -> CL_FUN, EInstance.empty, []
    | Sort _ -> CL_SORT, EInstance.empty, []
    |  _ -> raise Not_found


let subst_cl_typ env subst ct = match ct with
    CL_SORT
  | CL_FUN
  | CL_SECVAR _ -> ct
  | CL_PROJ c ->
    let c' = subst_proj_repr subst c in
      if c' == c then ct else CL_PROJ c'
  | CL_CONST c ->
      let c',t = subst_con subst c in
      if c' == c then ct else (match t with
          | None -> CL_CONST c'
          | Some t ->
            pi1 (find_class_type env Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)))
  | 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, cl, u, args) =
    try
      let (cl, u, args) = find_class_type env sigma t in
      let { cl_param = n1 } = class_info cl in
      (t, n1, cl, u, args)
    with Not_found ->
      let t = Tacred.hnf_constr env sigma t in
      let (cl, u, args) = find_class_type env sigma t in
      let { cl_param = n1 } = class_info cl in
      (t, n1, cl, u, args)
  in
  if Int.equal (List.length args) n1 then t, cl else raise Not_found

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

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

let pr_class x = str (string_of_class x)

(* lookup paths *)

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

let lookup_path_to_fun_from_class s =
  lookup_path_between_class (s, CL_FUN)

let lookup_path_to_sort_from_class s =
  lookup_path_between_class (s, CL_SORT)

(* advanced path lookup *)

let apply_on_class_of env sigma t cont =
  try
    let (cl,u,args) = find_class_type env sigma t in
    let { cl_param = n1 } = class_info cl in
    if not (Int.equal (List.length args) n1) then raise Not_found;
    cont cl
  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 env sigma t in
    let { cl_param = n1 } = class_info cl in
    if not (Int.equal (List.length args) n1) then raise Not_found;
    cont cl

let lookup_path_between env sigma ~src:s ~tgt:t =
  apply_on_class_of env sigma s (fun i ->
      apply_on_class_of env sigma t (fun j ->
          lookup_path_between_class (i,j)))

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 evd = Evd.from_env env in
  let evd, c = Evd.fresh_global env evd coe.coe_value in
  let c = fst (Reductionops.whd_all_stack env evd c) in
  match EConstr.kind evd c with
  | Constr.Construct (c, _) ->
    (* we don't return the modified evd as we drop the universes *)
    c, Inductiveops.constructor_nrealargs env c -1
  | _ -> raise Not_found

let lookup_pattern_path_between env (s,t) =
  List.map (get_coercion_constructor env)
    (ClGraph.find (CL_IND s) (CL_IND t) !inheritance_graph)

let path_is_reversible p =
  List.for_all (fun c -> c.coe_reversible) p

(* rajouter une coercion dans le graphe *)

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

let install_path_printer f = path_printer := f

let print_path x = !path_printer x

let path_comparator :
  (Environ.env -> Evd.evar_map -> cl_typ -> inheritance_path -> inheritance_path -> bool) ref =
  ref (fun _ _ _ _ _ -> false)

let install_path_comparator f = path_comparator := f

let compare_path env sigma cl p q = !path_comparator env sigma cl p q

let warn_ambiguous_path =
  CWarnings.create ~name:"ambiguous-paths" ~category:CWarnings.CoreCategories.coercions
    (fun l -> prlist_with_sep fnl (fun (c,p,q) ->
         str"New coercion path " ++ print_path (c,p) ++
         if List.is_empty q then
           str" is not definitionally an identity function."
         else
           str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l)

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

let different_class_params env ci =
  if (class_info ci).cl_param > 0 then true
  else
    match ci with
    | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i)
    | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c)
    | _ -> false

let add_coercion_in_graph env sigma ?(update=false) ic =
  let source = ic.coe_source in
  let target = ic.coe_target in
  let source_info = class_info source in
  let target_info = class_info target in
  let old_inheritance_graph = !inheritance_graph in
  let ambig_paths :
    ((cl_typ * cl_typ) * inheritance_path * inheritance_path) list ref =
    ref [] in
  let check_coherence (i, j as ij) p q =
    let i_info = class_info i in
    let j_info = class_info j in
    let between_ij = ClTypSet.inter i_info.cl_reachable_from j_info.cl_reachable_to in
    if cl_typ_eq i_info.cl_repr i &&
       cl_typ_eq j_info.cl_repr j &&
       ClTypSet.is_empty
         (ClTypSet.diff (ClTypSet.inter between_ij source_info.cl_reachable_to)
            i_info.cl_reachable_to) &&
       ClTypSet.is_empty
         (ClTypSet.diff
            (ClTypSet.inter between_ij target_info.cl_reachable_from)
            j_info.cl_reachable_from) &&
       not (compare_path env sigma i p q)
    then
      ambig_paths := (ij, p, q) :: !ambig_paths
  in
  let try_add_new_path (i,j as ij) p =
    if cl_typ_eq i j then check_coherence ij p [];
    if not (cl_typ_eq i j) || different_class_params env i then
      if update then let () = add_path ij p in true else
        match lookup_path_between_class ij with
        | q -> (if not (cl_typ_eq i j) then check_coherence ij p q); false
        | exception Not_found -> add_path ij p; true
    else
      false
  in
  if try_add_new_path (source, target) [ic] then begin
    let rev = ClGraph.dst source old_inheritance_graph in
    let dir = ClGraph.src target old_inheritance_graph in
    let iter s p =
      if not (cl_typ_eq s source) then
        let _ = try_add_new_path (s, target) (p@[ic]) in
        let iter v q =
          if not (cl_typ_eq target v) then
            ignore (try_add_new_path (s,v) (p@[ic]@q))
        in
        ClTypMap.iter iter dir
    in
    let () = ClTypMap.iter iter rev in
    let iter t p =
      if not (cl_typ_eq t target) then
        ignore (try_add_new_path (source, t) (ic::p))
    in
    ClTypMap.iter iter dir
  end;
  class_tab := ClTypMap.mapi (fun k k_info ->
      let reachable_k_source = ClTypSet.mem k source_info.cl_reachable_to in
      let reachable_target_k = ClTypSet.mem k target_info.cl_reachable_from in
      { k_info with
        cl_reachable_from =
          if reachable_k_source then
            ClTypSet.union
              k_info.cl_reachable_from target_info.cl_reachable_from
          else
            k_info.cl_reachable_from;
        cl_reachable_to =
          if reachable_target_k then
            ClTypSet.union k_info.cl_reachable_to source_info.cl_reachable_to
          else
            k_info.cl_reachable_to;
        cl_repr =
          if reachable_k_source && reachable_target_k then
            target_info.cl_repr
          else
            k_info.cl_repr
      }) !class_tab;
  match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths

let subst_coercion subst c =
  let env = Global.env () in
  let coe = subst_coe_typ subst c.coe_value in
  let typ = subst_mps subst c.coe_typ in
  let cls = subst_cl_typ env subst c.coe_source in
  let clt = subst_cl_typ env subst c.coe_target in
  let clp = Option.Smart.map (subst_proj_repr subst) c.coe_is_projection in
  if c.coe_value == coe && c.coe_source == cls && c.coe_target == clt &&
     c.coe_is_projection == clp
  then c
  else { c with coe_value = coe; coe_typ = typ; coe_source = cls; coe_target = clt;
                coe_is_projection = clp; }

(* Computation of the class arity *)

let reference_arity_length env sigma ref =
  let t, _ = Typeops.type_of_global_in_context env ref in
  List.length (fst (Reductionops.splay_arity env sigma (EConstr.of_constr t)))

let projection_arity_length env sigma p =
  reference_arity_length env sigma (GlobRef.ConstRef (Projection.Repr.constant p))

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

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

let add_class env sigma cl =
  if not (class_exists cl) then
    let cl_singleton = ClTypSet.singleton cl in
    add_new_class cl {
      cl_param = class_params env sigma cl;
      cl_reachable_from = cl_singleton;
      cl_reachable_to = cl_singleton;
      cl_repr = cl }

let declare_coercion env sigma ?update c =
  let () = add_class env sigma c.coe_source in
  let () = add_class env sigma c.coe_target in
  let () = add_coercion c.coe_value c in
  add_coercion_in_graph env sigma ?update c

(* For printing purpose *)
let classes () =
  List.rev (ClTypMap.fold (fun x _ acc -> x :: acc) !class_tab [])
let coercions () =
  List.rev (CoeTypMap.fold (fun _ y acc -> y::acc) !coercion_tab [])

let inheritance_graph () =
  ClGraph.bindings !inheritance_graph

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

module CoercionPrinting =
  struct
    type t = coe_typ
    module Set = GlobRef.Set
    let encode _env = coercion_of_reference
    let subst = subst_coe_typ
    let printer x = Nametab.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")
  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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct