src/Pure/ML-Systems/alice.ML
author wenzelm
Tue Apr 03 19:24:22 2007 +0200 (2007-04-03)
changeset 22575 2ed8a11f3172
parent 22563 78fb2af1a5c3
child 22576 1beba4e2aa9f
permissions -rw-r--r--
fixed chr/explode;
     1 (*  Title:      Pure/ML-Systems/alice.ML
     2     ID:         $Id$
     3 
     4 Compatibility file for Alice 1.4 (CVS version).
     5 val ml_system = "alice";
     6 use "ML-Systems/alice.ML";
     7 *)
     8 
     9 fun exit 0 = (OS.Process.exit OS.Process.success): unit
    10   | exit _ = OS.Process.exit OS.Process.failure;
    11 
    12 
    13 (** ML system related **)
    14 
    15 (*low-level pointer equality*)
    16 fun pointer_eq (_: 'a, _: 'a) = false;
    17 
    18 
    19 (* restore old-style character / string functions *)
    20 
    21 exception Ord;
    22 fun ord "" = raise Ord
    23   | ord s = Char.ord (String.sub (s, 0));
    24 
    25 val chr = String.str o chr;
    26 val explode = map String.str o String.explode;
    27 val implode = String.concat;
    28 
    29 
    30 (* Poly/ML emulation *)
    31 
    32 fun quit () = exit 0;
    33 
    34 fun print_depth n = Print.depth := n;
    35 
    36 
    37 (* compiler-independent timing functions *)
    38 
    39 structure Timer =
    40 struct
    41   open Timer;
    42   type cpu_timer = unit;
    43   fun startCPUTimer () = ();
    44   fun checkCPUTimer () = {sys = Time.zeroTime, usr = Time.zeroTime};
    45   fun checkGCTime () = Time.zeroTime;
    46 end;
    47 
    48 fun start_timing () =
    49   let val CPUtimer = Timer.startCPUTimer();
    50       val time = Timer.checkCPUTimer(CPUtimer)
    51   in  (CPUtimer,time)  end;
    52 
    53 fun end_timing (CPUtimer, {sys,usr}) =
    54   let open Time  (*...for Time.toString, Time.+ and Time.- *)
    55       val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
    56   in  "User " ^ toString (usr2-usr) ^
    57       "  All "^ toString (sys2-sys + usr2-usr) ^
    58       " secs"
    59       handle Time => ""
    60   end;
    61 
    62 fun check_timer timer =
    63   let
    64     val {sys, usr} = Timer.checkCPUTimer timer;
    65     val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
    66   in (sys, usr, gc) end;
    67 
    68 
    69 (*prompts*)
    70 fun ml_prompts p1 p2 = ();
    71 
    72 (*dummy implementation*)
    73 fun profile (n: int) f x = f x;
    74 
    75 (*dummy implementation*)
    76 fun exception_trace f = f ();
    77 
    78 (*dummy implementation*)
    79 fun print x = x;
    80 
    81 
    82 (* toplevel pretty printing (see also Pure/install_pp.ML) *)
    83 
    84 fun make_pp path pprint = (path, pprint);
    85 fun install_pp (path, pp) = ();
    86 
    87 
    88 (* ML command execution *)
    89 
    90 fun use_text name (print, err) verbose txt = (Compiler.eval txt; ());
    91 
    92 fun use_file _ _ name = use name;
    93 
    94 
    95 
    96 (** interrupts **)
    97 
    98 exception Interrupt;
    99 
   100 fun ignore_interrupt f x = f x;
   101 fun raise_interrupt f x = f x;
   102 
   103 
   104 (* basis library fixes *)
   105 
   106 structure TextIO =
   107 struct
   108   open TextIO;
   109 
   110   fun inputLine is =
   111     (case TextIO.inputLine is of
   112       SOME str => str
   113     | NONE => "")
   114     handle IO.Io _ => raise Interrupt;
   115 end;
   116 
   117 
   118 (* bounded time execution *)
   119 
   120 (*dummy implementation*)
   121 fun interrupt_timeout time f x =
   122   f x;
   123 
   124 
   125 
   126 (** OS related **)
   127 
   128 (* system command execution *)
   129 
   130 (*execute Unix command which doesn't take any input from stdin and
   131   sends its output to stdout; could be done more easily by Unix.execute,
   132   but that function doesn't use the PATH*)
   133 fun execute command =
   134   let
   135     val tmp_name = OS.FileSys.tmpName ();
   136     val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
   137     val result = TextIO.inputAll is;
   138   in
   139     TextIO.closeIn is;
   140     OS.FileSys.remove tmp_name;
   141     result
   142   end;
   143 
   144 (*plain version; with return code*)
   145 val system = OS.Process.system: string -> int;
   146 
   147 structure OS =
   148 struct
   149   open OS;
   150   structure FileSys =
   151   struct
   152     fun fileId name =
   153       (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[1]'") of
   154         "" => raise Fail "OS.FileSys.fileId"   (* FIXME IO.Io!? *)
   155       | s => (case Int.fromString s of NONE => raise Fail "OS.FileSys.fileId" | SOME i => i));
   156     val compare = Int.compare;
   157     open FileSys;
   158   end;
   159 end;
   160 
   161 
   162 (* getenv *)
   163 
   164 fun getenv var =
   165   (case OS.Process.getEnv var of
   166     NONE => ""
   167   | SOME txt => txt);