[recordops] complete API rewrite; the module is now called [structures]

7 files changed, 53 insertions, 58 deletions

diff --git a/vernac/canonical.ml b/vernac/canonical.ml
index eaa6c84791..2c04032ca0 100644
--- a/vernac/canonical.ml
+++ b/vernac/canonical.ml
@@ -7,30 +7,30 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
-open Names
 open Libobject
-open Recordops
+open Structures
 
 let open_canonical_structure i (_, (o,_)) =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  if Int.equal i 1 then register_canonical_structure env sigma ~warn:false o
+  if Int.equal i 1 then Instance.register env sigma ~warn:false o
 
 let cache_canonical_structure (_, (o,_)) =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  register_canonical_structure ~warn:true env sigma o
+  Instance.register ~warn:true env sigma o
 
-let discharge_canonical_structure (_,((gref, _ as x), local)) =
+let discharge_canonical_structure (_,(x, local)) =
+  let gref = Instance.repr x in
   if local || (Globnames.isVarRef gref && Lib.is_in_section gref) then None
   else Some (x, local)
 
 
-let inCanonStruc : (GlobRef.t * inductive) * bool -> obj =
+let inCanonStruc : Instance.t * bool -> obj =
   declare_object {(default_object "CANONICAL-STRUCTURE") with
                   open_function = simple_open open_canonical_structure;
                   cache_function = cache_canonical_structure;
-                  subst_function = (fun (subst,(c,local)) -> subst_canonical_structure subst c, local);
+                  subst_function = (fun (subst,(c,local)) -> Instance.subst subst c, local);
                   classify_function = (fun x -> Substitute x);
                   discharge_function = discharge_canonical_structure }
 
@@ -39,4 +39,4 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
 let declare_canonical_structure ?(local=false) ref =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  add_canonical_structure (check_and_decompose_canonical_structure env sigma ref, local)
+  add_canonical_structure (Instance.make env sigma ref, local)
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index 86b15739f9..26d696ff8e 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -90,7 +90,7 @@ let uniform_cond sigma ctx lt =
 
 let class_of_global = function
   | GlobRef.ConstRef sp ->
-    (match Recordops.find_primitive_projection sp with
+    (match Structures.PrimitiveProjections.find_opt sp with
      | Some p -> CL_PROJ p | None -> CL_CONST sp)
   | GlobRef.IndRef sp -> CL_IND sp
   | GlobRef.VarRef id -> CL_SECVAR id
@@ -141,8 +141,8 @@ let get_target env t ind =
     CL_FUN
   else
     match pi1 (find_class_type env 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)
+    | CL_CONST p when Structures.PrimitiveProjections.mem p ->
+      CL_PROJ (Option.get @@ Structures.PrimitiveProjections.find_opt p)
     | x -> x
 
 let strength_of_cl = function
@@ -265,7 +265,7 @@ let inCoercion : coe_info_typ -> obj =
 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
+    | GlobRef.ConstRef c -> Structures.PrimitiveProjections.find_opt c
     | _ -> None
   in
   let c = {
diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml
index 1b811f3db7..39520a68ec 100644
--- a/vernac/comSearch.ml
+++ b/vernac/comSearch.ml
@@ -41,8 +41,8 @@ let kind_searcher = Decls.(function
     Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Coercionops.coe_value gr &&
                                       (k' <> SubClass && k' <> IdentityCoercion || c.Coercionops.coe_is_identity)) coercions)
   | IsDefinition CanonicalStructure ->
-    let canonproj = Recordops.canonical_projections () in
-    Inr (fun gr -> List.exists (fun c -> GlobRef.equal (snd c).Recordops.o_ORIGIN gr) canonproj)
+    let canonproj = Structures.CSTable.entries () in
+    Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Structures.CSTable.solution gr) canonproj)
   | IsDefinition Scheme ->
     let schemes = DeclareScheme.all_schemes () in
     Inr (fun gr -> Indset.exists (fun c -> GlobRef.equal (GlobRef.IndRef c) gr) schemes)
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml
index 7050ddc042..2ab6e3bb15 100644
--- a/vernac/declareInd.ml
+++ b/vernac/declareInd.ml
@@ -76,7 +76,7 @@ let objInductive : inductive_obj Libobject.Dyn.tag =
 
 let inInductive v = Libobject.Dyn.Easy.inj v objInductive
 
