Factor code between records and typeclasses

proux01 · proux01 · commit cd77691b4421 · 2022-04-01T10:47:52.000+02:00
This is a followup of #12611
diff --git a/vernac/record.ml b/vernac/record.ml
@@ -118,6 +118,7 @@ end
 
 type projection_flags = {
   pf_subclass: bool;
+  pf_priority: int option;
   pf_canonical: bool;
 }
 
@@ -413,7 +414,7 @@ let build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls param
 
 (** [declare_projections] prepares the common context for all record
    projections and then calls [build_proj] for each one. *)
-let declare_projections indsp univs ?(kind=Decls.StructureComponent) inhabitant_id flags fieldimpls fields =
+let declare_projections indsp univs ~kind inhabitant_id flags fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
   let poly = Declareops.inductive_is_polymorphic mib in
@@ -528,7 +529,7 @@ let data_name id rdata =
    The entry point is [definition_structure], which will match on the
    declared [kind] and then either follow the regular record
    declaration path to [declare_structure] or handle the record as a
-   class declaration with [declare_class].
+   definitional class declaration with [declare_class_constant].
 
 *)
 
@@ -538,8 +539,8 @@ let data_name id rdata =
   - prepares and declares the corresponding record projections, mainly taken care of by
     [declare_projections]
 *)
-let declare_structure ~cumulative finite ~univs ~variances ~primitive_proj
-  paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) =
+let declare_structure ~cumulative finite ~univs ~variances ~primitive_proj ~proj_kind
+  paramimpls params template (record_data : Data.t list) =
   let nparams = List.length params in
   let (univs, ubinders) = univs in
   let poly, projunivs =
@@ -592,20 +593,34 @@ let declare_structure ~cumulative finite ~univs ~variances ~primitive_proj
   let map i { Data.is_coercion; coers; rdata = { DataR.implfs; fields; _}; inhabitant_id; id; _ } =
     let rsp = (kn, i) in (* This is ind path of idstruc *)
     let cstr = (rsp, 1) in
-    let projections = declare_projections rsp (projunivs,ubinders) ~kind inhabitant_id coers implfs fields in
+    let projections = declare_projections rsp (projunivs,ubinders) ~kind:proj_kind inhabitant_id coers implfs fields in
     let build = GlobRef.ConstructRef cstr in
     let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~poly in
     let struc = Structure.make (Global.env ()) rsp projections in
     let () = declare_structure_entry struc in
-    rsp
+    GlobRef.IndRef rsp
   in
-  List.mapi map record_data
+  List.mapi map record_data, []
 
 let implicits_of_context ctx =
   List.map (fun name -> CAst.make (Some (name,true)))
     (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
 
-let build_class_constant ~univs ~rdata ~primitive_proj field implfs params paramimpls coers binder id proj_name =
+(* declare definitional class (typeclasses that are not record) *)
+let declare_class_constant ~univs paramimpls params data =
+  let id, rdata, coers, inhabitant_id = match data with
+    | [{ Data.id; rdata; is_coercion; coers; inhabitant_id }] ->
+       assert (not is_coercion);  (* should be ensured by caller *)
+       let coers = List.map (fun { pf_subclass; pf_priority } -> if pf_subclass then Some { hint_priority = pf_priority; hint_pattern = None } else None) coers in
+       id, rdata, coers, inhabitant_id
+    | _ -> assert false in  (* should be ensured by caller *)
+  let implfs = rdata.DataR.implfs in
+  let field, binder, proj_name = match rdata.DataR.fields with
+    | [ LocalAssum ({binder_name=Name proj_name} as binder, field)
+      | LocalDef ({binder_name=Name proj_name} as binder, _, field) ] ->
+       let binder = {binder with binder_name=Name inhabitant_id} in
+       field, binder, proj_name
+    | _ -> assert false in  (* should be ensured by caller *)
   let class_body = it_mkLambda_or_LetIn field params in
   let class_type = it_mkProd_or_LetIn rdata.DataR.arity params in
   let class_entry =
@@ -641,44 +656,29 @@ let build_class_constant ~univs ~rdata ~primitive_proj field implfs params param
     meth_info = sub;
     meth_const = Some proj_cst;
   } in
