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

8 files changed, 386 insertions, 260 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e1d6fff3e4..285fea183b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -19,7 +19,7 @@ open Context
 open Vars
 open Reduction
 open Reductionops
-open Recordops
+open Structures
 open Evarutil
 open Evardefine
 open Evarsolve
@@ -230,33 +230,30 @@ let occur_rigidly flags env evd (evk,_) t =
    projection would have been reduced) *)
 
 let check_conv_record env sigma (t1,sk1) (t2,sk2) =
+  let open ValuePattern in
   let (proji, u), arg = Termops.global_app_of_constr sigma t1 in
-  let canon_s,sk2_effective =
+  let (sigma, solution), sk2_effective =
     try
       match EConstr.kind sigma t2 with
         Prod (_,a,b) -> (* assert (l2=[]); *)
           let _, a, b = destProd sigma t2 in
           if noccurn sigma 1 b then
-            lookup_canonical_conversion env (proji, Prod_cs),
+            CanonicalSolution.find env sigma (proji, Prod_cs),
             (Stack.append_app [|a;pop b|] Stack.empty)
           else raise Not_found
       | Sort s ->
         let s = ESorts.kind sigma s in
-        lookup_canonical_conversion env
+        CanonicalSolution.find env sigma
           (proji, Sort_cs (Sorts.family s)),[]
       | Proj (p, c) ->
-        lookup_canonical_conversion env (proji, Proj_cs (Projection.repr p)), Stack.append_app [|c|] sk2
+        CanonicalSolution.find env sigma(proji, Proj_cs (Names.Projection.repr p)), Stack.append_app [|c|] sk2
       | _ ->
         let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in
-          lookup_canonical_conversion env (proji, Const_cs c2),sk2
+          CanonicalSolution.find env sigma (proji, Const_cs c2),sk2
     with Not_found ->
-      let (c, cs) = lookup_canonical_conversion env (proji,Default_cs) in
-        (c,cs),[]
+      CanonicalSolution.find env sigma (proji,Default_cs), []
   in
-  let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs;
-        o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in
-  let us = List.map EConstr.of_constr us in
-  let params = List.map EConstr.of_constr params in
+  let open CanonicalSolution in
   let params1, c1, extra_args1 =
     match arg with
     | Some c -> (* A primitive projection applied to c *)
@@ -267,28 +264,19 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
         with _ -> raise Not_found
       in Stack.append_app_list ind_args Stack.empty, c, sk1
     | None ->
-      match Stack.strip_n_app nparams sk1 with
+      match Stack.strip_n_app solution.nparams sk1 with
       | Some (params1, c1, extra_args1) -> params1, c1, extra_args1
       | _ -> raise Not_found in
   let us2,extra_args2 =
-    let l_us = List.length us in
+    let l_us = List.length solution.cvalue_arguments in
       if Int.equal l_us 0 then Stack.empty,sk2_effective
       else match (Stack.strip_n_app (l_us-1) sk2_effective) with
       | None -> raise Not_found
       | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in
