diff options
author | 2013-05-09 21:53:44 +0000 | |
---|---|---|
committer | 2013-05-09 21:53:44 +0000 | |
commit | 3b005bfdb2d595f5b8e094f940ae26f072780faf (patch) | |
tree | 15e7099f22d401561960de753c06add75cf53989 /lib | |
parent | 9f3ccbf420eec91410dea100b217a60f7defa5f2 (diff) |
Documenting the Tries module, uniformizing the names according to
Map/Set style and renaming the file accordingly as Trie.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16504 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
-rw-r--r-- | lib/lib.mllib | 2 | ||||
-rw-r--r-- | lib/trie.ml (renamed from lib/tries.ml) | 79 | ||||
-rw-r--r-- | lib/trie.mli | 52 | ||||
-rw-r--r-- | lib/tries.mli | 34 |
4 files changed, 99 insertions, 68 deletions
diff --git a/lib/lib.mllib b/lib/lib.mllib index 088bbf010..c28da5ace 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -11,7 +11,7 @@ System Gmap Fset Fmap -Tries +Trie Profile Explore Predicate diff --git a/lib/tries.ml b/lib/trie.ml index 90d23bf19..d0bcc0155 100644 --- a/lib/tries.ml +++ b/lib/trie.ml @@ -6,73 +6,86 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +module type S = +sig + type label + type data + type t + val empty : t + val get : t -> data list + val next : t -> label -> t + val labels : t -> label list + val add : label list -> data -> t -> t + val remove : label list -> data -> t -> t + val iter : (label list -> data -> unit) -> t -> unit +end - -module Make = - functor (X : Set.OrderedType) -> - functor (Y : Map.OrderedType) -> +module Make (Y : Map.OrderedType) (X : Set.OrderedType) = struct - module T_dom = Fset.Make(X) - module T_codom = Fmap.Make(Y) - type t = Node of T_dom.t * t T_codom.t +module T_dom = Fset.Make(X) +module T_codom = Fmap.Make(Y) + +type data = X.t +type label = Y.t +type t = Node of T_dom.t * t T_codom.t - let codom_to_list m = T_codom.fold (fun x y l -> (x,y)::l) m [] +let codom_to_list m = T_codom.fold (fun x y l -> (x,y)::l) m [] - let codom_rng m = T_codom.fold (fun _ y acc -> y::acc) m [] +let codom_rng m = T_codom.fold (fun _ y acc -> y::acc) m [] - let codom_dom m = T_codom.fold (fun x _ acc -> x::acc) m [] +let codom_dom m = T_codom.fold (fun x _ acc -> x::acc) m [] - let empty = Node (T_dom.empty, T_codom.empty) +let empty = Node (T_dom.empty, T_codom.empty) - let map (Node (_,m)) lbl = T_codom.find lbl m +let next (Node (_,m)) lbl = T_codom.find lbl m - let xtract (Node (hereset,_)) = T_dom.elements hereset - - let dom (Node (_,m)) = codom_dom m +let get (Node (hereset,_)) = T_dom.elements hereset - let in_dom (Node (_,m)) lbl = T_codom.mem lbl m +let labels (Node (_,m)) = codom_dom m - let is_empty_node (Node(a,b)) = (T_dom.elements a = []) & (codom_to_list b = []) +let in_dom (Node (_,m)) lbl = T_codom.mem lbl m + +let is_empty_node (Node(a,b)) = (T_dom.elements a = []) && (codom_to_list b = []) let assure_arc m lbl = - if T_codom.mem lbl m then + if T_codom.mem lbl m then m - else + else T_codom.add lbl (Node (T_dom.empty,T_codom.empty)) m let cleanse_arcs (Node (hereset,m)) = - let l = codom_rng m in + let l = codom_rng m in Node(hereset, if List.for_all is_empty_node l then T_codom.empty else m) let rec at_path f (Node (hereset,m)) = function - | [] -> + | [] -> cleanse_arcs (Node(f hereset,m)) | h::t -> - let m = assure_arc m h in + let m = assure_arc m h in cleanse_arcs (Node(hereset, T_codom.add h (at_path f (T_codom.find h m) t) m)) -let add tm (path,v) = +let add path v tm = at_path (fun hereset -> T_dom.add v hereset) tm path - -let rmv tm (path,v) = + +let remove path v tm = at_path (fun hereset -> T_dom.remove v hereset) tm path -let app f tlm = +let iter f tlm = let rec apprec pfx (Node(hereset,m)) = - let path = List.rev pfx in - T_dom.iter (fun v -> f(path,v)) hereset; + let path = List.rev pfx in + T_dom.iter (fun v -> f path v) hereset; T_codom.iter (fun l tm -> apprec (l::pfx) tm) m - in + in apprec [] tlm - -let to_list tlm = + +let to_list tlm = let rec torec pfx (Node(hereset,m)) = - let path = List.rev pfx in + let path = List.rev pfx in List.flatten((List.map (fun v -> (path,v)) (T_dom.elements hereset)):: (List.map (fun (l,tm) -> torec (l::pfx) tm) (codom_to_list m))) - in + in torec [] tlm end diff --git a/lib/trie.mli b/lib/trie.mli new file mode 100644 index 000000000..6d14cf9cb --- /dev/null +++ b/lib/trie.mli @@ -0,0 +1,52 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Generic functorized trie data structure. *) + +module type S = +sig + (** A trie is a generalization of the map data structure where the keys are + themselves lists. *) + + type label + (** Keys of the trie structure are [label list]. *) + + type data + (** Data on nodes of tries are finite sets of [data]. *) + + type t + (** The trie data structure. Essentially a finite map with keys [label list] + and content [data Set.t]. *) + + val empty : t + (** The empty trie. *) + + val get : t -> data list + (** Get the data at the current node. *) + + val next : t -> label -> t + (** [next t lbl] returns the subtrie of [t] pointed by [lbl]. + @raise Not_found if there is none. *) + + val labels : t -> label list + (** Get the list of defined labels at the current node. *) + + val add : label list -> data -> t -> t + (** [add t path v] adds [v] at path [path] in [t]. *) + + val remove : label list -> data -> t -> t + (** [remove t path v] removes [v] from path [path] in [t]. *) + + val iter : (label list -> data -> unit) -> t -> unit + (** Apply a function to all contents. *) + +end + +module Make (Label : Set.OrderedType) (Data : Set.OrderedType) : S + with type label = Label.t and type data = Data.t +(** Generating functor, for a given type of labels and data. *) diff --git a/lib/tries.mli b/lib/tries.mli deleted file mode 100644 index 8e8376772..000000000 --- a/lib/tries.mli +++ /dev/null @@ -1,34 +0,0 @@ - - - - - -module Make : - functor (X : Set.OrderedType) -> - functor (Y : Map.OrderedType) -> -sig - - type t - - val empty : t - - (** Work on labels, not on paths. *) - - val map : t -> Y.t -> t - - val xtract : t -> X.t list - - val dom : t -> Y.t list - - val in_dom : t -> Y.t -> bool - - (** Work on paths, not on labels. *) - - val add : t -> Y.t list * X.t -> t - - val rmv : t -> Y.t list * X.t -> t - - val app : ((Y.t list * X.t) -> unit) -> t -> unit - - val to_list : t -> (Y.t list * X.t) list -end |