--- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Wed Mar 04 11:05:02 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,534 +0,0 @@
-theory Program
-imports Introduction
-begin
-
-section {* Turning Theories into Programs \label{sec:program} *}
-
-subsection {* The @{text "Isabelle/HOL"} default setup *}
-
-text {*
- We have already seen how by default equations stemming from
- @{command definition}/@{command primrec}/@{command fun}
- statements are used for code generation. This default behaviour
- can be changed, e.g. by providing different code equations.
- All kinds of customisation shown in this section is \emph{safe}
- in the sense that the user does not have to worry about
- correctness -- all programs generatable that way are partially
- correct.
-*}
-
-subsection {* Selecting code equations *}
-
-text {*
- Coming back to our introductory example, we
- could provide an alternative code equations for @{const dequeue}
- explicitly:
-*}
-
-lemma %quote [code]:
- "dequeue (AQueue xs []) =
- (if xs = [] then (None, AQueue [] [])
- else dequeue (AQueue [] (rev xs)))"
- "dequeue (AQueue xs (y # ys)) =
- (Some y, AQueue xs ys)"
- by (cases xs, simp_all) (cases "rev xs", simp_all)
-
-text {*
- \noindent The annotation @{text "[code]"} is an @{text Isar}
- @{text attribute} which states that the given theorems should be
- considered as code equations for a @{text fun} statement --
- the corresponding constant is determined syntactically. The resulting code:
-*}
-
-text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
-
-text {*
- \noindent You may note that the equality test @{term "xs = []"} has been
- replaced by the predicate @{term "null xs"}. This is due to the default
- setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
-
- Changing the default constructor set of datatypes is also
- possible. See \secref{sec:datatypes} for an example.
-
- As told in \secref{sec:concept}, code generation is based
- on a structured collection of code theorems.
- For explorative purpose, this collection
- may be inspected using the @{command code_thms} command:
-*}
-
-code_thms %quote dequeue
-
-text {*
- \noindent prints a table with \emph{all} code equations
- for @{const dequeue}, including
- \emph{all} code equations those equations depend
- on recursively.
-
- Similarly, the @{command code_deps} command shows a graph
- visualising dependencies between code equations.
-*}
-
-subsection {* @{text class} and @{text instantiation} *}
-
-text {*
- Concerning type classes and code generation, let us examine an example
- from abstract algebra:
-*}
-
-class %quote semigroup =
- fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
- assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
-
-class %quote monoid = semigroup +
- fixes neutral :: 'a ("\<one>")
- assumes neutl: "\<one> \<otimes> x = x"
- and neutr: "x \<otimes> \<one> = x"
-
-instantiation %quote nat :: monoid
-begin
-
-primrec %quote mult_nat where
- "0 \<otimes> n = (0\<Colon>nat)"
- | "Suc m \<otimes> n = n + m \<otimes> n"
-
-definition %quote neutral_nat where
- "\<one> = Suc 0"
-
-lemma %quote add_mult_distrib:
- fixes n m q :: nat
- shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q"
- by (induct n) simp_all
-
-instance %quote proof
- fix m n q :: nat
- show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
- by (induct m) (simp_all add: add_mult_distrib)
- show "\<one> \<otimes> n = n"
- by (simp add: neutral_nat_def)
- show "m \<otimes> \<one> = 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 \<Rightarrow> 'a \<Rightarrow> 'a" where
- "pow 0 a = \<one>"
- | "pow (Suc n) a = a \<otimes> pow n a"
-
-text {*
- \noindent This we use to define the discrete exponentiation function:
-*}
-
-definition %quote bexp :: "nat \<Rightarrow> nat" where
- "bexp n = pow n (Suc (Suc 0))"
-
-text {*
- \noindent The corresponding code:
-*}
-
-text %quote {*@{code_stmts bexp (Haskell)}*}
-
-text {*
- \noindent This is a convenient place to show how explicit dictionary construction
- manifests in generated code (here, the same example in @{text SML}):
-*}
-
-text %quote {*@{code_stmts bexp (SML)}*}
-
-text {*
- \noindent Note the parameters with trailing underscore (@{verbatim "A_"})
- which are the dictionary parameters.
-*}
-
-subsection {* The preprocessor \label{sec:preproc} *}
-
-text {*
- Before selected function theorems are turned into abstract
- code, a chain of definitional transformation steps is carried
- out: \emph{preprocessing}. In essence, the preprocessor
- consists of two components: a \emph{simpset} and \emph{function transformers}.
-
- The \emph{simpset} allows to employ the full generality of the Isabelle
- simplifier. Due to the interpretation of theorems
- as code equations, rewrites are applied to the right
- hand side and the arguments of the left hand side of an
- equation, but never to the constant heading the left hand side.
- An important special case are \emph{inline theorems} which may be
- declared and undeclared using the
- \emph{code inline} or \emph{code inline del} attribute respectively.
-
- Some common applications:
-*}
-
-text_raw {*
- \begin{itemize}
-*}
-
-text {*
- \item replacing non-executable constructs by executable ones:
-*}
-
-lemma %quote [code inline]:
- "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
-
-text {*
- \item eliminating superfluous constants:
-*}
-
-lemma %quote [code inline]:
- "1 = Suc 0" by simp
-
-text {*
- \item replacing executable but inconvenient constructs:
-*}
-
-lemma %quote [code inline]:
- "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
-
-text_raw {*
- \end{itemize}
-*}
-
-text {*
- \noindent \emph{Function transformers} provide a very general interface,
- transforming a list of function theorems to another
- list of function theorems, provided that neither the heading
- constant nor its type change. The @{term "0\<Colon>nat"} / @{const Suc}
- pattern elimination implemented in
- theory @{text Efficient_Nat} (see \secref{eff_nat}) uses this
- interface.
-
- \noindent The current setup of the preprocessor may be inspected using
- the @{command print_codesetup} command.
- @{command code_thms} provides a convenient
- mechanism to inspect the impact of a preprocessor setup
- on code equations.
-
- \begin{warn}
- The attribute \emph{code unfold}
- associated with the @{text "SML code generator"} also applies to
- the @{text "generic code generator"}:
- \emph{code unfold} implies \emph{code inline}.
- \end{warn}
-*}
-
-subsection {* Datatypes \label{sec:datatypes} *}
-
-text {*
- Conceptually, any datatype is spanned by a set of
- \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
- "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
- @{text "\<tau>"}. The HOL datatype package by default registers any new
- datatype in the table of datatypes, which may be inspected using the
- @{command print_codesetup} command.
-
- In some cases, it is appropriate to alter or extend this table. As
- an example, we will develop an alternative representation of the
- queue example given in \secref{sec:intro}. The amortised
- representation is convenient for generating code but exposes its
- \qt{implementation} details, which may be cumbersome when proving
- theorems about it. Therefore, here a simple, straightforward
- representation of queues:
-*}
-
-datatype %quote 'a queue = Queue "'a list"
-
-definition %quote empty :: "'a queue" where
- "empty = Queue []"
-
-primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
- "enqueue x (Queue xs) = Queue (xs @ [x])"
-
-fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
- "dequeue (Queue []) = (None, Queue [])"
- | "dequeue (Queue (x # xs)) = (Some x, Queue xs)"
-
-text {*
- \noindent This we can use directly for proving; for executing,
- we provide an alternative characterisation:
-*}
-
-definition %quote AQueue :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a queue" where
- "AQueue xs ys = Queue (ys @ rev xs)"
-
-code_datatype %quote AQueue
-
-text {*
- \noindent Here we define a \qt{constructor} @{const "AQueue"} which
- is defined in terms of @{text "Queue"} and interprets its arguments
- according to what the \emph{content} of an amortised queue is supposed
- to be. Equipped with this, we are able to prove the following equations
- for our primitive queue operations which \qt{implement} the simple
- queues in an amortised fashion:
-*}
-
-lemma %quote empty_AQueue [code]:
- "empty = AQueue [] []"
- unfolding AQueue_def empty_def by simp
-
-lemma %quote enqueue_AQueue [code]:
- "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
- unfolding AQueue_def by simp
-
-lemma %quote dequeue_AQueue [code]:
- "dequeue (AQueue xs []) =
- (if xs = [] then (None, AQueue [] [])
- else dequeue (AQueue [] (rev xs)))"
- "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
- unfolding AQueue_def by simp_all
-
-text {*
- \noindent For completeness, we provide a substitute for the
- @{text case} combinator on queues:
-*}
-
-definition %quote
- aqueue_case_def: "aqueue_case = queue_case"
-
-lemma %quote aqueue_case [code, code inline]:
- "queue_case = aqueue_case"
- unfolding aqueue_case_def ..
-
-lemma %quote case_AQueue [code]:
- "aqueue_case f (AQueue xs ys) = f (ys @ rev xs)"
- unfolding aqueue_case_def AQueue_def by simp
-
-text {*
- \noindent The resulting code looks as expected:
-*}
-
-text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
-
-text {*
- \noindent From this example, it can be glimpsed that using own
- constructor sets is a little delicate since it changes the set of
- valid patterns for values of that type. Without going into much
- detail, here some practical hints:
-
- \begin{itemize}
-
- \item When changing the constructor set for datatypes, take care
- to provide an alternative for the @{text case} combinator
- (e.g.~by replacing it using the preprocessor).
-
- \item Values in the target language need not to be normalised --
- different values in the target language may represent the same
- value in the logic.
-
- \item Usually, a good methodology to deal with the subtleties of
- pattern matching is to see the type as an abstract type: provide
- a set of operations which operate on the concrete representation
- of the type, and derive further operations by combinations of
- these primitive ones, without relying on a particular
- representation.
-
- \end{itemize}
-*}
-
-
-subsection {* Equality and wellsortedness *}
-
-text {*
- Surely you have already noticed how equality is treated
- by the code generator:
-*}
-
-primrec %quote collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "collect_duplicates xs ys [] = xs"
- | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
- then if z \<in> set ys
- then collect_duplicates xs ys zs
- else collect_duplicates xs (z#ys) zs
- else collect_duplicates (z#xs) (z#ys) zs)"
-
-text {*
- \noindent The membership test during preprocessing is rewritten,
- resulting in @{const List.member}, which itself
- performs an explicit equality check.
-*}
-
-text %quote {*@{code_stmts collect_duplicates (SML)}*}
-
-text {*
- \noindent Obviously, polymorphic equality is implemented the Haskell
- way using a type class. How is this achieved? HOL introduces
- an explicit class @{class eq} with a corresponding operation
- @{const eq_class.eq} such that @{thm eq [no_vars]}.
- The preprocessing framework does the rest by propagating the
- @{class eq} constraints through all dependent code equations.
- For datatypes, instances of @{class eq} are implicitly derived
- when possible. For other types, you may instantiate @{text eq}
- manually like any other type class.
-
- Though this @{text eq} class is designed to get rarely in
- the way, a subtlety
- enters the stage when definitions of overloaded constants
- are dependent on operational equality. For example, let
- us define a lexicographic ordering on tuples
- (also see theory @{theory Product_ord}):
-*}
-
-instantiation %quote "*" :: (order, order) order
-begin
-
-definition %quote [code del]:
- "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
-
-definition %quote [code del]:
- "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
-
-instance %quote proof
-qed (auto simp: less_eq_prod_def less_prod_def intro: order_less_trans)
-
-end %quote
-
-lemma %quote order_prod [code]:
- "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
- x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
- "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
- x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
- by (simp_all add: less_prod_def less_eq_prod_def)
-
-text {*
- \noindent Then code generation will fail. Why? The definition
- of @{term "op \<le>"} depends on equality on both arguments,
- which are polymorphic and impose an additional @{class eq}
- class constraint, which the preprocessor does not propagate
- (for technical reasons).
-
- The solution is to add @{class eq} explicitly to the first sort arguments in the
- code theorems:
-*}
-
-lemma %quote order_prod_code [code]:
- "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
- x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
- "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
- x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
- by (simp_all add: less_prod_def less_eq_prod_def)
-
-text {*
- \noindent Then code generation succeeds:
-*}
-
-text %quote {*@{code_stmts "op \<le> \<Colon> _ \<times> _ \<Rightarrow> _ \<times> _ \<Rightarrow> bool" (SML)}*}
-
-text {*
- In some cases, the automatically derived code equations
- for equality on a particular type may not be appropriate.
- As example, watch the following datatype representing
- monomorphic parametric types (where type constructors
- are referred to by natural numbers):
-*}
-
-datatype %quote monotype = Mono nat "monotype list"
-(*<*)
-lemma monotype_eq:
- "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<equiv>
- eq_class.eq tyco1 tyco2 \<and> eq_class.eq typargs1 typargs2" by (simp add: eq)
-(*>*)
-
-text {*
- \noindent Then code generation for SML would fail with a message
- that the generated code contains illegal mutual dependencies:
- the theorem @{thm monotype_eq [no_vars]} already requires the
- instance @{text "monotype \<Colon> eq"}, which itself requires
- @{thm monotype_eq [no_vars]}; Haskell has no problem with mutually
- recursive @{text instance} and @{text function} definitions,
- but the SML serialiser does not support this.
-
- In such cases, you have to provide your own equality equations
- involving auxiliary constants. In our case,
- @{const [show_types] list_all2} can do the job:
-*}
-
-lemma %quote monotype_eq_list_all2 [code]:
- "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<longleftrightarrow>
- eq_class.eq tyco1 tyco2 \<and> list_all2 eq_class.eq typargs1 typargs2"
- by (simp add: eq list_all2_eq [symmetric])
-
-text {*
- \noindent does not depend on instance @{text "monotype \<Colon> eq"}:
-*}
-
-text %quote {*@{code_stmts "eq_class.eq :: monotype \<Rightarrow> monotype \<Rightarrow> bool" (SML)}*}
-
-
-subsection {* Explicit partiality *}
-
-text {*
- Partiality usually enters the game by partial patterns, as
- in the following example, again for amortised queues:
-*}
-
-definition %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
- "strict_dequeue q = (case dequeue q
- of (Some x, q') \<Rightarrow> (x, q'))"
-
-lemma %quote strict_dequeue_AQueue [code]:
- "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
- "strict_dequeue (AQueue xs []) =
- (case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
- by (simp_all add: strict_dequeue_def dequeue_AQueue split: list.splits)
-
-text {*
- \noindent In the corresponding code, there is no equation
- for the pattern @{term "AQueue [] []"}:
-*}
-
-text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*}
-
-text {*
- \noindent In some cases it is desirable to have this
- pseudo-\qt{partiality} more explicitly, e.g.~as follows:
-*}
-
-axiomatization %quote empty_queue :: 'a
-
-definition %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
- "strict_dequeue' q = (case dequeue q of (Some x, q') \<Rightarrow> (x, q') | _ \<Rightarrow> empty_queue)"
-
-lemma %quote strict_dequeue'_AQueue [code]:
- "strict_dequeue' (AQueue xs []) = (if xs = [] then empty_queue
- else strict_dequeue' (AQueue [] (rev xs)))"
- "strict_dequeue' (AQueue xs (y # ys)) =
- (y, AQueue xs ys)"
- by (simp_all add: strict_dequeue'_def dequeue_AQueue split: list.splits)
-
-text {*
- Observe that on the right hand side of the definition of @{const
- "strict_dequeue'"} the constant @{const empty_queue} occurs
- which is unspecified.
-
- Normally, if constants without any code equations occur in a
- program, the code generator complains (since in most cases this is
- not what the user expects). But such constants can also be thought
- of as function definitions with no equations which always fail,
- since there is never a successful pattern match on the left hand
- side. In order to categorise a constant into that category
- explicitly, use @{command "code_abort"}:
-*}
-
-code_abort %quote empty_queue
-
-text {*
- \noindent Then the code generator will just insert an error or
- exception at the appropriate position:
-*}
-
-text %quote {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*}
-
-text {*
- \noindent This feature however is rarely needed in practice.
- Note also that the @{text HOL} default setup already declares
- @{const undefined} as @{command "code_abort"}, which is most
- likely to be used in such situations.
-*}
-
-end
-
\ No newline at end of file