From 89c1ac8061dd044b1625a4b5f2ca65226f3826ee Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Dec 2020 17:21:13 +0100
Subject: Preserve the context_val structure as much as possible in Logic.move.

Instead of going back and forth between the representations, we take
advantage of the fact we always leave context suffixes untouched.
---
 proofs/logic.ml | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 8b31c07f5e..b99148c98e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -170,9 +170,9 @@ let move_location_eq m1 m2 = match m1, m2 with
 | _ -> false
 
 let split_sign env sigma hfrom hto l =
-  let rec splitrec left toleft = function
-    | [] -> error_no_such_hypothesis env sigma hfrom
-    | d :: right ->
+  let rec splitrec left toleft sign = match EConstr.match_named_context_val sign with
+    | None -> error_no_such_hypothesis env sigma hfrom
+    | Some (d, _, right) ->
         let hyp = NamedDecl.get_id d in
         if Id.equal hyp hfrom then
           (left,right,d, toleft || move_location_eq hto MoveLast)
@@ -225,11 +225,10 @@ let move_hyp env sigma toleft (left,declfrom,right) hto =
   in
   let open EConstr in
   if toleft then
-    let right =
-      List.fold_right push_named_context_val right empty_named_context_val in
     List.fold_left (fun sign d -> push_named_context_val d sign)
       right (moverec [] [declfrom] left)
   else
+    let right = named_context_of_val right in
     let right =
       List.fold_right push_named_context_val
         (moverec [] [declfrom] right) empty_named_context_val in
@@ -237,14 +236,12 @@ let move_hyp env sigma toleft (left,declfrom,right) hto =
       right left
 
 let move_hyp_in_named_context env sigma hfrom hto sign =
-  let open EConstr in
   let (left,right,declfrom,toleft) =
-    split_sign env sigma hfrom hto (named_context_of_val sign) in
+    split_sign env sigma hfrom hto sign in
   move_hyp env sigma toleft (left,declfrom,right) hto
 
 let insert_decl_in_named_context env sigma decl hto sign =
-  let open EConstr in
-  move_hyp env sigma false ([],decl,named_context_of_val sign) hto
+  move_hyp env sigma false ([],decl,sign) hto
 
 (**********************************************************************)
 
-- 
cgit v1.2.3


From 7ffd746e9156de69affaa3f284fce631ae0d6ef8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Dec 2020 18:00:52 +0100
Subject: Specialize the code of Logic.move.

---
 proofs/logic.ml | 96 +++++++++++++++++++++++++++++++--------------------------
 1 file changed, 53 insertions(+), 43 deletions(-)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index b99148c98e..2e8f8295fb 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -169,51 +169,36 @@ let move_location_eq m1 m2 = match m1, m2 with
 | MoveFirst, MoveFirst -> true
 | _ -> false
 
-let split_sign env sigma hfrom hto l =
-  let rec splitrec left toleft sign = match EConstr.match_named_context_val sign with
-    | None -> error_no_such_hypothesis env sigma hfrom
-    | Some (d, _, right) ->
-        let hyp = NamedDecl.get_id d in
-        if Id.equal hyp hfrom then
-          (left,right,d, toleft || move_location_eq hto MoveLast)
-        else
-          let is_toleft = match hto with
-          | MoveAfter h' | MoveBefore h' -> Id.equal hyp h'
-          | _ -> false
-          in
-          splitrec (d::left) (toleft || is_toleft)
-            right
+let mem_id_context id ctx = Id.Map.mem id ctx.Environ.env_named_map
+
+let split_sign env sigma hfrom l =
+  let () = if not (mem_id_context hfrom l) then error_no_such_hypothesis env sigma hfrom in
+  let rec splitrec left sign = match EConstr.match_named_context_val sign with
+  | None -> assert false
+  | Some (d, _, right) ->
+    let hyp = NamedDecl.get_id d in
+    if Id.equal hyp hfrom then (left, right, d)
+    else splitrec (d :: left) right
   in
-    splitrec [] false l
-
-let hyp_of_move_location = function
-  | MoveAfter id -> id
-  | MoveBefore id -> id
-  | _ -> assert false
+  splitrec [] l
 
 let move_hyp env sigma toleft (left,declfrom,right) hto =
