src/Pure/ML-Systems/poplogml.ML
author berghofe
Mon Jan 21 14:18:49 2008 +0100 (2008-01-21)
changeset 25939 ddea202704b4
parent 24688 a5754ca5c510
child 26084 a7475459c740
permissions -rw-r--r--
Removed Logic.auto_rename.
     1 (*  Title:      Pure/ML-Systems/poplogml.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Compatibility file for Poplog/PML (version 15.6/2.1).
     6 *)
     7 
     8 (* Compiler and runtime options *)
     9 
    10 val ml_system_fix_ints = false;
    11 
    12 val _ = Compile.filetype := ".ML";
    13 val _ = Memory.hilim := let fun MB n = n div 4 * 1024 * 1024 in MB 120 end;
    14 val _ = Memory.stacklim := 10 * ! Memory.stacklim;
    15 
    16 fun pointer_eq (_: 'a, _: 'a) = false;
    17 
    18 
    19 (* ML toplevel *)
    20 
    21 fun ml_prompts p1 p2 = ();
    22 
    23 fun make_pp path pprint = ();
    24 fun install_pp _ = ();
    25 
    26 fun get_print_depth () = 10;
    27 fun print_depth _ = ();
    28 
    29 fun exception_trace f = f ();
    30 fun profile (n: int) f x = f x;
    31 
    32 
    33 
    34 (** Basis structures **)
    35 
    36 structure General =
    37 struct
    38   exception Subscript = Array.Subscript;
    39   exception Size;
    40   exception Fail of string;
    41   fun exnMessage (exn: exn) = "exception " ^ makestring exn ^ " raised";
    42   datatype order = LESS | EQUAL | GREATER;
    43 end;
    44 open General;
    45 
    46 structure Bool =
    47 struct
    48   val toString: bool -> string = makestring;
    49 end;
    50 
    51 structure Option =
    52 struct
    53   open Option;
    54   exception Option;
    55 
    56   fun valOf (SOME x) = x
    57     | valOf NONE = raise Option;
    58 
    59   fun getOpt (SOME x, _) = x
    60     | getOpt (NONE, x) = x;
    61 
    62   fun isSome (SOME _) = true
    63     | isSome NONE = false;
    64 end;
    65 open Option;
    66 
    67 structure Option =
    68 struct
    69   open Option;
    70   fun map f (SOME x) = SOME (f x)
    71     | map _ NONE = NONE;
    72 end;
    73 
    74 structure Int =
    75 struct
    76   open Int;
    77   type int = int;
    78   val toString: int -> string = makestring;
    79   fun fromInt (i: int) = i;
    80   val fromString = String.stringint;
    81   val op + = op + : int * int -> int;
    82   val op - = op - : int * int -> int;
    83   val op * = op * : int * int -> int;
    84   val op div = op div : int * int -> int;
    85   val op mod = op mod : int * int -> int;
    86   fun pow (x, y) = power x y : int;
    87   val op < = op < : int * int -> bool;
    88   val op > = op > : int * int -> bool;
    89   val op <= = op <= : int * int -> bool;
    90   val op >= = op >= : int * int -> bool;
    91   val abs = abs: int -> int;
    92   val sign = sign: int -> int;
    93   fun max (x, y) : int = if x < y then y else x;
    94   fun min (x, y) : int = if x < y then x else y;
    95   fun compare (x: int, y) = if x = y then EQUAL else if x < y then LESS else GREATER;
    96 end;
    97 
    98 structure IntInf = Int;
    99 
   100 structure Real =
   101 struct
   102   open Real;
   103   val toString: real -> string = makestring;
   104   fun max (x, y) : real = if x < y then y else x;
   105   fun min (x, y) : real = if x < y then x else y;
   106   val real = real;
   107   val floor = floor;
   108   val realFloor = real o floor;
   109   fun ceil x = ~1 - floor (~ (x + 1.0));
   110   fun round x = floor (x + 0.5);  (*does not do round-to-nearest*)
   111   fun trunc x = if x < 0.0 then ceil x else floor x;
   112 end;
   113 
   114 structure String =
   115 struct
   116   open String;
   117   type char = string
   118   fun str (c: char) = c: string;
   119   val translate = mapstring;
   120   val isPrefix = isprefix;
   121   val isSuffix = issuffix;
   122   val size = size;
   123   fun compare (x: string, y) = if x = y then EQUAL else if x < y then LESS else GREATER;
   124   fun substring (s, i, n) = String.substring i (i + n) s
   125     handle String.Substring => raise Subscript;
   126 end;
   127 
   128 structure List =
   129 struct
   130   open List;
   131 
   132   exception Empty;
   133   fun null [] = true | null _ = false;
   134   fun hd (x :: _) = x | hd _ = raise Empty;
   135   fun tl (_ :: xs) = xs | tl _ = raise Empty;
   136   val map = map;
   137 
   138   fun foldl f b [] = b
   139     | foldl f b (x :: xs) = foldl f (f (x, b)) xs;
   140 
   141   fun foldr f b [] = b
   142     | foldr f b (x :: xs) = f (x, foldr f b xs);
   143 
   144   fun last []      = raise Empty
   145     | last [x]     = x
   146     | last (x::xs) = last xs;
   147 
   148   fun nth (xs, n) =
   149       let fun h []      _ = raise Subscript
   150             | h (x::xs) n = if n=0 then x else h xs (n-1)
   151       in if n<0 then raise Subscript else h xs n end;
   152 
   153   fun drop (xs, n) =
   154       let fun h xs      0 = xs
   155             | h []      n = raise Subscript
   156             | h (x::xs) n = h xs (n-1)
   157       in if n<0 then raise Subscript else h xs n end;
   158 
   159   fun take (xs, n) =
   160       let fun h xs      0 = []
   161             | h []      n = raise Subscript
   162             | h (x::xs) n = x :: h xs (n-1)
   163       in if n<0 then raise Subscript else h xs n end;
   164 
   165   fun concat []      = []
   166     | concat (l::ls) = l @ concat ls;
   167 
   168   fun mapPartial f []      = []
   169     | mapPartial f (x::xs) =
   170          (case f x of NONE   => mapPartial f xs
   171                     | SOME y => y :: mapPartial f xs);
   172 
   173   fun find _ []        = NONE
   174     | find p (x :: xs) = if p x then SOME x else find p xs;
   175 
   176 
   177   (*copy the list preserving elements that satisfy the predicate*)
   178   fun filter p [] = []
   179     | filter p (x :: xs) = if p x then x :: filter p xs else filter p xs;
   180 
   181   (*Partition list into elements that satisfy predicate and those that don't.
   182     Preserves order of elements in both lists.*)
   183   fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) =
   184       let fun part ([], answer) = answer
   185             | part (x::xs, (ys, ns)) = if p(x)
   186               then  part (xs, (x::ys, ns))
   187               else  part (xs, (ys, x::ns))
   188       in  part (rev ys, ([], []))  end;
   189 
   190 end;
   191 exception Empty = List.Empty;
   192 val null = List.null;
   193 val hd = List.hd;
   194 val tl = List.tl;
   195 val map = List.map;
   196 val foldl = List.foldl;
   197 val foldr = List.foldr;
   198 val app = List.app;
   199 val length = List.length;
   200 
   201 structure ListPair =
   202 struct
   203   fun zip ([], [])      = []
   204     | zip (x::xs,y::ys) = (x,y) :: zip(xs,ys);
   205 
   206   fun unzip [] = ([],[])
   207     | unzip((x,y)::pairs) =
   208           let val (xs,ys) = unzip pairs
   209           in  (x::xs, y::ys)  end;
   210 
   211   fun app f (x::xs, y::ys) = (f (x, y); app f (xs, ys))
   212     | app f _ = ();
   213 
   214   fun map f ([], [])      = []
   215     | map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys);
   216 
   217   fun exists p =
   218     let fun boolf ([], [])      = false
   219           | boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys)
   220     in boolf end;
   221 
   222   fun all p =
   223     let fun boolf ([], [])      = true
   224           | boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys)
   225     in boolf end;
   226 end;
   227 
   228 structure TextIO =
   229 struct
   230   type instream = instream;
   231   type outstream = outstream;
   232   exception Io = Io;
   233   val stdIn = std_in;
   234   val stdOut = std_out;
   235   val stdErr = std_err;
   236   val openIn = open_in;
   237   val openAppend = open_append;
   238   val openOut = open_out;
   239   val closeIn = close_in;
   240   val closeOut = close_out;
   241   val inputN = input;
   242   val inputAll = fn is => inputN (is, 1000000000);
   243   val inputLine = input_line;
   244   val endOfStream = end_of_stream;
   245   val output = output;
   246   val flushOut = flush_out;
   247 end;
   248 
   249 
   250 
   251 (** Compiler-independent timing functions **)
   252 
   253 fun start_timing() = "FIXME";
   254 fun end_timing (s: string) = s;
   255 fun check_timer _ = (0, 0, 0);
   256 
   257 structure Timer =
   258 struct
   259   type cpu_timer = int;
   260   fun startCPUTimer () = 0;
   261 end;
   262 
   263 structure Time =
   264 struct
   265   exception Time;
   266   type time = int;
   267   val toString: time -> string = makestring;
   268   val zeroTime = 0;
   269   fun now () = 0;
   270   fun (x: int) + y = x + y;
   271   fun (x: int) - y = x - y;
   272 end;
   273 
   274 
   275 
   276 (** interrupts **)      (*Note: may get into race conditions*)
   277 
   278 fun ignore_interrupt f x = f x;
   279 fun raise_interrupt f x = f x;
   280 
   281 
   282 
   283 (** OS related **)
   284 
   285 val tmp_name =
   286   let val count = ref 0 in
   287     fn () => (count := ! count + 1;
   288       "/tmp/pml" ^ Int.toString (OS.pid ()) ^ "." ^ Int.toString (! count))
   289   end;
   290 
   291 local
   292 
   293 fun shell cmdline = OS.execve "/bin/sh" ["sh", "-c", cmdline] (OS.envlist());
   294 
   295 fun execute_rc cmdline =
   296   let
   297     fun wait pid =
   298       (case OS.wait () of
   299         NONE => wait pid
   300       | SOME (pid', rc) =>
   301           if pid = pid' then rc div 256 else raise OS.Error ("wait", "wrong pid", ""));
   302   in
   303     (case OS.fork () of
   304       NONE => shell cmdline
   305     | SOME pid => wait pid)
   306   end;
   307 
   308 fun squote s = "'" ^ s ^ "'";
   309 fun remove name = (execute_rc ("/bin/rm -- " ^ squote name); ());
   310 fun is_dir name = execute_rc ("perl -e \"exit (-d " ^ squote name ^ " ? 0 : 1)\"") = 0;
   311 
   312 fun execute_result cmdline =
   313   let
   314     val tmp = tmp_name ();
   315     val rc = execute_rc (cmdline  ^ " > " ^ tmp);
   316     val instream = TextIO.openIn tmp;
   317     val result = TextIO.inputAll instream;
   318     val _ = TextIO.closeIn instream;
   319     val _ = remove tmp;
   320   in (rc, result) end;
   321 
   322 in
   323 
   324 fun exit rc = shell ("exit " ^ Int.toString rc);
   325 fun quit () = exit 0;
   326 
   327 fun execute cmdline = #2 (execute_result cmdline);
   328 
   329 fun system cmdline =
   330   let val (rc, result) = execute_result cmdline
   331   in TextIO.output (TextIO.stdOut, result); TextIO.flushOut TextIO.stdOut; rc end;
   332 
   333 val string_of_pid: int -> string = makestring;
   334 
   335 fun getenv var = (case OS.translate var of NONE => "" | SOME s => s);
   336 
   337 structure OS =
   338 struct
   339   structure FileSys =
   340   struct
   341     val tmpName = tmp_name;
   342     val chDir = OS.cd;
   343     val getDir = OS.pwd;
   344     val remove = remove;
   345     val isDir = is_dir;
   346     val compare = Int.compare;
   347 
   348     fun modTime name =
   349       (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[9]'") of
   350         "" => raise TextIO.Io "OS.FileSys.modTime"
   351       | s => Int.fromString s);
   352     fun fileId name =
   353       (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[1]'") of
   354         "" => raise TextIO.Io "OS.FileSys.fileId"
   355       | s => Int.fromString s);
   356   end;
   357 end;
   358 
   359 end;
   360 
   361 
   362 (* use *)
   363 
   364 local val pml_use = use in
   365 
   366 fun use name =
   367   if name = "ROOT.ML" then   (*workaround error about looping compilations*)
   368     let
   369       val instream = TextIO.openIn name;
   370       val txt = TextIO.inputAll instream;
   371       val _ = TextIO.closeIn;
   372     in use_string txt end
   373   else pml_use name;
   374 
   375 end;
   376 
   377 fun use_text _ _ _ txt = use_string txt;
   378 fun use_file _ _ name = use name;