From 143c10b37e360a1d115904c46a954e86904ee203 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 8 Sep 2007 23:41:54 +0000
Subject: [PATCH] the order of abstraction is now correct, but there is an
 orrible hack to make eq_OF_eq have the right type.

---
 .../components/tactics/closeCoercionGraph.ml  | 41 +++++++++++++++++--
 1 file changed, 38 insertions(+), 3 deletions(-)

diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index d558c0ef0..95b9fd6e0 100644
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/components/tactics/closeCoercionGraph.ml
@@ -152,11 +152,40 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
       | t -> t
     in
     let skip_appl = function | Cic.Appl l -> List.tl l | _ -> assert false in
+    let rec metas_of_term_and_types t =
+      let metas = CicUtil.metas_of_term t in
+      let types = 
+       List.flatten       
+        (List.map 
+          (fun (i,_) -> try 
+            let _,_,ty = CicUtil.lookup_meta i body_metasenv in metas_of_term_and_types ty
+            with CicUtil.Meta_not_found _ -> []) 
+          metas)
+      in
+      metas @ types
+    in
+    let sorted_metas_of_term world t = 
+      let metas = metas_of_term_and_types t in
+      (* this check should be useless *)
+      let metas = List.filter (fun (i,_)->List.exists (fun (j,_,_) -> j=i) world) metas in
+      let order_metas metasenv metas = 
+        let module OT = struct type t = int let compare = Pervasives.compare end in
+        let module S = HTopoSort.Make (OT) in
+        let dep i = 
+          try 
+            let _,_,ty = List.find (fun (j,_,_) -> j=i) metasenv in
+            let metas = List.map fst (CicUtil.metas_of_term ty) in
+            HExtlib.list_uniq (List.sort Pervasives.compare metas)
+          with Not_found -> []
+        in
+          S.topological_sort (List.map (fun (i,_) -> i) metas) dep 
+      in 
+      order_metas world metas
+    in
     let metas_that_saturate l =
       List.fold_left 
         (fun (acc,n) t ->
-          let metas = CicUtil.metas_of_term t in
-          let metas = List.map fst metas in
+          let metas = sorted_metas_of_term body_metasenv t in
           let metas = 
             List.filter (fun i -> List.for_all (fun (j,_) -> j<>i) acc) metas in
           let metas = List.map (fun i -> i,n) metas in
@@ -181,7 +210,13 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
      with
       Failure _ -> assert false
     in
-    let meta2no = fst (metas_that_saturate (l_c2_b @ l_c1 @ l_c2_a)) in
+    (* BIG HACK ORRIBLE:
+     * it should be (l_c2_b @ l_c1 @ l_c2_a), but in this case sym (eq_f) gets
+     *  \A,B,f,x,y,Exy and not \B,A,f,x,y,Exy
+     * as an orrible side effect, the other composites get a type lyke
+     *  \A,x,y,Exy,B,f with 2 saturations
+     *)
+    let meta2no = fst (metas_that_saturate (l_c1 @ l_c2_b @ l_c2_a)) in
     let sorted =
      List.sort 
       (fun (i,ctx1,ty1) (j,ctx1,ty1) -> 
-- 
2.39.2