X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fextlib%2Fdiscrimination_tree.mli;h=bf6b071f1ca2bc98f4aeebc5738ab068dc17489c;hb=5431da8145e4a84596d312fc02b552881d119100;hp=95e33d6ad43f0669354f0c53d8660afb381ce24b;hpb=3ba4306ecd693b48f70ecbe9916aec6975373549;p=helm.git diff --git a/matita/components/extlib/discrimination_tree.mli b/matita/components/extlib/discrimination_tree.mli index 95e33d6ad..bf6b071f1 100644 --- a/matita/components/extlib/discrimination_tree.mli +++ b/matita/components/extlib/discrimination_tree.mli @@ -63,8 +63,19 @@ module type DiscriminationTree = val in_index : t -> input -> (data -> bool) -> bool val retrieve_generalizations : t -> input -> dataset val retrieve_unifiables : t -> input -> dataset - val retrieve_generalizations_sorted : t -> input -> (data * int) list - val retrieve_unifiables_sorted : t -> input -> (data * int) list + + (* the int is the number of symbools that matched, note that + * Collector.to_list returns a sorted list, biggest matches first. *) + module type Collector = sig + type t + val empty : t + val union : t -> t -> t + val inter : t -> t -> data list + val to_list : t -> data list + end + module Collector : Collector + val retrieve_generalizations_sorted : t -> input -> Collector.t + val retrieve_unifiables_sorted : t -> input -> Collector.t end