author  wenzelm 
Thu, 06 Mar 2008 20:17:50 +0100  
changeset 26220  d34b68c21f9a 
parent 26084  a7475459c740 
child 26385  ae7564661e76 
permissions  rwrr 
4403  1 
(* Title: Pure/MLSystems/smlnj.ML 
2 
ID: $Id$ 

3 

5708  4 
Compatibility file for Standard ML of New Jersey 110 or later. 
4403  5 
*) 
6 

24599
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

7 
use "MLSystems/proper_int.ML"; 
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

8 
use "MLSystems/overloading_smlnj.ML"; 
23965
f93e509659c1
MLSystems/exn.ML, MLSystems/multithreading_dummy.ML;
wenzelm
parents:
23921
diff
changeset

9 
use "MLSystems/exn.ML"; 
25732  10 
use "MLSystems/universal.ML"; 
24688
a5754ca5c510
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
24599
diff
changeset

11 
use "MLSystems/multithreading.ML"; 
26220  12 
use "MLSystems/system_shell.ML"; 
23921
947152add153
added compatibility file for ML systems without multithreading;
wenzelm
parents:
23826
diff
changeset

13 

16542  14 

15 
(*lowlevel pointer equality*) 

16502  16 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

17 
CM.autoload "$smlnj/init/init.cmi"; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

18 
val pointer_eq = InlineT.ptreql; 
16528  19 

16502  20 

4403  21 
(* restore oldstyle character / string functions *) 
22 

24145  23 
val ord = mk_int o SML90.ord; 
24 
val chr = SML90.chr o dest_int; 

10725  25 
val explode = SML90.explode; 
26 
val implode = SML90.implode; 

4403  27 

28 

29 
(* New Jersey ML parameters *) 

30 

31 
val _ = 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

32 
(Control.Print.printLength := 1000; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

33 
Control.Print.printDepth := 350; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

34 
Control.Print.stringDepth := 250; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

35 
Control.Print.signatures := 2; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

36 
Control.MC.matchRedundantError := false); 
4403  37 

38 

39 
(* Poly/ML emulation *) 

40 

24599
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

41 
val exit = exit o dest_int; 
4403  42 
fun quit () = exit 0; 
43 

44 
(*limit the printing depth  divided by 2 for comparibility with Poly/ML*) 

24329  45 
local 
24599
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

46 
val depth = ref (10: int); 
24329  47 
in 
48 
fun get_print_depth () = ! depth; 

49 
fun print_depth n = 

50 
(depth := n; 

51 
Control.Print.printDepth := dest_int n div 2; 

52 
Control.Print.printLength := dest_int n); 

53 
end; 

4403  54 

5816  55 
(* compilerindependent timing functions *) 
4403  56 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

57 
fun start_timing () = 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

58 
let val CPUtimer = Timer.startCPUTimer(); 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

59 
val time = Timer.checkCPUTimer(CPUtimer) 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

60 
in (CPUtimer,time) end; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

61 

6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

62 
fun end_timing (CPUtimer, {sys,usr}) = 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

63 
let open Time (*...for Time.toString, Time.+ and Time. *) 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

64 
val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer) 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

65 
in "User " ^ toString (usr2usr) ^ 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

66 
" All "^ toString (sys2sys + usr2usr) ^ 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

67 
" secs" 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

68 
handle Time => "" 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

69 
end; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

70 

6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

71 
fun check_timer timer = 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

72 
let 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

73 
val {sys, usr} = Timer.checkCPUTimer timer; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

74 
val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *) 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

75 
in (sys, usr, gc) end; 
4403  76 

77 

16660  78 
(*prompts*) 
4977  79 
fun ml_prompts p1 p2 = 
21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

80 
(Control.primaryPrompt := p1; Control.secondaryPrompt := p2); 
4977  81 

17511  82 
(*dummy implementation*) 
16681  83 
fun profile (n: int) f x = f x; 
84 

