src/Pure/ML-Systems/smlnj.ML
author wenzelm
Mon Jul 23 14:06:11 2007 +0200 (2007-07-23)
changeset 23921 947152add153
parent 23826 463903573934
child 23965 f93e509659c1
permissions -rw-r--r--
added compatibility file for ML systems without multithreading;
     1 (*  Title:      Pure/ML-Systems/smlnj.ML
     2     ID:         $Id$
     3 
     4 Compatibility file for Standard ML of New Jersey 110 or later.
     5 *)
     6 
     7 use "ML-Systems/no_multithreading.ML";
     8 
     9 
    10 (** ML system related **)
    11 
    12 (*low-level pointer equality*)
    13 
    14 CM.autoload "$smlnj/init/init.cmi";
    15 val pointer_eq = InlineT.ptreql;
    16 
    17 
    18 (* restore old-style character / string functions *)
    19 
    20 val ord     = SML90.ord;
    21 val chr     = SML90.chr;
    22 val explode = SML90.explode;
    23 val implode = SML90.implode;
    24 
    25 
    26 (* New Jersey ML parameters *)
    27 
    28 val _ =
    29  (Control.Print.printLength := 1000;
    30   Control.Print.printDepth := 350;
    31   Control.Print.stringDepth := 250;
    32   Control.Print.signatures := 2;
    33   Control.MC.matchRedundantError := false);
    34 
    35 
    36 (* Poly/ML emulation *)
    37 
    38 fun quit () = exit 0;
    39 
    40 (*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
    41 fun print_depth n =
    42  (Control.Print.printDepth := n div 2;
    43   Control.Print.printLength := n);
    44 
    45 
    46 (* compiler-independent timing functions *)
    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   (Control.primaryPrompt := p1; Control.secondaryPrompt := 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 (*dummy implementation*)
    83 fun makestring x = "dummy string for SML New Jersey";
    84 
    85 
    86 (* toplevel pretty printing (see also Pure/install_pp.ML) *)
    87 
    88 fun make_pp path pprint =
    89   let
    90     open PrettyPrint;
    91 
    92     fun pp pps obj =
    93       pprint obj
    94         (string pps, openHOVBox pps o Rel,
    95           fn wd => break pps {nsp=wd, offset=0}, fn () => newline pps,
    96           fn () => closeBox pps);
    97   in (path, pp) end;
    98 
    99 fun install_pp (path, pp) = CompilerPPTable.install_pp path pp;
   100 
   101 
   102 (* ML command execution *)
   103 
   104 fun use_text name (print, err) verbose txt =
   105   let
   106     val ref out_orig = Control.Print.out;
   107 
   108     val out_buffer = ref ([]: string list);
   109     val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
   110     fun output () =
   111       let val str = implode (rev (! out_buffer))
   112       in String.substring (str, 0, Int.max (0, size str - 1)) end;
   113   in
   114     Control.Print.out := out;
   115     Backend.Interact.useStream (TextIO.openString txt) handle exn =>
   116       (Control.Print.out := out_orig;
   117         err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
   118     Control.Print.out := out_orig;
   119     if verbose then print (output ()) else ()
   120   end;
   121 
   122 fun use_file _ _ name = use name;
   123 
   124 
   125 
   126 (** interrupts **)
   127 
   128 exception Interrupt;
   129 
   130 local
   131 
   132 fun capture f x = ((f x): unit; NONE) handle exn => SOME exn;
   133 
   134 fun release NONE = ()
   135   | release (SOME exn) = raise exn;
   136 
   137 in
   138 
   139 fun ignore_interrupt f x =
   140   let
   141     val old_handler = Signals.setHandler (Signals.sigINT, Signals.IGNORE);
   142     val result = capture f x;
   143     val _ = Signals.setHandler (Signals.sigINT, old_handler);
   144   in release result end;
   145 
   146 fun raise_interrupt f x =
   147   let
   148     val interrupted = ref false;
   149     val result = ref NONE;
   150     val old_handler = Signals.inqHandler Signals.sigINT;
   151   in
   152     SMLofNJ.Cont.callcc (fn cont =>
   153       (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => (interrupted := true; cont)));
   154       result := capture f x));
   155     Signals.setHandler (Signals.sigINT, old_handler);
   156     if ! interrupted then raise Interrupt else release (! result)
   157   end;
   158 
   159 end;
   160 
   161 
   162 (* basis library fixes *)
   163 
   164 structure TextIO =
   165 struct
   166   open TextIO;
   167   fun inputLine is = TextIO.inputLine is
   168     handle IO.Io _ => raise Interrupt;
   169 end;
   170 
   171 
   172 (* bounded time execution *)
   173 
   174 fun interrupt_timeout time f x =
   175   TimeLimit.timeLimit time f x
   176     handle TimeLimit.TimeOut => raise Interrupt;
   177 
   178 
   179 (** Signal handling: emulation of the Poly/ML Signal structure. Note that types
   180     Posix.Signal.signal and Signals.signal differ **)
   181 
   182 structure IsaSignal =
   183 struct
   184 
   185 datatype sig_handle = SIG_DFL | SIG_IGN | SIG_HANDLE of Signals.signal -> unit;
   186 
   187 (*From the SML/NJ documentation: "HANDLER(f) installs a handler for a
   188   signal. When signal is delivered to the process, the execution state
   189   of the current thread will be bundled up as a continuation k, then
   190   f(signal,n,k) will be called. The number n is the number of times
   191   signal has been signalled since the last time f was invoked for it."*)
   192 
   193 fun toAction SIG_DFL = Signals.DEFAULT
   194   | toAction SIG_IGN = Signals.IGNORE
   195   | toAction (SIG_HANDLE iu) =
   196       Signals.HANDLER (fn (signo,_,cont) => (iu signo; cont));
   197 
   198 (*The types are correct, but I'm not sure about the semantics!*)
   199 fun fromAction Signals.DEFAULT = SIG_DFL
   200   | fromAction Signals.IGNORE = SIG_IGN
   201   | fromAction (Signals.HANDLER f) =
   202       SIG_HANDLE (fn signo => SMLofNJ.Cont.callcc (fn k => (f (signo,0,k); ())));
   203 
   204 (*Poly/ML version has type  int * sig_handle -> sig_handle*)
   205 fun signal (signo, sh) = fromAction (Signals.setHandler (signo, toAction sh));
   206 
   207 val usr1 = UnixSignals.sigUSR1
   208 val usr2 = UnixSignals.sigUSR2
   209 val alrm = UnixSignals.sigALRM
   210 val chld = UnixSignals.sigCHLD
   211 val cont = UnixSignals.sigCONT
   212 val int = UnixSignals.sigINT
   213 val quit = UnixSignals.sigQUIT
   214 val term = UnixSignals.sigTERM
   215 
   216 end;
   217 
   218 
   219 (** OS related **)
   220 
   221 (* current directory *)
   222 
   223 val cd = OS.FileSys.chDir;
   224 val pwd = OS.FileSys.getDir;
   225 
   226 
   227 (* system command execution *)
   228 
   229 (*execute Unix command which doesn't take any input from stdin and
   230   sends its output to stdout; could be done more easily by Unix.execute,
   231   but that function doesn't use the PATH*)
   232 fun execute command =
   233   let
   234     val tmp_name = OS.FileSys.tmpName ();
   235     val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
   236     val result = TextIO.inputAll is;
   237   in
   238     TextIO.closeIn is;
   239     OS.FileSys.remove tmp_name;
   240     result
   241   end;
   242 
   243 (*plain version; with return code*)
   244 val system = OS.Process.system: string -> int;
   245 
   246 
   247 (*Convert a process ID to a decimal string (chiefly for tracing)*)
   248 fun string_of_pid pid =
   249     Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));
   250 
   251 
   252 (* getenv *)
   253 
   254 fun getenv var =
   255   (case OS.Process.getEnv var of
   256     NONE => ""
   257   | SOME txt => txt);