# HG changeset patch
# User wenzelm
# Date 1128451093 -7200
# Node ID 8f443890fab94cd3af8ee929346be7137718ef69
# Parent  87a9b1d48e25a6766c4e26a478e3a81dcbc5d02a
Compatibility file for Poplog/PML (version 15.6/2.1).

diff -r 87a9b1d48e25 -r 8f443890fab9 src/Pure/ML-Systems/poplogml.ML
--- /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);