# HG changeset patch
# User wenzelm
# Date 1085167662 -7200
# Node ID b7dac2fae5bb3b21d0a20bd59cf02cec323aa3a8
# Parent  23e51b22c710ec601d41d7546dfe4fd837a2db11
added fold, product; removed transitive_closure;

diff -r 23e51b22c710 -r b7dac2fae5bb src/Pure/library.ML
--- a/src/Pure/library.ML	Fri May 21 21:27:10 2004 +0200
+++ b/src/Pure/library.ML	Fri May 21 21:27:42 2004 +0200
@@ -86,6 +86,7 @@
   val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
   val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
+  val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
   val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val length: 'a list -> int
@@ -108,6 +109,7 @@
   val separate: 'a -> 'a list -> 'a list
   val replicate: int -> 'a -> 'a list
   val multiply: 'a list * 'a list list -> 'a list list
+  val product: 'a list -> 'b list -> ('a * 'b) list
   val filter: ('a -> bool) -> 'a list -> 'a list
   val filter_out: ('a -> bool) -> 'a list -> 'a list
   val mapfilter: ('a -> 'b option) -> 'a list -> 'b list
@@ -287,7 +289,6 @@
   val partition: ('a -> bool) -> 'a list -> 'a list * 'a list
   val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
   val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
-  val transitive_closure: (string * string list) list -> (string * string list) list
   val gensym: string -> string
   val scanwords: (string -> bool) -> string list -> string list
   datatype 'a mtree = Join of 'a * 'a mtree list
@@ -493,6 +494,8 @@
         | itr (x::l) = f(x, itr l)
   in  itr l  end;
 
+fun fold f xs y = foldl (fn (y', x) => f x y') (y, xs);
+
 fun foldl_map _ (x, []) = (x, [])
   | foldl_map f (x, y :: ys) =
       let
@@ -607,6 +610,11 @@
 fun multiply ([], _) = []
   | multiply (x :: xs, yss) = map (cons x) yss @ multiply (xs, yss);
 
+(*direct product*)
+fun product _ [] = []
+  | product [] _ = []
+  | product (x :: xs) ys = map (pair x) ys @ product xs ys;
+
 
 (* filter *)
 
@@ -1361,17 +1369,6 @@
   in  part i end;
 
 
-(* transitive closure (not Warshall's algorithm) *)
-
-fun transitive_closure [] = []
-  | transitive_closure ((x, ys)::ps) =
-      let val qs = transitive_closure ps
-          val zs = foldl (fn (zs, y) => assocs qs y union_string zs) (ys, ys)
-          fun step(u, us) = (u, if x mem_string us then zs union_string us
-                                else us)
-      in (x, zs) :: map step qs end;
-
-
 (* generating identifiers *)
 
 (** Freshly generated identifiers; supplied prefix MUST start with a letter **)