src/Pure/ML-Systems/polyml.ML
author wenzelm
Wed Nov 26 14:35:55 2014 +0100 (2014-11-26 ago)
changeset 59055 5a7157b8e870
parent 57834 0d295e339f52
child 59127 723b11f8ffbf
permissions -rw-r--r--
more informative failure of protocol commands, with exception trace;
eliminated obsolete Runtime.TERMINATE (left-over from former 'exit' command);
wenzelm@33538
     1
(*  Title:      Pure/ML-Systems/polyml.ML
wenzelm@47980
     2
    Author:     Makarius
wenzelm@29714
     3
wenzelm@50910
     4
Compatibility wrapper for Poly/ML.
wenzelm@29714
     5
*)
wenzelm@29714
     6
wenzelm@56275
     7
(* ML name space *)
wenzelm@56275
     8
wenzelm@56275
     9
structure ML_Name_Space =
wenzelm@56275
    10
struct
wenzelm@56275
    11
  open PolyML.NameSpace;
wenzelm@56275
    12
  type T = PolyML.NameSpace.nameSpace;
wenzelm@56275
    13
  val global = PolyML.globalNameSpace;
wenzelm@56275
    14
  val initial_val =
wenzelm@56275
    15
    List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
wenzelm@56275
    16
      (#allVal global ());
wenzelm@56275
    17
  val initial_type = #allType global ();
wenzelm@56275
    18
  val initial_fixity = #allFix global ();
wenzelm@56275
    19
  val initial_structure = #allStruct global ();
wenzelm@56275
    20
  val initial_signature = #allSig global ();
wenzelm@56275
    21
  val initial_functor = #allFunct global ();
wenzelm@56275
    22
end;
wenzelm@56275
    23
wenzelm@56275
    24
wenzelm@54717
    25
(* ML system operations *)
wenzelm@54717
    26
wenzelm@54717
    27
use "ML-Systems/ml_system.ML";
wenzelm@54717
    28
wenzelm@54717
    29
if ML_System.name = "polyml-5.3.0"
wenzelm@54717
    30
then use "ML-Systems/share_common_data_polyml-5.3.0.ML"
wenzelm@54717
    31
else ();
wenzelm@54717
    32
wenzelm@54717
    33
structure ML_System =
wenzelm@54717
    34
struct
wenzelm@54717
    35
wenzelm@54717
    36
open ML_System;
wenzelm@54717
    37
wenzelm@54717
    38
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
wenzelm@54717
    39
val save_state = PolyML.SaveState.saveState;
wenzelm@54717
    40
wenzelm@54717
    41
end;
wenzelm@54717
    42
wenzelm@54717
    43
wenzelm@47980
    44
(* exceptions *)
wenzelm@30673
    45
wenzelm@31427
    46
fun reraise exn =
wenzelm@31427
    47
  (case PolyML.exceptionLocation exn of
wenzelm@31427
    48
    NONE => raise exn
wenzelm@31427
    49
  | SOME location => PolyML.raiseWithLocation (exn, location));
wenzelm@31427
    50
wenzelm@47980
    51
exception Interrupt = SML90.Interrupt;
wenzelm@47980
    52
wenzelm@47980
    53
use "General/exn.ML";
wenzelm@47980
    54
wenzelm@47980
    55
wenzelm@47980
    56
(* multithreading *)
wenzelm@47980
    57
wenzelm@47980
    58
val seconds = Time.fromReal;
wenzelm@47980
    59
wenzelm@47980
    60
if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ())
wenzelm@47980
    61
then ()
wenzelm@47980
    62
else use "ML-Systems/single_assignment_polyml.ML";
wenzelm@47980
    63
wenzelm@47980
    64
open Thread;
wenzelm@47980
    65
use "ML-Systems/multithreading.ML";
wenzelm@29714
    66
use "ML-Systems/multithreading_polyml.ML";
wenzelm@47980
    67
wenzelm@39616
    68
use "ML-Systems/unsynchronized.ML";
wenzelm@39616
    69
val _ = PolyML.Compiler.forgetValue "ref";
wenzelm@39616
    70
val _ = PolyML.Compiler.forgetType "ref";
wenzelm@29714
    71
wenzelm@47980
    72
wenzelm@47980
    73
(* pervasive environment *)
wenzelm@47980
    74
wenzelm@47980
    75
val _ = PolyML.Compiler.forgetValue "isSome";
wenzelm@47980
    76
val _ = PolyML.Compiler.forgetValue "getOpt";
wenzelm@47980
    77
val _ = PolyML.Compiler.forgetValue "valOf";
wenzelm@47980
    78
val _ = PolyML.Compiler.forgetValue "foldl";
wenzelm@47980
    79
val _ = PolyML.Compiler.forgetValue "foldr";
wenzelm@47980
    80
val _ = PolyML.Compiler.forgetValue "print";
wenzelm@47980
    81
val _ = PolyML.Compiler.forgetValue "explode";
wenzelm@47980
    82
val _ = PolyML.Compiler.forgetValue "concat";
wenzelm@47980
    83
wenzelm@47980
    84
