# HG changeset patch # User wenzelm # Date 1086433525 -7200 # Node ID 515fa02eee9a24735966e0b6da72ddc08446a8af # Parent 8b9a372b3e9008f05b9c4e8e2d7a77178157c6b4 obsolete; diff -r 8b9a372b3e90 -r 515fa02eee9a lib/scripts/run-mlworks --- a/lib/scripts/run-mlworks Fri Jun 04 11:51:31 2004 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,56 +0,0 @@ -#!/usr/bin/env bash -# -# $Id$ -# Author: Markus Wenzel, TU Muenchen -# License: GPL (GNU GENERAL PUBLIC LICENSE) -# -# MLWorks startup script (for 1.0r2 or later). - -export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE - - -## diagnostics - -function fail_out() -{ - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 -} - - -## prepare databases - -if [ -z "$INFILE" ]; then - EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" - MLWORKS="mlworks-basis -tty" -else - EXIT="" - MLWORKS="mlimage -load $INFILE -tty" -fi - -if [ -z "$OUTFILE" ]; then - COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' -else - COMMIT="fun commit () = (Shell.saveImage (\"$OUTFILE\", false); true);" - [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } -fi - - -## run it! - -MLTEXT="$EXIT $COMMIT $MLTEXT" -MLEXIT="commit();" - -if [ -z "$TERMINATE" ]; then - FEEDER_OPTS="" -else - FEEDER_OPTS="-q" -fi - -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ - { read FPID; "$ML_HOME"/$MLWORKS $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } -RC="$?" - -[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" - -exit "$RC" diff -r 8b9a372b3e90 -r 515fa02eee9a lib/scripts/run-smlnj-0.93 --- a/lib/scripts/run-smlnj-0.93 Fri Jun 04 11:51:31 2004 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,81 +0,0 @@ -#!/usr/bin/env bash -# -# $Id$ -# Author: Markus Wenzel, TU Muenchen -# License: GPL (GNU GENERAL PUBLIC LICENSE) -# -# SML/NJ startup script (for 0.93). - -export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE - - -## diagnostics - -function fail_out() -{ - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 -} - -function check_mlhome_file() -{ - if [ ! -f "$1" ]; then - echo "Unable to locate $1" >&2 - echo "Please check your ML_HOME setting!" >&2 - exit 2 - fi -} - - -## prepare databases - -if [ -z "$INFILE" ]; then - INFILE="$ML_HOME/sml" - check_mlhome_file "$INFILE" - EXIT="val exit: int -> unit = System.Unsafe.CInterface.exit;" -else - EXIT="" -fi - -MOVE="" - -if [ -z "$OUTFILE" ]; then - COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);' -else - if [ "$INFILE" -ef "$OUTFILE" ]; then - OUTDIR=$(dirname "$OUTFILE")/tmp - OUTFILE="$OUTDIR"/$(basename "$OUTFILE") - mkdir -p "$OUTDIR" || fail_out - MOVE=true - fi - [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } - COMMIT="fun commit () = not (exportML\"$OUTFILE\");" -fi - - -## run it! - -MLTEXT="$EXIT $COMMIT $MLTEXT" -MLEXIT="commit();" - -if [ -z "$TERMINATE" ]; then - FEEDER_OPTS="" -else - FEEDER_OPTS="-q" -fi - -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ - { read FPID; "$INFILE" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } -RC="$?" - - -## fix heap file - -[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" - -if [ -n "$MOVE" -a -f "$OUTFILE" ]; then - rm -f "$INFILE" || fail_out - mv "$OUTFILE" "$INFILE" || fail_out -fi - -exit "$RC" diff -r 8b9a372b3e90 -r 515fa02eee9a src/Pure/ML-Systems/mlworks.ML --- a/src/Pure/ML-Systems/mlworks.ML Fri Jun 04 11:51:31 2004 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,136 +0,0 @@ -(* Title: Pure/ML-Systems/mlworks.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1996 University of Cambridge - -Compatibility file for MLWorks version 1.0r2 or later. -*) - -(** ML system related **) - -(* restore old-style character / string functions *) - -val ord = SML90.ord; -val chr = SML90.chr; -val explode = SML90.explode; -val implode = SML90.implode; - - -(* MLWorks parameters *) - -val _ = - (MLWorks.Internal.Runtime.Event.stack_overflow_handler - (fn () => - let val max_stack = MLWorks.Internal.Runtime.Memory.max_stack_blocks - in max_stack := (!max_stack * 3) div 2 + 5; - print ("#### Increasing stack to " ^ Int.toString (64 * !max_stack) ^ - "KB\n") - end); - MLWorks.Internal.Runtime.Memory.gc_message_level := 10; - (*Is this of any use at all?*) - Shell.Options.set (Shell.Options.ValuePrinter.showExnDetails, true)); - - -(* Poly/ML emulation *) - -(*To exit the system with an exit code -- an alternative to ^D *) -fun exit 0 = (OS.Process.exit OS.Process.success): unit - | exit _ = OS.Process.exit OS.Process.failure; -fun quit () = exit 0; - -(*limit the printing depth*) -fun print_depth n = - let open Shell.Options - in set (ValuePrinter.maximumDepth, n div 2); - set (ValuePrinter.maximumSeqSize, n) - end; - -(*interface for toplevel pretty printers, see also Pure/install_pp.ML*) -(*n.a.*) -fun make_pp path pprint = (); -fun install_pp _ = (); - -(*prompts*) -(*n.a.??*) -fun ml_prompts p1 p2 = (); - - -(** Compiler-independent timing functions **) - -use "ML-Systems/cpu-timer-gc.ML" - -(* bounded time execution *) - -(* FIXME proper implementation available? *) - -structure TimeLimit : sig - exception TimeOut - val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b -end = struct - exception TimeOut - fun timeLimit t f x = - f x; -end; - -(* ML command execution *) - -(*Can one redirect 'use' directly to an instream?*) -fun use_text _ _ txt = - let - val tmp_name = OS.FileSys.tmpName (); - val tmp_file = TextIO.openOut tmp_name; - in - TextIO.output (tmp_file, txt); - TextIO.closeOut tmp_file; - use tmp_name; - OS.FileSys.remove tmp_name - end; - - - -(** interrupts **) (*Note: may get into race conditions*) - -exception Interrupt; - -MLWorks.Internal.Runtime.Event.interrupt_handler (fn () => raise Interrupt); - -fun ignore_interrupt f x = f x; -fun raise_interrupt f x = f x; - - - -(** OS related **) - -(* system command execution *) - -(*execute Unix command which doesn't take any input from stdin and - sends its output to stdout; could be done more easily by Unix.execute, - but that function doesn't use the PATH*) -fun execute command = - let - val tmp_name = OS.FileSys.tmpName (); - val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name); - val result = TextIO.inputAll is; - in - TextIO.closeIn is; - OS.FileSys.remove tmp_name; - result - end; - -(*plain version; with return code*) -fun system cmd = - if OS.Process.system cmd = OS.Process.success then 0 else 1; - - -(* file handling *) - -(*get time of last modification*) -fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => ""; - - -(* getenv *) - -fun getenv var = - (case OS.Process.getEnv var of - NONE => "" - | SOME txt => txt); diff -r 8b9a372b3e90 -r 515fa02eee9a src/Pure/ML-Systems/polyml-3.x.ML --- a/src/Pure/ML-Systems/polyml-3.x.ML Fri Jun 04 11:51:31 2004 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,132 +0,0 @@ -(* 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 (versions 2.x and 3.x). -*) - -open PolyML ExtendedIO; - -(*needs the Basis Library emulation*) -use "basis.ML"; - - -structure String = -struct - fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j) - handle Substring => raise Subscript - fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1)) - handle Subscript => false - fun str (s : string) = s; - fun translate f s = implode (map f (explode s)); -end; - - -(** ML system related **) - -(** Compiler-independent timing functions **) - -(*Note start point for timing*) -fun startTiming() = System.processtime (); - -(*Finish timing and return string*) -fun endTiming before = - "User + GC: " ^ - makestring (real (System.processtime () - before) / 10.0) ^ - " secs"; - - -(* prompts *) - -fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); - - -(* toplevel pretty printing (see also Pure/install_pp.ML) *) - -fun make_pp _ pprint (str, blk, brk, en) obj = - pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0), - fn () => brk (99999, 0), en); - - -(* ML command execution -- 'eval' *) - -local - -fun drop_last [] = [] - | drop_last [x] = [] - | drop_last (x :: xs) = x :: drop_last xs; - -val drop_last_char = implode o drop_last o explode; - -in - -fun use_text (print, err) verbose txt = - let - val in_buffer = ref (explode txt); - val out_buffer = ref ([]: string list); - fun output () = drop_last_char (implode (rev (! out_buffer))); - - fun get () = - (case ! in_buffer of - [] => "" - | c :: cs => (in_buffer := cs; c)); - fun put s = out_buffer := s :: ! out_buffer; - - fun exec () = - (case ! in_buffer of - [] => () - | _ => (PolyML.compiler (get, put) (); exec ())); - in - exec () handle exn => (err (output ()); raise exn); - if verbose then print (output ()) else () - end; - - - -(** interrupts **) (*Note: may get into race conditions*) - -fun ignore_interrupt f x = f x; -fun raise_interrupt f x = f x; - - - -(** OS related **) - -(* system command execution *) - -(*execute Unix command which doesn't take any input from stdin and - sends its output to stdout*) -fun execute command = - let - val (is, os) = ExtendedIO.execute command; - val _ = close_out os; - val result = input (is, 999999); - in close_in is; result end; - -fun system cmd = (print (execute cmd); 0); (* FIXME rc not available *) - - -(* file handling *) - -(*get time of last modification*) -fun file_info name = Int.toString (System.filedate name) handle _ => ""; - -structure OS = -struct - structure FileSys = - struct - val chDir = PolyML.cd; - fun remove name = (execute ("rm " ^ name); ()); - fun getDir () = drop_last_char (execute "pwd"); - end; -end; - - -(* getenv *) - -fun getenv var = drop_last_char - (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'")); - - -end; diff -r 8b9a372b3e90 -r 515fa02eee9a src/Pure/ML-Systems/smlnj-0.93.ML --- a/src/Pure/ML-Systems/smlnj-0.93.ML Fri Jun 04 11:51:31 2004 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,195 +0,0 @@ -(* Title: Pure/ML-Systems/smlnj-0.93.ML - ID: $Id$ - Author: Carsten Clasohm, TU Muenchen - Copyright 1996 TU Muenchen - -Compatibility file for Standard ML of New Jersey version 0.93. -*) - -(*needs the Basis Library emulation*) -use "basis.ML"; - -structure String = -struct - fun substring args = String.substring args - handle String.Substring => raise Subscript; - fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1)) - handle Subscript => false; - fun str (s : string) = s; - fun translate f s = implode (map f (explode s)); -end; - - - -(** ML system related **) - -(* New Jersey ML parameters *) - -System.Control.Runtime.gcmessages := 0; - - -(* Poly/ML emulation *) - -fun quit () = exit 0; - -(*limit the printing depth -- divided by 2 for comparibility with Poly/ML*) -fun print_depth n = - (System.Control.Print.printDepth := n div 2; - System.Control.Print.printLength := n); - - - -(* timing *) - -(*Note start point for timing*) -fun startTiming() = System.Timer.start_timer(); - -(*Finish timing and return string*) -local - (*print microseconds, suppressing trailing zeroes*) - fun umakestring 0 = "" - | umakestring n = - chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000)); - - fun string_of_time (System.Timer.TIME {sec, usec}) = - makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec) - -in - -fun endTiming start = - let val nongc = System.Timer.check_timer(start) - and gc = System.Timer.check_timer_gc(start); - val both = System.Timer.add_time(nongc, gc) - in "Non GC " ^ string_of_time nongc ^ - " GC " ^ string_of_time gc ^ - " both "^ string_of_time both ^ " secs\n" - end -end; - - -(* prompts *) - -fun ml_prompts p1 p2 = (); - - -(* toplevel pretty printing (see also Pure/install_pp.ML) *) - -fun make_pp path pprint = - let - open System.PrettyPrint; - - fun pp pps obj = - pprint obj - (add_string pps, begin_block pps INCONSISTENT, - fn wd => add_break pps (wd, 0), fn () => add_newline pps, - fn () => end_block pps); - in - (path, pp) - end; - -fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp; - - -(* ML command execution *) - -fun use_text _ _ = System.Compile.use_stream o open_string; - - - -(** interrupts **) - -exception Interrupt; - -local - -fun capture f x = ((f x): unit; NONE) handle exn => SOME exn; - -fun release NONE = () - | release (SOME exn) = raise exn; - -structure Signals = System.Signals; - -in - -fun ignore_interrupt f x = - let - val old_handler = Signals.inqHandler Signals.SIGINT; - val _ = Signals.setHandler (Signals.SIGINT, SOME #2); - val result = capture f x; - val _ = Signals.setHandler (Signals.SIGINT, old_handler); - in release result end; - -fun raise_interrupt f x = - let - val interrupted = ref false; - val result = ref NONE; - val old_handler = Signals.inqHandler Signals.SIGINT; - in - callcc (fn cont => - (Signals.setHandler (Signals.SIGINT, SOME (fn _ => (interrupted := true; cont))); - result := capture f x)); - Signals.setHandler (Signals.SIGINT, old_handler); - if ! interrupted then raise Interrupt else release (! result) - end; - -end; - - -(** OS related **) - -(* system command execution *) - -(*execute Unix command which doesn't take any input from stdin and - sends its output to stdout; could be done more easily by IO.execute, - but that function seems to be buggy in SML/NJ 0.93*) -fun execute command = - let - val tmp_name = "/tmp/isabelle-execute"; - val is = (System.system (command ^ " > " ^ tmp_name); open_in tmp_name); - val result = input (is, 999999); - in - close_in is; - System.Unsafe.SysIO.unlink tmp_name; - result - end; - -(*plain version; with return code*) -fun system cmd = System.system cmd div 256; - - -(* file handling *) - -(*get time of last modification*) -local - open System.Timer System.Unsafe.SysIO; -in - fun file_info name = makestring (mtime (PATH name)) handle _ => ""; -end; - -structure OS = -struct - structure FileSys = - struct - val chDir = System.Directory.cd; - val remove = System.Unsafe.SysIO.unlink; - val getDir = System.Directory.getWD; - end; -end; - -(*redefine to flush its output immediately -- temporary patch suggested - by Kim Dam Petersen*) (* FIXME !? *) -val output = fn (s, t) => (output (s, t); flush_out s); - - -(* getenv *) - -local - fun drop_last [] = [] - | drop_last [x] = [] - | drop_last (x :: xs) = x :: drop_last xs; - - val drop_last_char = implode o drop_last o explode; -in - fun getenv var = drop_last_char - (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'")); -end; diff -r 8b9a372b3e90 -r 515fa02eee9a src/Pure/basis.ML --- a/src/Pure/basis.ML Fri Jun 04 11:51:31 2004 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,192 +0,0 @@ -(* Title: Pure/basis.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Basis Library emulation. Needed for Poly/ML and Standard ML of New -Jersey version 0.93 to 1.08. Full compatibility cannot be obtained -using a file: what about char constants? -*) - -exception Subscript; - -structure Bool = - struct - fun toString true = "true" - | toString false = "false" - end; - - -structure Option = - struct - exception Option - - datatype 'a option = NONE | SOME of 'a - - fun getOpt (SOME v, _) = v - | getOpt (NONE, a) = a - - fun isSome (SOME _) = true - | isSome NONE = false - - fun valOf (SOME v) = v - | valOf NONE = raise Option - end; - - -structure Int = - struct - type int = int - fun toString (i: int) = makestring i; - fun max (x, y) = if x < y then y else x : int; - fun min (x, y) = if x < y then x else y : int; - end; - - -structure Real = - struct - fun toString (x: real) = makestring x; - fun max (x, y) = if x < y then y else x : real; - fun min (x, y) = if x < y then x else y : real; - val real = real; - val floor = floor; - fun ceil x = ~1 - floor (~ (x + 1.0)); - fun round x = floor (x + 0.5); (*does not do round-to-nearest*) - fun trunc x = if x < 0.0 then ceil x else floor x; - end; - - -structure List = - struct - exception Empty - - fun last [] = raise Empty - | last [x] = x - | last (x::xs) = last xs; - - fun nth (xs, n) = - let fun h [] _ = raise Subscript - | h (x::xs) n = if n=0 then x else h xs (n-1) - in if n<0 then raise Subscript else h xs n end; - - fun drop (xs, n) = - let fun h xs 0 = xs - | h [] n = raise Subscript - | h (x::xs) n = h xs (n-1) - in if n<0 then raise Subscript else h xs n end; - - fun take (xs, n) = - let fun h xs 0 = [] - | h [] n = raise Subscript - | h (x::xs) n = x :: h xs (n-1) - in if n<0 then raise Subscript else h xs n end; - - fun concat [] = [] - | concat (l::ls) = l @ concat ls; - - fun mapPartial f [] = [] - | mapPartial f (x::xs) = - (case f x of Option.NONE => mapPartial f xs - | Option.SOME y => y :: mapPartial f xs); - - fun find _ [] = Option.NONE - | find p (x :: xs) = if p x then Option.SOME x else find p xs; - - - (*copy the list preserving elements that satisfy the predicate*) - fun filter p [] = [] - | filter p (x :: xs) = if p x then x :: filter p xs else filter p xs; - - (*Partition list into elements that satisfy predicate and those that don't. - Preserves order of elements in both lists.*) - fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) = - let fun part ([], answer) = answer - | part (x::xs, (ys, ns)) = if p(x) - then part (xs, (x::ys, ns)) - else part (xs, (ys, x::ns)) - in part (rev ys, ([], [])) end; - - end; - - -structure ListPair = - struct - fun zip ([], []) = [] - | zip (x::xs,y::ys) = (x,y) :: zip(xs,ys); - - fun unzip [] = ([],[]) - | unzip((x,y)::pairs) = - let val (xs,ys) = unzip pairs - in (x::xs, y::ys) end; - - fun map f ([], []) = [] - | map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys); - - fun exists p = - let fun boolf ([], []) = false - | boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys) - in boolf end; - - fun all p = - let fun boolf ([], []) = true - | boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys) - in boolf end; - end; - - -structure TextIO = - struct - type instream = instream - and outstream = outstream - exception Io of {name: string, function: string, cause: exn} - val stdIn = std_in - val stdOut = std_out - val stdErr = std_out - val openIn = open_in - val openAppend = open_append - val openOut = open_out - val closeIn = close_in - val closeOut = close_out - val inputN = input - val inputAll = fn is => inputN (is, 999999) - val inputLine = input_line - val endOfStream = end_of_stream - val output = output - val flushOut = flush_out - end; - - -fun print s = (output (std_out, s); flush_out std_out); - - -structure General = -struct - -local - fun raised name = "exception " ^ name ^ " raised"; - fun raised_msg name msg = raised name ^ ": " ^ msg; -in - fun exnMessage Match = raised_msg "Match" "nonexhaustive match failure" - | exnMessage Bind = raised_msg "Bind" "nonexhaustive binding failure" - | exnMessage (Io msg) = "I/O error: " ^ msg - | exnMessage Neg = raised "Neg" - | exnMessage Sum = raised "Sum" - | exnMessage Diff = raised "Diff" - | exnMessage Prod = raised "Prod" - | exnMessage Quot = raised "Quot" - | exnMessage Abs = raised "Abs" - | exnMessage Div = raised "Div" - | exnMessage Mod = raised "Mod" - | exnMessage Floor = raised "Floor" - | exnMessage Sqrt = raised "Sqrt" - | exnMessage Exp = raised "Exp" - | exnMessage Ln = raised "Ln" - | exnMessage Ord = raised "Ord" - | exnMessage Subscript = raised_msg "Subscript " "subscript out of bounds" - | exnMessage Option.Option = raised "Option.Option" - | exnMessage List.Empty = raised "List.Empty" - | exnMessage (TextIO.Io {name, ...}) = raised_msg "TextIO.Io" name - | exnMessage exn = raised "???"; -end; - -end;