diff options
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 72 |
1 files changed, 22 insertions, 50 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 54a1aa9aa0..5560e5e5f5 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -120,9 +120,6 @@ let class_tab = let coercion_tab = Summary.ref ~name:"coercion_tab" (CoeTypMap.empty : coe_info_typ CoeTypMap.t) -let coercions_in_scope = - Summary.ref ~name:"coercions_in_scope" GlobRef.Set_env.empty - module ClPairOrd = struct type t = cl_index * cl_index @@ -308,9 +305,16 @@ 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 print_path l +let path_comparator : (inheritance_path -> inheritance_path -> bool) ref = + ref (fun _ _ -> false) + +let install_path_comparator f = path_comparator := f + +let compare_path p q = !path_comparator p q + +let warn_ambiguous_path = + CWarnings.create ~name:"ambiguous-paths" ~category:"typechecker" + (fun l -> strbrk"Ambiguous paths: " ++ prlist_with_sep fnl print_path l) (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) @@ -329,21 +333,15 @@ let add_coercion_in_graph (ic,source,target) = 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; + if not (Bijint.Index.equal i j) || different_class_params i then + match lookup_path_between_class ij with + | q -> + if not (compare_path p q) then + ambig_paths := (ij,p)::!ambig_paths; + false + | exception Not_found -> (add_new_path ij p; true) + else 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 () @@ -364,9 +362,7 @@ let add_coercion_in_graph (ic,source,target) = end) old_inheritance_graph end; - let is_ambig = match !ambig_paths with [] -> false | _ -> true in - if is_ambig && not !Flags.quiet then - Feedback.msg_info (message_ambig !ambig_paths) + match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths type coercion = { coercion_type : coe_typ; @@ -400,13 +396,6 @@ let class_params = function let add_class cl = add_new_class cl { cl_param = class_params cl } -let get_automatically_import_coercions = - Goptions.declare_bool_option_and_ref - ~depr:true (* Remove in 8.8 *) - ~name:"automatic import of coercions" - ~key:["Automatic";"Coercions";"Import"] - ~value:false - let cache_coercion (_, c) = let () = add_class c.coercion_source in let () = add_class c.coercion_target in @@ -422,20 +411,9 @@ let cache_coercion (_, c) = let () = add_new_coercion c.coercion_type xf in add_coercion_in_graph (xf,is,it) -let load_coercion _ o = - if get_automatically_import_coercions () then - cache_coercion o - -let set_coercion_in_scope (_, c) = - let r = c.coercion_type in - coercions_in_scope := GlobRef.Set_env.add r !coercions_in_scope - let open_coercion i o = - if Int.equal i 1 then begin - set_coercion_in_scope o; - if not (get_automatically_import_coercions ()) then - cache_coercion o - end + if Int.equal i 1 then + cache_coercion o let subst_coercion (subst, c) = let coe = subst_coe_typ subst c.coercion_type in @@ -469,10 +447,7 @@ let classify_coercion obj = let inCoercion : coercion -> obj = declare_object {(default_object "COERCION") with open_function = open_coercion; - load_function = load_coercion; - cache_function = (fun objn -> - set_coercion_in_scope objn; - cache_coercion objn); + cache_function = cache_coercion; subst_function = subst_coercion; classify_function = classify_coercion; discharge_function = discharge_coercion } @@ -532,6 +507,3 @@ let hide_coercion coe = let coe_info = coercion_info coe in Some coe_info.coe_param else None - -let is_coercion_in_scope r = - GlobRef.Set_env.mem r !coercions_in_scope |