71888
|
1 |
(* Title: Pure/System/scala_compiler.ML
|
71881
|
2 |
Author: Makarius
|
|
3 |
|
71888
|
4 |
Scala compiler operations.
|
71881
|
5 |
*)
|
|
6 |
|
71888
|
7 |
signature SCALA_COMPILER =
|
71881
|
8 |
sig
|
71888
|
9 |
val toplevel: string -> unit
|
71887
|
10 |
val declaration: string -> unit
|
71881
|
11 |
end;
|
|
12 |
|
71888
|
13 |
structure Scala_Compiler: SCALA_COMPILER =
|
71881
|
14 |
struct
|
|
15 |
|
71887
|
16 |
(* check declaration *)
|
|
17 |
|
71888
|
18 |
fun toplevel source =
|
71881
|
19 |
let val errors =
|
71888
|
20 |
\<^scala>\<open>scala_toplevel\<close> source
|
71881
|
21 |
|> YXML.parse_body
|
|
22 |
|> let open XML.Decode in list string end
|
|
23 |
in if null errors then () else error (cat_lines errors) end;
|
|
24 |
|
71888
|
25 |
fun declaration source =
|
|
26 |
toplevel ("package test\nobject Test { " ^ source ^ " }");
|
|
27 |
|
71887
|
28 |
|
|
29 |
(* antiquotations *)
|
|
30 |
|
|
31 |
local
|
|
32 |
|
|
33 |
fun make_list bg en = space_implode "," #> enclose bg en;
|
|
34 |
|
|
35 |
fun print_args [] = ""
|
|
36 |
| print_args xs = make_list "(" ")" xs;
|
|
37 |
|
|
38 |
fun print_types [] = ""
|
|
39 |
| print_types Ts = make_list "[" "]" Ts;
|
|
40 |
|
|
41 |
fun print_class (c, Ts) = c ^ print_types Ts;
|
|
42 |
|
|
43 |
val types =
|
|
44 |
Scan.optional (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]") [];
|
|
45 |
|
|
46 |
val in_class =
|
|
47 |
Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "in" |-- Parse.name -- types --| Parse.$$$ ")");
|
|
48 |
|
|
49 |
val arguments =
|
|
50 |
(Parse.nat >> (fn n => replicate n "_") ||
|
|
51 |
Parse.list (Parse.underscore || Parse.name >> (fn T => "_ : " ^ T))) >> print_args
|
|
52 |
|| Scan.succeed " _";
|
|
53 |
|
|
54 |
val method_arguments = Scan.optional (Parse.$$$ "(" |-- arguments --| Parse.$$$ ")") " _";
|
|
55 |
|
|
56 |
in
|
|
57 |
|
|
58 |
val _ =
|
|
59 |
Theory.setup
|
|
60 |
(Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_type\<close>
|
|
61 |
(Scan.lift (Parse.embedded -- (types >> print_types)))
|
|
62 |
(fn _ => fn (t, type_args) =>
|
|
63 |
(declaration ("type _Test_" ^ type_args ^ " = " ^ t ^ type_args); t ^ type_args)) #>
|
|
64 |
|
|
65 |
Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_object\<close>
|
|
66 |
(Scan.lift Parse.embedded)
|
|
67 |
(fn _ => fn object => (declaration ("val _test_ = " ^ object); object)) #>
|
|
68 |
|
|
69 |
Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_method\<close>
|
|
70 |
(Scan.lift (Scan.option in_class -- Parse.embedded -- types -- method_arguments))
|
|
71 |
(fn _ => fn (((class, method), method_types), method_args) =>
|
|
72 |
let
|
|
73 |
val class_types = (case class of SOME (_, Ts) => Ts | NONE => []);
|
|
74 |
val def = "def _test_" ^ print_types (merge (op =) (method_types, class_types));
|
|
75 |
val def_context =
|
|
76 |
(case class of
|
|
77 |
NONE => def ^ " = "
|
|
78 |
| SOME c => def ^ "(_this_ : " ^ print_class c ^ ") = _this_.");
|
|
79 |
val source = def_context ^ method ^ method_args;
|
|
80 |
val _ = declaration source;
|
|
81 |
in (case class of NONE => method | SOME c => print_class c ^ "." ^ method) end));
|
|
82 |
|
71881
|
83 |
end;
|
71887
|
84 |
|
|
85 |
end;
|