src/Doc/Codegen/Further.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (23 months ago)
changeset 67022 49309fe530fd
parent 66453 cc19f7ca2ed6
child 67207 ad538f6c5d2f
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 theory Further
     2 imports Codegen_Basics.Setup
     3 begin
     4 
     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/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>
    57 
    58 subsection \<open>Specialities of the @{text Scala} target language \label{sec:scala}\<close>
    59 
    60 text \<open>
    61   @{text Scala} deviates from languages of the ML family in a couple
    62   of aspects; those which affect code generation mainly have to do with
    63   @{text Scala}'s type system:
    64 
    65   \begin{itemize}
    66 
    67     \item @{text Scala} prefers tupled syntax over curried syntax.
    68 
    69     \item @{text Scala} sacrifices Hindely-Milner type inference for a
    70       much more rich type system with subtyping etc.  For this reason
    71       type arguments sometimes have to be given explicitly in square
    72       brackets (mimicking System F syntax).
    73 
    74     \item In contrast to @{text Haskell} where most specialities of
    75       the type system are implemented using \emph{type classes},
    76       @{text Scala} provides a sophisticated system of \emph{implicit
    77       arguments}.
    78 
    79   \end{itemize}
    80 
    81   \noindent Concerning currying, the @{text Scala} serializer counts
    82   arguments in code equations to determine how many arguments
    83   shall be tupled; remaining arguments and abstractions in terms
    84   rather than function definitions are always curried.
    85 
    86   The second aspect affects user-defined adaptations with @{command
    87   code_printing}.  For regular terms, the @{text Scala} serializer prints
    88   all type arguments explicitly.  For user-defined term adaptations
    89   this is only possible for adaptations which take no arguments: here
    90   the type arguments are just appended.  Otherwise they are ignored;
    91   hence user-defined adaptations for polymorphic constants have to be
    92   designed very carefully to avoid ambiguity.
    93 \<close>
    94 
    95 
    96 subsection \<open>Modules namespace\<close>
    97 
    98 text \<open>
    99   When invoking the @{command export_code} command it is possible to
   100   leave out the @{keyword "module_name"} part; then code is
   101   distributed over different modules, where the module name space
   102   roughly is induced by the Isabelle theory name space.
   103 
   104   Then sometimes the awkward situation occurs that dependencies
   105   between definitions introduce cyclic dependencies between modules,
   106   which in the @{text Haskell} world leaves you to the mercy of the
   107   @{text Haskell} implementation you are using, while for @{text
   108   SML}/@{text OCaml} code generation is not possible.
   109 
   110   A solution is to declare module names explicitly.  Let use assume
   111   the three cyclically dependent modules are named \emph{A}, \emph{B}
   112   and \emph{C}.  Then, by stating
   113 \<close>
   114 
   115 code_identifier %quote
   116   code_module A \<rightharpoonup> (SML) ABC
   117 | code_module B \<rightharpoonup> (SML) ABC
   118 | code_module C \<rightharpoonup> (SML) ABC
   119 
   120 text \<open>
   121   \noindent we explicitly map all those modules on \emph{ABC},
   122   resulting in an ad-hoc merge of this three modules at serialisation
   123   time.
   124 \<close>
   125 
   126 subsection \<open>Locales and interpretation\<close>
   127 
   128 text \<open>
   129   A technical issue comes to surface when generating code from
   130   specifications stemming from locale interpretation into global
   131   theories.
   132 
   133   Let us assume a locale specifying a power operation on arbitrary
   134   types:
   135 \<close>
   136 
   137 locale %quote power =
   138   fixes power :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
   139   assumes power_commute: "power x \<circ> power y = power y \<circ> power x"
   140 begin
   141 
   142 text \<open>
   143   \noindent Inside that locale we can lift @{text power} to exponent
   144   lists by means of a specification relative to that locale:
   145 \<close>
   146 
   147 primrec %quote powers :: "'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   148   "powers [] = id"
   149 | "powers (x # xs) = power x \<circ> powers xs"
   150 
   151 lemma %quote powers_append:
   152   "powers (xs @ ys) = powers xs \<circ> powers ys"
   153   by (induct xs) simp_all
   154 
   155 lemma %quote powers_power:
   156   "powers xs \<circ> power x = power x \<circ> powers xs"
   157   by (induct xs)
   158     (simp_all del: o_apply id_apply add: comp_assoc,
   159       simp del: o_apply add: o_assoc power_commute)
   160 
   161 lemma %quote powers_rev:
   162   "powers (rev xs) = powers xs"
   163     by (induct xs) (simp_all add: powers_append powers_power)
   164 
   165 end %quote
   166 
   167 text \<open>
   168   After an interpretation of this locale (say, @{command_def
   169   global_interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f
   170   :: 'a \<Rightarrow> 'a). f ^^ n)"}), one could naively expect to have a constant @{text
   171   "fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"} for which code
   172   can be generated.  But this not the case: internally, the term
   173   @{text "fun_power.powers"} is an abbreviation for the foundational
   174   term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"}
   175   (see @{cite "isabelle-locale"} for the details behind).
   176 
   177   Fortunately, a succint solution is available: a dedicated
   178   rewrite definition:
   179 \<close>
   180 
   181 global_interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"
   182   defines funpows = fun_power.powers
   183   by unfold_locales
   184     (simp_all add: fun_eq_iff funpow_mult mult.commute)
   185 
   186 text \<open>
   187   \noindent This amends the interpretation morphisms such that
   188   occurrences of the foundational term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"}
   189   are folded to a newly defined constant @{const funpows}.
   190 
   191   After this setup procedure, code generation can continue as usual:
   192 \<close>
   193 
   194 text %quotetypewriter \<open>
   195   @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}
   196 \<close>
   197 
   198 
   199 subsection \<open>Parallel computation\<close>
   200 
   201 text \<open>
   202   Theory @{text Parallel} in \<^dir>\<open>~~/src/HOL/Library\<close> contains
   203   operations to exploit parallelism inside the Isabelle/ML
   204   runtime engine.
   205 \<close>
   206 
   207 subsection \<open>Imperative data structures\<close>
   208 
   209 text \<open>
   210   If you consider imperative data structures as inevitable for a
   211   specific application, you should consider \emph{Imperative
   212   Functional Programming with Isabelle/HOL}
   213   @{cite "bulwahn-et-al:2008:imperative"}; the framework described there
   214   is available in session @{text Imperative_HOL}, together with a
   215   short primer document.
   216 \<close>
   217 
   218 end