discriminations nets

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@123 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 58 insertions, 76 deletions

diff --git a/lib/gmap.ml b/lib/gmap.ml
index beb0a1994e..52af882b35 100644
--- a/lib/gmap.ml
+++ b/lib/gmap.ml
@@ -107,3 +107,12 @@
         Empty -> accu
       | Node(l, v, d, r, _) ->
           fold f l (f v d (fold f r accu))
+
+(* Added with respect to ocaml standard library. *)
+
+    let dom m = fold (fun x _ acc -> x::acc) m []
+
+    let rng m = fold (fun _ y acc -> y::acc) m []
+
+    let to_list m = fold (fun x y acc -> (x,y)::acc) m []
+
diff --git a/lib/gmap.mli b/lib/gmap.mli
index 861e730e26..908bad1bcf 100644
--- a/lib/gmap.mli
+++ b/lib/gmap.mli
@@ -14,3 +14,9 @@ val mem :  'a -> ('a,'b) t -> bool
 val iter : ('a -> 'b -> unit) -> ('a,'b) t -> unit
 val map : ('b -> 'c) -> ('a,'b) t -> ('a,'c) t
 val fold : ('a -> 'b -> 'c -> 'c) -> ('a,'b) t -> 'c -> 'c
+
+(* Additions with respect to ocaml standard library. *)
+
+val dom : ('a,'b) t -> 'a list
+val rng : ('a,'b) t -> 'b list
+val to_list : ('a,'b) t -> ('a * 'b) list
diff --git a/lib/tlm.ml b/lib/tlm.ml
index 9b61de9336..d16353f1ec 100644
--- a/lib/tlm.ml
+++ b/lib/tlm.ml
@@ -1,92 +1,56 @@
 
 (* $Id$ *)
 
-(* 1er choix : une liste
-module MySet = struct
-  type 'a t = 'a list
-  let mt = []
-  let add = add_set
-  let rmv = rmv_set
-  let toList l = l
-  let app = List.map
-end
-*)
+type ('a,'b) t = Node of 'b Gset.t * ('a, ('a,'b) t) Gmap.t
 
-(* 2 ème choix : un arbre *)
-module MySet = struct
-  type 'a t = 'a Coq_set.t
-  let mt = Coq_set.empty
-  let add = Coq_set.add
-  let rmv = Coq_set.remove
-  let toList = Coq_set.elements
-  let app f l = Coq_set.fold (fun a b -> add (f a) b) l mt
-end
+let empty = Node (Gset.empty, Gmap.empty)
 
-module type MyMapType = sig
-  type ('a, 'b) t
-  val create : unit -> ('a,'b) t
-  val map : ('a,'b) t -> 'a -> 'b
-  val dom : ('a,'b) t -> 'a list
-  val rng : ('a,'b) t -> 'b list
-  val in_dom : ('a,'b) t -> 'a -> bool
-  val add : ('a,'b) t -> 'a * 'b -> ('a,'b) t
-  val remap : ('a,'b) t -> 'a -> 'b -> ('a,'b) t
-  val app : (('a * 'c) -> unit) -> ('a,'c) t -> unit
-  val toList : ('a,'b) t -> ('a * 'b) list
-end;;
+let map (Node (_,m)) lbl = Gmap.find lbl m
 
-module MyMap = (Listmap : MyMapType);;
+let xtract (Node (hereset,_)) = Gset.elements hereset
 
-type ('a,'b) t =
-    NODE of 'b MySet.t * ('a, ('a,'b) t) MyMap.t;;
+let dom (Node (_,m)) = Gmap.dom m
 
-let create () = NODE(MySet.mt,MyMap.create());;
+let in_dom (Node (_,m)) lbl = Gmap.mem lbl m
 
