src/Doc/Codegen/Further.thy
changeset 59377 056945909f60
parent 59003 16d92d37a8a1
child 59378 065f349852e6
     1.1 --- a/src/Doc/Codegen/Further.thy	Thu Jan 15 13:39:41 2015 +0100
     1.2 +++ b/src/Doc/Codegen/Further.thy	Thu Jan 15 13:39:41 2015 +0100
     1.3 @@ -2,11 +2,11 @@
     1.4  imports Setup "~~/src/Tools/Permanent_Interpretation"
     1.5  begin
     1.6  
     1.7 -section {* Further issues \label{sec:further} *}
     1.8 +section \<open>Further issues \label{sec:further}\<close>
     1.9  
    1.10 -subsection {* Specialities of the @{text Scala} target language \label{sec:scala} *}
    1.11 +subsection \<open>Specialities of the @{text Scala} target language \label{sec:scala}\<close>
    1.12  
    1.13 -text {*
    1.14 +text \<open>
    1.15    @{text Scala} deviates from languages of the ML family in a couple
    1.16    of aspects; those which affect code generation mainly have to do with
    1.17    @{text Scala}'s type system:
    1.18 @@ -43,7 +43,7 @@
    1.19    Isabelle's type classes are mapped onto @{text Scala} implicits; in
    1.20    cases with diamonds in the subclass hierarchy this can lead to
    1.21    ambiguities in the generated code:
    1.22 -*}
    1.23 +\<close>
    1.24  
    1.25  class %quote class1 =
    1.26    fixes foo :: "'a \<Rightarrow> 'a"
    1.27 @@ -52,62 +52,62 @@
    1.28  
    1.29  class %quote class3 = class1
    1.30  
    1.31 -text {*
    1.32 +text \<open>
    1.33    \noindent Here both @{class class2} and @{class class3} inherit from @{class class1},
    1.34    forming the upper part of a diamond.
    1.35 -*}
    1.36 +\<close>
    1.37  
    1.38  definition %quote bar :: "'a :: {class2, class3} \<Rightarrow> 'a" where
    1.39    "bar = foo"
    1.40  
    1.41 -text {*
    1.42 +text \<open>
    1.43    \noindent This yields the following code:
    1.44 -*}
    1.45 +\<close>
    1.46  
    1.47 -text %quotetypewriter {*
    1.48 +text %quotetypewriter \<open>
    1.49    @{code_stmts bar (Scala)}
    1.50 -*}
    1.51 +\<close>
    1.52  
    1.53 -text {*
    1.54 +text \<open>
    1.55    \noindent This code is rejected by the @{text Scala} compiler: in
    1.56    the definition of @{text bar}, it is not clear from where to derive
    1.57    the implicit argument for @{text foo}.
    1.58  
    1.59    The solution to the problem is to close the diamond by a further
    1.60    class with inherits from both @{class class2} and @{class class3}:
    1.61 -*}
    1.62 +\<close>
    1.63  
    1.64  class %quote class4 = class2 + class3
    1.65  
    1.66 -text {*
    1.67 +text \<open>
    1.68    \noindent Then the offending code equation can be restricted to
    1.69    @{class class4}:
    1.70 -*}
    1.71 +\<close>
    1.72  
    1.73  lemma %quote [code]:
    1.74    "(bar :: 'a::class4 \<Rightarrow> 'a) = foo"
    1.75    by (simp only: bar_def)
    1.76  
    1.77 -text {*
    1.78 +text \<open>
    1.79    \noindent with the following code:
    1.80 -*}
    1.81 +\<close>
    1.82  
    1.83 -text %quotetypewriter {*
    1.84 +text %quotetypewriter \<open>
    1.85    @{code_stmts bar (Scala)}
    1.86 -*}
    1.87 +\<close>
    1.88  
    1.89 -text {*
    1.90 +text \<open>
    1.91    \noindent which exposes no ambiguity.
    1.92  
    1.93    Since the preprocessor (cf.~\secref{sec:preproc}) propagates sort
    1.94    constraints through a system of code equations, it is usually not
    1.95    very difficult to identify the set of code equations which actually
    1.96    needs more restricted sort constraints.
    1.97 -*}
    1.98 +\<close>
    1.99  
   1.100 -subsection {* Modules namespace *}
   1.101 +subsection \<open>Modules namespace\<close>
   1.102  
   1.103 -text {*
   1.104 +text \<open>
   1.105    When invoking the @{command export_code} command it is possible to
   1.106    leave out the @{keyword "module_name"} part; then code is
   1.107    distributed over different modules, where the module name space
   1.108 @@ -122,38 +122,38 @@
   1.109    A solution is to declare module names explicitly.  Let use assume
   1.110    the three cyclically dependent modules are named \emph{A}, \emph{B}
   1.111    and \emph{C}.  Then, by stating
   1.112 -*}
   1.113 +\<close>
   1.114  
   1.115  code_identifier %quote
   1.116    code_module A \<rightharpoonup> (SML) ABC
   1.117  | code_module B \<rightharpoonup> (SML) ABC
   1.118  | code_module C \<rightharpoonup> (SML) ABC
   1.119  
   1.120 -text {*
   1.121 +text \<open>
   1.122    \noindent we explicitly map all those modules on \emph{ABC},
   1.123    resulting in an ad-hoc merge of this three modules at serialisation
   1.124    time.
   1.125 -*}
   1.126 +\<close>
   1.127  
   1.128 -subsection {* Locales and interpretation *}
   1.129 +subsection \<open>Locales and interpretation\<close>
   1.130  
   1.131 -text {*
   1.132 +text \<open>
   1.133    A technical issue comes to surface when generating code from
   1.134    specifications stemming from locale interpretation.
   1.135  
   1.136    Let us assume a locale specifying a power operation on arbitrary
   1.137    types:
   1.138 -*}
   1.139 +\<close>
   1.140  
   1.141  locale %quote power =
   1.142    fixes power :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
   1.143    assumes power_commute: "power x \<circ> power y = power y \<circ> power x"
   1.144  begin
   1.145  
   1.146 -text {*
   1.147 +text \<open>
   1.148    \noindent Inside that locale we can lift @{text power} to exponent
   1.149    lists by means of specification relative to that locale:
   1.150 -*}
   1.151 +\<close>
   1.152  
   1.153  primrec %quote powers :: "'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   1.154    "powers [] = id"
   1.155 @@ -175,7 +175,7 @@
   1.156  
   1.157  end %quote
   1.158  
   1.159 -text {*
   1.160 +text \<open>
   1.161    After an interpretation of this locale (say, @{command_def
   1.162    interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f
   1.163    :: 'a \<Rightarrow> 'a). f ^^ n)"}), one would expect to have a constant @{text
   1.164 @@ -189,43 +189,43 @@
   1.165    achieved.  First, a dedicated definition of the constant on which
   1.166    the local @{text "powers"} after interpretation is supposed to be
   1.167    mapped on:
   1.168 -*}
   1.169 +\<close>
   1.170  
   1.171  definition %quote funpows :: "nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
   1.172    [code del]: "funpows = power.powers (\<lambda>n f. f ^^ n)"
   1.173  
   1.174 -text {*
   1.175 +text \<open>
   1.176    \noindent In general, the pattern is @{text "c = t"} where @{text c}
   1.177    is the name of the future constant and @{text t} the foundational
   1.178    term corresponding to the local constant after interpretation.
   1.179  
   1.180    The interpretation itself is enriched with an equation @{text "t = c"}:
   1.181 -*}
   1.182 +\<close>
   1.183  
   1.184  interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)" where
   1.185    "power.powers (\<lambda>n f. f ^^ n) = funpows"
   1.186    by unfold_locales
   1.187      (simp_all add: fun_eq_iff funpow_mult mult.commute funpows_def)
   1.188  
   1.189 -text {*
   1.190 +text \<open>
   1.191    \noindent This additional equation is trivially proved by the
   1.192    definition itself.
   1.193  
   1.194    After this setup procedure, code generation can continue as usual:
   1.195 -*}
   1.196 +\<close>
   1.197  
   1.198 -text %quotetypewriter {*
   1.199 +text %quotetypewriter \<open>
   1.200    @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}
   1.201 -*} (*<*)
   1.202 +\<close> (*<*)
   1.203  
   1.204 -(*>*) text {*
   1.205 +(*>*) text \<open>
   1.206    Fortunately, an even more succint approach is available using command
   1.207    @{command permanent_interpretation}.  This is available
   1.208    by importing theory @{file "~~/src/Tools/Permanent_Interpretation.thy"}.
   1.209    Then the pattern above collapses to
   1.210 -*} (*<*)
   1.211 +\<close> (*<*)
   1.212  
   1.213 -setup {* Sign.add_path "funpows" *}
   1.214 +setup \<open>Sign.add_path "funpows"\<close>
   1.215  hide_const (open) funpows
   1.216  
   1.217  (*>*)
   1.218 @@ -234,43 +234,43 @@
   1.219    by unfold_locales
   1.220      (simp_all add: fun_eq_iff funpow_mult mult.commute) (*<*)
   1.221  
   1.222 -setup {* Sign.parent_path *}
   1.223 +setup \<open>Sign.parent_path\<close>
   1.224  
   1.225  (*>*)
   1.226  
   1.227  
   1.228 -subsection {* Parallel computation *}
   1.229 +subsection \<open>Parallel computation\<close>
   1.230  
   1.231 -text {*
   1.232 +text \<open>
   1.233    Theory @{text Parallel} in @{file "~~/src/HOL/Library"} contains
   1.234    operations to exploit parallelism inside the Isabelle/ML
   1.235    runtime engine.
   1.236 -*}
   1.237 +\<close>
   1.238  
   1.239 -subsection {* Imperative data structures *}
   1.240 +subsection \<open>Imperative data structures\<close>
   1.241  
   1.242 -text {*
   1.243 +text \<open>
   1.244    If you consider imperative data structures as inevitable for a
   1.245    specific application, you should consider \emph{Imperative
   1.246    Functional Programming with Isabelle/HOL}
   1.247    @{cite "bulwahn-et-al:2008:imperative"}; the framework described there
   1.248    is available in session @{text Imperative_HOL}, together with a
   1.249    short primer document.
   1.250 -*}
   1.251 +\<close>
   1.252  
   1.253  
   1.254 -subsection {* ML system interfaces \label{sec:ml} *}
   1.255 +subsection \<open>ML system interfaces \label{sec:ml}\<close>
   1.256  
   1.257 -text {*
   1.258 +text \<open>
   1.259    Since the code generator framework not only aims to provide a nice
   1.260    Isar interface but also to form a base for code-generation-based
   1.261    applications, here a short description of the most fundamental ML
   1.262    interfaces.
   1.263 -*}
   1.264 +\<close>
   1.265  
   1.266 -subsubsection {* Managing executable content *}
   1.267 +subsubsection \<open>Managing executable content\<close>
   1.268  
   1.269 -text %mlref {*
   1.270 +text %mlref \<open>
   1.271    \begin{mldecls}
   1.272    @{index_ML Code.read_const: "theory -> string -> string"} \\
   1.273    @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
   1.274 @@ -322,12 +322,12 @@
   1.275       if @{text const} is no constructor.
   1.276  
   1.277    \end{description}
   1.278 -*}
   1.279 +\<close>
   1.280  
   1.281  
   1.282 -subsubsection {* Data depending on the theory's executable content *}
   1.283 +subsubsection \<open>Data depending on the theory's executable content\<close>
   1.284  
   1.285 -text {*
   1.286 +text \<open>
   1.287    Implementing code generator applications on top of the framework set
   1.288    out so far usually not only involves using those primitive
   1.289    interfaces but also storing code-dependent data and various other
   1.290 @@ -373,7 +373,7 @@
   1.291    \item @{text change_yield} update with side result.
   1.292  
   1.293    \end{description}
   1.294 -*}
   1.295 +\<close>
   1.296  
   1.297  end
   1.298