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