-  [cref, [m]]
-
-let build_record_constant ~rdata ~univs ~variances ~cumulative ~template ~primitive_proj
-    fields params paramimpls is_coercion coers id idbuild inhabitant_id =
-  let record_data =
-    { Data.id
-    ; idbuild
-    ; is_coercion = false
-    (* to be replaced by the following line after deprecation phase
-       (started in 8.16, c.f., https://github.com/coq/coq/pull/15802 ) *)
-    (* ; is_coercion *)
-    ; coers = List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) coers
-    (* to be replaced by the following line after deprecation phase
-       (started in 8.16, c.f., https://github.com/coq/coq/pull/15802 ) *)
-    (* ; coers = List.map (fun c -> { pf_subclass = c <> None ; pf_canonical = true }) coers *)
-    ; rdata
-    ; inhabitant_id
-    } in
-  let inds = declare_structure ~cumulative Declarations.BiFinite ~univs ~variances ~primitive_proj paramimpls
-      params template ~kind:Decls.Method ~name:[|inhabitant_id|] [record_data]
-  in
-  let map ind =
-    let map decl b y = {
-      meth_name = RelDecl.get_name decl;
-      meth_info = b;
-      meth_const = y;
-    } in
-    let l = List.map3 map (List.rev fields) coers (Structure.find_projections ind) in
-    GlobRef.IndRef ind, l
-  in
-  List.map map inds
+  [cref], [m]
+
+(* deprecated in 8.16, to be removed at the end of the deprecation phase
+   (c.f., https://github.com/coq/coq/pull/15802 ) *)
+let warn_future_coercion_class_constructor =
+  CWarnings.create ~name:"future-coercion-class-constructor" ~category:"records"
+    ~default:CWarnings.AsError
+    Pp.(fun () -> str "'Class >' currently does nothing. Use 'Class' instead.")
+
+(* deprecated in 8.16, to be removed at the end of the deprecation phase
+   (c.f., https://github.com/coq/coq/pull/15802 ) *)
+let warn_future_coercion_class_field =
+  CWarnings.create ~name:"future-coercion-class-field" ~category:"records" Pp.(fun () ->
+      str "A coercion will be introduced in future versions when using ':>' in 'Class' declarations. "
+      ++ str "Use '#[global] Existing Instance field.' instead if you don't want the coercion.")
 
 (** [declare_class] will prepare and declare a [Class]. This is done in
    2 steps:
 
-  1. two markedly different paths are followed depending on whether the
-   class declaration refers to a constant "definitional classes" or to
-   a record, that is to say:
+  1. two markedly different paths were followed depending on whether the
+   class declaration refers to a constant "definitional classes"
+   (with [declare_class_constant]) or to a record (with [declare_structure]),
+   that is to say:
 
       Class foo := bar : T.
 
@@ -692,29 +692,34 @@ let build_record_constant ~rdata ~univs ~variances ~cumulative ~template ~primit
 
       Class foo := { ... }.
 
-  2. declare the class, using the information from 1. in the form of [Classes.typeclass]
+  2. now, declare the class, using the information ([inds] and [def]) from 1.
+   in the form of [Classes.typeclass]
 
   *)
-let declare_class def ~cumulative ~univs ~variances ~primitive_proj id idbuild inhabitant_id paramimpls params
-    rdata template ?(kind=Decls.StructureComponent) is_coercion coers =
-  let implfs =
-    (* Make the class implicit in the projections, and the params if applicable. *)
-    let impls = implicits_of_context params in
-      List.map (fun x -> impls @ x) rdata.DataR.implfs
-  in
-  let rdata = { rdata with DataR.implfs } in
-  let fields = rdata.DataR.fields in
-  let data =
-    match fields with
-    | [ LocalAssum ({binder_name=Name proj_name} as binder, field)
-      | LocalDef ({binder_name=Name proj_name} as binder, _, field) ] when def ->
-      assert (not is_coercion);  (* should be ensured by caller *)
-      let binder = {binder with binder_name=Name inhabitant_id} in
-      build_class_constant ~rdata ~univs ~primitive_proj field implfs params paramimpls coers binder id proj_name
+let declare_class ~univs params inds def data =
+  let id, idbuild, rdata, is_coercion, coers, inhabitant_id = match data with
+    | [{ Data.id; idbuild; rdata; is_coercion; coers; inhabitant_id }] ->
+       if is_coercion then warn_future_coercion_class_constructor ();
+       if List.exists (fun pf -> pf.pf_subclass) coers then
+         warn_future_coercion_class_field ();
+       let coers = List.map (fun { pf_subclass; pf_priority } -> if pf_subclass then Some { hint_priority = pf_priority; hint_pattern = None } else None) coers in
+       id, idbuild, rdata, is_coercion, coers, inhabitant_id
     | _ ->
-      build_record_constant ~rdata ~univs ~variances ~cumulative ~template ~primitive_proj
-        fields params paramimpls is_coercion coers id idbuild inhabitant_id
+       CErrors.user_err (str "Mutual definitional classes are not handled.") in
+  let fields = rdata.DataR.fields in
+  let map ind =
+    let map decl b y = {
+      meth_name = RelDecl.get_name decl;
+      meth_info = b;
+      meth_const = y;
+    } in
+    let l = match ind with
+      | GlobRef.IndRef ind ->
+         List.map3 map (List.rev fields) coers (Structure.find_projections ind)
+      | _ -> def in
+    ind, l
   in
+  let data = List.map map inds in
   let univs, params, fields =
     match fst univs with
     | UState.Polymorphic_entry uctx ->
@@ -739,9 +744,9 @@ let declare_class def ~cumulative ~univs ~variances ~primitive_proj id idbuild i
     in
     let env = Global.env () in
     let sigma = Evd.from_env env in
-    Classes.add_class env sigma k; impl
+    Classes.add_class env sigma k
   in
-  List.map map data
+  List.iter map data
 
 let add_constant_class env sigma cst =
   let ty, univs = Typeops.type_of_global_in_context env (GlobRef.ConstRef cst) in
@@ -855,69 +860,6 @@ let extract_record_data records =
   in
   ps, data
 
-(* deprecated in 8.16, to be removed at the end of the deprecation phase
-   (c.f., https://github.com/coq/coq/pull/15802 ) *)
-let warn_future_coercion_class_constructor =
-  CWarnings.create ~name:"future-coercion-class-constructor" ~category:"records"
-    ~default:CWarnings.AsError
-    Pp.(fun () -> str "'Class >' currently does nothing. Use 'Class' instead.")
-
-(* deprecated in 8.16, to be removed at the end of the deprecation phase
-   (c.f., https://github.com/coq/coq/pull/15802 ) *)
-let warn_future_coercion_class_field =
-  CWarnings.create ~name:"future-coercion-class-field" ~category:"records" Pp.(fun () ->
-      str "A coercion will be introduced in future versions when using ':>' in 'Class' declarations. "
-      ++ str "Use '#[global] Existing Instance field.' instead if you don't want the coercion.")
-
-(* declaring structures, common data to refactor *)
-let class_structure ~cumulative ~template ~impargs ~univs ~params ~primitive_proj def records data =
-  let { Ast.name; is_coercion; cfs; idbuild; default_inhabitant_id; _ }, rdata = match records, data with
-    | [r], [d] -> r, d
-    | _, _ ->
-      CErrors.user_err (str "Mutual definitional classes are not handled.")
-  in
-  if is_coercion then warn_future_coercion_class_constructor ();
-  if List.exists (function (_, { rf_subclass = Vernacexpr.BackInstance; _ }) -> true | _ -> false) cfs then
-    warn_future_coercion_class_field ();
-  let coers = List.map (fun (_, { rf_subclass; rf_priority }) ->
-      match rf_subclass with
-      | Vernacexpr.BackInstance -> Some {hint_priority = rf_priority; hint_pattern = None}
-      | Vernacexpr.NoInstance -> None)
-      cfs
-  in
-  let inhabitant_id =
-    match default_inhabitant_id with
-    | None -> Namegen.next_ident_away name.CAst.v (Termops.vars_of_env (Global.env()))
-    | Some id -> id
-  in
-  declare_class def ~cumulative ~univs ~primitive_proj name.CAst.v idbuild inhabitant_id
-    impargs params rdata template is_coercion coers
-
-let regular_structure ~cumulative ~template ~impargs ~univs ~variances ~params ~finite ~primitive_proj
-    records data =
-  let adjust_impls impls = impargs @ [CAst.make None] @ impls in
-  let data = List.map (fun ({ DataR.implfs; _ } as d) -> { d with DataR.implfs = List.map adjust_impls implfs }) data in
-  (* let map (min_univ, arity, fieldimpls, fields) { Ast.name; is_coercion; cfs; idbuild; _ } = *)
-  let map rdata { Ast.name; is_coercion; cfs; idbuild; default_inhabitant_id; _ } =
-    let coers = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
-        { pf_subclass =
-            (match rf_subclass with Vernacexpr.BackInstance -> true | Vernacexpr.NoInstance -> false);
-          pf_canonical = rf_canonical })
-        cfs
-    in
-    let inhabitant_id =
-      match default_inhabitant_id with
-      | None -> data_name name.CAst.v rdata
-      | Some n -> n
-    in
-    { Data.id = name.CAst.v; idbuild; rdata; is_coercion; coers; inhabitant_id }
-  in
-  let data = List.map2 map data records in
-  let inds = declare_structure ~cumulative finite ~univs ~variances ~primitive_proj
-      impargs params template data
-  in
-  List.map (fun ind -> GlobRef.IndRef ind) inds
-
 (** [fs] corresponds to fields and [ps] to parameters; [coers] is a
     list telling if the corresponding fields must me declared as coercions
     or subinstances. *)
@@ -936,17 +878,50 @@ let definition_structure udecl kind ~template ~cumulative ~poly ~primitive_proj
         typecheck_params_and_fields (kind = Class true) poly udecl ps data) ()
   in
   let template = template, auto_template in
-  match kind with
-  | Class def ->
-    class_structure ~template ~impargs ~cumulative ~params ~univs ~variances ~primitive_proj
-      def records data
-  | Inductive_kw | CoInductive | Variant | Record | Structure ->
-    regular_structure ~cumulative ~template ~impargs ~univs ~variances ~params ~finite ~primitive_proj
-      records data
+  let is_class = match kind with Class def -> Some def
+    | Inductive_kw | CoInductive | Variant | Record | Structure -> None in
+  let adjust_impls impls = match is_class with
+    | None -> impargs @ [CAst.make None] @ impls
+    | Some _ -> implicits_of_context params @ impls in
+  let data = List.map DataR.(fun d -> { d with implfs = List.map adjust_impls d.implfs }) data in
+  let map rdata { Ast.name; is_coercion; cfs; idbuild; default_inhabitant_id; _ } =
+    let coers = List.map (fun (_, { rf_subclass; rf_priority; rf_canonical }) ->
+      { pf_subclass = Vernacexpr.(match rf_subclass with BackInstance -> true | NoInstance -> false)
+      ; pf_priority = rf_priority; pf_canonical = rf_canonical })
+      cfs
+    in
+    let inhabitant_id =
+      match default_inhabitant_id, is_class with
+      | None, Some _ -> Namegen.next_ident_away name.CAst.v (Termops.vars_of_env (Global.env()))
+      | None, None -> data_name name.CAst.v rdata
+      | Some id, _ -> id
+    in
+    { Data.id = name.CAst.v; idbuild; rdata; is_coercion; coers; inhabitant_id }
+  in
+  let data = List.map2 map data records in
+  let inds, def = match is_class with
+    | Some true -> declare_class_constant ~univs impargs params data
+    | Some false | None ->
+       let proj_kind =
+         Decls.(match is_class with None -> StructureComponent | _ -> Method) in
+       (* remove the following block after deprecation phase
+          (started in 8.16, c.f., https://github.com/coq/coq/pull/15802 ) *)
+       let data' = if is_class = None then data else
+         List.map (fun d ->
+             { d with
+               Data.is_coercion = false
+             ; coers = List.map (fun _ -> { pf_subclass = false ; pf_priority = None ; pf_canonical = true }) d.Data.coers
+           }) data in
+       declare_structure ~cumulative finite ~univs ~variances ~primitive_proj
+         ~proj_kind impargs params template data'
+  in
+  if is_class <> None then declare_class ~univs params inds def data;
+  inds
 
 module Internal = struct
   type nonrec projection_flags = projection_flags = {
     pf_subclass: bool;
+    pf_priority: int option;
     pf_canonical: bool;
   }
   let declare_projections = declare_projections
diff --git a/vernac/record.mli b/vernac/record.mli
@@ -43,13 +43,14 @@ val declare_existing_class : GlobRef.t -> unit
 module Internal : sig
   type projection_flags = {
     pf_subclass: bool;
+    pf_priority: int option;
     pf_canonical: bool;
   }
 
   val declare_projections
     : Names.inductive
     -> Entries.universes_entry * UnivNames.universe_binders
-    -> ?kind:Decls.definition_object_kind
+    -> kind:Decls.definition_object_kind
     -> Names.Id.t
     -> projection_flags list
     -> Impargs.manual_implicits list
