src/Doc/Codegen/Further.thy
changeset 63303 7cffe366d333
parent 63241 f59fd6cc935e
child 63669 256fc20716f2
     1.1 --- a/src/Doc/Codegen/Further.thy	Tue Jun 14 15:54:28 2016 +0100
     1.2 +++ b/src/Doc/Codegen/Further.thy	Tue Jun 14 20:48:41 2016 +0200
     1.3 @@ -39,71 +39,8 @@
     1.4    the type arguments are just appended.  Otherwise they are ignored;
     1.5    hence user-defined adaptations for polymorphic constants have to be
     1.6    designed very carefully to avoid ambiguity.
     1.7 -
     1.8 -  Isabelle's type classes are mapped onto @{text Scala} implicits; in
     1.9 -  cases with diamonds in the subclass hierarchy this can lead to
    1.10 -  ambiguities in the generated code:
    1.11 -\<close>
    1.12 -
    1.13 -class %quote class1 =
    1.14 -  fixes foo :: "'a \<Rightarrow> 'a"
    1.15 -
    1.16 -class %quote class2 = class1
    1.17 -
    1.18 -class %quote class3 = class1
    1.19 -
    1.20 -text \<open>
    1.21 -  \noindent Here both @{class class2} and @{class class3} inherit from @{class class1},
    1.22 -  forming the upper part of a diamond.
    1.23 -\<close>
    1.24 -
    1.25 -definition %quote bar :: "'a :: {class2, class3} \<Rightarrow> 'a" where
    1.26 -  "bar = foo"
    1.27 -
    1.28 -text \<open>
    1.29 -  \noindent This yields the following code:
    1.30 -\<close>
    1.31 -
    1.32 -text %quotetypewriter \<open>
    1.33 -  @{code_stmts bar (Scala)}
    1.34  \<close>
    1.35  
    1.36 -text \<open>
    1.37 -  \noindent This code is rejected by the @{text Scala} compiler: in
    1.38 -  the definition of @{text bar}, it is not clear from where to derive
    1.39 -  the implicit argument for @{text foo}.
    1.40 -
    1.41 -  The solution to the problem is to close the diamond by a further
    1.42 -  class with inherits from both @{class class2} and @{class class3}:
    1.43 -\<close>
    1.44 -
    1.45 -class %quote class4 = class2 + class3
    1.46 -
    1.47 -text \<open>
    1.48 -  \noindent Then the offending code equation can be restricted to
    1.49 -  @{class class4}:
    1.50 -\<close>
    1.51 -
    1.52 -lemma %quote [code]:
    1.53 -  "(bar :: 'a::class4 \<Rightarrow> 'a) = foo"
    1.54 -  by (simp only: bar_def)
    1.55 -
    1.56 -text \<open>
    1.57 -  \noindent with the following code:
    1.58 -\<close>
    1.59 -
    1.60 -text %quotetypewriter \<open>
    1.61 -  @{code_stmts bar (Scala)}
    1.62 -\<close>
    1.63 -
    1.64 -text \<open>
    1.65 -  \noindent which exposes no ambiguity.
    1.66 -
    1.67 -  Since the preprocessor (cf.~\secref{sec:preproc}) propagates sort
    1.68 -  constraints through a system of code equations, it is usually not
    1.69 -  very difficult to identify the set of code equations which actually
    1.70 -  needs more restricted sort constraints.
    1.71 -\<close>
    1.72  
    1.73  subsection \<open>Modules namespace\<close>
    1.74