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