Quelle  Introduction.thy

theory Introduction
imports Setup
begin (*<*)

ML ‹
 Isabelle_System.make_directory (File.tmp_path (Path.basic "examples"))
\<close> (*>*)

section ‹Introduction›

text ‹
 This tutorial introduces the code generator facilities of ‹Isabelle/HOL›. It allows to turn (a certain class of) HOL
 specifications into corresponding executable code in the programming
 languages ‹SML› cite‹SML›, ‹OCaml› cite‹OCaml›,
 ‹Haskell› cite‹"haskell-revised-report"› and ‹Scala›
 cite‹"scala-overview-tech-report"›.

 To profit from this tutorial, some familiarity and experience with
 Isabelle/HOL cite‹"isa-tutorial"› and its basic theories is assumed.
 ›


subsection ‹Code generation principle: shallow embedding \label{sec:principle}›

text ‹
 The key concept for understanding Isabelle's code generation is
 \emph{shallow embedding}: logical entities like constants, types and
 classes are identified with corresponding entities in the target
 language. In particular, the carrier of a generated program's
 semantics are \emph{equational theorems} from the logic. If we view
 a generated program as an implementation of a higher-order rewrite
 system, then every rewrite step performed by the program can be
 simulated in the logic, which guarantees partial correctness
 cite‹"Haftmann-Nipkow:2010:code"›.
 ›


subsection ‹A quick start with the Isabelle/HOL toolbox \label{sec:queue_example}›

text ‹
 In a HOL theory, the @{command_def datatype} and @{command_def
 definition}/@{command_def primrec}/@{command_def fun} declarations
 form the core of a functional programming language. By default
 equational theorems stemming from those are used for generated code,
 therefore \qt{naive} code generation can proceed without further
 ado.

 For example, here a simple \qt{implementation} of amortised queues:
 ›

datatype %quote 'a queue = AQueue "'a list" "'a list"

definition %quote empty :: "'a queue" where
  "empty = AQueue [] []"

primrec %quote enqueue :: "'a ==> 'a queue ==> 'a queue" where
  "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"