-let map (NODE (_,m)) lbl = MyMap.map m lbl;;
-let xtract (NODE (hereset,_)) = MySet.toList hereset;;
-let dom (NODE (_,m)) = MyMap.dom m;;
-let in_dom (NODE (_,m)) lbl = MyMap.in_dom m lbl;;
-
-let is_empty_node (NODE(a,b)) = (MySet.toList a = []) & (MyMap.toList b = []);;
+let is_empty_node (Node(a,b)) = (Gset.elements a = []) & (Gmap.to_list b = [])
 
 let assure_arc m lbl =
-    if MyMap.in_dom m lbl then m
-    else MyMap.add m (lbl,NODE (MySet.mt,MyMap.create()))
-;;
-
-let cleanse_arcs (NODE (hereset,m)) =
-let l = MyMap.rng m
-in NODE(hereset,if List.for_all is_empty_node l then MyMap.create() else m)
-;;
-
-let rec at_path f (NODE (hereset,m)) = function
-    [] -> cleanse_arcs(NODE(f hereset,m))
+  if Gmap.mem lbl m then 
+    m
+  else 
+    Gmap.add lbl (Node (Gset.empty,Gmap.empty)) m
+
+let cleanse_arcs (Node (hereset,m)) =
+  let l = Gmap.rng m in 
+  Node(hereset, if List.for_all is_empty_node l then Gmap.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,
-                         MyMap.remap m h (at_path f (MyMap.map m h) t)))
-;;
+      let m = assure_arc m h in 
+      cleanse_arcs (Node(hereset,
+                         Gmap.add h (at_path f (Gmap.find h m) t) m))
 
 let add tm (path,v) =
-    at_path (fun hereset -> MySet.add v hereset) tm path
-;;
-
+  at_path (fun hereset -> Gset.add v hereset) tm path
+    
 let rmv tm (path,v) =
-    at_path (fun hereset -> MySet.rmv v hereset) tm path
-;;
+  at_path (fun hereset -> Gset.remove v hereset) tm path
 
 let app f tlm = 
- let rec apprec pfx (NODE(hereset,m)) =
-    let path = List.rev pfx
-    in (MySet.app (fun v -> f(path,v)) hereset;
-        MyMap.app (fun (l,tm) -> apprec (l::pfx) tm) m)
- in apprec [] tlm
-;;
+  let rec apprec pfx (Node(hereset,m)) =
+    let path = List.rev pfx in 
+    Gset.iter (fun v -> f(path,v)) hereset;
+    Gmap.iter (fun l tm -> apprec (l::pfx) tm) m
+  in 
+  apprec [] tlm
     
-let toList tlm = 
- let rec torec pfx (NODE(hereset,m)) =
-    let path = List.rev pfx
-    in List.flatten((List.map (fun v -> (path,v)) (MySet.toList hereset))::
-            (List.map (fun (l,tm) -> torec (l::pfx) tm) (MyMap.toList m)))
- in torec [] 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)) (Gset.elements hereset))::
+		 (List.map (fun (l,tm) -> torec (l::pfx) tm) (Gmap.to_list m)))
+  in 
+  torec [] tlm
diff --git a/lib/tlm.mli b/lib/tlm.mli
index 41af7c1aba..44a2adc8bf 100644
--- a/lib/tlm.mli
+++ b/lib/tlm.mli
@@ -1,9 +1,12 @@
 
 (* $Id$ *)
 
+(* Tries. This module implements a data structure [('a,'b) t] mapping lists
+   of values of type ['a] to sets (as lists) of values of type ['b]. *)
+
 type ('a,'b) t
 
-val create : unit -> ('a,'b) t
+val empty : ('a,'b) t
 
 (* Work on labels, not on paths. *)
 
@@ -17,6 +20,6 @@ val in_dom : ('a,'b) t -> 'a -> bool
 val add : ('a,'b) t -> 'a list * 'b -> ('a,'b) t
 val rmv : ('a,'b) t -> ('a list * 'b) -> ('a,'b) t
 
-val app : (('a list * 'c) -> unit) -> ('a,'c) t -> unit
+val app : (('a list * 'b) -> unit) -> ('a,'b) t -> unit
 val to_list : ('a,'b) t -> ('a list * 'b) list