src/Pure/ML/ml_compiler0.ML
author wenzelm
Wed, 06 Apr 2016 11:57:21 +0200
changeset 62886 72c475e03e22
parent 62877 741560a5283b
child 62894 047129a6e200
permissions -rw-r--r--
simplified bootstrap: critical structures remain accessible in ML_Root context;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62508
d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents: 62505
diff changeset
     1
(*  Title:      Pure/ML/ml_compiler0.ML
62817
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
     2
    Author:     Makarius
31312
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
     3
62817
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
     4
Runtime compilation and evaluation for bootstrap.
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
     5
Initial ML use operations.
31312
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
     6
*)
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
     7
62494
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
     8
signature ML_COMPILER0 =
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
     9
sig
62821
48c24d0b6d85 tuned signature;
wenzelm
parents: 62819
diff changeset
    10
  type polyml_location = PolyML.location
62494
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
    11
  type context =
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
    12
   {name_space: ML_Name_Space.T,
62716
d80b9f4990e4 explicit print_depth for the sake of Spec_Check.determine_type;
wenzelm
parents: 62668
diff changeset
    13
    print_depth: int option,
62494
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
    14
    here: int -> string -> string,
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
    15
    print: string -> unit,
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
    16
    error: string -> unit}
62817
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    17
  val make_context: ML_Name_Space.T -> context
62494
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
    18
  val use_text: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
    19
  val use_file: context -> {debug: bool, verbose: bool} -> string -> unit
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
    20
  val debug_option: bool option -> bool
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
    21
  val use_operations: (bool option -> string -> unit) ->
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
    22
    {use: string -> unit, use_debug: string -> unit, use_no_debug: string -> unit}
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
    23
end;
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
    24
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
    25
structure ML_Compiler0: ML_COMPILER0 =
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
    26
struct
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
    27
62821
48c24d0b6d85 tuned signature;
wenzelm
parents: 62819
diff changeset
    28
type polyml_location = PolyML.location;
48c24d0b6d85 tuned signature;
wenzelm
parents: 62819
diff changeset
    29
48c24d0b6d85 tuned signature;
wenzelm
parents: 62819
diff changeset
    30
62817
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    31
(* global options *)
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    32
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    33
val _ = PolyML.Compiler.reportUnreferencedIds := true;
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    34
val _ = PolyML.Compiler.reportExhaustiveHandlers := true;
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    35
val _ = PolyML.Compiler.printInAlphabeticalOrder := false;
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    36
val _ = PolyML.Compiler.maxInlineSize := 80;
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    37
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    38
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    39
(* context *)
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    40
62494
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
    41
type context =
62490
39d01eaf5292 ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents: 62489
diff changeset
    42
 {name_space: ML_Name_Space.T,
62716
d80b9f4990e4 explicit print_depth for the sake of Spec_Check.determine_type;
wenzelm
parents: 62668
diff changeset
    43
  print_depth: int option,
62493
dd154240a53c load secure.ML earlier;
wenzelm
parents: 62490
diff changeset
    44
  here: int -> string -> string,
62490
39d01eaf5292 ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents: 62489
diff changeset
    45
  print: string -> unit,
39d01eaf5292 ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents: 62489
diff changeset
    46
  error: string -> unit};
39d01eaf5292 ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents: 62489
diff changeset
    47
62817
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    48
fun make_context name_space : context =
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    49
 {name_space = name_space,
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    50
  print_depth = NONE,
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    51
  here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    52
  print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    53
  error = fn s => error s};
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    54
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    55
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    56
(* use operations *)
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    57
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    58
local
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    59
31312
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
    60
fun drop_newline s =
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
    61
  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
    62
  else s;
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
    63
62529
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 62508
diff changeset
    64
fun ml_input start_line name txt =
62504
f14f17e656a6 clarified modules;
wenzelm
parents: 62501
diff changeset
    65
  let
62662
291cc01f56f5 @{make_string} is available during Pure bootstrap;
wenzelm
parents: 62529
diff changeset
    66
    fun input line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
62504
f14f17e656a6 clarified modules;
wenzelm
parents: 62501
diff changeset
    67
          let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
62662
291cc01f56f5 @{make_string} is available during Pure bootstrap;
wenzelm
parents: 62529
diff changeset
    68
          in input line cs (s :: res) end
