Merge PR #10075: [Record] Une a record to gather field declaration attributes

Reviewed-by: gares

8 files changed, 44 insertions, 47 deletions

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 1feb8acd5f..d69824a256 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -191,41 +191,33 @@ let warn_projection_no_head_constant =
 
 (* Intended to always succeed *)
 let compute_canonical_projections env ~warn (con,ind) =
-  let ctx = Environ.constant_context env con in
-  let u = Univ.make_abstract_instance ctx in
-  let v = (mkConstU (con,u)) in
+  let o_CTX = Environ.constant_context env con in
+  let u = Univ.make_abstract_instance o_CTX in
+  let o_DEF = mkConstU (con, u) in
   let c = Environ.constant_value_in env (con,u) in
   let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in
   let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
   let t = EConstr.Unsafe.to_constr t in
-  let lt = List.rev_map snd sign 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 params, projs = List.chop p args 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 lps = List.combine lpj projs in
   let nenv = Termops.push_rels_assum sign env in
-  let comp =
-    List.fold_left
-      (fun l (spopt,t) -> (* comp=components *)
-	 match spopt with
-           | Some proji_sp ->
-	       begin
-		 try
-		   let patt, n , args = cs_pattern_of_constr nenv t in
-		     ((ConstRef proji_sp, patt, t, n, args) :: l)
-		 with Not_found ->
-                   if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp);
-                   l
-	       end
-	   | _ -> l)
-      [] lps in
-  List.map (fun (refi,c,t,inj,argj) ->
-    (refi,(c,t)),
-    {o_DEF=v; o_CTX=ctx; o_INJ=inj; o_TABS=lt;
-     o_TPARAMS=params; o_NPARAMS=List.length params; o_TCOMPS=argj})
-    comp
+  List.fold_left2 (fun acc spopt t ->
+      Option.cata (fun proji_sp ->
+          match cs_pattern_of_constr nenv t with
+          | patt, o_INJ, o_TCOMPS ->
+            ((ConstRef proji_sp, (patt, t)),
+             { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
+            :: acc
+          | exception Not_found ->
+            if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp);
+            acc
+        ) acc spopt
+    ) [] lpj projs
 
 let pr_cs_pattern = function
     Const_cs c -> Nametab.pr_global_env Id.Set.empty c
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 674b4285d2..4a4c5c94e9 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -137,7 +137,7 @@ let classify_vernac e =
         | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
         | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @
            CList.map_filter (function
-            | ((_,AssumExpr({v=Names.Name n},_)),_),_ -> Some n
+            | AssumExpr({v=Names.Name n},_), _ -> Some n
             | _ -> None) l) l in
         VtSideff (List.flatten ids), VtLater
     | VernacScheme l ->
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index d97fb523f7..59d2a66259 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -447,8 +447,10 @@ GRAMMAR EXTEND Gram
 *)
   (* ... with coercions *)
   record_field:
-  [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> { n } ];
-      ntn = decl_notation -> { (bd,pri),ntn } ] ]
+  [ [ bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ];
+      rf_notation = decl_notation -> {
+      let rf_subclass, rf_decl = bd in
+      rf_decl, { rf_subclass ; rf_priority ; rf_notation } } ] ]
   ;
   record_fields:
     [ [ f = record_field; ";"; fs = record_fields -> { f :: fs }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 327efcda2b..889dbafabd 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -446,15 +446,15 @@ open Pputils
     | Some true -> str" :>"
     | Some false -> str" :>>"
 
-  let pr_record_field ((x, pri), ntn) =
+  let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = ntn }) =
     let env = Global.env () in
     let sigma = Evd.from_env env in
     let prx = match x with
-      | (oc,AssumExpr (id,t)) ->
+      | AssumExpr (id,t) ->
         hov 1 (pr_lname id ++
                  pr_oc oc ++ spc() ++
                  pr_lconstr_expr env sigma t)
