author | wenzelm |
Tue, 24 Mar 2009 16:11:09 +0100 | |
changeset 30705 | e8ab35c6ade6 |
parent 30704 | d6d4828e74a2 |
child 30709 | d9ca766bf24c |
permissions | -rw-r--r-- |
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML/ml_test.ML |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
3 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
4 |
Test of advanced ML compiler invocation in Poly/ML 5.3. |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
5 |
*) |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
6 |
|
30646 | 7 |
signature ML_TEST = |
8 |
sig |
|
30680 | 9 |
val eval: bool -> Position.T -> ML_Lex.token list -> unit |
30646 | 10 |
end |
11 |
||
12 |
structure ML_Test: ML_TEST = |
|
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
13 |
struct |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
14 |
|
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
15 |
(* extra ML environment *) |
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
16 |
|
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
17 |
structure Extra_Env = GenericDataFun |
30646 | 18 |
( |
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
19 |
type T = Position.T Inttab.table; (*position of registered tokens*) |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
20 |
val empty = Inttab.empty; |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
21 |
val extend = I; |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
22 |
fun merge _ = Inttab.merge (K true); |
30646 | 23 |
); |
24 |
||
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
25 |
fun inherit_env context = |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
26 |
ML_Context.inherit_env context #> |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
27 |
Extra_Env.put (Extra_Env.get context); |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
28 |
|
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
29 |
fun register_tokens toks context = |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
30 |
let |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
31 |
val regs = map (fn tok => (serial (), tok)) toks; |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
32 |
val context' = context |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
33 |
|> Extra_Env.map (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs); |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
34 |
in (regs, context') end; |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
35 |
|
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
36 |
fun pos_of_location context |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
37 |
({file, startLine = line, startPosition = i, endPosition = j, ...}: location) = |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
38 |
(case pairself (Inttab.lookup (Extra_Env.get context)) (i, j) of |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
39 |
(SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2) |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
40 |
| (SOME pos, NONE) => pos |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
41 |
| _ => Position.line_file line file); |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
42 |
|
30646 | 43 |
|
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
44 |
(* parse trees *) |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
45 |
|
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
46 |
fun report_parse_tree context = |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
47 |
let |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
48 |
val pos_of = pos_of_location context; |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
49 |
fun report loc (PTtype types) = (* FIXME body text *) |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
50 |
Position.report Markup.ML_typing (pos_of loc) |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
51 |
| report loc (PTdeclaredAt decl) = |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
52 |
Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) "" |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
53 |
|> Position.report_text Markup.ML_ref (pos_of loc) |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
54 |
| report _ (PTnextSibling tree) = report_tree (tree ()) |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
55 |
| report _ (PTfirstChild tree) = report_tree (tree ()) |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
56 |
| report _ _ = () |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
57 |
and report_tree (loc, props) = List.app (report loc) props; |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
58 |
in report_tree end; |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
59 |
|
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
60 |
|
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
61 |
(* eval ML source tokens *) |
30680 | 62 |
|
63 |
fun use_text ({name_space = space, print, error, ...}: use_context) verbose pos toks = |
|
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
64 |
let |
30680 | 65 |
(* input *) |
66 |
||
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
67 |
val input = Context.>>> (register_tokens toks); |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
68 |
val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input); |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
69 |
|
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
70 |
val current_line = ref (the_default 1 (Position.line_of pos)); |
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
71 |
|
30705
e8ab35c6ade6
get_index: produce index of next pending token, not the last one;
wenzelm
parents:
30704
diff
changeset
|
72 |
fun get_index () = |
e8ab35c6ade6
get_index: produce index of next pending token, not the last one;
wenzelm
parents:
30704
diff
changeset
|
73 |
the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer)); |
e8ab35c6ade6
get_index: produce index of next pending token, not the last one;
wenzelm
parents:
30704
diff
changeset
|
74 |
|
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
75 |
fun get () = |
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
76 |
(case ! input_buffer of |
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
77 |
[] => NONE |
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
78 |
| (_, []) :: rest => (input_buffer := rest; get ()) |
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
79 |
| (i, c :: cs) :: rest => |
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
80 |
(input_buffer := (i, cs) :: rest; |
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
81 |
if c = #"\n" then current_line := ! current_line + 1 else (); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
82 |
SOME c)); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
83 |
|
30680 | 84 |
|
85 |
(* output *) |
|
86 |
||
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
87 |
val output_buffer = ref Buffer.empty; |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
88 |
fun output () = Buffer.content (! output_buffer); |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
89 |
fun put s = change output_buffer (Buffer.add s); |
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
90 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
91 |
fun put_message {message, hard, location, context = _} = |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
92 |
(put (if hard then "Error: " else "Warning: "); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
93 |
put (Pretty.string_of (Pretty.from_ML (pretty_ml message))); |
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
94 |
put (Position.str_of (pos_of_location (the (Context.thread_data ())) location) ^ "\n")); |
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
95 |
|
30680 | 96 |
|
97 |
(* results *) |
|
98 |
||
99 |
fun apply_result {fixes, types, signatures, structures, functors, values} = |
|
100 |
let |
|
101 |
fun add_prefix prefix (PrettyBlock (ind, consistent, context, prts)) = |
|
102 |
let |
|
103 |
fun make_prefix context = |
|
104 |
(case get_first (fn ContextParentStructure p => SOME p | _ => NONE) context of |
|
105 |
SOME (name, sub_context) => make_prefix sub_context ^ name ^ "." |
|
106 |
| NONE => prefix); |
|
107 |
val this_prefix = make_prefix context; |
|
108 |
in PrettyBlock (ind, consistent, context, map (add_prefix this_prefix) prts) end |
|
109 |
| add_prefix prefix (prt as PrettyString s) = |
|
110 |
if prefix = "" then prt else PrettyString (prefix ^ s) |
|
111 |
| add_prefix _ (prt as PrettyBreak _) = prt; |
|
112 |
||
113 |
val depth = get_print_depth (); |
|
114 |
val with_struct = ! PolyML.Compiler.printTypesWithStructureName; |
|
115 |
||
116 |
fun display disp x = |
|
117 |
if depth > 0 then |
|
118 |
(disp x |
|
119 |
|> with_struct ? add_prefix "" |
|
120 |
|> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n") |
|
121 |
else (); |
|
122 |
||
123 |
fun apply_fix (a, b) = |
|
124 |
(display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b)); |
|
125 |
fun apply_type (a, b) = |
|
126 |
(display PolyML.NameSpace.displayType (b, depth); #enterType space (a, b)); |
|
127 |
fun apply_sig (a, b) = |
|
128 |
(display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b)); |
|
129 |
fun apply_struct (a, b) = |
|
130 |
(display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b)); |
|
131 |
fun apply_funct (a, b) = |
|
132 |
(display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b)); |
|
133 |
fun apply_val (a, b) = |
|
134 |
(display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b)); |
|
135 |
in |
|
136 |
List.app apply_fix fixes; |
|
137 |
List.app apply_type types; |
|
138 |
List.app apply_sig signatures; |
|
139 |
List.app apply_struct structures; |
|
140 |
List.app apply_funct functors; |
|
141 |
List.app apply_val values |
|
142 |
end; |
|
143 |
||
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
144 |
fun result_fun (phase1, phase2) () = |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
145 |
(case phase1 of NONE => () |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
146 |
| SOME parse_tree => report_parse_tree (the (Context.thread_data ())) parse_tree; |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
147 |
case phase2 of NONE => error "Static Errors" |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
148 |
| SOME code => apply_result (Toplevel.program code)); |
30680 | 149 |
|
150 |
||
151 |
(* compiler invocation *) |
|
30646 | 152 |
|
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
153 |
val parameters = |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
154 |
[PolyML.Compiler.CPOutStream put, |
30680 | 155 |
PolyML.Compiler.CPNameSpace space, |
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
156 |
PolyML.Compiler.CPErrorMessageProc put_message, |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
157 |
PolyML.Compiler.CPLineNo (fn () => ! current_line), |
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
158 |
PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)), |
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
159 |
PolyML.Compiler.CPLineOffset get_index, |
30680 | 160 |
PolyML.Compiler.CPCompilerResultFun result_fun]; |
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
161 |
val _ = |
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
162 |
(while not (List.null (! input_buffer)) do |
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
163 |
PolyML.compiler (get, parameters) ()) |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
164 |
handle exn => |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
165 |
(put ("Exception- " ^ General.exnMessage exn ^ " raised"); |
30677 | 166 |
error (output ()); raise exn); |
30680 | 167 |
in if verbose then print (output ()) else () end; |
168 |
||
169 |
val eval = use_text ML_Context.local_context; |
|
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
170 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
171 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
172 |
(* ML test command *) |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
173 |
|
30680 | 174 |
fun ML_test (txt, pos) = |
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
175 |
let |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
176 |
val _ = Position.report Markup.ML_source pos; |
30644 | 177 |
val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos); |
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
178 |
val ((env, body), env_ctxt) = ML_Context.eval_antiquotes (ants, pos) (Context.thread_data ()); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
179 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
180 |
val _ = Context.setmp_thread_data env_ctxt |
30680 | 181 |
(fn () => (eval false Position.none env; Context.thread_data ())) () |
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
182 |
|> (fn NONE => () | SOME context' => Context.>> (inherit_env context')); |
30680 | 183 |
val _ = eval true pos body; |
184 |
val _ = eval false Position.none (ML_Lex.tokenize "structure Isabelle = struct end"); |
|
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
185 |
in () end; |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
186 |
|
30644 | 187 |
|
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
188 |
local structure P = OuterParse and K = OuterKeyword in |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
189 |
|
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
190 |
fun propagate_env (context as Context.Proof lthy) = |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
191 |
Context.Proof (LocalTheory.map_contexts (inherit_env context) lthy) |
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
192 |
| propagate_env context = context; |
30644 | 193 |
|
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
194 |
val _ = |
30644 | 195 |
OuterSyntax.command "ML_test" "advanced ML compiler test" (K.tag_ml K.thy_decl) |
196 |
(P.ML_source >> (fn src => |
|
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset
|
197 |
Toplevel.generic_theory (ML_Context.exec (fn () => ML_test src) #> propagate_env))); |
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
198 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
199 |
end; |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
200 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
201 |
end; |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
202 |