291cc01f56f5 @{make_string} is available during Pure bootstrap;
wenzelm
parents: 62529
diff changeset
    69
      | input line (#"@" :: #"{" :: #"m" :: #"a" :: #"k" :: #"e" :: #"_" ::
291cc01f56f5 @{make_string} is available during Pure bootstrap;
wenzelm
parents: 62529
diff changeset
    70
            #"s" :: #"t" :: #"r" :: #"i" :: #"n" :: #"g" :: #"}" :: cs) res =
291cc01f56f5 @{make_string} is available during Pure bootstrap;
wenzelm
parents: 62529
diff changeset
    71
          input line cs (ML_Pretty.make_string_fn "" :: res)
62877
741560a5283b avoid malformed Isabelle symbols during bootstrap;
wenzelm
parents: 62821
diff changeset
    72
      | input line (#"\\" :: #"<" :: cs) res = input line cs ("\092\092<" :: res)
62662
291cc01f56f5 @{make_string} is available during Pure bootstrap;
wenzelm
parents: 62529
diff changeset
    73
      | input line (#"\n" :: cs) res = input (line + 1) cs ("\n" :: res)
291cc01f56f5 @{make_string} is available during Pure bootstrap;
wenzelm
parents: 62529
diff changeset
    74
      | input line (c :: cs) res = input line cs (str c :: res)
291cc01f56f5 @{make_string} is available during Pure bootstrap;
wenzelm
parents: 62529
diff changeset
    75
      | input _ [] res = rev res;
291cc01f56f5 @{make_string} is available during Pure bootstrap;
wenzelm
parents: 62529
diff changeset
    76
  in String.concat (input start_line (String.explode txt) []) end;
62504
f14f17e656a6 clarified modules;
wenzelm
parents: 62501
diff changeset
    77
62817
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    78
in
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
    79
62716
d80b9f4990e4 explicit print_depth for the sake of Spec_Check.determine_type;
wenzelm
parents: 62668
diff changeset
    80
fun use_text ({name_space, print_depth, here, print, error, ...}: context)
d80b9f4990e4 explicit print_depth for the sake of Spec_Check.determine_type;
wenzelm
parents: 62668
diff changeset
    81
    {line, file, verbose, debug} text =
31312
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
    82
  let
60955
wenzelm
parents: 56435
diff changeset
    83
    val current_line = Unsynchronized.ref line;
62529
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 62508
diff changeset
    84
    val in_buffer = Unsynchronized.ref (String.explode (ml_input line file text));
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31480
diff changeset
    85
    val out_buffer = Unsynchronized.ref ([]: string list);
31312
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
    86
    fun output () = drop_newline (implode (rev (! out_buffer)));
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
    87
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
    88
    fun get () =
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
    89
      (case ! in_buffer of
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
    90
        [] => NONE
60955
wenzelm
parents: 56435
diff changeset
    91
      | c :: cs =>
wenzelm
parents: 56435
diff changeset
    92
          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
31312
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
    93
    fun put s = out_buffer := s :: ! out_buffer;
60955
wenzelm
parents: 56435
diff changeset
    94
    fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} =
31312
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
    95
     (put (if hard then "Error: " else "Warning: ");
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
    96
      PolyML.prettyPrint (put, 76) msg1;
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
    97
      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
62493
dd154240a53c load secure.ML earlier;
wenzelm
parents: 62490
diff changeset
    98
      put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n"));
31312
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
    99
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
   100
    val parameters =
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
   101
     [PolyML.Compiler.CPOutStream put,
31471
e3987b32e401 use_text: pass file name to compiler, tuned;
wenzelm
parents: 31433
diff changeset
   102
      PolyML.Compiler.CPNameSpace name_space,
31312
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
   103
      PolyML.Compiler.CPErrorMessageProc put_message,
60955
wenzelm
parents: 56435
diff changeset
   104
      PolyML.Compiler.CPLineNo (fn () => ! current_line),
wenzelm
parents: 56435
diff changeset
   105
      PolyML.Compiler.CPFileName file,
62501
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62494
diff changeset
   106
      PolyML.Compiler.CPPrintInAlphabeticalOrder false,
62716
d80b9f4990e4 explicit print_depth for the sake of Spec_Check.determine_type;
wenzelm
parents: 62668
diff changeset
   107
      PolyML.Compiler.CPDebug debug] @
d80b9f4990e4 explicit print_depth for the sake of Spec_Check.determine_type;
wenzelm
parents: 62668
diff changeset
   108
     (case print_depth of NONE => [] | SOME d => [PolyML.Compiler.CPPrintDepth (fn () => d)]);
31312
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
   109
    val _ =
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
   110
      (while not (List.null (! in_buffer)) do
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
   111
        PolyML.compiler (get, parameters) ())
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
   112
      handle exn =>
62505
9e2a65912111 clarified modules;
wenzelm
parents: 62504
diff changeset
   113
        if Exn.is_interrupt exn then Exn.reraise exn
39242
28d3809ff91f primitive use_text: let interrupts pass unhindered;
wenzelm
parents: 38470
diff changeset
   114
        else
28d3809ff91f primitive use_text: let interrupts pass unhindered;
wenzelm
parents: 38470
diff changeset
   115
         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
62505
9e2a65912111 clarified modules;
wenzelm
parents: 62504
diff changeset
   116
          error (output ()); Exn.reraise exn);
31312
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
   117
  in if verbose then print (output ()) else () end;
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
   118
62817
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
   119
end;
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
   120
60956
10d463883dc2 explicit debug flag for ML compiler;
wenzelm
parents: 60955
diff changeset
   121
fun use_file context {verbose, debug} file =
31312
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
   122
  let
60955
wenzelm
parents: 56435
diff changeset
   123
    val instream = TextIO.openIn file;
60956
10d463883dc2 explicit debug flag for ML compiler;
wenzelm
parents: 60955
diff changeset
   124
    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
10d463883dc2 explicit debug flag for ML compiler;
wenzelm
parents: 60955
diff changeset
   125
  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
31312
1c00e4ff3c99 more modular setup of runtime compilation;
wenzelm
parents:
diff changeset
   126
62817
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
   127
fun use_operations (use_ : bool option -> string -> unit) =
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
   128
  {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
   129
62490
39d01eaf5292 ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents: 62489
diff changeset
   130
62494
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
   131
fun debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
   132
  | debug_option (SOME debug) = debug;
62490
39d01eaf5292 ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents: 62489
diff changeset
   133
62817
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
   134
end;
62489
36f11bc393a2 use bootstrap compiler earlier;
wenzelm
parents: 62387
diff changeset
   135
62817
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
   136
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
   137
(* initial use operations *)
62494
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
   138
62493
dd154240a53c load secure.ML earlier;
wenzelm
parents: 62490
diff changeset
   139
val {use, use_debug, use_no_debug} =
62817
744bfd770123 clarified modules;
wenzelm
parents: 62716
diff changeset
   140
  let val context = ML_Compiler0.make_context ML_Name_Space.global in
62494
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
   141
    ML_Compiler0.use_operations (fn opt_debug => fn file =>
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
   142
      ML_Compiler0.use_file context
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
   143
        {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
   144
      handle ERROR msg => (#print context msg; raise error "ML error"))
b90109b2487c clarified modules;
wenzelm
parents: 62493
diff changeset
   145
  end;
62819
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62817
diff changeset
   146
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62817
diff changeset
   147
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62817
diff changeset
   148
(* export type-dependent functions *)
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62817
diff changeset
   149
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62817
diff changeset
   150
ML_Compiler0.use_text
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62817
diff changeset
   151
  (ML_Compiler0.make_context
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62817
diff changeset
   152
    (ML_Name_Space.global_values
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62817
diff changeset
   153
      [("prettyRepresentation", "ML_system_pretty"),
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62817
diff changeset
   154
       ("addPrettyPrinter", "ML_system_pp"),
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62817
diff changeset
   155
       ("addOverload", "ML_system_overload")]))
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62817
diff changeset
   156
  {debug = false, file = "", line = 0, verbose = false}
62886
72c475e03e22 simplified bootstrap: critical structures remain accessible in ML_Root context;
wenzelm
parents: 62877
diff changeset
   157
  "open PolyML RunCall" handle ERROR _ => ();