17511  85 
(*dummy implementation*) 
16681  86 
fun exception_trace f = f (); 
4977  87 

18384  88 
(*dummy implementation*) 
89 
fun print x = x; 

16681  90 

23770  91 
(*dummy implementation*) 
92 
fun makestring x = "dummy string for SML New Jersey"; 

93 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

94 

24290  95 
(* toplevel pretty printing (see also Pure/pure_setup.ML) *) 
4403  96 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

97 
fun make_pp path pprint = 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

98 
let 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

99 
open PrettyPrint; 
4403  100 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

101 
fun pp pps obj = 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

102 
pprint obj 
24145  103 
(string pps, openHOVBox pps o Rel o dest_int, 
104 
fn wd => break pps {nsp=dest_int wd, offset=0}, fn () => newline pps, 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

105 
fn () => closeBox pps); 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

106 
in (path, pp) end; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

107 

6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

108 
fun install_pp (path, pp) = CompilerPPTable.install_pp path pp; 
4403  109 

110 

111 
(* ML command execution *) 

112 

24599
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

113 
fun use_text (tune: string > string) name (print, err) verbose txt = 
5090  114 
let 
21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

115 
val ref out_orig = Control.Print.out; 
5090  116 

117 
val out_buffer = ref ([]: string list); 

118 
val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())}; 

10914  119 
fun output () = 
7890  120 
let val str = implode (rev (! out_buffer)) 
10914  121 
in String.substring (str, 0, Int.max (0, size str  1)) end; 
5090  122 
in 
21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

123 
Control.Print.out := out; 
24599
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

124 
Backend.Interact.useStream (TextIO.openString (tune txt)) handle exn => 
22144  125 
(Control.Print.out := out_orig; 
126 
err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn); 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

127 
Control.Print.out := out_orig; 
10914  128 
if verbose then print (output ()) else () 
5090  129 
end; 
4403  130 

24599
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

131 
fun use_file tune output verbose name = 
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

132 
let 
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

133 
val instream = TextIO.openIn name; 
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

134 
val txt = TextIO.inputAll instream before TextIO.closeIn instream; 
7b0ecf9a9055
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24329
diff
changeset

135 
in use_text tune name output verbose txt end; 
21770  136 

137 

4403  138 

5816  139 
(** interrupts **) 
140 

12990  141 
exception Interrupt; 
142 

26084
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

143 
local 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

144 

a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

145 
fun change_signal new_handler f x = 
5816  146 
let 
26084
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

147 
val old_handler = Signals.setHandler (Signals.sigINT, new_handler); 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

148 
val result = Exn.capture (f old_handler) x; 
12990  149 
val _ = Signals.setHandler (Signals.sigINT, old_handler); 
23965
f93e509659c1
MLSystems/exn.ML, MLSystems/multithreading_dummy.ML;
wenzelm
parents:
23921
diff
changeset

150 
in Exn.release result end; 
5816  151 

26084
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

152 
in 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

153 

a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

154 
fun interruptible (f: 'a > 'b) x = 
12990  155 
let 
26084
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

156 
val result = ref (Exn.Exn Interrupt: 'b Exn.result); 
12990  157 
val old_handler = Signals.inqHandler Signals.sigINT; 
5816  158 
in 
12990  159 
SMLofNJ.Cont.callcc (fn cont => 
26084
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

160 
(Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => cont)); 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

161 
result := Exn.capture f x)); 
12990  162 
Signals.setHandler (Signals.sigINT, old_handler); 
26084
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

163 
Exn.release (! result) 
12990  164 
end; 
5816  165 

26084
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

166 
fun uninterruptible f = 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

167 
change_signal Signals.IGNORE 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

168 
(fn old_handler => f (fn g => change_signal old_handler (fn _ => g))); 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

169 

a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

170 
end; 
a7475459c740
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents:
25732
diff
changeset

171 

