Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several tactics.

Reviewed-by: ppedrot

5 files changed, 108 insertions, 92 deletions

diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index bd717e2d1f..52e3364109 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -21,42 +21,15 @@ module NamedDecl = Context.Named.Declaration
 
 (** Processing occurrences *)
 
-type occurrence_error =
-  | InvalidOccurrence of int list
-  | IncorrectInValueOccurrence of Id.t
-
-let explain_invalid_occurrence l =
-  let l = List.sort_uniquize Int.compare l in
-  str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ")
-  ++ prlist_with_sep spc int l ++ str "."
-
 let explain_incorrect_in_value_occurrence id =
   Id.print id ++ str " has no value."
 
-let explain_occurrence_error = function
-  | InvalidOccurrence l -> explain_invalid_occurrence l
-  | IncorrectInValueOccurrence id -> explain_incorrect_in_value_occurrence id
-
-let error_occurrences_error e =
-  user_err  (explain_occurrence_error e)
-
-let error_invalid_occurrence occ =
-  error_occurrences_error (InvalidOccurrence occ)
-
-let check_used_occurrences nbocc (nowhere_except_in,locs) =
-  let rest = List.filter (fun o -> o >= nbocc) locs in
-  match rest with
-  | [] -> ()
-  | _ -> error_occurrences_error (InvalidOccurrence rest)
-
 let proceed_with_occurrences f occs x =
   match occs with
   | NoOccurrences -> x
   | occs ->
-    let plocs = Locusops.convert_occs occs in
-    assert (List.for_all (fun x -> x >= 0) (snd plocs));
-    let (nbocc,x) = f 1 x in
-    check_used_occurrences nbocc plocs;
+    let (occs,x) = f (Locusops.initialize_occurrence_counter occs) x in
+    Locusops.check_used_occurrences occs;
     x
 
 (** Applying a function over a named_declaration with an hypothesis
@@ -70,7 +43,7 @@ let map_named_declaration_with_hyploc f hyploc acc decl =
   in
   match decl,hyploc with
   | LocalAssum (id,_), InHypValueOnly ->
-      error_occurrences_error (IncorrectInValueOccurrence id.Context.binder_name)
+      user_err (explain_incorrect_in_value_occurrence id.Context.binder_name)
   | LocalAssum (id,typ), _ ->
       let acc,typ = f acc typ in acc, LocalAssum (id,typ)
   | LocalDef (id,body,typ), InHypTypeOnly ->
@@ -101,43 +74,43 @@ type 'a testing_function = {
    means all occurrences except the ones in l *)
 
 let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t =
-  let (nowhere_except_in,locs) = Locusops.convert_occs occs in
-  let maxocc = List.fold_right max locs 0 in
-  let pos = ref occ in
+  let count = ref (Locusops.initialize_occurrence_counter occs) in
   let nested = ref false in
-  let add_subst t subst =
+  let add_subst pos t subst =
     try
       test.testing_state <- test.merge_fun subst test.testing_state;
-      test.last_found <- Some ((cl,!pos),t)
+      test.last_found <- Some ((cl,pos),t)
     with NotUnifiable e when not like_first ->
       let lastpos = Option.get test.last_found in
-     raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,e)) in
+     raise (SubtermUnificationError (!nested,((cl,pos),t),lastpos,e)) in
   let rec substrec k t =
-    if nowhere_except_in && !pos > maxocc then t else
+    if Locusops.occurrences_done !count then t else
     try
       let subst = test.match_fun test.testing_state t in
-      if Locusops.is_selected !pos occs then
+      let selected, count' = Locusops.update_occurrence_counter !count in count := count';
+      if selected then
+        let pos = Locusops.current_occurrence !count in
         (if !nested then begin
           (* in case it is nested but not later detected as unconvertible,
              as when matching "id _" in "id (id 0)" *)
           let lastpos = Option.get test.last_found in
-          raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,None))
+          raise (SubtermUnificationError (!nested,((cl,pos),t),lastpos,None))
          end;
-         add_subst t subst; incr pos;
+         add_subst pos t subst;
          (* Check nested matching subterms *)
-         if not (Locusops.is_all_occurrences occs) && occs != Locus.NoOccurrences then
+         if Locusops.more_specific_occurrences !count then
            begin nested := true; ignore (subst_below k t); nested := false end;
          (* Do the effective substitution *)
          Vars.lift k (bywhat ()))
       else
-        (incr pos; subst_below k t)
+        subst_below k t
     with NotUnifiable _ ->
       subst_below k t
   and subst_below k t =
     map_constr_with_binders_left_to_right sigma (fun d k -> k+1) substrec k t
   in
   let t' = substrec 0 t in
