author | paulson |
Tue, 18 Nov 2003 11:03:56 +0100 | |
changeset 14261 | 6c418d139f74 |
parent 13037 | f7f29f8380ce |
permissions | -rw-r--r-- |
2402 | 1 |
(* Title: Pure/basis.ML |
2217 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
5021 | 6 |
Basis Library emulation. Needed for Poly/ML and Standard ML of New |
7 |
Jersey version 0.93 to 1.08. Full compatibility cannot be obtained |
|
8 |
using a file: what about char constants? |
|
2217 | 9 |
*) |
10 |
||
2265 | 11 |
exception Subscript; |
12 |
||
2230
275a5a699ff7
Structure Bool and value Int.toString needed to replace makestring calls
paulson
parents:
2217
diff
changeset
|
13 |
structure Bool = |
275a5a699ff7
Structure Bool and value Int.toString needed to replace makestring calls
paulson
parents:
2217
diff
changeset
|
14 |
struct |
275a5a699ff7
Structure Bool and value Int.toString needed to replace makestring calls
paulson
parents:
2217
diff
changeset
|
15 |
fun toString true = "true" |
275a5a699ff7
Structure Bool and value Int.toString needed to replace makestring calls
paulson
parents:
2217
diff
changeset
|
16 |
| toString false = "false" |
275a5a699ff7
Structure Bool and value Int.toString needed to replace makestring calls
paulson
parents:
2217
diff
changeset
|
17 |
end; |
275a5a699ff7
Structure Bool and value Int.toString needed to replace makestring calls
paulson
parents:
2217
diff
changeset
|
18 |
|
3244
71b760618f30
Basis library version of type "option" now resides in its own structure Option
paulson
parents:
3047
diff
changeset
|
19 |
|
71b760618f30
Basis library version of type "option" now resides in its own structure Option
paulson
parents:
3047
diff
changeset
|
20 |
structure Option = |
2862 | 21 |
struct |
22 |
exception Option |
|
23 |
||
24 |
datatype 'a option = NONE | SOME of 'a |
|
25 |
||
26 |
fun getOpt (SOME v, _) = v |
|
27 |
| getOpt (NONE, a) = a |
|
28 |
||
29 |
fun isSome (SOME _) = true |
|
30 |
| isSome NONE = false |
|
31 |
||
32 |
fun valOf (SOME v) = v |
|
33 |
| valOf NONE = raise Option |
|
34 |
end; |
|
35 |
||
36 |
||
2217 | 37 |
structure Int = |
38 |
struct |
|
5643 | 39 |
type int = int |
2230
275a5a699ff7
Structure Bool and value Int.toString needed to replace makestring calls
paulson
parents:
2217
diff
changeset
|
40 |
fun toString (i: int) = makestring i; |
2217 | 41 |
fun max (x, y) = if x < y then y else x : int; |
42 |
fun min (x, y) = if x < y then x else y : int; |
|
43 |
end; |
|
44 |
||
2265 | 45 |
|
5208
cea0adbc7276
added Real structure (taken from SML/NJ basis lib);
wenzelm
parents:
5021
diff
changeset
|
46 |
structure Real = |
cea0adbc7276
added Real structure (taken from SML/NJ basis lib);
wenzelm
parents:
5021
diff
changeset
|
47 |
struct |
cea0adbc7276
added Real structure (taken from SML/NJ basis lib);
wenzelm
parents:
5021
diff
changeset
|
48 |
fun toString (x: real) = makestring x; |
cea0adbc7276
added Real structure (taken from SML/NJ basis lib);
wenzelm
parents:
5021
diff
changeset
|
49 |
fun max (x, y) = if x < y then y else x : real; |
cea0adbc7276
added Real structure (taken from SML/NJ basis lib);
wenzelm
parents:
5021
diff
changeset
|
50 |
fun min (x, y) = if x < y then x else y : real; |
cea0adbc7276
added Real structure (taken from SML/NJ basis lib);
wenzelm
parents:
5021
diff
changeset
|
51 |
val real = real; |
cea0adbc7276
added Real structure (taken from SML/NJ basis lib);
wenzelm
parents:
5021
diff
changeset
|
52 |
val floor = floor; |
cea0adbc7276
added Real structure (taken from SML/NJ basis lib);
wenzelm
parents:
5021
diff
changeset
|
53 |
fun ceil x = ~1 - floor (~ (x + 1.0)); |
cea0adbc7276
added Real structure (taken from SML/NJ basis lib);
wenzelm
parents:
5021
diff
changeset
|
54 |
fun round x = floor (x + 0.5); (*does not do round-to-nearest*) |
cea0adbc7276
added Real structure (taken from SML/NJ basis lib);
wenzelm
parents:
5021
diff
changeset
|
55 |
fun trunc x = if x < 0.0 then ceil x else floor x; |
cea0adbc7276
added Real structure (taken from SML/NJ basis lib);
wenzelm
parents:
5021
diff
changeset
|
56 |
end; |
cea0adbc7276
added Real structure (taken from SML/NJ basis lib);
wenzelm
parents:
5021
diff
changeset
|
57 |
|
cea0adbc7276
added Real structure (taken from SML/NJ basis lib);
wenzelm
parents:
5021
diff
changeset
|
58 |
|
2265 | 59 |
structure List = |
60 |
struct |
|
61 |
exception Empty |
|
62 |
||
63 |
fun last [] = raise Empty |
|
64 |
| last [x] = x |
|
65 |
| last (x::xs) = last xs; |
|
66 |
||
67 |
fun nth (xs, n) = |
|
68 |
let fun h [] _ = raise Subscript |
|
69 |
| h (x::xs) n = if n=0 then x else h xs (n-1) |
|
70 |
in if n<0 then raise Subscript else h xs n end; |
|
71 |
||
72 |
fun drop (xs, n) = |
|
73 |
let fun h xs 0 = xs |
|
74 |
| h [] n = raise Subscript |
|
75 |
| h (x::xs) n = h xs (n-1) |
|
76 |
in if n<0 then raise Subscript else h xs n end; |
|
77 |
||
78 |
fun take (xs, n) = |
|
79 |
let fun h xs 0 = [] |
|
80 |
| h [] n = raise Subscript |
|
81 |
| h (x::xs) n = x :: h xs (n-1) |
|
82 |
in if n<0 then raise Subscript else h xs n end; |
|
83 |
||
84 |
fun concat [] = [] |
|
85 |
| concat (l::ls) = l @ concat ls; |
|
2862 | 86 |
|
87 |
fun mapPartial f [] = [] |
|
88 |
| mapPartial f (x::xs) = |
|
3244
71b760618f30
Basis library version of type "option" now resides in its own structure Option
paulson
parents:
3047
diff
changeset
|
89 |
(case f x of Option.NONE => mapPartial f xs |
71b760618f30
Basis library version of type "option" now resides in its own structure Option
paulson
parents:
3047
diff
changeset
|
90 |
| Option.SOME y => y :: mapPartial f xs); |
2884 | 91 |
|
3244
71b760618f30
Basis library version of type "option" now resides in its own structure Option
paulson
parents:
3047
diff
changeset
|
92 |
fun find _ [] = Option.NONE |
71b760618f30
Basis library version of type "option" now resides in its own structure Option
paulson
parents:
3047
diff
changeset
|
93 |
| find p (x :: xs) = if p x then Option.SOME x else find p xs; |
2884 | 94 |
|
95 |
||
96 |
(*copy the list preserving elements that satisfy the predicate*) |
|
97 |
fun filter p [] = [] |
|
98 |
| filter p (x :: xs) = if p x then x :: filter p xs else filter p xs; |
|
99 |
||
100 |
(*Partition list into elements that satisfy predicate and those that don't. |
|
101 |
Preserves order of elements in both lists.*) |
|
102 |
fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) = |
|
103 |
let fun part ([], answer) = answer |
|
104 |
| part (x::xs, (ys, ns)) = if p(x) |
|
105 |
then part (xs, (x::ys, ns)) |
|
106 |
else part (xs, (ys, x::ns)) |
|
107 |
in part (rev ys, ([], [])) end; |
|
108 |
||
2265 | 109 |
end; |
110 |
||
111 |
||
112 |
structure ListPair = |
|
113 |
struct |
|
114 |
fun zip ([], []) = [] |
|
115 |
| zip (x::xs,y::ys) = (x,y) :: zip(xs,ys); |
|
116 |
||
117 |
fun unzip [] = ([],[]) |
|
118 |
| unzip((x,y)::pairs) = |
|
119 |
let val (xs,ys) = unzip pairs |
|
120 |
in (x::xs, y::ys) end; |
|
121 |
||
122 |
fun map f ([], []) = [] |
|
123 |
| map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys); |
|
124 |
||
2884 | 125 |
fun exists p = |
2265 | 126 |
let fun boolf ([], []) = false |
2884 | 127 |
| boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys) |
2265 | 128 |
in boolf end; |
129 |
||
2884 | 130 |
fun all p = |
2265 | 131 |
let fun boolf ([], []) = true |
2884 | 132 |
| boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys) |
2265 | 133 |
in boolf end; |
134 |
end; |
|
135 |
||
136 |
||
2217 | 137 |
structure TextIO = |
138 |
struct |
|
139 |
type instream = instream |
|
140 |
and outstream = outstream |
|
141 |
exception Io of {name: string, function: string, cause: exn} |
|
142 |
val stdIn = std_in |
|
143 |
val stdOut = std_out |
|
13037
f7f29f8380ce
val stdErr = std_out (std_err is unavaliable in polyml-3.x);
wenzelm
parents:
11852
diff
changeset
|
144 |
val stdErr = std_out |
2217 | 145 |
val openIn = open_in |
146 |
val openAppend = open_append |
|
147 |
val openOut = open_out |
|
148 |
val closeIn = close_in |
|
149 |
val closeOut = close_out |
|
150 |
val inputN = input |
|
151 |
val inputAll = fn is => inputN (is, 999999) |
|
152 |
val inputLine = input_line |
|
153 |
val endOfStream = end_of_stream |
|
154 |
val output = output |
|
155 |
val flushOut = flush_out |
|
156 |
end; |
|
2470
273580d5c040
A definition of "print", unfortunately overridden by each "open PolyML"
paulson
parents:
2402
diff
changeset
|
157 |
|
273580d5c040
A definition of "print", unfortunately overridden by each "open PolyML"
paulson
parents:
2402
diff
changeset
|
158 |
|
273580d5c040
A definition of "print", unfortunately overridden by each "open PolyML"
paulson
parents:
2402
diff
changeset
|
159 |
fun print s = (output (std_out, s); flush_out std_out); |
5021 | 160 |
|
161 |
||
162 |
structure General = |
|
163 |
struct |
|
164 |
||
165 |
local |
|
166 |
fun raised name = "exception " ^ name ^ " raised"; |
|
167 |
fun raised_msg name msg = raised name ^ ": " ^ msg; |
|
168 |
in |
|
169 |
fun exnMessage Match = raised_msg "Match" "nonexhaustive match failure" |
|
170 |
| exnMessage Bind = raised_msg "Bind" "nonexhaustive binding failure" |
|
171 |
| exnMessage (Io msg) = "I/O error: " ^ msg |
|
172 |
| exnMessage Neg = raised "Neg" |
|
173 |
| exnMessage Sum = raised "Sum" |
|
174 |
| exnMessage Diff = raised "Diff" |
|
175 |
| exnMessage Prod = raised "Prod" |
|
176 |
| exnMessage Quot = raised "Quot" |
|
177 |
| exnMessage Abs = raised "Abs" |
|
178 |
| exnMessage Div = raised "Div" |
|
179 |
| exnMessage Mod = raised "Mod" |
|
180 |
| exnMessage Floor = raised "Floor" |
|
181 |
| exnMessage Sqrt = raised "Sqrt" |
|
182 |
| exnMessage Exp = raised "Exp" |
|
183 |
| exnMessage Ln = raised "Ln" |
|
184 |
| exnMessage Ord = raised "Ord" |
|
185 |
| exnMessage Subscript = raised_msg "Subscript " "subscript out of bounds" |
|
186 |
| exnMessage Option.Option = raised "Option.Option" |
|
187 |
| exnMessage List.Empty = raised "List.Empty" |
|
188 |
| exnMessage (TextIO.Io {name, ...}) = raised_msg "TextIO.Io" name |
|
189 |
| exnMessage exn = raised "???"; |
|
190 |
end; |
|
191 |
||
192 |
end; |