1.1 --- a/lib/scripts/run-mlworks Fri Jun 04 11:51:31 2004 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,56 +0,0 @@
1.4 -#!/usr/bin/env bash
1.5 -#
1.6 -# $Id$
1.7 -# Author: Markus Wenzel, TU Muenchen
1.8 -# License: GPL (GNU GENERAL PUBLIC LICENSE)
1.9 -#
1.10 -# MLWorks startup script (for 1.0r2 or later).
1.11 -
1.12 -export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
1.13 -
1.14 -
1.15 -## diagnostics
1.16 -
1.17 -function fail_out()
1.18 -{
1.19 - echo "Unable to create output heap file: \"$OUTFILE\"" >&2
1.20 - exit 2
1.21 -}
1.22 -
1.23 -
1.24 -## prepare databases
1.25 -
1.26 -if [ -z "$INFILE" ]; then
1.27 - EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
1.28 - MLWORKS="mlworks-basis -tty"
1.29 -else
1.30 - EXIT=""
1.31 - MLWORKS="mlimage -load $INFILE -tty"
1.32 -fi
1.33 -
1.34 -if [ -z "$OUTFILE" ]; then
1.35 - COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
1.36 -else
1.37 - COMMIT="fun commit () = (Shell.saveImage (\"$OUTFILE\", false); true);"
1.38 - [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
1.39 -fi
1.40 -
1.41 -
1.42 -## run it!
1.43 -
1.44 -MLTEXT="$EXIT $COMMIT $MLTEXT"
1.45 -MLEXIT="commit();"
1.46 -
1.47 -if [ -z "$TERMINATE" ]; then
1.48 - FEEDER_OPTS=""
1.49 -else
1.50 - FEEDER_OPTS="-q"
1.51 -fi
1.52 -
1.53 -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
1.54 - { read FPID; "$ML_HOME"/$MLWORKS $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
1.55 -RC="$?"
1.56 -
1.57 -[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
1.58 -
1.59 -exit "$RC"
2.1 --- a/lib/scripts/run-smlnj-0.93 Fri Jun 04 11:51:31 2004 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,81 +0,0 @@
2.4 -#!/usr/bin/env bash
2.5 -#
2.6 -# $Id$
2.7 -# Author: Markus Wenzel, TU Muenchen
2.8 -# License: GPL (GNU GENERAL PUBLIC LICENSE)
2.9 -#
2.10 -# SML/NJ startup script (for 0.93).
2.11 -
2.12 -export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
2.13 -
2.14 -
2.15 -## diagnostics
2.16 -
2.17 -function fail_out()
2.18 -{
2.19 - echo "Unable to create output heap file: \"$OUTFILE\"" >&2
2.20 - exit 2
2.21 -}
2.22 -
2.23 -function check_mlhome_file()
2.24 -{
2.25 - if [ ! -f "$1" ]; then
2.26 - echo "Unable to locate $1" >&2
2.27 - echo "Please check your ML_HOME setting!" >&2
2.28 - exit 2
2.29 - fi
2.30 -}
2.31 -
2.32 -
2.33 -## prepare databases
2.34 -
2.35 -if [ -z "$INFILE" ]; then
2.36 - INFILE="$ML_HOME/sml"
2.37 - check_mlhome_file "$INFILE"
2.38 - EXIT="val exit: int -> unit = System.Unsafe.CInterface.exit;"
2.39 -else
2.40 - EXIT=""
2.41 -fi
2.42 -
2.43 -MOVE=""
2.44 -
2.45 -if [ -z "$OUTFILE" ]; then
2.46 - COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);'
2.47 -else
2.48 - if [ "$INFILE" -ef "$OUTFILE" ]; then
2.49 - OUTDIR=$(dirname "$OUTFILE")/tmp
2.50 - OUTFILE="$OUTDIR"/$(basename "$OUTFILE")
2.51 - mkdir -p "$OUTDIR" || fail_out
2.52 - MOVE=true
2.53 - fi
2.54 - [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
2.55 - COMMIT="fun commit () = not (exportML\"$OUTFILE\");"
2.56 -fi
2.57 -
2.58 -
2.59 -## run it!
2.60 -
2.61 -MLTEXT="$EXIT $COMMIT $MLTEXT"
2.62 -MLEXIT="commit();"
2.63 -
2.64 -if [ -z "$TERMINATE" ]; then
2.65 - FEEDER_OPTS=""
2.66 -else
2.67 - FEEDER_OPTS="-q"
2.68 -fi
2.69 -
2.70 -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
2.71 - { read FPID; "$INFILE" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
2.72 -RC="$?"
2.73 -
2.74 -
2.75 -## fix heap file
2.76 -
2.77 -[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
2.78 -
2.79 -if [ -n "$MOVE" -a -f "$OUTFILE" ]; then
2.80 - rm -f "$INFILE" || fail_out
2.81 - mv "$OUTFILE" "$INFILE" || fail_out
2.82 -fi
2.83 -
2.84 -exit "$RC"
3.1 --- a/src/Pure/ML-Systems/mlworks.ML Fri Jun 04 11:51:31 2004 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,136 +0,0 @@
3.4 -(* Title: Pure/ML-Systems/mlworks.ML
3.5 - ID: $Id$
3.6 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
3.7 - Copyright 1996 University of Cambridge
3.8 -
3.9 -Compatibility file for MLWorks version 1.0r2 or later.
3.10 -*)
3.11 -
3.12 -(** ML system related **)
3.13 -
3.14 -(* restore old-style character / string functions *)
3.15 -
3.16 -val ord = SML90.ord;
3.17 -val chr = SML90.chr;
3.18 -val explode = SML90.explode;
3.19 -val implode = SML90.implode;
3.20 -
3.21 -
3.22 -(* MLWorks parameters *)
3.23 -
3.24 -val _ =
3.25 - (MLWorks.Internal.Runtime.Event.stack_overflow_handler
3.26 - (fn () =>
3.27 - let val max_stack = MLWorks.Internal.Runtime.Memory.max_stack_blocks
3.28 - in max_stack := (!max_stack * 3) div 2 + 5;
3.29 - print ("#### Increasing stack to " ^ Int.toString (64 * !max_stack) ^
3.30 - "KB\n")
3.31 - end);
3.32 - MLWorks.Internal.Runtime.Memory.gc_message_level := 10;
3.33 - (*Is this of any use at all?*)
3.34 - Shell.Options.set (Shell.Options.ValuePrinter.showExnDetails, true));
3.35 -
3.36 -
3.37 -(* Poly/ML emulation *)
3.38 -
3.39 -(*To exit the system with an exit code -- an alternative to ^D *)
3.40 -fun exit 0 = (OS.Process.exit OS.Process.success): unit
3.41 - | exit _ = OS.Process.exit OS.Process.failure;
3.42 -fun quit () = exit 0;
3.43 -
3.44 -(*limit the printing depth*)
3.45 -fun print_depth n =
3.46 - let open Shell.Options
3.47 - in set (ValuePrinter.maximumDepth, n div 2);
3.48 - set (ValuePrinter.maximumSeqSize, n)
3.49 - end;
3.50 -
3.51 -(*interface for toplevel pretty printers, see also Pure/install_pp.ML*)
3.52 -(*n.a.*)
3.53 -fun make_pp path pprint = ();
3.54 -fun install_pp _ = ();
3.55 -
3.56 -(*prompts*)
3.57 -(*n.a.??*)
3.58 -fun ml_prompts p1 p2 = ();
3.59 -
3.60 -
3.61 -(** Compiler-independent timing functions **)
3.62 -
3.63 -use "ML-Systems/cpu-timer-gc.ML"
3.64 -
3.65 -(* bounded time execution *)
3.66 -
3.67 -(* FIXME proper implementation available? *)
3.68 -
3.69 -structure TimeLimit : sig
3.70 - exception TimeOut
3.71 - val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
3.72 -end = struct
3.73 - exception TimeOut
3.74 - fun timeLimit t f x =
3.75 - f x;
3.76 -end;
3.77 -
3.78 -(* ML command execution *)
3.79 -
3.80 -(*Can one redirect 'use' directly to an instream?*)
3.81 -fun use_text _ _ txt =
3.82 - let
3.83 - val tmp_name = OS.FileSys.tmpName ();
3.84 - val tmp_file = TextIO.openOut tmp_name;
3.85 - in
3.86 - TextIO.output (tmp_file, txt);
3.87 - TextIO.closeOut tmp_file;
3.88 - use tmp_name;
3.89 - OS.FileSys.remove tmp_name
3.90 - end;
3.91 -
3.92 -
3.93 -
3.94 -(** interrupts **) (*Note: may get into race conditions*)
3.95 -
3.96 -exception Interrupt;
3.97 -
3.98 -MLWorks.Internal.Runtime.Event.interrupt_handler (fn () => raise Interrupt);
3.99 -
3.100 -fun ignore_interrupt f x = f x;
3.101 -fun raise_interrupt f x = f x;
3.102 -
3.103 -
3.104 -
3.105 -(** OS related **)
3.106 -
3.107 -(* system command execution *)
3.108 -
3.109 -(*execute Unix command which doesn't take any input from stdin and
3.110 - sends its output to stdout; could be done more easily by Unix.execute,
3.111 - but that function doesn't use the PATH*)
3.112 -fun execute command =
3.113 - let
3.114 - val tmp_name = OS.FileSys.tmpName ();
3.115 - val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
3.116 - val result = TextIO.inputAll is;
3.117 - in
3.118 - TextIO.closeIn is;
3.119 - OS.FileSys.remove tmp_name;
3.120 - result
3.121 - end;
3.122 -
3.123 -(*plain version; with return code*)
3.124 -fun system cmd =
3.125 - if OS.Process.system cmd = OS.Process.success then 0 else 1;
3.126 -
3.127 -
3.128 -(* file handling *)
3.129 -
3.130 -(*get time of last modification*)
3.131 -fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
3.132 -
3.133 -
3.134 -(* getenv *)
3.135 -
3.136 -fun getenv var =
3.137 - (case OS.Process.getEnv var of
3.138 - NONE => ""
3.139 - | SOME txt => txt);
4.1 --- a/src/Pure/ML-Systems/polyml-3.x.ML Fri Jun 04 11:51:31 2004 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,132 +0,0 @@
4.4 -(* Title: Pure/ML-Systems/polyml.ML
4.5 - ID: $Id$
4.6 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4.7 - Copyright 1991 University of Cambridge
4.8 -
4.9 -Compatibility file for Poly/ML (versions 2.x and 3.x).
4.10 -*)
4.11 -
4.12 -open PolyML ExtendedIO;
4.13 -
4.14 -(*needs the Basis Library emulation*)
4.15 -use "basis.ML";
4.16 -
4.17 -
4.18 -structure String =
4.19 -struct
4.20 - fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j)
4.21 - handle Substring => raise Subscript
4.22 - fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1))
4.23 - handle Subscript => false
4.24 - fun str (s : string) = s;
4.25 - fun translate f s = implode (map f (explode s));
4.26 -end;
4.27 -
4.28 -
4.29 -(** ML system related **)
4.30 -
4.31 -(** Compiler-independent timing functions **)
4.32 -
4.33 -(*Note start point for timing*)
4.34 -fun startTiming() = System.processtime ();
4.35 -
4.36 -(*Finish timing and return string*)
4.37 -fun endTiming before =
4.38 - "User + GC: " ^
4.39 - makestring (real (System.processtime () - before) / 10.0) ^
4.40 - " secs";
4.41 -
4.42 -
4.43 -(* prompts *)
4.44 -
4.45 -fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
4.46 -
4.47 -
4.48 -(* toplevel pretty printing (see also Pure/install_pp.ML) *)
4.49 -
4.50 -fun make_pp _ pprint (str, blk, brk, en) obj =
4.51 - pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
4.52 - fn () => brk (99999, 0), en);
4.53 -
4.54 -
4.55 -(* ML command execution -- 'eval' *)
4.56 -
4.57 -local
4.58 -
4.59 -fun drop_last [] = []
4.60 - | drop_last [x] = []
4.61 - | drop_last (x :: xs) = x :: drop_last xs;
4.62 -
4.63 -val drop_last_char = implode o drop_last o explode;
4.64 -
4.65 -in
4.66 -
4.67 -fun use_text (print, err) verbose txt =
4.68 - let
4.69 - val in_buffer = ref (explode txt);
4.70 - val out_buffer = ref ([]: string list);
4.71 - fun output () = drop_last_char (implode (rev (! out_buffer)));
4.72 -
4.73 - fun get () =
4.74 - (case ! in_buffer of
4.75 - [] => ""
4.76 - | c :: cs => (in_buffer := cs; c));
4.77 - fun put s = out_buffer := s :: ! out_buffer;
4.78 -
4.79 - fun exec () =
4.80 - (case ! in_buffer of
4.81 - [] => ()
4.82 - | _ => (PolyML.compiler (get, put) (); exec ()));
4.83 - in
4.84 - exec () handle exn => (err (output ()); raise exn);
4.85 - if verbose then print (output ()) else ()
4.86 - end;
4.87 -
4.88 -
4.89 -
4.90 -(** interrupts **) (*Note: may get into race conditions*)
4.91 -
4.92 -fun ignore_interrupt f x = f x;
4.93 -fun raise_interrupt f x = f x;
4.94 -
4.95 -
4.96 -
4.97 -(** OS related **)
4.98 -
4.99 -(* system command execution *)
4.100 -
4.101 -(*execute Unix command which doesn't take any input from stdin and
4.102 - sends its output to stdout*)
4.103 -fun execute command =
4.104 - let
4.105 - val (is, os) = ExtendedIO.execute command;
4.106 - val _ = close_out os;
4.107 - val result = input (is, 999999);
4.108 - in close_in is; result end;
4.109 -
4.110 -fun system cmd = (print (execute cmd); 0); (* FIXME rc not available *)
4.111 -
4.112 -
4.113 -(* file handling *)
4.114 -
4.115 -(*get time of last modification*)
4.116 -fun file_info name = Int.toString (System.filedate name) handle _ => "";
4.117 -
4.118 -structure OS =
4.119 -struct
4.120 - structure FileSys =
4.121 - struct
4.122 - val chDir = PolyML.cd;
4.123 - fun remove name = (execute ("rm " ^ name); ());
4.124 - fun getDir () = drop_last_char (execute "pwd");
4.125 - end;
4.126 -end;
4.127 -
4.128 -
4.129 -(* getenv *)
4.130 -
4.131 -fun getenv var = drop_last_char
4.132 - (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
4.133 -
4.134 -
4.135 -end;
5.1 --- a/src/Pure/ML-Systems/smlnj-0.93.ML Fri Jun 04 11:51:31 2004 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,195 +0,0 @@
5.4 -(* Title: Pure/ML-Systems/smlnj-0.93.ML
5.5 - ID: $Id$
5.6 - Author: Carsten Clasohm, TU Muenchen
5.7 - Copyright 1996 TU Muenchen
5.8 -
5.9 -Compatibility file for Standard ML of New Jersey version 0.93.
5.10 -*)
5.11 -
5.12 -(*needs the Basis Library emulation*)
5.13 -use "basis.ML";
5.14 -
5.15 -structure String =
5.16 -struct
5.17 - fun substring args = String.substring args
5.18 - handle String.Substring => raise Subscript;
5.19 - fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1))
5.20 - handle Subscript => false;
5.21 - fun str (s : string) = s;
5.22 - fun translate f s = implode (map f (explode s));
5.23 -end;
5.24 -
5.25 -
5.26 -
5.27 -(** ML system related **)
5.28 -
5.29 -(* New Jersey ML parameters *)
5.30 -
5.31 -System.Control.Runtime.gcmessages := 0;
5.32 -
5.33 -
5.34 -(* Poly/ML emulation *)
5.35 -
5.36 -fun quit () = exit 0;
5.37 -
5.38 -(*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
5.39 -fun print_depth n =
5.40 - (System.Control.Print.printDepth := n div 2;
5.41 - System.Control.Print.printLength := n);
5.42 -
5.43 -
5.44 -
5.45 -(* timing *)
5.46 -
5.47 -(*Note start point for timing*)
5.48 -fun startTiming() = System.Timer.start_timer();
5.49 -
5.50 -(*Finish timing and return string*)
5.51 -local
5.52 - (*print microseconds, suppressing trailing zeroes*)
5.53 - fun umakestring 0 = ""
5.54 - | umakestring n =
5.55 - chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000));
5.56 -
5.57 - fun string_of_time (System.Timer.TIME {sec, usec}) =
5.58 - makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
5.59 -
5.60 -in
5.61 -
5.62 -fun endTiming start =
5.63 - let val nongc = System.Timer.check_timer(start)
5.64 - and gc = System.Timer.check_timer_gc(start);
5.65 - val both = System.Timer.add_time(nongc, gc)
5.66 - in "Non GC " ^ string_of_time nongc ^
5.67 - " GC " ^ string_of_time gc ^
5.68 - " both "^ string_of_time both ^ " secs\n"
5.69 - end
5.70 -end;
5.71 -
5.72 -
5.73 -(* prompts *)
5.74 -
5.75 -fun ml_prompts p1 p2 = ();
5.76 -
5.77 -
5.78 -(* toplevel pretty printing (see also Pure/install_pp.ML) *)
5.79 -
5.80 -fun make_pp path pprint =
5.81 - let
5.82 - open System.PrettyPrint;
5.83 -
5.84 - fun pp pps obj =
5.85 - pprint obj
5.86 - (add_string pps, begin_block pps INCONSISTENT,
5.87 - fn wd => add_break pps (wd, 0), fn () => add_newline pps,
5.88 - fn () => end_block pps);
5.89 - in
5.90 - (path, pp)
5.91 - end;
5.92 -
5.93 -fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
5.94 -
5.95 -
5.96 -(* ML command execution *)
5.97 -
5.98 -fun use_text _ _ = System.Compile.use_stream o open_string;
5.99 -
5.100 -
5.101 -
5.102 -(** interrupts **)
5.103 -
5.104 -exception Interrupt;
5.105 -
5.106 -local
5.107 -
5.108 -fun capture f x = ((f x): unit; NONE) handle exn => SOME exn;
5.109 -
5.110 -fun release NONE = ()
5.111 - | release (SOME exn) = raise exn;
5.112 -
5.113 -structure Signals = System.Signals;
5.114 -
5.115 -in
5.116 -
5.117 -fun ignore_interrupt f x =
5.118 - let
5.119 - val old_handler = Signals.inqHandler Signals.SIGINT;
5.120 - val _ = Signals.setHandler (Signals.SIGINT, SOME #2);
5.121 - val result = capture f x;
5.122 - val _ = Signals.setHandler (Signals.SIGINT, old_handler);
5.123 - in release result end;
5.124 -
5.125 -fun raise_interrupt f x =
5.126 - let
5.127 - val interrupted = ref false;
5.128 - val result = ref NONE;
5.129 - val old_handler = Signals.inqHandler Signals.SIGINT;
5.130 - in
5.131 - callcc (fn cont =>
5.132 - (Signals.setHandler (Signals.SIGINT, SOME (fn _ => (interrupted := true; cont)));
5.133 - result := capture f x));
5.134 - Signals.setHandler (Signals.SIGINT, old_handler);
5.135 - if ! interrupted then raise Interrupt else release (! result)
5.136 - end;
5.137 -
5.138 -end;
5.139 -
5.140 -
5.141 -(** OS related **)
5.142 -
5.143 -(* system command execution *)
5.144 -
5.145 -(*execute Unix command which doesn't take any input from stdin and
5.146 - sends its output to stdout; could be done more easily by IO.execute,
5.147 - but that function seems to be buggy in SML/NJ 0.93*)
5.148 -fun execute command =
5.149 - let
5.150 - val tmp_name = "/tmp/isabelle-execute";
5.151 - val is = (System.system (command ^ " > " ^ tmp_name); open_in tmp_name);
5.152 - val result = input (is, 999999);
5.153 - in
5.154 - close_in is;
5.155 - System.Unsafe.SysIO.unlink tmp_name;
5.156 - result
5.157 - end;
5.158 -
5.159 -(*plain version; with return code*)
5.160 -fun system cmd = System.system cmd div 256;
5.161 -
5.162 -
5.163 -(* file handling *)
5.164 -
5.165 -(*get time of last modification*)
5.166 -local
5.167 - open System.Timer System.Unsafe.SysIO;
5.168 -in
5.169 - fun file_info name = makestring (mtime (PATH name)) handle _ => "";
5.170 -end;
5.171 -
5.172 -structure OS =
5.173 -struct
5.174 - structure FileSys =
5.175 - struct
5.176 - val chDir = System.Directory.cd;
5.177 - val remove = System.Unsafe.SysIO.unlink;
5.178 - val getDir = System.Directory.getWD;
5.179 - end;
5.180 -end;
5.181 -
5.182 -(*redefine to flush its output immediately -- temporary patch suggested
5.183 - by Kim Dam Petersen*) (* FIXME !? *)
5.184 -val output = fn (s, t) => (output (s, t); flush_out s);
5.185 -
5.186 -
5.187 -(* getenv *)
5.188 -
5.189 -local
5.190 - fun drop_last [] = []
5.191 - | drop_last [x] = []
5.192 - | drop_last (x :: xs) = x :: drop_last xs;
5.193 -
5.194 - val drop_last_char = implode o drop_last o explode;
5.195 -in
5.196 - fun getenv var = drop_last_char
5.197 - (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
5.198 -end;
6.1 --- a/src/Pure/basis.ML Fri Jun 04 11:51:31 2004 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,192 +0,0 @@
6.4 -(* Title: Pure/basis.ML
6.5 - ID: $Id$
6.6 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
6.7 - Copyright 1993 University of Cambridge
6.8 -
6.9 -Basis Library emulation. Needed for Poly/ML and Standard ML of New
6.10 -Jersey version 0.93 to 1.08. Full compatibility cannot be obtained
6.11 -using a file: what about char constants?
6.12 -*)
6.13 -
6.14 -exception Subscript;
6.15 -
6.16 -structure Bool =
6.17 - struct
6.18 - fun toString true = "true"
6.19 - | toString false = "false"
6.20 - end;
6.21 -
6.22 -
6.23 -structure Option =
6.24 - struct
6.25 - exception Option
6.26 -
6.27 - datatype 'a option = NONE | SOME of 'a
6.28 -
6.29 - fun getOpt (SOME v, _) = v
6.30 - | getOpt (NONE, a) = a
6.31 -
6.32 - fun isSome (SOME _) = true
6.33 - | isSome NONE = false
6.34 -
6.35 - fun valOf (SOME v) = v
6.36 - | valOf NONE = raise Option
6.37 - end;
6.38 -
6.39 -
6.40 -structure Int =
6.41 - struct
6.42 - type int = int
6.43 - fun toString (i: int) = makestring i;
6.44 - fun max (x, y) = if x < y then y else x : int;
6.45 - fun min (x, y) = if x < y then x else y : int;
6.46 - end;
6.47 -
6.48 -
6.49 -structure Real =
6.50 - struct
6.51 - fun toString (x: real) = makestring x;
6.52 - fun max (x, y) = if x < y then y else x : real;
6.53 - fun min (x, y) = if x < y then x else y : real;
6.54 - val real = real;
6.55 - val floor = floor;
6.56 - fun ceil x = ~1 - floor (~ (x + 1.0));
6.57 - fun round x = floor (x + 0.5); (*does not do round-to-nearest*)
6.58 - fun trunc x = if x < 0.0 then ceil x else floor x;
6.59 - end;
6.60 -
6.61 -
6.62 -structure List =
6.63 - struct
6.64 - exception Empty
6.65 -
6.66 - fun last [] = raise Empty
6.67 - | last [x] = x
6.68 - | last (x::xs) = last xs;
6.69 -
6.70 - fun nth (xs, n) =
6.71 - let fun h [] _ = raise Subscript
6.72 - | h (x::xs) n = if n=0 then x else h xs (n-1)
6.73 - in if n<0 then raise Subscript else h xs n end;
6.74 -
6.75 - fun drop (xs, n) =
6.76 - let fun h xs 0 = xs
6.77 - | h [] n = raise Subscript
6.78 - | h (x::xs) n = h xs (n-1)
6.79 - in if n<0 then raise Subscript else h xs n end;
6.80 -
6.81 - fun take (xs, n) =
6.82 - let fun h xs 0 = []
6.83 - | h [] n = raise Subscript
6.84 - | h (x::xs) n = x :: h xs (n-1)
6.85 - in if n<0 then raise Subscript else h xs n end;
6.86 -
6.87 - fun concat [] = []
6.88 - | concat (l::ls) = l @ concat ls;
6.89 -
6.90 - fun mapPartial f [] = []
6.91 - | mapPartial f (x::xs) =
6.92 - (case f x of Option.NONE => mapPartial f xs
6.93 - | Option.SOME y => y :: mapPartial f xs);
6.94 -
6.95 - fun find _ [] = Option.NONE
6.96 - | find p (x :: xs) = if p x then Option.SOME x else find p xs;
6.97 -
6.98 -
6.99 - (*copy the list preserving elements that satisfy the predicate*)
6.100 - fun filter p [] = []
6.101 - | filter p (x :: xs) = if p x then x :: filter p xs else filter p xs;
6.102 -
6.103 - (*Partition list into elements that satisfy predicate and those that don't.
6.104 - Preserves order of elements in both lists.*)
6.105 - fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) =
6.106 - let fun part ([], answer) = answer
6.107 - | part (x::xs, (ys, ns)) = if p(x)
6.108 - then part (xs, (x::ys, ns))
6.109 - else part (xs, (ys, x::ns))
6.110 - in part (rev ys, ([], [])) end;
6.111 -
6.112 - end;
6.113 -
6.114 -
6.115 -structure ListPair =
6.116 - struct
6.117 - fun zip ([], []) = []
6.118 - | zip (x::xs,y::ys) = (x,y) :: zip(xs,ys);
6.119 -
6.120 - fun unzip [] = ([],[])
6.121 - | unzip((x,y)::pairs) =
6.122 - let val (xs,ys) = unzip pairs
6.123 - in (x::xs, y::ys) end;
6.124 -
6.125 - fun map f ([], []) = []
6.126 - | map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys);
6.127 -
6.128 - fun exists p =
6.129 - let fun boolf ([], []) = false
6.130 - | boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys)
6.131 - in boolf end;
6.132 -
6.133 - fun all p =
6.134 - let fun boolf ([], []) = true
6.135 - | boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys)
6.136 - in boolf end;
6.137 - end;
6.138 -
6.139 -
6.140 -structure TextIO =
6.141 - struct
6.142 - type instream = instream
6.143 - and outstream = outstream
6.144 - exception Io of {name: string, function: string, cause: exn}
6.145 - val stdIn = std_in
6.146 - val stdOut = std_out
6.147 - val stdErr = std_out
6.148 - val openIn = open_in
6.149 - val openAppend = open_append
6.150 - val openOut = open_out
6.151 - val closeIn = close_in
6.152 - val closeOut = close_out
6.153 - val inputN = input
6.154 - val inputAll = fn is => inputN (is, 999999)
6.155 - val inputLine = input_line
6.156 - val endOfStream = end_of_stream
6.157 - val output = output
6.158 - val flushOut = flush_out
6.159 - end;
6.160 -
6.161 -
6.162 -fun print s = (output (std_out, s); flush_out std_out);
6.163 -
6.164 -
6.165 -structure General =
6.166 -struct
6.167 -
6.168 -local
6.169 - fun raised name = "exception " ^ name ^ " raised";
6.170 - fun raised_msg name msg = raised name ^ ": " ^ msg;
6.171 -in
6.172 - fun exnMessage Match = raised_msg "Match" "nonexhaustive match failure"
6.173 - | exnMessage Bind = raised_msg "Bind" "nonexhaustive binding failure"
6.174 - | exnMessage (Io msg) = "I/O error: " ^ msg
6.175 - | exnMessage Neg = raised "Neg"
6.176 - | exnMessage Sum = raised "Sum"
6.177 - | exnMessage Diff = raised "Diff"
6.178 - | exnMessage Prod = raised "Prod"
6.179 - | exnMessage Quot = raised "Quot"
6.180 - | exnMessage Abs = raised "Abs"
6.181 - | exnMessage Div = raised "Div"
6.182 - | exnMessage Mod = raised "Mod"
6.183 - | exnMessage Floor = raised "Floor"
6.184 - | exnMessage Sqrt = raised "Sqrt"
6.185 - | exnMessage Exp = raised "Exp"
6.186 - | exnMessage Ln = raised "Ln"
6.187 - | exnMessage Ord = raised "Ord"
6.188 - | exnMessage Subscript = raised_msg "Subscript " "subscript out of bounds"
6.189 - | exnMessage Option.Option = raised "Option.Option"
6.190 - | exnMessage List.Empty = raised "List.Empty"
6.191 - | exnMessage (TextIO.Io {name, ...}) = raised_msg "TextIO.Io" name
6.192 - | exnMessage exn = raised "???";
6.193 -end;
6.194 -
6.195 -end;