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