-  (!pos, t')
+  (!count, t')
 
 let replace_term_occ_modulo evd occs test bywhat t =
   let occs',like_first =
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index 436b730a88..1ddae01e2b 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -65,6 +65,3 @@ val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first ->
 val subst_closed_term_occ_decl : env -> evar_map ->
   (occurrences * hyp_location_flag) or_like_first ->
   constr -> named_declaration -> named_declaration * evar_map
-
-(** Miscellaneous *)
-val error_invalid_occurrence : int list -> 'a
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 86352eb79a..256d61a32b 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Util
 open Locus
 
 (** Utilities on or_var *)
@@ -27,12 +28,43 @@ let occurrences_map f = function
     if l' = [] then AllOccurrences else AllOccurrencesBut l'
   | (NoOccurrences|AllOccurrences|AtLeastOneOccurrence) as o -> o
 
-let convert_occs = function
-  | AtLeastOneOccurrence -> (false,[])
-  | AllOccurrences -> (false,[])
-  | AllOccurrencesBut l -> (false,l)
-  | NoOccurrences -> (true,[])
-  | OnlyOccurrences l -> (true,l)
+type occurrences_count = {current: int; remaining: int list; where: (bool * int)}
+
+let error_invalid_occurrence l =
+  CErrors.user_err Pp.(str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ")
+  ++ prlist_with_sep spc int l ++ str ".")
+
+let initialize_occurrence_counter occs =
+  let (nowhere_except_in,occs) =
+    match occs with
+    | AtLeastOneOccurrence -> (false,[])
+    | AllOccurrences -> (false,[])
+    | AllOccurrencesBut l -> (false,List.sort_uniquize Int.compare l)
+    | NoOccurrences -> (true,[])
+    | OnlyOccurrences l -> (true,List.sort_uniquize Int.compare l) in
+  let max =
+    match occs with
+    | n::_ when n <= 0 -> error_invalid_occurrence [n]
+    | [] -> 0
+    | _ -> Util.List.last occs in
+  {current = 0; remaining = occs; where = (nowhere_except_in,max)}
+
+let update_occurrence_counter {current; remaining; where = (nowhere_except_in,_ as where)} =
+  let current = succ current in
+  match remaining with
+  | occ::remaining when Int.equal current occ -> (nowhere_except_in,{current;remaining;where})
+  | _ -> (not nowhere_except_in,{current;remaining;where})
+
+let check_used_occurrences {remaining} =
+  if not (Util.List.is_empty remaining) then error_invalid_occurrence remaining
+
+let occurrences_done {current; where = (nowhere_except_in,max)} =
+  nowhere_except_in && current > max
+
+let current_occurrence {current} = current
+
+let more_specific_occurrences {current; where = (_,max)} =
+  current <= max
 
 let is_selected occ = function
   | AtLeastOneOccurrence -> true
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
index 911ccc1a38..748bfbc252 100644
--- a/pretyping/locusops.mli
+++ b/pretyping/locusops.mli
@@ -20,13 +20,44 @@ val or_var_map : ('a -> 'b) -> 'a or_var -> 'b or_var
 val occurrences_map :
   ('a list -> 'b list) -> 'a occurrences_gen -> 'b occurrences_gen
 
-(** From occurrences to a list of positions (or complement of positions) *)
-val convert_occs : occurrences -> bool * int list
+(** {6 Counting occurrences} *)
+
+type occurrences_count
+  (** A counter of occurrences associated to a list of occurrences *)
+
+(** Three basic functions to initialize, count, and conclude a loop
+    browsing over subterms *)
+
+val initialize_occurrence_counter : occurrences -> occurrences_count
+  (** Initialize an occurrence_counter *)
+
+val update_occurrence_counter : occurrences_count -> bool * occurrences_count
+  (** Increase the occurrence counter by one and tell if the current occurrence is selected *)
+
+val check_used_occurrences : occurrences_count -> unit
+  (** Increase the occurrence counter and tell if the current occurrence is selected *)
+
+(** Auxiliary functions about occurrence counters *)
+
+val current_occurrence : occurrences_count -> int
+  (** Tell the value of the current occurrence *)
+
+val occurrences_done : occurrences_count -> bool
+  (** Tell if there are no more occurrences to select and if the loop
+      can be shortcut *)
+
+val more_specific_occurrences : occurrences_count -> bool
+  (** Tell if there are no more occurrences to select (or unselect)
+      and if an inner loop can be shortcut *)
+
+(** {6 Miscellaneous} *)
 
 val is_selected : int -> occurrences -> bool
 
 val is_all_occurrences : 'a occurrences_gen -> bool
 
+val error_invalid_occurrence : int list -> 'a
+
 (** Usual clauses *)
 
 val allHypsAndConcl : 'a clause_expr
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9cf7119709..c705ac16e7 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1046,28 +1046,23 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c =
   | _ -> map_constr_with_binders_left_to_right sigma g f acc c
 
 let e_contextually byhead (occs,c) f = begin fun env sigma t ->
-  let (nowhere_except_in,locs) = Locusops.convert_occs occs in
-  let maxocc = List.fold_right max locs 0 in
-  let pos = ref 1 in
+  let count = ref (Locusops.initialize_occurrence_counter occs) in
   (* FIXME: we do suspicious things with this evarmap *)
   let evd = ref sigma in
   let rec traverse nested (env,c as envc) t =
-    if nowhere_except_in && (!pos > maxocc) then (* Shortcut *) t
+    if Locusops.occurrences_done !count then (* Shortcut *) t
     else
     try
       let subst =
         if byhead then matches_head env sigma c t
         else Constr_matching.matches env sigma c t in
-      let ok =
-        if nowhere_except_in then Int.List.mem !pos locs
-        else not (Int.List.mem !pos locs) in
-      incr pos;
+      let ok, count' = Locusops.update_occurrence_counter !count in count := count';
       if ok then begin
         if Option.has_some nested then
-          user_err  (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str ".");
+          user_err  (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (Locusops.current_occurrence !count) ++ str ".");
         (* Skip inner occurrences for stable counting of occurrences *)
-        if locs != [] then
-          ignore (traverse_below (Some (!pos-1)) envc t);
+        if Locusops.more_specific_occurrences !count then
+          ignore (traverse_below (Some (Locusops.current_occurrence !count)) envc t);
         let (evm, t) = (f subst) env !evd t in
         (evd := evm; t)
       end
@@ -1087,7 +1082,7 @@ let e_contextually byhead (occs,c) f = begin fun env sigma t ->
           (traverse nested) envc sigma t
   in
   let t' = traverse None (env,c) t in
-  if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs;
+  Locusops.check_used_occurrences !count;
   (!evd, t')
   end
 
@@ -1105,28 +1100,25 @@ let match_constr_evaluable_ref sigma c evref =
   | Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty
   | _, _ -> None
 
-let substlin env sigma evalref n (nowhere_except_in,locs) c =
-  let maxocc = List.fold_right max locs 0 in
-  let pos = ref n in
-  assert (List.for_all (fun x -> x >= 0) locs);
+let substlin env sigma evalref occs c =
+  let count = ref (Locusops.initialize_occurrence_counter occs) in
   let value u = value_of_evaluable_ref env evalref u in
   let rec substrec () c =
-    if nowhere_except_in && !pos > maxocc then c
+    if Locusops.occurrences_done !count then c
     else
       match match_constr_evaluable_ref sigma c evalref with
       | Some u ->
-        let ok =
-          if nowhere_except_in then Int.List.mem !pos locs
-          else not (Int.List.mem !pos locs) in
-          incr pos;
-          if ok then value u else c
+        let ok, count' = Locusops.update_occurrence_counter !count in
+        count := count';
+        if ok then value u else c
       | None ->
         map_constr_with_binders_left_to_right sigma
           (fun _ () -> ())
           substrec () c
   in
   let t' = substrec () c in
-  (!pos, t')
+  Locusops.check_used_occurrences !count;
+  (Locusops.current_occurrence !count, t')
 
 let string_of_evaluable_ref env = function
   | EvalVarRef id -> Id.to_string id
@@ -1154,23 +1146,14 @@ let unfold env sigma name c =
  * at the occurrences of occ_list. If occ_list is empty, unfold all occurrences.
  * Performs a betaiota reduction after unfolding. *)
 let unfoldoccs env sigma (occs,name) c =
-  let unfo nowhere_except_in locs =
-    let (nbocc,uc) = substlin env sigma name 1 (nowhere_except_in,locs) c in
-    if Int.equal nbocc 1 then
+  match occs with
+  | NoOccurrences -> c
+  | AllOccurrences -> unfold env sigma name c
+  | OnlyOccurrences _ | AllOccurrencesBut _ | AtLeastOneOccurrence ->
+    let (occ,uc) = substlin env sigma name occs c in
+    if Int.equal occ 0 then
       user_err Pp.(str ((string_of_evaluable_ref env name)^" does not occur."));
-    let rest = List.filter (fun o -> o >= nbocc) locs in
-    let () = match rest with
-    | [] -> ()
-    | _ -> error_invalid_occurrence rest
-    in
     nf_betaiotazeta env sigma uc
-  in
-  match occs with
-    | NoOccurrences -> c
-    | AllOccurrences -> unfold env sigma name c
-    | OnlyOccurrences l -> unfo true l
-    | AllOccurrencesBut l -> unfo false l
-    | AtLeastOneOccurrence -> unfo false []
 
 (* Unfold reduction tactic: *)
 let unfoldn loccname env sigma c =