1.1 --- a/etc/settings Sat Jun 14 17:26:09 2008 +0200
1.2 +++ b/etc/settings Sat Jun 14 17:26:10 2008 +0200
1.3 @@ -67,13 +67,6 @@
1.4 #ML_OPTIONS=""
1.5 #ML_PLATFORM=""
1.6
1.7 -# Poplog/PML version 15.6/2.1 (experimental!)
1.8 -#ML_SYSTEM=poplogml
1.9 -#ML_HOME="/usr/local/poplog/current-poplog/bin"
1.10 -#ML_OPTIONS="-noinit"
1.11 -#ML_SUFFIX=".psv"
1.12 -#ML_PLATFORM=""
1.13 -
1.14
1.15 ###
1.16 ### Interactive sessions (cf. isatool tty)
2.1 --- a/lib/scripts/run-poplogml Sat Jun 14 17:26:09 2008 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,131 +0,0 @@
2.4 -#!/usr/bin/env bash
2.5 -#
2.6 -# $Id$
2.7 -# Author: Makarius
2.8 -#
2.9 -# Poplog/PML startup script (version 15.6/2.1).
2.10 -
2.11 -export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
2.12 -
2.13 -
2.14 -## diagnostics
2.15 -
2.16 -function fail_out()
2.17 -{
2.18 - echo "Unable to create output heap file: \"$OUTFILE\"" >&2
2.19 - exit 2
2.20 -}
2.21 -
2.22 -function check_mlhome_file()
2.23 -{
2.24 - if [ ! -f "$1" ]; then
2.25 - echo "Unable to locate $1" >&2
2.26 - echo "Please check your ML_HOME setting!" >&2
2.27 - exit 2
2.28 - fi
2.29 -}
2.30 -
2.31 -function check_heap_file()
2.32 -{
2.33 - if [ ! -f "$1" ]; then
2.34 - echo "Expected to find ML heap file $1" >&2
2.35 - return 1
2.36 - else
2.37 - return 0
2.38 - fi
2.39 -}
2.40 -
2.41 -
2.42 -## prepare databases
2.43 -
2.44 -if [ -z "$INFILE" ]; then
2.45 - EXIT="fun exit (i: int) = OS.execve \"/bin/sh\" [\"sh\", \"-c\", \"exit \" ^ makestring i] (OS.envlist());"
2.46 - USE='pop11
2.47 -section $-ml;
2.48 -
2.49 -ml_exception Use of string;
2.50 -
2.51 -ml_val use : string -> unit =
2.52 -procedure(name) with_props use;
2.53 - lvars name, path;
2.54 - lconstant UseExn = exception("Use");
2.55 -
2.56 - define dlocal pop_exception_handler(n, msg, idstring, severity);
2.57 - returnunless(severity == `E` or severity == `R`)(false);
2.58 - erasenum(n);
2.59 - raise(UseExn(name));
2.60 - enddefine;
2.61 -
2.62 - unless sourcefile(name) ->> path then raise(UseExn(name)) endunless;
2.63 - ml_load(path);
2.64 - ml_unit;
2.65 -endprocedure;
2.66 -
2.67 -ml_val use_string : string -> unit =
2.68 -procedure(str) with_props use_string;
2.69 - lvars str;
2.70 - lconstant UseExn = exception("Use");
2.71 -
2.72 - define dlocal pop_exception_handler(n, msg, idstring, severity);
2.73 - [n ^n msg ^msg idstring ^idstring severity ^severity] ==>
2.74 - returnunless(severity == `E` or severity == `R`)(false);
2.75 - erasenum(n);
2.76 - raise(UseExn(str));
2.77 - enddefine;
2.78 -
2.79 - ml_compile(stringin(str));
2.80 - ml_unit;
2.81 -endprocedure;
2.82 -
2.83 -endsection;
2.84 -ml'
2.85 - DB=""
2.86 -else
2.87 - EXIT=""
2.88 - USE=""
2.89 - DB="+$INFILE"
2.90 -fi
2.91 -
2.92 -if [ -z "$OUTFILE" ]; then
2.93 - COMMIT='fun commit () = (StdIO.output (StdIO.std_err, "Error - Database is not opened for writing.\n"); false);'
2.94 -else
2.95 - ML_OPTIONS="$ML_OPTIONS -nort"
2.96 - if [ -z "$NOWRITE" ]; then
2.97 - COMMIT="fun commit () = if System.make {image =\"$OUTFILE\", lock = false, share = false, banner = false, init = false} then System.restart() else true;"
2.98 - else
2.99 - COMMIT="fun commit () = if System.make {image =\"$OUTFILE\", lock = true, share = true, banner = false, init = false} then System.restart() else true;"
2.100 - fi
2.101 - [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
2.102 -fi
2.103 -
2.104 -
2.105 -## run it!
2.106 -
2.107 -POPLOG="$ML_HOME/poplog"
2.108 -check_mlhome_file "$POPLOG"
2.109 -
2.110 -INIT="$ISABELLE_TMP/init.ml"
2.111 -echo 'pop11
2.112 -section $-ml;
2.113 -false -> ml_quiet;
2.114 -endsection;
2.115 -ml' > "$INIT"
2.116 -
2.117 -echo "$EXIT $USE $COMMIT $MLTEXT" >> "$INIT"
2.118 -
2.119 -if [ -n "$TERMINATE" ]; then
2.120 - ML_OPTIONS="$ML_OPTIONS -nostdin"
2.121 - echo "commit();" >> "$INIT"
2.122 -fi
2.123 -
2.124 -"$POPLOG" pml "$DB" $ML_OPTIONS -load "$INIT" 2>&1
2.125 -RC="$?"
2.126 -
2.127 -rm -f "$INIT"
2.128 -
2.129 -if [ -n "$OUTFILE" ] && check_heap_file "$OUTFILE"; then
2.130 - [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
2.131 - rm -f "$OUTFILE-"
2.132 -fi
2.133 -
2.134 -exit "$RC"
3.1 --- a/src/Pure/ML-Systems/poplogml.ML Sat Jun 14 17:26:09 2008 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,378 +0,0 @@
3.4 -(* Title: Pure/ML-Systems/poplogml.ML
3.5 - ID: $Id$
3.6 - Author: Makarius
3.7 -
3.8 -Compatibility file for Poplog/PML (version 15.6/2.1).
3.9 -*)
3.10 -
3.11 -(* Compiler and runtime options *)
3.12 -
3.13 -val ml_system_fix_ints = false;
3.14 -
3.15 -val _ = Compile.filetype := ".ML";
3.16 -val _ = Memory.hilim := let fun MB n = n div 4 * 1024 * 1024 in MB 120 end;
3.17 -val _ = Memory.stacklim := 10 * ! Memory.stacklim;
3.18 -
3.19 -fun pointer_eq (_: 'a, _: 'a) = false;
3.20 -
3.21 -
3.22 -(* ML toplevel *)
3.23 -
3.24 -fun ml_prompts p1 p2 = ();
3.25 -
3.26 -fun make_pp path pprint = ();
3.27 -fun install_pp _ = ();
3.28 -
3.29 -fun get_print_depth () = 10;
3.30 -fun print_depth _ = ();
3.31 -
3.32 -fun exception_trace f = f ();
3.33 -fun profile (n: int) f x = f x;
3.34 -
3.35 -
3.36 -
3.37 -(** Basis structures **)
3.38 -
3.39 -structure General =
3.40 -struct
3.41 - exception Subscript = Array.Subscript;
3.42 - exception Size;
3.43 - exception Fail of string;
3.44 - fun exnMessage (exn: exn) = "exception " ^ makestring exn ^ " raised";
3.45 - datatype order = LESS | EQUAL | GREATER;
3.46 -end;
3.47 -open General;
3.48 -
3.49 -structure Bool =
3.50 -struct
3.51 - val toString: bool -> string = makestring;
3.52 -end;
3.53 -
3.54 -structure Option =
3.55 -struct
3.56 - open Option;
3.57 - exception Option;
3.58 -
3.59 - fun valOf (SOME x) = x
3.60 - | valOf NONE = raise Option;
3.61 -
3.62 - fun getOpt (SOME x, _) = x
3.63 - | getOpt (NONE, x) = x;
3.64 -
3.65 - fun isSome (SOME _) = true
3.66 - | isSome NONE = false;
3.67 -end;
3.68 -open Option;
3.69 -
3.70 -structure Option =
3.71 -struct
3.72 - open Option;
3.73 - fun map f (SOME x) = SOME (f x)
3.74 - | map _ NONE = NONE;
3.75 -end;
3.76 -
3.77 -structure Int =
3.78 -struct
3.79 - open Int;
3.80 - type int = int;
3.81 - val toString: int -> string = makestring;
3.82 - fun fromInt (i: int) = i;
3.83 - val fromString = String.stringint;
3.84 - val op + = op + : int * int -> int;
3.85 - val op - = op - : int * int -> int;
3.86 - val op * = op * : int * int -> int;
3.87 - val op div = op div : int * int -> int;
3.88 - val op mod = op mod : int * int -> int;
3.89 - fun pow (x, y) = power x y : int;
3.90 - val op < = op < : int * int -> bool;
3.91 - val op > = op > : int * int -> bool;
3.92 - val op <= = op <= : int * int -> bool;
3.93 - val op >= = op >= : int * int -> bool;
3.94 - val abs = abs: int -> int;
3.95 - val sign = sign: int -> int;
3.96 - fun max (x, y) : int = if x < y then y else x;
3.97 - fun min (x, y) : int = if x < y then x else y;
3.98 - fun compare (x: int, y) = if x = y then EQUAL else if x < y then LESS else GREATER;
3.99 -end;
3.100 -
3.101 -structure IntInf = Int;
3.102 -
3.103 -structure Real =
3.104 -struct
3.105 - open Real;
3.106 - val toString: real -> string = makestring;
3.107 - fun max (x, y) : real = if x < y then y else x;
3.108 - fun min (x, y) : real = if x < y then x else y;
3.109 - val real = real;
3.110 - val floor = floor;
3.111 - val realFloor = real o floor;
3.112 - fun ceil x = ~1 - floor (~ (x + 1.0));
3.113 - fun round x = floor (x + 0.5); (*does not do round-to-nearest*)
3.114 - fun trunc x = if x < 0.0 then ceil x else floor x;
3.115 -end;
3.116 -
3.117 -structure String =
3.118 -struct
3.119 - open String;
3.120 - type char = string
3.121 - fun str (c: char) = c: string;
3.122 - val translate = mapstring;
3.123 - val isPrefix = isprefix;
3.124 - val isSuffix = issuffix;
3.125 - val size = size;
3.126 - fun compare (x: string, y) = if x = y then EQUAL else if x < y then LESS else GREATER;
3.127 - fun substring (s, i, n) = String.substring i (i + n) s
3.128 - handle String.Substring => raise Subscript;
3.129 -end;
3.130 -
3.131 -structure List =
3.132 -struct
3.133 - open List;
3.134 -
3.135 - exception Empty;
3.136 - fun null [] = true | null _ = false;
3.137 - fun hd (x :: _) = x | hd _ = raise Empty;
3.138 - fun tl (_ :: xs) = xs | tl _ = raise Empty;
3.139 - val map = map;
3.140 -
3.141 - fun foldl f b [] = b
3.142 - | foldl f b (x :: xs) = foldl f (f (x, b)) xs;
3.143 -
3.144 - fun foldr f b [] = b
3.145 - | foldr f b (x :: xs) = f (x, foldr f b xs);
3.146 -
3.147 - fun last [] = raise Empty
3.148 - | last [x] = x
3.149 - | last (x::xs) = last xs;
3.150 -
3.151 - fun nth (xs, n) =
3.152 - let fun h [] _ = raise Subscript
3.153 - | h (x::xs) n = if n=0 then x else h xs (n-1)
3.154 - in if n<0 then raise Subscript else h xs n end;
3.155 -
3.156 - fun drop (xs, n) =
3.157 - let fun h xs 0 = xs
3.158 - | h [] n = raise Subscript
3.159 - | h (x::xs) n = h xs (n-1)
3.160 - in if n<0 then raise Subscript else h xs n end;
3.161 -
3.162 - fun take (xs, n) =
3.163 - let fun h xs 0 = []
3.164 - | h [] n = raise Subscript
3.165 - | h (x::xs) n = x :: h xs (n-1)
3.166 - in if n<0 then raise Subscript else h xs n end;
3.167 -
3.168 - fun concat [] = []
3.169 - | concat (l::ls) = l @ concat ls;
3.170 -
3.171 - fun mapPartial f [] = []
3.172 - | mapPartial f (x::xs) =
3.173 - (case f x of NONE => mapPartial f xs
3.174 - | SOME y => y :: mapPartial f xs);
3.175 -
3.176 - fun find _ [] = NONE
3.177 - | find p (x :: xs) = if p x then SOME x else find p xs;
3.178 -
3.179 -
3.180 - (*copy the list preserving elements that satisfy the predicate*)
3.181 - fun filter p [] = []
3.182 - | filter p (x :: xs) = if p x then x :: filter p xs else filter p xs;
3.183 -
3.184 - (*Partition list into elements that satisfy predicate and those that don't.
3.185 - Preserves order of elements in both lists.*)
3.186 - fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) =
3.187 - let fun part ([], answer) = answer
3.188 - | part (x::xs, (ys, ns)) = if p(x)
3.189 - then part (xs, (x::ys, ns))
3.190 - else part (xs, (ys, x::ns))
3.191 - in part (rev ys, ([], [])) end;
3.192 -
3.193 -end;
3.194 -exception Empty = List.Empty;
3.195 -val null = List.null;
3.196 -val hd = List.hd;
3.197 -val tl = List.tl;
3.198 -val map = List.map;
3.199 -val foldl = List.foldl;
3.200 -val foldr = List.foldr;
3.201 -val app = List.app;
3.202 -val length = List.length;
3.203 -
3.204 -structure ListPair =
3.205 -struct
3.206 - fun zip ([], []) = []
3.207 - | zip (x::xs,y::ys) = (x,y) :: zip(xs,ys);
3.208 -
3.209 - fun unzip [] = ([],[])
3.210 - | unzip((x,y)::pairs) =
3.211 - let val (xs,ys) = unzip pairs
3.212 - in (x::xs, y::ys) end;
3.213 -
3.214 - fun app f (x::xs, y::ys) = (f (x, y); app f (xs, ys))
3.215 - | app f _ = ();
3.216 -
3.217 - fun map f ([], []) = []
3.218 - | map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys);
3.219 -
3.220 - fun exists p =
3.221 - let fun boolf ([], []) = false
3.222 - | boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys)
3.223 - in boolf end;
3.224 -
3.225 - fun all p =
3.226 - let fun boolf ([], []) = true
3.227 - | boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys)
3.228 - in boolf end;
3.229 -end;
3.230 -
3.231 -structure TextIO =
3.232 -struct
3.233 - type instream = instream;
3.234 - type outstream = outstream;
3.235 - exception Io = Io;
3.236 - val stdIn = std_in;
3.237 - val stdOut = std_out;
3.238 - val stdErr = std_err;
3.239 - val openIn = open_in;
3.240 - val openAppend = open_append;
3.241 - val openOut = open_out;
3.242 - val closeIn = close_in;
3.243 - val closeOut = close_out;
3.244 - val inputN = input;
3.245 - val inputAll = fn is => inputN (is, 1000000000);
3.246 - val inputLine = input_line;
3.247 - val endOfStream = end_of_stream;
3.248 - val output = output;
3.249 - val flushOut = flush_out;
3.250 -end;
3.251 -
3.252 -
3.253 -
3.254 -(** Compiler-independent timing functions **)
3.255 -
3.256 -fun start_timing() = "FIXME";
3.257 -fun end_timing (s: string) = s;
3.258 -fun check_timer _ = (0, 0, 0);
3.259 -
3.260 -structure Timer =
3.261 -struct
3.262 - type cpu_timer = int;
3.263 - fun startCPUTimer () = 0;
3.264 -end;
3.265 -
3.266 -structure Time =
3.267 -struct
3.268 - exception Time;
3.269 - type time = int;
3.270 - val toString: time -> string = makestring;
3.271 - val zeroTime = 0;
3.272 - fun now () = 0;
3.273 - fun (x: int) + y = x + y;
3.274 - fun (x: int) - y = x - y;
3.275 -end;
3.276 -
3.277 -
3.278 -
3.279 -(** interrupts **) (*Note: may get into race conditions*)
3.280 -
3.281 -fun interruptible f x = f x;
3.282 -fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
3.283 -
3.284 -
3.285 -
3.286 -(** OS related **)
3.287 -
3.288 -val tmp_name =
3.289 - let val count = ref 0 in
3.290 - fn () => (count := ! count + 1;
3.291 - "/tmp/pml" ^ Int.toString (OS.pid ()) ^ "." ^ Int.toString (! count))
3.292 - end;
3.293 -
3.294 -local
3.295 -
3.296 -fun shell cmdline = OS.execve "/bin/sh" ["sh", "-c", cmdline] (OS.envlist());
3.297 -
3.298 -fun execute_rc cmdline =
3.299 - let
3.300 - fun wait pid =
3.301 - (case OS.wait () of
3.302 - NONE => wait pid
3.303 - | SOME (pid', rc) =>
3.304 - if pid = pid' then rc div 256 else raise OS.Error ("wait", "wrong pid", ""));
3.305 - in
3.306 - (case OS.fork () of
3.307 - NONE => shell cmdline
3.308 - | SOME pid => wait pid)
3.309 - end;
3.310 -
3.311 -fun squote s = "'" ^ s ^ "'";
3.312 -fun remove name = (execute_rc ("/bin/rm -- " ^ squote name); ());
3.313 -fun is_dir name = execute_rc ("perl -e \"exit (-d " ^ squote name ^ " ? 0 : 1)\"") = 0;
3.314 -
3.315 -fun execute_result cmdline =
3.316 - let
3.317 - val tmp = tmp_name ();
3.318 - val rc = execute_rc (cmdline ^ " > " ^ tmp);
3.319 - val instream = TextIO.openIn tmp;
3.320 - val result = TextIO.inputAll instream;
3.321 - val _ = TextIO.closeIn instream;
3.322 - val _ = remove tmp;
3.323 - in (rc, result) end;
3.324 -
3.325 -in
3.326 -
3.327 -fun exit rc = shell ("exit " ^ Int.toString rc);
3.328 -fun quit () = exit 0;
3.329 -
3.330 -fun execute cmdline = #2 (execute_result cmdline);
3.331 -
3.332 -fun system cmdline =
3.333 - let val (rc, result) = execute_result cmdline
3.334 - in TextIO.output (TextIO.stdOut, result); TextIO.flushOut TextIO.stdOut; rc end;
3.335 -
3.336 -val string_of_pid: int -> string = makestring;
3.337 -
3.338 -fun getenv var = (case OS.translate var of NONE => "" | SOME s => s);
3.339 -
3.340 -structure OS =
3.341 -struct
3.342 - structure FileSys =
3.343 - struct
3.344 - val tmpName = tmp_name;
3.345 - val chDir = OS.cd;
3.346 - val getDir = OS.pwd;
3.347 - val remove = remove;
3.348 - val isDir = is_dir;
3.349 - val compare = Int.compare;
3.350 -
3.351 - fun modTime name =
3.352 - (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[9]'") of
3.353 - "" => raise TextIO.Io "OS.FileSys.modTime"
3.354 - | s => Int.fromString s);
3.355 - fun fileId name =
3.356 - (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[1]'") of
3.357 - "" => raise TextIO.Io "OS.FileSys.fileId"
3.358 - | s => Int.fromString s);
3.359 - end;
3.360 -end;
3.361 -
3.362 -end;
3.363 -
3.364 -
3.365 -(* use *)
3.366 -
3.367 -local val pml_use = use in
3.368 -
3.369 -fun use name =
3.370 - if name = "ROOT.ML" then (*workaround error about looping compilations*)
3.371 - let
3.372 - val instream = TextIO.openIn name;
3.373 - val txt = TextIO.inputAll instream;
3.374 - val _ = TextIO.closeIn;
3.375 - in use_string txt end
3.376 - else pml_use name;
3.377 -
3.378 -end;
3.379 -
3.380 -fun use_text _ _ _ _ txt = use_string txt;
3.381 -fun use_file _ _ _ name = use name;