# HG changeset patch # User wenzelm # Date 1163197330 -3600 # Node ID 6d2306b2376d4933b85589c4e65337142632abc2 # Parent 2b60e9b70a8cca5e926ae13ce69baa9649e883a0 tuned names of start_timing,/end_timing/check_timer; removed obsolete ML compatibility fragments; diff -r 2b60e9b70a8c -r 6d2306b2376d src/Pure/ML-Systems/mosml.ML --- a/src/Pure/ML-Systems/mosml.ML Fri Nov 10 23:22:04 2006 +0100 +++ b/src/Pure/ML-Systems/mosml.ML Fri Nov 10 23:22:10 2006 +0100 @@ -27,6 +27,7 @@ load "OS"; load "Process"; load "FileSys"; +load "IO"; (*low-level pointer equality*) local val cast : 'a -> int = Obj.magic @@ -93,7 +94,34 @@ load "Timer"; -use "ML-Systems/cpu-timer-gc.ML"; +fun start_timing () = + let val CPUtimer = Timer.startCPUTimer(); + val time = Timer.checkCPUTimer(CPUtimer) + in (CPUtimer,time) end; + +fun end_timing (CPUtimer, {gc,sys,usr}) = + let open Time (*...for Time.toString, Time.+ and Time.- *) + val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer) + in "User " ^ toString (usr2-usr) ^ + " GC " ^ toString (gc2-gc) ^ + " All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^ + " secs" + handle Time => "" + end; + +fun check_timer timer = + let val {sys, usr, gc} = Timer.checkCPUTimer timer + in (sys, usr, gc) end; + + +(* SML basis library fixes *) + +structure TextIO = +struct + fun canInput _ = raise IO.Io {cause = Fail "undefined", function = "canInput", name = ""}; + open TextIO; +end; + (* bounded time execution *) diff -r 2b60e9b70a8c -r 6d2306b2376d src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Fri Nov 10 23:22:04 2006 +0100 +++ b/src/Pure/ML-Systems/polyml.ML Fri Nov 10 23:22:10 2006 +0100 @@ -1,7 +1,5 @@ (* Title: Pure/ML-Systems/polyml.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge Compatibility file for Poly/ML (version 4.0, 4.1, 4.1.x). *) @@ -50,7 +48,25 @@ (* compiler-independent timing functions *) -use "ML-Systems/cpu-timer-basis.ML"; +fun start_timing () = + let val CPUtimer = Timer.startCPUTimer(); + val time = Timer.checkCPUTimer(CPUtimer) + in (CPUtimer,time) end; + +fun end_timing (CPUtimer, {sys,usr}) = + let open Time (*...for Time.toString, Time.+ and Time.- *) + val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer) + in "User " ^ toString (usr2-usr) ^ + " All "^ toString (sys2-sys + usr2-usr) ^ + " secs" + handle Time => "" + end; + +fun check_timer timer = + let + val {sys, usr} = Timer.checkCPUTimer timer; + val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *) + in (sys, usr, gc) end; (* bounded time execution *) diff -r 2b60e9b70a8c -r 6d2306b2376d src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Fri Nov 10 23:22:04 2006 +0100 +++ b/src/Pure/ML-Systems/smlnj.ML Fri Nov 10 23:22:10 2006 +0100 @@ -1,25 +1,16 @@ (* Title: Pure/ML-Systems/smlnj.ML ID: $Id$ - Author: Carsten Clasohm and Markus Wenzel, TU Muenchen Compatibility file for Standard ML of New Jersey 110 or later. *) -(case #version_id (Compiler.version) of - [110, x] => if x >= 35 then use "ML-Systems/smlnj-compiler.ML" else () -| _ => ()); - (** ML system related **) (*low-level pointer equality*) -(*dummy version -- may get overridden in smlnj-ptreql.ML*) -fun pointer_eq (x:'a, y) = false; - -(case #version_id (Compiler.version) of - [110, x] => if x >= 49 then use "ML-Systems/smlnj-ptreql.ML" else () -| _ => ()); +CM.autoload "$smlnj/init/init.cmi"; +val pointer_eq = InlineT.ptreql; (* restore old-style character / string functions *) @@ -33,11 +24,11 @@ (* New Jersey ML parameters *) val _ = - (Compiler.Control.Print.printLength := 1000; - Compiler.Control.Print.printDepth := 350; - Compiler.Control.Print.stringDepth := 250; - Compiler.Control.Print.signatures := 2; - Compiler.Control.MC.matchRedundantError := false); + (Control.Print.printLength := 1000; + Control.Print.printDepth := 350; + Control.Print.stringDepth := 250; + Control.Print.signatures := 2; + Control.MC.matchRedundantError := false); (* Poly/ML emulation *) @@ -46,22 +37,36 @@ (*limit the printing depth -- divided by 2 for comparibility with Poly/ML*) fun print_depth n = - (Compiler.Control.Print.printDepth := n div 2; - Compiler.Control.Print.printLength := n); + (Control.Print.printDepth := n div 2; + Control.Print.printLength := n); (* compiler-independent timing functions *) -(case #version_id (Compiler.version) of - [110, x] => if x >= 44 - then use "ML-Systems/cpu-timer-basis.ML" - else use "ML-Systems/cpu-timer-gc.ML" -| _ => use "ML-Systems/cpu-timer-gc.ML"); +fun start_timing () = + let val CPUtimer = Timer.startCPUTimer(); + val time = Timer.checkCPUTimer(CPUtimer) + in (CPUtimer,time) end; + +fun end_timing (CPUtimer, {sys,usr}) = + let open Time (*...for Time.toString, Time.+ and Time.- *) + val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer) + in "User " ^ toString (usr2-usr) ^ + " All "^ toString (sys2-sys + usr2-usr) ^ + " secs" + handle Time => "" + end; + +fun check_timer timer = + let + val {sys, usr} = Timer.checkCPUTimer timer; + val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *) + in (sys, usr, gc) end; (*prompts*) fun ml_prompts p1 p2 = - (Compiler.Control.primaryPrompt := p1; Compiler.Control.secondaryPrompt := p2); + (Control.primaryPrompt := p1; Control.secondaryPrompt := p2); (*dummy implementation*) fun profile (n: int) f x = f x; @@ -72,22 +77,28 @@ (*dummy implementation*) fun print x = x; + (* toplevel pretty printing (see also Pure/install_pp.ML) *) -(case #version_id (Compiler.version) of - [110, x] => if x >= 44 - then use "ML-Systems/smlnj-pp-new.ML" - else use "ML-Systems/smlnj-pp-old.ML" -| _ => use "ML-Systems/smlnj-pp-old.ML"); +fun make_pp path pprint = + let + open PrettyPrint; -fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp; + fun pp pps obj = + pprint obj + (string pps, openHOVBox pps o Rel, + fn wd => break pps {nsp=wd, offset=0}, fn () => newline pps, + fn () => closeBox pps); + in (path, pp) end; + +fun install_pp (path, pp) = CompilerPPTable.install_pp path pp; (* ML command execution *) fun use_text (print, err) verbose txt = let - val ref out_orig = Compiler.Control.Print.out; + val ref out_orig = Control.Print.out; val out_buffer = ref ([]: string list); val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())}; @@ -95,10 +106,10 @@ let val str = implode (rev (! out_buffer)) in String.substring (str, 0, Int.max (0, size str - 1)) end; in - Compiler.Control.Print.out := out; - Compiler.Interact.useStream (TextIO.openString txt) handle exn => - (Compiler.Control.Print.out := out_orig; err (output ()); raise exn); - Compiler.Control.Print.out := out_orig; + Control.Print.out := out; + Backend.Interact.useStream (TextIO.openString txt) handle exn => + (Control.Print.out := out_orig; err (output ()); raise exn); + Control.Print.out := out_orig; if verbose then print (output ()) else () end; @@ -138,17 +149,26 @@ end; -(case #version_id (Compiler.version) of - [110, x] => if x >= 44 - then use "ML-Systems/smlnj-basis-compat.ML" - else () -| _ => ()); + +(* basis library fixes *) + +structure TextIO = +struct + open TextIO; + fun inputLine is = + (case TextIO.inputLine is of + SOME str => str + | NONE => "") + handle IO.Io _ => raise Interrupt; +end; (* bounded time execution *) -use "ML-Systems/smlnj-interrupt-timeout.ML"; +fun interrupt_timeout time f x = + TimeLimit.timeLimit time f x + handle TimeLimit.TimeOut => raise Interrupt; (** Signal handling: emulation of the Poly/ML Signal structure. Note that types @@ -214,7 +234,7 @@ (*Convert a process ID to a decimal string (chiefly for tracing)*) -fun string_of_pid pid = +fun string_of_pid pid = Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));