letin are now sorted properly.

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 52918d9af1359017f94b3ffd4b6e6af5f534d528..bceb3ebc2b150f6b6b27722f58f0b23277177a08 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -89,7 +89,7 @@ let string_of_equality ?env eq =
               id w (CicPp.ppterm ty)
               (CicPp.ppterm left) 
               (Utils.string_of_comparison o) (CicPp.ppterm right)
-       (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
+        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
   | Some (_, context, _) -> 
       let names = Utils.names_of_context context in
       let w, _, (ty, left, right, o), m , id = open_equality eq in
@@ -97,7 +97,7 @@ let string_of_equality ?env eq =
               id w (CicPp.pp ty names)
               (CicPp.pp left names) (Utils.string_of_comparison o)
               (CicPp.pp right names)
-       (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
+        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
 ;;
 
 let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
@@ -522,12 +522,12 @@ let string_of_id names id =
     | Exact t -> 
         Printf.sprintf "%d = %s: %s = %s [%s]" id
           (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
-       (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
+        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
     | Step (_,(step,id1, (_,id2), _) ) ->
         Printf.sprintf "%6d: %s %6d %6d   %s = %s [%s]" id
           (string_of_rule step)
           id1 id2 (CicPp.pp l names) (CicPp.pp r names)
-       (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
+        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
   with
       Not_found -> assert false
 
@@ -549,6 +549,54 @@ let pp_proof names goalproof proof subst id initial_goal =
   "\nand then subsumed by " ^ string_of_int id ^ " when " ^ Subst.ppsubst subst
 ;;
 
+module OT = 
+  struct
+    type t = int
+    let compare = Pervasives.compare
+  end
+
+module M = Map.Make(OT)
+
+let rec find_deps m i = 
+  if M.mem i m then m
+  else 
+    let p,_,_ = proof_of_id i in
+    match p with
+    | Exact _ -> M.add i [] m
+    | Step (_,(_,id1,(_,id2),_)) -> 
+        let m = find_deps m id1 in
+        let m = find_deps m id2 in
+        M.add i (M.find id1 m @ M.find id2 m @ [id1;id2]) m
+;;
+
+let topological_sort l = 
+  (* build the partial order relation *)
+  let m = 
+    List.fold_left (fun m i -> find_deps m i)
+    M.empty l
+  in
+  let m = M.map (fun x -> Some x) m in
+  (* utils *)
+  let keys m = M.fold (fun i _ acc -> i::acc) m [] in
+  let split l m = List.filter (fun i -> M.find i m = Some []) l in
+  let purge l m = 
+    M.mapi 
+      (fun k v -> if List.mem k l then None else 
+         match v with
+         | None -> None
+         | Some ll -> Some (List.filter (fun i -> not (List.mem i l)) ll)) 
+      m
+  in
+  let rec aux m = 
+      let keys = keys m in
+      let ok = split keys m in
+      let m = purge ok m in
+      ok @ (if ok = [] then [] else aux m)
+  in
+  aux m
+;;
+  
+
 (* returns the list of ids that should be factorized *)
 let get_duplicate_step_in_wfo l p =
   let ol = List.rev l in
@@ -556,39 +604,33 @@ let get_duplicate_step_in_wfo l p =
   (* NOTE: here the n parameter is an approximation of the dependency 
      between equations. To do things seriously we should maintain a 
      dependency graph. This approximation is not perfect. *)
-  let add i n = 
+  let add i = 
     let p,_,_ = proof_of_id i in 
     match p with 
     | Exact _ -> true
     | _ -> 
         try 
-          let (pos,no) = Hashtbl.find h i in
-          Hashtbl.replace h i (pos,no+1);
+          let no = Hashtbl.find h i in
+          Hashtbl.replace h i (no+1);
           false
-        with Not_found -> Hashtbl.add h i (n,1);true
+        with Not_found -> Hashtbl.add h i 1;true
   in
-  let rec aux n = function
-    | Exact _ -> n
+  let rec aux = function
+    | Exact _ -> ()
     | Step (_,(_,i1,(_,i2),_)) -> 
-       let go_on_1 = add i1 n in
-       let go_on_2 = add i2 n in
-        max 
-         (if go_on_1 then aux (n+1) (let p,_,_ = proof_of_id i1 in p) else n+1)
-         (if go_on_2 then aux (n+1) (let p,_,_ = proof_of_id i2 in p) else n+1)
-  in
-  let i = aux 0 p in 
-  let _ = 
-    List.fold_left 
-      (fun acc (_,_,id,_,_) -> aux acc (let p,_,_ = proof_of_id id in p))
-      i ol
-  in
+        let go_on_1 = add i1 in
+        let go_on_2 = add i2 in
+        if go_on_1 then aux (let p,_,_ = proof_of_id i1 in p);
+        if go_on_2 then aux (let p,_,_ = proof_of_id i2 in p)
+  in
+  aux p;
+  List.iter
+    (fun (_,_,id,_,_) -> aux (let p,_,_ = proof_of_id id in p))
+    ol;
   (* now h is complete *)
-  let proofs = Hashtbl.fold (fun k (pos,count) acc->(k,pos,count)::acc) h [] in
-  let proofs = List.filter (fun (_,_,c) -> c > 1) proofs in
-  let proofs = 
-    List.sort (fun (_,c1,_) (_,c2,_) -> Pervasives.compare c2 c1) proofs 
-  in
-  List.map (fun (i,_,_) -> i) proofs
+  let proofs = Hashtbl.fold (fun k count acc-> (k,count)::acc) h [] in
+  let proofs = List.filter (fun (_,c) -> c > 1) proofs in
+  topological_sort (List.map (fun (i,_) -> i) proofs)
 ;;
 
 let build_proof_term h lift proof =
@@ -613,11 +655,11 @@ let build_proof_term h lift proof =
            | _ -> assert false
          in
          let p =   build_proof_step lift subst p1 p2 pos l r pred in
-(*      let cond =  (not (List.mem 302 (Utils.metas_of_term p)) || id1 = 8 || id1 = 132) in
-          if not cond then
-            prerr_endline ("ERROR " ^ string_of_int id1 ^ " " ^ string_of_int id2);
-          assert cond;*)
-          p
+(*         let cond =  (not (List.mem 302 (Utils.metas_of_term p)) || id1 = 8 || id1 = 132) in
+           if not cond then
+             prerr_endline ("ERROR " ^ string_of_int id1 ^ " " ^ string_of_int id2);
+           assert cond;*)
+           p
   in
    aux proof
 ;;
@@ -714,7 +756,7 @@ let fix_metas newmeta eq =
   let to_be_relocated = 
     HExtlib.list_uniq 
       (List.sort Pervasives.compare 
-        (Utils.metas_of_term left @ Utils.metas_of_term right)) 
+         (Utils.metas_of_term left @ Utils.metas_of_term right)) 
   in
   let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated in
   let ty = Subst.apply_subst subst ty in