minor: in constrintern.ml:sort_fields, clarify build_patt

The code was a big "try..with" defining all useful quantities at
once. I tried to lift definitions out of this try..with to define them
as early as possible: the record's information and the first field
name are fetched before processing the other fields.

There were two calls in the try..with body that could raise the
Not_found exception (or at least I don't know the code well enough to
be sure that either of them cannot): `shortest_qualid_of_global` and
`build_patt`. They are now split in two separate try..with blocks,
both raising the same exception (with a shared error message named
`env_error_msg`). Someone familiar with the invariants at play could
probably remove one of the two blocks, streamlining the code even
further.

I'm a bit surprised by the main logic part (the big (if .. else if
.. else if ..) block in the new code), and there is a question in
a comment. I hope to get it answered during code review and remove it
(and maybe simplify the code).

Finally, there was an apparently-stale comment in the code:
  (* insertion of Constextern.reference_global *)
of course Constextern.reference_global corresponds to now function
that I could find. After trying to understand the meaning of this
comment, I decided to just remove it.

1 files changed, 54 insertions, 42 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index dc80140d4..3bd03aecc 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1038,52 +1038,64 @@ let sort_fields ~complete loc l completer =
      when pattern-matching, the list of fields may be partial. *)
   match l with
     | [] -> None
-    | (refer, value)::rem ->
-        let (nparams,          (* the number of parameters *)
-             base_constructor, (* the reference constructor of the record *)
-             (max,             (* number of params *)
-              (first_index,    (* index of the first field of the record *)
-               list_proj)))    (* list of projections *)
+    | (first_field_ref, first_field_value):: other_fields ->
+        let env_error_msg = "Environment corruption for records." in
+        let first_field_glob_ref =
+          try global_reference_of_reference first_field_ref
+          with Not_found -> anomaly (Pp.str env_error_msg) in
+        let record =
+          try Recordops.find_projection first_field_glob_ref
+          with Not_found ->
+            user_err_loc (loc_of_reference first_field_ref, "intern",
+                          pr_reference first_field_ref ++ str": Not a projection")
+        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 = ConstructRef record.Recordops.s_CONST in
+          try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id)
+          with Not_found -> anomaly (Pp.str env_error_msg) 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 *)
           =
-          let record =
-            try Recordops.find_projection
-              (global_reference_of_reference refer)
-            with Not_found ->
-              user_err_loc (loc_of_reference refer, "intern", pr_reference refer ++ str": Not a projection")
-            in
-          (* elimination of the first field from the projections *)
-          let rec build_patt l m i acc =
-            match l with
-              | [] -> (i, acc)
-              | (Some name) :: b ->
-                 begin match m with
+          (* elimitate 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 name) :: projs ->
+                 let field_glob_ref = ConstRef name in
+                 let first_field = eq_gr field_glob_ref first_field_glob_ref in
+                 begin match proj_kinds with
                     | [] -> anomaly (Pp.str "Number of projections mismatch")
-                    | (_, regular)::tm ->
-                       begin match global_reference_of_reference refer with
-                       | ConstRef name' when eq_constant name name' ->
-                         if not regular && complete then
-                           user_err_loc (loc, "", str "No local fields allowed in a record construction.")
-                         else build_patt b tm (i + 1) (i, snd acc) (* we found it *)
-                       | _ ->
-                          build_patt b tm
-                            (if not regular && complete then i else i + 1)
-                            (if not regular && complete then acc
-                             else fst acc, (i, ConstRef name) :: snd acc)
-                       end
+                    | (_, regular) :: proj_kinds ->
+                       if first_field && not regular && complete then
+                         (* G.S.: why do we fail only in the
+                            first-field case? I would expect to fail
+                            whenever (not regular && complete), and
+                            skip the fields only when (not complete *)
+                         user_err_loc (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_ref) :: acc)
                  end
-              | None :: b-> (* we don't want anonymous fields *)
+              | None :: projs ->
                  if complete then
+                   (* we don't want anonymous fields *)
                    user_err_loc (loc, "", str "This record contains anonymous fields.")
-                 else build_patt b m (i+1) acc
-                   (* anonymous arguments don't appear in m *)
-          in
-          let ind = record.Recordops.s_CONST in
-          try (* insertion of Constextern.reference_global *)
-            (record.Recordops.s_EXPECTEDPARAM,
-             Qualid (loc, shortest_qualid_of_global Id.Set.empty (ConstructRef ind)),
-             build_patt record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 (0,[]))
-          with Not_found -> anomaly (Pp.str "Environment corruption for records.")
+                 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
         (* now we want to have all fields of the pattern indexed by their place in
            the constructor *)
         let rec sf patts accpatt =
@@ -1109,7 +1121,7 @@ let sort_fields ~complete loc l completer =
                let (index, projs) = add_patt (snd accpatt) [] in
                  sf q ((index, patt)::fst accpatt, projs) in
         let (unsorted_indexed_pattern, remainings) =
-          sf rem ([first_index, value], list_proj) in
+          sf other_fields ([first_field_index, first_field_value], proj_list) in
         (* we sort them *)
         let sorted_indexed_pattern =
           let cmp_by_index (i, _) (j, _) = Int.compare i j in
@@ -1120,7 +1132,7 @@ let sort_fields ~complete loc l completer =
         (* a function to remove indice *)
         let rec clean_list l i acc =
           match l with
-            | [] -> complete_list (max - i) acc
+            | [] -> complete_list (end_index - i) acc
             | (k, p)::q-> clean_list q k (p::(complete_list (k - i) acc))
           in
         Some (nparams, base_constructor,