Merge PR coq#18221: Fix various issues around recarg computation

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <[email protected]>

interp/constrexpr_ops.ml

@@ -551,46 +551,6 @@ let patntn_loc ?loc (args,argslist,binders) =
 let error_invalid_pattern_notation ?loc () =
   CErrors.user_err ?loc  (str "Invalid notation for pattern.")
 
-(* Interpret the index of a recursion order annotation *)
-let split_at_annot bl na =
-  let open CAst in
-  let names = List.map (fun { v } -> v) (names_of_local_assums bl) in
-  match na with
-  | None ->
-    begin match names with
-      | [] -> CErrors.user_err (Pp.str "A fixpoint needs at least one parameter.")
-      | _ -> ([], bl)
-    end
-  | Some { loc; v = id } ->
-    let rec aux acc = function
-      | CLocalAssum (bls, k, t) as x :: rest ->
-        let test { CAst.v = na } = match na with
-          | Name id' -> Id.equal id id'
-          | Anonymous -> false
-        in
-        let l, r = List.split_when test bls in
-        begin match r with
-          | [] -> aux (x :: acc) rest
-          | _ ->
-            let ans = match l with
-              | [] -> acc
-              | _ -> CLocalAssum (l, k, t) :: acc
-            in
-            (List.rev ans, CLocalAssum (r, k, t) :: rest)
-        end
-      | CLocalDef ({ CAst.v = na },_,_) as x :: rest ->
-        if Name.equal (Name id) na then
-          CErrors.user_err ?loc
-            (Id.print id ++ str" must be a proper parameter and not a local definition.")
-        else
-          aux (x :: acc) rest
-      | CLocalPattern _ :: rest ->
-        Loc.raise ?loc (Gramlib.Grammar.Error "pattern with quote not allowed after fix")
-      | [] ->
-        CErrors.user_err ?loc
-          (str "No parameter named " ++ Id.print id ++ str".")
-    in aux [] bl
-
 (** Pseudo-constructors *)
 
 let mkIdentC id   = CAst.make @@ CRef (qualid_of_ident id,None)

interp/constrexpr_ops.mli

@@ -124,8 +124,6 @@ val occur_var_constr_expr : Id.t -> constr_expr -> bool
 (** Return all (non-qualified) names treating binders as names *)
 val names_of_constr_expr : constr_expr -> Id.Set.t
 
-val split_at_annot : local_binder_expr list -> lident option -> local_binder_expr list * local_binder_expr list
-
 val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> notation -> (int * int) list
 val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> notation -> (int * int) list
 

interp/constrintern.ml

@@ -2171,12 +2171,22 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
                let (env',bl) = List.fold_left intern_local_binder (env,[]) bl in
                let bl = List.rev_map glob_local_binder_of_extended bl in
                let n = Option.map (fun recarg ->
-                   List.fold_left_until (fun n (id,_,body,_) -> match body with
-                       | None ->
-                         if Name.equal id (Name recarg.v) then Stop n else Cont (n+1)
-                       | Some _ -> Cont n (* let-ins don't count *))
-                     0 bl)
-                   recarg
+                 let exception Found of int in
+                 try
+                   List.fold_left (fun n (id,_,body,_) ->
+                     match body, Name.equal id (Name recarg.v) with
+                     | None, true -> raise (Found n)
+                     | Some _, true ->
+                         CErrors.user_err ?loc
+                           (Name.print id ++ str" must be a proper parameter and not a local definition.")
+                     | None, false -> n + 1
+                     | Some _, false -> n (* let-ins don't count *))
+                     0 bl |> ignore;
+                   CErrors.user_err ?loc:recarg.loc
+                     (str "No parameter named " ++ Id.print recarg.v ++ str".");
+                 with
+                   Found k -> k)
+                 recarg
                in
                let bl_impls = remember_binders_impargs env' bl in
                (n, bl, intern_type env' ty, bl_impls)) dl in

pretyping/pretyping.ml

@@ -93,6 +93,9 @@ let search_guard ?loc env possible_indexes fixdefs =
     indexes
   else
     (* we now search recursively among all combinations *)
+    let combinations = List.combinations possible_indexes in
+    if List.is_empty combinations then
+      user_err ?loc (Pp.str "A fixpoint needs at least one parameter.");
     (try
        List.iter
          (fun l ->
@@ -109,7 +112,7 @@ let search_guard ?loc env possible_indexes fixdefs =
               let env = Environ.set_typing_flags flags env in
               check_fix env fix; raise (Found indexes)
             with TypeError _ -> ())
-         (List.combinations possible_indexes);
+          combinations;
        let errmsg = "Cannot guess decreasing argument of fix." in
          user_err ?loc (Pp.str errmsg)
      with Found indexes -> indexes)
@@ -813,7 +816,7 @@ struct
             Array.to_list (Array.mapi
                              (fun i annot -> match annot with
                              | Some n -> [n]
-                             | None -> List.map_i (fun i _ -> i) 0 ctxtv.(i))
+                             | None -> List.interval 0 (Context.Rel.nhyps ctxtv.(i) - 1))
            vn)
           in
           let fixdecls = (names,ftys,fdefs) in

test-suite/bugs/bug_18215.v

@@ -0,0 +1,5 @@
+Fail Definition a := fix f {struct unbound} :=
+  fun (t : unit) => tt.
+
+Generalizable Variable A.
+Fixpoint fails `(l : list A) {struct l} : unit := tt.

vernac/comFixpoint.ml

@@ -103,17 +103,31 @@ let check_true_recursivity env evd ~isfix fixl =
     | [x,Inr []] -> warn_non_recursive (x,isfix)
     | _ -> ()
 
+(* Interpret the index of a recursion order annotation *)
+exception Found of int
+let find_rec_annot bl ctx na =
+  let name = Name na.CAst.v in
+  try
+    Context.Rel.fold_outside (fun decl n ->
+      match Context.Rel.Declaration.(get_value decl, Name.equal (get_name decl) name) with
+      | None, true -> raise (Found n)
+      | Some _, true ->
+          let loc = List.find_map (fun id -> if Name.equal name id.CAst.v then Some id.CAst.loc else None) (Constrexpr_ops.names_of_local_binders bl) in
+          let loc = Option.default na.CAst.loc loc in
+          CErrors.user_err ?loc
+            (Name.print name ++ str" must be a proper parameter and not a local definition.")
+      | None, false -> n + 1
+      | Some _, false -> n (* let-ins don't count *))
+      ~init:0 ctx |> ignore;
+    CErrors.user_err ?loc:na.loc
+      (str "No parameter named " ++ Id.print na.v ++ str".");
+  with
+    Found k -> k
+
 let interp_fix_context ~program_mode ~cofix env sigma fix =
-  let before, after =
-    if not cofix
-    then Constrexpr_ops.split_at_annot fix.Vernacexpr.binders fix.Vernacexpr.rec_order
-    else [], fix.Vernacexpr.binders in
-  let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in
-  let sigma, (impl_env', ((env'', ctx'), imps')) =
-    interp_context_evars ~program_mode ~impl_env env' sigma after
-  in
-  let annot = Option.map (fun _ -> List.length (Termops.assums_of_rel_context ctx)) fix.Vernacexpr.rec_order in
-  sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
+  let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma fix.Vernacexpr.binders in
+  let annot = Option.map (find_rec_annot fix.Vernacexpr.binders ctx) fix.Vernacexpr.rec_order in
+  sigma, ((env', ctx), (impl_env, imps), annot)
 
 let interp_fix_ccl ~program_mode sigma impls (env,_) fix =
   let flags = Pretyping.{ all_no_fail_flags with program_mode } in