author | wenzelm |
Sat, 16 Feb 2008 16:44:02 +0100 | |
changeset 26084 | a7475459c740 |
parent 24688 | a5754ca5c510 |
child 26884 | 67c54c53da28 |
permissions | -rw-r--r-- |
17758 | 1 |
(* Title: Pure/ML-Systems/poplogml.ML |
2 |
ID: $Id$ |
|
3 |
Author: Makarius |
|
4 |
||
5 |
Compatibility file for Poplog/PML (version 15.6/2.1). |
|
6 |
*) |
|
7 |
||
17798 | 8 |
(* Compiler and runtime options *) |
9 |
||
24597 | 10 |
val ml_system_fix_ints = false; |
11 |
||
17798 | 12 |
val _ = Compile.filetype := ".ML"; |
17808 | 13 |
val _ = Memory.hilim := let fun MB n = n div 4 * 1024 * 1024 in MB 120 end; |
17798 | 14 |
val _ = Memory.stacklim := 10 * ! Memory.stacklim; |
15 |
||
16 |
fun pointer_eq (_: 'a, _: 'a) = false; |
|
17 |
||
18 |
||
19 |
(* ML toplevel *) |
|
20 |
||
21 |
fun ml_prompts p1 p2 = (); |
|
22 |
||
23 |
fun make_pp path pprint = (); |
|
24 |
fun install_pp _ = (); |
|
25 |
||
24329 | 26 |
fun get_print_depth () = 10; |
17798 | 27 |
fun print_depth _ = (); |
28 |
||
29 |
fun exception_trace f = f (); |
|
30 |
fun profile (n: int) f x = f x; |
|
31 |
||
32 |
||
33 |
||
17758 | 34 |
(** Basis structures **) |
35 |
||
36 |
structure General = |
|
37 |
struct |
|
38 |
exception Subscript = Array.Subscript; |
|
39 |
exception Size; |
|
40 |
exception Fail of string; |
|
41 |
fun exnMessage (exn: exn) = "exception " ^ makestring exn ^ " raised"; |
|
42 |
datatype order = LESS | EQUAL | GREATER; |
|
43 |
end; |
|
44 |
open General; |
|
45 |
||
46 |
structure Bool = |
|
47 |
struct |
|
48 |
val toString: bool -> string = makestring; |
|
49 |
end; |
|
50 |
||
51 |
structure Option = |
|
52 |
struct |
|
53 |
open Option; |
|
54 |
exception Option; |
|
55 |
||
56 |
fun valOf (SOME x) = x |
|
57 |
| valOf NONE = raise Option; |
|
58 |
||
59 |
fun getOpt (SOME x, _) = x |
|
60 |
| getOpt (NONE, x) = x; |
|
61 |
||
62 |
fun isSome (SOME _) = true |
|
63 |
| isSome NONE = false; |
|
64 |
end; |
|
65 |
open Option; |
|
66 |
||
67 |
structure Option = |
|
68 |
struct |
|
69 |
open Option; |
|
70 |
fun map f (SOME x) = SOME (f x) |
|
71 |
| map _ NONE = NONE; |
|
72 |
end; |
|
73 |
||
74 |
structure Int = |
|
75 |
struct |
|
76 |
open Int; |
|
77 |
type int = int; |
|
78 |
val toString: int -> string = makestring; |
|
79 |
fun fromInt (i: int) = i; |
|
80 |
val fromString = String.stringint; |
|
17798 | 81 |
val op + = op + : int * int -> int; |
82 |
val op - = op - : int * int -> int; |
|
83 |
val op * = op * : int * int -> int; |
|
84 |
val op div = op div : int * int -> int; |
|
85 |
val op mod = op mod : int * int -> int; |
|
86 |
fun pow (x, y) = power x y : int; |
|
87 |
val op < = op < : int * int -> bool; |
|
88 |
val op > = op > : int * int -> bool; |
|
89 |
val op <= = op <= : int * int -> bool; |
|
90 |
val op >= = op >= : int * int -> bool; |
|
91 |
val abs = abs: int -> int; |
|
92 |
val sign = sign: int -> int; |
|
17758 | 93 |
fun max (x, y) : int = if x < y then y else x; |
94 |
fun min (x, y) : int = if x < y then x else y; |
|
95 |
fun compare (x: int, y) = if x = y then EQUAL else if x < y then LESS else GREATER; |
|
96 |
end; |
|
97 |
||
98 |
structure IntInf = Int; |
|
99 |
||
100 |
structure Real = |
|
101 |
struct |
|
102 |
open Real; |
|
103 |
val toString: real -> string = makestring; |
|
104 |
fun max (x, y) : real = if x < y then y else x; |
|
105 |
fun min (x, y) : real = if x < y then x else y; |
|
106 |
val real = real; |
|
107 |
val floor = floor; |
|
108 |
val realFloor = real o floor; |
|
109 |
fun ceil x = ~1 - floor (~ (x + 1.0)); |
|
110 |
fun round x = floor (x + 0.5); (*does not do round-to-nearest*) |
|
111 |
fun trunc x = if x < 0.0 then ceil x else floor x; |
|
112 |
end; |
|
113 |
||
114 |
structure String = |
|
115 |
struct |
|
116 |
open String; |
|
117 |
type char = string |
|
118 |
fun str (c: char) = c: string; |
|
119 |
val translate = mapstring; |
|
120 |
val isPrefix = isprefix; |
|
121 |
val isSuffix = issuffix; |
|
122 |
val size = size; |
|
123 |
fun compare (x: string, y) = if x = y then EQUAL else if x < y then LESS else GREATER; |
|
124 |
fun substring (s, i, n) = String.substring i (i + n) s |
|
125 |
handle String.Substring => raise Subscript; |
|
126 |
end; |
|
127 |
||
128 |
structure List = |
|
129 |
struct |
|
130 |
open List; |
|
17798 | 131 |
|
132 |
exception Empty; |
|
133 |
fun null [] = true | null _ = false; |
|
134 |
fun hd (x :: _) = x | hd _ = raise Empty; |
|
135 |
fun tl (_ :: xs) = xs | tl _ = raise Empty; |
|
17758 | 136 |
val map = map; |
137 |
||
17798 | 138 |
fun foldl f b [] = b |
139 |
| foldl f b (x :: xs) = foldl f (f (x, b)) xs; |
|
140 |
||
141 |
fun foldr f b [] = b |
|
142 |
| foldr f b (x :: xs) = f (x, foldr f b xs); |
|
143 |
||
17758 | 144 |
fun last [] = raise Empty |
145 |
| last [x] = x |
|
146 |
| last (x::xs) = last xs; |
|
147 |
||
148 |
fun nth (xs, n) = |
|
149 |
let fun h [] _ = raise Subscript |
|
150 |
| h (x::xs) n = if n=0 then x else h xs (n-1) |
|
151 |
in if n<0 then raise Subscript else h xs n end; |
|
152 |
||
153 |
fun drop (xs, n) = |
|
154 |
let fun h xs 0 = xs |
|
155 |
| h [] n = raise Subscript |
|
156 |
| h (x::xs) n = h xs (n-1) |
|
157 |
in if n<0 then raise Subscript else h xs n end; |
|
158 |
||
159 |
fun take (xs, n) = |
|
160 |
let fun h xs 0 = [] |
|
161 |
| h [] n = raise Subscript |
|
162 |
| h (x::xs) n = x :: h xs (n-1) |
|
163 |
in if n<0 then raise Subscript else h xs n end; |
|
164 |
||
165 |
fun concat [] = [] |
|
166 |
| concat (l::ls) = l @ concat ls; |
|
167 |
||
168 |
fun mapPartial f [] = [] |
|
169 |
| mapPartial f (x::xs) = |
|
170 |
(case f x of NONE => mapPartial f xs |
|
171 |
| SOME y => y :: mapPartial f xs); |
|
172 |
||
173 |
fun find _ [] = NONE |
|
174 |
| find p (x :: xs) = if p x then SOME x else find p xs; |
|
175 |
||
176 |
||
177 |
(*copy the list preserving elements that satisfy the predicate*) |
|
178 |
fun filter p [] = [] |
|
179 |
| filter p (x :: xs) = if p x then x :: filter p xs else filter p xs; |
|
180 |
||
181 |
(*Partition list into elements that satisfy predicate and those that don't. |
|
182 |
Preserves order of elements in both lists.*) |
|
183 |
fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) = |
|
184 |
let fun part ([], answer) = answer |
|
185 |
| part (x::xs, (ys, ns)) = if p(x) |
|
186 |
then part (xs, (x::ys, ns)) |
|
187 |
else part (xs, (ys, x::ns)) |
|
188 |
in part (rev ys, ([], [])) end; |
|
189 |
||
190 |
end; |
|
17798 | 191 |
exception Empty = List.Empty; |
192 |
val null = List.null; |
|
193 |
val hd = List.hd; |
|
194 |
val tl = List.tl; |
|
195 |
val map = List.map; |
|
196 |
val foldl = List.foldl; |
|
197 |
val foldr = List.foldr; |
|
198 |
val app = List.app; |
|
199 |
val length = List.length; |
|
17758 | 200 |
|
201 |
structure ListPair = |
|
202 |
struct |
|
203 |
fun zip ([], []) = [] |
|
204 |
| zip (x::xs,y::ys) = (x,y) :: zip(xs,ys); |
|
205 |
||
206 |
fun unzip [] = ([],[]) |
|
207 |
| unzip((x,y)::pairs) = |
|
208 |
let val (xs,ys) = unzip pairs |
|
209 |
in (x::xs, y::ys) end; |
|
210 |
||
211 |
fun app f (x::xs, y::ys) = (f (x, y); app f (xs, ys)) |
|
212 |
| app f _ = (); |
|
213 |
||
214 |
fun map f ([], []) = [] |
|
215 |
| map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys); |
|
216 |
||
217 |
fun exists p = |
|
218 |
let fun boolf ([], []) = false |
|
219 |
| boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys) |
|
220 |
in boolf end; |
|
221 |
||
222 |
fun all p = |
|
223 |
let fun boolf ([], []) = true |
|
224 |
| boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys) |
|
225 |
in boolf end; |
|
226 |
end; |
|
227 |
||
228 |
structure TextIO = |
|
229 |
struct |
|
230 |
type instream = instream; |
|
231 |
type outstream = outstream; |
|
232 |
exception Io = Io; |
|
233 |
val stdIn = std_in; |
|
234 |
val stdOut = std_out; |
|
235 |
val stdErr = std_err; |
|
236 |
val openIn = open_in; |
|
237 |
val openAppend = open_append; |
|
238 |
val openOut = open_out; |
|
239 |
val closeIn = close_in; |
|
240 |
val closeOut = close_out; |
|
241 |
val inputN = input; |
|
242 |
val inputAll = fn is => inputN (is, 1000000000); |
|
243 |
val inputLine = input_line; |
|
244 |
val endOfStream = end_of_stream; |
|
245 |
val output = output; |
|
246 |
val flushOut = flush_out; |
|
247 |
end; |
|
248 |
||
249 |
||
250 |
||
251 |
(** Compiler-independent timing functions **) |
|
252 |
||
21295
63552bc99cfb
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18760
diff
changeset
|
253 |
fun start_timing() = "FIXME"; |
63552bc99cfb
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18760
diff
changeset
|
254 |
fun end_timing (s: string) = s; |
63552bc99cfb
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18760
diff
changeset
|
255 |
fun check_timer _ = (0, 0, 0); |
17758 | 256 |
|
257 |
structure Timer = |
|
258 |
struct |
|
259 |
type cpu_timer = int; |
|
260 |
fun startCPUTimer () = 0; |
|
261 |
end; |
|
262 |
||
263 |
structure Time = |
|
264 |
struct |
|
265 |
exception Time; |
|
266 |
type time = int; |
|
267 |
val toString: time -> string = makestring; |
|
268 |
val zeroTime = 0; |
|
269 |
fun now () = 0; |
|
270 |
fun (x: int) + y = x + y; |
|
271 |
fun (x: int) - y = x - y; |
|
272 |
end; |
|
273 |
||
274 |
||
275 |
||
276 |
(** interrupts **) (*Note: may get into race conditions*) |
|
277 |
||
26084
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
24688
diff
changeset
|
278 |
fun interruptible f x = f x; |
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
24688
diff
changeset
|
279 |
fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x; |
17758 | 280 |
|
281 |
||
282 |
||
283 |
(** OS related **) |
|
284 |
||
285 |
val tmp_name = |
|
286 |
let val count = ref 0 in |
|
287 |
fn () => (count := ! count + 1; |
|
288 |
"/tmp/pml" ^ Int.toString (OS.pid ()) ^ "." ^ Int.toString (! count)) |
|
289 |
end; |
|
290 |
||
291 |
local |
|
292 |
||
293 |
fun shell cmdline = OS.execve "/bin/sh" ["sh", "-c", cmdline] (OS.envlist()); |
|
294 |
||
295 |
fun execute_rc cmdline = |
|
296 |
let |
|
297 |
fun wait pid = |
|
298 |
(case OS.wait () of |
|
299 |
NONE => wait pid |
|
300 |
| SOME (pid', rc) => |
|
301 |
if pid = pid' then rc div 256 else raise OS.Error ("wait", "wrong pid", "")); |
|
302 |
in |
|
303 |
(case OS.fork () of |
|
304 |
NONE => shell cmdline |
|
305 |
| SOME pid => wait pid) |
|
306 |
end; |
|
307 |
||
308 |
fun squote s = "'" ^ s ^ "'"; |
|
309 |
fun remove name = (execute_rc ("/bin/rm -- " ^ squote name); ()); |
|
17862 | 310 |
fun is_dir name = execute_rc ("perl -e \"exit (-d " ^ squote name ^ " ? 0 : 1)\"") = 0; |
17758 | 311 |
|
312 |
fun execute_result cmdline = |
|
313 |
let |
|
314 |
val tmp = tmp_name (); |
|
315 |
val rc = execute_rc (cmdline ^ " > " ^ tmp); |
|
316 |
val instream = TextIO.openIn tmp; |
|
317 |
val result = TextIO.inputAll instream; |
|
318 |
val _ = TextIO.closeIn instream; |
|
319 |
val _ = remove tmp; |
|
320 |
in (rc, result) end; |
|
321 |
||
322 |
in |
|
323 |
||
324 |
fun exit rc = shell ("exit " ^ Int.toString rc); |
|
325 |
fun quit () = exit 0; |
|
326 |
||
327 |
fun execute cmdline = #2 (execute_result cmdline); |
|
328 |
||
329 |
fun system cmdline = |
|
330 |
let val (rc, result) = execute_result cmdline |
|
331 |
in TextIO.output (TextIO.stdOut, result); TextIO.flushOut TextIO.stdOut; rc end; |
|
332 |
||
17824 | 333 |
val string_of_pid: int -> string = makestring; |
334 |
||
17758 | 335 |
fun getenv var = (case OS.translate var of NONE => "" | SOME s => s); |
336 |
||
337 |
structure OS = |
|
338 |
struct |
|
339 |
structure FileSys = |
|
340 |
struct |
|
341 |
val tmpName = tmp_name; |
|
342 |
val chDir = OS.cd; |
|
343 |
val getDir = OS.pwd; |
|
344 |
val remove = remove; |
|
345 |
val isDir = is_dir; |
|
346 |
val compare = Int.compare; |
|
347 |
||
348 |
fun modTime name = |
|
17862 | 349 |
(case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[9]'") of |
350 |
"" => raise TextIO.Io "OS.FileSys.modTime" |
|
351 |
| s => Int.fromString s); |
|
17758 | 352 |
fun fileId name = |
17862 | 353 |
(case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[1]'") of |
354 |
"" => raise TextIO.Io "OS.FileSys.fileId" |
|
355 |
| s => Int.fromString s); |
|
17758 | 356 |
end; |
357 |
end; |
|
358 |
||
359 |
end; |
|
360 |
||
361 |
||
17798 | 362 |
(* use *) |
363 |
||
364 |
local val pml_use = use in |
|
365 |
||
366 |
fun use name = |
|
367 |
if name = "ROOT.ML" then (*workaround error about looping compilations*) |
|
368 |
let |
|
369 |
val instream = TextIO.openIn name; |
|
370 |
val txt = TextIO.inputAll instream; |
|
371 |
val _ = TextIO.closeIn; |
|
372 |
in use_string txt end |
|
373 |
else pml_use name; |
|
374 |
||
375 |
end; |
|
376 |
||
22144 | 377 |
fun use_text _ _ _ txt = use_string txt; |
21770 | 378 |
fun use_file _ _ name = use name; |