Skip to content

Commit

Permalink
Minimize the set of multiple inheritance paths to check for conversion
Browse files Browse the repository at this point in the history 
The table of coercion classes (`class_tab`) has been extended with information
about reachability. The conversion checking of multiple inheritance paths (of
coercions) will be skipped if these paths can be reduced to a set of smaller
paths in some sense, and this will be determined based on that reachability
information.
  • Loading branch information
@pi8027
pi8027 committed Mar 7, 2021
1 parent 0d20fdb commit fa3716a
Show file tree
Hide file tree
Showing 2 changed files with 110 additions and 58 deletions.
154 changes: 97 additions & 57 deletions pretyping/coercionops.ml
View file
Expand Up @@ -30,44 +30,41 @@ type cl_typ =
| CL_IND of inductive
| CL_PROJ of Projection.Repr.t

type cl_info_typ = {
cl_param : int
}

type coe_typ = GlobRef.t

module CoeTypMap = GlobRef.Map_env

type coe_info_typ = {
coe_value : GlobRef.t;
coe_local : bool;
coe_is_identity : bool;
coe_is_projection : Projection.Repr.t option;
coe_param : int;
}

let coe_info_typ_equal c1 c2 =
GlobRef.equal c1.coe_value c2.coe_value &&
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 -> 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)

let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
type cl_info_typ = {
cl_param : int;
cl_reachable_from : ClTypSet.t;
cl_reachable_to : ClTypSet.t;
cl_repr : cl_typ;
}

type coe_typ = GlobRef.t

module CoeTypMap = GlobRef.Map_env

type coe_info_typ = {
coe_value : GlobRef.t;
coe_local : bool;
coe_is_identity : bool;
coe_is_projection : Projection.Repr.t option;
coe_param : int;
}

type inheritance_path = coe_info_typ list

Expand All @@ -85,10 +82,11 @@ sig
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 find : Index.t -> 'a t -> cl_typ * 'a
val revfind : cl_typ -> 'a t -> Index.t * 'a
val add : cl_typ -> 'a -> 'a t -> 'a t
val dom : 'a t -> cl_typ list
val mapi : (Index.t -> cl_typ -> 'a -> 'b) -> 'a t -> 'b t
end
=
struct
Expand All @@ -98,18 +96,28 @@ struct
type 'a t = { v : (cl_typ * 'a) Int.Map.t; s : int; inv : int ClTypMap.t }
let empty = { v = Int.Map.empty; s = 0; inv = ClTypMap.empty }
let mem y b = ClTypMap.mem y b.inv
let map x b = Int.Map.find x b.v
let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (Int.Map.find n b.v))
let find x b = Int.Map.find x b.v
let revfind y b =
let n = ClTypMap.find y b.inv in (n, snd (Int.Map.find n b.v))
let add x y b =
{ v = Int.Map.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 [])
let mapi f b = { v = Int.Map.mapi (fun i (cl, x) -> (cl, f i cl x)) b.v;
s = b.s; inv = b.inv }
end

type cl_index = Bijint.Index.t

let init_class_tab =
let open Bijint in
add CL_FUN { cl_param = 0 } (add CL_SORT { cl_param = 0 } empty)
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 Bijint.t)
Expand All @@ -133,8 +141,7 @@ let inheritance_graph =
(* 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
class_tab := Bijint.add cl s !class_tab

let add_new_coercion coe s =
coercion_tab := CoeTypMap.add coe s !coercion_tab
Expand All @@ -144,13 +151,13 @@ let add_new_path x y =

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

let class_info cl = Bijint.revmap cl !class_tab
let class_info cl = Bijint.revfind 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 class_info_from_index i = Bijint.find i !class_tab

let cl_fun_index = fst(class_info CL_FUN)

Expand Down Expand Up @@ -328,31 +335,39 @@ let different_class_params env i =
| CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c)
| _ -> false

