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