wenzelm@26215
|
1 |
(* Title: Pure/ML-Systems/polyml_common.ML
|
wenzelm@26215
|
2 |
ID: $Id$
|
wenzelm@26215
|
3 |
|
wenzelm@26215
|
4 |
Compatibility file for Poly/ML -- common part for 4.x and 5.x.
|
wenzelm@26215
|
5 |
*)
|
wenzelm@26215
|
6 |
|
wenzelm@26215
|
7 |
use "ML-Systems/exn.ML";
|
wenzelm@26215
|
8 |
if List.exists (fn s => s = "Universal") (PolyML.Compiler.structureNames ()) then ()
|
wenzelm@26215
|
9 |
else use "ML-Systems/universal.ML";
|
wenzelm@26215
|
10 |
use "ML-Systems/multithreading.ML";
|
wenzelm@26215
|
11 |
use "ML-Systems/time_limit.ML";
|
wenzelm@26220
|
12 |
use "ML-Systems/system_shell.ML";
|
wenzelm@26220
|
13 |
|
wenzelm@26215
|
14 |
|
wenzelm@26215
|
15 |
|
wenzelm@26215
|
16 |
(** ML system and platform related **)
|
wenzelm@26215
|
17 |
|
wenzelm@26215
|
18 |
(* Compiler options *)
|
wenzelm@26215
|
19 |
|
wenzelm@26215
|
20 |
val ml_system_fix_ints = false;
|
wenzelm@26215
|
21 |
|
wenzelm@26215
|
22 |
PolyML.Compiler.printInAlphabeticalOrder := false;
|
wenzelm@26215
|
23 |
PolyML.Compiler.maxInlineSize := 80;
|
wenzelm@26215
|
24 |
|
wenzelm@26215
|
25 |
|
wenzelm@26215
|
26 |
(* String compatibility *)
|
wenzelm@26215
|
27 |
|
wenzelm@26215
|
28 |
(*low-level pointer equality*)
|
wenzelm@26215
|
29 |
val pointer_eq = Address.wordEq;
|
wenzelm@26215
|
30 |
|
wenzelm@26215
|
31 |
|
wenzelm@26215
|
32 |
(* old Poly/ML emulation *)
|
wenzelm@26215
|
33 |
|
wenzelm@26215
|
34 |
local
|
wenzelm@26215
|
35 |
val orig_exit = exit;
|
wenzelm@26215
|
36 |
in
|
wenzelm@26215
|
37 |
open PolyML;
|
wenzelm@26215
|
38 |
val exit = orig_exit;
|
wenzelm@26215
|
39 |
fun quit () = exit 0;
|
wenzelm@26215
|
40 |
end;
|
wenzelm@26215
|
41 |
|
wenzelm@26215
|
42 |
|
wenzelm@26215
|
43 |
(* restore old-style character / string functions *)
|
wenzelm@26215
|
44 |
|
wenzelm@26215
|
45 |
val ord = SML90.ord;
|
wenzelm@26215
|
46 |
val chr = SML90.chr;
|
wenzelm@26215
|
47 |
val explode = SML90.explode;
|
wenzelm@26215
|
48 |
val implode = SML90.implode;
|
wenzelm@26215
|
49 |
|
wenzelm@26215
|
50 |
|
wenzelm@26215
|
51 |
(* compiler-independent timing functions *)
|
wenzelm@26215
|
52 |
|
wenzelm@26215
|
53 |
fun start_timing () =
|
wenzelm@26215
|
54 |
let val CPUtimer = Timer.startCPUTimer();
|
wenzelm@26215
|
55 |
val time = Timer.checkCPUTimer(CPUtimer)
|
wenzelm@26215
|
56 |
in (CPUtimer,time) end;
|
wenzelm@26215
|
57 |
|
wenzelm@26215
|
58 |
fun end_timing (CPUtimer, {sys,usr}) =
|
wenzelm@26215
|
59 |
let open Time (*...for Time.toString, Time.+ and Time.- *)
|
wenzelm@26215
|
60 |
val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
|
wenzelm@26215
|
61 |
in "User " ^ toString (usr2-usr) ^
|
wenzelm@26215
|
62 |
" All "^ toString (sys2-sys + usr2-usr) ^
|
wenzelm@26215
|
63 |
" secs"
|
wenzelm@26215
|
64 |
handle Time => ""
|
wenzelm@26215
|
65 |
end;
|
wenzelm@26215
|
66 |
|
wenzelm@26215
|
67 |
fun check_timer timer =
|
wenzelm@26215
|
68 |
let
|
wenzelm@26215
|
69 |
val {sys, usr} = Timer.checkCPUTimer timer;
|
wenzelm@26215
|
70 |
val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *)
|
wenzelm@26215
|
71 |
in (sys, usr, gc) end;
|
wenzelm@26215
|
72 |
|
wenzelm@26215
|
73 |
|
wenzelm@26215
|
74 |
(* prompts *)
|
wenzelm@26215
|
75 |
|
wenzelm@26215
|
76 |
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
|
wenzelm@26215
|
77 |
|
wenzelm@26215
|
78 |
|
wenzelm@26215
|
79 |
(* toplevel pretty printing (see also Pure/pure_setup.ML) *)
|
wenzelm@26215
|
80 |
|
wenzelm@26215
|
81 |
fun make_pp _ pprint (str, blk, brk, en) _ _ obj =
|
wenzelm@26215
|
82 |
pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
|
wenzelm@26215
|
83 |
fn () => brk (99999, 0), en);
|
wenzelm@26215
|
84 |
|
wenzelm@26215
|
85 |
(*print depth*)
|
wenzelm@26215
|
86 |
local
|
wenzelm@26215
|
87 |
val depth = ref 10;
|
wenzelm@26215
|
88 |
in
|
wenzelm@26215
|
89 |
fun get_print_depth () = ! depth;
|
wenzelm@26215
|
90 |
fun print_depth n = (depth := n; PolyML.print_depth n);
|
wenzelm@26215
|
91 |
end;
|
wenzelm@26215
|
92 |
|
wenzelm@26215
|
93 |
|
wenzelm@26215
|
94 |
(* ML command execution -- 'eval' *)
|
wenzelm@26215
|
95 |
|
wenzelm@26215
|
96 |
fun use_text (tune: string -> string) name (print, err) verbose txt =
|
wenzelm@26215
|
97 |
let
|
wenzelm@26215
|
98 |
val in_buffer = ref (explode (tune txt));
|
wenzelm@26215
|
99 |
val out_buffer = ref ([]: string list);
|
wenzelm@26215
|
100 |
fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
|
wenzelm@26215
|
101 |
|
wenzelm@26215
|
102 |
fun get () =
|
wenzelm@26215
|
103 |
(case ! in_buffer of
|
wenzelm@26215
|
104 |
[] => ""
|
wenzelm@26215
|
105 |
| c :: cs => (in_buffer := cs; c));
|
wenzelm@26215
|
106 |
fun put s = out_buffer := s :: ! out_buffer;
|
wenzelm@26215
|
107 |
|
wenzelm@26215
|
108 |
fun exec () =
|
wenzelm@26215
|
109 |
(case ! in_buffer of
|
wenzelm@26215
|
110 |
[] => ()
|
wenzelm@26215
|
111 |
| _ => (PolyML.compiler (get, put) (); exec ()));
|
wenzelm@26215
|
112 |
in
|
wenzelm@26215
|
113 |
exec () handle exn =>
|
wenzelm@26215
|
114 |
(err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
|
wenzelm@26215
|
115 |
if verbose then print (output ()) else ()
|
wenzelm@26215
|
116 |
end;
|
wenzelm@26215
|
117 |
|
wenzelm@26215
|
118 |
fun use_file tune output verbose name =
|
wenzelm@26215
|
119 |
let
|
wenzelm@26215
|
120 |
val instream = TextIO.openIn name;
|
wenzelm@26215
|
121 |
val txt = TextIO.inputAll instream before TextIO.closeIn instream;
|
wenzelm@26215
|
122 |
in use_text tune name output verbose txt end;
|
wenzelm@26215
|
123 |
|
wenzelm@26215
|
124 |
|
wenzelm@26215
|
125 |
(*eval command line arguments*)
|
wenzelm@26215
|
126 |
local
|
wenzelm@26215
|
127 |
fun println s =
|
wenzelm@26215
|
128 |
(TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut);
|
wenzelm@26215
|
129 |
fun eval "-q" = ()
|
wenzelm@26215
|
130 |
| eval txt = use_text (fn x => x) "" (println, println) false txt;
|
wenzelm@26215
|
131 |
in
|
wenzelm@26215
|
132 |
val _ = PolyML.onEntry (fn () =>
|
wenzelm@26215
|
133 |
(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ()));
|
wenzelm@26215
|
134 |
app eval (CommandLine.arguments ())));
|
wenzelm@26215
|
135 |
end;
|
wenzelm@26215
|
136 |
|
wenzelm@26215
|
137 |
|
wenzelm@26215
|
138 |
|
wenzelm@26215
|
139 |
(** interrupts **)
|
wenzelm@26215
|
140 |
|
wenzelm@26215
|
141 |
exception Interrupt = SML90.Interrupt;
|
wenzelm@26215
|
142 |
|
wenzelm@26215
|
143 |
local
|
wenzelm@26215
|
144 |
|
wenzelm@26215
|
145 |
val sig_int = 2;
|
wenzelm@26215
|
146 |
val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
|
wenzelm@26215
|
147 |
|
wenzelm@26215
|
148 |
val _ = Signal.signal (sig_int, default_handler);
|
wenzelm@26215
|
149 |
|
wenzelm@26215
|
150 |
fun change_signal new_handler f x =
|
wenzelm@26215
|
151 |
let
|
wenzelm@26215
|
152 |
(*RACE wrt. other signals!*)
|
wenzelm@26215
|
153 |
val old_handler = Signal.signal (sig_int, new_handler);
|
wenzelm@26215
|
154 |
val result = Exn.capture (f old_handler) x;
|
wenzelm@26215
|
155 |
val _ = Signal.signal (sig_int, old_handler);
|
wenzelm@26215
|
156 |
in Exn.release result end;
|
wenzelm@26215
|
157 |
|
wenzelm@26215
|
158 |
in
|
wenzelm@26215
|
159 |
|
wenzelm@26215
|
160 |
fun interruptible f = change_signal default_handler (fn _ => f);
|
wenzelm@26215
|
161 |
|
wenzelm@26215
|
162 |
fun uninterruptible f =
|
wenzelm@26215
|
163 |
change_signal Signal.SIG_IGN
|
wenzelm@26215
|
164 |
(fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
|
wenzelm@26215
|
165 |
|
wenzelm@26215
|
166 |
end;
|
wenzelm@26215
|
167 |
|
wenzelm@26215
|
168 |
|
wenzelm@26215
|
169 |
|
wenzelm@26215
|
170 |
(** OS related **)
|
wenzelm@26215
|
171 |
|
wenzelm@26215
|
172 |
(* Posix patches *)
|
wenzelm@26215
|
173 |
|
wenzelm@26215
|
174 |
(*This extension of the Poly/ML Signal structure is only necessary
|
wenzelm@26215
|
175 |
because in SML/NJ, types Posix.Signal.signal and Signals.signal differ.*)
|
wenzelm@26215
|
176 |
structure IsaSignal =
|
wenzelm@26215
|
177 |
struct
|
wenzelm@26215
|
178 |
open Signal
|
wenzelm@26215
|
179 |
val usr1 = Posix.Signal.usr1
|
wenzelm@26215
|
180 |
val usr2 = Posix.Signal.usr2
|
wenzelm@26215
|
181 |
val alrm = Posix.Signal.alrm
|
wenzelm@26215
|
182 |
val chld = Posix.Signal.chld
|
wenzelm@26215
|
183 |
val cont = Posix.Signal.cont
|
wenzelm@26215
|
184 |
val int = Posix.Signal.int
|
wenzelm@26215
|
185 |
val quit = Posix.Signal.quit
|
wenzelm@26215
|
186 |
end;
|
wenzelm@26215
|
187 |
|
wenzelm@26215
|
188 |
|
wenzelm@26215
|
189 |
(* current directory *)
|
wenzelm@26215
|
190 |
|
wenzelm@26215
|
191 |
val cd = OS.FileSys.chDir;
|
wenzelm@26215
|
192 |
val pwd = OS.FileSys.getDir;
|
wenzelm@26215
|
193 |
|
wenzelm@26215
|
194 |
|
wenzelm@26215
|
195 |
(*Convert a process ID to a decimal string (chiefly for tracing)*)
|
wenzelm@26215
|
196 |
fun string_of_pid pid =
|
wenzelm@26215
|
197 |
Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));
|
wenzelm@26215
|
198 |
|
wenzelm@26215
|
199 |
|
wenzelm@26215
|
200 |
(* getenv *)
|
wenzelm@26215
|
201 |
|
wenzelm@26215
|
202 |
fun getenv var =
|
wenzelm@26215
|
203 |
(case OS.Process.getEnv var of
|
wenzelm@26215
|
204 |
NONE => ""
|
wenzelm@26215
|
205 |
| SOME txt => txt);
|
wenzelm@26215
|
206 |
|
wenzelm@26215
|
207 |
|
wenzelm@26215
|
208 |
(* profile execution *)
|
wenzelm@26215
|
209 |
|
wenzelm@26215
|
210 |
fun profile 0 f x = f x
|
wenzelm@26215
|
211 |
| profile n f x =
|
wenzelm@26215
|
212 |
let
|
wenzelm@26215
|
213 |
val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
|
wenzelm@26215
|
214 |
val res = Exn.capture f x;
|
wenzelm@26215
|
215 |
val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
|
wenzelm@26215
|
216 |
in Exn.release res end;
|
wenzelm@26215
|
217 |
|