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(-)

(limited to 'proofs')

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