src/Pure/ML-Systems/polyml_common.ML
changeset 26215 94d32a7cd0fb
child 26220 d34b68c21f9a
equal deleted inserted replaced
26214:73ed8cb8ac4d 26215:94d32a7cd0fb
       
     1 (*  Title:      Pure/ML-Systems/polyml_common.ML
       
     2     ID:         $Id$
       
     3 
       
     4 Compatibility file for Poly/ML -- common part for 4.x and 5.x.
       
     5 *)
       
     6 
       
     7 use "ML-Systems/exn.ML";
       
     8 if List.exists (fn s => s = "Universal") (PolyML.Compiler.structureNames ()) then ()
       
     9 else use "ML-Systems/universal.ML";
       
    10 use "ML-Systems/multithreading.ML";
       
    11 use "ML-Systems/time_limit.ML";
       
    12 
       
    13 
       
    14 (** ML system and platform related **)
       
    15 
       
    16 (* Compiler options *)
       
    17 
       
    18 val ml_system_fix_ints = false;
       
    19 
       
    20 PolyML.Compiler.printInAlphabeticalOrder := false;
       
    21 PolyML.Compiler.maxInlineSize := 80;
       
    22 
       
    23 
       
    24 (* String compatibility *)
       
    25 
       
    26 (*low-level pointer equality*)
       
    27 val pointer_eq = Address.wordEq;
       
    28 
       
    29 
       
    30 (* old Poly/ML emulation *)
       
    31 
       
    32 local
       
    33   val orig_exit = exit;
       
    34 in
       
    35   open PolyML;
       
    36   val exit = orig_exit;
       
    37   fun quit () = exit 0;
       
    38 end;
       
    39 
       
    40 
       
    41 (* restore old-style character / string functions *)
       
    42 
       
    43 val ord = SML90.ord;
       
    44 val chr = SML90.chr;
       
    45 val explode = SML90.explode;
       
    46 val implode = SML90.implode;
       
    47 
       
    48 
       
    49 (* compiler-independent timing functions *)
       
    50 
       
    51 fun start_timing () =
       
    52   let val CPUtimer = Timer.startCPUTimer();
       
    53       val time = Timer.checkCPUTimer(CPUtimer)
       
    54   in  (CPUtimer,time)  end;
       
    55 
       
    56 fun end_timing (CPUtimer, {sys,usr}) =
       
    57   let open Time  (*...for Time.toString, Time.+ and Time.- *)
       
    58       val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
       
    59   in  "User " ^ toString (usr2-usr) ^
       
    60       "  All "^ toString (sys2-sys + usr2-usr) ^
       
    61       " secs"
       
    62       handle Time => ""
       
    63   end;
       
    64 
       
    65 fun check_timer timer =
       
    66   let
       
    67     val {sys, usr} = Timer.checkCPUTimer timer;
       
    68     val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
       
    69   in (sys, usr, gc) end;
       
    70 
       
    71 
       
    72 (* prompts *)
       
    73 
       
    74 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
       
    75 
       
    76 
       
    77 (* toplevel pretty printing (see also Pure/pure_setup.ML) *)
       
    78 
       
    79 fun make_pp _ pprint (str, blk, brk, en) _ _ obj =
       
    80   pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
       
    81     fn () => brk (99999, 0), en);
       
    82 
       
    83 (*print depth*)
       
    84 local
       
    85   val depth = ref 10;
       
    86 in
       
    87   fun get_print_depth () = ! depth;
       
    88   fun print_depth n = (depth := n; PolyML.print_depth n);
       
    89 end;
       
    90 
       
    91 
       
    92 (* ML command execution -- 'eval' *)
       
    93 
       
    94 fun use_text (tune: string -> string) name (print, err) verbose txt =
       
    95   let
       
    96     val in_buffer = ref (explode (tune txt));
       
    97     val out_buffer = ref ([]: string list);
       
    98     fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
       
    99 
       
   100     fun get () =
       
   101       (case ! in_buffer of
       
   102         [] => ""
       
   103       | c :: cs => (in_buffer := cs; c));
       
   104     fun put s = out_buffer := s :: ! out_buffer;
       
   105 
       
   106     fun exec () =
       
   107       (case ! in_buffer of
       
   108         [] => ()
       
   109       | _ => (PolyML.compiler (get, put) (); exec ()));
       
   110   in
       
   111     exec () handle exn =>
       
   112       (err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
       
   113     if verbose then print (output ()) else ()
       
   114   end;
       
   115 
       
   116 fun use_file tune output verbose name =
       
   117   let
       
   118     val instream = TextIO.openIn name;
       
   119     val txt = TextIO.inputAll instream before TextIO.closeIn instream;
       
   120   in use_text tune name output verbose txt end;
       
   121 
       
   122 
       
   123 (*eval command line arguments*)
       
   124 local
       
   125   fun println s =
       
   126     (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut);
       
   127   fun eval "-q" = ()
       
   128     | eval txt = use_text (fn x => x) "" (println, println) false txt;
       
   129 in
       
   130   val _ = PolyML.onEntry (fn () =>
       
   131    (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ()));
       
   132     app eval (CommandLine.arguments ())));
       
   133 end;
       
   134 
       
   135 
       
   136 
       
   137 (** interrupts **)
       
   138 
       
   139 exception Interrupt = SML90.Interrupt;
       
   140 
       
   141 local
       
   142 
       
   143 val sig_int = 2;
       
   144 val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
       
   145 
       
   146 val _ = Signal.signal (sig_int, default_handler);
       
   147 
       
   148 fun change_signal new_handler f x =
       
   149   let
       
   150     (*RACE wrt. other signals!*)
       
   151     val old_handler = Signal.signal (sig_int, new_handler);
       
   152     val result = Exn.capture (f old_handler) x;
       
   153     val _ = Signal.signal (sig_int, old_handler);
       
   154   in Exn.release result end;
       
   155 
       
   156 in
       
   157 
       
   158 fun interruptible f = change_signal default_handler (fn _ => f);
       
   159 
       
   160 fun uninterruptible f =
       
   161   change_signal Signal.SIG_IGN
       
   162     (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
       
   163 
       
   164 end;
       
   165 
       
   166 
       
   167 
       
   168 (** OS related **)
       
   169 
       
   170 (* Posix patches *)
       
   171 
       
   172 (*This extension of the Poly/ML Signal structure is only necessary
       
   173   because in SML/NJ, types Posix.Signal.signal and Signals.signal differ.*)
       
   174 structure IsaSignal =
       
   175 struct
       
   176   open Signal
       
   177   val usr1 = Posix.Signal.usr1
       
   178   val usr2 = Posix.Signal.usr2
       
   179   val alrm = Posix.Signal.alrm
       
   180   val chld = Posix.Signal.chld
       
   181   val cont = Posix.Signal.cont
       
   182   val int  = Posix.Signal.int
       
   183   val quit = Posix.Signal.quit
       
   184 end;
       
   185 
       
   186 
       
   187 (* current directory *)
       
   188 
       
   189 val cd = OS.FileSys.chDir;
       
   190 val pwd = OS.FileSys.getDir;
       
   191 
       
   192 
       
   193 (* system command execution *)
       
   194 
       
   195 (*execute Unix command which doesn't take any input from stdin and
       
   196   sends its output to stdout; could be done more easily by Unix.execute,
       
   197   but that function doesn't use the PATH*)
       
   198 fun execute command =
       
   199   let
       
   200     val tmp_name = OS.FileSys.tmpName ();
       
   201     val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
       
   202     val result = TextIO.inputAll is;
       
   203   in
       
   204     TextIO.closeIn is;
       
   205     OS.FileSys.remove tmp_name;
       
   206     result
       
   207   end;
       
   208 
       
   209 (*plain version; with return code*)
       
   210 fun system cmd =
       
   211   if OS.Process.isSuccess (OS.Process.system cmd) then 0 else 1;
       
   212 
       
   213 
       
   214 (*Convert a process ID to a decimal string (chiefly for tracing)*)
       
   215 fun string_of_pid pid =
       
   216   Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));
       
   217 
       
   218 
       
   219 (* getenv *)
       
   220 
       
   221 fun getenv var =
       
   222   (case OS.Process.getEnv var of
       
   223     NONE => ""
       
   224   | SOME txt => txt);
       
   225 
       
   226 
       
   227 (* profile execution *)
       
   228 
       
   229 fun profile 0 f x = f x
       
   230   | profile n f x =
       
   231       let
       
   232         val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
       
   233         val res = Exn.capture f x;
       
   234         val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
       
   235       in Exn.release res end;
       
   236