From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- tactics/dn.ml | 102 ++++++++++++++++++++++++++++------------------------------ 1 file changed, 50 insertions(+), 52 deletions(-) (limited to 'tactics/dn.ml') diff --git a/tactics/dn.ml b/tactics/dn.ml index a0889ab8..3b1614d6 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -1,103 +1,101 @@ +open Util +type 'res lookup_res = Label of 'res | Nothing | Everything - - - -module Make = - functor (X : Set.OrderedType) -> +module Make = 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 m = 0 then - n-n' + if Int.equal m 0 then + 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 m = (X.compare x1 y1) in - if m = 0 then (Z.compare x2 y2) else - m + module ZSet = Set.Make(Z) + module X_tries = + struct + type t = ZSet.t + let nil = ZSet.empty + let is_nil = ZSet.is_empty + let add = ZSet.union + let sub = ZSet.diff end - module T = Tries.Make(X_tries)(Y_tries) - - type decompose_fun = X.t -> (Y.t * X.t list) option - - type 'res lookup_res = Label of 'res | Nothing | Everything - + module Trie = Trie.Make(Y_tries)(X_tries) + + type 'a decompose_fun = 'a -> (Y.t * 'a list) option + 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 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) -> ZSet.elements (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 (ZSet.singleton 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 (ZSet.singleton inf) tm + + let app f tm = Trie.iter (fun _ p -> ZSet.iter f p) tm + end - + -- cgit v1.2.3