-      | (oc,DefExpr(id,b,opt)) -> (match opt with
+      | DefExpr(id,b,opt) -> (match opt with
           | Some t ->
             hov 1 (pr_lname id ++
                      pr_oc oc ++ spc() ++
diff --git a/vernac/record.ml b/vernac/record.ml
index 74e5a03659..f489707eb3 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -634,7 +634,7 @@ let declare_existing_class g =
 open Vernacexpr
 
 let check_unique_names records =
-  let extract_name acc (((_, bnd), _), _) = match bnd with
+  let extract_name acc (rf_decl, _) = match rf_decl with
       Vernacexpr.AssumExpr({CAst.v=Name id},_) -> id::acc
     | Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc
     | _ -> acc in
@@ -649,15 +649,15 @@ let check_unique_names records =
 let check_priorities kind records =
   let isnot_class = match kind with Class false -> false | _ -> true in
   let has_priority (_, _, _, cfs, _, _) =
-    List.exists (fun ((_, pri), _) -> not (Option.is_empty pri)) cfs
+    List.exists (fun (_, { rf_priority }) -> not (Option.is_empty rf_priority)) cfs
   in
   if isnot_class && List.exists has_priority records then
     user_err Pp.(str "Priorities only allowed for type class substructures")
 
 let extract_record_data records =
   let map (is_coe, id, _, cfs, idbuild, s) =
-    let fs = List.map (fun (((_, f), _), _) -> f) cfs in
-    id.CAst.v, s, List.map snd cfs, fs
+    let fs = List.map fst cfs in
+    id.CAst.v, s, List.map (fun (_, { rf_notation }) -> rf_notation) cfs, fs
   in
   let data = List.map map records in
   let pss = List.map (fun (_, _, ps, _, _, _) -> ps) records in
@@ -691,16 +691,15 @@ let definition_structure udecl kind ~template cum poly finite records =
     | [r], [d] -> r, d
     | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled")
     in
-    let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in
-    let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
+    let priorities = List.map (fun (_, { rf_priority }) -> {hint_priority = rf_priority ; hint_pattern = None}) cfs in
+    let coers = List.map (fun (_, { rf_subclass }) -> rf_subclass) cfs in
     declare_class def cum ubinders univs id.CAst.v idbuild
       implpars params arity template implfs fields coers priorities
   | _ ->
     let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in
     let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
     let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
-      let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
-      let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in
+      let coe = List.map (fun (_, { rf_subclass }) -> not (Option.is_empty rf_subclass)) cfs in
       id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe
     in
     let data = List.map2 map data records in
diff --git a/vernac/record.mli b/vernac/record.mli
index 12a2a765b5..d6e63901cd 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -33,7 +33,7 @@ val definition_structure :
   (coercion_flag *
   Names.lident *
   local_binder_expr list *
-  (local_decl_expr with_instance with_priority with_notation) list *
+  (local_decl_expr * record_field_attr) list *
   Id.t * constr_expr option) list ->
   GlobRef.t list
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0f6374c506..388f6957cf 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -684,7 +684,7 @@ let vernac_record ~template udecl cum k poly finite records =
     let () =
       if Dumpglob.dump () then
         let () = Dumpglob.dump_definition id false "rec" in
-        let iter (((_, x), _), _) = match x with
+        let iter (x, _) = match x with
         | Vernacexpr.AssumExpr ({loc;v=Name id}, _) ->
           Dumpglob.dump_definition (make ?loc id) false "proj"
         | _ -> ()
@@ -743,7 +743,8 @@ let vernac_inductive ~atts cum lo finite indl =
     let (id, bl, c, l) = Option.get is_defclass in
     let (coe, (lid, ce)) = l in
     let coe' = if coe then Some true else None in
-    let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in
+    let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce),
+            { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] } in
     vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]]
   else if List.for_all is_record indl then
     (* Mutual record case *)
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 99b457effe..34a9b9394a 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -143,13 +143,16 @@ type decl_notation = lstring * constr_expr * scope_name option
 type simple_binder = lident list  * constr_expr
 type class_binder = lident * constr_expr list
 type 'a with_coercion = coercion_flag * 'a
-type 'a with_instance = instance_flag * 'a
-type 'a with_notation = 'a * decl_notation list
-type 'a with_priority = 'a * int option
+(* Attributes of a record field declaration *)
+type record_field_attr = {
+  rf_subclass: instance_flag; (* the projection is an implicit coercion or an instance *)
+  rf_priority: int option; (* priority of the instance, if relevant *)
+  rf_notation: decl_notation list;
+  }
 type constructor_expr = (lident * constr_expr) with_coercion
 type constructor_list_or_record_decl_expr =
   | Constructors of constructor_expr list
-  | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list
+  | RecordDecl of lident option * (local_decl_expr * record_field_attr) list
 type inductive_expr =
   ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind *
     constructor_list_or_record_decl_expr