wenzelm@2402
|
1 |
(* Title: Pure/basis.ML
|
paulson@2217
|
2 |
ID: $Id$
|
paulson@2217
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
paulson@2217
|
4 |
Copyright 1993 University of Cambridge
|
paulson@2217
|
5 |
|
wenzelm@2402
|
6 |
Basis Library emulation.
|
paulson@2217
|
7 |
|
wenzelm@2402
|
8 |
Needed for Poly/ML and Standard ML of New Jersey version 0.93 to 1.08.
|
paulson@2217
|
9 |
|
paulson@2217
|
10 |
Full compatibility cannot be obtained using a file: what about char constants?
|
paulson@2217
|
11 |
*)
|
paulson@2217
|
12 |
|
paulson@2265
|
13 |
exception Subscript;
|
paulson@2265
|
14 |
|
paulson@2230
|
15 |
structure Bool =
|
paulson@2230
|
16 |
struct
|
paulson@2230
|
17 |
fun toString true = "true"
|
paulson@2230
|
18 |
| toString false = "false"
|
paulson@2230
|
19 |
end;
|
paulson@2230
|
20 |
|
paulson@3244
|
21 |
|
paulson@3244
|
22 |
structure Option =
|
paulson@2862
|
23 |
struct
|
paulson@2862
|
24 |
exception Option
|
paulson@2862
|
25 |
|
paulson@2862
|
26 |
datatype 'a option = NONE | SOME of 'a
|
paulson@2862
|
27 |
|
paulson@2862
|
28 |
fun getOpt (SOME v, _) = v
|
paulson@2862
|
29 |
| getOpt (NONE, a) = a
|
paulson@2862
|
30 |
|
paulson@2862
|
31 |
fun isSome (SOME _) = true
|
paulson@2862
|
32 |
| isSome NONE = false
|
paulson@2862
|
33 |
|
paulson@2862
|
34 |
fun valOf (SOME v) = v
|
paulson@2862
|
35 |
| valOf NONE = raise Option
|
paulson@2862
|
36 |
end;
|
paulson@2862
|
37 |
|
paulson@2862
|
38 |
|
paulson@2217
|
39 |
structure Int =
|
paulson@2217
|
40 |
struct
|
paulson@2230
|
41 |
fun toString (i: int) = makestring i;
|
paulson@2217
|
42 |
fun max (x, y) = if x < y then y else x : int;
|
paulson@2217
|
43 |
fun min (x, y) = if x < y then x else y : int;
|
paulson@2217
|
44 |
end;
|
paulson@2217
|
45 |
|
paulson@2265
|
46 |
|
paulson@2265
|
47 |
structure List =
|
paulson@2265
|
48 |
struct
|
paulson@2265
|
49 |
exception Empty
|
paulson@2265
|
50 |
|
paulson@2265
|
51 |
fun last [] = raise Empty
|
paulson@2265
|
52 |
| last [x] = x
|
paulson@2265
|
53 |
| last (x::xs) = last xs;
|
paulson@2265
|
54 |
|
paulson@2265
|
55 |
fun nth (xs, n) =
|
paulson@2265
|
56 |
let fun h [] _ = raise Subscript
|
paulson@2265
|
57 |
| h (x::xs) n = if n=0 then x else h xs (n-1)
|
paulson@2265
|
58 |
in if n<0 then raise Subscript else h xs n end;
|
paulson@2265
|
59 |
|
paulson@2265
|
60 |
fun drop (xs, n) =
|
paulson@2265
|
61 |
let fun h xs 0 = xs
|
paulson@2265
|
62 |
| h [] n = raise Subscript
|
paulson@2265
|
63 |
| h (x::xs) n = h xs (n-1)
|
paulson@2265
|
64 |
in if n<0 then raise Subscript else h xs n end;
|
paulson@2265
|
65 |
|
paulson@2265
|
66 |
fun take (xs, n) =
|
paulson@2265
|
67 |
let fun h xs 0 = []
|
paulson@2265
|
68 |
| h [] n = raise Subscript
|
paulson@2265
|
69 |
| h (x::xs) n = x :: h xs (n-1)
|
paulson@2265
|
70 |
in if n<0 then raise Subscript else h xs n end;
|
paulson@2265
|
71 |
|
paulson@2265
|
72 |
fun concat [] = []
|
paulson@2265
|
73 |
| concat (l::ls) = l @ concat ls;
|
paulson@2862
|
74 |
|
paulson@2862
|
75 |
fun mapPartial f [] = []
|
paulson@2862
|
76 |
| mapPartial f (x::xs) =
|
paulson@3244
|
77 |
(case f x of Option.NONE => mapPartial f xs
|
paulson@3244
|
78 |
| Option.SOME y => y :: mapPartial f xs);
|
paulson@2884
|
79 |
|
paulson@3244
|
80 |
fun find _ [] = Option.NONE
|
paulson@3244
|
81 |
| find p (x :: xs) = if p x then Option.SOME x else find p xs;
|
paulson@2884
|
82 |
|
paulson@2884
|
83 |
|
paulson@2884
|
84 |
(*copy the list preserving elements that satisfy the predicate*)
|
paulson@2884
|
85 |
fun filter p [] = []
|
paulson@2884
|
86 |
| filter p (x :: xs) = if p x then x :: filter p xs else filter p xs;
|
paulson@2884
|
87 |
|
paulson@2884
|
88 |
(*Partition list into elements that satisfy predicate and those that don't.
|
paulson@2884
|
89 |
Preserves order of elements in both lists.*)
|
paulson@2884
|
90 |
fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) =
|
paulson@2884
|
91 |
let fun part ([], answer) = answer
|
paulson@2884
|
92 |
| part (x::xs, (ys, ns)) = if p(x)
|
paulson@2884
|
93 |
then part (xs, (x::ys, ns))
|
paulson@2884
|
94 |
else part (xs, (ys, x::ns))
|
paulson@2884
|
95 |
in part (rev ys, ([], [])) end;
|
paulson@2884
|
96 |
|
paulson@2265
|
97 |
end;
|
paulson@2265
|
98 |
|
paulson@2265
|
99 |
|
paulson@2265
|
100 |
structure ListPair =
|
paulson@2265
|
101 |
struct
|
paulson@2265
|
102 |
fun zip ([], []) = []
|
paulson@2265
|
103 |
| zip (x::xs,y::ys) = (x,y) :: zip(xs,ys);
|
paulson@2265
|
104 |
|
paulson@2265
|
105 |
fun unzip [] = ([],[])
|
paulson@2265
|
106 |
| unzip((x,y)::pairs) =
|
paulson@2265
|
107 |
let val (xs,ys) = unzip pairs
|
paulson@2265
|
108 |
in (x::xs, y::ys) end;
|
paulson@2265
|
109 |
|
paulson@2265
|
110 |
fun map f ([], []) = []
|
paulson@2265
|
111 |
| map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys);
|
paulson@2265
|
112 |
|
paulson@2884
|
113 |
fun exists p =
|
paulson@2265
|
114 |
let fun boolf ([], []) = false
|
paulson@2884
|
115 |
| boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys)
|
paulson@2265
|
116 |
in boolf end;
|
paulson@2265
|
117 |
|
paulson@2884
|
118 |
fun all p =
|
paulson@2265
|
119 |
let fun boolf ([], []) = true
|
paulson@2884
|
120 |
| boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys)
|
paulson@2265
|
121 |
in boolf end;
|
paulson@2265
|
122 |
end;
|
paulson@2265
|
123 |
|
paulson@2265
|
124 |
|
paulson@2217
|
125 |
structure TextIO =
|
paulson@2217
|
126 |
struct
|
paulson@2217
|
127 |
type instream = instream
|
paulson@2217
|
128 |
and outstream = outstream
|
paulson@2217
|
129 |
exception Io of {name: string, function: string, cause: exn}
|
paulson@2217
|
130 |
val stdIn = std_in
|
paulson@2217
|
131 |
val stdOut = std_out
|
paulson@2217
|
132 |
val openIn = open_in
|
paulson@2217
|
133 |
val openAppend = open_append
|
paulson@2217
|
134 |
val openOut = open_out
|
paulson@2217
|
135 |
val closeIn = close_in
|
paulson@2217
|
136 |
val closeOut = close_out
|
paulson@2217
|
137 |
val inputN = input
|
paulson@2217
|
138 |
val inputAll = fn is => inputN (is, 999999)
|
paulson@2217
|
139 |
val inputLine = input_line
|
paulson@2217
|
140 |
val endOfStream = end_of_stream
|
paulson@2217
|
141 |
val output = output
|
paulson@2217
|
142 |
val flushOut = flush_out
|
paulson@2217
|
143 |
end;
|
paulson@2470
|
144 |
|
paulson@2470
|
145 |
|
paulson@2470
|
146 |
fun print s = (output (std_out, s); flush_out std_out);
|