src/Doc/Codegen/Introduction.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 66453 cc19f7ca2ed6
child 68484 59793df7f853
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
haftmann@28213
     1
theory Introduction
wenzelm@66453
     2
imports Codegen_Basics.Setup
haftmann@59378
     3
begin (*<*)
haftmann@59378
     4
haftmann@59378
     5
ML \<open>
haftmann@59378
     6
  Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples"))
haftmann@59378
     7
\<close> (*>*)
haftmann@28213
     8
haftmann@59377
     9
section \<open>Introduction\<close>
haftmann@38405
    10
haftmann@59377
    11
text \<open>
haftmann@38437
    12
  This tutorial introduces the code generator facilities of @{text
haftmann@38437
    13
  "Isabelle/HOL"}.  It allows to turn (a certain class of) HOL
haftmann@38437
    14
  specifications into corresponding executable code in the programming
wenzelm@58620
    15
  languages @{text SML} @{cite SML}, @{text OCaml} @{cite OCaml},
wenzelm@58620
    16
  @{text Haskell} @{cite "haskell-revised-report"} and @{text Scala}
wenzelm@58620
    17
  @{cite "scala-overview-tech-report"}.
haftmann@38405
    18
haftmann@38437
    19
  To profit from this tutorial, some familiarity and experience with
wenzelm@58620
    20
  @{theory HOL} @{cite "isa-tutorial"} and its basic theories is assumed.
haftmann@59377
    21
\<close>
haftmann@38405
    22
haftmann@38405
    23
haftmann@59377
    24
subsection \<open>Code generation principle: shallow embedding \label{sec:principle}\<close>
haftmann@28213
    25
haftmann@59377
    26
text \<open>
haftmann@38437
    27
  The key concept for understanding Isabelle's code generation is
haftmann@38437
    28
  \emph{shallow embedding}: logical entities like constants, types and
haftmann@38437
    29
  classes are identified with corresponding entities in the target
haftmann@38437
    30
  language.  In particular, the carrier of a generated program's
haftmann@38437
    31
  semantics are \emph{equational theorems} from the logic.  If we view
haftmann@38437
    32
  a generated program as an implementation of a higher-order rewrite
haftmann@38437
    33
  system, then every rewrite step performed by the program can be
haftmann@38437
    34
  simulated in the logic, which guarantees partial correctness
wenzelm@58620
    35
  @{cite "Haftmann-Nipkow:2010:code"}.
haftmann@59377
    36
\<close>
haftmann@28213
    37
haftmann@38437
    38
haftmann@59377
    39
subsection \<open>A quick start with the Isabelle/HOL toolbox \label{sec:queue_example}\<close>
haftmann@28419
    40
haftmann@59377
    41
text \<open>
blanchet@58310
    42
  In a HOL theory, the @{command_def datatype} and @{command_def
haftmann@38505
    43
  definition}/@{command_def primrec}/@{command_def fun} declarations
haftmann@38505
    44
  form the core of a functional programming language.  By default
haftmann@38505
    45
  equational theorems stemming from those are used for generated code,
haftmann@38505
    46
  therefore \qt{naive} code generation can proceed without further
haftmann@38505
    47
  ado.
haftmann@28419
    48
haftmann@28419
    49
  For example, here a simple \qt{implementation} of amortised queues:
haftmann@59377
    50
\<close>
haftmann@28419
    51
blanchet@58310
    52
datatype %quote 'a queue = AQueue "'a list" "'a list"
haftmann@28419
    53
haftmann@28564
    54
definition %quote empty :: "'a queue" where
haftmann@29798
    55
  "empty = AQueue [] []"
haftmann@28419
    56
haftmann@28564
    57
primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
haftmann@29798
    58
  "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
haftmann@28419
    59
haftmann@28564
    60
fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
haftmann@29798
    61
    "dequeue (AQueue [] []) = (None, AQueue [] [])"
haftmann@29798
    62
  | "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
haftmann@29798
    63
  | "dequeue (AQueue xs []) =
haftmann@38437
    64
      (case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))" (*<*)
haftmann@38437
    65
haftmann@38437
    66
lemma %invisible dequeue_nonempty_Nil [simp]:
haftmann@38437
    67
  "xs \<noteq> [] \<Longrightarrow> dequeue (AQueue xs []) = (case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))"
haftmann@38437
    68
  by (cases xs) (simp_all split: list.splits) (*>*)
haftmann@28419
    69
haftmann@59377
    70
text \<open>\noindent Then we can generate code e.g.~for @{text SML} as follows:\<close>
haftmann@28213
    71
haftmann@28564
    72
export_code %quote empty dequeue enqueue in SML
wenzelm@65981
    73
  module_name Example file "$ISABELLE_TMP/example.ML"
haftmann@28419
    74
