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 ---------------------- tactics/dn.ml | 82 ++++++++++++++++++++++++++--------------------------- 6 files changed, 185 insertions(+), 154 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 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 diff --git a/tactics/dn.ml b/tactics/dn.ml index 768cdf94e2..1373ca3fbd 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -2,101 +2,101 @@ open Util -module Make = +module Make = functor (X : Set.OrderedType) -> functor (Y : Map.OrderedType) -> functor (Z : Map.OrderedType) -> struct - + module Y_tries = struct type t = (Y.t * int) option - let compare x y = + let compare x y = match x,y with None,None -> 0 - | Some (l,n),Some (l',n') -> + | Some (l,n),Some (l',n') -> let m = Y.compare l l' in if Int.equal m 0 then - n-n' + n-n' else m | Some(l,n),None -> 1 | None, Some(l,n) -> -1 end module X_tries = struct type t = X.t * Z.t - let compare (x1,x2) (y1,y2) = + let compare (x1,x2) (y1,y2) = let m = (X.compare x1 y1) in - if Int.equal m 0 then (Z.compare x2 y2) else + if Int.equal m 0 then (Z.compare x2 y2) else m end - module T = Tries.Make(X_tries)(Y_tries) - + module Trie = Trie.Make(Y_tries)(X_tries) + type decompose_fun = X.t -> (Y.t * X.t list) option - + type 'res lookup_res = Label of 'res | Nothing | Everything - + type 'tree lookup_fun = 'tree -> (Y.t * 'tree list) lookup_res - type t = T.t + type t = Trie.t - let create () = T.empty + let create () = Trie.empty -(* [path_of dna pat] returns the list of nodes of the pattern [pat] read in +(* [path_of dna pat] returns the list of nodes of the pattern [pat] read in prefix ordering, [dna] is the function returning the main node of a pattern *) let path_of dna = let rec path_of_deferred = function | [] -> [] | h::tl -> pathrec tl h - + and pathrec deferred t = match dna t with - | None -> + | None -> None :: (path_of_deferred deferred) | Some (lbl,[]) -> (Some (lbl,0))::(path_of_deferred deferred) | Some (lbl,(h::def_subl as v)) -> (Some (lbl,List.length v))::(pathrec (def_subl@deferred) h) - in + in pathrec [] - + let tm_of tm lbl = - try [T.map tm lbl, true] with Not_found -> [] - + try [Trie.next tm lbl, true] with Not_found -> [] + let rec skip_arg n tm = - if Int.equal n 0 then [tm,true] + if Int.equal n 0 then [tm, true] else - List.flatten - (List.map - (fun a -> match a with - | None -> skip_arg (pred n) (T.map tm a) - | Some (lbl,m) -> - skip_arg (pred n + m) (T.map tm a)) - (T.dom tm)) - + let labels = Trie.labels tm in + let map lbl = match lbl with + | None -> skip_arg (pred n) (Trie.next tm lbl) + | Some (_, m) -> + skip_arg (pred n + m) (Trie.next tm lbl) + in + List.flatten (List.map map labels) + let lookup tm dna t = let rec lookrec t tm = match dna t with | Nothing -> tm_of tm None | Label(lbl,v) -> tm_of tm None@ - (List.fold_left - (fun l c -> + (List.fold_left + (fun l c -> List.flatten(List.map (fun (tm, b) -> if b then lookrec c tm else [tm,b]) l)) (tm_of tm (Some(lbl,List.length v))) v) | Everything -> skip_arg 1 tm - in - List.flatten (List.map (fun (tm,b) -> T.xtract tm) (lookrec t tm)) - + in + List.flatten (List.map (fun (tm,b) -> Trie.get tm) (lookrec t tm)) + let add tm dna (pat,inf) = - let p = path_of dna pat in T.add tm (p,(pat,inf)) - + let p = path_of dna pat in Trie.add p (pat, inf) tm + let rmv tm dna (pat,inf) = - let p = path_of dna pat in T.rmv tm (p,(pat,inf)) - - let app f tm = T.app (fun (_,p) -> f p) tm - + let p = path_of dna pat in Trie.remove p (pat, inf) tm + + let app f tm = Trie.iter (fun _ p -> f p) tm + end - + -- cgit v1.2.3