Quelques structures de donnée plus les modules principaux (et

parfaitement en cours) de la nouvelle machinerie de preuves.



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

2 files changed, 135 insertions, 0 deletions

diff --git a/lib/biassoc.ml b/lib/biassoc.ml
new file mode 100644
index 0000000000..2c8fc32167
--- /dev/null
+++ b/lib/biassoc.ml
@@ -0,0 +1,74 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: biassoc.ml aspiwack $ *)
+
+(* This modules implements a bidirectional association table,
+   that is a table where both values can be seen as the key for
+   the association.
+   For soundness reason, when adding an association [(a,b)] both
+   [a] and [b] must be unique.
+
+   Map is a reasonably efficient datastructure, which compares rather
+   well (in average) to the more imperative Hashtables. In that respect
+   and since persistent datastructures are used in the kernel, I write
+   this in the functional style.
+
+   This module have been originally written for being used both in the
+   retroknowledge for its internal representation (thus in the kernel)
+   and in the interactive proof system for associating dependent goals
+   to an evar. *)
+
+(* The internal representation is a straightforward pair of Maps
+   (one from a type 'a to a type 'b, and the other from the 
+   type 'b to the type 'a). Both are updated synchronously to 
+   provide fast access in both directions. *)
+
+
+
+
+type ('a,'b) biassoc = { left:('a,'b) Gmap.t ; right:('b,'a) Gmap.t }
+    
+let empty = { left=Gmap.empty ; right=Gmap.empty }
+let is_empty bm = (Gmap.is_empty bm.left)&&(Gmap.is_empty bm.right)
+  
+let find_with_left lt bm = Gmap.find lt bm.left
+let find_with_right rt bm = Gmap.find rt bm.right
+  
+let mem_with_left lt bm = Gmap.mem lt bm.left
+let mem_with_right rt bm = Gmap.mem rt bm.right
+  
+(* remove functions are not a direct lifting of the 
+   functions from either components, since you have to 
+   remove the corresponding binding in the second Map *)
+let remove_with_left lt bm = 
+  try 
+    let rt = find_with_left lt bm in
+      { left = Gmap.remove lt bm.left ;
+        right = Gmap.remove rt bm.right }
+  with Not_found ->
+    (* if there is no (lt, ?) in the left Map, then there
+       is no (?,lt) in the Right table. Thus bm is already
+       free of any reference to lt *)
+    bm
+      
+let remove_with_right rt bm = (* see remove_with_left *)
+  try 
+    let lt = find_with_right rt bm in
+      { left = Gmap.remove lt bm.left ;
+        right = Gmap.remove rt bm.right }
+  with Not_found ->
+    bm
+      
+let add lt rt bm = 
+  if not (mem_with_left lt bm) && not (mem_with_right rt bm) then
+    { left = Gmap.add lt rt bm.left ;
+      right = Gmap.add rt lt bm.right }
+  else
+    raise (Invalid_argument "Biassoc: non unique values")
+
diff --git a/lib/biassoc.mli b/lib/biassoc.mli
new file mode 100644
index 0000000000..45426d1bc3
--- /dev/null
+++ b/lib/biassoc.mli
@@ -0,0 +1,61 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: biassoc.ml aspiwack $ *)
+
+(* This modules implements a bidirectional association table,
+   that is a table where both values can be seen as the key for
+   the association.
+   For soundness reason, when adding an association [(a,b)] both
+   [a] and [b] must be unique.
+
+   Map is a reasonably efficient datastructure, which compares rather
+   well (in average) to the more imperative Hashtables. In that respect
+   and since persistent datastructures are used in the kernel, I write
+   this in the functional style.
+
+   This module have been originally written for being used both in the
+   retroknowledge for its internal representation (thus in the kernel)
+   and in the interactive proof system for associating dependent goals
+   to an evar. *)
+
+
+
+type ('a,'b) biassoc
+(** the type of bidirectional association table between
+    ['a] and ['b] *)
+    
+val empty : ('a,'b) biassoc
+(** the empty bidirectional association table *)
+val is_empty : ('a,'b) biassoc -> bool
+(** tests the emptyness of a bidirectional association table *)
+val add : 'a -> 'b -> ('a,'b) biassoc -> ('a,'b) biassoc
+(** [add lt rt bm] return a bidirectional association table identical 
+    to [bm] except that there is an additional association between
+    [lt] and [rt].
+    If [lt] or [rt] are already present in an association in [bm]
+    then it raises [Invalid_argument "Biassoc: non unique values"] 
+    instead *)
+val find_with_left : 'a  -> ('a,'b) biassoc -> 'b
+(** [find_with_left lt bm] returns the value associated to [lt] it 
+    there is one. It raises [Not_found] otherwise. *)
+val find_with_right : 'b -> ('a,'b) biassoc -> 'a
+(** [find_with_right] works as [find_with_left] except that
+    it implements the other direction of the association. *)
+val remove_with_left : 'a -> ('a,'b) biassoc -> ('a,'b) biassoc
+(** [remove_with_left lt bm] returns a stack identical to [bm]
+    except that any association with [lt] has been removed. *)
+val remove_with_right : 'b -> ('a,'b) biassoc -> ('a,'b) biassoc
+(** [remove_with_right] works as [remove_with_left] except that
+    the key is from the right side of the associations. *)
+val mem_with_left : 'a -> ('a,'b) biassoc -> bool
+(** [mem_with_left lt bm] returns [true] if there is a value
+    associated to [lt] in [bm]. It returns [false] otherwise. *)
+val mem_with_right : 'b -> ('a,'b) biassoc -> bool
+(** [mem_with_right] works as [mem_with_left] except that it
+    implements the other direction. *)