Merge PR #12027: Fix #3415: coqdoc links projections rather than constructor in record tuples

Reviewed-by: ejgallego

7 files changed, 118 insertions, 73 deletions

diff --git a/doc/changelog/08-tools/12027-master+fix3415-coqdoc-record.rst b/doc/changelog/08-tools/12027-master+fix3415-coqdoc-record.rst
new file mode 100644
index 0000000000..ae9b69e592
--- /dev/null
+++ b/doc/changelog/08-tools/12027-master+fix3415-coqdoc-record.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Fields of a record tuple now link in coqdoc to their definition
+  (`#12027 <https://github.com/coq/coq/pull/12027>`_, fixes
+  `#3415 <https://github.com/coq/coq/issues/3415>`_,
+  by Hugo Herbelin; ).
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b72802d911..f82783f47d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1428,62 +1428,28 @@ let inductive_of_record loc record =
 let sort_fields ~complete loc fields completer =
   match fields with
     | [] -> None
-    | (first_field_ref, first_field_value):: other_fields ->
+    | (first_field_ref, _):: _ ->
         let (first_field_glob_ref, record) =
           try
             let gr = locate_reference first_field_ref in
+            Dumpglob.add_glob ?loc:first_field_ref.CAst.loc gr;
             (gr, Recordops.find_projection gr)
           with Not_found ->
-            raise (InternalizationError(loc, NotAProjection first_field_ref))
+            raise (InternalizationError(first_field_ref.CAst.loc, NotAProjection first_field_ref))
         in
         (* the number of parameters *)
         let nparams = record.Recordops.s_EXPECTEDPARAM in
         (* the reference constructor of the record *)
-        let base_constructor =
-          let global_record_id = GlobRef.ConstructRef record.Recordops.s_CONST in
-          try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id
-          with Not_found ->
-            anomaly (str "Environment corruption for records.") in
+        let base_constructor = GlobRef.ConstructRef record.Recordops.s_CONST in
         let () = check_duplicate ?loc fields in
