author | wenzelm |
Sun, 22 Mar 2009 19:12:36 +0100 | |
changeset 30640 | 3f3d1e218b64 |
child 30644 | 2948f4494e86 |
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 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
7 |
structure ML_Test = |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
8 |
struct |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
9 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
10 |
(* eval ML source tokens *) |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
11 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
12 |
fun eval pos toks = |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
13 |
let |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
14 |
val (print, err) = Output.ml_output; |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
15 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
16 |
val input = toks |> map (fn tok => |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
17 |
(serial (), (String.explode (ML_Lex.text_of tok), ML_Lex.pos_of tok))); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
18 |
val index_pos = Inttab.lookup (Inttab.make (map (apsnd snd) input)); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
19 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
20 |
fun pos_of ({file, startLine = line, startPosition = i, endPosition = j, ...}: location) = |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
21 |
(case (index_pos i, index_pos j) of |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
22 |
(SOME p, SOME q) => Position.encode_range (p, q) |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
23 |
| (SOME p, NONE) => p |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
24 |
| _ => Position.line_file line file); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
25 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
26 |
val in_buffer = ref (map (apsnd fst) input); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
27 |
val current_line = ref (the_default 1 (Position.line_of pos)); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
28 |
fun get () = |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
29 |
(case ! in_buffer of |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
30 |
[] => NONE |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
31 |
| (_, []) :: rest => (in_buffer := rest; get ()) |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
32 |
| (i, c :: cs) :: rest => |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
33 |
(in_buffer := (i, cs) :: rest; |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
34 |
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
|
35 |
SOME c)); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
36 |
fun get_index () = (case ! in_buffer of [] => 0 | (i, _) :: _ => i); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
37 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
38 |
val out_buffer = ref ([]: string list); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
39 |
fun put s = out_buffer := s :: ! out_buffer; |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
40 |
fun output () = implode (rev (! out_buffer)); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
41 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
42 |
fun put_message {message, hard, location, context = _} = |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
43 |
(put (if hard then "Error: " else "Warning: "); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
44 |
put (Pretty.string_of (Pretty.from_ML (pretty_ml message))); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
45 |
put (Position.str_of (pos_of location) ^ "\n")); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
46 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
47 |
val parameters = |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
48 |
[PolyML.Compiler.CPOutStream put, |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
49 |
PolyML.Compiler.CPNameSpace ML_Context.name_space, |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
50 |
PolyML.Compiler.CPErrorMessageProc put_message, |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
51 |
PolyML.Compiler.CPLineNo (fn () => ! current_line), |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
52 |
PolyML.Compiler.CPLineOffset get_index, |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
53 |
PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)), |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
54 |
PolyML.Compiler.CPPrintInAlphabeticalOrder false]; |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
55 |
val _ = |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
56 |
(while not (List.null (! in_buffer)) do |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
57 |
PolyML.compiler (get, parameters) ()) |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
58 |
handle exn => |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
59 |
(put ("Exception- " ^ General.exnMessage exn ^ " raised"); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
60 |
err (output ()); raise exn); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
61 |
in print (output ()) end; |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
62 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
63 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
64 |
(* ML test command *) |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
65 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
66 |
fun ML_test (txt, pos) = |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
67 |
let |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
68 |
val _ = Position.report Markup.ML_source pos; |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
69 |
val ants = (Symbol_Pos.explode (txt, pos), pos) |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
70 |
|> Antiquote.read ML_Lex.report_token ML_Lex.scan_antiq; |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
71 |
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
|
72 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
73 |
val _ = Context.setmp_thread_data env_ctxt |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
74 |
(fn () => (eval Position.none env; Context.thread_data ())) () |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
75 |
|> (fn NONE => () | SOME context' => Context.>> (ML_Context.inherit_env context')); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
76 |
val _ = eval pos body; |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
77 |
val _ = eval Position.none (ML_Lex.tokenize "structure Isabelle = struct end"); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
78 |
in () end; |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
79 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
80 |
local structure P = OuterParse and K = OuterKeyword in |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
81 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
82 |
val _ = |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
83 |
OuterSyntax.command "ML_test" "advanced ML compiler test" (K.tag_ml K.diag) |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
84 |
(P.ML_source >> (fn src => Toplevel.generic_theory |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
85 |
(ML_Context.exec (fn () => ML_test src)))); |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
86 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
87 |
end; |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
88 |
|
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
89 |
end; |
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset
|
90 |