From cc3ded87f0f440eac2746d59b7aeba60ca9f691f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 Dec 2019 11:41:33 +0100 Subject: Rename files with Class in their name to make their role clearer. We restrict to those that are actually related to typeclasses, and perform the following renamings: Classops --> Coercionops Class --> ComCoercion --- dev/base_include | 6 +- .../11293-ppedrot-rename-class-files.sh | 9 + dev/top_printers.ml | 2 +- dev/top_printers.mli | 2 +- interp/constrextern.ml | 2 +- interp/notation.ml | 2 +- interp/notation.mli | 2 +- plugins/firstorder/ground.ml | 4 +- plugins/ssr/ssrvernac.mlg | 6 +- pretyping/classops.ml | 479 --------------------- pretyping/classops.mli | 127 ------ pretyping/coercion.ml | 2 +- pretyping/coercionops.ml | 479 +++++++++++++++++++++ pretyping/coercionops.mli | 127 ++++++ pretyping/pretyping.ml | 4 +- pretyping/pretyping.mllib | 2 +- vernac/class.ml | 379 ---------------- vernac/class.mli | 53 --- vernac/comAssumption.ml | 4 +- vernac/comCoercion.ml | 379 ++++++++++++++++ vernac/comCoercion.mli | 53 +++ vernac/comInductive.ml | 2 +- vernac/prettyp.ml | 6 +- vernac/prettyp.mli | 2 +- vernac/record.ml | 6 +- vernac/vernac.mllib | 2 +- vernac/vernacentries.ml | 14 +- 27 files changed, 1082 insertions(+), 1073 deletions(-) create mode 100644 dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh delete mode 100644 pretyping/classops.ml delete mode 100644 pretyping/classops.mli create mode 100644 pretyping/coercionops.ml create mode 100644 pretyping/coercionops.mli delete mode 100644 vernac/class.ml delete mode 100644 vernac/class.mli create mode 100644 vernac/comCoercion.ml create mode 100644 vernac/comCoercion.mli diff --git a/dev/base_include b/dev/base_include index 4841db8953..96a867475d 100644 --- a/dev/base_include +++ b/dev/base_include @@ -60,11 +60,11 @@ open Cases open Pattern open Patternops open Cbv -open Classops +open Coercionops open Arguments_renaming open Pretyping open Cbv -open Classops +open Coercionops open Clenv open Clenvtac open Constr_matching @@ -134,7 +134,7 @@ open Tacticals open Tactics open Eqschemes -open Class +open ComCoercion open ComDefinition open Indschemes open Ind_tables diff --git a/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh b/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh new file mode 100644 index 0000000000..a95170a455 --- /dev/null +++ b/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "11293" ] || [ "$CI_BRANCH" = "rename-class-files" ]; then + + elpi_CI_REF=rename-class-files + elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi + + mtac2_CI_REF=rename-class-files + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + +fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f7f2bcdcff..835c20a4f7 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -47,7 +47,7 @@ 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(Classops.pr_cl_index cl) +let ppclindex cl = pp(Coercionops.pr_cl_index cl) let ppscheme k = pp (Ind_tables.pr_scheme_kind k) let prrecarg = function diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 5a2144f996..133326523b 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -29,7 +29,7 @@ val ppind : Names.inductive -> unit val ppsp : Libnames.full_path -> unit val ppqualid : Libnames.qualid -> unit -val ppclindex : Classops.cl_index -> unit +val ppclindex : Coercionops.cl_index -> unit val ppscheme : 'a Ind_tables.scheme_kind -> unit diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 28f4f5aed6..cc0c1e4602 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -678,7 +678,7 @@ let remove_one_coercion inctx c = try match match_coercion_app c with | Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) -> let nargs = List.length args in - (match Classops.hide_coercion r with + (match Coercionops.hide_coercion r with | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) -> (* We skip the coercion *) let l = List.skipn (n - pars) args in diff --git a/interp/notation.ml b/interp/notation.ml index 5dc1658824..93969f3718 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1430,7 +1430,7 @@ let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) (* Mapping classes to scopes *) -open Classops +open Coercionops type scope_class = cl_typ diff --git a/interp/notation.mli b/interp/notation.mli index 864e500d56..ea5125f7ec 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -271,7 +271,7 @@ val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option (** Get the current scope bound to Sortclass, if it exists *) val current_type_scope_name : unit -> scope_name option -val scope_class_of_class : Classops.cl_typ -> scope_class +val scope_class_of_class : Coercionops.cl_typ -> scope_class (** Building notation key *) diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 2f26226f4e..4e7482d4af 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -18,11 +18,11 @@ open Tacticals.New let update_flags ()= let open TransparentState in - let f accu coe = match coe.Classops.coe_value with + let f accu coe = match coe.Coercionops.coe_value with | Names.GlobRef.ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst } | _ -> accu in - let flags = List.fold_left f TransparentState.full (Classops.coercions ()) in + let flags = List.fold_left f TransparentState.full (Coercionops.coercions ()) in red_flags:= CClosure.RedFlags.red_add_transparent CClosure.betaiotazeta diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 9f6fe0e651..d8dbf2f3dc 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -370,14 +370,14 @@ let coerce_search_pattern_to_sort hpat = let filter_head, coe_path = try let _, cp = - Classops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in + Coercionops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in warn (); true, cp with _ -> false, [] in let coerce hp coe_index = - let coe_ref = coe_index.Classops.coe_value in + let coe_ref = coe_index.Coercionops.coe_value in try - let n_imps = Option.get (Classops.hide_coercion coe_ref) in + let n_imps = Option.get (Coercionops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] with Not_found | Option.IsNone -> errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc () diff --git a/pretyping/classops.ml b/pretyping/classops.ml deleted file mode 100644 index 16021b66f8..0000000000 --- a/pretyping/classops.ml +++ /dev/null @@ -1,479 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* 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_ord 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) - -module IntMap = Map.Make(Int) - -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) IntMap.t; s : int; inv : int ClTypMap.t } - let empty = { v = IntMap.empty; s = 0; inv = ClTypMap.empty } - let mem y b = ClTypMap.mem y b.inv - let map x b = IntMap.find x b.v - let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (IntMap.find n b.v)) - let add x y b = - { v = IntMap.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 - 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) - -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 - -let add_new_coercion coe s = - coercion_tab := CoeTypMap.add coe s !coercion_tab - -let add_new_path x y = - inheritance_graph := ClPairMap.add x y !inheritance_graph - -(* class_info : cl_typ -> int * cl_info_typ *) - -let class_info cl = Bijint.revmap 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) - -(* coercion_info : coe_typ -> coe_info_typ *) - -let coercion_info coe = CoeTypMap.find coe !coercion_tab - -let coercion_exists coe = CoeTypMap.mem coe !coercion_tab - -(* find_class_type : evar_map -> constr -> cl_typ * universe_list * constr list *) - -let find_class_type sigma t = - let open EConstr in - let t', args = Reductionops.whd_betaiotazeta_stack sigma t in - match EConstr.kind sigma t' with - | Var id -> CL_SECVAR id, EInstance.empty, args - | Const (sp,u) -> CL_CONST sp, u, args - | Proj (p, c) when not (Projection.unfolded p) -> - CL_PROJ (Projection.repr p), EInstance.empty, (c :: args) - | Ind (ind_sp,u) -> CL_IND ind_sp, u, args - | Prod _ -> CL_FUN, EInstance.empty, [] - | Sort _ -> CL_SORT, EInstance.empty, [] - | _ -> raise Not_found - - -let subst_cl_typ subst ct = match ct with - CL_SORT - | CL_FUN - | CL_SECVAR _ -> ct - | CL_PROJ c -> - let c' = subst_proj_repr subst c in - if c' == c then ct else CL_PROJ c' - | CL_CONST c -> - let c',t = subst_con subst c in - if c' == c then ct else (match t with - | None -> CL_CONST c' - | Some t -> - pi1 (find_class_type Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value))) - | CL_IND i -> - let i' = subst_ind subst i in - if i' == i then ct else CL_IND i' - -(*CSC: here we should change the datatype for coercions: it should be possible - to declare any term as a coercion *) -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) = - try - let (cl, u, args) = find_class_type sigma t in - let (i, { cl_param = n1 } ) = class_info cl in - (t, n1, i, u, args) - with Not_found -> - let t = Tacred.hnf_constr env sigma t in - let (cl, u, args) = find_class_type sigma t in - let (i, { cl_param = n1 } ) = class_info cl in - (t, n1, i, 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)) - -let class_args_of env sigma c = pi3 (find_class_type sigma c) - -let string_of_class = function - | CL_FUN -> "Funclass" - | CL_SORT -> "Sortclass" - | CL_CONST sp -> - string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.ConstRef sp)) - | CL_PROJ sp -> - let sp = Projection.Repr.constant sp in - string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.ConstRef sp)) - | CL_IND sp -> - string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.IndRef sp)) - | CL_SECVAR sp -> - string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.VarRef sp)) - -let pr_class x = str (string_of_class x) - -(* lookup paths *) - -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) - -let lookup_path_to_sort_from_class s = - lookup_path_between_class (s,cl_sort_index) - -(* advanced path lookup *) - -let apply_on_class_of env sigma t cont = - try - let (cl,u,args) = find_class_type sigma t in - let (i, { cl_param = n1 } ) = class_info cl in - if not (Int.equal (List.length args) n1) then raise Not_found; - t, cont i - 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 sigma t in - let (i, { cl_param = n1 } ) = class_info cl in - if not (Int.equal (List.length args) n1) then raise Not_found; - t, cont i - -let lookup_path_between env sigma (s,t) = - let (s,(t,p)) = - apply_on_class_of env sigma s (fun i -> - apply_on_class_of env sigma t (fun j -> - lookup_path_between_class (i,j))) in - (s,t,p) - -let lookup_path_to_fun_from env sigma s = - apply_on_class_of env sigma s lookup_path_to_fun_from_class - -let lookup_path_to_sort_from env sigma s = - apply_on_class_of env sigma s lookup_path_to_sort_from_class - -let mkNamed = let open GlobRef in function - | ConstRef c -> EConstr.mkConst c - | VarRef v -> EConstr.mkVar v - | ConstructRef c -> EConstr.mkConstruct c - | IndRef i -> EConstr.mkInd i - -let get_coercion_constructor env coe = - let evd = Evd.from_env env in - let red x = fst (Reductionops.whd_all_stack env evd x) in - match EConstr.kind evd (red (mkNamed coe.coe_value)) with - | Constr.Construct (c, _) -> - c, Inductiveops.constructor_nrealargs env c -1 - | _ -> 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) - -(* rajouter une coercion dans le graphe *) - -let path_printer : ((cl_index * cl_index) * inheritance_path -> Pp.t) ref = - ref (fun _ -> str "") - -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 = - 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 -> prlist_with_sep fnl (fun (c,p,q) -> - str"New coercion path " ++ print_path (c,p) ++ - 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 *) - -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 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 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 -> - (* 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) - else - false - in - let try_add_new_path1 ij p = - let _ = try_add_new_path ij p in () - in - 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 - 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 - 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) - end) - old_inheritance_graph - end; - match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths - -type coercion = { - coercion_type : coe_typ; - coercion_local : bool; - coercion_is_id : bool; - coercion_is_proj : Projection.Repr.t option; - coercion_source : cl_typ; - coercion_target : cl_typ; - coercion_params : int; -} - -let subst_coercion subst c = - let coe = subst_coe_typ subst c.coercion_type in - let cls = subst_cl_typ subst c.coercion_source in - let clt = subst_cl_typ subst c.coercion_target in - let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in - if c.coercion_type == coe && c.coercion_source == cls && - c.coercion_target == clt && c.coercion_is_proj == clp - then c - else { c with coercion_type = coe; coercion_source = cls; - coercion_target = clt; coercion_is_proj = clp; } - -(* Computation of the class arity *) - -let reference_arity_length env sigma ref = - let t, _ = Typeops.type_of_global_in_context env ref in - List.length (fst (Reductionops.splay_arity env sigma (EConstr.of_constr t))) - -let projection_arity_length env sigma p = - let len = reference_arity_length env sigma (GlobRef.ConstRef (Projection.Repr.constant p)) in - len - Projection.Repr.npars p - -let class_params env sigma = function - | CL_FUN | CL_SORT -> 0 - | CL_CONST sp -> reference_arity_length env sigma (GlobRef.ConstRef sp) - | CL_PROJ sp -> projection_arity_length env sigma sp - | CL_SECVAR sp -> reference_arity_length env sigma (GlobRef.VarRef sp) - | CL_IND sp -> reference_arity_length env sigma (GlobRef.IndRef sp) - -(* add_class : cl_typ -> locality_flag option -> bool -> unit *) - -let add_class env sigma cl = - add_new_class cl { cl_param = class_params 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; - coe_is_identity = c.coercion_is_id; - coe_is_projection = c.coercion_is_proj; - coe_param = c.coercion_params; - } in - let () = add_new_coercion c.coercion_type xf in - add_coercion_in_graph env sigma (xf,is,it) - -(* For printing purpose *) -let pr_cl_index = Bijint.Index.print - -let classes () = Bijint.dom !class_tab -let coercions () = - List.rev (CoeTypMap.fold (fun _ y acc -> y::acc) !coercion_tab []) - -let inheritance_graph () = - ClPairMap.bindings !inheritance_graph - -let coercion_of_reference r = - let ref = Nametab.global r in - if not (coercion_exists ref) then - user_err ~hdr:"try_add_coercion" - (Nametab.pr_global_env Id.Set.empty ref ++ str" is not a coercion."); - ref - -module CoercionPrinting = - struct - type t = coe_typ - module Set = GlobRef.Set - let encode _env = coercion_of_reference - let subst = subst_coe_typ - let printer x = Nametab.pr_global_env Id.Set.empty x - let key = ["Printing";"Coercion"] - let title = "Explicitly printed coercions: " - let member_message x b = - str "Explicit printing of coercion " ++ printer x ++ - str (if b then " is set" else " is unset") - end - -module PrintingCoercion = Goptions.MakeRefTable(CoercionPrinting) - -let hide_coercion coe = - if not (PrintingCoercion.active coe) then - let coe_info = coercion_info coe in - Some coe_info.coe_param - else None diff --git a/pretyping/classops.mli b/pretyping/classops.mli deleted file mode 100644 index 9f633843eb..0000000000 --- a/pretyping/classops.mli +++ /dev/null @@ -1,127 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* cl_typ -> bool - -val subst_cl_typ : substitution -> cl_typ -> cl_typ - -(** Comparison of [cl_typ] *) -val cl_typ_ord : cl_typ -> cl_typ -> int - -(** This is the type of infos for declared classes *) -type cl_info_typ = { - cl_param : int } - -(** This is the type of coercion kinds *) -type coe_typ = GlobRef.t - -(** This is the type of infos for declared coercions *) -type coe_info_typ = { - coe_value : GlobRef.t; - coe_local : bool; - coe_is_identity : bool; - coe_is_projection : Projection.Repr.t option; - 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 - -(** {6 Access to classes infos } *) - -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 - -(** [find_class_type env sigma c] returns the head reference of [c], - its universe instance and its arguments *) -val find_class_type : 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_args_of : env -> evar_map -> types -> constr list - -(** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *) -type coercion = { - coercion_type : coe_typ; - coercion_local : bool; - coercion_is_id : bool; - coercion_is_proj : Projection.Repr.t option; - coercion_source : cl_typ; - coercion_target : cl_typ; - coercion_params : int; -} - -val subst_coercion : substitution -> coercion -> coercion - -val declare_coercion : env -> evar_map -> coercion -> unit - -(** {6 Access to coercions infos } *) -val coercion_exists : coe_typ -> bool - -(** {6 Lookup functions for coercion paths } *) - -(** @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 : env -> evar_map -> types * types -> - types * types * inheritance_path -val lookup_path_to_fun_from : env -> evar_map -> types -> - types * inheritance_path -val lookup_path_to_sort_from : env -> evar_map -> types -> - types * inheritance_path -val lookup_pattern_path_between : - env -> inductive * inductive -> (constructor * int) list - -(**/**) -(* Crade *) -val install_path_printer : - ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit -val install_path_comparator : - (env -> evar_map -> cl_index -> 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 classes : unit -> cl_typ list -val coercions : unit -> coe_info_typ list - -(** [hide_coercion] returns the number of params to skip if the coercion must - be hidden, [None] otherwise; it raises [Not_found] if not a coercion *) -val hide_coercion : coe_typ -> int option diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index f0e73bdb29..c980d204ca 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -27,7 +27,7 @@ open EConstr open Vars open Reductionops open Pretype_errors -open Classops +open Coercionops open Evarutil open Evarconv open Evd diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml new file mode 100644 index 0000000000..16021b66f8 --- /dev/null +++ b/pretyping/coercionops.ml @@ -0,0 +1,479 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* 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_ord 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) + +module IntMap = Map.Make(Int) + +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) IntMap.t; s : int; inv : int ClTypMap.t } + let empty = { v = IntMap.empty; s = 0; inv = ClTypMap.empty } + let mem y b = ClTypMap.mem y b.inv + let map x b = IntMap.find x b.v + let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (IntMap.find n b.v)) + let add x y b = + { v = IntMap.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 + 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) + +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 + +let add_new_coercion coe s = + coercion_tab := CoeTypMap.add coe s !coercion_tab + +let add_new_path x y = + inheritance_graph := ClPairMap.add x y !inheritance_graph + +(* class_info : cl_typ -> int * cl_info_typ *) + +let class_info cl = Bijint.revmap 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) + +(* coercion_info : coe_typ -> coe_info_typ *) + +let coercion_info coe = CoeTypMap.find coe !coercion_tab + +let coercion_exists coe = CoeTypMap.mem coe !coercion_tab + +(* find_class_type : evar_map -> constr -> cl_typ * universe_list * constr list *) + +let find_class_type sigma t = + let open EConstr in + let t', args = Reductionops.whd_betaiotazeta_stack sigma t in + match EConstr.kind sigma t' with + | Var id -> CL_SECVAR id, EInstance.empty, args + | Const (sp,u) -> CL_CONST sp, u, args + | Proj (p, c) when not (Projection.unfolded p) -> + CL_PROJ (Projection.repr p), EInstance.empty, (c :: args) + | Ind (ind_sp,u) -> CL_IND ind_sp, u, args + | Prod _ -> CL_FUN, EInstance.empty, [] + | Sort _ -> CL_SORT, EInstance.empty, [] + | _ -> raise Not_found + + +let subst_cl_typ subst ct = match ct with + CL_SORT + | CL_FUN + | CL_SECVAR _ -> ct + | CL_PROJ c -> + let c' = subst_proj_repr subst c in + if c' == c then ct else CL_PROJ c' + | CL_CONST c -> + let c',t = subst_con subst c in + if c' == c then ct else (match t with + | None -> CL_CONST c' + | Some t -> + pi1 (find_class_type Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value))) + | CL_IND i -> + let i' = subst_ind subst i in + if i' == i then ct else CL_IND i' + +(*CSC: here we should change the datatype for coercions: it should be possible + to declare any term as a coercion *) +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) = + try + let (cl, u, args) = find_class_type sigma t in + let (i, { cl_param = n1 } ) = class_info cl in + (t, n1, i, u, args) + with Not_found -> + let t = Tacred.hnf_constr env sigma t in + let (cl, u, args) = find_class_type sigma t in + let (i, { cl_param = n1 } ) = class_info cl in + (t, n1, i, 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)) + +let class_args_of env sigma c = pi3 (find_class_type sigma c) + +let string_of_class = function + | CL_FUN -> "Funclass" + | CL_SORT -> "Sortclass" + | CL_CONST sp -> + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.ConstRef sp)) + | CL_PROJ sp -> + let sp = Projection.Repr.constant sp in + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.ConstRef sp)) + | CL_IND sp -> + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.IndRef sp)) + | CL_SECVAR sp -> + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.VarRef sp)) + +let pr_class x = str (string_of_class x) + +(* lookup paths *) + +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) + +let lookup_path_to_sort_from_class s = + lookup_path_between_class (s,cl_sort_index) + +(* advanced path lookup *) + +let apply_on_class_of env sigma t cont = + try + let (cl,u,args) = find_class_type sigma t in + let (i, { cl_param = n1 } ) = class_info cl in + if not (Int.equal (List.length args) n1) then raise Not_found; + t, cont i + 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 sigma t in + let (i, { cl_param = n1 } ) = class_info cl in + if not (Int.equal (List.length args) n1) then raise Not_found; + t, cont i + +let lookup_path_between env sigma (s,t) = + let (s,(t,p)) = + apply_on_class_of env sigma s (fun i -> + apply_on_class_of env sigma t (fun j -> + lookup_path_between_class (i,j))) in + (s,t,p) + +let lookup_path_to_fun_from env sigma s = + apply_on_class_of env sigma s lookup_path_to_fun_from_class + +let lookup_path_to_sort_from env sigma s = + apply_on_class_of env sigma s lookup_path_to_sort_from_class + +let mkNamed = let open GlobRef in function + | ConstRef c -> EConstr.mkConst c + | VarRef v -> EConstr.mkVar v + | ConstructRef c -> EConstr.mkConstruct c + | IndRef i -> EConstr.mkInd i + +let get_coercion_constructor env coe = + let evd = Evd.from_env env in + let red x = fst (Reductionops.whd_all_stack env evd x) in + match EConstr.kind evd (red (mkNamed coe.coe_value)) with + | Constr.Construct (c, _) -> + c, Inductiveops.constructor_nrealargs env c -1 + | _ -> 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) + +(* rajouter une coercion dans le graphe *) + +let path_printer : ((cl_index * cl_index) * inheritance_path -> Pp.t) ref = + ref (fun _ -> str "") + +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 = + 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 -> prlist_with_sep fnl (fun (c,p,q) -> + str"New coercion path " ++ print_path (c,p) ++ + 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 *) + +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 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 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 -> + (* 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) + else + false + in + let try_add_new_path1 ij p = + let _ = try_add_new_path ij p in () + in + 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 + 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 + 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) + end) + old_inheritance_graph + end; + match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths + +type coercion = { + coercion_type : coe_typ; + coercion_local : bool; + coercion_is_id : bool; + coercion_is_proj : Projection.Repr.t option; + coercion_source : cl_typ; + coercion_target : cl_typ; + coercion_params : int; +} + +let subst_coercion subst c = + let coe = subst_coe_typ subst c.coercion_type in + let cls = subst_cl_typ subst c.coercion_source in + let clt = subst_cl_typ subst c.coercion_target in + let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in + if c.coercion_type == coe && c.coercion_source == cls && + c.coercion_target == clt && c.coercion_is_proj == clp + then c + else { c with coercion_type = coe; coercion_source = cls; + coercion_target = clt; coercion_is_proj = clp; } + +(* Computation of the class arity *) + +let reference_arity_length env sigma ref = + let t, _ = Typeops.type_of_global_in_context env ref in + List.length (fst (Reductionops.splay_arity env sigma (EConstr.of_constr t))) + +let projection_arity_length env sigma p = + let len = reference_arity_length env sigma (GlobRef.ConstRef (Projection.Repr.constant p)) in + len - Projection.Repr.npars p + +let class_params env sigma = function + | CL_FUN | CL_SORT -> 0 + | CL_CONST sp -> reference_arity_length env sigma (GlobRef.ConstRef sp) + | CL_PROJ sp -> projection_arity_length env sigma sp + | CL_SECVAR sp -> reference_arity_length env sigma (GlobRef.VarRef sp) + | CL_IND sp -> reference_arity_length env sigma (GlobRef.IndRef sp) + +(* add_class : cl_typ -> locality_flag option -> bool -> unit *) + +let add_class env sigma cl = + add_new_class cl { cl_param = class_params 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; + coe_is_identity = c.coercion_is_id; + coe_is_projection = c.coercion_is_proj; + coe_param = c.coercion_params; + } in + let () = add_new_coercion c.coercion_type xf in + add_coercion_in_graph env sigma (xf,is,it) + +(* For printing purpose *) +let pr_cl_index = Bijint.Index.print + +let classes () = Bijint.dom !class_tab +let coercions () = + List.rev (CoeTypMap.fold (fun _ y acc -> y::acc) !coercion_tab []) + +let inheritance_graph () = + ClPairMap.bindings !inheritance_graph + +let coercion_of_reference r = + let ref = Nametab.global r in + if not (coercion_exists ref) then + user_err ~hdr:"try_add_coercion" + (Nametab.pr_global_env Id.Set.empty ref ++ str" is not a coercion."); + ref + +module CoercionPrinting = + struct + type t = coe_typ + module Set = GlobRef.Set + let encode _env = coercion_of_reference + let subst = subst_coe_typ + let printer x = Nametab.pr_global_env Id.Set.empty x + let key = ["Printing";"Coercion"] + let title = "Explicitly printed coercions: " + let member_message x b = + str "Explicit printing of coercion " ++ printer x ++ + str (if b then " is set" else " is unset") + end + +module PrintingCoercion = Goptions.MakeRefTable(CoercionPrinting) + +let hide_coercion coe = + if not (PrintingCoercion.active coe) then + let coe_info = coercion_info coe in + Some coe_info.coe_param + else None diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli new file mode 100644 index 0000000000..9f633843eb --- /dev/null +++ b/pretyping/coercionops.mli @@ -0,0 +1,127 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* cl_typ -> bool + +val subst_cl_typ : substitution -> cl_typ -> cl_typ + +(** Comparison of [cl_typ] *) +val cl_typ_ord : cl_typ -> cl_typ -> int + +(** This is the type of infos for declared classes *) +type cl_info_typ = { + cl_param : int } + +(** This is the type of coercion kinds *) +type coe_typ = GlobRef.t + +(** This is the type of infos for declared coercions *) +type coe_info_typ = { + coe_value : GlobRef.t; + coe_local : bool; + coe_is_identity : bool; + coe_is_projection : Projection.Repr.t option; + 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 + +(** {6 Access to classes infos } *) + +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 + +(** [find_class_type env sigma c] returns the head reference of [c], + its universe instance and its arguments *) +val find_class_type : 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_args_of : env -> evar_map -> types -> constr list + +(** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *) +type coercion = { + coercion_type : coe_typ; + coercion_local : bool; + coercion_is_id : bool; + coercion_is_proj : Projection.Repr.t option; + coercion_source : cl_typ; + coercion_target : cl_typ; + coercion_params : int; +} + +val subst_coercion : substitution -> coercion -> coercion + +val declare_coercion : env -> evar_map -> coercion -> unit + +(** {6 Access to coercions infos } *) +val coercion_exists : coe_typ -> bool + +(** {6 Lookup functions for coercion paths } *) + +(** @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 : env -> evar_map -> types * types -> + types * types * inheritance_path +val lookup_path_to_fun_from : env -> evar_map -> types -> + types * inheritance_path +val lookup_path_to_sort_from : env -> evar_map -> types -> + types * inheritance_path +val lookup_pattern_path_between : + env -> inductive * inductive -> (constructor * int) list + +(**/**) +(* Crade *) +val install_path_printer : + ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit +val install_path_comparator : + (env -> evar_map -> cl_index -> 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 classes : unit -> cl_typ list +val coercions : unit -> coe_info_typ list + +(** [hide_coercion] returns the number of params to skip if the coercion must + be hidden, [None] otherwise; it raises [Not_found] if not a coercion *) +val hide_coercion : coe_typ -> int option diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0364e1b61f..bfdb471c46 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1326,7 +1326,7 @@ let understand_ltac flags env sigma lvar kind c = (sigma, c) let path_convertible env sigma i p q = - let open Classops in + 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 let mkGApp(rt,rtl) = DAst.make @@ Glob_term.GApp(rt,rtl) in @@ -1379,4 +1379,4 @@ let path_convertible env sigma i p q = let _ = Evarconv.unify_delay env sigma tp tq in true with Evarconv.UnableToUnify _ | PretypeError _ -> false -let _ = Classops.install_path_comparator path_convertible +let _ = Coercionops.install_path_comparator path_convertible diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 7e140f4399..07154d4e03 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -26,7 +26,7 @@ Constr_matching Tacred Typeclasses_errors Typeclasses -Classops +Coercionops Program Coercion Detyping diff --git a/vernac/class.ml b/vernac/class.ml deleted file mode 100644 index 3c43b125d1..0000000000 --- a/vernac/class.ml +++ /dev/null @@ -1,379 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* - (Printer.pr_global g ++ str" is already a coercion") - | NotAFunction -> - (Printer.pr_global g ++ str" is not a function") - | NoSource (Some cl) -> - (str "Cannot recognize " ++ pr_class cl ++ str " as a source class of " - ++ Printer.pr_global g) - | NoSource None -> - (str ": cannot find the source class of " ++ Printer.pr_global g) - | ForbiddenSourceClass cl -> - pr_class cl ++ str " cannot be a source class" - | NoTarget -> - (str"Cannot find the target class") - | WrongTarget (clt,cl) -> - (str"Found target class " ++ pr_class cl ++ - str " instead of " ++ pr_class clt) - | NotAClass ref -> - (str "Type of " ++ Printer.pr_global ref ++ - str " does not end with a sort") - -(* Verifications pour l'ajout d'une classe *) - -let check_reference_arity ref = - let env = Global.env () in - let c, _ = Typeops.type_of_global_in_context env ref in - if not (Reductionops.is_arity env (Evd.from_env env) (EConstr.of_constr c)) (* FIXME *) then - raise (CoercionError (NotAClass ref)) - -let check_arity = function - | CL_FUN | CL_SORT -> () - | CL_CONST cst -> check_reference_arity (GlobRef.ConstRef cst) - | CL_PROJ p -> check_reference_arity (GlobRef.ConstRef (Projection.Repr.constant p)) - | CL_SECVAR id -> check_reference_arity (GlobRef.VarRef id) - | CL_IND kn -> check_reference_arity (GlobRef.IndRef kn) - -(* Coercions *) - -(* check that the computed target is the provided one *) -let check_target clt = function - | Some cl when not (cl_typ_eq cl clt) -> raise (CoercionError (WrongTarget(clt,cl))) - | _ -> () - -(* condition d'heritage uniforme *) - -let uniform_cond sigma ctx lt = - List.for_all2eq (EConstr.eq_constr sigma) - lt (Context.Rel.to_extended_list EConstr.mkRel 0 ctx) - -let class_of_global = function - | GlobRef.ConstRef sp -> - (match Recordops.find_primitive_projection sp with - | Some p -> CL_PROJ p | None -> CL_CONST sp) - | GlobRef.IndRef sp -> CL_IND sp - | GlobRef.VarRef id -> CL_SECVAR id - | GlobRef.ConstructRef _ as c -> - user_err ~hdr:"class_of_global" - (str "Constructors, such as " ++ Printer.pr_global c ++ - str ", cannot be used as a class.") - -(* -lp est la liste (inverse'e) des arguments de la coercion -ids est le nom de la classe source -sps_opt est le sp de la classe source dans le cas des structures -retourne: -la classe source -nbre d'arguments de la classe -le constr de la class -la liste des variables dont depend la classe source -l'indice de la classe source dans la liste lp -*) - -let get_source lp source = - let open Context.Rel.Declaration in - match source with - | None -> - (* Take the latest non let-in argument *) - let rec aux = function - | [] -> raise Not_found - | LocalDef _ :: lt -> aux lt - | LocalAssum (_,t1) :: lt -> - let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in - cl1,lt,lv1,1 - in aux lp - | Some cl -> - (* Take the first argument that matches *) - let rec aux acc = function - | [] -> raise Not_found - | LocalDef _ as decl :: lt -> aux (decl::acc) lt - | LocalAssum (_,t1) as decl :: lt -> - try - let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in - if cl_typ_eq cl cl1 then cl1,acc,lv1,Context.Rel.nhyps lt+1 - else raise Not_found - with Not_found -> aux (decl::acc) lt - in aux [] (List.rev lp) - -let get_target t ind = - if (ind > 1) then - CL_FUN - else - match pi1 (find_class_type Evd.empty (EConstr.of_constr t)) with - | CL_CONST p when Recordops.is_primitive_projection p -> - CL_PROJ (Option.get @@ Recordops.find_primitive_projection p) - | x -> x - -let strength_of_cl = function - | CL_CONST kn -> `GLOBAL - | CL_SECVAR id -> `LOCAL - | _ -> `GLOBAL - -let strength_of_global = function - | GlobRef.VarRef _ -> `LOCAL - | _ -> `GLOBAL - -let get_strength stre ref cls clt = - let stres = strength_of_cl cls in - let stret = strength_of_cl clt in - let stref = strength_of_global ref in - strength_min [stre;stres;stret;stref] - -let ident_key_of_class = function - | CL_FUN -> "Funclass" - | CL_SORT -> "Sortclass" - | CL_CONST sp -> Label.to_string (Constant.label sp) - | CL_PROJ sp -> Label.to_string (Projection.Repr.label sp) - | CL_IND (sp,_) -> Label.to_string (MutInd.label sp) - | CL_SECVAR id -> Id.to_string id - -(* Identity coercion *) - -let error_not_transparent source = - user_err ~hdr:"build_id_coercion" - (pr_class source ++ str " must be a transparent constant.") - -let build_id_coercion idf_opt source poly = - let env = Global.env () in - let sigma = Evd.from_env env in - let sigma, vs = match source with - | CL_CONST sp -> Evd.fresh_global env sigma (GlobRef.ConstRef sp) - | _ -> error_not_transparent source in - let vs = EConstr.Unsafe.to_constr vs in - let c = match constant_opt_value_in env (destConst vs) with - | Some c -> c - | None -> error_not_transparent source in - let lams,t = decompose_lam_assum c in - let val_f = - it_mkLambda_or_LetIn - (mkLambda (make_annot (Name Namegen.default_dependent_ident) Sorts.Relevant, - applistc vs (Context.Rel.to_extended_list mkRel 0 lams), - mkRel 1)) - lams - in - let typ_f = - List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d) - (mkProd (make_annot Anonymous Sorts.Relevant, applistc vs (Context.Rel.to_extended_list mkRel 0 lams), lift 1 t)) - lams - in - (* juste pour verification *) - let _ = - if not - (Reductionops.is_conv_leq env sigma - (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f)) (EConstr.of_constr typ_f)) - then - user_err (strbrk - "Cannot be defined as coercion (maybe a bad number of arguments).") - in - let name = - match idf_opt with - | Some idf -> idf - | None -> - let cl,u,_ = find_class_type sigma (EConstr.of_constr t) in - Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ - (ident_key_of_class cl)) - in - let univs = Evd.univ_entry ~poly sigma in - let constr_entry = (* Cast is necessary to express [val_f] is identity *) - DefinitionEntry - (definition_entry ~types:typ_f ~univs - ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) - in - let kind = Decls.(IsDefinition IdentityCoercion) in - let kn = declare_constant ~name ~kind constr_entry in - GlobRef.ConstRef kn - -let check_source = function -| Some (CL_FUN as s) -> raise (CoercionError (ForbiddenSourceClass s)) -| _ -> () - -let cache_coercion (_,c) = - let env = Global.env () in - let sigma = Evd.from_env env in - Classops.declare_coercion env sigma c - -let open_coercion i o = - if Int.equal i 1 then - cache_coercion o - -let discharge_coercion (_, c) = - if c.coercion_local then None - else - let n = - try - let ins = Lib.section_instance c.coercion_type in - Array.length (snd ins) - with Not_found -> 0 - in - let nc = { c with - coercion_params = n + c.coercion_params; - coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj; - } in - Some nc - -let classify_coercion obj = - if obj.coercion_local then Dispose else Substitute obj - -let inCoercion : coercion -> obj = - declare_object {(default_object "COERCION") with - open_function = open_coercion; - cache_function = cache_coercion; - subst_function = (fun (subst,c) -> subst_coercion subst c); - classify_function = classify_coercion; - discharge_function = discharge_coercion } - -let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps = - let isproj = - match coef with - | GlobRef.ConstRef c -> Recordops.find_primitive_projection c - | _ -> None - in - let c = { - coercion_type = coef; - coercion_local = local; - coercion_is_id = isid; - coercion_is_proj = isproj; - coercion_source = cls; - coercion_target = clt; - coercion_params = ps; - } in - Lib.add_anonymous_leaf (inCoercion c) - -(* -nom de la fonction coercion -strength de f -nom de la classe source (optionnel) -sp de la classe source (dans le cas des structures) -nom de la classe target (optionnel) -booleen "coercion identite'?" - -lorque source est None alors target est None aussi. -*) - -let warn_uniform_inheritance = - CWarnings.create ~name:"uniform-inheritance" ~category:"typechecker" - (fun g -> - Printer.pr_global g ++ - strbrk" does not respect the uniform inheritance condition") - -let add_new_coercion_core coef stre poly source target isid = - check_source source; - let t, _ = Typeops.type_of_global_in_context (Global.env ()) coef in - if coercion_exists coef then raise (CoercionError AlreadyExists); - let lp,tg = decompose_prod_assum t in - let llp = List.length lp in - if Int.equal llp 0 then raise (CoercionError NotAFunction); - let (cls,ctx,lvs,ind) = - try - get_source lp source - with Not_found -> - raise (CoercionError (NoSource source)) - in - check_source (Some cls); - if not (uniform_cond Evd.empty (* FIXME - for when possibly called with unresolved evars in the future *) - ctx lvs) then - warn_uniform_inheritance coef; - let clt = - try - get_target tg ind - with Not_found -> - raise (CoercionError NoTarget) - in - check_target clt target; - check_arity cls; - check_arity clt; - let local = match get_strength stre coef cls clt with - | `LOCAL -> true - | `GLOBAL -> false - in - declare_coercion coef ~local ~isid ~src:cls ~target:clt ~params:(List.length lvs) - - -let try_add_new_coercion_core ref ~local c d e f = - try add_new_coercion_core ref (loc_of_bool local) c d e f - with CoercionError e -> - user_err ~hdr:"try_add_new_coercion_core" - (explain_coercion_error ref e ++ str ".") - -let try_add_new_coercion ref ~local ~poly = - try_add_new_coercion_core ref ~local poly None None false - -let try_add_new_coercion_subclass cl ~local ~poly = - let coe_ref = build_id_coercion None cl poly in - try_add_new_coercion_core coe_ref ~local poly (Some cl) None true - -let try_add_new_coercion_with_target ref ~local ~poly ~source ~target = - try_add_new_coercion_core ref ~local poly (Some source) (Some target) false - -let try_add_new_identity_coercion id ~local ~poly ~source ~target = - let ref = build_id_coercion (Some id) source poly in - try_add_new_coercion_core ref ~local poly (Some source) (Some target) true - -let try_add_new_coercion_with_source ref ~local ~poly ~source = - try_add_new_coercion_core ref ~local poly (Some source) None false - -let add_coercion_hook poly { DeclareDef.Hook.S.scope; dref; _ } = - let open DeclareDef in - let local = match scope with - | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *) - | Global ImportNeedQualified -> true - | Global ImportDefaultBehavior -> false - in - let () = try_add_new_coercion dref ~local ~poly in - let msg = Nametab.pr_global_env Id.Set.empty dref ++ str " is now a coercion" in - Flags.if_verbose Feedback.msg_info msg - -let add_coercion_hook ~poly = DeclareDef.Hook.make (add_coercion_hook poly) - -let add_subclass_hook ~poly { DeclareDef.Hook.S.scope; dref; _ } = - let open DeclareDef in - let stre = match scope with - | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *) - | Global ImportNeedQualified -> true - | Global ImportDefaultBehavior -> false - in - let cl = class_of_global dref in - try_add_new_coercion_subclass cl ~local:stre ~poly - -let add_subclass_hook ~poly = DeclareDef.Hook.make (add_subclass_hook ~poly) diff --git a/vernac/class.mli b/vernac/class.mli deleted file mode 100644 index 3254d5d981..0000000000 --- a/vernac/class.mli +++ /dev/null @@ -1,53 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* local:bool - -> poly:bool - -> source:cl_typ - -> target:cl_typ - -> unit - -(** [try_add_new_coercion ref s] declares [ref], assumed to be of type - [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *) -val try_add_new_coercion : GlobRef.t -> local:bool -> poly:bool -> unit - -(** [try_add_new_coercion_subclass cst s] expects that [cst] denotes a - transparent constant which unfolds to some class [tg]; it declares - an identity coercion from [cst] to [tg], named something like - ["Id_cst_tg"] *) -val try_add_new_coercion_subclass : cl_typ -> local:bool -> poly:bool -> unit - -(** [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion - from [src] to [tg] where the target is inferred from the type of [ref] *) -val try_add_new_coercion_with_source : GlobRef.t -> local:bool -> - poly:bool -> source:cl_typ -> unit - -(** [try_add_new_identity_coercion id s src tg] enriches the - environment with a new definition of name [id] declared as an - identity coercion from [src] to [tg] *) -val try_add_new_identity_coercion - : Id.t - -> local:bool - -> poly:bool -> source:cl_typ -> target:cl_typ -> unit - -val add_coercion_hook : poly:bool -> DeclareDef.Hook.t - -val add_subclass_hook : poly:bool -> DeclareDef.Hook.t - -val class_of_global : GlobRef.t -> cl_typ diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 8a403e5a03..625ffb5a06 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -32,7 +32,7 @@ let declare_variable is_coe ~kind typ imps impl {CAst.v=name} = let env = Global.env () in let sigma = Evd.from_env env in let () = Classes.declare_instance env sigma None true r in - let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in + let () = if is_coe then ComCoercion.try_add_new_coercion r ~local:true ~poly:false in () let instance_of_univ_entry = function @@ -65,7 +65,7 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name | Declare.ImportNeedQualified -> true | Declare.ImportDefaultBehavior -> false in - let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in + let () = if is_coe then ComCoercion.try_add_new_coercion gr ~local ~poly in let inst = instance_of_univ_entry univs in (gr,inst) diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml new file mode 100644 index 0000000000..56ab6f289d --- /dev/null +++ b/vernac/comCoercion.ml @@ -0,0 +1,379 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* + (Printer.pr_global g ++ str" is already a coercion") + | NotAFunction -> + (Printer.pr_global g ++ str" is not a function") + | NoSource (Some cl) -> + (str "Cannot recognize " ++ pr_class cl ++ str " as a source class of " + ++ Printer.pr_global g) + | NoSource None -> + (str ": cannot find the source class of " ++ Printer.pr_global g) + | ForbiddenSourceClass cl -> + pr_class cl ++ str " cannot be a source class" + | NoTarget -> + (str"Cannot find the target class") + | WrongTarget (clt,cl) -> + (str"Found target class " ++ pr_class cl ++ + str " instead of " ++ pr_class clt) + | NotAClass ref -> + (str "Type of " ++ Printer.pr_global ref ++ + str " does not end with a sort") + +(* Verifications pour l'ajout d'une classe *) + +let check_reference_arity ref = + let env = Global.env () in + let c, _ = Typeops.type_of_global_in_context env ref in + if not (Reductionops.is_arity env (Evd.from_env env) (EConstr.of_constr c)) (* FIXME *) then + raise (CoercionError (NotAClass ref)) + +let check_arity = function + | CL_FUN | CL_SORT -> () + | CL_CONST cst -> check_reference_arity (GlobRef.ConstRef cst) + | CL_PROJ p -> check_reference_arity (GlobRef.ConstRef (Projection.Repr.constant p)) + | CL_SECVAR id -> check_reference_arity (GlobRef.VarRef id) + | CL_IND kn -> check_reference_arity (GlobRef.IndRef kn) + +(* Coercions *) + +(* check that the computed target is the provided one *) +let check_target clt = function + | Some cl when not (cl_typ_eq cl clt) -> raise (CoercionError (WrongTarget(clt,cl))) + | _ -> () + +(* condition d'heritage uniforme *) + +let uniform_cond sigma ctx lt = + List.for_all2eq (EConstr.eq_constr sigma) + lt (Context.Rel.to_extended_list EConstr.mkRel 0 ctx) + +let class_of_global = function + | GlobRef.ConstRef sp -> + (match Recordops.find_primitive_projection sp with + | Some p -> CL_PROJ p | None -> CL_CONST sp) + | GlobRef.IndRef sp -> CL_IND sp + | GlobRef.VarRef id -> CL_SECVAR id + | GlobRef.ConstructRef _ as c -> + user_err ~hdr:"class_of_global" + (str "Constructors, such as " ++ Printer.pr_global c ++ + str ", cannot be used as a class.") + +(* +lp est la liste (inverse'e) des arguments de la coercion +ids est le nom de la classe source +sps_opt est le sp de la classe source dans le cas des structures +retourne: +la classe source +nbre d'arguments de la classe +le constr de la class +la liste des variables dont depend la classe source +l'indice de la classe source dans la liste lp +*) + +let get_source lp source = + let open Context.Rel.Declaration in + match source with + | None -> + (* Take the latest non let-in argument *) + let rec aux = function + | [] -> raise Not_found + | LocalDef _ :: lt -> aux lt + | LocalAssum (_,t1) :: lt -> + let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in + cl1,lt,lv1,1 + in aux lp + | Some cl -> + (* Take the first argument that matches *) + let rec aux acc = function + | [] -> raise Not_found + | LocalDef _ as decl :: lt -> aux (decl::acc) lt + | LocalAssum (_,t1) as decl :: lt -> + try + let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in + if cl_typ_eq cl cl1 then cl1,acc,lv1,Context.Rel.nhyps lt+1 + else raise Not_found + with Not_found -> aux (decl::acc) lt + in aux [] (List.rev lp) + +let get_target t ind = + if (ind > 1) then + CL_FUN + else + match pi1 (find_class_type Evd.empty (EConstr.of_constr t)) with + | CL_CONST p when Recordops.is_primitive_projection p -> + CL_PROJ (Option.get @@ Recordops.find_primitive_projection p) + | x -> x + +let strength_of_cl = function + | CL_CONST kn -> `GLOBAL + | CL_SECVAR id -> `LOCAL + | _ -> `GLOBAL + +let strength_of_global = function + | GlobRef.VarRef _ -> `LOCAL + | _ -> `GLOBAL + +let get_strength stre ref cls clt = + let stres = strength_of_cl cls in + let stret = strength_of_cl clt in + let stref = strength_of_global ref in + strength_min [stre;stres;stret;stref] + +let ident_key_of_class = function + | CL_FUN -> "Funclass" + | CL_SORT -> "Sortclass" + | CL_CONST sp -> Label.to_string (Constant.label sp) + | CL_PROJ sp -> Label.to_string (Projection.Repr.label sp) + | CL_IND (sp,_) -> Label.to_string (MutInd.label sp) + | CL_SECVAR id -> Id.to_string id + +(* Identity coercion *) + +let error_not_transparent source = + user_err ~hdr:"build_id_coercion" + (pr_class source ++ str " must be a transparent constant.") + +let build_id_coercion idf_opt source poly = + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma, vs = match source with + | CL_CONST sp -> Evd.fresh_global env sigma (GlobRef.ConstRef sp) + | _ -> error_not_transparent source in + let vs = EConstr.Unsafe.to_constr vs in + let c = match constant_opt_value_in env (destConst vs) with + | Some c -> c + | None -> error_not_transparent source in + let lams,t = decompose_lam_assum c in + let val_f = + it_mkLambda_or_LetIn + (mkLambda (make_annot (Name Namegen.default_dependent_ident) Sorts.Relevant, + applistc vs (Context.Rel.to_extended_list mkRel 0 lams), + mkRel 1)) + lams + in + let typ_f = + List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d) + (mkProd (make_annot Anonymous Sorts.Relevant, applistc vs (Context.Rel.to_extended_list mkRel 0 lams), lift 1 t)) + lams + in + (* juste pour verification *) + let _ = + if not + (Reductionops.is_conv_leq env sigma + (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f)) (EConstr.of_constr typ_f)) + then + user_err (strbrk + "Cannot be defined as coercion (maybe a bad number of arguments).") + in + let name = + match idf_opt with + | Some idf -> idf + | None -> + let cl,u,_ = find_class_type sigma (EConstr.of_constr t) in + Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ + (ident_key_of_class cl)) + in + let univs = Evd.univ_entry ~poly sigma in + let constr_entry = (* Cast is necessary to express [val_f] is identity *) + DefinitionEntry + (definition_entry ~types:typ_f ~univs + ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) + in + let kind = Decls.(IsDefinition IdentityCoercion) in + let kn = declare_constant ~name ~kind constr_entry in + GlobRef.ConstRef kn + +let check_source = function +| Some (CL_FUN as s) -> raise (CoercionError (ForbiddenSourceClass s)) +| _ -> () + +let cache_coercion (_,c) = + let env = Global.env () in + let sigma = Evd.from_env env in + Coercionops.declare_coercion env sigma c + +let open_coercion i o = + if Int.equal i 1 then + cache_coercion o + +let discharge_coercion (_, c) = + if c.coercion_local then None + else + let n = + try + let ins = Lib.section_instance c.coercion_type in + Array.length (snd ins) + with Not_found -> 0 + in + let nc = { c with + coercion_params = n + c.coercion_params; + coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj; + } in + Some nc + +let classify_coercion obj = + if obj.coercion_local then Dispose else Substitute obj + +let inCoercion : coercion -> obj = + declare_object {(default_object "COERCION") with + open_function = open_coercion; + cache_function = cache_coercion; + subst_function = (fun (subst,c) -> subst_coercion subst c); + classify_function = classify_coercion; + discharge_function = discharge_coercion } + +let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps = + let isproj = + match coef with + | GlobRef.ConstRef c -> Recordops.find_primitive_projection c + | _ -> None + in + let c = { + coercion_type = coef; + coercion_local = local; + coercion_is_id = isid; + coercion_is_proj = isproj; + coercion_source = cls; + coercion_target = clt; + coercion_params = ps; + } in + Lib.add_anonymous_leaf (inCoercion c) + +(* +nom de la fonction coercion +strength de f +nom de la classe source (optionnel) +sp de la classe source (dans le cas des structures) +nom de la classe target (optionnel) +booleen "coercion identite'?" + +lorque source est None alors target est None aussi. +*) + +let warn_uniform_inheritance = + CWarnings.create ~name:"uniform-inheritance" ~category:"typechecker" + (fun g -> + Printer.pr_global g ++ + strbrk" does not respect the uniform inheritance condition") + +let add_new_coercion_core coef stre poly source target isid = + check_source source; + let t, _ = Typeops.type_of_global_in_context (Global.env ()) coef in + if coercion_exists coef then raise (CoercionError AlreadyExists); + let lp,tg = decompose_prod_assum t in + let llp = List.length lp in + if Int.equal llp 0 then raise (CoercionError NotAFunction); + let (cls,ctx,lvs,ind) = + try + get_source lp source + with Not_found -> + raise (CoercionError (NoSource source)) + in + check_source (Some cls); + if not (uniform_cond Evd.empty (* FIXME - for when possibly called with unresolved evars in the future *) + ctx lvs) then + warn_uniform_inheritance coef; + let clt = + try + get_target tg ind + with Not_found -> + raise (CoercionError NoTarget) + in + check_target clt target; + check_arity cls; + check_arity clt; + let local = match get_strength stre coef cls clt with + | `LOCAL -> true + | `GLOBAL -> false + in + declare_coercion coef ~local ~isid ~src:cls ~target:clt ~params:(List.length lvs) + + +let try_add_new_coercion_core ref ~local c d e f = + try add_new_coercion_core ref (loc_of_bool local) c d e f + with CoercionError e -> + user_err ~hdr:"try_add_new_coercion_core" + (explain_coercion_error ref e ++ str ".") + +let try_add_new_coercion ref ~local ~poly = + try_add_new_coercion_core ref ~local poly None None false + +let try_add_new_coercion_subclass cl ~local ~poly = + let coe_ref = build_id_coercion None cl poly in + try_add_new_coercion_core coe_ref ~local poly (Some cl) None true + +let try_add_new_coercion_with_target ref ~local ~poly ~source ~target = + try_add_new_coercion_core ref ~local poly (Some source) (Some target) false + +let try_add_new_identity_coercion id ~local ~poly ~source ~target = + let ref = build_id_coercion (Some id) source poly in + try_add_new_coercion_core ref ~local poly (Some source) (Some target) true + +let try_add_new_coercion_with_source ref ~local ~poly ~source = + try_add_new_coercion_core ref ~local poly (Some source) None false + +let add_coercion_hook poly { DeclareDef.Hook.S.scope; dref; _ } = + let open DeclareDef in + let local = match scope with + | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *) + | Global ImportNeedQualified -> true + | Global ImportDefaultBehavior -> false + in + let () = try_add_new_coercion dref ~local ~poly in + let msg = Nametab.pr_global_env Id.Set.empty dref ++ str " is now a coercion" in + Flags.if_verbose Feedback.msg_info msg + +let add_coercion_hook ~poly = DeclareDef.Hook.make (add_coercion_hook poly) + +let add_subclass_hook ~poly { DeclareDef.Hook.S.scope; dref; _ } = + let open DeclareDef in + let stre = match scope with + | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *) + | Global ImportNeedQualified -> true + | Global ImportDefaultBehavior -> false + in + let cl = class_of_global dref in + try_add_new_coercion_subclass cl ~local:stre ~poly + +let add_subclass_hook ~poly = DeclareDef.Hook.make (add_subclass_hook ~poly) diff --git a/vernac/comCoercion.mli b/vernac/comCoercion.mli new file mode 100644 index 0000000000..f98ef4fdd6 --- /dev/null +++ b/vernac/comCoercion.mli @@ -0,0 +1,53 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* local:bool + -> poly:bool + -> source:cl_typ + -> target:cl_typ + -> unit + +(** [try_add_new_coercion ref s] declares [ref], assumed to be of type + [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *) +val try_add_new_coercion : GlobRef.t -> local:bool -> poly:bool -> unit + +(** [try_add_new_coercion_subclass cst s] expects that [cst] denotes a + transparent constant which unfolds to some class [tg]; it declares + an identity coercion from [cst] to [tg], named something like + ["Id_cst_tg"] *) +val try_add_new_coercion_subclass : cl_typ -> local:bool -> poly:bool -> unit + +(** [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion + from [src] to [tg] where the target is inferred from the type of [ref] *) +val try_add_new_coercion_with_source : GlobRef.t -> local:bool -> + poly:bool -> source:cl_typ -> unit + +(** [try_add_new_identity_coercion id s src tg] enriches the + environment with a new definition of name [id] declared as an + identity coercion from [src] to [tg] *) +val try_add_new_identity_coercion + : Id.t + -> local:bool + -> poly:bool -> source:cl_typ -> target:cl_typ -> unit + +val add_coercion_hook : poly:bool -> DeclareDef.Hook.t + +val add_subclass_hook : poly:bool -> DeclareDef.Hook.t + +val class_of_global : GlobRef.t -> cl_typ diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index b603c54026..8de1c69424 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -553,7 +553,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes + List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index eb7b28f15b..d04a02febc 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -199,7 +199,7 @@ let print_opacity ref = (*******************) let print_if_is_coercion ref = - if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else [] + if Coercionops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else [] (*******************) (* *) @@ -951,7 +951,7 @@ let inspect env sigma depth = (*************************************************************************) (* Pretty-printing functions coming from classops.ml *) -open Classops +open Coercionops let print_coercion_value v = Printer.pr_global v.coe_value @@ -965,7 +965,7 @@ let print_path ((i,j),p) = str"] : ") ++ print_class i ++ str" >-> " ++ print_class j -let _ = Classops.install_path_printer print_path +let _ = Coercionops.install_path_printer print_path let print_graph () = prlist_with_sep fnl print_path (inheritance_graph()) diff --git a/vernac/prettyp.mli b/vernac/prettyp.mli index dc4280f286..2ee9c4ed33 100644 --- a/vernac/prettyp.mli +++ b/vernac/prettyp.mli @@ -52,7 +52,7 @@ val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t val print_graph : unit -> Pp.t val print_classes : unit -> Pp.t val print_coercions : unit -> Pp.t -val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t +val print_path_between : Coercionops.cl_typ -> Coercionops.cl_typ -> Pp.t val print_canonical_projections : env -> Evd.evar_map -> Pp.t (** Pretty-printing functions for type classes and instances *) diff --git a/vernac/record.ml b/vernac/record.ml index ea10e06d02..df9b4a0914 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -366,8 +366,8 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f let refi = GlobRef.ConstRef kn in Impargs.maybe_declare_manual_implicits false refi impls; if flags.pf_subclass then begin - let cl = Class.class_of_global (GlobRef.IndRef indsp) in - Class.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl + let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in + ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl end; let i = if is_local_assum decl then i+1 else i in (Some kn::sp_projs, i, Projection term::subst) @@ -489,7 +489,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let cstr = (rsp, 1) in let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in let build = GlobRef.ConstructRef cstr in - let () = if is_coe then Class.try_add_new_coercion build ~local:false ~poly in + let () = if is_coe then ComCoercion.try_add_new_coercion build ~local:false ~poly in let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in rsp in diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 5226c2ba65..7b4924eaed 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -21,7 +21,7 @@ RecLemmas Library Prettyp Lemmas -Class +ComCoercion Auto_ind_decl Search Indschemes diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 439ec61d38..604d1b28ff 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -49,9 +49,9 @@ let get_goal_or_global_context ~pstate glnum = | Some p -> Pfedit.get_goal_context p glnum let cl_of_qualid = function - | FunClass -> Classops.CL_FUN - | SortClass -> Classops.CL_SORT - | RefClass r -> Class.class_of_global (Smartlocate.smart_global ~head:true r) + | FunClass -> Coercionops.CL_FUN + | SortClass -> Coercionops.CL_SORT + | RefClass r -> ComCoercion.class_of_global (Smartlocate.smart_global ~head:true r) let scope_class_of_qualid qid = Notation.scope_class_of_class (cl_of_qualid qid) @@ -524,11 +524,11 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = let vernac_definition_hook ~local ~poly = let open Decls in function | Coercion -> - Some (Class.add_coercion_hook ~poly) + Some (ComCoercion.add_coercion_hook ~poly) | CanonicalStructure -> Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) | SubClass -> - Some (Class.add_subclass_hook ~poly) + Some (ComCoercion.add_subclass_hook ~poly) | _ -> None let fresh_name_for_anonymous_theorem () = @@ -1034,7 +1034,7 @@ let vernac_coercion ~atts ref qids qidt = let target = cl_of_qualid qidt in let source = cl_of_qualid qids in let ref' = smart_global ref in - Class.try_add_new_coercion_with_target ref' ~local ~poly ~source ~target; + ComCoercion.try_add_new_coercion_with_target ref' ~local ~poly ~source ~target; Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion") let vernac_identity_coercion ~atts id qids qidt = @@ -1042,7 +1042,7 @@ let vernac_identity_coercion ~atts id qids qidt = let local = enforce_locality local in let target = cl_of_qualid qidt in let source = cl_of_qualid qids in - Class.try_add_new_identity_coercion id ~local ~poly ~source ~target + ComCoercion.try_add_new_identity_coercion id ~local ~poly ~source ~target (* Type classes *) -- cgit v1.2.3