From a4a2345e2efaf4cc64aa4daf40e2bce05a400f12 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 11 Jan 2011 15:12:32 +0000 Subject: [PATCH] coercion lookup now returns coercions ranked using the number of symbols matched, the more precise match first --- .../components/extlib/discrimination_tree.ml | 70 +++++++++++++++++-- .../components/extlib/discrimination_tree.mli | 18 +++-- matita/components/ng_refiner/nCicCoercion.ml | 21 +++--- matita/components/ng_refiner/nCicCoercion.mli | 3 + 4 files changed, 90 insertions(+), 22 deletions(-) diff --git a/matita/components/extlib/discrimination_tree.ml b/matita/components/extlib/discrimination_tree.ml index d69228b0c..cdc498e9c 100644 --- a/matita/components/extlib/discrimination_tree.ml +++ b/matita/components/extlib/discrimination_tree.ml @@ -70,8 +70,17 @@ 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 + + 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 module Make (I:Indexable) (A:Set.S) : DiscriminationTree @@ -184,10 +193,61 @@ and type data = A.elt and type dataset = A.t = module O = struct type t = A.t * int - let compare (_,a) (_,b) = compare b a + let compare (sa,wa) (sb,wb) = + let c = compare wb wa in + if c <> 0 then c else A.compare sb sa end module S = Set.Make(O) + (* TASSI: here we should think of a smarted data structure *) + 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 with type t = S.t = struct + type t = S.t + let union = S.union + let empty = S.empty + + let merge l = + let rec aux s w = function + | [] -> [s,w] + | (t, wt)::tl when w = wt -> aux (A.union s t) w tl + | (t, wt)::tl -> (s, w) :: aux t wt tl + in + match l with + | [] -> [] + | (s, w) :: l -> aux s w l + + let rec undup ~eq = function + | [] -> [] + | x :: tl -> x :: undup ~eq (List.filter (fun y -> not(eq x y)) tl) + + let to_list t = + undup ~eq:(fun x y -> A.equal (A.singleton x) (A.singleton y)) + (List.flatten (List.map + (fun x,_ -> A.elements x) (merge (S.elements t)))) + + let inter t1 t2 = + let l1 = merge (S.elements t1) in + let l2 = merge (S.elements t2) in + let res = + List.flatten + (List.map + (fun s, w -> + HExtlib.filter_map (fun x -> + try Some (x, w + snd (List.find (fun (s,w) -> A.mem x s) l2)) + with Not_found -> None) + (A.elements s)) + l1) + in + undup ~eq:(fun x y -> A.equal (A.singleton x) (A.singleton y)) + (List.map fst (List.sort (fun (_,x) (_,y) -> y - x) res)) + end + let retrieve_sorted unif tree term = let path = I.path_string_of term in let rec retrieve n path tree = @@ -209,9 +269,7 @@ and type data = A.elt and type dataset = A.t = | no, path -> retrieve n path no with Not_found -> S.empty) in - List.flatten - (List.map (fun x -> List.map (fun y -> y, snd x) (A.elements (fst x))) - (S.elements (retrieve 0 path tree))) + retrieve 0 path tree ;; let retrieve_generalizations_sorted tree term = diff --git a/matita/components/extlib/discrimination_tree.mli b/matita/components/extlib/discrimination_tree.mli index c07715b21..bf6b071f1 100644 --- a/matita/components/extlib/discrimination_tree.mli +++ b/matita/components/extlib/discrimination_tree.mli @@ -63,11 +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 - (* the int is the number of symbools that matched, the list - * is sorted with biggest matches first. the same data may match - * twice, and thus appear twice with different number of matches *) - 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 diff --git a/matita/components/ng_refiner/nCicCoercion.ml b/matita/components/ng_refiner/nCicCoercion.ml index 73da9579f..3b6da0af5 100644 --- a/matita/components/ng_refiner/nCicCoercion.ml +++ b/matita/components/ng_refiner/nCicCoercion.ml @@ -18,8 +18,7 @@ let convert_term = ref (fun _ _ -> assert false);; let set_convert_term f = convert_term := f;; module COT : Set.OrderedType -with type t = string * NCic.term * int * int * NCic.term * -NCic.term = +with type t = string * NCic.term * int * int * NCic.term * NCic.term = struct type t = string * NCic.term * int * int * NCic.term * NCic.term let compare = Pervasives.compare @@ -84,31 +83,31 @@ let look_for_coercion status metasenv subst context infty expty = let set_src = List.fold_left (fun set infty -> - CoercionSet.union (DB.retrieve_unifiables db_src infty) set) - CoercionSet.empty src_class + DB.Collector.union (DB.retrieve_unifiables_sorted db_src infty) set) + DB.Collector.empty src_class in let set_tgt = List.fold_left (fun set expty -> - CoercionSet.union (DB.retrieve_unifiables db_tgt expty) set) - CoercionSet.empty tgt_class + DB.Collector.union (DB.retrieve_unifiables_sorted db_tgt expty) set) + DB.Collector.empty tgt_class in debug (lazy ("CANDIDATES SRC: " ^ String.concat "," (List.map (fun (name,t,_,_,_,_) -> name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t) - (CoercionSet.elements set_src)))); + (DB.Collector.to_list set_src)))); debug (lazy ("CANDIDATES TGT: " ^ String.concat "," (List.map (fun (name,t,_,_,_,_) -> name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t) - (CoercionSet.elements set_tgt)))); + (DB.Collector.to_list set_tgt)))); - let candidates = CoercionSet.inter set_src set_tgt in + let candidates = DB.Collector.inter set_src set_tgt in debug (lazy ("CANDIDATES: " ^ String.concat "," (List.map (fun (name,t,_,_,_,_) -> name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t) - (CoercionSet.elements candidates)))); + candidates))); List.map (fun (name,t,arity,arg,_,_) -> @@ -130,7 +129,7 @@ let look_for_coercion status metasenv subst context infty expty = string_of_int (List.length args) ^ " == " ^ string_of_int arg)); name,metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg) - (CoercionSet.elements candidates) + candidates ;; (* CSC: very inefficient implementation! diff --git a/matita/components/ng_refiner/nCicCoercion.mli b/matita/components/ng_refiner/nCicCoercion.mli index d85484a2a..8ea0107de 100644 --- a/matita/components/ng_refiner/nCicCoercion.mli +++ b/matita/components/ng_refiner/nCicCoercion.mli @@ -36,6 +36,9 @@ val index_coercion: #status as 'status -> string -> NCic.term -> NCic.term -> NCic.term -> int -> int -> 'status +(* NOTE: the name of the coercion is used to sort coercions, thus + * two coercions matching the same number of symbols are sorted + * according to their name *) val look_for_coercion: #status -> NCic.metasenv -> NCic.substitution -> NCic.context -> -- 2.39.2