From eaf5880ed69963b3ad37cb1f8a1fd48b2918e58b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 Sep 2008 12:47:23 +0000 Subject: [PATCH] more abstract discrimination tree --- .../components/cic/discrimination_tree.ml | 31 +++++++++++++++++-- .../components/cic/discrimination_tree.mli | 27 ++++++++++------ .../ng_refiner/nDiscriminationTree.ml | 20 +++++++++--- .../ng_refiner/nDiscriminationTree.mli | 10 +++--- .../paramodulation/equality_indexing.ml | 9 ++---- .../paramodulation/equality_indexing.mli | 2 +- .../tactics/paramodulation/indexing.mli | 2 +- helm/software/components/tactics/universe.ml | 2 +- 8 files changed, 72 insertions(+), 31 deletions(-) diff --git a/helm/software/components/cic/discrimination_tree.ml b/helm/software/components/cic/discrimination_tree.ml index 1609fba56..faccadf65 100644 --- a/helm/software/components/cic/discrimination_tree.ml +++ b/helm/software/components/cic/discrimination_tree.ml @@ -105,9 +105,29 @@ let arity_of = function | _ -> 0 ;; -module DiscriminationTreeIndexing = - functor (I:Indexable) -> - functor (A:Set.S) -> +module type DiscriminationTree = + sig + + type input + type data + type dataset + type constant_name + type t + + val iter : t -> (constant_name path -> dataset -> unit) -> unit + + val empty : t + val index : t -> input -> data -> t + val remove_index : t -> input -> data -> t + val in_index : t -> input -> (data -> bool) -> bool + val retrieve_generalizations : t -> input -> dataset + val retrieve_unifiables : t -> input -> dataset + end + +module Make (I:Indexable) (A:Set.S) : DiscriminationTree +with type constant_name = I.constant_name and type input = I.input +and type data = A.elt and type dataset = A.t = + struct module OrderedPathStringElement = struct @@ -115,6 +135,11 @@ module DiscriminationTreeIndexing = let compare = I.compare end + type constant_name = I.constant_name + type data = A.elt + type dataset = A.t + type input = I.input + module PSMap = Map.Make(OrderedPathStringElement);; type key = PSMap.key diff --git a/helm/software/components/cic/discrimination_tree.mli b/helm/software/components/cic/discrimination_tree.mli index ae6fe0347..a31129306 100644 --- a/helm/software/components/cic/discrimination_tree.mli +++ b/helm/software/components/cic/discrimination_tree.mli @@ -48,20 +48,27 @@ end module CicIndexable : Indexable with type input = Cic.term and type constant_name = UriManager.uri -module DiscriminationTreeIndexing : - functor (I: Indexable) -> - functor (A : Set.S) -> +module type DiscriminationTree = sig - type t - val iter : t -> (I.constant_name path -> A.t -> unit) -> unit + type input + type data + type dataset + type constant_name + type t + + val iter : t -> (constant_name path -> dataset -> unit) -> unit val empty : t - val index : t -> I.input -> A.elt -> t - val remove_index : t -> I.input -> A.elt -> t - val in_index : t -> I.input -> (A.elt -> bool) -> bool - val retrieve_generalizations : t -> I.input -> A.t - val retrieve_unifiables : t -> I.input -> A.t + val index : t -> input -> data -> t + val remove_index : t -> input -> data -> t + val in_index : t -> input -> (data -> bool) -> bool + val retrieve_generalizations : t -> input -> dataset + val retrieve_unifiables : t -> input -> dataset end +module Make (I : Indexable) (A : Set.S) : DiscriminationTree +with type constant_name = I.constant_name and type input = I.input +and type data = A.elt and type dataset = A.t + diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.ml b/helm/software/components/ng_refiner/nDiscriminationTree.ml index d3a334a59..bd64cfe5d 100644 --- a/helm/software/components/ng_refiner/nDiscriminationTree.ml +++ b/helm/software/components/ng_refiner/nDiscriminationTree.ml @@ -24,10 +24,22 @@ *) (* $Id$ *) -(* -module NCicIndexable : Discrimination_tree.Indexable + +open Discrimination_tree + +module TermOT : Set.OrderedType with type t = NCic.term = struct + type t = NCic.term + let compare = Pervasives.compare +end + +module TermSet = Set.Make(TermOT) + +module NCicIndexable : Indexable with type input = NCic.term and type constant_name = NUri.uri = struct +type input = NCic.term +type constant_name = NUri.uri + let ppelem = function | Constant (uri,arity) -> "("^NUri.name_of_uri uri ^ "," ^ string_of_int arity^")" @@ -71,6 +83,4 @@ let string_of_path l = String.concat "." (List.map ppelem l) ;; end -module DiscriminationTree = - Discrimination_tree.DiscriminationTreeIndexing(NCicIndexable) - *) +module DiscriminationTree = Make(NCicIndexable)(TermSet) diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.mli b/helm/software/components/ng_refiner/nDiscriminationTree.mli index 29fdbb68e..b00827716 100644 --- a/helm/software/components/ng_refiner/nDiscriminationTree.mli +++ b/helm/software/components/ng_refiner/nDiscriminationTree.mli @@ -23,10 +23,12 @@ * http://cs.unibo.it/helm/. *) -(* module NCicIndexable : Discrimination_tree.Indexable with type input = NCic.term and type constant_name = NUri.uri -module DiscriminationTree : - Discrimination_tree.DiscriminationTreeIndexing(NCicIndexable) -*) +module TermSet : Set.S with type elt = NCic.term + +module DiscriminationTree : Discrimination_tree.DiscriminationTree +with type constant_name = NCicIndexable.constant_name +and type input = NCicIndexable.input +and type data = TermSet.elt and type dataset = TermSet.t diff --git a/helm/software/components/tactics/paramodulation/equality_indexing.ml b/helm/software/components/tactics/paramodulation/equality_indexing.ml index 390fa1c98..458433aba 100644 --- a/helm/software/components/tactics/paramodulation/equality_indexing.ml +++ b/helm/software/components/tactics/paramodulation/equality_indexing.ml @@ -28,8 +28,7 @@ module type EqualityIndex = sig module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality - type t = - Discrimination_tree.DiscriminationTreeIndexing(Discrimination_tree.CicIndexable)(PosEqSet).t + type t = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t val empty : t val retrieve_generalizations : t -> Cic.term -> PosEqSet.t val retrieve_unifiables : t -> Cic.term -> PosEqSet.t @@ -51,8 +50,7 @@ struct module PosEqSet = Set.Make(OrderedPosEquality);; - include - Discrimination_tree.DiscriminationTreeIndexing(Discrimination_tree.CicIndexable)(PosEqSet) + include Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet) (* DISCRIMINATION TREES *) @@ -97,8 +95,7 @@ module PT = module PosEqSet = Set.Make(OrderedPosEquality);; - include - Discrimination_tree.DiscriminationTreeIndexing(Discrimination_tree.CicIndexable)(PosEqSet) + include Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet) (* DISCRIMINATION TREES *) diff --git a/helm/software/components/tactics/paramodulation/equality_indexing.mli b/helm/software/components/tactics/paramodulation/equality_indexing.mli index 4ac6d54ec..c4b9df0ea 100644 --- a/helm/software/components/tactics/paramodulation/equality_indexing.mli +++ b/helm/software/components/tactics/paramodulation/equality_indexing.mli @@ -26,7 +26,7 @@ module type EqualityIndex = sig module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality - type t = Discrimination_tree.DiscriminationTreeIndexing(Discrimination_tree.CicIndexable)(PosEqSet).t + type t = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t val empty : t val retrieve_generalizations : t -> Cic.term -> PosEqSet.t val retrieve_unifiables : t -> Cic.term -> PosEqSet.t diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli index 9e7ba76f7..52afad8c2 100644 --- a/helm/software/components/tactics/paramodulation/indexing.mli +++ b/helm/software/components/tactics/paramodulation/indexing.mli @@ -31,7 +31,7 @@ module Index : with type elt = Utils.pos * Equality.equality and type t = Equality_indexing.DT.PosEqSet.t type t = - Discrimination_tree.DiscriminationTreeIndexing(Discrimination_tree.CicIndexable)(PosEqSet).t + Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t end val index : Index.t -> Equality.equality -> Index.t diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml index b914fab06..a7418461e 100644 --- a/helm/software/components/tactics/universe.ml +++ b/helm/software/components/tactics/universe.ml @@ -28,7 +28,7 @@ module Codomain = struct let compare = Pervasives.compare end module S = Set.Make(Codomain) -module TI = Discrimination_tree.DiscriminationTreeIndexing(Discrimination_tree.CicIndexable)(S) +module TI = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(S) type universe = TI.t let empty = TI.empty -- 2.39.2