aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/lib.mllib2
-rw-r--r--lib/trie.ml (renamed from lib/tries.ml)79
-rw-r--r--lib/trie.mli52
-rw-r--r--lib/tries.mli34
-rw-r--r--tactics/dn.ml82
5 files changed, 140 insertions, 109 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
diff --git a/tactics/dn.ml b/tactics/dn.ml
index 768cdf94e..1373ca3fb 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
-
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-15 12:21:44 +0000