author | wenzelm |
Sat, 06 Jun 2009 19:58:11 +0200 | |
changeset 31475 | 85e864045497 |
parent 31437 | 70309dc3deac |
child 31477 | ae1a00e1a2f6 |
permissions | -rw-r--r-- |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML/ml_compiler_polyml-5.3.ML |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
3 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
4 |
Advanced runtime compilation for Poly/ML 5.3 (SVN 762). |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
5 |
*) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
6 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
7 |
signature ML_COMPILER = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
8 |
sig |
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
9 |
val exception_position: exn -> Position.T |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
10 |
val eval: bool -> Position.T -> ML_Lex.token list -> unit |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
11 |
end |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
12 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
13 |
structure ML_Compiler: ML_COMPILER = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
14 |
struct |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
15 |
|
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
16 |
(* source locations *) |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
17 |
|
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
18 |
fun position_of (loc: PolyML.location) = |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
19 |
let |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
20 |
val {file = text, startLine = line, startPosition = offset, |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
21 |
endLine = end_line, endPosition = end_offset} = loc; |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
22 |
val loc_props = |
31434
1f9b6a5dc8cc
more robust treatment of bootstrap source positions;
wenzelm
parents:
31429
diff
changeset
|
23 |
(case YXML.parse text of |
1f9b6a5dc8cc
more robust treatment of bootstrap source positions;
wenzelm
parents:
31429
diff
changeset
|
24 |
XML.Elem (e, atts, _) => if e = Markup.positionN then atts else [] |
1f9b6a5dc8cc
more robust treatment of bootstrap source positions;
wenzelm
parents:
31429
diff
changeset
|
25 |
| XML.Text s => Position.file_name s); |
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
26 |
in |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
27 |
Position.value Markup.lineN line @ |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
28 |
Position.value Markup.offsetN offset @ |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
29 |
Position.value Markup.end_lineN end_line @ |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
30 |
Position.value Markup.end_offsetN end_offset @ |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
31 |
loc_props |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
32 |
end |> Position.of_properties; |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
33 |
|
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
34 |
fun exception_position exn = |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
35 |
(case PolyML.exceptionLocation exn of |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
36 |
NONE => Position.none |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
37 |
| SOME loc => position_of loc); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
38 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
39 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
40 |
(* parse trees *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
41 |
|
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
42 |
fun report_parse_tree depth space = |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
43 |
let |
31475 | 44 |
fun report_decl markup loc decl = |
45 |
Position.report_text Markup.ML_ref (position_of loc) |
|
46 |
(Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) ""); |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
47 |
fun report loc (PolyML.PTtype types) = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
48 |
PolyML.NameSpace.displayTypeExpression (types, depth, space) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
49 |
|> pretty_ml |> Pretty.from_ML |> Pretty.string_of |
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
50 |
|> Position.report_text Markup.ML_typing (position_of loc) |
31475 | 51 |
| report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl |
52 |
| report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl |
|
53 |
| report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
54 |
| report _ (PolyML.PTnextSibling tree) = report_tree (tree ()) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
55 |
| report _ (PolyML.PTfirstChild tree) = report_tree (tree ()) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
56 |
| report _ _ = () |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
57 |
and report_tree (loc, props) = List.app (report loc) props; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
58 |
in report_tree end; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
59 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
60 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
61 |
(* eval ML source tokens *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
62 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
63 |
fun eval verbose pos toks = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
64 |
let |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
65 |
val _ = Secure.secure_mltext (); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
66 |
val {name_space = space, print, error = err, ...} = ML_Env.local_context; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
67 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
68 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
69 |
(* input *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
70 |
|
31437 | 71 |
val location_props = |
72 |
Markup.markup (Markup.position |> Markup.properties |
|
73 |
(filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))) ""; |
|
74 |
||
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
75 |
val input = toks |> maps (fn tok => |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
76 |
let |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
77 |
val syms = Symbol.explode (ML_Lex.check_content_of tok); |
31437 | 78 |
val (ps, _) = fold_map (fn s => fn p => (p, Position.advance s p)) syms |
79 |
(Position.reset_range (ML_Lex.pos_of tok)); |
|
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
80 |
in ps ~~ map (String.explode o Symbol.esc) syms end); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
81 |
|
31475 | 82 |
val end_pos = |
83 |
if null toks then Position.none |
|
84 |
else ML_Lex.end_pos_of (List.last toks); |
|
85 |
||
86 |
val input_buffer = ref (input @ [(end_pos, [#"\n"])]); |
|
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
87 |
val line = ref (the_default 1 (Position.line_of pos)); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
88 |
|
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
89 |
fun get_offset () = |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
90 |
the_default 0 |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
91 |
(get_first (fn (_, []) => NONE | (p, _) => Position.offset_of p) (! input_buffer)); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
92 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
93 |
fun get () = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
94 |
(case ! input_buffer of |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
95 |
[] => NONE |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
96 |
| (_, []) :: rest => (input_buffer := rest; get ()) |
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
97 |
| (p, c :: cs) :: rest => |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
98 |
(input_buffer := (p, cs) :: rest; |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
99 |
if c = #"\n" then line := ! line + 1 else (); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
100 |
SOME c)); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
101 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
102 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
103 |
(* output *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
104 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
105 |
val output_buffer = ref Buffer.empty; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
106 |
fun output () = Buffer.content (! output_buffer); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
107 |
fun put s = change output_buffer (Buffer.add s); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
108 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
109 |
fun put_message {message, hard, location, context = _} = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
110 |
(put (if hard then "Error: " else "Warning: "); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
111 |
put (Pretty.string_of (Pretty.from_ML (pretty_ml message))); |
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
112 |
put (Position.str_of (position_of location) ^ "\n")); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
113 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
114 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
115 |
(* results *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
116 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
117 |
val depth = get_print_depth (); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
118 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
119 |
fun apply_result {fixes, types, signatures, structures, functors, values} = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
120 |
let |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
121 |
fun display disp x = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
122 |
if depth > 0 then |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
123 |
(disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n") |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
124 |
else (); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
125 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
126 |
fun apply_fix (a, b) = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
127 |
(display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b)); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
128 |
fun apply_type (a, b) = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
129 |
(display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b)); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
130 |
fun apply_sig (a, b) = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
131 |
(display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b)); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
132 |
fun apply_struct (a, b) = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
133 |
(display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b)); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
134 |
fun apply_funct (a, b) = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
135 |
(display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b)); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
136 |
fun apply_val (a, b) = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
137 |
(display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b)); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
138 |
in |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
139 |
List.app apply_fix fixes; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
140 |
List.app apply_type types; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
141 |
List.app apply_sig signatures; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
142 |
List.app apply_struct structures; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
143 |
List.app apply_funct functors; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
144 |
List.app apply_val values |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
145 |
end; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
146 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
147 |
fun result_fun (phase1, phase2) () = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
148 |
(case phase1 of NONE => () |
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
149 |
| SOME parse_tree => report_parse_tree depth space parse_tree; |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
150 |
case phase2 of NONE => err "Static Errors" |
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
151 |
| SOME code => apply_result (code ())); (* FIXME cf. Toplevel.program *) |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
152 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
153 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
154 |
(* compiler invocation *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
155 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
156 |
val parameters = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
157 |
[PolyML.Compiler.CPOutStream put, |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
158 |
PolyML.Compiler.CPNameSpace space, |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
159 |
PolyML.Compiler.CPErrorMessageProc put_message, |
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
160 |
PolyML.Compiler.CPLineNo (fn () => ! line), |
31475 | 161 |
PolyML.Compiler.CPLineOffset get_offset, |
31437 | 162 |
PolyML.Compiler.CPFileName location_props, |
31475 | 163 |
PolyML.Compiler.CPCompilerResultFun result_fun, |
164 |
PolyML.Compiler.CPPrintInAlphabeticalOrder false]; |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
165 |
val _ = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
166 |
(while not (List.null (! input_buffer)) do |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
167 |
PolyML.compiler (get, parameters) ()) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
168 |
handle exn => |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
169 |
(put ("Exception- " ^ General.exnMessage exn ^ " raised"); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
170 |
err (output ()); raise exn); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
171 |
in if verbose then print (output ()) else () end; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
172 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
173 |
end; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
174 |