1 theory Further |
1 theory Further |
2 imports Setup |
2 imports Setup |
3 begin |
3 begin |
4 |
4 |
5 section \<open>Further issues \label{sec:further}\<close> |
5 section \<open>Further issues \label{sec:further}\<close> |
|
6 |
|
7 subsection \<open>Incorporating generated code directly into the system runtime -- @{text code_reflect}\<close> |
|
8 |
|
9 subsubsection \<open>Static embedding of generated code into the system runtime\<close> |
|
10 |
|
11 text \<open> |
|
12 The @{ML_antiquotation code} antiquotation is lightweight, but the generated code |
|
13 is only accessible while the ML section is processed. Sometimes this |
|
14 is not appropriate, especially if the generated code contains datatype |
|
15 declarations which are shared with other parts of the system. In these |
|
16 cases, @{command_def code_reflect} can be used: |
|
17 \<close> |
|
18 |
|
19 code_reflect %quote Sum_Type |
|
20 datatypes sum = Inl | Inr |
|
21 functions "Sum_Type.sum.projl" "Sum_Type.sum.projr" |
|
22 |
|
23 text \<open> |
|
24 \noindent @{command code_reflect} takes a structure name and |
|
25 references to datatypes and functions; for these code is compiled |
|
26 into the named ML structure and the \emph{Eval} target is modified |
|
27 in a way that future code generation will reference these |
|
28 precompiled versions of the given datatypes and functions. This |
|
29 also allows to refer to the referenced datatypes and functions from |
|
30 arbitrary ML code as well. |
|
31 |
|
32 A typical example for @{command code_reflect} can be found in the |
|
33 @{theory Predicate} theory. |
|
34 \<close> |
|
35 |
|
36 |
|
37 subsubsection \<open>Separate compilation\<close> |
|
38 |
|
39 text \<open> |
|
40 For technical reasons it is sometimes necessary to separate |
|
41 generation and compilation of code which is supposed to be used in |
|
42 the system runtime. For this @{command code_reflect} with an |
|
43 optional \<^theory_text>\<open>file\<close> argument can be used: |
|
44 \<close> |
|
45 |
|
46 code_reflect %quote Rat |
|
47 datatypes rat |
|
48 functions Fract |
|
49 "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)" |
|
50 "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)" |
|
51 file "$ISABELLE_TMP/examples/rat.ML" |
|
52 |
|
53 text \<open> |
|
54 \noindent This merely generates the referenced code to the given |
|
55 file which can be included into the system runtime later on. |
|
56 \<close> |
6 |
57 |
7 subsection \<open>Specialities of the @{text Scala} target language \label{sec:scala}\<close> |
58 subsection \<open>Specialities of the @{text Scala} target language \label{sec:scala}\<close> |
8 |
59 |
9 text \<open> |
60 text \<open> |
10 @{text Scala} deviates from languages of the ML family in a couple |
61 @{text Scala} deviates from languages of the ML family in a couple |