speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
authorwenzelm
Fri Nov 20 21:52:05 2015 +0100 (2015-11-20)
changeset 617155dc95d957569
parent 61714 7c1ad030f0c9
child 61716 08236d919586
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
lib/scripts/run-polyml-5.6
src/Pure/ML-Systems/ml_name_space_polyml-5.6.ML
src/Pure/ML-Systems/ml_name_space_polyml.ML
src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML
src/Pure/ML-Systems/ml_profiling_polyml.ML
src/Pure/ML-Systems/polyml-5.6.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/scripts/run-polyml-5.6	Fri Nov 20 21:52:05 2015 +0100
     1.3 @@ -0,0 +1,106 @@
     1.4 +#!/usr/bin/env bash
     1.5 +# :mode=shellscript:
     1.6 +#
     1.7 +# Author: Makarius
     1.8 +#
     1.9 +# Startup script for Poly/ML 5.6.
    1.10 +
    1.11 +export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
    1.12 +
    1.13 +
    1.14 +## diagnostics
    1.15 +
    1.16 +function fail()
    1.17 +{
    1.18 +  echo "$1" >&2
    1.19 +  exit 2
    1.20 +}
    1.21 +
    1.22 +function fail_out()
    1.23 +{
    1.24 +  fail "Unable to create output heap file: \"$OUTFILE\""
    1.25 +}
    1.26 +
    1.27 +function check_file()
    1.28 +{
    1.29 +  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
    1.30 +}
    1.31 +
    1.32 +
    1.33 +## compiler executables and libraries
    1.34 +
    1.35 +[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
    1.36 +
    1.37 +POLY="$ML_HOME/poly"
    1.38 +check_file "$POLY"
    1.39 +
    1.40 +librarypath "$ML_HOME"
    1.41 +
    1.42 +
    1.43 +
    1.44 +## prepare databases
    1.45 +
    1.46 +case "$ML_PLATFORM" in
    1.47 +  *-windows)
    1.48 +    PLATFORM_INFILE="$(platform_path -m "$INFILE")"
    1.49 +    PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")"
    1.50 +    ;;
    1.51 +  *)
    1.52 +    PLATFORM_INFILE="$INFILE"
    1.53 +    PLATFORM_OUTFILE="$OUTFILE"
    1.54 +    ;;
    1.55 +esac
    1.56 +
    1.57 +if [ -z "$INFILE" ]; then
    1.58 +  INIT=""
    1.59 +  case "$ML_PLATFORM" in
    1.60 +    *-windows)
    1.61 +      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));"
    1.62 +      ;;
    1.63 +    *)
    1.64 +      EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
    1.65 +      ;;
    1.66 +  esac
    1.67 +else
    1.68 +  check_file "$INFILE"
    1.69 +  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));"
    1.70 +  EXIT=""
    1.71 +fi
    1.72 +
    1.73 +if [ -z "$OUTFILE" ]; then
    1.74 +  MLEXIT=""
    1.75 +else
    1.76 +  if [ -z "$INFILE" ]; then
    1.77 +    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);"
    1.78 +  else
    1.79 +    MLEXIT="Session.save \"$OUTFILE\";"
    1.80 +  fi
    1.81 +  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    1.82 +fi
    1.83 +
    1.84 +
    1.85 +## run it!
    1.86 +
    1.87 +MLTEXT="$INIT $EXIT $MLTEXT"
    1.88 +
    1.89 +if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
    1.90 +  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
    1.91 +    --error-exit </dev/null
    1.92 +  RC="$?"
    1.93 +else
    1.94 +  if [ -z "$TERMINATE" ]; then
    1.95 +    FEEDER_OPTS=""
    1.96 +  else
    1.97 +    FEEDER_OPTS="-q"
    1.98 +    ML_OPTIONS="$ML_OPTIONS --error-exit"
    1.99 +  fi
   1.100 +  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
   1.101 +    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
   1.102 +  RC="$?"
   1.103 +fi
   1.104 +
   1.105 +[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
   1.106 +
   1.107 +exit "$RC"
   1.108 +
   1.109 +#:wrap=soft:maxLineLen=100:
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/ML-Systems/ml_name_space_polyml-5.6.ML	Fri Nov 20 21:52:05 2015 +0100
     2.3 @@ -0,0 +1,33 @@
     2.4 +(*  Title:      Pure/ML-Systems/ml_name_space_polyml-5.6.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Name space for Poly/ML.
     2.8 +*)
     2.9 +
    2.10 +structure ML_Name_Space =
    2.11 +struct
    2.12 +  open PolyML.NameSpace;
    2.13 +
    2.14 +  type T = PolyML.NameSpace.nameSpace;
    2.15 +  val global = PolyML.globalNameSpace;
    2.16 +  val forget_global_structure = PolyML.Compiler.forgetStructure;
    2.17 +
    2.18 +  type valueVal = Values.value;
    2.19 +  fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
    2.20 +  fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
    2.21 +
    2.22 +  type typeVal = TypeConstrs.typeConstr;
    2.23 +  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
    2.24 +
    2.25 +  type fixityVal = Infixes.fixity;
    2.26 +  fun displayFix (_: string, x) = Infixes.print x;
    2.27 +
    2.28 +  type structureVal = Structures.structureVal;
    2.29 +  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
    2.30 +
    2.31 +  type signatureVal = Signatures.signatureVal;
    2.32 +  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
    2.33 +
    2.34 +  type functorVal = Functors.functorVal;
    2.35 +  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
    2.36 +end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/ML-Systems/ml_name_space_polyml.ML	Fri Nov 20 21:52:05 2015 +0100
     3.3 @@ -0,0 +1,13 @@
     3.4 +(*  Title:      Pure/ML-Systems/ml_name_space_polyml.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Name space for Poly/ML.
     3.8 +*)
     3.9 +
    3.10 +structure ML_Name_Space =
    3.11 +struct
    3.12 +  open PolyML.NameSpace;
    3.13 +  type T = nameSpace;
    3.14 +  val global = PolyML.globalNameSpace;
    3.15 +  val forget_global_structure = PolyML.Compiler.forgetStructure;
    3.16 +end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML	Fri Nov 20 21:52:05 2015 +0100
     4.3 @@ -0,0 +1,17 @@
     4.4 +(*  Title:      Pure/ML-Systems/ml_profiling_polyml-5.6.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Profiling for Poly/ML 5.6.
     4.8 +*)
     4.9 +
    4.10 +fun profile 0 f x = f x
    4.11 +  | profile n f x =
    4.12 +      let
    4.13 +        val mode =
    4.14 +          (case n of
    4.15 +            1 => PolyML.Profiling.ProfileTime
    4.16 +          | 2 => PolyML.Profiling.ProfileAllocations
    4.17 +          | 3 => PolyML.Profiling.ProfileLongIntEmulation
    4.18 +          | 6 => PolyML.Profiling.ProfileTimeThisThread
    4.19 +          | _ => raise Fail ("Bad profile mode: " ^ Int.toString n));
    4.20 +      in PolyML.Profiling.profile mode f x end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/ML-Systems/ml_profiling_polyml.ML	Fri Nov 20 21:52:05 2015 +0100
     5.3 @@ -0,0 +1,13 @@
     5.4 +(*  Title:      Pure/ML-Systems/ml_profiling_polyml.ML
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Profiling for Poly/ML.
     5.8 +*)
     5.9 +
    5.10 +fun profile 0 f x = f x
    5.11 +  | profile n f x =
    5.12 +      let
    5.13 +        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
    5.14 +        val res = Exn.capture f x;
    5.15 +        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
    5.16 +      in Exn.release res end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/ML-Systems/polyml-5.6.ML	Fri Nov 20 21:52:05 2015 +0100
     6.3 @@ -0,0 +1,22 @@
     6.4 +(*  Title:      Pure/ML-Systems/polyml-5.6.ML
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Compatibility wrapper for Poly/ML 5.6.
     6.8 +*)
     6.9 +
    6.10 +structure Thread =
    6.11 +struct
    6.12 +  open Thread;
    6.13 +
    6.14 +  structure Thread =
    6.15 +  struct
    6.16 +    open Thread;
    6.17 +
    6.18 +    fun numProcessors () =
    6.19 +      (case Thread.numPhysicalProcessors () of
    6.20 +        SOME n => n
    6.21 +      | NONE => Thread.numProcessors ());
    6.22 +  end;
    6.23 +end;
    6.24 +
    6.25 +use "ML-Systems/polyml.ML";
     7.1 --- a/src/Pure/ML-Systems/polyml.ML	Fri Nov 20 15:54:46 2015 +0000
     7.2 +++ b/src/Pure/ML-Systems/polyml.ML	Fri Nov 20 21:52:05 2015 +0100
     7.3 @@ -6,11 +6,15 @@
     7.4  
     7.5  (* initial ML name space *)
     7.6  
     7.7 +use "ML-Systems/ml_system.ML";
     7.8 +
     7.9 +if ML_System.name = "polyml-5.6"
    7.10 +then use "ML-Systems/ml_name_space_polyml-5.6.ML"
    7.11 +else use "ML-Systems/ml_name_space_polyml.ML";
    7.12 +
    7.13  structure ML_Name_Space =
    7.14  struct
    7.15 -  open PolyML.NameSpace;
    7.16 -  type T = PolyML.NameSpace.nameSpace;
    7.17 -  val global = PolyML.globalNameSpace;
    7.18 +  open ML_Name_Space;
    7.19    val initial_val =
    7.20      List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
    7.21        (#allVal global ());
    7.22 @@ -19,14 +23,11 @@
    7.23    val initial_structure = #allStruct global ();
    7.24    val initial_signature = #allSig global ();
    7.25    val initial_functor = #allFunct global ();
    7.26 -  val forget_global_structure = PolyML.Compiler.forgetStructure;
    7.27  end;
    7.28  
    7.29  
    7.30  (* ML system operations *)
    7.31  
    7.32 -use "ML-Systems/ml_system.ML";
    7.33 -
    7.34  if ML_System.name = "polyml-5.3.0"
    7.35  then use "ML-Systems/share_common_data_polyml-5.3.0.ML"
    7.36  else ();
    7.37 @@ -60,6 +61,7 @@
    7.38  if ML_System.name = "polyml-5.5.1"
    7.39    orelse ML_System.name = "polyml-5.5.2"
    7.40    orelse ML_System.name = "polyml-5.5.3"
    7.41 +  orelse ML_System.name = "polyml-5.6"
    7.42  then use "ML-Systems/exn_trace_polyml-5.5.1.ML"
    7.43  else ();
    7.44  
    7.45 @@ -77,6 +79,7 @@
    7.46  use "ML-Systems/multithreading_polyml.ML";
    7.47  
    7.48  if ML_System.name = "polyml-5.5.3"
    7.49 +  orelse ML_System.name = "polyml-5.6"
    7.50  then use "ML-Systems/ml_stack_polyml-5.5.3.ML"
    7.51  else use "ML-Systems/ml_stack_dummy.ML";
    7.52  
    7.53 @@ -108,16 +111,9 @@
    7.54  
    7.55  (* ML runtime system *)
    7.56  
    7.57 -val timing = PolyML.timing;
    7.58 -val profiling = PolyML.profiling;
    7.59 -
    7.60 -fun profile 0 f x = f x
    7.61 -  | profile n f x =
    7.62 -      let
    7.63 -        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
    7.64 -        val res = Exn.capture f x;
    7.65 -        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
    7.66 -      in Exn.release res end;
    7.67 +if ML_System.name = "polyml-5.6"
    7.68 +then use "ML-Systems/ml_profiling_polyml-5.6.ML"
    7.69 +else use "ML-Systems/ml_profiling_polyml.ML";
    7.70  
    7.71  val pointer_eq = PolyML.pointerEq;
    7.72  
    7.73 @@ -176,11 +172,12 @@
    7.74  structure ML_Name_Space =
    7.75  struct
    7.76    open ML_Name_Space;
    7.77 -  val display_val = pretty_ml o PolyML.NameSpace.displayVal;
    7.78 +  val display_val = pretty_ml o displayVal;
    7.79  end;
    7.80  
    7.81  use "ML-Systems/ml_compiler_parameters.ML";
    7.82  if ML_System.name = "polyml-5.5.3"
    7.83 +  orelse ML_System.name = "polyml-5.6"
    7.84  then use "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" else ();
    7.85  
    7.86  use "ML-Systems/use_context.ML";
    7.87 @@ -195,6 +192,7 @@
    7.88  
    7.89  use "ML-Systems/ml_parse_tree.ML";
    7.90  if ML_System.name = "polyml-5.5.3"
    7.91 +  orelse ML_System.name = "polyml-5.6"
    7.92  then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
    7.93  
    7.94  fun toplevel_pp context (_: string list) pp =
    7.95 @@ -209,5 +207,6 @@
    7.96  (* ML debugger *)
    7.97  
    7.98  if ML_System.name = "polyml-5.5.3"
    7.99 +  orelse ML_System.name = "polyml-5.6"
   7.100  then use "ML-Systems/ml_debugger_polyml-5.5.3.ML"
   7.101  else use "ML-Systems/ml_debugger.ML";
     8.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Fri Nov 20 15:54:46 2015 +0000
     8.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Fri Nov 20 21:52:05 2015 +0100
     8.3 @@ -39,7 +39,7 @@
     8.4          is_reported pos ?
     8.5            let
     8.6              val xml =
     8.7 -              PolyML.NameSpace.displayTypeExpression (types, depth, space)
     8.8 +              ML_Name_Space.displayTypeExpression (types, depth, space)
     8.9                |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    8.10                |> Output.output |> YXML.parse_body;
    8.11            in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
    8.12 @@ -188,17 +188,17 @@
    8.13            else ();
    8.14  
    8.15          fun apply_fix (a, b) =
    8.16 -          (#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b));
    8.17 +          (#enterFix space (a, b); display ML_Name_Space.displayFix (a, b));
    8.18          fun apply_type (a, b) =
    8.19 -          (#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space));
    8.20 +          (#enterType space (a, b); display ML_Name_Space.displayType (b, depth, space));
    8.21          fun apply_sig (a, b) =
    8.22 -          (#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space));
    8.23 +          (#enterSig space (a, b); display ML_Name_Space.displaySig (b, depth, space));
    8.24          fun apply_struct (a, b) =
    8.25 -          (#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space));
    8.26 +          (#enterStruct space (a, b); display ML_Name_Space.displayStruct (b, depth, space));
    8.27          fun apply_funct (a, b) =
    8.28 -          (#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space));
    8.29 +          (#enterFunct space (a, b); display ML_Name_Space.displayFunct (b, depth, space));
    8.30          fun apply_val (a, b) =
    8.31 -          (#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space));
    8.32 +          (#enterVal space (a, b); display ML_Name_Space.displayVal (b, depth, space));
    8.33        in
    8.34          List.app apply_fix fixes;
    8.35          List.app apply_type types;
     9.1 --- a/src/Pure/ROOT	Fri Nov 20 15:54:46 2015 +0000
     9.2 +++ b/src/Pure/ROOT	Fri Nov 20 21:52:05 2015 +0100
     9.3 @@ -11,10 +11,14 @@
     9.4      "ML-Systems/ml_debugger.ML"
     9.5      "ML-Systems/ml_debugger_polyml-5.5.3.ML"
     9.6      "ML-Systems/ml_name_space.ML"
     9.7 +    "ML-Systems/ml_name_space_polyml-5.6.ML"
     9.8 +    "ML-Systems/ml_name_space_polyml.ML"
     9.9      "ML-Systems/ml_parse_tree.ML"
    9.10      "ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
    9.11      "ML-Systems/ml_positions.ML"
    9.12      "ML-Systems/ml_pretty.ML"
    9.13 +    "ML-Systems/ml_profiling_polyml-5.6.ML"
    9.14 +    "ML-Systems/ml_profiling_polyml.ML"
    9.15      "ML-Systems/ml_stack_dummy.ML"
    9.16      "ML-Systems/ml_stack_polyml-5.5.3.ML"
    9.17      "ML-Systems/ml_system.ML"
    9.18 @@ -23,6 +27,7 @@
    9.19      "ML-Systems/overloading_smlnj.ML"
    9.20      "ML-Systems/polyml-5.5.2.ML"
    9.21      "ML-Systems/polyml-5.5.3.ML"
    9.22 +    "ML-Systems/polyml-5.6.ML"
    9.23      "ML-Systems/polyml.ML"
    9.24      "ML-Systems/pp_dummy.ML"
    9.25      "ML-Systems/proper_int.ML"
    9.26 @@ -47,10 +52,14 @@
    9.27      "ML-Systems/ml_debugger.ML"
    9.28      "ML-Systems/ml_debugger_polyml-5.5.3.ML"
    9.29      "ML-Systems/ml_name_space.ML"
    9.30 +    "ML-Systems/ml_name_space_polyml-5.6.ML"
    9.31 +    "ML-Systems/ml_name_space_polyml.ML"
    9.32      "ML-Systems/ml_parse_tree.ML"
    9.33      "ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
    9.34      "ML-Systems/ml_positions.ML"
    9.35      "ML-Systems/ml_pretty.ML"
    9.36 +    "ML-Systems/ml_profiling_polyml-5.6.ML"
    9.37 +    "ML-Systems/ml_profiling_polyml.ML"
    9.38      "ML-Systems/ml_stack_dummy.ML"
    9.39      "ML-Systems/ml_stack_polyml-5.5.3.ML"
    9.40      "ML-Systems/ml_system.ML"
    9.41 @@ -59,6 +68,7 @@
    9.42      "ML-Systems/overloading_smlnj.ML"
    9.43      "ML-Systems/polyml-5.5.2.ML"
    9.44      "ML-Systems/polyml-5.5.3.ML"
    9.45 +    "ML-Systems/polyml-5.6.ML"
    9.46      "ML-Systems/polyml.ML"
    9.47      "ML-Systems/pp_dummy.ML"
    9.48      "ML-Systems/proper_int.ML"
    10.1 --- a/src/Pure/ROOT.ML	Fri Nov 20 15:54:46 2015 +0000
    10.2 +++ b/src/Pure/ROOT.ML	Fri Nov 20 21:52:05 2015 +0100
    10.3 @@ -106,6 +106,7 @@
    10.4    orelse ML_System.name = "polyml-5.5.1"
    10.5    orelse ML_System.name = "polyml-5.5.2"
    10.6    orelse ML_System.name = "polyml-5.5.3"
    10.7 +  orelse ML_System.name = "polyml-5.6"
    10.8  then use "ML/ml_statistics_polyml-5.5.0.ML"
    10.9  else use "ML/ml_statistics_dummy.ML";
   10.10