aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--pretyping/classops.ml30
1 files changed, 22 insertions, 8 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index a9a65b8d1..333384505 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -99,8 +99,18 @@ let class_tab =
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 = Int.compare i1 i2 in
+ if c = 0 then Int.compare j1 j2 else c
+end
+
+module ClPairMap = Map.Make(ClPairOrd)
+
let inheritance_graph =
- ref (Gmap.empty : (cl_index * cl_index, inheritance_path) Gmap.t)
+ ref (ClPairMap.empty : inheritance_path ClPairMap.t)
let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph)
@@ -119,14 +129,14 @@ let add_new_coercion coe s =
coercion_tab := CoeTypMap.add coe s !coercion_tab
let add_new_path x y =
- inheritance_graph := Gmap.add x y !inheritance_graph
+ 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:= Gmap.empty
+ inheritance_graph:= ClPairMap.empty
let _ =
Summary.declare_summary "inh_graph"
@@ -221,7 +231,7 @@ let pr_class x = str (string_of_class x)
(* lookup paths *)
let lookup_path_between_class (s,t) =
- Gmap.find (s,t) !inheritance_graph
+ ClPairMap.find (s,t) !inheritance_graph
let lookup_path_to_fun_from_class s =
lookup_path_between_class (s,cl_fun_index)
@@ -271,7 +281,7 @@ let get_coercion_constructor coe =
let lookup_pattern_path_between (s,t) =
let i = inductive_class_of s in
let j = inductive_class_of t in
- List.map get_coercion_constructor (Gmap.find (i,j) !inheritance_graph)
+ List.map get_coercion_constructor (ClPairMap.find (i,j) !inheritance_graph)
(* coercion_value : coe_index -> unsafe_judgment * bool *)
@@ -323,12 +333,12 @@ let add_coercion_in_graph (ic,source,target) =
let _ = try_add_new_path ij p in ()
in
if try_add_new_path (source,target) [ic] then begin
- Gmap.iter
+ ClPairMap.iter
(fun (s,t) p ->
if not (Int.equal s t) then begin
if Int.equal t source then begin
try_add_new_path1 (s,target) (p@[ic]);
- Gmap.iter
+ ClPairMap.iter
(fun (u,v) q ->
if not (Int.equal u v) && Int.equal u target && not (List.equal coe_info_typ_equal p q) then
try_add_new_path1 (s,v) (p@[ic]@q))
@@ -467,7 +477,11 @@ let pr_cl_index n = int n
let classes () = Bijint.dom !class_tab
let coercions () =
List.rev (CoeTypMap.fold (fun _ y acc -> y::acc) !coercion_tab [])
-let inheritance_graph () = Gmap.to_list !inheritance_graph
+
+let inheritance_graph () =
+ (** FIXME: in 3.12 use Map.keys *)
+ let fold k v acc = (k, v) :: acc in
+ ClPairMap.fold fold !inheritance_graph []
let coercion_of_reference r =
let ref = Nametab.global r in