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

1 files changed, 0 insertions, 379 deletions

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       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open CErrors
-open Util
-open Pp
-open Names
-open Term
-open Constr
-open Context
-open Vars
-open Termops
-open Environ
-open Classops
-open Declare
-open Libobject
-
-let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL
-
-let loc_of_bool b = if b then `LOCAL else `GLOBAL
-
-(* Errors *)
-
-type coercion_error_kind =
-  | AlreadyExists
-  | NotAFunction
-  | NoSource of cl_typ option
-  | ForbiddenSourceClass of cl_typ
-  | NoTarget
-  | WrongTarget of cl_typ * cl_typ
-  | NotAClass of GlobRef.t
-
-exception CoercionError of coercion_error_kind
-
-let explain_coercion_error g = function
-  | AlreadyExists ->
-      (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)