Add checks for invalid occurrences in setoid rewrite.

We additionally check that occurrence 0 is invalid in simpl at,
unfold at, etc.

8 files changed, 133 insertions, 114 deletions

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 0b5d36b845..4a2c298caa 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -608,7 +608,7 @@ END
 {
 
 let subst_var_with_hole occ tid t =
-  let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in
+  let occref = if occ > 0 then ref occ else Locusops.error_invalid_occurrence [occ] in
   let locref = ref 0 in
   let rec substrec x = match DAst.get x with
     | GVar id ->
@@ -628,7 +628,7 @@ let subst_var_with_hole occ tid t =
     | _ -> map_glob_constr_left_to_right substrec x in
   let t' = substrec t
   in
-  if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t'
+  if !occref > 0 then Locusops.error_invalid_occurrence [occ] else t'
 
 let subst_hole_with_term occ tc t =
   let locref = ref 0 in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 77162ce89a..59533eb3e3 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -855,26 +855,20 @@ let coerce env cstr res =
   let res = { res with rew_evars = evars } in
     apply_constraint env res.rew_car rel prf cstr res
 
-let apply_rule unify loccs : int pure_strategy =
-  let (nowhere_except_in,occs) = convert_occs loccs in
-  let is_occ occ =
-    if nowhere_except_in
-    then List.mem occ occs
-    else not (List.mem occ occs)
-  in
-  { strategy = fun { state = occ ; env ;
+let apply_rule unify : occurrences_count pure_strategy =
+  { strategy = fun { state = occs ; env ;
                      term1 = t ; ty1 = ty ; cstr ; evars } ->
       let unif = if isEvar (goalevars evars) t then None else unify env evars t in
         match unif with
-        | None -> (occ, Fail)
+        | None -> (occs, Fail)
         | Some rew ->
-          let occ = succ occ in
-            if not (is_occ occ) then (occ, Fail)
-            else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity)
+          let b, occs = update_occurrence_counter occs in
+            if not b then (occs, Fail)
+            else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occs, Identity)
             else
               let res = { rew with rew_car = ty } in
               let res = Success (coerce env cstr res) in
-              (occ, res)
+              (occs, res)
     }
 
 let apply_lemma l2r flags oc by loccs : strategy = { strategy =
@@ -890,9 +884,10 @@ let apply_lemma l2r flags oc by loccs : strategy = { strategy =
       | None -> None
       | Some rew -> Some rew
     in
-    let _, res = (apply_rule unify loccs).strategy { input with
-                                                     state = 0 ;
+    let loccs, res = (apply_rule unify).strategy { input with
+                                                     state = initialize_occurrence_counter loccs ;
                                                      evars } in
+    check_used_occurrences loccs;
     (), res
                                                    }
 
@@ -1423,12 +1418,13 @@ let rewrite_with l2r flags c occs : strategy = { strategy =
       let (sigma, rew) = refresh_hypinfo env sigma c in
       unify_eqn rew l2r flags env (sigma, cstrs) None t
     in
-    let app = apply_rule unify occs in
+    let app = apply_rule unify in
     let strat =
       Strategies.fix (fun aux ->
         Strategies.choice app (subterm true default_flags aux))
     in
-    let _, res = strat.strategy { input with state = 0 } in
+    let occs, res = strat.strategy { input with state = initialize_occurrence_counter occs } in
+    check_used_occurrences occs;
     ((), res)
                                                }
 
@@ -2076,11 +2072,12 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals =
   Proofview.Goal.enter begin fun gl ->
   let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in
   let unify env evars t = unify_abs res l2r sort env evars t in
-  let app = apply_rule unify occs in
+  let app = apply_rule unify in
   let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in
   let substrat = Strategies.fix recstrat in
   let strat = { strategy = fun ({ state = () } as input) ->
-    let _, res = substrat.strategy { input with state = 0 } in
+    let occs, res = substrat.strategy { input with state = initialize_occurrence_counter occs } in
+    check_used_occurrences occs;
     (), res
               }
   in
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 =
diff --git a/test-suite/success/rewrite_in.v b/test-suite/success/rewrite_in.v
index 29fe915ff4..3433866239 100644
--- a/test-suite/success/rewrite_in.v
+++ b/test-suite/success/rewrite_in.v
@@ -5,4 +5,10 @@ Goal forall (P Q : Prop) (f:P->Prop) (p:P), (P<->Q) -> f p -> True.
   rewrite H in p || trivial.
 Qed.
 
-
+Goal 1 = 0 -> 0 = 1.
+  intro H.
+  Fail rewrite H at 1 2 3. (* bug #13566 *)
+  Fail rewrite H at 0.
+  rewrite H at 1.
+  reflexivity.
+Qed.