val ord = SML90.ord;
wenzelm@47980
    85
val chr = SML90.chr;
wenzelm@47980
    86
val raw_explode = SML90.explode;
wenzelm@47980
    87
val implode = SML90.implode;
wenzelm@47980
    88
wenzelm@54342
    89
val io_buffer_size = 4096;
wenzelm@54342
    90
wenzelm@47980
    91
fun quit () = exit 0;
wenzelm@47980
    92
wenzelm@47980
    93
wenzelm@47980
    94
(* ML runtime system *)
wenzelm@47980
    95
wenzelm@59055
    96
fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
wenzelm@47980
    97
val timing = PolyML.timing;
wenzelm@47980
    98
val profiling = PolyML.profiling;
wenzelm@47980
    99
wenzelm@47980
   100
fun profile 0 f x = f x
wenzelm@47980
   101
  | profile n f x =
wenzelm@47980
   102
      let
wenzelm@47980
   103
        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
wenzelm@47980
   104
        val res = Exn.capture f x;
wenzelm@47980
   105
        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
wenzelm@47980
   106
      in Exn.release res end;
wenzelm@47980
   107
wenzelm@29714
   108
val pointer_eq = PolyML.pointerEq;
wenzelm@29714
   109
wenzelm@47980
   110
wenzelm@47980
   111
(* ML compiler *)
wenzelm@47980
   112
wenzelm@47980
   113
use "ML-Systems/use_context.ML";
wenzelm@56435
   114
use "ML-Systems/ml_positions.ML";
wenzelm@47980
   115
use "ML-Systems/compiler_polyml.ML";
wenzelm@47980
   116
wenzelm@32778
   117
PolyML.Compiler.reportUnreferencedIds := true;
wenzelm@47980
   118
PolyML.Compiler.printInAlphabeticalOrder := false;
wenzelm@47980
   119
PolyML.Compiler.maxInlineSize := 80;
wenzelm@47980
   120
wenzelm@47980
   121
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
wenzelm@30626
   122
wenzelm@30626
   123
wenzelm@47980
   124
(* ML toplevel pretty printing *)
wenzelm@47980
   125
wenzelm@47980
   126
use "ML-Systems/ml_pretty.ML";
wenzelm@47980
   127
wenzelm@47980
   128
local
wenzelm@47980
   129
  val depth = Unsynchronized.ref 10;
wenzelm@47980
   130
in
wenzelm@56281
   131
  fun get_default_print_depth () = ! depth;
wenzelm@56285
   132
  fun default_print_depth n = (depth := n; PolyML.print_depth n);
wenzelm@56285
   133
  val _ = default_print_depth 10;
wenzelm@47980
   134
end;
wenzelm@47980
   135
wenzelm@47980
   136
val error_depth = PolyML.error_depth;
wenzelm@30626
   137
wenzelm@30676
   138
val pretty_ml =
wenzelm@30676
   139
  let
wenzelm@51638
   140
    fun convert _ (PolyML.PrettyBreak (wd, _)) = ML_Pretty.Break (false, wd)
wenzelm@54718
   141
      | convert _ (PolyML.PrettyBlock (_, _,
wenzelm@51638
   142
            [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
wenzelm@51638
   143
          ML_Pretty.Break (true, 1)
wenzelm@51638
   144
      | convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
wenzelm@30676
   145
          let
wenzelm@30676
   146
            fun property name default =
wenzelm@31318
   147
              (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
wenzelm@31318
   148
                SOME (PolyML.ContextProperty (_, b)) => b
wenzelm@54718
   149
              | _ => default);
wenzelm@30676
   150
            val bg = property "begin" "";
wenzelm@30676
   151
            val en = property "end" "";
wenzelm@30676
   152
            val len' = property "length" len;
wenzelm@30676
   153
          in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
wenzelm@31318
   154
      | convert len (PolyML.PrettyString s) =
wenzelm@30676
   155
          ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
wenzelm@30676
   156
  in convert "" end;
wenzelm@30638
   157
wenzelm@51638
   158
fun ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0)
wenzelm@51638
   159
  | ml_pretty (ML_Pretty.Break (true, _)) =
wenzelm@51638
   160
      PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
wenzelm@51638
   161
        [PolyML.PrettyString " "])
wenzelm@51638
   162
  | ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
wenzelm@30679
   163
      let val context =
wenzelm@31318
   164
        (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
wenzelm@31318
   165
        (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
wenzelm@31318
   166
      in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end
wenzelm@30676
   167
  | ml_pretty (ML_Pretty.String (s, len)) =
wenzelm@31318
   168
      if len = size s then PolyML.PrettyString s
wenzelm@31318
   169
      else PolyML.PrettyBlock
wenzelm@51638
   170
        (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]);
wenzelm@30626
   171
wenzelm@30673
   172
fun toplevel_pp context (_: string list) pp =
wenzelm@30673
   173
  use_text context (1, "pp") false
wenzelm@31318
   174
    ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
wenzelm@30626
   175
wenzelm@36162
   176
val ml_make_string =
wenzelm@57834
   177
  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, Isabelle.ML_print_depth ())))))";
wenzelm@36162
   178