diff options
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 1 | ||||
| -rw-r--r-- | dev/top_printers.mli | 2 | ||||
| -rw-r--r-- | pretyping/coercionops.ml | 188 | ||||
| -rw-r--r-- | pretyping/coercionops.mli | 21 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 7 | ||||
| -rw-r--r-- | test-suite/output/relaxed_ambiguous_paths.out | 20 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 19 |
8 files changed, 91 insertions, 168 deletions
diff --git a/dev/base_include b/dev/base_include index f375a867bc..061bf1f3e1 100644 --- a/dev/base_include +++ b/dev/base_include @@ -16,7 +16,6 @@ #install_printer (* kernel_name *) ppkn;; #install_printer (* constant *) ppcon;; #install_printer (* projection *) ppproj;; -#install_printer (* cl_index *) ppclindex;; #install_printer (* recarg Rtree.t *) ppwf_paths;; #install_printer (* constr *) print_pure_constr;; #install_printer (* patch *) ppripos;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f8fd8b3d5b..67fe7b980b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -52,7 +52,6 @@ let ppmind kn = pp(MutInd.debug_print kn) let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i) let ppsp sp = pp(pr_path sp) let ppqualid qid = pp(pr_qualid qid) -let ppclindex cl = pp(Coercionops.pr_cl_index cl) let ppscheme k = pp (Ind_tables.pr_scheme_kind k) let prrecarg = Declareops.pp_recarg diff --git a/dev/top_printers.mli b/dev/top_printers.mli index b4b24d743a..ba7d92f907 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -29,8 +29,6 @@ val ppind : Names.inductive -> unit val ppsp : Libnames.full_path -> unit val ppqualid : Libnames.qualid -> unit -val ppclindex : Coercionops.cl_index -> unit - val ppscheme : 'a Ind_tables.scheme_kind -> unit val prrecarg : Declarations.recarg -> Pp.t diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml index ac89dfd747..b62dbdb412 100644 --- a/pretyping/coercionops.ml +++ b/pretyping/coercionops.ml @@ -34,6 +34,31 @@ type cl_info_typ = { cl_param : int } +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 ClPairOrd = +struct + type t = cl_typ * cl_typ + let compare (i1, j1) (i2, j2) = + let c = cl_typ_ord i1 i2 in + if Int.equal c 0 then cl_typ_ord j1 j2 else c +end + +module ClTypMap = Map.Make(ClTyp) +module ClPairMap = Map.Make(ClPairOrd) + type coe_typ = GlobRef.t module CoeTypMap = GlobRef.Map_env @@ -53,88 +78,26 @@ let coe_info_typ_equal c1 c2 = 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 *) - -module ClTyp = struct - type t = cl_typ - let compare = cl_typ_ord -end - -module ClTypMap = Map.Make(ClTyp) - -let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0 - type inheritance_path = coe_info_typ list -(* table des classes, des coercions et graphe d'heritage *) - -module Bijint : -sig - module Index : - sig - type t - val compare : t -> t -> int - val equal : t -> t -> bool - val print : t -> Pp.t - end - 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 add : cl_typ -> 'a -> 'a t -> 'a t - val dom : 'a t -> cl_typ list -end -= -struct - - module Index = struct include Int let print = Pp.int end - - 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 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 []) -end - -type cl_index = Bijint.Index.t - let init_class_tab = - let open Bijint in + let open ClTypMap in add CL_FUN { cl_param = 0 } (add CL_SORT { cl_param = 0 } empty) let class_tab = - Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ Bijint.t) + Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ ClTypMap.t) let coercion_tab = Summary.ref ~name:"coercion_tab" (CoeTypMap.empty : coe_info_typ CoeTypMap.t) -module ClPairOrd = -struct - type t = cl_index * cl_index - let compare (i1, j1) (i2, j2) = - let c = Bijint.Index.compare i1 i2 in - if Int.equal c 0 then Bijint.Index.compare j1 j2 else c -end - -module ClPairMap = Map.Make(ClPairOrd) - let inheritance_graph = Summary.ref ~name:"inheritance_graph" (ClPairMap.empty : inheritance_path ClPairMap.t) (* 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 + if not (ClTypMap.mem cl !class_tab) then + class_tab := ClTypMap.add cl s !class_tab let add_new_coercion coe s = coercion_tab := CoeTypMap.add coe s !coercion_tab @@ -144,17 +107,9 @@ 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 = ClTypMap.find 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 cl_fun_index = fst(class_info CL_FUN) - -let cl_sort_index = fst(class_info CL_SORT) +let class_exists cl = ClTypMap.mem cl !class_tab let coercion_info coe = CoeTypMap.find coe !coercion_tab @@ -200,20 +155,18 @@ let subst_coe_typ subst t = subst_global_reference subst t (* class_of : Term.constr -> int *) let class_of env sigma t = - let (t, n1, i, u, args) = + let (t, n1, cl, u, args) = try let (cl, u, args) = find_class_type env sigma t in - let (i, { cl_param = n1 } ) = class_info cl in - (t, n1, i, u, args) + let { cl_param = n1 } = class_info cl in + (t, n1, cl, u, args) with Not_found -> let t = Tacred.hnf_constr env sigma t in let (cl, u, args) = find_class_type env sigma t in - let (i, { cl_param = n1 } ) = class_info cl in - (t, n1, i, u, args) + let { cl_param = n1 } = class_info cl in + (t, n1, cl, u, args) in - if Int.equal (List.length args) n1 then t, i else raise Not_found - -let inductive_class_of ind = fst (class_info (CL_IND ind)) + if Int.equal (List.length args) n1 then t, cl else raise Not_found let class_args_of env sigma c = pi3 (find_class_type env sigma c) @@ -238,26 +191,26 @@ let lookup_path_between_class (s,t) = ClPairMap.find (s,t) !inheritance_graph let lookup_path_to_fun_from_class s = - lookup_path_between_class (s,cl_fun_index) + lookup_path_between_class (s, CL_FUN) let lookup_path_to_sort_from_class s = - lookup_path_between_class (s,cl_sort_index) + lookup_path_between_class (s, CL_SORT) (* advanced path lookup *) let apply_on_class_of env sigma t cont = try let (cl,u,args) = find_class_type env sigma t in - let (i, { cl_param = n1 } ) = class_info cl in + let { cl_param = n1 } = class_info cl in if not (Int.equal (List.length args) n1) then raise Not_found; - t, cont i + t, cont cl with Not_found -> (* Is it worth to be more incremental on the delta steps? *) let t = Tacred.hnf_constr env sigma t in let (cl, u, args) = find_class_type env sigma t in - let (i, { cl_param = n1 } ) = class_info cl in + let { cl_param = n1 } = class_info cl in if not (Int.equal (List.length args) n1) then raise Not_found; - t, cont i + t, cont cl let lookup_path_between env sigma (s,t) = let (s,(t,p)) = @@ -287,25 +240,25 @@ let get_coercion_constructor env coe = | _ -> raise Not_found let lookup_pattern_path_between env (s,t) = - let i = inductive_class_of s in - let j = inductive_class_of t in - List.map (get_coercion_constructor env) (ClPairMap.find (i,j) !inheritance_graph) + List.map (get_coercion_constructor env) + (ClPairMap.find (CL_IND s, CL_IND t) !inheritance_graph) (* rajouter une coercion dans le graphe *) -let path_printer : ((cl_index * cl_index) * inheritance_path -> Pp.t) ref = +let path_printer : ((cl_typ * cl_typ) * 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 -> cl_index -> inheritance_path -> inheritance_path -> bool) ref = +let path_comparator : + (Environ.env -> Evd.evar_map -> cl_typ -> 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 compare_path env sigma cl p q = !path_comparator env sigma cl p q let warn_ambiguous_path = CWarnings.create ~name:"ambiguous-paths" ~category:"typechecker" @@ -316,29 +269,29 @@ let warn_ambiguous_path = else str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l) -(* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit +(* add_coercion_in_graph : coe_index * cl_typ * cl_typ -> unit coercion,source,target *) -let different_class_params env i = - let ci = class_info_from_index i in - if (snd ci).cl_param > 0 then true - else - match fst ci with - | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i) - | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c) - | _ -> false +let different_class_params env ci = + if (class_info ci).cl_param > 0 then true + else + match ci with + | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i) + | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c) + | _ -> false let add_coercion_in_graph env sigma (ic,source,target) = 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_typ * cl_typ) * inheritance_path * inheritance_path) list ref = + 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 + if cl_typ_eq 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 + if not (cl_typ_eq 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 @@ -362,16 +315,16 @@ let add_coercion_in_graph env sigma (ic,source,target) = if try_add_new_path (source,target) [ic] then begin ClPairMap.iter (fun (s,t) p -> - if not (Bijint.Index.equal s t) then begin - if Bijint.Index.equal t source then begin + if not (cl_typ_eq s t) then begin + if cl_typ_eq t source then begin 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 then + if not (cl_typ_eq u v) && cl_typ_eq u target then try_add_new_path1 (s,v) (p@[ic]@q)) old_inheritance_graph end; - if Bijint.Index.equal s target then try_add_new_path1 (source,t) (ic::p) + if cl_typ_eq s target then try_add_new_path1 (source,t) (ic::p) end) old_inheritance_graph end; @@ -424,8 +377,6 @@ let add_class env sigma 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; @@ -434,12 +385,11 @@ 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 - -let classes () = Bijint.dom !class_tab +let classes () = + List.rev (ClTypMap.fold (fun x _ acc -> x :: acc) !class_tab []) let coercions () = List.rev (CoeTypMap.fold (fun _ y acc -> y::acc) !coercion_tab []) diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli index 073500b155..b7c46122a4 100644 --- a/pretyping/coercionops.mli +++ b/pretyping/coercionops.mli @@ -47,9 +47,6 @@ type coe_info_typ = { coe_param : int; } -(** [cl_index] is the type of class keys *) -type cl_index - (** This is the type of paths from a class to another *) type inheritance_path = coe_info_typ list @@ -57,20 +54,15 @@ type inheritance_path = coe_info_typ list val class_exists : cl_typ -> bool -val class_info : cl_typ -> (cl_index * cl_info_typ) (** @raise Not_found if this type is not a class *) - -val class_info_from_index : cl_index -> cl_typ * cl_info_typ +val class_info : cl_typ -> cl_info_typ (** [find_class_type env sigma c] returns the head reference of [c], its universe instance and its arguments *) val find_class_type : env -> evar_map -> types -> cl_typ * EInstance.t * constr list (** raises [Not_found] if not convertible to a class *) -val class_of : env -> evar_map -> types -> types * cl_index - -(** raises [Not_found] if not mapped to a class *) -val inductive_class_of : inductive -> cl_index +val class_of : env -> evar_map -> types -> types * cl_typ val class_args_of : env -> evar_map -> types -> constr list @@ -98,7 +90,7 @@ val coercion_info : coe_typ -> coe_info_typ (** @raise Not_found in the following functions when no path exists *) -val lookup_path_between_class : cl_index * cl_index -> inheritance_path +val lookup_path_between_class : cl_typ * cl_typ -> inheritance_path val lookup_path_between : env -> evar_map -> types * types -> types * types * inheritance_path val lookup_path_to_fun_from : env -> evar_map -> types -> @@ -111,16 +103,15 @@ val lookup_pattern_path_between : (**/**) (* Crade *) val install_path_printer : - ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit + ((cl_typ * cl_typ) * inheritance_path -> Pp.t) -> unit val install_path_comparator : - (env -> evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) -> unit + (env -> evar_map -> cl_typ -> inheritance_path -> inheritance_path -> bool) -> unit (**/**) (** {6 This is for printing purpose } *) val string_of_class : cl_typ -> string val pr_class : cl_typ -> Pp.t -val pr_cl_index : cl_index -> Pp.t -val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list +val inheritance_graph : unit -> ((cl_typ * cl_typ) * inheritance_path) list val classes : unit -> cl_typ list val coercions : unit -> coe_info_typ list diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e86a8a28c9..3ccc6ea125 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1398,7 +1398,7 @@ 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 i p q = +let path_convertible env sigma cl p q = let open Coercionops in let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in let mkGVar id = DAst.make @@ Glob_term.GVar(id) in @@ -1423,7 +1423,7 @@ let path_convertible env sigma i p q = p' | [] -> (* identity function for the class [i]. *) - let cl,params = class_info_from_index i in + let params = (class_info cl).cl_param in let clty = match cl with | CL_SORT -> mkGSort (Glob_term.UAnonymous {rigid=false}) @@ -1434,8 +1434,7 @@ let path_convertible env sigma i p q = | 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)) + List.init params (fun n -> Id.of_string ("x" ^ string_of_int n)) in List.fold_right (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@ diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out index ac5a09bad7..48368c7ede 100644 --- a/test-suite/output/relaxed_ambiguous_paths.out +++ b/test-suite/output/relaxed_ambiguous_paths.out @@ -3,32 +3,32 @@ Warning: New coercion path [ac; cd] : A >-> D is ambiguous with existing [ab; bd] : A >-> D. [ambiguous-paths,typechecker] [ab] : A >-> B -[ab; bd] : A >-> D [ac] : A >-> C +[ab; bd] : A >-> D [bd] : B >-> D [cd] : C >-> D File "stdin", line 26, characters 0-28: Warning: New coercion path [ab; bc] : A >-> C is ambiguous with existing [ac] : A >-> C. [ambiguous-paths,typechecker] +[ab] : A >-> B [ac] : A >-> C [ac; cd] : A >-> D -[ab] : A >-> B -[cd] : C >-> D [bc] : B >-> C [bc; cd] : B >-> D +[cd] : C >-> D [B_A] : B >-> A [C_A] : C >-> A -[D_B] : D >-> B [D_A] : D >-> A +[D_B] : D >-> B [D_C] : D >-> C [A'_A] : A' >-> A -[B_A'] : B >-> A' [B_A'; A'_A] : B >-> A -[C_A'] : C >-> A' +[B_A'] : B >-> A' [C_A'; A'_A] : C >-> A -[D_B; B_A'] : D >-> A' +[C_A'] : C >-> A' [D_A] : D >-> A +[D_B; B_A'] : D >-> A' [D_B] : D >-> B [D_C] : D >-> C File "stdin", line 121, characters 0-86: @@ -36,12 +36,12 @@ Warning: New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing [D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker] [A'_A] : A' >-> A -[B_A'] : B >-> A' [B_A'; A'_A] : B >-> A -[C_A'] : C >-> A' +[B_A'] : B >-> A' [C_A'; A'_A] : C >-> A -[D_B; B_A'] : D >-> A' +[C_A'] : C >-> A' [D_A] : D >-> A +[D_B; B_A'] : D >-> A' [D_B] : D >-> B [D_C] : D >-> C File "stdin", line 130, characters 0-47: diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 79a0cdf8d1..ec6e3b44ba 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -976,15 +976,11 @@ open Coercionops let print_coercion_value v = Printer.pr_global v.coe_value -let print_class i = - let cl,_ = class_info_from_index i in - pr_class cl - let print_path ((i,j),p) = hov 2 ( str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++ str"] : ") ++ - print_class i ++ str" >-> " ++ print_class j + pr_class i ++ str" >-> " ++ pr_class j let _ = Coercionops.install_path_printer print_path @@ -997,25 +993,16 @@ let print_classes () = let print_coercions () = pr_sequence print_coercion_value (coercions()) -let index_of_class cl = - try - fst (class_info cl) - with Not_found -> - user_err ~hdr:"index_of_class" - (pr_class cl ++ spc() ++ str "not a defined class.") - let print_path_between cls clt = - let i = index_of_class cls in - let j = index_of_class clt in let p = try - lookup_path_between_class (i,j) + lookup_path_between_class (cls, clt) with Not_found -> user_err ~hdr:"index_cl_of_id" (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") in - print_path ((i,j),p) + print_path ((cls, clt), p) let print_canonical_projections env sigma grefs = let match_proj_gref ((x,y),c) gr = |