# HG changeset patch
# User paulson
# Date 849174139 -3600
# Node ID 3123fef88dce17e91ce873a03a9ed1963aefcd97
# Parent  f298678bd54a9b6d9ae1809d217d10b2107c6ef2
Addition of structures List and ListPair

diff -r f298678bd54a -r 3123fef88dce src/Pure/basis.ML
--- a/src/Pure/basis.ML	Thu Nov 28 10:41:14 1996 +0100
+++ b/src/Pure/basis.ML	Thu Nov 28 10:42:19 1996 +0100
@@ -10,6 +10,8 @@
 Full compatibility cannot be obtained using a file: what about char constants?
 *)
 
+exception Subscript;
+
 structure Bool =
   struct
   fun toString true  = "true"
@@ -23,6 +25,62 @@
   fun min (x, y) = if x < y then x else y : int;
   end;
 
+
+structure List =
+  struct
+  exception Empty
+
+  fun last []      = raise Empty
+    | last [x]     = x
+    | last (x::xs) = last xs;
+
+  fun nth (xs, n) =
+      let fun h []      _ = raise Subscript
+	    | h (x::xs) n = if n=0 then x else h xs (n-1)
+      in if n<0 then raise Subscript else h xs n end;
+
+  fun drop (xs, n) =
+      let fun h xs      0 = xs
+	    | h []      n = raise Subscript
+	    | h (x::xs) n = h xs (n-1)
+      in if n<0 then raise Subscript else h xs n end;
+
+  fun take (xs, n) =
+      let fun h xs      0 = []
+	    | h []      n = raise Subscript
+	    | h (x::xs) n = x :: h xs (n-1)
+      in if n<0 then raise Subscript else h xs n end;
+
+  fun concat []      = []
+    | concat (l::ls) = l @ concat ls;
+  end;
+
+
+structure ListPair =
+  struct
+  fun zip ([], [])      = []
+    | zip (x::xs,y::ys) = (x,y) :: zip(xs,ys);
+
+  fun unzip [] = ([],[])
+    | unzip((x,y)::pairs) =
+	  let val (xs,ys) = unzip pairs
+	  in  (x::xs, y::ys)  end;
+
+  fun map f ([], [])      = []
+    | map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys);
+
+  fun exists pred =
+    let fun boolf ([], [])      = false
+	  | boolf (x::xs,y::ys) = pred(x,y) orelse boolf (xs,ys)
+    in boolf end;
+
+  fun all pred =
+    let fun boolf ([], [])      = true
+	  | boolf (x::xs,y::ys) = pred(x,y) andalso boolf (xs,ys)
+    in boolf end;
+  end;
+
+
 structure TextIO =
   struct
   type instream = instream