-let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c
+let cache_prim (_,(p,c)) = Structures.PrimitiveProjections.register p c
 
 let load_prim _ p = cache_prim p
 
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index ec6e3b44ba..a3cd7a8edc 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -24,7 +24,6 @@ open Impargs
 open Libobject
 open Libnames
 open Globnames
-open Recordops
 open Printer
 open Printmod
 open Context.Rel.Declaration
@@ -1005,22 +1004,24 @@ let print_path_between cls clt =
   print_path ((cls, clt), p)
 
 let print_canonical_projections env sigma grefs =
-  let match_proj_gref ((x,y),c) gr =
-    GlobRef.equal x gr ||
-    begin match y with
-      | Const_cs y -> GlobRef.equal y gr
+  let open Structures in
+  let match_proj_gref { CSTable.projection; value; solution } gr =
+    GlobRef.equal projection gr ||
+    begin match value with
+      | ValuePattern.Const_cs y -> GlobRef.equal y gr
       | _ -> false
     end ||
-    GlobRef.equal c.o_ORIGIN gr
+    GlobRef.equal solution gr
   in
   let projs =
     List.filter (fun p -> List.for_all (match_proj_gref p) grefs)
-      (canonical_projections ())
+      (CSTable.entries ())
   in
   prlist_with_sep fnl
-    (fun ((r1,r2),o) -> pr_cs_pattern r2 ++
+    (fun { CSTable.projection; value; solution } ->
+    ValuePattern.print value ++
     str " <- " ++
-    pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma o.o_DEF ++ str " )")
+    pr_global projection ++ str " ( " ++ pr_global solution ++ str " )")
     projs
 
 (*************************************************************************)
diff --git a/vernac/record.ml b/vernac/record.ml
index ff6bdc5199..fccc3e4fbd 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -22,6 +22,7 @@ open Type_errors
 open Constrexpr
 open Constrexpr_ops
 open Context.Rel.Declaration
+open Structures
 
 module RelDecl = Context.Rel.Declaration
 
@@ -348,7 +349,7 @@ let instantiate_possibly_recursive_type ind u ntypes paramdecls fields =
    this could be refactored as noted above by moving to the
    higher-level declare constant API *)
 let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramdecls
-    paramargs decl impls fid subst sp_projs nfi ti i indsp mib lifted_fields x rp =
+    paramargs decl impls fid subst nfi ti i indsp mib lifted_fields x rp =
   let ccl = subst_projection fid subst ti in
   let body, p_opt = match decl with
     | LocalDef (_,ci,_) -> subst_projection fid subst ci, None
@@ -396,32 +397,33 @@ let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramde
     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)
+  (Some kn, i, Projection term::subst)
 
 (** [build_proj] will build a projection for each field, or skip if
    the field is anonymous, i.e. [_ : t] *)
 let build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs
-    (nfi,i,kinds,sp_projs,subst) flags decl impls =
+    (nfi,i,kinds,subst) flags decl impls =
   let fi = RelDecl.get_name decl in
   let ti = RelDecl.get_type decl in
-  let (sp_projs,i,subst) =
+  let (sp_proj,i,subst) =
     match fi with
     | Anonymous ->
-      (None::sp_projs,i,NoProjection fi::subst)
+      (None,i,NoProjection fi::subst)
     | Name fid ->
       try build_named_proj
             ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramdecls paramargs decl impls fid
-            subst sp_projs nfi ti i indsp mib lifted_fields x rp
+            subst nfi ti i indsp mib lifted_fields x rp
       with NotDefinable why as exn ->
         let _, info = Exninfo.capture exn in
         warning_or_error ~info flags.pf_subclass indsp why;