fun %quote dequeue :: "'a queue ==> 'a option × 'a queue" where
    "dequeue (AQueue [] []) = (None, AQueue [] [])"
  | "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
  | "dequeue (AQueue xs []) =
      (case rev xs of y # ys ==> (Some y, AQueue [] ys))" (*<*)

lemma %invisible dequeue_nonempty_Nil [simp]:
  "xs ≠ [] ==> dequeue (AQueue xs []) = (case rev xs of y # ys ==> (Some y, AQueue [] ys))"
  by (cases xs) (simp_all split: list.splits) (*>*)

text ‹\noindent Then we can generate code e.g.~for ‹SML› as follows:›

export_code %quote empty dequeue enqueue in SML module_name Example

text ‹\noindent resulting in the following code:›

text %quote ‹
 @{code_stmts empty enqueue dequeue (SML)}
 ›

text ‹
 \noindent The @{command_def export_code} command takes multiple constants
 for which code shall be generated; anything else needed for those is
 added implicitly. Then follows a target language identifier and a freely
 chosen 🪙‹module_name›.

 Output is written to a logical file-system within the theory context,
 with the theory name and ``🍋‹code›'' as overall prefix. There is also a
 formal session export using the same name: the result may be explored in
 the Isabelle/jEdit Prover IDE using the file-browser on the URL
 ``🍋‹isabelle-export:›''.

 The file name is determined by the target language together with an
 optional 🪙‹file_prefix› (the default is ``🍋‹export›'' with a consecutive
 number within the current theory). For ‹SML›, ‹OCaml› and ‹Scala›, the
 file prefix becomes a plain file with extension (e.g.\ ``🍋‹.ML›'' for
 SML). For ‹Haskell› the file prefix becomes a directory that is populated
 with a separate file for each module (with extension ``🍋‹.hs›'').

 Consider the following example:
 ›

export_code %quote empty dequeue enqueue in Haskell
  module_name Example file_prefix example

text ‹
 \noindent This is the corresponding code:
 ›

text %quote ‹
 @{code_stmts empty enqueue dequeue (Haskell)}
 ›

text ‹
 \noindent For more details about @{command export_code} see
 \secref{sec:further}.
 ›


subsection ‹Type classes›

text ‹
 Code can also be generated from type classes in a Haskell-like
 manner. For illustration here an example from abstract algebra:
 ›

class %quote semigroup =
  fixes mult :: "'a ==> 'a ==> 'a" (infixl ‹⊗› 70)
  assumes assoc: "(x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)"

class %quote monoid = semigroup +
  fixes neutral :: 'a (‹1›)
  assumes neutl: "1 ⊗ x = x"
    and neutr: "x ⊗ 1 = x"

instantiation %quote nat :: monoid
begin

primrec %quote mult_nat where
    "0 ⊗ n = (0::nat)"
  | "Suc m ⊗ n = n + m ⊗ n"

definition %quote neutral_nat where
  "1 = Suc 0"

lemma %quote add_mult_distrib:
  fixes n m q :: nat
  shows "(n + m) ⊗ q = n ⊗ q + m ⊗ q"
  by (induct n) simp_all

instance %quote proof
  fix m n q :: nat
  show "m ⊗ n ⊗ q = m ⊗ (n ⊗ q)"
    by (induct m) (simp_all add: add_mult_distrib)
  show "1 ⊗ n = n"
    by (simp add: neutral_nat_def)
  show "m ⊗ 1 = m"
    by (induct m) (simp_all add: neutral_nat_def)
qed

end %quote

text ‹
 \noindent We define the natural operation of the natural numbers
 on monoids:
 ›

primrec %quote (in monoid) pow :: "nat ==> 'a ==> 'a" where
    "pow 0 a = 1"
  | "pow (Suc n) a = a ⊗ pow n a"

text ‹
 \noindent This we use to define the discrete exponentiation
 function:
 ›

definition %quote bexp :: "nat ==> nat" where
  "bexp n = pow n (Suc (Suc 0))"

text ‹
 \noindent The corresponding code in Haskell uses that language's
 native classes:
 ›

text %quote ‹
 @{code_stmts bexp (Haskell)}
 ›

text ‹
 \noindent This is a convenient place to show how explicit dictionary
 construction manifests in generated code -- the same example in
 ‹SML›:
 ›

text %quote ‹
 @{code_stmts bexp (SML)}
 ›

text ‹
 \noindent Note the parameters with trailing underscore (🍋‹A_›), which are the dictionary parameters.
 ›


subsection ‹How to continue from here›

text ‹
 What you have seen so far should be already enough in a lot of
 cases. If you are content with this, you can quit reading here.

 Anyway, to understand situations where problems occur or to increase
 the scope of code generation beyond default, it is necessary to gain
 some understanding how the code generator actually works:

 \begin{itemize}

 \item The foundations of the code generator are described in
 \secref{sec:foundations}.

 \item In particular \secref{sec:utterly_wrong} gives hints how to
 debug situations where code generation does not succeed as
 expected.

 \item The scope and quality of generated code can be increased
 dramatically by applying refinement techniques, which are
 introduced in \secref{sec:refinement}.

 \item How to define partial functions such that code can be generated
 is explained in \secref{sec:partial}.

 \item Inductive predicates can be turned executable using an
 extension of the code generator \secref{sec:inductive}.

 \item If you want to utilize code generation to obtain fast
 evaluators e.g.~for decision procedures, have a look at
 \secref{sec:evaluation}.

 \item You may want to skim over the more technical sections
 \secref{sec:adaptation} and \secref{sec:further}.

 \item The target language Scala cite‹"scala-overview-tech-report"›
 comes with some specialities discussed in \secref{sec:scala}.

 \item For exhaustive syntax diagrams etc. you should visit the
 Isabelle/Isar Reference Manual cite‹"isabelle-isar-ref"›.

 \end{itemize}

 \bigskip

 \begin{center}\fbox{\fbox{\begin{minipage}{8cm}

 \begin{center}\textit{Happy proving, happy hacking!}\end{center}

 \end{minipage}}}\end{center}
 ›

end