fixing problem with CompCert: reordering resulting from tac change was not closed w.r.t. dependencies

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11634 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 22 insertions, 34 deletions

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 99252ce65..24ab23f4a 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -1058,6 +1058,19 @@ let global_vars_set_of_decl env = function
       Idset.union (global_vars_set env t)
         (global_vars_set env c)
 
+let dependency_closure env sign hyps =
+  if Idset.is_empty hyps then [] else
+    let (_,lh) =
+      Sign.fold_named_context_reverse
+        (fun (hs,hl) (x,_,_ as d) ->
+          if Idset.mem x hs then
+            (Idset.union (global_vars_set_of_decl env d) (Idset.remove x hs),
+            x::hl)
+          else (hs,hl))
+        ~init:(hyps,[])
+        sign in
+    List.rev lh
+
 let default_x = id_of_string "x"
 
 let rec next_name_away_in_cases_pattern id avoid =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index f5f1a459f..ccdb98031 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -255,6 +255,10 @@ val make_all_name_different : env -> env
 val global_vars : env -> constr -> identifier list
 val global_vars_set_of_decl : env -> named_declaration -> Idset.t
 
+(* Gives an ordered list of hypotheses, closed by dependencies,
+   containing a given set *)
+val dependency_closure : env -> named_context -> Idset.t -> identifier list
+
 (* Test if an identifier is the basename of a global reference *)
 val is_section_variable : identifier -> bool
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 391d6f466..83693827c 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -143,8 +143,7 @@ let mt_q = (Idmap.empty,[])
 let push_val y = function
     (_,[] as q) -> q
   | (m, (x,l)::q) -> (m, (x,Idset.add y l)::q)
-let push_item x v q =
-  let (m,l) = push_val x q in
+let push_item x v (m,l) =
   (Idmap.add x v m, (x,Idset.empty)::l)
 let mem_q x (m,_) = Idmap.mem x m
 let rec find_q x (m,q) =
@@ -158,7 +157,7 @@ let rec find_q x (m,q) =
     | (x',l as i)::((x'',l'')::q as itl) ->
         if x=x' then
           ((v,Idset.union accs l),
-           (m',List.rev acc@(x'',Idset.union l l'')::q))
+           (m',List.rev acc@(x'',Idset.add x (Idset.union l l''))::q))
         else find (Idset.union l accs) (i::acc) itl in
   find Idset.empty [] q
 
@@ -200,43 +199,15 @@ let reorder_val_context env sign ord =
   val_of_named_context (reorder_context env (named_context_of_val sign) ord)
 
 
+
+
 let check_decl_position env sign (x,_,_ as d) =
   let needed = global_vars_set_of_decl env d in
-  let deps =
-    list_map_filter (fun (id,_,_) ->
-      if Idset.mem id needed then Some id else None)
-      (named_context_of_val sign) in
+  let deps = dependency_closure env (named_context_of_val sign) needed in
   if List.mem x deps then
     error ("Cannot create self-referring hypothesis "^string_of_id x);
   x::deps
 
-
-(******)
-(* older version (performs more swapping) 
-let reorder_context sign ord =
-  let ords = List.fold_left Idset.add Idset.empty sign in
-  let rec step expected moved_hyps ctxt_head ctxt_tail =
-    if not (Idset.is_empty expected) then
-      match ctxt_head with
-          [] -> failwith "some hyps not found" (* those in expected *)
-        | (x,_,_ as d) :: ctxt ->
-            if Idset.mem x expected then
-              step
-                (Idset.remove x expected)
-                (Idmap.add x (d,Idset.empty) move_hyps)
-                ctxt ctxt_tail
-            else
-              step expected (push_hyp x moved_hyps) ctxt (d::ctxt_tail)
-    else begin
-      (* TODO: check free var constraints *)
-      let ctxt_mid =
-        List.map (fun h -> fst (Idmap.find h moved_hyps)) ords
-
-      in List.rev ctxt_tail @ ctxt_mid @ ctxt_head
-    end in
-  step ords Idmap.empty sign []
-*)
-
 (* Auxiliary functions for primitive MOVE tactic
  *
  * [move_hyp with_dep toleft (left,(hfrom,typfrom),right) hto] moves