1 (* Title: Pure/ML/ml_compiler_polyml-5.3.ML |
|
2 Author: Makarius |
|
3 |
|
4 Advanced runtime compilation for Poly/ML 5.3.0 or later. |
|
5 *) |
|
6 |
|
7 structure ML_Compiler: ML_COMPILER = |
|
8 struct |
|
9 |
|
10 (* source locations *) |
|
11 |
|
12 fun position_of (loc: PolyML.location) = |
|
13 let |
|
14 val {file = text, startLine = line, startPosition = offset, |
|
15 endLine = _, endPosition = end_offset} = loc; |
|
16 val props = |
|
17 (case YXML.parse text of |
|
18 XML.Elem ((e, atts), _) => if e = Isabelle_Markup.positionN then atts else [] |
|
19 | XML.Text s => Position.file_name s); |
|
20 in |
|
21 Position.make {line = line, offset = offset, end_offset = end_offset, props = props} |
|
22 end; |
|
23 |
|
24 fun exn_position exn = |
|
25 (case PolyML.exceptionLocation exn of |
|
26 NONE => Position.none |
|
27 | SOME loc => position_of loc); |
|
28 |
|
29 val exn_messages = Runtime.exn_messages exn_position; |
|
30 val exn_message = Runtime.exn_message exn_position; |
|
31 |
|
32 |
|
33 (* parse trees *) |
|
34 |
|
35 fun report_parse_tree depth space = |
|
36 let |
|
37 val reported_text = |
|
38 (case Context.thread_data () of |
|
39 SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt |
|
40 | _ => Position.reported_text); |
|
41 |
|
42 fun reported_entity kind loc decl = |
|
43 reported_text (position_of loc) |
|
44 (Isabelle_Markup.entityN, |
|
45 (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) ""; |
|
46 |
|
47 fun reported loc (PolyML.PTtype types) = |
|
48 cons |
|
49 (PolyML.NameSpace.displayTypeExpression (types, depth, space) |
|
50 |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |
|
51 |> reported_text (position_of loc) Isabelle_Markup.ML_typing) |
|
52 | reported loc (PolyML.PTdeclaredAt decl) = |
|
53 cons (reported_entity Isabelle_Markup.ML_defN loc decl) |
|
54 | reported loc (PolyML.PTopenedAt decl) = |
|
55 cons (reported_entity Isabelle_Markup.ML_openN loc decl) |
|
56 | reported loc (PolyML.PTstructureAt decl) = |
|
57 cons (reported_entity Isabelle_Markup.ML_structN loc decl) |
|
58 | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ()) |
|
59 | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ()) |
|
60 | reported _ _ = I |
|
61 and reported_tree (loc, props) = fold (reported loc) props; |
|
62 in fn tree => Output.report (implode (reported_tree tree [])) end; |
|
63 |
|
64 |
|
65 (* eval ML source tokens *) |
|
66 |
|
67 fun eval verbose pos toks = |
|
68 let |
|
69 val _ = Secure.secure_mltext (); |
|
70 val space = ML_Env.name_space; |
|
71 |
|
72 |
|
73 (* input *) |
|
74 |
|
75 val location_props = |
|
76 op ^ (YXML.output_markup (Isabelle_Markup.position |> Markup.properties |
|
77 (filter (member (op =) |
|
78 [Isabelle_Markup.idN, Isabelle_Markup.fileN] o #1) (Position.properties_of pos)))); |
|
79 |
|
80 val input_buffer = |
|
81 Unsynchronized.ref (toks |> map |
|
82 (`(maps (String.explode o Symbol.esc) o Symbol.explode o ML_Lex.check_content_of))); |
|
83 |
|
84 fun get () = |
|
85 (case ! input_buffer of |
|
86 (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c) |
|
87 | ([], _) :: rest => (input_buffer := rest; SOME #" ") |
|
88 | [] => NONE); |
|
89 |
|
90 fun get_pos () = |
|
91 (case ! input_buffer of |
|
92 (_ :: _, tok) :: _ => ML_Lex.pos_of tok |
|
93 | ([], tok) :: _ => ML_Lex.end_pos_of tok |
|
94 | [] => Position.none); |
|
95 |
|
96 |
|
97 (* output channels *) |
|
98 |
|
99 val writeln_buffer = Unsynchronized.ref Buffer.empty; |
|
100 fun write s = Unsynchronized.change writeln_buffer (Buffer.add s); |
|
101 fun output_writeln () = writeln (Buffer.content (! writeln_buffer)); |
|
102 |
|
103 val warnings = Unsynchronized.ref ([]: string list); |
|
104 fun warn msg = Unsynchronized.change warnings (cons msg); |
|
105 fun output_warnings () = List.app warning (rev (! warnings)); |
|
106 |
|
107 val error_buffer = Unsynchronized.ref Buffer.empty; |
|
108 fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n"); |
|
109 fun flush_error () = writeln (Buffer.content (! error_buffer)); |
|
110 fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer))); |
|
111 |
|
112 fun message {message = msg, hard, location = loc, context = _} = |
|
113 let |
|
114 val pos = position_of loc; |
|
115 val txt = |
|
116 (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report) |
|
117 ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^ |
|
118 Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^ |
|
119 Position.reported_text pos Isabelle_Markup.report ""; |
|
120 in if hard then err txt else warn txt end; |
|
121 |
|
122 |
|
123 (* results *) |
|
124 |
|
125 val depth = get_print_depth (); |
|
126 |
|
127 fun apply_result {fixes, types, signatures, structures, functors, values} = |
|
128 let |
|
129 fun display disp x = |
|
130 if depth > 0 then |
|
131 (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n") |
|
132 else (); |
|
133 |
|
134 fun apply_fix (a, b) = |
|
135 (#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b)); |
|
136 fun apply_type (a, b) = |
|
137 (#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space)); |
|
138 fun apply_sig (a, b) = |
|
139 (#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space)); |
|
140 fun apply_struct (a, b) = |
|
141 (#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space)); |
|
142 fun apply_funct (a, b) = |
|
143 (#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space)); |
|
144 fun apply_val (a, b) = |
|
145 (#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space)); |
|
146 in |
|
147 List.app apply_fix fixes; |
|
148 List.app apply_type types; |
|
149 List.app apply_sig signatures; |
|
150 List.app apply_struct structures; |
|
151 List.app apply_funct functors; |
|
152 List.app apply_val values |
|
153 end; |
|
154 |
|
155 exception STATIC_ERRORS of unit; |
|
156 |
|
157 fun result_fun (phase1, phase2) () = |
|
158 ((case phase1 of |
|
159 NONE => () |
|
160 | SOME parse_tree => report_parse_tree depth space parse_tree); |
|
161 (case phase2 of |
|
162 NONE => raise STATIC_ERRORS () |
|
163 | SOME code => |
|
164 apply_result |
|
165 ((code |
|
166 |> Runtime.debugging |
|
167 |> Runtime.toplevel_error (err o exn_message)) ()))); |
|
168 |
|
169 |
|
170 (* compiler invocation *) |
|
171 |
|
172 val parameters = |
|
173 [PolyML.Compiler.CPOutStream write, |
|
174 PolyML.Compiler.CPNameSpace space, |
|
175 PolyML.Compiler.CPErrorMessageProc message, |
|
176 PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos), |
|
177 PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos), |
|
178 PolyML.Compiler.CPFileName location_props, |
|
179 PolyML.Compiler.CPCompilerResultFun result_fun, |
|
180 PolyML.Compiler.CPPrintInAlphabeticalOrder false]; |
|
181 val _ = |
|
182 (while not (List.null (! input_buffer)) do |
|
183 PolyML.compiler (get, parameters) ()) |
|
184 handle exn => |
|
185 if Exn.is_interrupt exn then reraise exn |
|
186 else |
|
187 let |
|
188 val exn_msg = |
|
189 (case exn of |
|
190 STATIC_ERRORS () => "" |
|
191 | Runtime.TOPLEVEL_ERROR => "" |
|
192 | _ => "Exception- " ^ General.exnMessage exn ^ " raised"); |
|
193 val _ = output_warnings (); |
|
194 val _ = output_writeln (); |
|
195 in raise_error exn_msg end; |
|
196 in |
|
197 if verbose then (output_warnings (); flush_error (); output_writeln ()) |
|
198 else () |
|
199 end; |
|
200 |
|
201 end; |
|
202 |
|