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