--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/run-polyml-5.6 Fri Nov 20 21:52:05 2015 +0100
@@ -0,0 +1,106 @@
+#!/usr/bin/env bash
+# :mode=shellscript:
+#
+# Author: Makarius
+#
+# Startup script for Poly/ML 5.6.
+
+export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
+
+
+## diagnostics
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+function fail_out()
+{
+ fail "Unable to create output heap file: \"$OUTFILE\""
+}
+
+function check_file()
+{
+ [ ! -f "$1" ] && fail "Unable to locate \"$1\""
+}
+
+
+## compiler executables and libraries
+
+[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
+
+POLY="$ML_HOME/poly"
+check_file "$POLY"
+
+librarypath "$ML_HOME"
+
+
+
+## prepare databases
+
+case "$ML_PLATFORM" in
+ *-windows)
+ PLATFORM_INFILE="$(platform_path -m "$INFILE")"
+ PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")"
+ ;;
+ *)
+ PLATFORM_INFILE="$INFILE"
+ PLATFORM_OUTFILE="$OUTFILE"
+ ;;
+esac
+
+if [ -z "$INFILE" ]; then
+ INIT=""
+ case "$ML_PLATFORM" in
+ *-windows)
+ EXIT="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc));"
+ ;;
+ *)
+ EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
+ ;;
+ esac
+else
+ check_file "$INFILE"
+ INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));"
+ EXIT=""
+fi
+
+if [ -z "$OUTFILE" ]; then
+ MLEXIT=""
+else
+ if [ -z "$INFILE" ]; then
+ MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$PLATFORM_OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); OS.Process.exit OS.Process.success);"
+ else
+ MLEXIT="Session.save \"$OUTFILE\";"
+ fi
+ [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+fi
+
+
+## run it!
+
+MLTEXT="$INIT $EXIT $MLTEXT"
+
+if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
+ "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
+ --error-exit </dev/null
+ RC="$?"
+else
+ if [ -z "$TERMINATE" ]; then
+ FEEDER_OPTS=""
+ else
+ FEEDER_OPTS="-q"
+ ML_OPTIONS="$ML_OPTIONS --error-exit"
+ fi
+ "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+ { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
+ RC="$?"
+fi
+
+[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
+
+exit "$RC"
+
+#:wrap=soft:maxLineLen=100:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_name_space_polyml-5.6.ML Fri Nov 20 21:52:05 2015 +0100
@@ -0,0 +1,33 @@
+(* Title: Pure/ML-Systems/ml_name_space_polyml-5.6.ML
+ Author: Makarius
+
+Name space for Poly/ML.
+*)
+
+structure ML_Name_Space =
+struct
+ open PolyML.NameSpace;
+
+ type T = PolyML.NameSpace.nameSpace;
+ val global = PolyML.globalNameSpace;
+ val forget_global_structure = PolyML.Compiler.forgetStructure;
+
+ type valueVal = Values.value;
+ fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
+ fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
+
+ type typeVal = TypeConstrs.typeConstr;
+ fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
+
+ type fixityVal = Infixes.fixity;
+ fun displayFix (_: string, x) = Infixes.print x;
+
+ type structureVal = Structures.structureVal;
+ fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
+
+ type signatureVal = Signatures.signatureVal;
+ fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
+
+ type functorVal = Functors.functorVal;
+ fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_name_space_polyml.ML Fri Nov 20 21:52:05 2015 +0100
@@ -0,0 +1,13 @@
+(* Title: Pure/ML-Systems/ml_name_space_polyml.ML
+ Author: Makarius
+
+Name space for Poly/ML.
+*)
+
+structure ML_Name_Space =
+struct
+ open PolyML.NameSpace;
+ type T = nameSpace;
+ val global = PolyML.globalNameSpace;
+ val forget_global_structure = PolyML.Compiler.forgetStructure;
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML Fri Nov 20 21:52:05 2015 +0100
@@ -0,0 +1,17 @@
+(* Title: Pure/ML-Systems/ml_profiling_polyml-5.6.ML
+ Author: Makarius
+
+Profiling for Poly/ML 5.6.
+*)
+
+fun profile 0 f x = f x
+ | profile n f x =
+ let
+ val mode =
+ (case n of
+ 1 => PolyML.Profiling.ProfileTime
+ | 2 => PolyML.Profiling.ProfileAllocations
+ | 3 => PolyML.Profiling.ProfileLongIntEmulation
+ | 6 => PolyML.Profiling.ProfileTimeThisThread
+ | _ => raise Fail ("Bad profile mode: " ^ Int.toString n));
+ in PolyML.Profiling.profile mode f x end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_profiling_polyml.ML Fri Nov 20 21:52:05 2015 +0100
@@ -0,0 +1,13 @@
+(* Title: Pure/ML-Systems/ml_profiling_polyml.ML
+ Author: Makarius
+
+Profiling for Poly/ML.
+*)
+
+fun profile 0 f x = f x
+ | profile n f x =
+ let
+ val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
+ val res = Exn.capture f x;
+ val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
+ in Exn.release res end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml-5.6.ML Fri Nov 20 21:52:05 2015 +0100
@@ -0,0 +1,22 @@
+(* Title: Pure/ML-Systems/polyml-5.6.ML
+ Author: Makarius
+
+Compatibility wrapper for Poly/ML 5.6.
+*)
+
+structure Thread =
+struct
+ open Thread;
+
+ structure Thread =
+ struct
+ open Thread;
+
+ fun numProcessors () =
+ (case Thread.numPhysicalProcessors () of
+ SOME n => n
+ | NONE => Thread.numProcessors ());
+ end;
+end;
+
+use "ML-Systems/polyml.ML";
--- a/src/Pure/ML-Systems/polyml.ML Fri Nov 20 15:54:46 2015 +0000
+++ b/src/Pure/ML-Systems/polyml.ML Fri Nov 20 21:52:05 2015 +0100
@@ -6,11 +6,15 @@
(* initial ML name space *)
+use "ML-Systems/ml_system.ML";
+
+if ML_System.name = "polyml-5.6"
+then use "ML-Systems/ml_name_space_polyml-5.6.ML"
+else use "ML-Systems/ml_name_space_polyml.ML";
+
structure ML_Name_Space =
struct
- open PolyML.NameSpace;
- type T = PolyML.NameSpace.nameSpace;
- val global = PolyML.globalNameSpace;
+ open ML_Name_Space;
val initial_val =
List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
(#allVal global ());
@@ -19,14 +23,11 @@
val initial_structure = #allStruct global ();
val initial_signature = #allSig global ();
val initial_functor = #allFunct global ();
- val forget_global_structure = PolyML.Compiler.forgetStructure;
end;
(* ML system operations *)
-use "ML-Systems/ml_system.ML";
-
if ML_System.name = "polyml-5.3.0"
then use "ML-Systems/share_common_data_polyml-5.3.0.ML"
else ();
@@ -60,6 +61,7 @@
if ML_System.name = "polyml-5.5.1"
orelse ML_System.name = "polyml-5.5.2"
orelse ML_System.name = "polyml-5.5.3"
+ orelse ML_System.name = "polyml-5.6"
then use "ML-Systems/exn_trace_polyml-5.5.1.ML"
else ();
@@ -77,6 +79,7 @@
use "ML-Systems/multithreading_polyml.ML";
if ML_System.name = "polyml-5.5.3"
+ orelse ML_System.name = "polyml-5.6"
then use "ML-Systems/ml_stack_polyml-5.5.3.ML"
else use "ML-Systems/ml_stack_dummy.ML";
@@ -108,16 +111,9 @@
(* ML runtime system *)
-val timing = PolyML.timing;
-val profiling = PolyML.profiling;
-
-fun profile 0 f x = f x
- | profile n f x =
- let
- val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
- val res = Exn.capture f x;
- val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
- in Exn.release res end;
+if ML_System.name = "polyml-5.6"
+then use "ML-Systems/ml_profiling_polyml-5.6.ML"
+else use "ML-Systems/ml_profiling_polyml.ML";
val pointer_eq = PolyML.pointerEq;
@@ -176,11 +172,12 @@
structure ML_Name_Space =
struct
open ML_Name_Space;
- val display_val = pretty_ml o PolyML.NameSpace.displayVal;
+ val display_val = pretty_ml o displayVal;
end;
use "ML-Systems/ml_compiler_parameters.ML";
if ML_System.name = "polyml-5.5.3"
+ orelse ML_System.name = "polyml-5.6"
then use "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" else ();
use "ML-Systems/use_context.ML";
@@ -195,6 +192,7 @@
use "ML-Systems/ml_parse_tree.ML";
if ML_System.name = "polyml-5.5.3"
+ orelse ML_System.name = "polyml-5.6"
then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
fun toplevel_pp context (_: string list) pp =
@@ -209,5 +207,6 @@
(* ML debugger *)
if ML_System.name = "polyml-5.5.3"
+ orelse ML_System.name = "polyml-5.6"
then use "ML-Systems/ml_debugger_polyml-5.5.3.ML"
else use "ML-Systems/ml_debugger.ML";
--- a/src/Pure/ML/ml_compiler_polyml.ML Fri Nov 20 15:54:46 2015 +0000
+++ b/src/Pure/ML/ml_compiler_polyml.ML Fri Nov 20 21:52:05 2015 +0100
@@ -39,7 +39,7 @@
is_reported pos ?
let
val xml =
- PolyML.NameSpace.displayTypeExpression (types, depth, space)
+ ML_Name_Space.displayTypeExpression (types, depth, space)
|> pretty_ml |> Pretty.from_ML |> Pretty.string_of
|> Output.output |> YXML.parse_body;
in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
@@ -188,17 +188,17 @@
else ();
fun apply_fix (a, b) =
- (#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b));
+ (#enterFix space (a, b); display ML_Name_Space.displayFix (a, b));
fun apply_type (a, b) =
- (#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space));
+ (#enterType space (a, b); display ML_Name_Space.displayType (b, depth, space));
fun apply_sig (a, b) =
- (#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space));
+ (#enterSig space (a, b); display ML_Name_Space.displaySig (b, depth, space));
fun apply_struct (a, b) =
- (#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space));
+ (#enterStruct space (a, b); display ML_Name_Space.displayStruct (b, depth, space));
fun apply_funct (a, b) =
- (#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space));
+ (#enterFunct space (a, b); display ML_Name_Space.displayFunct (b, depth, space));
fun apply_val (a, b) =
- (#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space));
+ (#enterVal space (a, b); display ML_Name_Space.displayVal (b, depth, space));
in
List.app apply_fix fixes;
List.app apply_type types;
--- a/src/Pure/ROOT Fri Nov 20 15:54:46 2015 +0000
+++ b/src/Pure/ROOT Fri Nov 20 21:52:05 2015 +0100
@@ -11,10 +11,14 @@
"ML-Systems/ml_debugger.ML"
"ML-Systems/ml_debugger_polyml-5.5.3.ML"
"ML-Systems/ml_name_space.ML"
+ "ML-Systems/ml_name_space_polyml-5.6.ML"
+ "ML-Systems/ml_name_space_polyml.ML"
"ML-Systems/ml_parse_tree.ML"
"ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
"ML-Systems/ml_positions.ML"
"ML-Systems/ml_pretty.ML"
+ "ML-Systems/ml_profiling_polyml-5.6.ML"
+ "ML-Systems/ml_profiling_polyml.ML"
"ML-Systems/ml_stack_dummy.ML"
"ML-Systems/ml_stack_polyml-5.5.3.ML"
"ML-Systems/ml_system.ML"
@@ -23,6 +27,7 @@
"ML-Systems/overloading_smlnj.ML"
"ML-Systems/polyml-5.5.2.ML"
"ML-Systems/polyml-5.5.3.ML"
+ "ML-Systems/polyml-5.6.ML"
"ML-Systems/polyml.ML"
"ML-Systems/pp_dummy.ML"
"ML-Systems/proper_int.ML"
@@ -47,10 +52,14 @@
"ML-Systems/ml_debugger.ML"
"ML-Systems/ml_debugger_polyml-5.5.3.ML"
"ML-Systems/ml_name_space.ML"
+ "ML-Systems/ml_name_space_polyml-5.6.ML"
+ "ML-Systems/ml_name_space_polyml.ML"
"ML-Systems/ml_parse_tree.ML"
"ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
"ML-Systems/ml_positions.ML"
"ML-Systems/ml_pretty.ML"
+ "ML-Systems/ml_profiling_polyml-5.6.ML"
+ "ML-Systems/ml_profiling_polyml.ML"
"ML-Systems/ml_stack_dummy.ML"
"ML-Systems/ml_stack_polyml-5.5.3.ML"
"ML-Systems/ml_system.ML"
@@ -59,6 +68,7 @@
"ML-Systems/overloading_smlnj.ML"
"ML-Systems/polyml-5.5.2.ML"
"ML-Systems/polyml-5.5.3.ML"
+ "ML-Systems/polyml-5.6.ML"
"ML-Systems/polyml.ML"
"ML-Systems/pp_dummy.ML"
"ML-Systems/proper_int.ML"
--- a/src/Pure/ROOT.ML Fri Nov 20 15:54:46 2015 +0000
+++ b/src/Pure/ROOT.ML Fri Nov 20 21:52:05 2015 +0100
@@ -106,6 +106,7 @@
orelse ML_System.name = "polyml-5.5.1"
orelse ML_System.name = "polyml-5.5.2"
orelse ML_System.name = "polyml-5.5.3"
+ orelse ML_System.name = "polyml-5.6"
then use "ML/ml_statistics_polyml-5.5.0.ML"
else use "ML/ml_statistics_dummy.ML";