1.1 --- a/src/Pure/ML-Systems/mosml.ML Sat Feb 06 22:06:18 2010 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,259 +0,0 @@
1.4 -(* Title: Pure/ML-Systems/mosml.ML
1.5 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1.6 - Author: Makarius
1.7 -
1.8 -Compatibility file for Moscow ML 2.01
1.9 -
1.10 -NOTE: saving images does not work; may run it interactively as follows:
1.11 -
1.12 -$ cd Isabelle/src/Pure
1.13 -$ isabelle-process RAW_ML_SYSTEM
1.14 -> val ml_system = "mosml";
1.15 -> use "ML-Systems/mosml.ML";
1.16 -> use "ROOT.ML";
1.17 -> Session.finish ();
1.18 -> cd "../FOL";
1.19 -> use "ROOT.ML";
1.20 -> Session.finish ();
1.21 -> cd "../ZF";
1.22 -> use "ROOT.ML";
1.23 -*)
1.24 -
1.25 -(** ML system related **)
1.26 -
1.27 -val ml_system_fix_ints = false;
1.28 -
1.29 -fun forget_structure _ = ();
1.30 -
1.31 -load "Obj";
1.32 -load "Word";
1.33 -load "Bool";
1.34 -load "Int";
1.35 -load "Real";
1.36 -load "ListPair";
1.37 -load "OS";
1.38 -load "Process";
1.39 -load "FileSys";
1.40 -load "IO";
1.41 -load "CharVector";
1.42 -
1.43 -exception Interrupt;
1.44 -fun reraise exn = raise exn;
1.45 -
1.46 -use "ML-Systems/unsynchronized.ML";
1.47 -use "General/exn.ML";
1.48 -use "ML-Systems/universal.ML";
1.49 -use "ML-Systems/thread_dummy.ML";
1.50 -use "ML-Systems/multithreading.ML";
1.51 -use "ML-Systems/time_limit.ML";
1.52 -use "ML-Systems/ml_name_space.ML";
1.53 -use "ML-Systems/ml_pretty.ML";
1.54 -use "ML-Systems/use_context.ML";
1.55 -
1.56 -
1.57 -(*low-level pointer equality*)
1.58 -local val cast : 'a -> int = Obj.magic
1.59 -in fun pointer_eq (x:'a, y:'a) = (cast x = cast y) end;
1.60 -
1.61 -(*proper implementation available?*)
1.62 -structure IntInf =
1.63 -struct
1.64 - fun divMod (x, y) = (x div y, x mod y);
1.65 -
1.66 - local
1.67 - fun log 1 a = a
1.68 - | log n a = log (n div 2) (a + 1);
1.69 - in
1.70 - fun log2 n = if n > 0 then log n 0 else raise Domain;
1.71 - end;
1.72 -
1.73 - open Int;
1.74 -end;
1.75 -
1.76 -structure Substring =
1.77 -struct
1.78 - open Substring;
1.79 - val full = all;
1.80 -end;
1.81 -
1.82 -structure Real =
1.83 -struct
1.84 - open Real;
1.85 - val realFloor = real o floor;
1.86 -end;
1.87 -
1.88 -structure String =
1.89 -struct
1.90 - fun isSuffix s1 s2 =
1.91 - let val n1 = size s1 and n2 = size s2
1.92 - in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
1.93 - open String;
1.94 -end;
1.95 -
1.96 -structure Time =
1.97 -struct
1.98 - open Time;
1.99 - fun toString t = Time.toString t
1.100 - handle Overflow => Real.toString (Time.toReal t); (*workaround Y2004 bug*)
1.101 -end;
1.102 -
1.103 -structure OS =
1.104 -struct
1.105 - open OS
1.106 - structure Process =
1.107 - struct
1.108 - open Process
1.109 - fun sleep _ = raise Fail "OS.Process.sleep undefined"
1.110 - end;
1.111 - structure FileSys = FileSys
1.112 -end;
1.113 -
1.114 -exception Option = Option.Option;
1.115 -
1.116 -
1.117 -(*limit the printing depth*)
1.118 -local
1.119 - val depth = ref 10;
1.120 -in
1.121 - fun get_print_depth () = ! depth;
1.122 - fun print_depth n =
1.123 - (depth := n;
1.124 - Meta.printDepth := n div 2;
1.125 - Meta.printLength := n);
1.126 -end;
1.127 -
1.128 -(*dummy implementation*)
1.129 -fun toplevel_pp _ _ _ = ();
1.130 -
1.131 -(*dummy implementation*)
1.132 -fun ml_prompts p1 p2 = ();
1.133 -
1.134 -(*dummy implementation*)
1.135 -fun profile (n: int) f x = f x;
1.136 -
1.137 -(*dummy implementation*)
1.138 -fun exception_trace f = f ();
1.139 -
1.140 -
1.141 -
1.142 -(** Compiler-independent timing functions **)
1.143 -
1.144 -load "Timer";
1.145 -
1.146 -fun start_timing () =
1.147 - let
1.148 - val timer = Timer.startCPUTimer ();
1.149 - val time = Timer.checkCPUTimer timer;
1.150 - in (timer, time) end;
1.151 -
1.152 -fun end_timing (timer, {gc, sys, usr}) =
1.153 - let
1.154 - open Time; (*...for Time.toString, Time.+ and Time.- *)
1.155 - val {gc = gc2, sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
1.156 - val user = usr2 - usr + gc2 - gc;
1.157 - val all = user + sys2 - sys;
1.158 - val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => "";
1.159 - in {message = message, user = user, all = all} end;
1.160 -
1.161 -
1.162 -(* SML basis library fixes *)
1.163 -
1.164 -structure TextIO =
1.165 -struct
1.166 - fun canInput _ = raise IO.Io {cause = Fail "undefined", function = "canInput", name = ""};
1.167 - open TextIO;
1.168 - fun inputLine is =
1.169 - let val s = TextIO.inputLine is
1.170 - in if s = "" then NONE else SOME s end;
1.171 - fun getOutstream _ = ();
1.172 - structure StreamIO =
1.173 - struct
1.174 - fun setBufferMode _ = ();
1.175 - end
1.176 -end;
1.177 -
1.178 -structure IO =
1.179 -struct
1.180 - open IO;
1.181 - val BLOCK_BUF = ();
1.182 -end;
1.183 -
1.184 -
1.185 -(* ML command execution *)
1.186 -
1.187 -(*Can one redirect 'use' directly to an instream?*)
1.188 -fun use_text ({tune_source, ...}: use_context) _ _ txt =
1.189 - let
1.190 - val tmp_name = FileSys.tmpName ();
1.191 - val tmp_file = TextIO.openOut tmp_name;
1.192 - in
1.193 - TextIO.output (tmp_file, tune_source txt);
1.194 - TextIO.closeOut tmp_file;
1.195 - use tmp_name;
1.196 - FileSys.remove tmp_name
1.197 - end;
1.198 -
1.199 -fun use_file _ _ name = use name;
1.200 -
1.201 -
1.202 -
1.203 -(** interrupts **) (*Note: may get into race conditions*)
1.204 -
1.205 -(* FIXME proper implementation available? *)
1.206 -
1.207 -fun interruptible f x = f x;
1.208 -fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
1.209 -
1.210 -
1.211 -
1.212 -(** OS related **)
1.213 -
1.214 -(*dummy implementation*)
1.215 -structure Posix =
1.216 -struct
1.217 - structure ProcEnv =
1.218 - struct
1.219 - fun getpid () = 0;
1.220 - end;
1.221 -end;
1.222 -
1.223 -local
1.224 -
1.225 -fun read_file name =
1.226 - let val is = TextIO.openIn name
1.227 - in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
1.228 -
1.229 -fun write_file name txt =
1.230 - let val os = TextIO.openOut name
1.231 - in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
1.232 -
1.233 -in
1.234 -
1.235 -fun bash_output script =
1.236 - let
1.237 - val script_name = OS.FileSys.tmpName ();
1.238 - val _ = write_file script_name script;
1.239 -
1.240 - val output_name = OS.FileSys.tmpName ();
1.241 -
1.242 - val status =
1.243 - OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
1.244 - script_name ^ " /dev/null " ^ output_name);
1.245 - val rc = if status = OS.Process.success then 0 else 1;
1.246 -
1.247 - val output = read_file output_name handle IO.Io _ => "";
1.248 - val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
1.249 - val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
1.250 - in (output, rc) end;
1.251 -
1.252 -end;
1.253 -
1.254 -val cd = OS.FileSys.chDir;
1.255 -val pwd = OS.FileSys.getDir;
1.256 -
1.257 -val process_id = Int.toString o Posix.ProcEnv.getpid;
1.258 -
1.259 -fun getenv var =
1.260 - (case Process.getEnv var of
1.261 - NONE => ""
1.262 - | SOME txt => txt);