-  let test_dep d d2 =
-    if toleft
-    then occur_var_in_decl env sigma (NamedDecl.get_id d2) d
-    else occur_var_in_decl env sigma (NamedDecl.get_id d) d2
-  in
-  let rec moverec first middle = function
-    | [] ->
-        if match hto with MoveFirst | MoveLast -> false | _ -> true then
-          error_no_such_hypothesis env sigma (hyp_of_move_location hto);
-        List.rev first @ List.rev middle
+  let open EConstr in
+  let push_rev prefix sign = List.fold_left (fun accu d -> push_named_context_val d accu) sign prefix in
+  let rec moverec_toleft first middle = function
+    | [] -> List.rev first @ List.rev middle
     | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
         List.rev first @ List.rev middle @ right
     | d :: right ->
         let hyp = NamedDecl.get_id d in
         let (first',middle') =
-          if List.exists (test_dep d) middle then
+          if List.exists (fun d2 -> occur_var_in_decl env sigma (NamedDecl.get_id d2) d) middle then
             if not (move_location_eq hto (MoveAfter hyp)) then
               (first, d::middle)
             else
               user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++
                 pr_move_location Id.print hto ++
-                str (if toleft then ": it occurs in the type of " else ": it depends on ")
+                str ": it occurs in the type of "
                 ++ Id.print hyp ++ str ".")
           else
             (d::first, middle)
@@ -221,23 +206,48 @@ let move_hyp env sigma toleft (left,declfrom,right) hto =
         if move_location_eq hto (MoveAfter hyp) then
           List.rev first' @ List.rev middle' @ right
         else
-          moverec first' middle' right
+          moverec_toleft first' middle' right
+  in
+  let rec moverec_toright first middle right = match EConstr.match_named_context_val right with
+    | None -> push_rev first @@ push_rev middle right
+    | Some (d, _, _) when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
+        push_rev first @@ push_rev middle @@ right
+    | Some (d, _, right) ->
+        let hyp = NamedDecl.get_id d in
+        let (first',middle') =
+          if List.exists (fun d2 -> occur_var_in_decl env sigma hyp d2) middle then
+            if not (move_location_eq hto (MoveAfter hyp)) then
+              (first, d::middle)
+            else
+              user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++
+                pr_move_location Id.print hto ++
+                str ": it depends on "
+                ++ Id.print hyp ++ str ".")
+          else
+            (d::first, middle)
+        in
+        if move_location_eq hto (MoveAfter hyp) then
+          push_rev first' @@ push_rev middle' @@ right
+        else
+          moverec_toright first' middle' right
   in
-  let open EConstr in
   if toleft then
     List.fold_left (fun sign d -> push_named_context_val d sign)
-      right (moverec [] [declfrom] left)
+      right (moverec_toleft [] [declfrom] left)
   else
-    let right = named_context_of_val right in
-    let right =
-      List.fold_right push_named_context_val
-        (moverec [] [declfrom] right) empty_named_context_val in
-    List.fold_left (fun sign d -> push_named_context_val d sign)
-      right left
+    let right = moverec_toright [] [declfrom] right in
+    push_rev left @@ right
 
 let move_hyp_in_named_context env sigma hfrom hto sign =
-  let (left,right,declfrom,toleft) =
-    split_sign env sigma hfrom hto sign in
+  let (left, right, declfrom) = split_sign env sigma hfrom sign in
+  let toleft = match hto with
+  | MoveLast -> true
+  | MoveAfter id | MoveBefore id ->
+    if mem_id_context id right then false
+    else if mem_id_context id sign then true
+    else error_no_such_hypothesis env sigma id
+  | MoveFirst -> false
+  in
   move_hyp env sigma toleft (left,declfrom,right) hto
 
 let insert_decl_in_named_context env sigma decl hto sign =
-- 
cgit v1.2.3


From 4bdd1242d22e0870f2f0c97a83ece7e7eeeea7a1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Dec 2020 20:06:33 +0100
Subject: Do not construct intermediate lists in Logic.move.

---
 proofs/logic.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2e8f8295fb..c57a9344ff 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -184,11 +184,12 @@ let split_sign env sigma hfrom l =
 
 let move_hyp env sigma toleft (left,declfrom,right) hto =
   let open EConstr in
+  let push prefix sign = List.fold_right push_named_context_val prefix sign in
   let push_rev prefix sign = List.fold_left (fun accu d -> push_named_context_val d accu) sign prefix in
-  let rec moverec_toleft first middle = function
-    | [] -> List.rev first @ List.rev middle
+  let rec moverec_toleft ans first middle = function
+    | [] -> push middle @@ push first ans
     | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
-        List.rev first @ List.rev middle @ right
+      push_rev right @@ push middle @@ push first ans
     | d :: right ->
         let hyp = NamedDecl.get_id d in
         let (first',middle') =
