wenzelm@2341
|
1 |
(* Title: Pure/ML-Systems/polyml.ML
|
wenzelm@2341
|
2 |
ID: $Id$
|
wenzelm@2341
|
3 |
|
wenzelm@23139
|
4 |
Compatibility file for Poly/ML (version 4.1.x and 4.2.0).
|
wenzelm@2341
|
5 |
*)
|
wenzelm@2341
|
6 |
|
wenzelm@16374
|
7 |
(** ML system and platform related **)
|
wenzelm@16374
|
8 |
|
wenzelm@17077
|
9 |
(* String compatibility *)
|
wenzelm@17077
|
10 |
|
wenzelm@16516
|
11 |
(*low-level pointer equality*)
|
wenzelm@16516
|
12 |
val pointer_eq = Address.wordEq;
|
wenzelm@16502
|
13 |
|
wenzelm@16502
|
14 |
|
wenzelm@11078
|
15 |
(* old Poly/ML emulation *)
|
wenzelm@11078
|
16 |
|
wenzelm@11078
|
17 |
local
|
wenzelm@11078
|
18 |
val orig_exit = exit;
|
wenzelm@11078
|
19 |
in
|
wenzelm@11078
|
20 |
open PolyML;
|
wenzelm@11078
|
21 |
val exit = orig_exit;
|
wenzelm@11078
|
22 |
fun quit () = exit 0;
|
wenzelm@11078
|
23 |
end;
|
wenzelm@11078
|
24 |
|
wenzelm@11078
|
25 |
|
wenzelm@11078
|
26 |
(* restore old-style character / string functions *)
|
wenzelm@11078
|
27 |
|
wenzelm@11078
|
28 |
val ord = SML90.ord;
|
wenzelm@11078
|
29 |
val chr = SML90.chr;
|
wenzelm@11078
|
30 |
val explode = SML90.explode;
|
wenzelm@11078
|
31 |
val implode = SML90.implode;
|
wenzelm@11078
|
32 |
|
wenzelm@14870
|
33 |
|
skalberg@14519
|
34 |
(* compiler-independent timing functions *)
|
wenzelm@3588
|
35 |
|
wenzelm@21298
|
36 |
fun start_timing () =
|
wenzelm@21298
|
37 |
let val CPUtimer = Timer.startCPUTimer();
|
wenzelm@21298
|
38 |
val time = Timer.checkCPUTimer(CPUtimer)
|
wenzelm@21298
|
39 |
in (CPUtimer,time) end;
|
wenzelm@21298
|
40 |
|
wenzelm@21298
|
41 |
fun end_timing (CPUtimer, {sys,usr}) =
|
wenzelm@21298
|
42 |
let open Time (*...for Time.toString, Time.+ and Time.- *)
|
wenzelm@21298
|
43 |
val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
|
wenzelm@21298
|
44 |
in "User " ^ toString (usr2-usr) ^
|
wenzelm@21298
|
45 |
" All "^ toString (sys2-sys + usr2-usr) ^
|
wenzelm@21298
|
46 |
" secs"
|
wenzelm@21298
|
47 |
handle Time => ""
|
wenzelm@21298
|
48 |
end;
|
wenzelm@21298
|
49 |
|
wenzelm@21298
|
50 |
fun check_timer timer =
|
wenzelm@21298
|
51 |
let
|
wenzelm@21298
|
52 |
val {sys, usr} = Timer.checkCPUTimer timer;
|
wenzelm@21298
|
53 |
val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *)
|
wenzelm@21298
|
54 |
in (sys, usr, gc) end;
|
wenzelm@2341
|
55 |
|
wenzelm@14870
|
56 |
|
webertj@14850
|
57 |
(* bounded time execution *)
|
webertj@14850
|
58 |
|
wenzelm@21281
|
59 |
(*dummy implementation*)
|
webertj@18760
|
60 |
fun interrupt_timeout time f x =
|
webertj@18760
|
61 |
f x;
|
webertj@18760
|
62 |
|
wenzelm@14870
|
63 |
|
wenzelm@4977
|
64 |
(* prompts *)
|
wenzelm@4977
|
65 |
|
wenzelm@4984
|
66 |
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
|
wenzelm@4977
|
67 |
|
wenzelm@4977
|
68 |
|
wenzelm@3588
|
69 |
(* toplevel pretty printing (see also Pure/install_pp.ML) *)
|
wenzelm@2341
|
70 |
|
wenzelm@11078
|
71 |
fun make_pp _ pprint (str, blk, brk, en) _ _ obj =
|
wenzelm@2341
|
72 |
pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
|
wenzelm@2341
|
73 |
fn () => brk (99999, 0), en);
|
wenzelm@2341
|
74 |
|
wenzelm@2341
|
75 |
|
wenzelm@3588
|
76 |
(* ML command execution -- 'eval' *)
|
wenzelm@3588
|
77 |
|
wenzelm@22144
|
78 |
fun use_text name (print, err) verbose txt =
|
wenzelm@3588
|
79 |
let
|
wenzelm@5090
|
80 |
val in_buffer = ref (explode txt);
|
wenzelm@5090
|
81 |
val out_buffer = ref ([]: string list);
|
wenzelm@21715
|
82 |
fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
|
wenzelm@5090
|
83 |
|
wenzelm@5038
|
84 |
fun get () =
|
wenzelm@5090
|
85 |
(case ! in_buffer of
|
wenzelm@5038
|
86 |
[] => ""
|
wenzelm@5090
|
87 |
| c :: cs => (in_buffer := cs; c));
|
wenzelm@5090
|
88 |
fun put s = out_buffer := s :: ! out_buffer;
|
wenzelm@5090
|
89 |
|
wenzelm@5038
|
90 |
fun exec () =
|
wenzelm@5090
|
91 |
(case ! in_buffer of
|
wenzelm@5038
|
92 |
[] => ()
|
wenzelm@5090
|
93 |
| _ => (PolyML.compiler (get, put) (); exec ()));
|
wenzelm@5090
|
94 |
in
|
wenzelm@22144
|
95 |
exec () handle exn =>
|
wenzelm@22144
|
96 |
(err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
|
wenzelm@10914
|
97 |
if verbose then print (output ()) else ()
|
wenzelm@5090
|
98 |
end;
|
wenzelm@3588
|
99 |
|
wenzelm@21770
|
100 |
fun use_file _ _ name = use name;
|
wenzelm@21770
|
101 |
|
wenzelm@3588
|
102 |
|
wenzelm@15832
|
103 |
(*eval command line arguments*)
|
wenzelm@15832
|
104 |
local
|
wenzelm@15832
|
105 |
fun println s =
|
wenzelm@15832
|
106 |
(TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut);
|
wenzelm@21715
|
107 |
fun eval "-q" = ()
|
wenzelm@22144
|
108 |
| eval txt = use_text "" (println, println) false txt;
|
wenzelm@15832
|
109 |
in
|
wenzelm@15832
|
110 |
val _ = PolyML.onEntry (fn () => app eval (CommandLine.arguments ()));
|
wenzelm@15832
|
111 |
end;
|
wenzelm@15832
|
112 |
|
wenzelm@15832
|
113 |
|
wenzelm@5813
|
114 |
|
wenzelm@11078
|
115 |
(** interrupts **)
|
wenzelm@11078
|
116 |
|
wenzelm@11078
|
117 |
exception Interrupt = SML90.Interrupt;
|
wenzelm@11078
|
118 |
|
wenzelm@11078
|
119 |
local
|
wenzelm@11078
|
120 |
|
wenzelm@12989
|
121 |
fun capture f x = ((f x): unit; NONE) handle exn => SOME exn;
|
wenzelm@11078
|
122 |
|
wenzelm@12989
|
123 |
fun release NONE = ()
|
wenzelm@12989
|
124 |
| release (SOME exn) = raise exn;
|
wenzelm@11078
|
125 |
|
wenzelm@11078
|
126 |
val sig_int = 2;
|
wenzelm@11078
|
127 |
|
wenzelm@11078
|
128 |
fun change_signal new_handler f x =
|
wenzelm@11078
|
129 |
let
|
wenzelm@11078
|
130 |
(*RACE wrt. other signals*)
|
wenzelm@11078
|
131 |
val old_handler = Signal.signal (sig_int, new_handler);
|
wenzelm@11078
|
132 |
val result = capture f x;
|
wenzelm@11078
|
133 |
val _ = Signal.signal (sig_int, old_handler);
|
wenzelm@11078
|
134 |
in release result end;
|
wenzelm@11078
|
135 |
|
wenzelm@11078
|
136 |
val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
|
wenzelm@11078
|
137 |
|
wenzelm@11078
|
138 |
in
|
wenzelm@11078
|
139 |
|
wenzelm@11078
|
140 |
val _ = Signal.signal (sig_int, default_handler);
|
wenzelm@11078
|
141 |
|
wenzelm@12989
|
142 |
fun ignore_interrupt f = change_signal Signal.SIG_IGN f;
|
wenzelm@12989
|
143 |
fun raise_interrupt f = change_signal default_handler f;
|
wenzelm@11078
|
144 |
|
wenzelm@11078
|
145 |
end;
|
wenzelm@5813
|
146 |
|
wenzelm@5813
|
147 |
|
wenzelm@5813
|
148 |
|
wenzelm@3588
|
149 |
(** OS related **)
|
wenzelm@2341
|
150 |
|
wenzelm@21281
|
151 |
use "ML-Systems/polyml-posix.ML";
|
wenzelm@16659
|
152 |
|
wenzelm@16659
|
153 |
|
wenzelm@3588
|
154 |
(* system command execution *)
|
wenzelm@3588
|
155 |
|
wenzelm@3588
|
156 |
(*execute Unix command which doesn't take any input from stdin and
|
wenzelm@11078
|
157 |
sends its output to stdout; could be done more easily by Unix.execute,
|
wenzelm@11078
|
158 |
but that function doesn't use the PATH*)
|
wenzelm@3588
|
159 |
fun execute command =
|
wenzelm@3588
|
160 |
let
|
wenzelm@11078
|
161 |
val tmp_name = OS.FileSys.tmpName ();
|
wenzelm@11078
|
162 |
val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
|
wenzelm@11078
|
163 |
val result = TextIO.inputAll is;
|
wenzelm@11078
|
164 |
in
|
wenzelm@11078
|
165 |
TextIO.closeIn is;
|
wenzelm@11078
|
166 |
OS.FileSys.remove tmp_name;
|
wenzelm@11078
|
167 |
result
|
wenzelm@11078
|
168 |
end;
|
wenzelm@7855
|
169 |
|
wenzelm@11078
|
170 |
(*plain version; with return code*)
|
wenzelm@11078
|
171 |
fun system cmd =
|
wenzelm@11078
|
172 |
if OS.Process.isSuccess (OS.Process.system cmd) then 0 else 1;
|
wenzelm@3588
|
173 |
|
wenzelm@3588
|
174 |
|
wenzelm@17824
|
175 |
(*Convert a process ID to a decimal string (chiefly for tracing)*)
|
wenzelm@17824
|
176 |
fun string_of_pid pid =
|
wenzelm@23139
|
177 |
Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));
|
wenzelm@17824
|
178 |
|
wenzelm@17824
|
179 |
|
wenzelm@3588
|
180 |
(* getenv *)
|
wenzelm@2341
|
181 |
|
wenzelm@11078
|
182 |
fun getenv var =
|
wenzelm@11078
|
183 |
(case OS.Process.getEnv var of
|
wenzelm@11078
|
184 |
NONE => ""
|
wenzelm@11078
|
185 |
| SOME txt => txt);
|
paulson@15028
|
186 |
|
paulson@15028
|
187 |
|
wenzelm@16659
|
188 |
(* profile execution *)
|
paulson@15028
|
189 |
|
wenzelm@16659
|
190 |
local
|
paulson@15699
|
191 |
|
wenzelm@16659
|
192 |
fun no_profile () =
|
wenzelm@16659
|
193 |
RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
|
wenzelm@16659
|
194 |
|
wenzelm@16659
|
195 |
in
|
wenzelm@16659
|
196 |
|
wenzelm@16659
|
197 |
fun profile 0 f x = f x
|
wenzelm@16659
|
198 |
| profile n f x =
|
wenzelm@16659
|
199 |
(RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
|
wenzelm@16659
|
200 |
let val y = f x handle exn => (no_profile (); raise exn)
|
wenzelm@16659
|
201 |
in no_profile (); y end);
|
wenzelm@16659
|
202 |
|
wenzelm@16659
|
203 |
end;
|