1(* Title: Pure/ML/ml_compiler0.ML 2 Author: Makarius 3 4Runtime compilation and evaluation for bootstrap. 5Initial ML file operations. 6*) 7 8signature ML_COMPILER0 = 9sig 10 type polyml_location = PolyML.location 11 type context = 12 {name_space: ML_Name_Space.T, 13 print_depth: int option, 14 here: int -> string -> string, 15 print: string -> unit, 16 error: string -> unit} 17 val make_context: ML_Name_Space.T -> context 18 val ML: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit 19 val ML_file: context -> {debug: bool, verbose: bool} -> string -> unit 20 val debug_option: bool option -> bool 21 val ML_file_operations: (bool option -> string -> unit) -> 22 {ML_file: string -> unit, ML_file_debug: string -> unit, ML_file_no_debug: string -> unit} 23end; 24 25structure ML_Compiler0: ML_COMPILER0 = 26struct 27 28type polyml_location = PolyML.location; 29 30 31(* global options *) 32 33val _ = PolyML.Compiler.reportUnreferencedIds := true; 34val _ = PolyML.Compiler.reportExhaustiveHandlers := true; 35val _ = PolyML.Compiler.printInAlphabeticalOrder := false; 36val _ = PolyML.Compiler.maxInlineSize := 80; 37 38 39(* context *) 40 41type context = 42 {name_space: ML_Name_Space.T, 43 print_depth: int option, 44 here: int -> string -> string, 45 print: string -> unit, 46 error: string -> unit}; 47 48fun make_context name_space : context = 49 {name_space = name_space, 50 print_depth = NONE, 51 here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")", 52 print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut), 53 error = fn s => error s}; 54 55 56(* ML file operations *) 57 58local 59 60fun drop_newline s = 61 if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) 62 else s; 63 64fun ml_input start_line name txt = 65 let 66 fun input line (#"\\" :: #"<" :: #"^" :: #"h" :: #"e" :: #"r" :: #"e" :: #">" :: cs) res = 67 let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")" 68 in input line cs (s :: res) end 69 | input line (#"@" :: #"{" :: #"m" :: #"a" :: #"k" :: #"e" :: #"_" :: 70 #"s" :: #"t" :: #"r" :: #"i" :: #"n" :: #"g" :: #"}" :: cs) res = 71 input line cs (ML_Pretty.make_string_fn :: res) 72 | input line (#"\\" :: #"<" :: cs) res = input line cs ("\092\092<" :: res) 73 | input line (#"\n" :: cs) res = input (line + 1) cs ("\n" :: res) 74 | input line (c :: cs) res = input line cs (str c :: res) 75 | input _ [] res = rev res; 76 in String.concat (input start_line (String.explode txt) []) end; 77 78in 79 80fun ML {name_space, print_depth, here, print, error, ...} {line, file, verbose, debug} text = 81 let 82 val current_line = Unsynchronized.ref line; 83 val in_buffer = Unsynchronized.ref (String.explode (ml_input line file text)); 84 val out_buffer = Unsynchronized.ref ([]: string list); 85 fun output () = drop_newline (implode (rev (! out_buffer))); 86 87 fun get () = 88 (case ! in_buffer of 89 [] => NONE 90 | c :: cs => 91 (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); 92 fun put s = out_buffer := s :: ! out_buffer; 93 fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} = 94 (put (if hard then "Error: " else "Warning: "); 95 PolyML.prettyPrint (put, 76) msg1; 96 (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2); 97 put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n")); 98 99 val parameters = 100 [PolyML.Compiler.CPOutStream put, 101 PolyML.Compiler.CPNameSpace name_space, 102 PolyML.Compiler.CPErrorMessageProc put_message, 103 PolyML.Compiler.CPLineNo (fn () => ! current_line), 104 PolyML.Compiler.CPFileName file, 105 PolyML.Compiler.CPPrintInAlphabeticalOrder false, 106 PolyML.Compiler.CPDebug debug] @ 107 (case print_depth of NONE => [] | SOME d => [PolyML.Compiler.CPPrintDepth (fn () => d)]); 108 val _ = 109 (while not (List.null (! in_buffer)) do 110 PolyML.compiler (get, parameters) ()) 111 handle exn => 112 if Exn.is_interrupt exn then Exn.reraise exn 113 else 114 (put ("Exception- " ^ General.exnMessage exn ^ " raised"); 115 error (output ()); Exn.reraise exn); 116 in if verbose then print (output ()) else () end; 117 118end; 119 120fun ML_file context {verbose, debug} file = 121 let 122 val instream = TextIO.openIn file; 123 val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); 124 in ML context {line = 1, file = file, verbose = verbose, debug = debug} text end; 125 126fun ML_file_operations (f: bool option -> string -> unit) = 127 {ML_file = f NONE, ML_file_debug = f (SOME true), ML_file_no_debug = f (SOME false)}; 128 129 130fun debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true" 131 | debug_option (SOME debug) = debug; 132 133end; 134 135 136(* initial ML_file operations *) 137 138val {ML_file, ML_file_debug, ML_file_no_debug} = 139 let val context = ML_Compiler0.make_context ML_Name_Space.global in 140 ML_Compiler0.ML_file_operations (fn opt_debug => fn file => 141 ML_Compiler0.ML_file context 142 {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file 143 handle ERROR msg => (#print context msg; raise error "ML error")) 144 end; 145 146 147(* export type-dependent functions *) 148 149if Thread_Data.is_virtual then () 150else 151 ML_Compiler0.ML 152 (ML_Compiler0.make_context 153 (ML_Name_Space.global_values 154 [("prettyRepresentation", "ML_system_pretty"), 155 ("addPrettyPrinter", "ML_system_pp"), 156 ("addOverload", "ML_system_overload")])) 157 {debug = false, file = "", line = 0, verbose = false} 158 "open PolyML RunCall"; 159 160ML_system_pp (fn depth => fn pretty => fn var => pretty (Synchronized.value var, depth)); 161