@@ -204,9 +205,9 @@ let move_hyp env sigma toleft (left,declfrom,right) hto =
             (d::first, middle)
         in
         if move_location_eq hto (MoveAfter hyp) then
-          List.rev first' @ List.rev middle' @ right
+          push_rev right @@ push middle' @@ push first' ans
         else
-          moverec_toleft first' middle' right
+          moverec_toleft ans first' middle' right
   in
   let rec moverec_toright first middle right = match EConstr.match_named_context_val right with
     | None -> push_rev first @@ push_rev middle right
@@ -232,8 +233,7 @@ let move_hyp env sigma toleft (left,declfrom,right) hto =
           moverec_toright first' middle' right
   in
   if toleft then
-    List.fold_left (fun sign d -> push_named_context_val d sign)
-      right (moverec_toleft [] [declfrom] left)
+    moverec_toleft right [] [declfrom] left
   else
     let right = moverec_toright [] [declfrom] right in
     push_rev left @@ right
-- 
cgit v1.2.3


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 +++---
 proofs/logic.ml    | 32 ++++++++++++++++++--------------
 3 files changed, 34 insertions(+), 17 deletions(-)

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
diff --git a/proofs/logic.ml b/proofs/logic.ml
index c57a9344ff..f5c84be465 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -186,56 +186,60 @@ let move_hyp env sigma toleft (left,declfrom,right) hto =
   let open EConstr in
   let push prefix sign = List.fold_right push_named_context_val prefix sign in
   let push_rev prefix sign = List.fold_left (fun accu d -> push_named_context_val d accu) sign prefix in
-  let rec moverec_toleft ans first middle = function
+  let rec moverec_toleft ans first middle midvars = function
     | [] -> push middle @@ push first ans
     | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
       push_rev right @@ push middle @@ push first ans
     | d :: right ->
         let hyp = NamedDecl.get_id d in
-        let (first',middle') =
-          if List.exists (fun d2 -> occur_var_in_decl env sigma (NamedDecl.get_id d2) d) middle then
+        let (first', middle', midvars') =
+          if occur_vars_in_decl env sigma midvars d then
             if not (move_location_eq hto (MoveAfter hyp)) then
-              (first, d::middle)
+              (first, d :: middle, Id.Set.add hyp midvars)
             else
               user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++
                 pr_move_location Id.print hto ++
                 str ": it occurs in the type of "
                 ++ Id.print hyp ++ str ".")
           else
-            (d::first, middle)
+            (d::first, middle, midvars)
         in
         if move_location_eq hto (MoveAfter hyp) then
           push_rev right @@ push middle' @@ push first' ans
         else
-          moverec_toleft ans first' middle' right
+          moverec_toleft ans first' middle' midvars' right
   in
-  let rec moverec_toright first middle right = match EConstr.match_named_context_val right with
+  let rec moverec_toright first middle depvars right = match EConstr.match_named_context_val right with
     | None -> push_rev first @@ push_rev middle right
     | Some (d, _, _) when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
         push_rev first @@ push_rev middle @@ right
     | Some (d, _, right) ->
         let hyp = NamedDecl.get_id d in
-        let (first',middle') =
-          if List.exists (fun d2 -> occur_var_in_decl env sigma hyp d2) middle then
+        let (first', middle', depvars') =
+          if Id.Set.mem hyp depvars then
             if not (move_location_eq hto (MoveAfter hyp)) then
-              (first, d::middle)
+              let vars = global_vars_set_of_decl env sigma d in
+              let depvars = Id.Set.union vars depvars in
+              (first, d::middle, depvars)
             else
               user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++
                 pr_move_location Id.print hto ++
                 str ": it depends on "
                 ++ Id.print hyp ++ str ".")
           else
-            (d::first, middle)
+            (d::first, middle, depvars)
         in
         if move_location_eq hto (MoveAfter hyp) then
           push_rev first' @@ push_rev middle' @@ right
         else
-          moverec_toright first' middle' right
+          moverec_toright first' middle' depvars' right
   in
   if toleft then
-    moverec_toleft right [] [declfrom] left
+    let id = NamedDecl.get_id declfrom in
+    moverec_toleft right [] [declfrom] (Id.Set.singleton id) left
   else
-    let right = moverec_toright [] [declfrom] right in
+    let depvars = global_vars_set_of_decl env sigma declfrom in
+    let right = moverec_toright [] [declfrom] depvars right in
     push_rev left @@ right
 
 let move_hyp_in_named_context env sigma hfrom hto sign =
-- 
cgit v1.2.3