From 9caadc38de0e1c7b3362081da9482fc4455220a7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Dec 2020 20:27:42 +0100
Subject: More efficient variable membership check for Logic.move.

Instead of repeatedly crawling the same hypothesis again and again we
only iter the term once.
---
 engine/termops.ml  | 13 +++++++++++++
 engine/termops.mli |  6 +++---
 2 files changed, 16 insertions(+), 3 deletions(-)

(limited to 'engine')

diff --git a/engine/termops.ml b/engine/termops.ml
index d60aa69ccb..a0248fa01b 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -839,6 +839,16 @@ let occur_var env sigma id c =
   in
   try occur_rec c; false with Occur -> true
 
+let occur_vars env sigma ids c =
+  let rec occur_rec c =
+    match EConstr.destRef sigma c with
+    | gr, _ ->
+      let vars = vars_of_global env gr in
+      if not (Id.Set.is_empty (Id.Set.inter ids vars)) then raise Occur
+    | exception DestKO -> EConstr.iter sigma occur_rec c
+  in
+  try occur_rec c; false with Occur -> true
+
 exception OccurInGlobal of GlobRef.t
 
 let occur_var_indirectly env sigma id c =
@@ -853,6 +863,9 @@ let occur_var_indirectly env sigma id c =
 let occur_var_in_decl env sigma hyp decl =
   NamedDecl.exists (occur_var env sigma hyp) decl
 
+let occur_vars_in_decl env sigma hyps decl =
+  NamedDecl.exists (occur_vars env sigma hyps) decl
+
 let local_occur_var sigma id c =
   let rec occur c = match EConstr.kind sigma c with
   | Var id' -> if Id.equal id id' then raise Occur
diff --git a/engine/termops.mli b/engine/termops.mli
index bdde2c450d..0faebecb1b 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -89,9 +89,9 @@ val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool
 val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool
 val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool
 val occur_var_indirectly : env -> Evd.evar_map -> Id.t -> constr -> GlobRef.t option
-val occur_var_in_decl :
-  env -> Evd.evar_map ->
-  Id.t -> named_declaration -> bool
+val occur_var_in_decl : env -> Evd.evar_map -> Id.t -> named_declaration -> bool
+val occur_vars : env -> Evd.evar_map -> Id.Set.t -> constr -> bool
+val occur_vars_in_decl : env -> Evd.evar_map -> Id.Set.t -> named_declaration -> bool
 
 (** As {!occur_var} but assume the identifier not to be a section variable *)
 val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool
-- 
cgit v1.2.3