haftmann@59377
    75
text \<open>\noindent resulting in the following code:\<close>
haftmann@28419
    76
haftmann@59377
    77
text %quotetypewriter \<open>
haftmann@39683
    78
  @{code_stmts empty enqueue dequeue (SML)}
haftmann@59377
    79
\<close>
haftmann@28419
    80
haftmann@59377
    81
text \<open>
haftmann@38505
    82
  \noindent The @{command_def export_code} command takes a
haftmann@38505
    83
  space-separated list of constants for which code shall be generated;
haftmann@38505
    84
  anything else needed for those is added implicitly.  Then follows a
haftmann@38505
    85
  target language identifier and a freely chosen module name.  A file
haftmann@38505
    86
  name denotes the destination to store the generated code.  Note that
haftmann@38505
    87
  the semantics of the destination depends on the target language: for
haftmann@38814
    88
  @{text SML}, @{text OCaml} and @{text Scala} it denotes a \emph{file},
haftmann@38814
    89
  for @{text Haskell} it denotes a \emph{directory} where a file named as the
haftmann@38437
    90
  module name (with extension @{text ".hs"}) is written:
haftmann@59377
    91
\<close>
haftmann@28419
    92
haftmann@28564
    93
export_code %quote empty dequeue enqueue in Haskell
haftmann@59334
    94
  module_name Example file "$ISABELLE_TMP/examples/"
haftmann@28419
    95
haftmann@59377
    96
text \<open>
haftmann@38437
    97
  \noindent This is the corresponding code:
haftmann@59377
    98
\<close>
haftmann@28419
    99
haftmann@59377
   100
text %quotetypewriter \<open>
haftmann@39683
   101
  @{code_stmts empty enqueue dequeue (Haskell)}
haftmann@59377
   102
\<close>
haftmann@28419
   103
haftmann@59377
   104
text \<open>
haftmann@38437
   105
  \noindent For more details about @{command export_code} see
haftmann@38437
   106
  \secref{sec:further}.
haftmann@59377
   107
\<close>
haftmann@28213
   108
haftmann@38437
   109
haftmann@59377
   110
subsection \<open>Type classes\<close>
haftmann@38402
   111
haftmann@59377
   112
text \<open>
haftmann@38437
   113
  Code can also be generated from type classes in a Haskell-like
haftmann@38437
   114
  manner.  For illustration here an example from abstract algebra:
haftmann@59377
   115
\<close>
haftmann@38402
   116
haftmann@38437
   117
class %quote semigroup =
haftmann@38437
   118
  fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
haftmann@38437
   119
  assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
haftmann@38437
   120
haftmann@38437
   121
class %quote monoid = semigroup +
haftmann@38437
   122
  fixes neutral :: 'a ("\<one>")
haftmann@38437
   123
  assumes neutl: "\<one> \<otimes> x = x"
haftmann@38437
   124
    and neutr: "x \<otimes> \<one> = x"
haftmann@38437
   125
haftmann@38437
   126
instantiation %quote nat :: monoid
haftmann@38437
   127
begin
haftmann@38437
   128
haftmann@38437
   129
primrec %quote mult_nat where
wenzelm@61076
   130
    "0 \<otimes> n = (0::nat)"
haftmann@38437
   131
  | "Suc m \<otimes> n = n + m \<otimes> n"
haftmann@38437
   132
haftmann@38437
   133
definition %quote neutral_nat where
haftmann@38437
   134
  "\<one> = Suc 0"
haftmann@38437
   135
haftmann@38437
   136
lemma %quote add_mult_distrib:
haftmann@38437
   137
  fixes n m q :: nat
haftmann@38437
   138
  shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q"
haftmann@38437
   139
  by (induct n) simp_all
haftmann@38437
   140
haftmann@38437
   141
instance %quote proof
haftmann@38437
   142
  fix m n q :: nat
haftmann@38437
   143
  show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
haftmann@38437
   144
    by (induct m) (simp_all add: add_mult_distrib)
haftmann@38437
   145
  show "\<one> \<otimes> n = n"
haftmann@38437
   146
    by (simp add: neutral_nat_def)
haftmann@38437
   147
  show "m \<otimes> \<one> = m"
haftmann@38437
   148
    by (induct m) (simp_all add: neutral_nat_def)
haftmann@38437
   149
qed
haftmann@38437
   150
haftmann@38437
   151
end %quote
haftmann@28213
   152
haftmann@59377
   153
text \<open>
haftmann@38437
   154
  \noindent We define the natural operation of the natural numbers
haftmann@38437
   155
  on monoids:
haftmann@59377
   156
\<close>
haftmann@38437
   157
haftmann@38437
   158
primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
haftmann@38437
   159
    "pow 0 a = \<one>"