-  let u, ctx' = UnivGen.fresh_instance_from ctx None in
-  let subst = Univ.make_inverse_instance_subst u in
-  let c = EConstr.of_constr c in
-  let c' = subst_univs_level_constr subst c in
-  let t' = EConstr.of_constr t' in
-  let t' = subst_univs_level_constr subst t' in
-  let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in
-  let params = List.map (fun c -> subst_univs_level_constr subst c) params in
-  let us = List.map (fun c -> subst_univs_level_constr subst c) us in
-  let h, _ = decompose_app_vect sigma t' in
-    ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1),
-    (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
-    (n, Stack.zip sigma (t2,sk2))
+  let h, _ = decompose_app_vect sigma solution.body in
+    sigma,(h, t2),solution.constant,solution.abstractions_ty,(Stack.append_app_list solution.params Stack.empty,params1),
+    (Stack.append_app_list solution.cvalue_arguments Stack.empty,us2),(extra_args1,extra_args2),c1,
+    (solution.cvalue_abstraction, Stack.zip sigma (t2,sk2))
 
 (* Precondition: one of the terms of the pb is an uninstantiated evar,
  * possibly applied to arguments. *)
@@ -926,7 +914,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         and f2 i =
           (try
              if not flags.with_cs then raise Not_found
-             else conv_record flags env i
+             else conv_record flags env
                (try check_conv_record env i appr1 appr2
                 with Not_found -> check_conv_record env i appr2 appr1)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
@@ -989,7 +977,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         let f3 i =
           (try
              if not flags.with_cs then raise Not_found
-             else conv_record flags env i (check_conv_record env i appr1 appr2)
+             else conv_record flags env (check_conv_record env i appr1 appr2)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
         and f4 i =
           evar_eqappr_x flags env i pbty
@@ -1003,7 +991,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         let f3 i =
           (try
              if not flags.with_cs then raise Not_found
-             else conv_record flags env i (check_conv_record env i appr2 appr1)
+             else conv_record flags env (check_conv_record env i appr2 appr1)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
         and f4 i =
           evar_eqappr_x flags env i pbty appr1
@@ -1113,7 +1101,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         | LetIn _, _ -> assert false
       end
 
-and conv_record flags env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) =
+and conv_record flags env (evd,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) =
   (* Tries to unify the states
 
         (proji params1 c1 | sk1)   =   (proji params2 (c (?xs:bs)) | sk2)
@@ -1137,7 +1125,6 @@ and conv_record flags env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk
 
      had to be initially resolved
   *)
-  let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
   if Reductionops.Stack.compare_shape sk1 sk2 then
     let (evd',ks,_,test) =
       List.fold_left
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index be03ced7eb..965cd7de67 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -78,7 +78,7 @@ val check_problems_are_solved : env -> evar_map -> unit
 
 val check_conv_record : env -> evar_map ->
   state -> state ->
-  Univ.ContextSet.t * (constr * constr)
+  evar_map * (constr * constr)
   * constr * constr list * (constr Stack.t * constr Stack.t) *
     (constr Stack.t * constr Stack.t) *
     (constr Stack.t * constr Stack.t) * constr *
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index de1af62043..21b2137f09 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -35,6 +35,7 @@ open Environ
 open EConstr
 open Vars
 open Reductionops
+open Structures
 open Type_errors
 open Typing
 open Evarutil
@@ -801,8 +802,8 @@ struct
     in
     let app_f =
       match EConstr.kind sigma fj.uj_val with
-      | Const (p, u) when Recordops.is_primitive_projection p ->
-        let p = Option.get @@ Recordops.find_primitive_projection p in
+      | Const (p, u) when PrimitiveProjections.mem p ->
+        let p = Option.get @@ PrimitiveProjections.find_opt p in
         let p = Projection.make p false in
         let npars = Projection.npars p in
         fun n ->
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index c31ecc135c..980575abac 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -12,7 +12,7 @@ Cbv
 Find_subterm
 Evardefine
 Evarsolve
-Recordops
+Structures
 Heads
 Evarconv
 Typing
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
deleted file mode 100644
index 83927085e9..0000000000
--- a/pretyping/recordops.mli
+++ /dev/null
@@ -1,101 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \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 Names
-open Constr
-
-(** Operations concerning records and canonical structures *)
-
-(** {6 Records } *)
-(** A structure S is a non recursive inductive type with a single
-   constructor (the name of which defaults to Build_S) *)
-
-type proj_kind = {
-  pk_name: Name.t;
-  pk_true_proj: bool;
-  pk_canonical: bool;
-}
-
-type struc_typ = {
-  s_CONST : constructor;
-  s_EXPECTEDPARAM : int;
-  s_PROJKIND : proj_kind list;
-  s_PROJ : Constant.t option list;
-}
-
-val register_structure : struc_typ -> unit
-val subst_structure : Mod_subst.substitution -> struc_typ -> struc_typ
-val rebuild_structure : Environ.env -> struc_typ -> struc_typ
-
-(** [lookup_structure isp] returns the struc_typ associated to the
-   inductive path [isp] if it corresponds to a structure, otherwise
-   it fails with [Not_found] *)
-val lookup_structure : inductive -> struc_typ
-
-(** [lookup_projections isp] returns the projections associated to the
-   inductive path [isp] if it corresponds to a structure, otherwise
-   it fails with [Not_found] *)
-val lookup_projections : inductive -> Constant.t option list
-
-(** raise [Not_found] if not a projection *)
-val find_projection_nparams : GlobRef.t -> int
-
-(** raise [Not_found] if not a projection *)
-val find_projection : GlobRef.t -> struc_typ
-
-val is_projection : Constant.t -> bool
-
-(** Sets up the mapping from constants to primitive projections *)
-val register_primitive_projection : Projection.Repr.t -> Constant.t -> unit
-
-val is_primitive_projection : Constant.t -> bool
-
-val find_primitive_projection : Constant.t -> Projection.Repr.t option
-
-(** {6 Canonical structures } *)
-(** A canonical structure declares "canonical" conversion hints between
-    the effective components of a structure and the projections of the
-    structure *)
-
-(** A cs_pattern characterizes the form of a component of canonical structure *)
-type cs_pattern =
-    Const_cs of GlobRef.t
-  | Proj_cs of Projection.Repr.t
-  | Prod_cs
-  | Sort_cs of Sorts.family
-  | Default_cs
-
-type obj_typ = {
-  o_ORIGIN : GlobRef.t;
-  o_DEF : constr;
-  o_CTX : Univ.AUContext.t;
-  o_INJ : int option;      (** position of trivial argument *)
-  o_TABS : constr list;    (** ordered *)
-  o_TPARAMS : constr list; (** ordered *)
-  o_NPARAMS : int;
-  o_TCOMPS : constr list } (** ordered *)
-
-(** Return the form of the component of a canonical structure *)
-val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * constr list
-
-val pr_cs_pattern : cs_pattern -> Pp.t
-
-type cs = GlobRef.t * inductive
-
-val lookup_canonical_conversion : Environ.env -> (GlobRef.t * cs_pattern) -> constr * obj_typ
-val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map ->
-  cs -> unit
-val subst_canonical_structure : Mod_subst.substitution -> cs -> cs
-val is_open_canonical_projection :
-  Environ.env -> Evd.evar_map -> EConstr.t -> bool
-val canonical_projections : unit ->
-  ((GlobRef.t * cs_pattern) * obj_typ) list
-
-val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> cs
diff --git a/pretyping/recordops.ml b/pretyping/structures.ml
index aa862a912e..3ef6e98373 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/structures.ml
@@ -37,71 +37,67 @@ open Reductionops
          * the constant realizing this projection (if any).
 *)
 
-type proj_kind = {
-  pk_name: Name.t;
-  pk_true_proj: bool;
-  pk_canonical: bool;
+module Structure = struct
+
+type projection = {
+  proj_name : Names.Name.t;
+  proj_true : bool;
+  proj_canonical : bool;
+  proj_body : Names.Constant.t option;
+}
+
+type t = {
+  name : Names.inductive;
+  projections : projection list;
+  nparams : int;
 }
 
-type struc_typ = {
-  s_CONST : constructor;
-  s_EXPECTEDPARAM : int;
-  s_PROJKIND : proj_kind list;
-  s_PROJ : Constant.t option list }
+let make env name projections =
+  let nparams = Inductiveops.inductive_nparams env name in
+  { name; projections; nparams }
 
 let structure_table =
-  Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs"
+  Summary.ref (Indmap.empty : t Indmap.t) ~name:"record-structs"
 let projection_table =
-  Summary.ref (Cmap.empty : struc_typ Cmap.t) ~name:"record-projs"
+  Summary.ref (Cmap.empty : t Cmap.t) ~name:"record-projs"
 
-let register_structure ({ s_CONST = (ind,_); s_PROJ = projs; } as struc) =
-  structure_table := Indmap.add ind struc !structure_table;
+let register ({ name; projections; nparams } as s) =
+  structure_table := Indmap.add name s !structure_table;
   projection_table :=
-    List.fold_right (Option.fold_right (fun proj -> Cmap.add proj struc))
-      projs !projection_table
-
-let subst_structure subst struc =
-  let projs' =
-   (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
-   (* the first component of subst_con.                                   *)
-   List.Smart.map
-     (Option.Smart.map (subst_constant subst))
-    struc.s_PROJ
-  in
-  let id' = Globnames.subst_constructor subst struc.s_CONST in
-  if projs' == struc.s_PROJ && id' == struc.s_CONST
-  then struc
-  else { struc with s_CONST = id'; s_PROJ = projs' }
+    List.fold_right (fun { proj_body } m ->
+      Option.fold_right (fun proj -> Cmap.add proj s) proj_body m)
+    projections !projection_table
 
-let rebuild_structure env struc =
-  let mib = Environ.lookup_mind (fst (fst struc.s_CONST)) env in
-  let npars = mib.Declarations.mind_nparams in
-  { struc with s_EXPECTEDPARAM = npars }
+let subst subst ({ name; projections; nparams } as s) =
+  let subst_projection subst ({ proj_body } as p) =
+    let proj_body = Option.Smart.map (subst_constant subst) proj_body in
+    if proj_body == p.proj_body then p else
+    { p with proj_body } in
+  let projections = List.Smart.map (subst_projection subst) projections in
+  let name = Mod_subst.subst_ind subst name in
+  if projections == s.projections &&
+     name == s.name
+  then s
+  else { name; projections; nparams }
 
-let lookup_structure indsp = Indmap.find indsp !structure_table
+let rebuild env s =
+  let mib = Environ.lookup_mind (fst s.name) env in
+  let nparams = mib.Declarations.mind_nparams in
+  { s with nparams }
 
-let lookup_projections indsp = (lookup_structure indsp).s_PROJ
+let find indsp = Indmap.find indsp !structure_table
 
-let find_projection_nparams = function
-  | GlobRef.ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM
-  | _ -> raise Not_found
+let find_projections indsp =
+  (find indsp).projections |>
+  List.map (fun { proj_body } -> proj_body)
 
-let find_projection = function
-  | GlobRef.ConstRef cst -> Cmap.find cst !projection_table
-  | _ -> raise Not_found
+let find_from_projection cst = Cmap.find cst !projection_table
 
-let is_projection cst = Cmap.mem cst !projection_table
+let projection_nparams cst = (Cmap.find cst !projection_table).nparams
 
-let prim_table =
-  Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs"
-
-let register_primitive_projection p c =
-  prim_table := Cmap_env.add c p !prim_table
-
-let is_primitive_projection c = Cmap_env.mem c !prim_table
+let is_projection cst = Cmap.mem cst !projection_table
 
-let find_primitive_projection c =
-  try Some (Cmap_env.find c !prim_table) with Not_found -> None
+end
 
 (************************************************************************)
 (*s A canonical structure declares "canonical" conversion hints between *)
@@ -142,49 +138,55 @@ type obj_typ = {
   o_NPARAMS : int;
   o_TCOMPS : constr list } (* ordered *)
 
-type cs_pattern =
+module ValuePattern = struct
+
+type t =
     Const_cs of GlobRef.t
-  | Proj_cs of Projection.Repr.t
+  | Proj_cs of Names.Projection.Repr.t
   | Prod_cs
   | Sort_cs of Sorts.family
   | Default_cs
 
-let eq_cs_pattern env p1 p2 = match p1, p2 with
-| Const_cs gr1, Const_cs gr2 -> Environ.QGlobRef.equal env gr1 gr2
-| Proj_cs p1, Proj_cs p2 -> Environ.QProjection.Repr.equal env p1 p2
-| Prod_cs, Prod_cs -> true
-| Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2
-| Default_cs, Default_cs -> true
-| _ -> false
-
-let rec assoc_pat env a = function
-  | ((pat, t), e) :: xs -> if eq_cs_pattern env pat a then (t, e) else assoc_pat env a xs
-  | [] -> raise Not_found
-
-
-let object_table =
-  Summary.ref (GlobRef.Map.empty : ((cs_pattern * constr) * obj_typ) list GlobRef.Map.t)
-    ~name:"record-canonical-structs"
-
-let canonical_projections () =
-  GlobRef.Map.fold (fun x -> List.fold_right (fun ((y,_),c) acc -> ((x,y),c)::acc))
-    !object_table []
-
-let keep_true_projections projs kinds =
-  let filter (p, { pk_true_proj ; pk_canonical }) = if pk_true_proj then Some (p, pk_canonical) else None in
-  List.map_filter filter (List.combine projs kinds)
+let equal env p1 p2 = match p1, p2 with
+  | Const_cs gr1, Const_cs gr2 -> Environ.QGlobRef.equal env gr1 gr2
+  | Proj_cs p1, Proj_cs p2 -> Environ.QProjection.Repr.equal env p1 p2
+  | Prod_cs, Prod_cs -> true
+  | Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2
+  | Default_cs, Default_cs -> true
+  | _ -> false
 
-let rec cs_pattern_of_constr env t =
+let rec of_constr env t =
   match kind t with
   | App (f,vargs) ->
-    let patt, n, args = cs_pattern_of_constr env f in
+    let patt, n, args = of_constr env f in
     patt, n, args @ Array.to_list vargs
   | Rel n -> Default_cs, Some n, []
   | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
-  | Proj (p, c) -> Proj_cs (Projection.repr p), None, [c]
+  | Proj (p, c) -> Proj_cs (Names.Projection.repr p), None, [c]
   | Sort s -> Sort_cs (Sorts.family s), None, []
   | _ -> Const_cs (fst @@ destRef t) , None, []
 
+let print = function
+    Const_cs c -> Nametab.pr_global_env Id.Set.empty c
+  | Proj_cs p -> Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef (Names.Projection.Repr.constant p))
+  | Prod_cs -> str "_ -> _"
+  | Default_cs -> str "_"
+  | Sort_cs s -> Sorts.pr_sort_family s
+
+end
+
+let rec assoc_pat env a = function
+  | ((pat, t), e) :: xs -> if ValuePattern.equal env pat a then (t, e) else assoc_pat env a xs
+  | [] -> raise Not_found
+
+let object_table =
+  Summary.ref (GlobRef.Map.empty : ((ValuePattern.t * constr) * obj_typ) list GlobRef.Map.t)
+    ~name:"record-canonical-structs"
+
+let keep_true_projections projs =
+  let filter { Structure.proj_true ; proj_canonical; proj_body } = if proj_true then Some (proj_body, proj_canonical) else None in
+  List.map_filter filter projs
+
 let warn_projection_no_head_constant =
   CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
          (fun (sign,env,t,ref,proji_sp) ->
@@ -213,17 +215,17 @@ let compute_canonical_projections env ~warn (gref,ind) =
   let t = EConstr.Unsafe.to_constr t in
   let o_TABS = List.rev_map snd sign in
   let args = snd (decompose_app t) in
-  let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } =
-    lookup_structure ind in
+  let { Structure.nparams = p; projections = lpj } =
+    Structure.find ind in
   let o_TPARAMS, projs = List.chop p args in
   let o_NPARAMS = List.length o_TPARAMS in
-  let lpj = keep_true_projections lpj kl in
+  let lpj = keep_true_projections lpj in
   let nenv = Termops.push_rels_assum sign env in
   List.fold_left2 (fun acc (spopt, canonical) t ->
       if canonical
       then
         Option.cata (fun proji_sp ->
-            match cs_pattern_of_constr nenv t with
+            match ValuePattern.of_constr nenv t with
             | patt, o_INJ, o_TCOMPS ->
               ((GlobRef.ConstRef proji_sp, (patt, t)),
                { o_ORIGIN = gref ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
@@ -235,13 +237,6 @@ let compute_canonical_projections env ~warn (gref,ind) =
       else acc
     ) [] lpj projs
 
-let pr_cs_pattern = function
-    Const_cs c -> Nametab.pr_global_env Id.Set.empty c
-  | Proj_cs p -> Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef (Projection.Repr.constant p))
-  | Prod_cs -> str "_ -> _"
-  | Default_cs -> str "_"
-  | Sort_cs s -> Sorts.pr_sort_family s
-
 let warn_redundant_canonical_projection =
   CWarnings.create ~name:"redundant-canonical-projection" ~category:"typechecker"
          (fun (hd_val,prj,new_can_s,old_can_s) ->
@@ -249,26 +244,13 @@ let warn_redundant_canonical_projection =
           ++ strbrk " by " ++ prj ++ strbrk " in "
           ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)
 
-let register_canonical_structure ~warn env sigma o =
-    compute_canonical_projections env ~warn o |>
-    List.iter (fun ((proj, (cs_pat, _ as pat)), s) ->
-      let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in
-      match assoc_pat env cs_pat l with
-      | exception Not_found ->
-          object_table := GlobRef.Map.add proj ((pat, s) :: l) !object_table
-      | _, cs ->
-        if warn
-        then
-          let old_can_s = Termops.Internal.print_constr_env env sigma (EConstr.of_constr cs.o_DEF) in
-          let new_can_s = Termops.Internal.print_constr_env env sigma (EConstr.of_constr s.o_DEF) in
-          let prj = Nametab.pr_global_env Id.Set.empty proj in
-          let hd_val = pr_cs_pattern cs_pat in
-          warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s)
-      )
+module Instance = struct
 
-type cs = GlobRef.t * inductive
+type t = GlobRef.t * inductive
 
-let subst_canonical_structure subst (gref,ind as obj) =
+let repr = fst
+
+let subst subst (gref,ind as obj) =
   (* invariant: cst is an evaluable reference. Thus we can take *)
   (* the first component of subst_con.                                   *)
   match gref with
@@ -286,7 +268,7 @@ let error_not_structure ref description =
        (Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++
           description))
 
-let check_and_decompose_canonical_structure env sigma ref =
+let make env sigma ref =
   let vc =
     match ref with
     | GlobRef.ConstRef sp ->
@@ -311,17 +293,71 @@ let check_and_decompose_canonical_structure env sigma ref =
     | Construct ((indsp,1),u) -> indsp
     | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in
   let s =
-    try lookup_structure indsp
+    try Structure.find indsp
     with Not_found ->
       error_not_structure ref
         (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env sigma (EConstr.mkInd indsp)) in
-  let ntrue_projs = List.count (fun { pk_true_proj } -> pk_true_proj) s.s_PROJKIND in
-  if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
+  let ntrue_projs = List.count (fun { Structure.proj_true = x } -> x) s.Structure.projections in
+  if s.Structure.nparams + ntrue_projs > Array.length args then
     error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
   (ref,indsp)
 
-let lookup_canonical_conversion env (proj,pat) =
-  assoc_pat env pat (GlobRef.Map.find proj !object_table)
+let register ~warn env sigma o =
+    compute_canonical_projections env ~warn o |>
+    List.iter (fun ((proj, (cs_pat, _ as pat)), s) ->
+      let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in
+      match assoc_pat env cs_pat l with
+      | exception Not_found ->
+          object_table := GlobRef.Map.add proj ((pat, s) :: l) !object_table
+      | _, cs ->
+        if warn
+        then
+          let old_can_s = Termops.Internal.print_constr_env env sigma (EConstr.of_constr cs.o_DEF) in
+          let new_can_s = Termops.Internal.print_constr_env env sigma (EConstr.of_constr s.o_DEF) in
+          let prj = Nametab.pr_global_env Id.Set.empty proj in
+          let hd_val = ValuePattern.print cs_pat in
+          warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s)
+      )
+
+end
+
+(** The canonical solution of a problem (proj,val) is a global
+    [constant = fun abs : abstractions_ty => body] and
+    [ body = RecodConstructor params canon_values ] and the canonical value
+    corresponding to val is [val cvalue_arguments].
+    It is possible that val is one of the [abs] abstractions, eg [Default_cs],
+    and in that case [cvalue_abstraction = Some i] *)
+
+module CanonicalSolution = struct
+type t = {
+  constant : EConstr.t;
+
+  abstractions_ty : EConstr.t list;
+  body : EConstr.t;
+
+  nparams : int;
+  params : EConstr.t list;
+  cvalue_abstraction : int option;
+  cvalue_arguments : EConstr.t list;
+}
+
+let find env sigma (proj,pat) =
+  let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs;
+        o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = assoc_pat env pat (GlobRef.Map.find proj !object_table) in
+  let us = List.map EConstr.of_constr us in
+  let params = List.map EConstr.of_constr params in
+  let u, ctx' = UnivGen.fresh_instance_from ctx None in
+  let subst = Univ.make_inverse_instance_subst u in
+  let c = EConstr.of_constr c in
+  let c' = EConstr.Vars.subst_univs_level_constr subst c in
+  let t' = EConstr.of_constr t' in
+  let t' = EConstr.Vars.subst_univs_level_constr subst t' in
+  let bs' = List.map (EConstr.of_constr %> EConstr.Vars.subst_univs_level_constr subst) bs in
+  let params = List.map (fun c -> EConstr.Vars.subst_univs_level_constr subst c) params in
+  let us = List.map (fun c -> EConstr.Vars.subst_univs_level_constr subst c) us in
+  let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in
+  sigma, { body = t'; constant = c'; abstractions_ty = bs'; nparams; params; cvalue_arguments = us; cvalue_abstraction = n }
+
 
 let rec get_nth n = function
 | [] -> raise Not_found
@@ -336,12 +372,12 @@ let rec decompose_projection sigma c args =
   | Cast (c, _, _) -> decompose_projection sigma c args
   | App (c, arg) -> decompose_projection sigma c (arg :: args)
   | Const (c, u) ->
-     let n = find_projection_nparams (GlobRef.ConstRef c) in
+     let n = Structure.projection_nparams c in
      (* Check if there is some canonical projection attached to this structure *)
      let _ = GlobRef.Map.find (GlobRef.ConstRef c) !object_table in
      get_nth n args
   | Proj (p, c) ->
-     let _ = GlobRef.Map.find (GlobRef.ConstRef (Projection.constant p)) !object_table in
+     let _ = GlobRef.Map.find (GlobRef.ConstRef (Names.Projection.constant p)) !object_table in
      c
   | _ -> raise Not_found
 
@@ -355,3 +391,44 @@ let is_open_canonical_projection env sigma c =
       not (isConstruct sigma hd)
     with Failure _ -> false
   with Not_found -> false
+
+end
+
+module CSTable = struct
+
+type entry = {
+  projection : Names.GlobRef.t;
+  value : ValuePattern.t;
+  solution : Names.GlobRef.t;
+}
+
+let canonical_entry_of_object projection ((value,_), { o_ORIGIN = solution }) =
+  { projection; value; solution }
+
+let entries () =
+  GlobRef.Map.fold (fun p ol acc ->
+    List.fold_right (fun o acc -> canonical_entry_of_object p o :: acc) ol acc)
+    !object_table []
+
+let entries_for ~projection:p =
+  try
+    GlobRef.Map.find p !object_table |>
+    List.map (canonical_entry_of_object p)
+  with Not_found -> []
+
+end
+
+module PrimitiveProjections = struct
+
+let prim_table =
+  Summary.ref (Cmap_env.empty : Names.Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs"
+
+let register p c =
+  prim_table := Cmap_env.add c p !prim_table
+
+let mem c = Cmap_env.mem c !prim_table
+
+let find_opt c =
+  try Some (Cmap_env.find c !prim_table) with Not_found -> None
+
+end
diff --git a/pretyping/structures.mli b/pretyping/structures.mli
new file mode 100644
index 0000000000..a1cc38e8e0
--- /dev/null
+++ b/pretyping/structures.mli
@@ -0,0 +1,163 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \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)         *)
+(************************************************************************)
+
+
+(** A structure S is a non recursive inductive type with a single
+   constructor *)
+module Structure : sig
+
+(** A projection to a structure field *)
+type projection = {
+  proj_name : Names.Name.t;            (** field name *)
+  proj_true : bool;                    (** false for primitive records *)
+  proj_canonical : bool;               (** false = not to be used for CS inference *)
+  proj_body : Names.Constant.t option; (** the projection function *)
+}
+
+type t = {
+  name : Names.inductive;
+  projections : projection list;
+  nparams : int;
+}
+
+val make : Environ.env -> Names.inductive -> projection list -> t
+
+val register : t -> unit
+val subst : Mod_subst.substitution -> t -> t
+
+(** refreshes nparams, e.g. after section discharging *)
+val rebuild : Environ.env -> t -> t
+
+(** [find isp] returns the Structure.t associated to the
+   inductive path [isp] if it corresponds to a structure, otherwise
+   it fails with [Not_found] *)
+val find : Names.inductive -> t
+
+(** raise [Not_found] if not a structure projection *)
+val find_from_projection : Names.Constant.t -> t
+
+(** [lookup_projections isp] returns the projections associated to the
+   inductive path [isp] if it corresponds to a structure, otherwise
+   it fails with [Not_found] *)
+val find_projections : Names.inductive -> Names.Constant.t option list
+
+(** raise [Not_found] if not a projection *)
+val projection_nparams : Names.Constant.t -> int
+
+val is_projection : Names.Constant.t -> bool
+
+end
+
+(** A canonical instance declares "canonical" conversion hints between
+    the effective components of a structure and the projections of the
+    structure *)
+module Instance : sig
+
+type t
+
+(** Process a record instance, checkig it can be registered as canonical.
+    The record type must be declared as a canonical Structure.t beforehand.  *)
+val make : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> t
+
+(** Register an instance as canonical *)
+val register : warn:bool -> Environ.env -> Evd.evar_map -> t -> unit
+
+val subst : Mod_subst.substitution -> t -> t
+val repr : t -> Names.GlobRef.t
+
+end
+
+
+(** A ValuePattern.t characterizes the form of a component of canonical
+    instance and is used to query the data base of canonical instances *)
+module ValuePattern : sig
+
+type t =
+  | Const_cs of Names.GlobRef.t
+  | Proj_cs of Names.Projection.Repr.t
+  | Prod_cs
+  | Sort_cs of Sorts.family
+  | Default_cs
+
+val equal : Environ.env -> t -> t -> bool
+val print : t -> Pp.t
+
+(** Return the form of the component of a canonical structure *)
+val of_constr : Environ.env -> Constr.t -> t * int option * Constr.t list
+
+end
+
+
+(** The canonical solution of a problem (proj,val) is a global
+    [constant = fun abs : abstractions_ty => body] and
+    [body = RecodConstructor params canon_values] and the canonical value
+    corresponding to val is [val cvalue_arguments].
+    It is possible that val is one of the [abs] abstractions, eg [Default_cs],
+    and in that case [cvalue_abstraction = Some i] *)
+
+module CanonicalSolution : sig
+
+type t = {
+  constant : EConstr.t;
+
+  abstractions_ty : EConstr.t list;
+  body : EConstr.t;
+
+  nparams : int;
+  params : EConstr.t list;
+  cvalue_abstraction : int option;
+  cvalue_arguments : EConstr.t list;
+}
+
+(** [find (p,v)] returns a s such that p s = v.
+    The solution s gets a fresh universe instance and is decomposed into
+    bits for consumption by evarconv. Can raise [Not_found] on failure *)
+val find :
+  Environ.env -> Evd.evar_map -> (Names.GlobRef.t * ValuePattern.t) ->
+    Evd.evar_map * t
+
+(** [is_open_canonical_projection env sigma t] is true if t is a FieldName
+    applied to term which is not a constructor. Used by evarconv not to
+    unfold too much and lose a projection too early *)
+val is_open_canonical_projection :
+  Environ.env -> Evd.evar_map -> EConstr.t -> bool
+
+end
+
+(** Low level access to the Canonical Structure database *)
+module CSTable : sig
+
+type entry = {
+  projection : Names.GlobRef.t;
+  value : ValuePattern.t;
+  solution : Names.GlobRef.t;
+}
+
+(** [all] returns the list of tuples { p ; v ; s }
+   Note: p s = v *)
+val entries : unit -> entry list
+
+(** [entries_for p] returns the list of canonical entries that have
+    p as their FieldName *)
+val entries_for : projection:Names.GlobRef.t -> entry list
+
+end
+
+(** Some extra info for structures which are primitive records *)
+module PrimitiveProjections : sig
+
+(** Sets up the mapping from constants to primitive projections *)
+val register : Names.Projection.Repr.t -> Names.Constant.t -> unit
+
+val mem : Names.Constant.t -> bool
+
+val find_opt : Names.Constant.t -> Names.Projection.Repr.t option
+
+end
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index df0f49a033..18db75eed5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -22,13 +22,13 @@ open Namegen
 open Evd
 open Reduction
 open Reductionops
+open Structures
 open Evarutil
 open Evardefine
 open Evarsolve
 open Pretype_errors
 open Retyping
 open Coercion
-open Recordops
 open Locus
 open Locusops
 open Find_subterm
@@ -509,13 +509,13 @@ let key_of env sigma b flags f =
   match EConstr.kind sigma f with
   | Const (cst, u) when is_transparent env (ConstKey cst) &&
       (TransparentState.is_transparent_constant flags.modulo_delta cst
-       || Recordops.is_primitive_projection cst) ->
+       || PrimitiveProjections.mem cst) ->
       let u = EInstance.kind sigma u in
       Some (IsKey (ConstKey (cst, u)))
   | Var id when is_transparent env (VarKey id) &&
       TransparentState.is_transparent_variable flags.modulo_delta id ->
     Some (IsKey (VarKey id))
-  | Proj (p, c) when Projection.unfolded p
+  | Proj (p, c) when Names.Projection.unfolded p
     || (is_transparent env (ConstKey (Projection.constant p)) &&
        (TransparentState.is_transparent_constant flags.modulo_delta (Projection.constant p))) ->
     Some (IsProj (p, c))
@@ -1077,7 +1077,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
   and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) =
     let f1 () =
       if isApp_or_Proj sigma cM then
-          if is_open_canonical_projection curenv sigma cM then
+          if CanonicalSolution.is_open_canonical_projection curenv sigma cM then
             solve_canonical_projection curenvnb pb opt cM cN substn
           else error_cannot_unify (fst curenvnb) sigma (cM,cN)
       else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -1091,7 +1091,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
       else
         try f1 () with e when precatchable_exception e ->
           if isApp_or_Proj sigma cN then
-              if is_open_canonical_projection curenv sigma cN then
+              if CanonicalSolution.is_open_canonical_projection curenv sigma cN then
                 solve_canonical_projection curenvnb pb opt cN cM substn
               else error_cannot_unify (fst curenvnb) sigma (cM,cN)
           else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -1099,12 +1099,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
   and solve_canonical_projection curenvnb pb opt cM cN (sigma,ms,es) =
     let f1l1 = whd_nored_state (fst curenvnb) sigma (cM,Stack.empty) in
     let f2l2 = whd_nored_state (fst curenvnb) sigma (cN,Stack.empty) in
-    let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
+    let (sigma,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
       try Evarconv.check_conv_record (fst curenvnb) sigma f1l1 f2l2
       with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
     in
     if Reductionops.Stack.compare_shape ts ts1 then
-      let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
       let (evd,ks,_) =
         List.fold_left
           (fun (evd,ks,m) b ->