src/Tools/Metis/src/Sharing.sig
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 39502 cffceed8e7fa
child 72004 913162a47d9f
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;

(* ========================================================================= *)
(* PRESERVING SHARING OF ML VALUES                                           *)
(* Copyright (c) 2005 Joe Hurd, distributed under the BSD License            *)
(* ========================================================================= *)

signature Sharing =
sig

(* ------------------------------------------------------------------------- *)
(* Option operations.                                                        *)
(* ------------------------------------------------------------------------- *)

val mapOption : ('a -> 'a) -> 'a option -> 'a option

val mapsOption : ('a -> 's -> 'a * 's) -> 'a option -> 's -> 'a option * 's

(* ------------------------------------------------------------------------- *)
(* List operations.                                                          *)
(* ------------------------------------------------------------------------- *)

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

(* ------------------------------------------------------------------------- *)
(* Function caching.                                                         *)
(* ------------------------------------------------------------------------- *)

val cache : ('a * 'a -> order) -> ('a -> 'b) -> 'a -> 'b

(* ------------------------------------------------------------------------- *)
(* Hash consing.                                                             *)
(* ------------------------------------------------------------------------- *)

val hashCons : ('a * 'a -> order) -> 'a -> 'a

end