From f907c38ea57a42da7de279cc97db2bf5dc7d913b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 25 Oct 2004 14:39:44 +0000 Subject: [PATCH] sort hint's result accordingly to the "least goal left first" principle --- helm/ocaml/tactics/metadataQuery.ml | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 56bb93ac2..3fdecb8c5 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -63,10 +63,13 @@ let signature_of_hypothesis context = Constr.StringSet.union set (Constr.constants_of t)) Constr.StringSet.empty context -let intersect l1 l2 = - let set1 = List.fold_right Constr.StringSet.add l1 Constr.StringSet.empty in - let set2 = List.fold_right Constr.StringSet.add l2 Constr.StringSet.empty in - Constr.StringSet.elements (Constr.StringSet.inter set1 set2) +let intersect uris siguris = + let set1 = List.fold_right Constr.StringSet.add uris Constr.StringSet.empty in + let set2 = + List.fold_right Constr.StringSet.add siguris Constr.StringSet.empty + in + let inter = Constr.StringSet.inter set1 set2 in + List.filter (fun s -> Constr.StringSet.mem s inter) uris let filter_uris_forward ~dbh (main, constants) uris = let main_uris = @@ -130,8 +133,6 @@ let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) = end else filter_uris_backward ~dbh (main, other_constants) uris in -prerr_endline "URIS"; -List.iter prerr_endline uris; let rec aux = function | [] -> [] | uri :: tl -> @@ -154,7 +155,10 @@ List.iter prerr_endline uris; prerr_endline ("HO APPLICATO " ^ uri); status' :: aux tl) in - aux uris + List.stable_sort + (fun (_, (_, goals1)) (_, (_, goals2)) -> + Pervasives.compare (List.length goals1) (List.length goals2)) + (aux uris) let elim ~dbh uri = let constraints = -- 2.39.2