21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

172 

6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

173 
(* basis library fixes *) 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

174 

6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

175 
structure TextIO = 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

176 
struct 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

177 
open TextIO; 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22144
diff
changeset

178 
fun inputLine is = TextIO.inputLine is 
21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

179 
handle IO.Io _ => raise Interrupt; 
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

180 
end; 
17511  181 

18790
418131f631fc
interrupt_timeout now raises Interrupt instead of SML90.Interrupt
webertj
parents:
18760
diff
changeset

182 

16542  183 
(** Signal handling: emulation of the Poly/ML Signal structure. Note that types 
15702
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

184 
Posix.Signal.signal and Signals.signal differ **) 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

185 

2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

186 
structure IsaSignal = 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

187 
struct 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

188 

2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

189 
datatype sig_handle = SIG_DFL  SIG_IGN  SIG_HANDLE of Signals.signal > unit; 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

190 

16542  191 
(*From the SML/NJ documentation: "HANDLER(f) installs a handler for a 
192 
signal. When signal is delivered to the process, the execution state 

193 
of the current thread will be bundled up as a continuation k, then 

194 
f(signal,n,k) will be called. The number n is the number of times 

195 
signal has been signalled since the last time f was invoked for it."*) 

15702
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

196 

2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

197 
fun toAction SIG_DFL = Signals.DEFAULT 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

198 
 toAction SIG_IGN = Signals.IGNORE 
16542  199 
 toAction (SIG_HANDLE iu) = 
15702
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

200 
Signals.HANDLER (fn (signo,_,cont) => (iu signo; cont)); 
16542  201 

15702
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

202 
(*The types are correct, but I'm not sure about the semantics!*) 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

203 
fun fromAction Signals.DEFAULT = SIG_DFL 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

204 
 fromAction Signals.IGNORE = SIG_IGN 
16542  205 
 fromAction (Signals.HANDLER f) = 
15702
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

206 
SIG_HANDLE (fn signo => SMLofNJ.Cont.callcc (fn k => (f (signo,0,k); ()))); 
16542  207 

15702
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

208 
(*Poly/ML version has type int * sig_handle > sig_handle*) 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

209 
fun signal (signo, sh) = fromAction (Signals.setHandler (signo, toAction sh)); 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

210 

2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

211 
val usr1 = UnixSignals.sigUSR1 
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

212 
val usr2 = UnixSignals.sigUSR2 
17763  213 
val alrm = UnixSignals.sigALRM 
214 
val chld = UnixSignals.sigCHLD 

215 
val cont = UnixSignals.sigCONT 

216 
val int = UnixSignals.sigINT 

217 
val quit = UnixSignals.sigQUIT 

218 
val term = UnixSignals.sigTERM 

15702
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

219 

2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
14981
diff
changeset

220 
end; 
5816  221 

222 

4403  223 
(** OS related **) 
224 

23826
463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents:
23770
diff
changeset

225 
(* current directory *) 
463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents:
23770
diff
changeset

226 

463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents:
23770
diff
changeset

227 
val cd = OS.FileSys.chDir; 
463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents:
23770
diff
changeset

228 
val pwd = OS.FileSys.getDir; 
463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents:
23770
diff
changeset

229 

463903573934
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents:
23770
diff
changeset

230 

4403  231 
(* system command execution *) 
232 

26220  233 
val system_out = (fn (output, rc) => (output, mk_int rc)) o system_out; 
7855  234 

4403  235 

17824  236 
(*Convert a process ID to a decimal string (chiefly for tracing)*) 
21298
6d2306b2376d
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
18790
diff
changeset

237 
fun string_of_pid pid = 
26220  238 
Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid)); 
17824  239 

240 

4403  241 
(* getenv *) 
242 

243 
fun getenv var = 

244 
(case OS.Process.getEnv var of 

245 
NONE => "" 

246 
 SOME txt => txt); 