1.1 --- a/src/Pure/ML-Systems/poplogml.ML Sat Jun 14 17:26:09 2008 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,378 +0,0 @@
1.4 -(* Title: Pure/ML-Systems/poplogml.ML
1.5 - ID: $Id$
1.6 - Author: Makarius
1.7 -
1.8 -Compatibility file for Poplog/PML (version 15.6/2.1).
1.9 -*)
1.10 -
1.11 -(* Compiler and runtime options *)
1.12 -
1.13 -val ml_system_fix_ints = false;
1.14 -
1.15 -val _ = Compile.filetype := ".ML";
1.16 -val _ = Memory.hilim := let fun MB n = n div 4 * 1024 * 1024 in MB 120 end;
1.17 -val _ = Memory.stacklim := 10 * ! Memory.stacklim;
1.18 -
1.19 -fun pointer_eq (_: 'a, _: 'a) = false;
1.20 -
1.21 -
1.22 -(* ML toplevel *)
1.23 -
1.24 -fun ml_prompts p1 p2 = ();
1.25 -
1.26 -fun make_pp path pprint = ();
1.27 -fun install_pp _ = ();
1.28 -
1.29 -fun get_print_depth () = 10;
1.30 -fun print_depth _ = ();
1.31 -
1.32 -fun exception_trace f = f ();
1.33 -fun profile (n: int) f x = f x;
1.34 -
1.35 -
1.36 -
1.37 -(** Basis structures **)
1.38 -
1.39 -structure General =
1.40 -struct
1.41 - exception Subscript = Array.Subscript;
1.42 - exception Size;
1.43 - exception Fail of string;
1.44 - fun exnMessage (exn: exn) = "exception " ^ makestring exn ^ " raised";
1.45 - datatype order = LESS | EQUAL | GREATER;
1.46 -end;
1.47 -open General;
1.48 -
1.49 -structure Bool =
1.50 -struct
1.51 - val toString: bool -> string = makestring;
1.52 -end;
1.53 -
1.54 -structure Option =
1.55 -struct
1.56 - open Option;
1.57 - exception Option;
1.58 -
1.59 - fun valOf (SOME x) = x
1.60 - | valOf NONE = raise Option;
1.61 -
1.62 - fun getOpt (SOME x, _) = x
1.63 - | getOpt (NONE, x) = x;
1.64 -
1.65 - fun isSome (SOME _) = true
1.66 - | isSome NONE = false;
1.67 -end;
1.68 -open Option;
1.69 -
1.70 -structure Option =
1.71 -struct
1.72 - open Option;
1.73 - fun map f (SOME x) = SOME (f x)
1.74 - | map _ NONE = NONE;
1.75 -end;
1.76 -
1.77 -structure Int =
1.78 -struct
1.79 - open Int;
1.80 - type int = int;
1.81 - val toString: int -> string = makestring;
1.82 - fun fromInt (i: int) = i;
1.83 - val fromString = String.stringint;
1.84 - val op + = op + : int * int -> int;
1.85 - val op - = op - : int * int -> int;
1.86 - val op * = op * : int * int -> int;
1.87 - val op div = op div : int * int -> int;
1.88 - val op mod = op mod : int * int -> int;
1.89 - fun pow (x, y) = power x y : int;
1.90 - val op < = op < : int * int -> bool;
1.91 - val op > = op > : int * int -> bool;
1.92 - val op <= = op <= : int * int -> bool;
1.93 - val op >= = op >= : int * int -> bool;
1.94 - val abs = abs: int -> int;
1.95 - val sign = sign: int -> int;
1.96 - fun max (x, y) : int = if x < y then y else x;
1.97 - fun min (x, y) : int = if x < y then x else y;
1.98 - fun compare (x: int, y) = if x = y then EQUAL else if x < y then LESS else GREATER;
1.99 -end;
1.100 -
1.101 -structure IntInf = Int;
1.102 -
1.103 -structure Real =
1.104 -struct
1.105 - open Real;
1.106 - val toString: real -> string = makestring;
1.107 - fun max (x, y) : real = if x < y then y else x;
1.108 - fun min (x, y) : real = if x < y then x else y;
1.109 - val real = real;
1.110 - val floor = floor;
1.111 - val realFloor = real o floor;
1.112 - fun ceil x = ~1 - floor (~ (x + 1.0));
1.113 - fun round x = floor (x + 0.5); (*does not do round-to-nearest*)
1.114 - fun trunc x = if x < 0.0 then ceil x else floor x;
1.115 -end;
1.116 -
1.117 -structure String =
1.118 -struct
1.119 - open String;
1.120 - type char = string
1.121 - fun str (c: char) = c: string;
1.122 - val translate = mapstring;
1.123 - val isPrefix = isprefix;
1.124 - val isSuffix = issuffix;
1.125 - val size = size;
1.126 - fun compare (x: string, y) = if x = y then EQUAL else if x < y then LESS else GREATER;
1.127 - fun substring (s, i, n) = String.substring i (i + n) s
1.128 - handle String.Substring => raise Subscript;
1.129 -end;
1.130 -
1.131 -structure List =
1.132 -struct
1.133 - open List;
1.134 -
1.135 - exception Empty;
1.136 - fun null [] = true | null _ = false;
1.137 - fun hd (x :: _) = x | hd _ = raise Empty;
1.138 - fun tl (_ :: xs) = xs | tl _ = raise Empty;
1.139 - val map = map;
1.140 -
1.141 - fun foldl f b [] = b
1.142 - | foldl f b (x :: xs) = foldl f (f (x, b)) xs;
1.143 -
1.144 - fun foldr f b [] = b
1.145 - | foldr f b (x :: xs) = f (x, foldr f b xs);
1.146 -
1.147 - fun last [] = raise Empty
1.148 - | last [x] = x
1.149 - | last (x::xs) = last xs;
1.150 -
1.151 - fun nth (xs, n) =
1.152 - let fun h [] _ = raise Subscript
1.153 - | h (x::xs) n = if n=0 then x else h xs (n-1)
1.154 - in if n<0 then raise Subscript else h xs n end;
1.155 -
1.156 - fun drop (xs, n) =
1.157 - let fun h xs 0 = xs
1.158 - | h [] n = raise Subscript
1.159 - | h (x::xs) n = h xs (n-1)
1.160 - in if n<0 then raise Subscript else h xs n end;
1.161 -
1.162 - fun take (xs, n) =
1.163 - let fun h xs 0 = []
1.164 - | h [] n = raise Subscript
1.165 - | h (x::xs) n = x :: h xs (n-1)
1.166 - in if n<0 then raise Subscript else h xs n end;
1.167 -
1.168 - fun concat [] = []
1.169 - | concat (l::ls) = l @ concat ls;
1.170 -
1.171 - fun mapPartial f [] = []
1.172 - | mapPartial f (x::xs) =
1.173 - (case f x of NONE => mapPartial f xs
1.174 - | SOME y => y :: mapPartial f xs);
1.175 -
1.176 - fun find _ [] = NONE
1.177 - | find p (x :: xs) = if p x then SOME x else find p xs;
1.178 -
1.179 -
1.180 - (*copy the list preserving elements that satisfy the predicate*)
1.181 - fun filter p [] = []
1.182 - | filter p (x :: xs) = if p x then x :: filter p xs else filter p xs;
1.183 -
1.184 - (*Partition list into elements that satisfy predicate and those that don't.
1.185 - Preserves order of elements in both lists.*)
1.186 - fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) =
1.187 - let fun part ([], answer) = answer
1.188 - | part (x::xs, (ys, ns)) = if p(x)
1.189 - then part (xs, (x::ys, ns))
1.190 - else part (xs, (ys, x::ns))
1.191 - in part (rev ys, ([], [])) end;
1.192 -
1.193 -end;
1.194 -exception Empty = List.Empty;
1.195 -val null = List.null;
1.196 -val hd = List.hd;
1.197 -val tl = List.tl;
1.198 -val map = List.map;
1.199 -val foldl = List.foldl;
1.200 -val foldr = List.foldr;
1.201 -val app = List.app;
1.202 -val length = List.length;
1.203 -
1.204 -structure ListPair =
1.205 -struct
1.206 - fun zip ([], []) = []
1.207 - | zip (x::xs,y::ys) = (x,y) :: zip(xs,ys);
1.208 -
1.209 - fun unzip [] = ([],[])
1.210 - | unzip((x,y)::pairs) =
1.211 - let val (xs,ys) = unzip pairs
1.212 - in (x::xs, y::ys) end;
1.213 -
1.214 - fun app f (x::xs, y::ys) = (f (x, y); app f (xs, ys))
1.215 - | app f _ = ();
1.216 -
1.217 - fun map f ([], []) = []
1.218 - | map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys);
1.219 -
1.220 - fun exists p =
1.221 - let fun boolf ([], []) = false
1.222 - | boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys)
1.223 - in boolf end;
1.224 -
1.225 - fun all p =
1.226 - let fun boolf ([], []) = true
1.227 - | boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys)
1.228 - in boolf end;
1.229 -end;
1.230 -
1.231 -structure TextIO =
1.232 -struct
1.233 - type instream = instream;
1.234 - type outstream = outstream;
1.235 - exception Io = Io;
1.236 - val stdIn = std_in;
1.237 - val stdOut = std_out;
1.238 - val stdErr = std_err;
1.239 - val openIn = open_in;
1.240 - val openAppend = open_append;
1.241 - val openOut = open_out;
1.242 - val closeIn = close_in;
1.243 - val closeOut = close_out;
1.244 - val inputN = input;
1.245 - val inputAll = fn is => inputN (is, 1000000000);
1.246 - val inputLine = input_line;
1.247 - val endOfStream = end_of_stream;
1.248 - val output = output;
1.249 - val flushOut = flush_out;
1.250 -end;
1.251 -
1.252 -
1.253 -
1.254 -(** Compiler-independent timing functions **)
1.255 -
1.256 -fun start_timing() = "FIXME";
1.257 -fun end_timing (s: string) = s;
1.258 -fun check_timer _ = (0, 0, 0);
1.259 -
1.260 -structure Timer =
1.261 -struct
1.262 - type cpu_timer = int;
1.263 - fun startCPUTimer () = 0;
1.264 -end;
1.265 -
1.266 -structure Time =
1.267 -struct
1.268 - exception Time;
1.269 - type time = int;
1.270 - val toString: time -> string = makestring;
1.271 - val zeroTime = 0;
1.272 - fun now () = 0;
1.273 - fun (x: int) + y = x + y;
1.274 - fun (x: int) - y = x - y;
1.275 -end;
1.276 -
1.277 -
1.278 -
1.279 -(** interrupts **) (*Note: may get into race conditions*)
1.280 -
1.281 -fun interruptible f x = f x;
1.282 -fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
1.283 -
1.284 -
1.285 -
1.286 -(** OS related **)
1.287 -
1.288 -val tmp_name =
1.289 - let val count = ref 0 in
1.290 - fn () => (count := ! count + 1;
1.291 - "/tmp/pml" ^ Int.toString (OS.pid ()) ^ "." ^ Int.toString (! count))
1.292 - end;
1.293 -
1.294 -local
1.295 -
1.296 -fun shell cmdline = OS.execve "/bin/sh" ["sh", "-c", cmdline] (OS.envlist());
1.297 -
1.298 -fun execute_rc cmdline =
1.299 - let
1.300 - fun wait pid =
1.301 - (case OS.wait () of
1.302 - NONE => wait pid
1.303 - | SOME (pid', rc) =>
1.304 - if pid = pid' then rc div 256 else raise OS.Error ("wait", "wrong pid", ""));
1.305 - in
1.306 - (case OS.fork () of
1.307 - NONE => shell cmdline
1.308 - | SOME pid => wait pid)
1.309 - end;
1.310 -
1.311 -fun squote s = "'" ^ s ^ "'";
1.312 -fun remove name = (execute_rc ("/bin/rm -- " ^ squote name); ());
1.313 -fun is_dir name = execute_rc ("perl -e \"exit (-d " ^ squote name ^ " ? 0 : 1)\"") = 0;
1.314 -
1.315 -fun execute_result cmdline =
1.316 - let
1.317 - val tmp = tmp_name ();
1.318 - val rc = execute_rc (cmdline ^ " > " ^ tmp);
1.319 - val instream = TextIO.openIn tmp;
1.320 - val result = TextIO.inputAll instream;
1.321 - val _ = TextIO.closeIn instream;
1.322 - val _ = remove tmp;
1.323 - in (rc, result) end;
1.324 -
1.325 -in
1.326 -
1.327 -fun exit rc = shell ("exit " ^ Int.toString rc);
1.328 -fun quit () = exit 0;
1.329 -
1.330 -fun execute cmdline = #2 (execute_result cmdline);
1.331 -
1.332 -fun system cmdline =
1.333 - let val (rc, result) = execute_result cmdline
1.334 - in TextIO.output (TextIO.stdOut, result); TextIO.flushOut TextIO.stdOut; rc end;
1.335 -
1.336 -val string_of_pid: int -> string = makestring;
1.337 -
1.338 -fun getenv var = (case OS.translate var of NONE => "" | SOME s => s);
1.339 -
1.340 -structure OS =
1.341 -struct
1.342 - structure FileSys =
1.343 - struct
1.344 - val tmpName = tmp_name;
1.345 - val chDir = OS.cd;
1.346 - val getDir = OS.pwd;
1.347 - val remove = remove;
1.348 - val isDir = is_dir;
1.349 - val compare = Int.compare;
1.350 -
1.351 - fun modTime name =
1.352 - (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[9]'") of
1.353 - "" => raise TextIO.Io "OS.FileSys.modTime"
1.354 - | s => Int.fromString s);
1.355 - fun fileId name =
1.356 - (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[1]'") of
1.357 - "" => raise TextIO.Io "OS.FileSys.fileId"
1.358 - | s => Int.fromString s);
1.359 - end;
1.360 -end;
1.361 -
1.362 -end;
1.363 -
1.364 -
1.365 -(* use *)
1.366 -
1.367 -local val pml_use = use in
1.368 -
1.369 -fun use name =
1.370 - if name = "ROOT.ML" then (*workaround error about looping compilations*)
1.371 - let
1.372 - val instream = TextIO.openIn name;
1.373 - val txt = TextIO.inputAll instream;
1.374 - val _ = TextIO.closeIn;
1.375 - in use_string txt end
1.376 - else pml_use name;
1.377 -
1.378 -end;
1.379 -
1.380 -fun use_text _ _ _ _ txt = use_string txt;
1.381 -fun use_file _ _ _ name = use name;