1 (* Title: Pure/ML-Systems/mosml.ML |
|
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 Author: Makarius |
|
4 |
|
5 Compatibility file for Moscow ML 2.01 |
|
6 |
|
7 NOTE: saving images does not work; may run it interactively as follows: |
|
8 |
|
9 $ cd Isabelle/src/Pure |
|
10 $ isabelle-process RAW_ML_SYSTEM |
|
11 > val ml_system = "mosml"; |
|
12 > use "ML-Systems/mosml.ML"; |
|
13 > use "ROOT.ML"; |
|
14 > Session.finish (); |
|
15 > cd "../FOL"; |
|
16 > use "ROOT.ML"; |
|
17 > Session.finish (); |
|
18 > cd "../ZF"; |
|
19 > use "ROOT.ML"; |
|
20 *) |
|
21 |
|
22 (** ML system related **) |
|
23 |
|
24 val ml_system_fix_ints = false; |
|
25 |
|
26 fun forget_structure _ = (); |
|
27 |
|
28 load "Obj"; |
|
29 load "Word"; |
|
30 load "Bool"; |
|
31 load "Int"; |
|
32 load "Real"; |
|
33 load "ListPair"; |
|
34 load "OS"; |
|
35 load "Process"; |
|
36 load "FileSys"; |
|
37 load "IO"; |
|
38 load "CharVector"; |
|
39 |
|
40 exception Interrupt; |
|
41 fun reraise exn = raise exn; |
|
42 |
|
43 use "ML-Systems/unsynchronized.ML"; |
|
44 use "General/exn.ML"; |
|
45 use "ML-Systems/universal.ML"; |
|
46 use "ML-Systems/thread_dummy.ML"; |
|
47 use "ML-Systems/multithreading.ML"; |
|
48 use "ML-Systems/time_limit.ML"; |
|
49 use "ML-Systems/ml_name_space.ML"; |
|
50 use "ML-Systems/ml_pretty.ML"; |
|
51 use "ML-Systems/use_context.ML"; |
|
52 |
|
53 |
|
54 (*low-level pointer equality*) |
|
55 local val cast : 'a -> int = Obj.magic |
|
56 in fun pointer_eq (x:'a, y:'a) = (cast x = cast y) end; |
|
57 |
|
58 (*proper implementation available?*) |
|
59 structure IntInf = |
|
60 struct |
|
61 fun divMod (x, y) = (x div y, x mod y); |
|
62 |
|
63 local |
|
64 fun log 1 a = a |
|
65 | log n a = log (n div 2) (a + 1); |
|
66 in |
|
67 fun log2 n = if n > 0 then log n 0 else raise Domain; |
|
68 end; |
|
69 |
|
70 open Int; |
|
71 end; |
|
72 |
|
73 structure Substring = |
|
74 struct |
|
75 open Substring; |
|
76 val full = all; |
|
77 end; |
|
78 |
|
79 structure Real = |
|
80 struct |
|
81 open Real; |
|
82 val realFloor = real o floor; |
|
83 end; |
|
84 |
|
85 structure String = |
|
86 struct |
|
87 fun isSuffix s1 s2 = |
|
88 let val n1 = size s1 and n2 = size s2 |
|
89 in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end; |
|
90 open String; |
|
91 end; |
|
92 |
|
93 structure Time = |
|
94 struct |
|
95 open Time; |
|
96 fun toString t = Time.toString t |
|
97 handle Overflow => Real.toString (Time.toReal t); (*workaround Y2004 bug*) |
|
98 end; |
|
99 |
|
100 structure OS = |
|
101 struct |
|
102 open OS |
|
103 structure Process = |
|
104 struct |
|
105 open Process |
|
106 fun sleep _ = raise Fail "OS.Process.sleep undefined" |
|
107 end; |
|
108 structure FileSys = FileSys |
|
109 end; |
|
110 |
|
111 exception Option = Option.Option; |
|
112 |
|
113 |
|
114 (*limit the printing depth*) |
|
115 local |
|
116 val depth = ref 10; |
|
117 in |
|
118 fun get_print_depth () = ! depth; |
|
119 fun print_depth n = |
|
120 (depth := n; |
|
121 Meta.printDepth := n div 2; |
|
122 Meta.printLength := n); |
|
123 end; |
|
124 |
|
125 (*dummy implementation*) |
|
126 fun toplevel_pp _ _ _ = (); |
|
127 |
|
128 (*dummy implementation*) |
|
129 fun ml_prompts p1 p2 = (); |
|
130 |
|
131 (*dummy implementation*) |
|
132 fun profile (n: int) f x = f x; |
|
133 |
|
134 (*dummy implementation*) |
|
135 fun exception_trace f = f (); |
|
136 |
|
137 |
|
138 |
|
139 (** Compiler-independent timing functions **) |
|
140 |
|
141 load "Timer"; |
|
142 |
|
143 fun start_timing () = |
|
144 let |
|
145 val timer = Timer.startCPUTimer (); |
|
146 val time = Timer.checkCPUTimer timer; |
|
147 in (timer, time) end; |
|
148 |
|
149 fun end_timing (timer, {gc, sys, usr}) = |
|
150 let |
|
151 open Time; (*...for Time.toString, Time.+ and Time.- *) |
|
152 val {gc = gc2, sys = sys2, usr = usr2} = Timer.checkCPUTimer timer; |
|
153 val user = usr2 - usr + gc2 - gc; |
|
154 val all = user + sys2 - sys; |
|
155 val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => ""; |
|
156 in {message = message, user = user, all = all} end; |
|
157 |
|
158 |
|
159 (* SML basis library fixes *) |
|
160 |
|
161 structure TextIO = |
|
162 struct |
|
163 fun canInput _ = raise IO.Io {cause = Fail "undefined", function = "canInput", name = ""}; |
|
164 open TextIO; |
|
165 fun inputLine is = |
|
166 let val s = TextIO.inputLine is |
|
167 in if s = "" then NONE else SOME s end; |
|
168 fun getOutstream _ = (); |
|
169 structure StreamIO = |
|
170 struct |
|
171 fun setBufferMode _ = (); |
|
172 end |
|
173 end; |
|
174 |
|
175 structure IO = |
|
176 struct |
|
177 open IO; |
|
178 val BLOCK_BUF = (); |
|
179 end; |
|
180 |
|
181 |
|
182 (* ML command execution *) |
|
183 |
|
184 (*Can one redirect 'use' directly to an instream?*) |
|
185 fun use_text ({tune_source, ...}: use_context) _ _ txt = |
|
186 let |
|
187 val tmp_name = FileSys.tmpName (); |
|
188 val tmp_file = TextIO.openOut tmp_name; |
|
189 in |
|
190 TextIO.output (tmp_file, tune_source txt); |
|
191 TextIO.closeOut tmp_file; |
|
192 use tmp_name; |
|
193 FileSys.remove tmp_name |
|
194 end; |
|
195 |
|
196 fun use_file _ _ name = use name; |
|
197 |
|
198 |
|
199 |
|
200 (** interrupts **) (*Note: may get into race conditions*) |
|
201 |
|
202 (* FIXME proper implementation available? *) |
|
203 |
|
204 fun interruptible f x = f x; |
|
205 fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x; |
|
206 |
|
207 |
|
208 |
|
209 (** OS related **) |
|
210 |
|
211 (*dummy implementation*) |
|
212 structure Posix = |
|
213 struct |
|
214 structure ProcEnv = |
|
215 struct |
|
216 fun getpid () = 0; |
|
217 end; |
|
218 end; |
|
219 |
|
220 local |
|
221 |
|
222 fun read_file name = |
|
223 let val is = TextIO.openIn name |
|
224 in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end; |
|
225 |
|
226 fun write_file name txt = |
|
227 let val os = TextIO.openOut name |
|
228 in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end; |
|
229 |
|
230 in |
|
231 |
|
232 fun bash_output script = |
|
233 let |
|
234 val script_name = OS.FileSys.tmpName (); |
|
235 val _ = write_file script_name script; |
|
236 |
|
237 val output_name = OS.FileSys.tmpName (); |
|
238 |
|
239 val status = |
|
240 OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^ |
|
241 script_name ^ " /dev/null " ^ output_name); |
|
242 val rc = if status = OS.Process.success then 0 else 1; |
|
243 |
|
244 val output = read_file output_name handle IO.Io _ => ""; |
|
245 val _ = OS.FileSys.remove script_name handle OS.SysErr _ => (); |
|
246 val _ = OS.FileSys.remove output_name handle OS.SysErr _ => (); |
|
247 in (output, rc) end; |
|
248 |
|
249 end; |
|
250 |
|
251 val cd = OS.FileSys.chDir; |
|
252 val pwd = OS.FileSys.getDir; |
|
253 |
|
254 val process_id = Int.toString o Posix.ProcEnv.getpid; |
|
255 |
|
256 fun getenv var = |
|
257 (case Process.getEnv var of |
|
258 NONE => "" |
|
259 | SOME txt => txt); |
|