author | wenzelm |
Fri, 28 Feb 1997 16:38:55 +0100 | |
changeset 2692 | 484ec6ca0c50 |
parent 2470 | 273580d5c040 |
child 2862 | 3f38cbd57d47 |
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 |
||
2402 | 6 |
Basis Library emulation. |
2217 | 7 |
|
2402 | 8 |
Needed for Poly/ML and Standard ML of New Jersey version 0.93 to 1.08. |
2217 | 9 |
|
10 |
Full compatibility cannot be obtained using a file: what about char constants? |
|
11 |
*) |
|
12 |
||
2265 | 13 |
exception Subscript; |
14 |
||
2230
275a5a699ff7
Structure Bool and value Int.toString needed to replace makestring calls
paulson
parents:
2217
diff
changeset
|
15 |
structure Bool = |
275a5a699ff7
Structure Bool and value Int.toString needed to replace makestring calls
paulson
parents:
2217
diff
changeset
|
16 |
struct |
275a5a699ff7
Structure Bool and value Int.toString needed to replace makestring calls
paulson
parents:
2217
diff
changeset
|
17 |
fun toString true = "true" |
275a5a699ff7
Structure Bool and value Int.toString needed to replace makestring calls
paulson
parents:
2217
diff
changeset
|
18 |
| toString false = "false" |
275a5a699ff7
Structure Bool and value Int.toString needed to replace makestring calls
paulson
parents:
2217
diff
changeset
|
19 |
end; |
275a5a699ff7
Structure Bool and value Int.toString needed to replace makestring calls
paulson
parents:
2217
diff
changeset
|
20 |
|
2217 | 21 |
structure Int = |
22 |
struct |
|
2230
275a5a699ff7
Structure Bool and value Int.toString needed to replace makestring calls
paulson
parents:
2217
diff
changeset
|
23 |
fun toString (i: int) = makestring i; |
2217 | 24 |
fun max (x, y) = if x < y then y else x : int; |
25 |
fun min (x, y) = if x < y then x else y : int; |
|
26 |
end; |
|
27 |
||
2265 | 28 |
|
29 |
structure List = |
|
30 |
struct |
|
31 |
exception Empty |
|
32 |
||
33 |
fun last [] = raise Empty |
|
34 |
| last [x] = x |
|
35 |
| last (x::xs) = last xs; |
|
36 |
||
37 |
fun nth (xs, n) = |
|
38 |
let fun h [] _ = raise Subscript |
|
39 |
| h (x::xs) n = if n=0 then x else h xs (n-1) |
|
40 |
in if n<0 then raise Subscript else h xs n end; |
|
41 |
||
42 |
fun drop (xs, n) = |
|
43 |
let fun h xs 0 = xs |
|
44 |
| h [] n = raise Subscript |
|
45 |
| h (x::xs) n = h xs (n-1) |
|
46 |
in if n<0 then raise Subscript else h xs n end; |
|
47 |
||
48 |
fun take (xs, n) = |
|
49 |
let fun h xs 0 = [] |
|
50 |
| h [] n = raise Subscript |
|
51 |
| h (x::xs) n = x :: h xs (n-1) |
|
52 |
in if n<0 then raise Subscript else h xs n end; |
|
53 |
||
54 |
fun concat [] = [] |
|
55 |
| concat (l::ls) = l @ concat ls; |
|
56 |
end; |
|
57 |
||
58 |
||
59 |
structure ListPair = |
|
60 |
struct |
|
61 |
fun zip ([], []) = [] |
|
62 |
| zip (x::xs,y::ys) = (x,y) :: zip(xs,ys); |
|
63 |
||
64 |
fun unzip [] = ([],[]) |
|
65 |
| unzip((x,y)::pairs) = |
|
66 |
let val (xs,ys) = unzip pairs |
|
67 |
in (x::xs, y::ys) end; |
|
68 |
||
69 |
fun map f ([], []) = [] |
|
70 |
| map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys); |
|
71 |
||
72 |
fun exists pred = |
|
73 |
let fun boolf ([], []) = false |
|
74 |
| boolf (x::xs,y::ys) = pred(x,y) orelse boolf (xs,ys) |
|
75 |
in boolf end; |
|
76 |
||
77 |
fun all pred = |
|
78 |
let fun boolf ([], []) = true |
|
79 |
| boolf (x::xs,y::ys) = pred(x,y) andalso boolf (xs,ys) |
|
80 |
in boolf end; |
|
81 |
end; |
|
82 |
||
83 |
||
2217 | 84 |
structure TextIO = |
85 |
struct |
|
86 |
type instream = instream |
|
87 |
and outstream = outstream |
|
88 |
exception Io of {name: string, function: string, cause: exn} |
|
89 |
val stdIn = std_in |
|
90 |
val stdOut = std_out |
|
91 |
val openIn = open_in |
|
92 |
val openAppend = open_append |
|
93 |
val openOut = open_out |
|
94 |
val closeIn = close_in |
|
95 |
val closeOut = close_out |
|
96 |
val inputN = input |
|
97 |
val inputAll = fn is => inputN (is, 999999) |
|
98 |
val inputLine = input_line |
|
99 |
val endOfStream = end_of_stream |
|
100 |
val output = output |
|
101 |
val flushOut = flush_out |
|
102 |
end; |
|
2470
273580d5c040
A definition of "print", unfortunately overridden by each "open PolyML"
paulson
parents:
2402
diff
changeset
|
103 |
|
273580d5c040
A definition of "print", unfortunately overridden by each "open PolyML"
paulson
parents:
2402
diff
changeset
|
104 |
|
273580d5c040
A definition of "print", unfortunately overridden by each "open PolyML"
paulson
parents:
2402
diff
changeset
|
105 |
fun print s = (output (std_out, s); flush_out std_out); |