src/Tools/Metis/src/Sharing.sig
changeset 39353 7f11d833d65b
parent 23510 4521fead5609
parent 39349 2d0a4361c3ef
child 39443 e330437cd22a
--- a/src/Tools/Metis/src/Sharing.sig	Mon Sep 13 16:44:20 2010 +0200
+++ b/src/Tools/Metis/src/Sharing.sig	Mon Sep 13 21:24:10 2010 +0200
@@ -1,16 +1,18 @@
 (* ========================================================================= *)
 (* PRESERVING SHARING OF ML VALUES                                           *)
-(* Copyright (c) 2005-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2005-2006 Joe Hurd, distributed under the BSD License       *)
 (* ========================================================================= *)
 
 signature Sharing =
 sig
 
 (* ------------------------------------------------------------------------- *)
-(* Pointer equality.                                                         *)
+(* Option operations.                                                        *)
 (* ------------------------------------------------------------------------- *)
 
-val pointerEqual : 'a * 'a -> bool
+val mapOption : ('a -> 'a) -> 'a option -> 'a option
+
+val mapsOption : ('a -> 's -> 'a * 's) -> 'a option -> 's -> 'a option * 's
 
 (* ------------------------------------------------------------------------- *)
 (* List operations.                                                          *)
@@ -18,6 +20,12 @@
 
 val map : ('a -> 'a) -> 'a list -> 'a list
 
+val revMap : ('a -> 'a) -> 'a list -> 'a list
+
+val maps : ('a -> 's -> 'a * 's) -> 'a list -> 's -> 'a list * 's
+
+val revMaps : ('a -> 's -> 'a * 's) -> 'a list -> 's -> 'a list * 's
+
 val updateNth : int * 'a -> 'a list -> 'a list
 
 val setify : ''a list -> ''a list