wenzelm@2402: (*  Title:      Pure/basis.ML
paulson@2217:     ID:         $Id$
paulson@2217:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2217:     Copyright   1993  University of Cambridge
paulson@2217: 
wenzelm@2402: Basis Library emulation.
paulson@2217: 
wenzelm@2402: Needed for Poly/ML and Standard ML of New Jersey version 0.93 to 1.08.
paulson@2217: 
paulson@2217: Full compatibility cannot be obtained using a file: what about char constants?
paulson@2217: *)
paulson@2217: 
paulson@2265: exception Subscript;
paulson@2265: 
paulson@2230: structure Bool =
paulson@2230:   struct
paulson@2230:   fun toString true  = "true"
paulson@2230:     | toString false = "false"
paulson@2230:   end;
paulson@2230: 
paulson@3244: 
paulson@3244: structure Option =
paulson@2862:   struct
paulson@2862:   exception Option
paulson@2862: 
paulson@2862:   datatype 'a option = NONE | SOME of 'a
paulson@2862: 
paulson@2862:   fun getOpt (SOME v, _) = v
paulson@2862:     | getOpt (NONE,   a) = a
paulson@2862: 
paulson@2862:   fun isSome (SOME _) = true 
paulson@2862:     | isSome NONE     = false
paulson@2862: 
paulson@2862:   fun valOf (SOME v) = v
paulson@2862:     | valOf NONE     = raise Option
paulson@2862:   end;
paulson@2862: 
paulson@2862: 
paulson@2217: structure Int =
paulson@2217:   struct
paulson@2230:   fun toString (i: int) = makestring i;
paulson@2217:   fun max (x, y) = if x < y then y else x : int;
paulson@2217:   fun min (x, y) = if x < y then x else y : int;
paulson@2217:   end;
paulson@2217: 
paulson@2265: 
paulson@2265: structure List =
paulson@2265:   struct
paulson@2265:   exception Empty
paulson@2265: 
paulson@2265:   fun last []      = raise Empty
paulson@2265:     | last [x]     = x
paulson@2265:     | last (x::xs) = last xs;
paulson@2265: 
paulson@2265:   fun nth (xs, n) =
paulson@2265:       let fun h []      _ = raise Subscript
paulson@2265: 	    | h (x::xs) n = if n=0 then x else h xs (n-1)
paulson@2265:       in if n<0 then raise Subscript else h xs n end;
paulson@2265: 
paulson@2265:   fun drop (xs, n) =
paulson@2265:       let fun h xs      0 = xs
paulson@2265: 	    | h []      n = raise Subscript
paulson@2265: 	    | h (x::xs) n = h xs (n-1)
paulson@2265:       in if n<0 then raise Subscript else h xs n end;
paulson@2265: 
paulson@2265:   fun take (xs, n) =
paulson@2265:       let fun h xs      0 = []
paulson@2265: 	    | h []      n = raise Subscript
paulson@2265: 	    | h (x::xs) n = x :: h xs (n-1)
paulson@2265:       in if n<0 then raise Subscript else h xs n end;
paulson@2265: 
paulson@2265:   fun concat []      = []
paulson@2265:     | concat (l::ls) = l @ concat ls;
paulson@2862: 
paulson@2862:   fun mapPartial f []      = []
paulson@2862:     | mapPartial f (x::xs) = 
paulson@3244:          (case f x of Option.NONE   => mapPartial f xs
paulson@3244:                     | Option.SOME y => y :: mapPartial f xs);
paulson@2884: 
paulson@3244:   fun find _ []        = Option.NONE
paulson@3244:     | find p (x :: xs) = if p x then Option.SOME x else find p xs;
paulson@2884: 
paulson@2884: 
paulson@2884:   (*copy the list preserving elements that satisfy the predicate*)
paulson@2884:   fun filter p [] = []
paulson@2884:     | filter p (x :: xs) = if p x then x :: filter p xs else filter p xs;
paulson@2884: 
paulson@2884:   (*Partition list into elements that satisfy predicate and those that don't.
paulson@2884:     Preserves order of elements in both lists.*)
paulson@2884:   fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) =
paulson@2884:       let fun part ([], answer) = answer
paulson@2884: 	    | part (x::xs, (ys, ns)) = if p(x)
paulson@2884: 	      then  part (xs, (x::ys, ns))
paulson@2884: 	      else  part (xs, (ys, x::ns))
paulson@2884:       in  part (rev ys, ([], []))  end;
paulson@2884: 
paulson@2265:   end;
paulson@2265: 
paulson@2265: 
paulson@2265: structure ListPair =
paulson@2265:   struct
paulson@2265:   fun zip ([], [])      = []
paulson@2265:     | zip (x::xs,y::ys) = (x,y) :: zip(xs,ys);
paulson@2265: 
paulson@2265:   fun unzip [] = ([],[])
paulson@2265:     | unzip((x,y)::pairs) =
paulson@2265: 	  let val (xs,ys) = unzip pairs
paulson@2265: 	  in  (x::xs, y::ys)  end;
paulson@2265: 
paulson@2265:   fun map f ([], [])      = []
paulson@2265:     | map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys);
paulson@2265: 
paulson@2884:   fun exists p =
paulson@2265:     let fun boolf ([], [])      = false
paulson@2884: 	  | boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys)
paulson@2265:     in boolf end;
paulson@2265: 
paulson@2884:   fun all p =
paulson@2265:     let fun boolf ([], [])      = true
paulson@2884: 	  | boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys)
paulson@2265:     in boolf end;
paulson@2265:   end;
paulson@2265: 
paulson@2265: 
paulson@2217: structure TextIO =
paulson@2217:   struct
paulson@2217:   type instream = instream
paulson@2217:   and  outstream = outstream
paulson@2217:   exception Io of {name: string, function: string, cause: exn}
paulson@2217:   val stdIn 	= std_in
paulson@2217:   val stdOut 	= std_out
paulson@2217:   val openIn 	= open_in
paulson@2217:   val openAppend = open_append
paulson@2217:   val openOut 	= open_out
paulson@2217:   val closeIn 	= close_in
paulson@2217:   val closeOut 	= close_out
paulson@2217:   val inputN 	= input
paulson@2217:   val inputAll  = fn is => inputN (is, 999999)
paulson@2217:   val inputLine = input_line
paulson@2217:   val endOfStream = end_of_stream
paulson@2217:   val output 	= output
paulson@2217:   val flushOut 	= flush_out
paulson@2217:   end;
paulson@2470: 
paulson@2470: 
paulson@2470: fun print s = (output (std_out, s); flush_out std_out);