--- a/src/Pure/basis.ML Fri Jun 04 11:51:31 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,192 +0,0 @@
-(* Title: Pure/basis.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Basis Library emulation. Needed for Poly/ML and Standard ML of New
-Jersey version 0.93 to 1.08. Full compatibility cannot be obtained
-using a file: what about char constants?
-*)
-
-exception Subscript;
-
-structure Bool =
- struct
- fun toString true = "true"
- | toString false = "false"
- end;
-
-
-structure Option =
- struct
- exception Option
-
- datatype 'a option = NONE | SOME of 'a
-
- fun getOpt (SOME v, _) = v
- | getOpt (NONE, a) = a
-
- fun isSome (SOME _) = true
- | isSome NONE = false
-
- fun valOf (SOME v) = v
- | valOf NONE = raise Option
- end;
-
-
-structure Int =
- struct
- type int = int
- fun toString (i: int) = makestring i;
- fun max (x, y) = if x < y then y else x : int;
- fun min (x, y) = if x < y then x else y : int;
- end;
-
-
-structure Real =
- struct
- fun toString (x: real) = makestring x;
- fun max (x, y) = if x < y then y else x : real;
- fun min (x, y) = if x < y then x else y : real;
- val real = real;
- val floor = floor;
- fun ceil x = ~1 - floor (~ (x + 1.0));
- fun round x = floor (x + 0.5); (*does not do round-to-nearest*)
- fun trunc x = if x < 0.0 then ceil x else floor x;
- 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;
-
- fun mapPartial f [] = []
- | mapPartial f (x::xs) =
- (case f x of Option.NONE => mapPartial f xs
- | Option.SOME y => y :: mapPartial f xs);
-
- fun find _ [] = Option.NONE
- | find p (x :: xs) = if p x then Option.SOME x else find p xs;
-
-
- (*copy the list preserving elements that satisfy the predicate*)
- fun filter p [] = []
- | filter p (x :: xs) = if p x then x :: filter p xs else filter p xs;
-
- (*Partition list into elements that satisfy predicate and those that don't.
- Preserves order of elements in both lists.*)
- fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) =
- let fun part ([], answer) = answer
- | part (x::xs, (ys, ns)) = if p(x)
- then part (xs, (x::ys, ns))
- else part (xs, (ys, x::ns))
- in part (rev ys, ([], [])) end;
-
- 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 p =
- let fun boolf ([], []) = false
- | boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys)
- in boolf end;
-
- fun all p =
- let fun boolf ([], []) = true
- | boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys)
- in boolf end;
- end;
-
-
-structure TextIO =
- struct
- type instream = instream
- and outstream = outstream
- exception Io of {name: string, function: string, cause: exn}
- val stdIn = std_in
- val stdOut = std_out
- val stdErr = std_out
- val openIn = open_in
- val openAppend = open_append
- val openOut = open_out
- val closeIn = close_in
- val closeOut = close_out
- val inputN = input
- val inputAll = fn is => inputN (is, 999999)
- val inputLine = input_line
- val endOfStream = end_of_stream
- val output = output
- val flushOut = flush_out
- end;
-
-
-fun print s = (output (std_out, s); flush_out std_out);
-
-
-structure General =
-struct
-
-local
- fun raised name = "exception " ^ name ^ " raised";
- fun raised_msg name msg = raised name ^ ": " ^ msg;
-in
- fun exnMessage Match = raised_msg "Match" "nonexhaustive match failure"
- | exnMessage Bind = raised_msg "Bind" "nonexhaustive binding failure"
- | exnMessage (Io msg) = "I/O error: " ^ msg
- | exnMessage Neg = raised "Neg"
- | exnMessage Sum = raised "Sum"
- | exnMessage Diff = raised "Diff"
- | exnMessage Prod = raised "Prod"
- | exnMessage Quot = raised "Quot"
- | exnMessage Abs = raised "Abs"
- | exnMessage Div = raised "Div"
- | exnMessage Mod = raised "Mod"
- | exnMessage Floor = raised "Floor"
- | exnMessage Sqrt = raised "Sqrt"
- | exnMessage Exp = raised "Exp"
- | exnMessage Ln = raised "Ln"
- | exnMessage Ord = raised "Ord"
- | exnMessage Subscript = raised_msg "Subscript " "subscript out of bounds"
- | exnMessage Option.Option = raised "Option.Option"
- | exnMessage List.Empty = raised "List.Empty"
- | exnMessage (TextIO.Io {name, ...}) = raised_msg "TextIO.Io" name
- | exnMessage exn = raised "???";
-end;
-
-end;