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