diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/classops.ml | 28 | ||||
| -rw-r--r-- | pretyping/classops.mli | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 31 |
3 files changed, 49 insertions, 12 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index c12a236d8e..16021b66f8 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -297,15 +297,15 @@ let lookup_pattern_path_between env (s,t) = (* rajouter une coercion dans le graphe *) -let path_printer : ((Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = +let path_printer : ((cl_index * cl_index) * 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 -> inheritance_path -> inheritance_path -> bool) ref = - ref (fun _ _ _ _ -> false) +let path_comparator : (Environ.env -> Evd.evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) ref = + ref (fun _ _ _ _ _ -> false) let install_path_comparator f = path_comparator := f @@ -315,7 +315,10 @@ let warn_ambiguous_path = CWarnings.create ~name:"ambiguous-paths" ~category:"typechecker" (fun l -> prlist_with_sep fnl (fun (c,p,q) -> str"New coercion path " ++ print_path (c,p) ++ - str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l) + 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_index * cl_index -> unit coercion,source,target *) @@ -334,10 +337,23 @@ let add_coercion_in_graph env sigma (ic,source,target) = let ambig_paths = (ref [] : ((cl_index * cl_index) * inheritance_path * inheritance_path) list ref) 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 not (Bijint.Index.equal i j) || different_class_params env i then match lookup_path_between_class ij with | q -> - if not (compare_path env sigma p q) then + (* 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) @@ -355,7 +371,7 @@ let add_coercion_in_graph env sigma (ic,source,target) = try_add_new_path1 (s,target) (p@[ic]); ClPairMap.iter (fun (u,v) q -> - if not (Bijint.Index.equal u v) && Bijint.Index.equal u target && not (List.equal coe_info_typ_equal p q) then + if not (Bijint.Index.equal u v) && Bijint.Index.equal u target then try_add_new_path1 (s,v) (p@[ic]@q)) old_inheritance_graph end; diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 9c5274286e..9f633843eb 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -111,7 +111,7 @@ val lookup_pattern_path_between : val install_path_printer : ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit val install_path_comparator : - (env -> evar_map -> inheritance_path -> inheritance_path -> bool) -> unit + (env -> evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) -> unit (**/**) (** {6 This is for printing purpose } *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 43f9e55e14..0364e1b61f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1325,19 +1325,20 @@ 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 env sigma p q = +let path_convertible env sigma i 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,Explicit,t,b) in + let mkGSort u = DAst.make @@ Glob_term.GSort u 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) + List.init (ic.coe_param + 1) + (fun n -> Id.of_string ("x" ^ string_of_int n)) in List.fold_right (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@ @@ -1345,9 +1346,29 @@ let path_convertible env sigma p q = (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)) + (mkGApp (mkGRef ic.coe_value, List.map mkGVar names)) p' - | [] -> anomaly (str "A coercion path shouldn't be empty.") + | [] -> + (* identity function for the class [i]. *) + let cl,params = class_info_from_index i in + let clty = + match cl with + | CL_SORT -> mkGSort (Glob_term.UAnonymous {rigid=false}) + | CL_FUN -> anomaly (str "A source class must not be Funclass.") + | CL_SECVAR v -> mkGRef (GlobRef.VarRef v) + | CL_CONST c -> mkGRef (GlobRef.ConstRef c) + | CL_IND i -> mkGRef (GlobRef.IndRef i) + | CL_PROJ p -> mkGRef (GlobRef.ConstRef (Projection.Repr.constant p)) + in + let names = + List.init params.cl_param + (fun n -> Id.of_string ("x" ^ string_of_int n)) + in + List.fold_right + (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@ + mkGLambda (Name (Id.of_string "x"), + mkGApp (clty, List.map mkGVar names), + mkGVar (Id.of_string "x")) in try let sigma,tp = understand_tcc env sigma (path_to_gterm p) in |