+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
+ (* without the uniq there is a stack overflow doing concatenation *)
+ let xxx = [id1;id2] @ M.find id1 m @ M.find id2 m in
+ let xxx = HExtlib.list_uniq (List.sort Pervasives.compare xxx) in
+ M.add i xxx 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 = (* keep only deps inside l *)
+ List.fold_left
+ (fun m' i ->
+ M.add i (List.filter (fun x -> List.mem x l) (M.find i m)) m')
+ 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 res =
+ let keys = keys m in
+ let ok = split keys m in
+ let m = purge ok m in
+ let res = ok @ res in
+ if ok = [] then res else aux m res
+ in
+ let rc = List.rev (aux m []) in
+ rc
+;;
+
+