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 --- 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 +- 11 files changed, 450 insertions(+), 450 deletions(-) delete mode 100644 vernac/class.ml delete mode 100644 vernac/class.mli create mode 100644 vernac/comCoercion.ml create mode 100644 vernac/comCoercion.mli (limited to 'vernac') 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