diff options
| -rw-r--r-- | lib/trie.ml | 30 | ||||
| -rw-r--r-- | lib/trie.mli | 13 | ||||
| -rw-r--r-- | tactics/dn.ml | 19 |
3 files changed, 44 insertions, 18 deletions
diff --git a/lib/trie.ml b/lib/trie.ml index f6dc657cc..a4a348c19 100644 --- a/lib/trie.ml +++ b/lib/trie.ml @@ -12,7 +12,7 @@ sig type data type t val empty : t - val get : t -> data list + val get : t -> data val next : t -> label -> t val labels : t -> label list val add : label list -> data -> t -> t @@ -20,25 +20,33 @@ sig val iter : (label list -> data -> unit) -> t -> unit end -module Make (Y : Map.OrderedType) (X : Set.OrderedType) = +module type Grp = +sig + type t + val nil : t + val is_nil : t -> bool + val add : t -> t -> t + val sub : t -> t -> t +end + +module Make (Y : Map.OrderedType) (X : Grp) = struct -module T_dom = Set.Make(X) module T_codom = Map.Make(Y) type data = X.t type label = Y.t -type t = Node of T_dom.t * t T_codom.t +type t = Node of X.t * t T_codom.t let codom_for_all f m = let fold key v accu = f v && accu in T_codom.fold fold m true -let empty = Node (T_dom.empty, T_codom.empty) +let empty = Node (X.nil, T_codom.empty) let next (Node (_,m)) lbl = T_codom.find lbl m -let get (Node (hereset,_)) = T_dom.elements hereset +let get (Node (hereset,_)) = hereset let labels (Node (_,m)) = (** FIXME: this is order-dependent. Try to find a more robust presentation? *) @@ -46,13 +54,13 @@ let labels (Node (_,m)) = let in_dom (Node (_,m)) lbl = T_codom.mem lbl m -let is_empty_node (Node(a,b)) = (T_dom.is_empty a) && (T_codom.is_empty b) +let is_empty_node (Node(a,b)) = (X.is_nil a) && (T_codom.is_empty 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 + T_codom.add lbl (Node (X.nil,T_codom.empty)) m let cleanse_arcs (Node (hereset,m)) = let m = if codom_for_all is_empty_node m then T_codom.empty else m in @@ -67,15 +75,15 @@ let rec at_path f (Node (hereset,m)) = function 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 + at_path (fun hereset -> X.add v hereset) tm path let remove path v tm = - at_path (fun hereset -> T_dom.remove v hereset) tm path + at_path (fun hereset -> X.sub hereset v) 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; + f path hereset; T_codom.iter (fun l tm -> apprec (l::pfx) tm) m in apprec [] tlm diff --git a/lib/trie.mli b/lib/trie.mli index 6d14cf9cb..f3eb51578 100644 --- a/lib/trie.mli +++ b/lib/trie.mli @@ -26,7 +26,7 @@ sig val empty : t (** The empty trie. *) - val get : t -> data list + val get : t -> data (** Get the data at the current node. *) val next : t -> label -> t @@ -47,6 +47,15 @@ sig end -module Make (Label : Set.OrderedType) (Data : Set.OrderedType) : S +module type Grp = +sig + type t + val nil : t + val is_nil : t -> bool + val add : t -> t -> t + val sub : t -> t -> t +end + +module Make (Label : Set.OrderedType) (Data : Grp) : S with type label = Label.t and type data = Data.t (** Generating functor, for a given type of labels and data. *) diff --git a/tactics/dn.ml b/tactics/dn.ml index 1373ca3fb..069e84fad 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -21,13 +21,22 @@ struct | Some(l,n),None -> 1 | None, Some(l,n) -> -1 end - module X_tries = struct + module XZOrd = struct type t = X.t * Z.t let compare (x1,x2) (y1,y2) = let m = (X.compare x1 y1) in if Int.equal m 0 then (Z.compare x2 y2) else m end + module XZ = Set.Make(XZOrd) + module X_tries = + struct + type t = XZ.t + let nil = XZ.empty + let is_nil = XZ.is_empty + let add = XZ.union + let sub = XZ.diff + end module Trie = Trie.Make(Y_tries)(X_tries) @@ -88,15 +97,15 @@ prefix ordering, [dna] is the function returning the main node of a pattern *) (tm_of tm (Some(lbl,List.length v))) v) | Everything -> skip_arg 1 tm in - List.flatten (List.map (fun (tm,b) -> Trie.get tm) (lookrec t tm)) + List.flatten (List.map (fun (tm,b) -> XZ.elements (Trie.get tm)) (lookrec t tm)) let add tm dna (pat,inf) = - let p = path_of dna pat in Trie.add p (pat, inf) tm + let p = path_of dna pat in Trie.add p (XZ.singleton (pat, inf)) tm let rmv tm dna (pat,inf) = - let p = path_of dna pat in Trie.remove p (pat, inf) tm + let p = path_of dna pat in Trie.remove p (XZ.singleton (pat, inf)) tm - let app f tm = Trie.iter (fun _ p -> f p) tm + let app f tm = Trie.iter (fun _ p -> XZ.iter f p) tm end |