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 |
|
8 (* Compiler and runtime options *) |
|
9 |
|
10 val ml_system_fix_ints = false; |
|
11 |
|
12 val _ = Compile.filetype := ".ML"; |
|
13 val _ = Memory.hilim := let fun MB n = n div 4 * 1024 * 1024 in MB 120 end; |
|
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 |
|
26 fun get_print_depth () = 10; |
|
27 fun print_depth _ = (); |
|
28 |
|
29 fun exception_trace f = f (); |
|
30 fun profile (n: int) f x = f x; |
|
31 |
|
32 |
|
33 |
|
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; |
|
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; |
|
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; |
|
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; |
|
136 val map = map; |
|
137 |
|
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 |
|
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; |
|
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; |
|
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 |
|
253 fun start_timing() = "FIXME"; |
|
254 fun end_timing (s: string) = s; |
|
255 fun check_timer _ = (0, 0, 0); |
|
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 |
|
278 fun interruptible f x = f x; |
|
279 fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x; |
|
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); ()); |
|
310 fun is_dir name = execute_rc ("perl -e \"exit (-d " ^ squote name ^ " ? 0 : 1)\"") = 0; |
|
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 |
|
333 val string_of_pid: int -> string = makestring; |
|
334 |
|
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 = |
|
349 (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[9]'") of |
|
350 "" => raise TextIO.Io "OS.FileSys.modTime" |
|
351 | s => Int.fromString s); |
|
352 fun fileId name = |
|
353 (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[1]'") of |
|
354 "" => raise TextIO.Io "OS.FileSys.fileId" |
|
355 | s => Int.fromString s); |
|
356 end; |
|
357 end; |
|
358 |
|
359 end; |
|
360 |
|
361 |
|
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 |
|
377 fun use_text _ _ _ _ txt = use_string txt; |
|
378 fun use_file _ _ _ name = use name; |
|