diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/classops.ml | 39 | ||||
| -rw-r--r-- | pretyping/classops.mli | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 36 |
3 files changed, 57 insertions, 20 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 306a76e35e..0c44732021 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -308,9 +308,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 +336,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 +365,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; diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 7c4842c8ae..a63f6a7487 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -100,6 +100,8 @@ val lookup_pattern_path_between : (* Crade *) val install_path_printer : ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit +val install_path_comparator : + (inheritance_path -> inheritance_path -> bool) -> unit (**/**) (** {6 This is for printing purpose } *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 9612932439..7405060188 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1128,3 +1128,39 @@ let understand_tcc ?flags env sigma ?expected_type c = let understand_ltac flags env sigma lvar kind c = let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in (sigma, c) + +let path_convertible p q = + let open Classops in + let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in + let mkGVar id = DAst.make @@ Glob_term.GVar(id) in + let mkGApp(rt,rtl) = DAst.make @@ Glob_term.GApp(rt,rtl) in + let mkGLambda(n,t,b) = DAst.make @@ Glob_term.GLambda(n,Decl_kinds.Explicit,t,b) in + let mkGHole () = DAst.make @@ Glob_term.GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None) in + let path_to_gterm p = + match p with + | ic :: p' -> + let names = + List.map (fun n -> Id.of_string ("x" ^ string_of_int n)) + (List.interval 0 ic.coe_param) + in + List.fold_right + (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@ + List.fold_left + (fun t ic -> + mkGApp (mkGRef ic.coe_value, + List.make ic.coe_param (mkGHole ()) @ [t])) + (mkGApp (mkGRef ic.coe_value, List.map (fun i -> mkGVar i) names)) + p' + | [] -> anomaly (str "A coercion path shouldn't be empty.") + in + try + let e = Global.env () in + let sigma,tp = understand_tcc e (Evd.from_env e) (path_to_gterm p) in + let sigma,tq = understand_tcc e sigma (path_to_gterm q) in + if Evd.has_undefined sigma then + false + else + let _ = Evarconv.unify_delay e sigma tp tq in true + with Evarconv.UnableToUnify _ | PretypeError _ -> false + +let _ = Classops.install_path_comparator path_convertible |