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