From 3b005bfdb2d595f5b8e094f940ae26f072780faf Mon Sep 17 00:00:00 2001 From: ppedrot Date: Thu, 9 May 2013 21:53:44 +0000 Subject: 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 --- lib/lib.mllib | 2 +- lib/trie.ml | 91 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/trie.mli | 52 ++++++++++++++++++++++++++++++++++ lib/tries.ml | 78 -------------------------------------------------- lib/tries.mli | 34 ---------------------- 5 files changed, 144 insertions(+), 113 deletions(-) create mode 100644 lib/trie.ml create mode 100644 lib/trie.mli delete mode 100644 lib/tries.ml delete mode 100644 lib/tries.mli (limited to 'lib') diff --git a/lib/lib.mllib b/lib/lib.mllib index 088bbf0102..c28da5ace1 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/trie.ml b/lib/trie.ml new file mode 100644 index 0000000000..d0bcc01554 --- /dev/null +++ b/lib/trie.ml @@ -0,0 +1,91 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 (Y : Map.OrderedType) (X : Set.OrderedType) = +struct + +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_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 empty = Node (T_dom.empty, T_codom.empty) + +let next (Node (_,m)) lbl = T_codom.find lbl m + +let get (Node (hereset,_)) = T_dom.elements hereset + +let labels (Node (_,m)) = codom_dom m + +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 + m + 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 + 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 + cleanse_arcs (Node(hereset, + T_codom.add h (at_path f (T_codom.find h m) t) m)) + +let add path v tm = + at_path (fun hereset -> T_dom.add v hereset) tm path + +let remove path v tm = + at_path (fun hereset -> T_dom.remove v hereset) tm path + +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; + T_codom.iter (fun l tm -> apprec (l::pfx) tm) m + in + apprec [] tlm + +let to_list tlm = + let rec torec pfx (Node(hereset,m)) = + 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 + torec [] tlm + +end diff --git a/lib/trie.mli b/lib/trie.mli new file mode 100644 index 0000000000..6d14cf9cbf --- /dev/null +++ b/lib/trie.mli @@ -0,0 +1,52 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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.ml b/lib/tries.ml deleted file mode 100644 index 90d23bf199..0000000000 --- a/lib/tries.ml +++ /dev/null @@ -1,78 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - functor (Y : Map.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 - - 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_dom m = T_codom.fold (fun x _ acc -> x::acc) m [] - - let empty = Node (T_dom.empty, T_codom.empty) - - let map (Node (_,m)) lbl = T_codom.find lbl m - - let xtract (Node (hereset,_)) = T_dom.elements hereset - - let dom (Node (_,m)) = codom_dom m - - 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 - m - 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 - 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 - cleanse_arcs (Node(hereset, - T_codom.add h (at_path f (T_codom.find h m) t) m)) - -let add tm (path,v) = - at_path (fun hereset -> T_dom.add v hereset) tm path - -let rmv tm (path,v) = - at_path (fun hereset -> T_dom.remove v hereset) tm path - -let app f tlm = - let rec apprec pfx (Node(hereset,m)) = - 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 - apprec [] tlm - -let to_list tlm = - let rec torec pfx (Node(hereset,m)) = - 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 - torec [] tlm - -end diff --git a/lib/tries.mli b/lib/tries.mli deleted file mode 100644 index 8e8376772e..0000000000 --- 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 -- cgit v1.2.3