--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/poplogml.ML Tue Oct 04 20:38:13 2005 +0200
@@ -0,0 +1,338 @@
+(* Title: Pure/ML-Systems/poplogml.ML
+ ID: $Id$
+ Author: Makarius
+
+Compatibility file for Poplog/PML (version 15.6/2.1).
+*)
+
+(** Basis structures **)
+
+fun pointer_eq (_: 'a, _: 'a) = false;
+
+structure General =
+struct
+ exception Subscript = Array.Subscript;
+ exception Size;
+ exception Fail of string;
+ fun exnMessage (exn: exn) = "exception " ^ makestring exn ^ " raised";
+ datatype order = LESS | EQUAL | GREATER;
+end;
+open General;
+
+structure Bool =
+struct
+ val toString: bool -> string = makestring;
+end;
+
+structure Option =
+struct
+ open Option;
+ exception Option;
+
+ fun valOf (SOME x) = x
+ | valOf NONE = raise Option;
+
+ fun getOpt (SOME x, _) = x
+ | getOpt (NONE, x) = x;
+
+ fun isSome (SOME _) = true
+ | isSome NONE = false;
+end;
+open Option;
+
+structure Option =
+struct
+ open Option;
+ fun map f (SOME x) = SOME (f x)
+ | map _ NONE = NONE;
+end;
+
+structure Int =
+struct
+ open Int;
+ type int = int;
+ val toString: int -> string = makestring;
+ fun fromInt (i: int) = i;
+ val fromString = String.stringint;
+ fun max (x, y) : int = if x < y then y else x;
+ fun min (x, y) : int = if x < y then x else y;
+ fun compare (x: int, y) = if x = y then EQUAL else if x < y then LESS else GREATER;
+end;
+
+structure IntInf = Int;
+
+structure Real =
+struct
+ open Real;
+ val toString: real -> string = makestring;
+ fun max (x, y) : real = if x < y then y else x;
+ fun min (x, y) : real = if x < y then x else y;
+ val real = real;
+ val floor = floor;
+ val realFloor = real o floor;
+ fun ceil x = ~1 - floor (~ (x + 1.0));
+ fun round x = floor (x + 0.5); (*does not do round-to-nearest*)
+ fun trunc x = if x < 0.0 then ceil x else floor x;
+end;
+
+structure String =
+struct
+ open String;
+ type char = string
+ fun str (c: char) = c: string;
+ val translate = mapstring;
+ val isPrefix = isprefix;
+ val isSuffix = issuffix;
+ val size = size;
+ fun compare (x: string, y) = if x = y then EQUAL else if x < y then LESS else GREATER;
+ fun substring (s, i, n) = String.substring i (i + n) s
+ handle String.Substring => raise Subscript;
+end;
+
+
+exception Empty;
+fun null [] = true | null _ = false;
+fun hd (x :: _) = x | hd _ = raise Empty;
+fun tl (_ :: xs) = xs | tl _ = raise Empty;
+val app = List.app;
+val length = List.length;
+
+fun foldl f b [] = b
+ | foldl f b (x :: xs) = foldl f (f (x, b)) xs;
+
+fun foldr f b [] = b
+ | foldr f b (x :: xs) = f (x, foldr f b xs);
+
+structure List =
+struct
+ open List;
+ val null = null;
+ val hd = hd;
+ val tl = tl;
+ val map = map;
+
+ fun last [] = raise Empty
+ | last [x] = x
+ | last (x::xs) = last xs;
+
+ fun nth (xs, n) =
+ let fun h [] _ = raise Subscript
+ | h (x::xs) n = if n=0 then x else h xs (n-1)
+ in if n<0 then raise Subscript else h xs n end;
+
+ fun drop (xs, n) =
+ let fun h xs 0 = xs
+ | h [] n = raise Subscript
+ | h (x::xs) n = h xs (n-1)
+ in if n<0 then raise Subscript else h xs n end;
+
+ fun take (xs, n) =
+ let fun h xs 0 = []
+ | h [] n = raise Subscript
+ | h (x::xs) n = x :: h xs (n-1)
+ in if n<0 then raise Subscript else h xs n end;
+
+ fun concat [] = []
+ | concat (l::ls) = l @ concat ls;
+
+ fun mapPartial f [] = []
+ | mapPartial f (x::xs) =
+ (case f x of NONE => mapPartial f xs
+ | SOME y => y :: mapPartial f xs);
+
+ fun find _ [] = NONE
+ | find p (x :: xs) = if p x then SOME x else find p xs;
+
+
+ (*copy the list preserving elements that satisfy the predicate*)
+ fun filter p [] = []
+ | filter p (x :: xs) = if p x then x :: filter p xs else filter p xs;
+
+ (*Partition list into elements that satisfy predicate and those that don't.
+ Preserves order of elements in both lists.*)
+ fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) =
+ let fun part ([], answer) = answer
+ | part (x::xs, (ys, ns)) = if p(x)
+ then part (xs, (x::ys, ns))
+ else part (xs, (ys, x::ns))
+ in part (rev ys, ([], [])) end;
+
+end;
+
+structure ListPair =
+struct
+ fun zip ([], []) = []
+ | zip (x::xs,y::ys) = (x,y) :: zip(xs,ys);
+
+ fun unzip [] = ([],[])
+ | unzip((x,y)::pairs) =
+ let val (xs,ys) = unzip pairs
+ in (x::xs, y::ys) end;
+
+ fun app f (x::xs, y::ys) = (f (x, y); app f (xs, ys))
+ | app f _ = ();
+
+ fun map f ([], []) = []
+ | map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys);
+
+ fun exists p =
+ let fun boolf ([], []) = false
+ | boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys)
+ in boolf end;
+
+ fun all p =
+ let fun boolf ([], []) = true
+ | boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys)
+ in boolf end;
+end;
+
+structure TextIO =
+struct
+ type instream = instream;
+ type outstream = outstream;
+ exception Io = Io;
+ val stdIn = std_in;
+ val stdOut = std_out;
+ val stdErr = std_err;
+ val openIn = open_in;
+ val openAppend = open_append;
+ val openOut = open_out;
+ val closeIn = close_in;
+ val closeOut = close_out;
+ val inputN = input;
+ val inputAll = fn is => inputN (is, 1000000000);
+ val inputLine = input_line;
+ val endOfStream = end_of_stream;
+ val output = output;
+ val flushOut = flush_out;
+end;
+
+
+
+(** Compiler-independent timing functions **)
+
+fun startTiming() = "FIXME";
+fun endTiming (s: string) = s;
+fun checkTimer _ = (0, 0, 0);
+
+structure Timer =
+struct
+ type cpu_timer = int;
+ fun startCPUTimer () = 0;
+end;
+
+structure Time =
+struct
+ exception Time;
+ type time = int;
+ val toString: time -> string = makestring;
+ val zeroTime = 0;
+ fun now () = 0;
+ fun (x: int) + y = x + y;
+ fun (x: int) - y = x - y;
+end;
+
+
+(* ML toplevel *)
+
+
+fun ml_prompts p1 p2 = ();
+
+fun make_pp path pprint = ();
+fun install_pp _ = ();
+
+fun print_depth _ = ();
+
+fun exception_trace f = f ();
+fun profile (n: int) f x = f x;
+
+
+
+(** interrupts **) (*Note: may get into race conditions*)
+
+fun ignore_interrupt f x = f x;
+fun raise_interrupt f x = f x;
+
+
+
+(** OS related **)
+
+val tmp_name =
+ let val count = ref 0 in
+ fn () => (count := ! count + 1;
+ "/tmp/pml" ^ Int.toString (OS.pid ()) ^ "." ^ Int.toString (! count))
+ end;
+
+local
+
+fun shell cmdline = OS.execve "/bin/sh" ["sh", "-c", cmdline] (OS.envlist());
+
+fun execute_rc cmdline =
+ let
+ fun wait pid =
+ (case OS.wait () of
+ NONE => wait pid
+ | SOME (pid', rc) =>
+ if pid = pid' then rc div 256 else raise OS.Error ("wait", "wrong pid", ""));
+ in
+ (case OS.fork () of
+ NONE => shell cmdline
+ | SOME pid => wait pid)
+ end;
+
+fun squote s = "'" ^ s ^ "'";
+fun remove name = (execute_rc ("/bin/rm -- " ^ squote name); ());
+fun is_dir name = execute_rc ("test -d " ^ squote name) = 0;
+fun is_present name = execute_rc ("test -e " ^ squote name) = 0;
+
+fun execute_result cmdline =
+ let
+ val tmp = tmp_name ();
+ val rc = execute_rc (cmdline ^ " > " ^ tmp);
+ val instream = TextIO.openIn tmp;
+ val result = TextIO.inputAll instream;
+ val _ = TextIO.closeIn instream;
+ val _ = remove tmp;
+ in (rc, result) end;
+
+fun int_of_string s =
+ Int.fromString (if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) else s);
+
+in
+
+fun exit rc = shell ("exit " ^ Int.toString rc);
+fun quit () = exit 0;
+
+fun execute cmdline = #2 (execute_result cmdline);
+
+fun system cmdline =
+ let val (rc, result) = execute_result cmdline
+ in TextIO.output (TextIO.stdOut, result); TextIO.flushOut TextIO.stdOut; rc end;
+
+fun getenv var = (case OS.translate var of NONE => "" | SOME s => s);
+
+structure OS =
+struct
+ structure FileSys =
+ struct
+ val tmpName = tmp_name;
+ val chDir = OS.cd;
+ val getDir = OS.pwd;
+ val remove = remove;
+ val isDir = is_dir;
+ val compare = Int.compare;
+
+ fun modTime name =
+ if is_present name then int_of_string (execute ("stat -c '%Y' " ^ squote name))
+ else raise TextIO.Io "OS.FileSys.modTime";
+
+ fun fileId name =
+ if is_present name then int_of_string (execute ("stat -c '%i' " ^ squote name))
+ else raise TextIO.Io "OS.FileSys.fileId";
+ end;
+end;
+
+end;
+
+
+fun use_text (print, err) verbose txt = raise Fail ("FIXME use_text: " ^ txt);