37 all type arguments explicitly. For user-defined term adaptations |
37 all type arguments explicitly. For user-defined term adaptations |
38 this is only possible for adaptations which take no arguments: here |
38 this is only possible for adaptations which take no arguments: here |
39 the type arguments are just appended. Otherwise they are ignored; |
39 the type arguments are just appended. Otherwise they are ignored; |
40 hence user-defined adaptations for polymorphic constants have to be |
40 hence user-defined adaptations for polymorphic constants have to be |
41 designed very carefully to avoid ambiguity. |
41 designed very carefully to avoid ambiguity. |
42 |
42 \<close> |
43 Isabelle's type classes are mapped onto @{text Scala} implicits; in |
43 |
44 cases with diamonds in the subclass hierarchy this can lead to |
|
45 ambiguities in the generated code: |
|
46 \<close> |
|
47 |
|
48 class %quote class1 = |
|
49 fixes foo :: "'a \<Rightarrow> 'a" |
|
50 |
|
51 class %quote class2 = class1 |
|
52 |
|
53 class %quote class3 = class1 |
|
54 |
|
55 text \<open> |
|
56 \noindent Here both @{class class2} and @{class class3} inherit from @{class class1}, |
|
57 forming the upper part of a diamond. |
|
58 \<close> |
|
59 |
|
60 definition %quote bar :: "'a :: {class2, class3} \<Rightarrow> 'a" where |
|
61 "bar = foo" |
|
62 |
|
63 text \<open> |
|
64 \noindent This yields the following code: |
|
65 \<close> |
|
66 |
|
67 text %quotetypewriter \<open> |
|
68 @{code_stmts bar (Scala)} |
|
69 \<close> |
|
70 |
|
71 text \<open> |
|
72 \noindent This code is rejected by the @{text Scala} compiler: in |
|
73 the definition of @{text bar}, it is not clear from where to derive |
|
74 the implicit argument for @{text foo}. |
|
75 |
|
76 The solution to the problem is to close the diamond by a further |
|
77 class with inherits from both @{class class2} and @{class class3}: |
|
78 \<close> |
|
79 |
|
80 class %quote class4 = class2 + class3 |
|
81 |
|
82 text \<open> |
|
83 \noindent Then the offending code equation can be restricted to |
|
84 @{class class4}: |
|
85 \<close> |
|
86 |
|
87 lemma %quote [code]: |
|
88 "(bar :: 'a::class4 \<Rightarrow> 'a) = foo" |
|
89 by (simp only: bar_def) |
|
90 |
|
91 text \<open> |
|
92 \noindent with the following code: |
|
93 \<close> |
|
94 |
|
95 text %quotetypewriter \<open> |
|
96 @{code_stmts bar (Scala)} |
|
97 \<close> |
|
98 |
|
99 text \<open> |
|
100 \noindent which exposes no ambiguity. |
|
101 |
|
102 Since the preprocessor (cf.~\secref{sec:preproc}) propagates sort |
|
103 constraints through a system of code equations, it is usually not |
|
104 very difficult to identify the set of code equations which actually |
|
105 needs more restricted sort constraints. |
|
106 \<close> |
|
107 |
44 |
108 subsection \<open>Modules namespace\<close> |
45 subsection \<open>Modules namespace\<close> |
109 |
46 |
110 text \<open> |
47 text \<open> |
111 When invoking the @{command export_code} command it is possible to |
48 When invoking the @{command export_code} command it is possible to |