-        (None::sp_projs,i,NoProjection fi::subst)
+        (None,i,NoProjection fi::subst)
   in
   (nfi - 1, i,
-   { Recordops.pk_name = fi
-   ; pk_true_proj = is_local_assum decl
-   ; pk_canonical = flags.pf_canonical } :: kinds
-  , sp_projs, subst)
+   { Structure.proj_name = fi
+   ; proj_true = is_local_assum decl
+   ; proj_canonical = flags.pf_canonical
+   ; proj_body = sp_proj } :: kinds
+  , subst)
 
 (** [declare_projections] prepares the common context for all record
    projections and then calls [build_proj] for each one. *)
@@ -445,11 +447,12 @@ let declare_projections indsp univs ?(kind=Decls.StructureComponent) binder_name
     | PrimRecord _ -> true
     | FakeRecord | NotRecord -> false
   in
-  let (_,_,kinds,sp_projs,_) =
+  let (_,_,canonical_projections,_) =
     List.fold_left3
       (build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs)
-      (List.length fields,0,[],[],[]) flags (List.rev fields) (List.rev fieldimpls)
-  in (kinds,sp_projs)
+      (List.length fields,0,[],[]) flags (List.rev fields) (List.rev fieldimpls)
+  in
+    List.rev canonical_projections
 
 open Typeclasses
 
@@ -485,20 +488,17 @@ let check_template ~template ~poly ~univs ~params { Data.id; rdata = { DataR.min
     (* auto detect template *)
     ComInductive.should_auto_template id (template && template_candidate ())
 
-let load_structure i (_, structure) =
-  Recordops.register_structure structure
+let load_structure i (_, structure) = Structure.register structure
 
-let cache_structure o =
-  load_structure 1 o
+let cache_structure o = load_structure 1 o
 
-let subst_structure (subst, obj) =
-  Recordops.subst_structure subst obj
+let subst_structure (subst, obj) = Structure.subst subst obj
 
 let discharge_structure (_, x) = Some x
 
-let rebuild_structure s = Recordops.rebuild_structure (Global.env()) s
+let rebuild_structure s = Structure.rebuild (Global.env()) s
 
-let inStruc : Recordops.struc_typ -> Libobject.obj =
+let inStruc : Structure.t -> Libobject.obj =
   let open Libobject in
   declare_object {(default_object "STRUCTURE") with
     cache_function = cache_structure;
@@ -601,17 +601,10 @@ let declare_structure ~cumulative finite ~ubind ~univs ~variances paramimpls par
   let map i { Data.is_coercion; coers; rdata = { DataR.implfs; fields; _}; _ } =
     let rsp = (kn, i) in (* This is ind path of idstruc *)
     let cstr = (rsp, 1) in
-    let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers implfs fields in
+    let projections = declare_projections rsp ctx ~kind binder_name.(i) 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 npars = Inductiveops.inductive_nparams (Global.env()) rsp in
-    let struc = {
-      Recordops.s_CONST = cstr;
-      s_PROJ = List.rev sp_projs;
-      s_PROJKIND = List.rev kinds;
-      s_EXPECTEDPARAM = npars;
-    }
-    in
+    let struc = Structure.make (Global.env ()) rsp projections in
     let () = declare_structure_entry struc in
     rsp
   in
@@ -674,7 +667,7 @@ let build_record_constant ~rdata ~ubind ~univs ~variances ~cumulative ~template
       meth_info = b;
       meth_const = y;
     } in
-    let l = List.map3 map (List.rev fields) coers (Recordops.lookup_projections ind) in
+    let l = List.map3 map (List.rev fields) coers (Structure.find_projections ind) in
     GlobRef.IndRef ind, l
   in
   List.map map inds
diff --git a/vernac/record.mli b/vernac/record.mli
index 7a40af048c..feb257da3c 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -11,6 +11,7 @@
 open Names
 open Vernacexpr
 open Constrexpr
+open Structures
 
 module Ast : sig
   type t =
@@ -51,8 +52,8 @@ module Internal : sig
     -> projection_flags list
     -> Impargs.manual_implicits list
     -> Constr.rel_context
-    -> Recordops.proj_kind list * Names.Constant.t option list
+    -> Structure.projection list
 
-  val declare_structure_entry : Recordops.struc_typ -> unit
+  val declare_structure_entry : Structure.t -> unit
 
 end