let add_coercion_in_graph env sigma (ic,source,target) =
let add_coercion_in_graph env sigma (ic, cls, clt) =
let source, source_info = class_info cls in
let target, target_info = class_info clt in
let old_inheritance_graph = !inheritance_graph in
let ambig_paths =
(ref [] : ((cl_index * cl_index) * inheritance_path * inheritance_path) list ref) in
let ambig_paths :
((cl_index * cl_index) * inheritance_path * inheritance_path) list ref =
ref []
in
let check_coherence (i, j as ij) p q =
let cli, i_info = class_info_from_index i in
let clj, j_info = class_info_from_index j in
let between_ij =
ClTypSet.inter i_info.cl_reachable_from j_info.cl_reachable_to in
if cl_typ_eq cli i_info.cl_repr &&
cl_typ_eq clj j_info.cl_repr &&
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 p is a cycle, we check whether p is definitionally an identity
function or not. If it is not, we report p as an ambiguous inheritance
path. *)
if Bijint.Index.equal i j && not (compare_path env sigma i p []) then
ambig_paths := (ij,p,[])::!ambig_paths;
if Bijint.Index.equal i j then check_coherence ij p [];
if not (Bijint.Index.equal i j) || different_class_params env i then
match lookup_path_between_class ij with
| q ->
(* p has the same source and target classes as an existing path q. We
report them as ambiguous inheritance paths if
1. p and q have no common element, and
2. p and q are not convertible.
If 1 does not hold, say p = p1 @ [c] @ p2 and q = q1 @ [c] @ q2,
convertibility of p1 and q1, also, p2 and q2 should be checked; thus,
checking the ambiguity of p and q is redundant with them. *)
if not (List.exists (fun c -> List.exists (coe_info_typ_equal c) q) p ||
compare_path env sigma i p q) then
ambig_paths := (ij,p,q)::!ambig_paths;
false
| exception Not_found -> (add_new_path ij p; true)
(if not (Bijint.Index.equal i j) then check_coherence ij p q); false
| exception Not_found -> add_new_path ij p; true
else
false
in
Expand All @@ -375,6 +390,27 @@ let add_coercion_in_graph env sigma (ic,source,target) =
end)
old_inheritance_graph
end;
class_tab := Bijint.mapi (fun k clk k_info ->
let reachable_k_source = ClTypSet.mem clk source_info.cl_reachable_to in
let reachable_target_k = ClTypSet.mem clk target_info.cl_reachable_from in
{ cl_param = k_info.cl_param;
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

type coercion = {
Expand Down Expand Up @@ -419,13 +455,17 @@ let class_params env sigma = function
(* add_class : cl_typ -> locality_flag option -> bool -> unit *)

let add_class env sigma cl =
add_new_class cl { cl_param = class_params 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 c =
let () = add_class env sigma c.coercion_source in
let () = add_class env sigma c.coercion_target in
let is, _ = class_info c.coercion_source in
let it, _ = class_info c.coercion_target in
let xf =
{ coe_value = c.coercion_type;
coe_local = c.coercion_local;
Expand All @@ -434,7 +474,7 @@ let declare_coercion env sigma c =
coe_param = c.coercion_params;
} in
let () = add_new_coercion c.coercion_type xf in
add_coercion_in_graph env sigma (xf,is,it)
add_coercion_in_graph env sigma (xf, c.coercion_source, c.coercion_target)

(* For printing purpose *)
let pr_cl_index = Bijint.Index.print
Expand Down
14 changes: 13 additions & 1 deletion pretyping/coercionops.mli
View file
Expand Up @@ -31,9 +31,21 @@ val subst_cl_typ : env -> substitution -> cl_typ -> cl_typ
(** Comparison of [cl_typ] *)
val cl_typ_ord : cl_typ -> cl_typ -> int

module ClTyp : Map.OrderedType with type t = cl_typ

module ClTypSet : Set.S with type t = Set.Make(ClTyp).t

(** This is the type of infos for declared classes *)
type cl_info_typ = {
cl_param : int }
(* 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;
}

(** This is the type of coercion kinds *)
type coe_typ = GlobRef.t
Expand Down

0 comments on commit fa3716a

Please sign in to comment.