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
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 =
| 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 =
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
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
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,_,_) ->
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!
#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 ->
projects / helm.git / commitdiff