haftmann@38437
   160
  | "pow (Suc n) a = a \<otimes> pow n a"
haftmann@28419
   161
haftmann@59377
   162
text \<open>
haftmann@38437
   163
  \noindent This we use to define the discrete exponentiation
haftmann@38437
   164
  function:
haftmann@59377
   165
\<close>
haftmann@38437
   166
haftmann@38437
   167
definition %quote bexp :: "nat \<Rightarrow> nat" where
haftmann@38437
   168
  "bexp n = pow n (Suc (Suc 0))"
haftmann@38437
   169
haftmann@59377
   170
text \<open>
haftmann@38437
   171
  \noindent The corresponding code in Haskell uses that language's
haftmann@38437
   172
  native classes:
haftmann@59377
   173
\<close>
haftmann@38437
   174
haftmann@59377
   175
text %quotetypewriter \<open>
haftmann@39683
   176
  @{code_stmts bexp (Haskell)}
haftmann@59377
   177
\<close>
haftmann@28419
   178
haftmann@59377
   179
text \<open>
haftmann@38437
   180
  \noindent This is a convenient place to show how explicit dictionary
haftmann@38437
   181
  construction manifests in generated code -- the same example in
haftmann@38437
   182
  @{text SML}:
haftmann@59377
   183
\<close>
haftmann@38437
   184
haftmann@59377
   185
text %quotetypewriter \<open>
haftmann@39683
   186
  @{code_stmts bexp (SML)}
haftmann@59377
   187
\<close>
haftmann@38437
   188
haftmann@59377
   189
text \<open>
haftmann@38437
   190
  \noindent Note the parameters with trailing underscore (@{verbatim
haftmann@38437
   191
  "A_"}), which are the dictionary parameters.
haftmann@59377
   192
\<close>
haftmann@38437
   193
haftmann@38437
   194
haftmann@59377
   195
subsection \<open>How to continue from here\<close>
haftmann@38437
   196
haftmann@59377
   197
text \<open>
haftmann@38437
   198
  What you have seen so far should be already enough in a lot of
haftmann@38437
   199
  cases.  If you are content with this, you can quit reading here.
haftmann@38437
   200
haftmann@38437
   201
  Anyway, to understand situations where problems occur or to increase
haftmann@38437
   202
  the scope of code generation beyond default, it is necessary to gain
haftmann@38437
   203
  some understanding how the code generator actually works:
haftmann@28419
   204
haftmann@28419
   205
  \begin{itemize}
haftmann@28419
   206
haftmann@38437
   207
    \item The foundations of the code generator are described in
haftmann@38437
   208
      \secref{sec:foundations}.
haftmann@38437
   209
haftmann@38437
   210
    \item In particular \secref{sec:utterly_wrong} gives hints how to
haftmann@38437
   211
      debug situations where code generation does not succeed as
haftmann@38437
   212
      expected.
haftmann@28419
   213
haftmann@38437
   214
    \item The scope and quality of generated code can be increased
haftmann@38437
   215
      dramatically by applying refinement techniques, which are
haftmann@38437
   216
      introduced in \secref{sec:refinement}.
haftmann@28419
   217
haftmann@38437
   218
    \item Inductive predicates can be turned executable using an
haftmann@38437
   219
      extension of the code generator \secref{sec:inductive}.
haftmann@38437
   220
haftmann@40753
   221
    \item If you want to utilize code generation to obtain fast
haftmann@40753
   222
      evaluators e.g.~for decision procedures, have a look at
haftmann@40753
   223
      \secref{sec:evaluation}.
haftmann@40753
   224
haftmann@38437
   225
    \item You may want to skim over the more technical sections
haftmann@38437
   226
      \secref{sec:adaptation} and \secref{sec:further}.
haftmann@38437
   227
wenzelm@58620
   228
    \item The target language Scala @{cite "scala-overview-tech-report"}
haftmann@42096
   229
      comes with some specialities discussed in \secref{sec:scala}.
haftmann@42096
   230
haftmann@38437
   231
    \item For exhaustive syntax diagrams etc. you should visit the
wenzelm@58620
   232
      Isabelle/Isar Reference Manual @{cite "isabelle-isar-ref"}.
haftmann@28419
   233
haftmann@28419
   234
  \end{itemize}
haftmann@28419
   235
haftmann@38437
   236
  \bigskip
haftmann@38437
   237
haftmann@38437
   238
  \begin{center}\fbox{\fbox{\begin{minipage}{8cm}
haftmann@38437
   239
haftmann@38437
   240
    \begin{center}\textit{Happy proving, happy hacking!}\end{center}
haftmann@38437
   241
haftmann@38437
   242
  \end{minipage}}}\end{center}
haftmann@59377
   243
\<close>
haftmann@28213
   244
haftmann@28213
   245
end
haftmann@46522
   246