-        let (end_index,    (* one past the last field index *)
-             first_field_index,  (* index of the first field of the record *)
-             proj_list)    (* list of projections *)
-          =
-          (* eliminate the first field from the projections,
-             but keep its index *)
-          let rec build_proj_list projs proj_kinds idx ~acc_first_idx acc =
-            match projs with
-              | [] -> (idx, acc_first_idx, acc)
-              | (Some field_glob_id) :: projs ->
-                 let field_glob_ref = GlobRef.ConstRef field_glob_id in
-                 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.")
-                    | { 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). *)
-                       if first_field && not regular && complete then
-                         user_err ?loc  (str "No local fields allowed in a record construction.")
-                       else if first_field then
-                         build_proj_list projs proj_kinds (idx+1) ~acc_first_idx:idx acc
-                       else if not regular && complete then
-                         (* skip non-regular fields *)
-                         build_proj_list projs proj_kinds idx ~acc_first_idx acc
-                       else
-                         build_proj_list projs proj_kinds (idx+1) ~acc_first_idx
-                                         ((idx, field_glob_id) :: acc)
-                 end
-              | None :: projs ->
-                 if complete then
-                   (* we don't want anonymous fields *)
-                   user_err ?loc  (str "This record contains anonymous fields.")
-                 else
-                   (* anonymous arguments don't appear in proj_kinds *)
-                   build_proj_list projs proj_kinds (idx+1) ~acc_first_idx acc
-          in
-          build_proj_list record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 ~acc_first_idx:0 []
-        in
+        let build_proj idx proj kind =
+          if proj = None && complete then
+            (* we don't want anonymous fields *)
+            user_err ?loc (str "This record contains anonymous fields.")
+          else
+            (idx, proj, kind.Recordops.pk_true_proj) in
+        let proj_list =
+          List.map2_i build_proj 1 record.Recordops.s_PROJ record.Recordops.s_PROJKIND in
         (* now we want to have all fields assignments indexed by their place in
            the constructor *)
         let rec index_fields fields remaining_projs acc =
@@ -1491,34 +1457,43 @@ let sort_fields ~complete loc fields completer =
             | (field_ref, field_value) :: fields ->
                let field_glob_ref = try locate_reference field_ref
                with Not_found ->
-                 user_err ?loc ~hdr:"intern"
+                 user_err ?loc:field_ref.CAst.loc ~hdr:"intern"
                                (str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in
-               let this_field_record = try Recordops.find_projection field_glob_ref
-                 with Not_found ->
-                   let inductive_ref = inductive_of_record loc record in
-                   raise (InternalizationError(loc, NotAProjectionOf (field_ref, inductive_ref)))
-               in
-               let remaining_projs, (field_index, _) =
-                 let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (GlobRef.ConstRef glob_id) in
+               let remaining_projs, (field_index, _, regular) =
+                 let the_proj = function
+                   | (idx, Some glob_id, _) -> GlobRef.equal field_glob_ref (GlobRef.ConstRef glob_id)
+                   | (idx, None, _) -> false in
                  try CList.extract_first the_proj remaining_projs
                  with Not_found ->
-                   let ind1 = inductive_of_record loc record in
-                   let ind2 = inductive_of_record loc this_field_record in
+                   let floc = field_ref.CAst.loc in
+                   let this_field_record =
+                     try Recordops.find_projection field_glob_ref
+                     with Not_found ->
+                       let inductive_ref = inductive_of_record floc record in
+                       raise (InternalizationError(floc, NotAProjectionOf (field_ref, inductive_ref))) in
+                   let ind1 = inductive_of_record floc record in
+                   let ind2 = inductive_of_record floc this_field_record in
                    raise (InternalizationError(loc, ProjectionsOfDifferentRecords (ind1, ind2)))
                in
+               if not regular && complete then
+                 (* "regular" is false when the field is defined
+                    by a let-in in the record declaration
+                    (its value is fixed from other fields). *)
+                 user_err ?loc  (str "No local fields allowed in a record construction.");
+               Dumpglob.add_glob ?loc:field_ref.CAst.loc field_glob_ref;
                index_fields fields remaining_projs ((field_index, field_value) :: acc)
             | [] ->
-               (* the order does not matter as we sort them next,
-                  List.rev_* is just for efficiency *)
                let remaining_fields =
-                 let complete_field (idx, field_ref) = (idx,
-                 completer idx field_ref record.Recordops.s_CONST) in
-                 List.rev_map complete_field remaining_projs in
+                 let complete_field (idx, field_ref, regular) =
+                   if not regular && complete then
+                     (* For terms, we keep only regular fields *)
+                     None
+                   else
+                     Some (idx, completer idx field_ref record.Recordops.s_CONST) in
+                 List.map_filter complete_field remaining_projs in
                List.rev_append remaining_fields acc
         in
-        let unsorted_indexed_fields =
-          index_fields other_fields proj_list
-            [(first_field_index, first_field_value)] in
+        let unsorted_indexed_fields = index_fields fields proj_list [] in
         let sorted_indexed_fields =
           let cmp_by_index (i, _) (j, _) = Int.compare i j in
           List.sort cmp_by_index unsorted_indexed_fields in
@@ -1677,9 +1652,9 @@ let drop_notations_pattern looked_for genv =
             if get_asymmetric_patterns () then pl else
             let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in
             List.rev_append pars pl in
-          match drop_syndef top scopes head pl with
-            | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
-            | None -> raise (InternalizationError (loc,NotAConstructor head))
+          let (_,argscs) = find_remaining_scopes [] pl head in
+          let pats = List.map2 (in_pat_sc scopes) argscs pl in
+          DAst.make ?loc @@ RCPatCstr(head, [], pats)
       end
     | CPatCstr (head, None, pl) ->
       begin
@@ -2064,7 +2039,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
                      (fun _idx fieldname constructorname ->
                          let open Evar_kinds in
                          let fieldinfo : Evar_kinds.record_field =
-                             {fieldname=fieldname; recordname=inductive_of_constructor constructorname}
+                             {fieldname=Option.get fieldname; recordname=inductive_of_constructor constructorname}
                              in
                          CAst.make ?loc @@ CHole (Some
                  (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with
@@ -2076,10 +2051,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
           match fields with
             | None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.")
             | Some (n, constrname, args) ->
+                let args_scopes = find_arguments_scope constrname in
                 let pars = List.make n (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) in
-                let app = CAst.make ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
-          intern env app
-        end
+                let args = intern_args env args_scopes (List.rev_append pars args) in
+                let hd = DAst.make @@ GRef (constrname,None) in
+                DAst.make ?loc @@ GApp (hd, args)
+       end
     | CCases (sty, rtnpo, tms, eqns) ->
         let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
           (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na))
diff --git a/test-suite/coqdoc/Record.html.out b/test-suite/coqdoc/Record.html.out
new file mode 100644
index 0000000000..371188dfbe
--- /dev/null
+++ b/test-suite/coqdoc/Record.html.out
@@ -0,0 +1,34 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
+<link href="coqdoc.css" rel="stylesheet" type="text/css" />
+<title>Coqdoc.Record</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library Coqdoc.Record</h1>
+
+<div class="code">
+<span class="id" title="keyword">Record</span> <a id="a" class="idref" href="#a"><span class="id" title="record">a</span></a> := { <a id="b" class="idref" href="#b"><span class="id" title="projection">b</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> ; <a id="c" class="idref" href="#c"><span class="id" title="projection">c</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> }.<br/>
+<span class="id" title="keyword">Definition</span> <a id="d" class="idref" href="#d"><span class="id" title="definition">d</span></a> := {| <a class="idref" href="Coqdoc.Record.html#b"><span class="id" title="projection">b</span></a> := 0 ; <a class="idref" href="Coqdoc.Record.html#c"><span class="id" title="projection">c</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> |}.<br/>
+</div>
+</div>
+
+<div id="footer">
+<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
+</div>
+
+</div>
+
+</body>
+</html>
\ No newline at end of file
diff --git a/test-suite/coqdoc/Record.tex.out b/test-suite/coqdoc/Record.tex.out
new file mode 100644
index 0000000000..4130ea9472
--- /dev/null
+++ b/test-suite/coqdoc/Record.tex.out
@@ -0,0 +1,27 @@
+\documentclass[12pt]{report}
+\usepackage[utf8x]{inputenc}
+
+%Warning: tipa declares many non-standard macros used by utf8x to
+%interpret utf8 characters but extra packages might have to be added
+%such as "textgreek" for Greek letters not already in tipa
+%or "stmaryrd" for mathematical symbols.
+%Utf8 codes missing a LaTeX interpretation can be defined by using
+%\DeclareUnicodeCharacter{code}{interpretation}.
+%Use coqdoc's option -p to add new packages or declarations.
+\usepackage{tipa}
+
+\usepackage[T1]{fontenc}
+\usepackage{fullpage}
+\usepackage{coqdoc}
+\usepackage{amsmath,amssymb}
+\usepackage{url}
+\begin{document}
+\coqlibrary{Coqdoc.Record}{Library }{Coqdoc.Record}
+
+\begin{coqdoccode}
+\coqdocnoindent
+\coqdockw{Record} \coqdef{Coqdoc.Record.a}{a}{\coqdocrecord{a}} := \{ \coqdef{Coqdoc.Record.b}{b}{\coqdocprojection{b}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} ; \coqdef{Coqdoc.Record.c}{c}{\coqdocprojection{c}} : \coqexternalref{bool}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{bool}} \}.\coqdoceol
+\coqdocnoindent
+\coqdockw{Definition} \coqdef{Coqdoc.Record.d}{d}{\coqdocdefinition{d}} := \{| \coqref{Coqdoc.Record.b}{\coqdocprojection{b}} := 0 ; \coqref{Coqdoc.Record.c}{\coqdocprojection{c}} := \coqexternalref{true}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{true}} |\}.\coqdoceol
+\end{coqdoccode}
+\end{document}
diff --git a/test-suite/coqdoc/Record.v b/test-suite/coqdoc/Record.v
new file mode 100644
index 0000000000..f362aade98
--- /dev/null
+++ b/test-suite/coqdoc/Record.v
@@ -0,0 +1,2 @@
+Record a := { b : nat ; c : bool }.
+Definition d := {| b := 0 ; c := true |}.
diff --git a/test-suite/coqdoc/bug11194.html.out b/test-suite/coqdoc/bug11194.html.out
index 6fc6533e59..56bf6eaaca 100644
--- a/test-suite/coqdoc/bug11194.html.out
+++ b/test-suite/coqdoc/bug11194.html.out
@@ -20,7 +20,7 @@
 
 <div class="code">
 <span class="id" title="keyword">Record</span> <a id="a_struct" class="idref" href="#a_struct"><span class="id" title="record">a_struct</span></a> := { <a id="anum" class="idref" href="#anum"><span class="id" title="projection">anum</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> }.<br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="keyword">Structure</span> <a id="a_struct_0" class="idref" href="#a_struct_0"><span class="id" title="definition">a_struct_0</span></a> := {| <a class="idref" href="Coqdoc.bug11194.html#Build_a_struct"><span class="id" title="constructor">anum</span></a> <a class="idref" href="Coqdoc.bug11194.html#Build_a_struct"><span class="id" title="constructor">:=</span></a> <a class="idref" href="Coqdoc.bug11194.html#Build_a_struct"><span class="id" title="constructor">0</span></a>|}.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="keyword">Structure</span> <a id="a_struct_0" class="idref" href="#a_struct_0"><span class="id" title="definition">a_struct_0</span></a> := {| <a class="idref" href="Coqdoc.bug11194.html#anum"><span class="id" title="projection">anum</span></a> := 0|}.<br/>
 <span class="id" title="keyword">Definition</span> <a id="rename_a_s_0" class="idref" href="#rename_a_s_0"><span class="id" title="definition">rename_a_s_0</span></a> := <a class="idref" href="Coqdoc.bug11194.html#a_struct_0"><span class="id" title="definition">a_struct_0</span></a>.<br/>
 <span class="id" title="keyword">Coercion</span> <a id="some_nat" class="idref" href="#some_nat"><span class="id" title="definition">some_nat</span></a> := (@<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>).<br/>
 <span class="id" title="keyword">Definition</span> <a id="rename_some_nat" class="idref" href="#rename_some_nat"><span class="id" title="definition">rename_some_nat</span></a> := <a class="idref" href="Coqdoc.bug11194.html#some_nat"><span class="id" title="definition">some_nat</span></a>.<br/>
diff --git a/test-suite/coqdoc/bug11194.tex.out b/test-suite/coqdoc/bug11194.tex.out
index 243dc20e8f..a262b45fc8 100644
--- a/test-suite/coqdoc/bug11194.tex.out
+++ b/test-suite/coqdoc/bug11194.tex.out
@@ -22,7 +22,7 @@
 \coqdocnoindent
 \coqdockw{Record} \coqdef{Coqdoc.bug11194.a struct}{a\_struct}{\coqdocrecord{a\_struct}} := \{ \coqdef{Coqdoc.bug11194.anum}{anum}{\coqdocprojection{anum}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} \}.\coqdoceol
 \coqdocnoindent
-\coqdockw{Canonical} \coqdockw{Structure} \coqdef{Coqdoc.bug11194.a struct 0}{a\_struct\_0}{\coqdocdefinition{a\_struct\_0}} := \{| \coqref{Coqdoc.bug11194.Build a struct}{\coqdocconstructor{anum}} \coqref{Coqdoc.bug11194.Build a struct}{\coqdocconstructor{:=}} \coqref{Coqdoc.bug11194.Build a struct}{\coqdocconstructor{0}}|\}.\coqdoceol
+\coqdockw{Canonical} \coqdockw{Structure} \coqdef{Coqdoc.bug11194.a struct 0}{a\_struct\_0}{\coqdocdefinition{a\_struct\_0}} := \{| \coqref{Coqdoc.bug11194.anum}{\coqdocprojection{anum}} := 0|\}.\coqdoceol
 \coqdocnoindent
 \coqdockw{Definition} \coqdef{Coqdoc.bug11194.rename a s 0}{rename\_a\_s\_0}{\coqdocdefinition{rename\_a\_s\_0}} := \coqref{Coqdoc.bug11194.a struct 0}{\coqdocdefinition{a\_struct\_0}}.\coqdoceol
 \coqdocnoindent