[Canonical structures] Some projections may not be canonical

6 files changed, 52 insertions, 27 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e5bf52571c..bb66658a37 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -850,10 +850,10 @@ let rec extern inctx scopes vars r =
 		     | Some c :: q ->
 		         match locs with
 			   | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
-			   | (_, false) :: locs' ->
+                           | { Recordops.pk_true_proj = false } :: locs' ->
 			       (* we don't want to print locals *)
 			       ip q locs' args acc
-			   | (_, true) :: locs' ->
+                           | { Recordops.pk_true_proj = true } :: locs' ->
 			       match args with
 				 | [] -> raise No_match
 				     (* we give up since the constructor is not complete *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c0801067ce..f06493b374 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1368,7 +1368,7 @@ let sort_fields ~complete loc fields completer =
                  let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in
                  begin match proj_kinds with
                     | [] -> anomaly (Pp.str "Number of projections mismatch.")
-                    | (_, regular) :: proj_kinds ->
+                    | { Recordops.pk_true_proj = regular } :: proj_kinds ->
                        (* "regular" is false when the field is defined
                            by a let-in in the record declaration
                            (its value is fixed from other fields). *)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index d69824a256..331fa2d288 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -27,16 +27,30 @@ open Reductionops
 (*s A structure S is a non recursive inductive type with a single
    constructor (the name of which defaults to Build_S) *)
 
-(* Table des structures: le nom de la structure (un [inductive]) donne
-   le nom du constructeur, le nombre de paramètres et pour chaque
-   argument réel du constructeur, le nom de la projection
-   correspondante, si valide, et un booléen disant si c'est une vraie
-   projection ou bien une fonction constante (associée à un LetIn) *)
+(* Table of structures.
+   It maps to each structure name (of type [inductive]):
+     - the name of its constructor;
+     - the number of parameters;
+     - for each true argument, some data about the corresponding projection:
+         * its name (may be anonymous);
+         * whether it is a true projection (as opposed to a constant function, LetIn);
+         * whether it should be used as a canonical hint;
+         * the constant realizing this projection (if any).
+*)
+
+type proj_kind = {
+  pk_name: Name.t;
+  pk_true_proj: bool;
+  pk_canonical: bool;
+}
+
+let mk_proj_kind pk_name pk_true_proj : proj_kind =
+  { pk_name ; pk_true_proj ; pk_canonical = true }
 
 type struc_typ = {
   s_CONST : constructor;
   s_EXPECTEDPARAM : int;
-  s_PROJKIND : (Name.t * bool) list;
+  s_PROJKIND : proj_kind list;
   s_PROJ : Constant.t option list }
 
 let structure_table =
@@ -47,7 +61,7 @@ let projection_table =
 (* TODO: could be unify struc_typ and struc_tuple ? *)
 
 type struc_tuple =
-    constructor * (Name.t * bool) list * Constant.t option list
+    constructor * proj_kind list * Constant.t option list
 
 let register_structure env (id,kl,projs) =
   let open Declarations in
@@ -161,7 +175,7 @@ let canonical_projections () =
     !object_table []
 
 let keep_true_projections projs kinds =
-  let filter (p, (_, b)) = if b then Some p else None in
+  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 rec cs_pattern_of_constr env t =
@@ -206,17 +220,20 @@ let compute_canonical_projections env ~warn (con,ind) =
   let o_NPARAMS = List.length o_TPARAMS in
   let lpj = keep_true_projections lpj kl in
   let nenv = Termops.push_rels_assum sign env in
-  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
+  List.fold_left2 (fun acc (spopt, canonical) t ->
+      if canonical
+      then
+        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
+      else acc
     ) [] lpj projs
 
 let pr_cs_pattern = function
@@ -288,7 +305,7 @@ let check_and_decompose_canonical_structure env sigma ref =
     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 snd s.s_PROJKIND 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
     error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
   (sp,indsp)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index f0594d513a..565454d3b3 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -17,14 +17,22 @@ open Constr
 (** 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;
+}
+
+val mk_proj_kind : Name.t -> bool -> proj_kind
+
 type struc_typ = {
   s_CONST : constructor;
   s_EXPECTEDPARAM : int;
-  s_PROJKIND : (Name.t * bool) list;
+  s_PROJKIND : proj_kind list;
   s_PROJ : Constant.t option list }
 
 type struc_tuple =
-    constructor * (Name.t * bool) list * Constant.t option list
+    constructor * proj_kind list * Constant.t option list
 
 val register_structure : Environ.env -> struc_tuple -> unit
 val subst_structure : Mod_subst.substitution -> struc_tuple -> struc_tuple
diff --git a/vernac/record.ml b/vernac/record.ml
index f489707eb3..9b0fbea148 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -368,7 +368,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
             with NotDefinable why ->
 	      warning_or_error coe indsp why;
 	      (None::sp_projs,i,NoProjection fi::subst) in
-      (nfi-1,i,(fi, is_local_assum decl)::kinds,sp_projs,subst))
+      (nfi - 1, i, Recordops.mk_proj_kind fi (is_local_assum decl) :: kinds, sp_projs, subst))
       (List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)
 
diff --git a/vernac/record.mli b/vernac/record.mli
index d6e63901cd..51ab7487d7 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -22,7 +22,7 @@ val declare_projections :
   bool list ->
   Impargs.manual_implicits list ->
   Constr.rel_context ->
-    (Name.t * bool) list * Constant.t option list
+    Recordops.proj_kind list * Constant.t option list
 
 val declare_structure_entry : Recordops.struc_tuple -> unit