# HG changeset patch # User haftmann # Date 1281703287 -7200 # Node ID 0dbbb511634df522ec7335eb141ec254ab802477 # Parent c4de81b7fdecf8d5164a283229c061c5604dc422# Parent bbb02b67caac95816605dda70b803f9f9eec9c0a merged diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/Thy/Foundations.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Codegen/Thy/Foundations.thy Fri Aug 13 14:41:27 2010 +0200 @@ -0,0 +1,432 @@ +theory Foundations +imports Introduction +begin + +section {* Code generation foundations \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} and @{command fun} + statements are used for code generation. This default behaviour + can be changed, e.g.\ by providing different code equations. + The customisations shown in this section are \emph{safe} + as regards correctness: all programs that can be generated 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. + 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 \ 'a \ 'a" (infixl "\" 70) + assumes assoc: "(x \ y) \ z = x \ (y \ z)" + +class %quote monoid = semigroup + + fixes neutral :: 'a ("\") + assumes neutl: "\ \ x = x" + and neutr: "x \ \ = 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 + "\ = 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 "\ \ n = n" + by (simp add: neutral_nat_def) + show "m \ \ = 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 = \" + | "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 (here, the same example in @{text SML}) + \cite{Haftmann-Nipkow:2010:code}: +*} + +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} can apply 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{unfold theorems}, which may be declared and removed using + the @{attribute code_unfold} or \emph{@{attribute code_unfold} del} + attribute, respectively. + + Some common applications: +*} + +text_raw {* + \begin{itemize} +*} + +text {* + \item replacing non-executable constructs by executable ones: +*} + +lemma %quote [code_unfold]: + "x \ set xs \ List.member xs x" by (fact in_set_member) + +text {* + \item eliminating superfluous constants: +*} + +lemma %quote [code_unfold]: + "1 = Suc 0" by (fact One_nat_def) + +text {* + \item replacing executable but inconvenient constructs: +*} + +lemma %quote [code_unfold]: + "xs = [] \ List.null xs" by (fact eq_Nil_null) + +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\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_codeproc} command. + @{command code_thms} provides a convenient + mechanism to inspect the impact of a preprocessor setup + on code equations. + + \begin{warn} + + Attribute @{attribute code_unfold} also applies to the + preprocessor of the ancient @{text "SML code generator"}; in case + this is not what you intend, use @{attribute code_inline} instead. + \end{warn} +*} + +subsection {* Datatypes \label{sec:datatypes} *} + +text {* + Conceptually, any datatype is spanned by a set of + \emph{constructors} of type @{text "\ = \ \ \ \\<^isub>1 \ \\<^isub>n"} where @{text + "{\\<^isub>1, \, \\<^isub>n}"} is exactly the set of \emph{all} type variables in + @{text "\"}. 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 is 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 \ 'a queue \ 'a queue" where + "enqueue x (Queue xs) = Queue (xs @ [x])" + +fun %quote dequeue :: "'a queue \ 'a option \ '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 \ 'a list \ '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: +*} + +lemma %quote queue_case_AQueue [code]: + "queue_case f (AQueue xs ys) = f (ys @ rev xs)" + unfolding 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 alternative equations for the @{text case} combinator. + + \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 *} + +text {* + Surely you have already noticed how equality is treated + by the code generator: +*} + +primrec %quote collect_duplicates :: "'a list \ 'a list \ 'a list \ 'a list" where + "collect_duplicates xs ys [] = xs" + | "collect_duplicates xs ys (z#zs) = (if z \ set xs + then if z \ 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 During preprocessing, the membership test 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. +*} + + +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 \ 'a \ 'a queue" where + "strict_dequeue q = (case dequeue q + of (Some x, q') \ (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 \ (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 \ 'a \ 'a queue" where + "strict_dequeue' q = (case dequeue q of (Some x, q') \ (x, q') | _ \ 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 unspecified constant @{const empty_queue} occurs. + + Normally, if constants without any code equations occur in a + program, the code generator complains (since in most cases this is + indeed an error). But such constants can also be thought + of as function definitions 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 diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/Thy/Further.thy --- a/doc-src/Codegen/Thy/Further.thy Fri Aug 13 12:15:25 2010 +0200 +++ b/doc-src/Codegen/Thy/Further.thy Fri Aug 13 14:41:27 2010 +0200 @@ -191,4 +191,140 @@ the framework described there is available in theory @{theory Imperative_HOL}. *} + +subsection {* ML system interfaces \label{sec:ml} *} + +text {* + Since the code generator framework not only aims to provide + a nice Isar interface but also to form a base for + code-generation-based applications, here a short + description of the most important ML interfaces. +*} + +subsubsection {* Managing executable content *} + +text %mlref {* + \begin{mldecls} + @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\ + @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\ + @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\ + @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\ + @{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option) + -> theory -> theory"} \\ + @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\ + @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\ + @{index_ML Code.get_type: "theory -> string + -> (string * sort) list * ((string * string list) * typ list) list"} \\ + @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"} + \end{mldecls} + + \begin{description} + + \item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function + theorem @{text "thm"} to executable content. + + \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes function + theorem @{text "thm"} from executable content, if present. + + \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes + the preprocessor simpset. + + \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds + function transformer @{text f} (named @{text name}) to executable content; + @{text f} is a transformer of the code equations belonging + to a certain function definition, depending on the + current theory context. Returning @{text NONE} indicates that no + transformation took place; otherwise, the whole process will be iterated + with the new code equations. + + \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes + function transformer named @{text name} from executable content. + + \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds + a datatype to executable content, with generation + set @{text cs}. + + \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"} + returns type constructor corresponding to + constructor @{text const}; returns @{text NONE} + if @{text const} is no constructor. + + \end{description} +*} + +subsubsection {* Auxiliary *} + +text %mlref {* + \begin{mldecls} + @{index_ML Code.read_const: "theory -> string -> string"} + \end{mldecls} + + \begin{description} + + \item @{ML Code.read_const}~@{text thy}~@{text s} + reads a constant as a concrete term expression @{text s}. + + \end{description} + +*} + +subsubsection {* Data depending on the theory's executable content *} + +text {* + Implementing code generator applications on top + of the framework set out so far usually not only + involves using those primitive interfaces + but also storing code-dependent data and various + other things. + + Due to incrementality of code generation, changes in the + theory's executable content have to be propagated in a + certain fashion. Additionally, such changes may occur + not only during theory extension but also during theory + merge, which is a little bit nasty from an implementation + point of view. The framework provides a solution + to this technical challenge by providing a functorial + data slot @{ML_functor Code_Data}; on instantiation + of this functor, the following types and operations + are required: + + \medskip + \begin{tabular}{l} + @{text "type T"} \\ + @{text "val empty: T"} \\ + \end{tabular} + + \begin{description} + + \item @{text T} the type of data to store. + + \item @{text empty} initial (empty) data. + + \end{description} + + \noindent An instance of @{ML_functor Code_Data} provides the following + interface: + + \medskip + \begin{tabular}{l} + @{text "change: theory \ (T \ T) \ T"} \\ + @{text "change_yield: theory \ (T \ 'a * T) \ 'a * T"} + \end{tabular} + + \begin{description} + + \item @{text change} update of current data (cached!) + by giving a continuation. + + \item @{text change_yield} update with side result. + + \end{description} +*} + +text {* + \bigskip + + \emph{Happy proving, happy hacking!} +*} + end diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/Thy/Inductive_Predicate.thy --- a/doc-src/Codegen/Thy/Inductive_Predicate.thy Fri Aug 13 12:15:25 2010 +0200 +++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy Fri Aug 13 14:41:27 2010 +0200 @@ -2,7 +2,7 @@ imports Setup begin -subsection {* Inductive Predicates *} +section {* Inductive Predicates *} (*<*) hide_const append diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/Thy/Introduction.thy --- a/doc-src/Codegen/Thy/Introduction.thy Fri Aug 13 12:15:25 2010 +0200 +++ b/doc-src/Codegen/Thy/Introduction.thy Fri Aug 13 14:41:27 2010 +0200 @@ -2,7 +2,17 @@ imports Setup begin -section {* Introduction and Overview *} +section {* Introduction *} + +subsection {* Code generation fundamental: shallow embedding *} + +subsection {* A quick start with the @{text "Isabelle/HOL"} toolbox *} + +subsection {* Type classes *} + +subsection {* How to continue from here *} + +subsection {* If something goes utterly wrong *} text {* This tutorial introduces a generic code generator for the @@ -111,6 +121,29 @@ for more details see \secref{sec:further}. *} +subsection {* If something utterly fails *} + +text {* + Under certain circumstances, the code generator fails to produce + code entirely. + + \begin{description} + + \ditem{generate only one module} + + \ditem{check with a different target language} + + \ditem{inspect code equations} + + \ditem{inspect preprocessor setup} + + \ditem{generate exceptions} + + \ditem{remove offending code equations} + + \end{description} +*} + subsection {* Code generator architecture \label{sec:concept} *} text {* diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/Thy/ML.thy --- a/doc-src/Codegen/Thy/ML.thy Fri Aug 13 12:15:25 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,162 +0,0 @@ -theory "ML" -imports Setup -begin - -section {* ML system interfaces \label{sec:ml} *} - -text {* - Since the code generator framework not only aims to provide - a nice Isar interface but also to form a base for - code-generation-based applications, here a short - description of the most important ML interfaces. -*} - -subsection {* Executable theory content: @{text Code} *} - -text {* - This Pure module implements the core notions of - executable content of a theory. -*} - -subsubsection {* Managing executable content *} - -text %mlref {* - \begin{mldecls} - @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\ - @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\ - @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\ - @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\ - @{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option) - -> theory -> theory"} \\ - @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\ - @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\ - @{index_ML Code.get_type: "theory -> string - -> (string * sort) list * ((string * string list) * typ list) list"} \\ - @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"} - \end{mldecls} - - \begin{description} - - \item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function - theorem @{text "thm"} to executable content. - - \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes function - theorem @{text "thm"} from executable content, if present. - - \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes - the preprocessor simpset. - - \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds - function transformer @{text f} (named @{text name}) to executable content; - @{text f} is a transformer of the code equations belonging - to a certain function definition, depending on the - current theory context. Returning @{text NONE} indicates that no - transformation took place; otherwise, the whole process will be iterated - with the new code equations. - - \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes - function transformer named @{text name} from executable content. - - \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds - a datatype to executable content, with generation - set @{text cs}. - - \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"} - returns type constructor corresponding to - constructor @{text const}; returns @{text NONE} - if @{text const} is no constructor. - - \end{description} -*} - -subsection {* Auxiliary *} - -text %mlref {* - \begin{mldecls} - @{index_ML Code.read_const: "theory -> string -> string"} - \end{mldecls} - - \begin{description} - - \item @{ML Code.read_const}~@{text thy}~@{text s} - reads a constant as a concrete term expression @{text s}. - - \end{description} - -*} - -subsection {* Implementing code generator applications *} - -text {* - Implementing code generator applications on top - of the framework set out so far usually not only - involves using those primitive interfaces - but also storing code-dependent data and various - other things. -*} - -subsubsection {* Data depending on the theory's executable content *} - -text {* - Due to incrementality of code generation, changes in the - theory's executable content have to be propagated in a - certain fashion. Additionally, such changes may occur - not only during theory extension but also during theory - merge, which is a little bit nasty from an implementation - point of view. The framework provides a solution - to this technical challenge by providing a functorial - data slot @{ML_functor Code_Data}; on instantiation - of this functor, the following types and operations - are required: - - \medskip - \begin{tabular}{l} - @{text "type T"} \\ - @{text "val empty: T"} \\ - @{text "val purge: theory \ string list option \ T \ T"} - \end{tabular} - - \begin{description} - - \item @{text T} the type of data to store. - - \item @{text empty} initial (empty) data. - - \item @{text purge}~@{text thy}~@{text consts} propagates changes in executable content; - @{text consts} indicates the kind - of change: @{ML NONE} stands for a fundamental change - which invalidates any existing code, @{text "SOME consts"} - hints that executable content for constants @{text consts} - has changed. - - \end{description} - - \noindent An instance of @{ML_functor Code_Data} provides the following - interface: - - \medskip - \begin{tabular}{l} - @{text "get: theory \ T"} \\ - @{text "change: theory \ (T \ T) \ T"} \\ - @{text "change_yield: theory \ (T \ 'a * T) \ 'a * T"} - \end{tabular} - - \begin{description} - - \item @{text get} retrieval of the current data. - - \item @{text change} update of current data (cached!) - by giving a continuation. - - \item @{text change_yield} update with side result. - - \end{description} -*} - -text {* - \bigskip - - \emph{Happy proving, happy hacking!} -*} - -end diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/Thy/Program.thy --- a/doc-src/Codegen/Thy/Program.thy Fri Aug 13 12:15:25 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,432 +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} and @{command fun} - statements are used for code generation. This default behaviour - can be changed, e.g.\ by providing different code equations. - The customisations shown in this section are \emph{safe} - as regards correctness: all programs that can be generated 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. - 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 \ 'a \ 'a" (infixl "\" 70) - assumes assoc: "(x \ y) \ z = x \ (y \ z)" - -class %quote monoid = semigroup + - fixes neutral :: 'a ("\") - assumes neutl: "\ \ x = x" - and neutr: "x \ \ = 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 - "\ = 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 "\ \ n = n" - by (simp add: neutral_nat_def) - show "m \ \ = 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 = \" - | "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 (here, the same example in @{text SML}) - \cite{Haftmann-Nipkow:2010:code}: -*} - -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} can apply 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{unfold theorems}, which may be declared and removed using - the @{attribute code_unfold} or \emph{@{attribute code_unfold} del} - attribute, respectively. - - Some common applications: -*} - -text_raw {* - \begin{itemize} -*} - -text {* - \item replacing non-executable constructs by executable ones: -*} - -lemma %quote [code_unfold]: - "x \ set xs \ List.member xs x" by (fact in_set_member) - -text {* - \item eliminating superfluous constants: -*} - -lemma %quote [code_unfold]: - "1 = Suc 0" by (fact One_nat_def) - -text {* - \item replacing executable but inconvenient constructs: -*} - -lemma %quote [code_unfold]: - "xs = [] \ List.null xs" by (fact eq_Nil_null) - -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\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_codeproc} command. - @{command code_thms} provides a convenient - mechanism to inspect the impact of a preprocessor setup - on code equations. - - \begin{warn} - - Attribute @{attribute code_unfold} also applies to the - preprocessor of the ancient @{text "SML code generator"}; in case - this is not what you intend, use @{attribute code_inline} instead. - \end{warn} -*} - -subsection {* Datatypes \label{sec:datatypes} *} - -text {* - Conceptually, any datatype is spanned by a set of - \emph{constructors} of type @{text "\ = \ \ \ \\<^isub>1 \ \\<^isub>n"} where @{text - "{\\<^isub>1, \, \\<^isub>n}"} is exactly the set of \emph{all} type variables in - @{text "\"}. 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 is 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 \ 'a queue \ 'a queue" where - "enqueue x (Queue xs) = Queue (xs @ [x])" - -fun %quote dequeue :: "'a queue \ 'a option \ '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 \ 'a list \ '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: -*} - -lemma %quote queue_case_AQueue [code]: - "queue_case f (AQueue xs ys) = f (ys @ rev xs)" - unfolding 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 alternative equations for the @{text case} combinator. - - \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 *} - -text {* - Surely you have already noticed how equality is treated - by the code generator: -*} - -primrec %quote collect_duplicates :: "'a list \ 'a list \ 'a list \ 'a list" where - "collect_duplicates xs ys [] = xs" - | "collect_duplicates xs ys (z#zs) = (if z \ set xs - then if z \ 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 During preprocessing, the membership test 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. -*} - - -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 \ 'a \ 'a queue" where - "strict_dequeue q = (case dequeue q - of (Some x, q') \ (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 \ (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 \ 'a \ 'a queue" where - "strict_dequeue' q = (case dequeue q of (Some x, q') \ (x, q') | _ \ 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 unspecified constant @{const empty_queue} occurs. - - Normally, if constants without any code equations occur in a - program, the code generator complains (since in most cases this is - indeed an error). But such constants can also be thought - of as function definitions 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 diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/Thy/ROOT.ML --- a/doc-src/Codegen/Thy/ROOT.ML Fri Aug 13 12:15:25 2010 +0200 +++ b/doc-src/Codegen/Thy/ROOT.ML Fri Aug 13 14:41:27 2010 +0200 @@ -1,10 +1,9 @@ no_document use_thy "Setup"; -no_document use_thys ["Efficient_Nat"]; use_thy "Introduction"; -use_thy "Program"; +use_thy "Foundations"; +use_thy "Refinement"; use_thy "Inductive_Predicate"; use_thy "Adaptation"; use_thy "Further"; -use_thy "ML"; diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/Thy/Refinement.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Codegen/Thy/Refinement.thy Fri Aug 13 14:41:27 2010 +0200 @@ -0,0 +1,7 @@ +theory Refinement +imports Setup +begin + +section {* Program and datatype refinement \label{sec:refinement} *} + +end diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/Thy/document/Foundations.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Codegen/Thy/document/Foundations.tex Fri Aug 13 14:41:27 2010 +0200 @@ -0,0 +1,1013 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Foundations}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Foundations\isanewline +\isakeyword{imports}\ Introduction\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupsection{Code generation foundations \label{sec:program}% +} +\isamarkuptrue% +% +\isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +We have already seen how by default equations stemming from + \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}, \hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}} and \hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} + statements are used for code generation. This default behaviour + can be changed, e.g.\ by providing different code equations. + The customisations shown in this section are \emph{safe} + as regards correctness: all programs that can be generated are partially + correct.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Selecting code equations% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Coming back to our introductory example, we + could provide an alternative code equations for \isa{dequeue} + explicitly:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline +\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar} + \isa{attribute} which states that the given theorems should be + considered as code equations for a \isa{fun} statement -- + the corresponding constant is determined syntactically. The resulting code:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ +\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ +\hspace*{0pt}dequeue (AQueue xs []) =\\ +\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\ +\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been + replaced by the predicate \isa{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. + This collection + may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{code{\isacharunderscore}thms}\isamarkupfalse% +\ dequeue% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent prints a table with \emph{all} code equations + for \isa{dequeue}, including + \emph{all} code equations those equations depend + on recursively. + + Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph + visualising dependencies between code equations.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{\isa{class} and \isa{instantiation}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Concerning type classes and code generation, let us examine an example + from abstract algebra:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{class}\isamarkupfalse% +\ semigroup\ {\isacharequal}\isanewline +\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline +\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{class}\isamarkupfalse% +\ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline +\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline +\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline +\ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{instantiation}\isamarkupfalse% +\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline +\isakeyword{begin}\isanewline +\isanewline +\isacommand{primrec}\isamarkupfalse% +\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline +\ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline +\ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline +\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline +\isanewline +\isacommand{instance}\isamarkupfalse% +\ \isacommand{proof}\isamarkupfalse% +\isanewline +\ \ \isacommand{fix}\isamarkupfalse% +\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline +\ \ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline +\ \ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline +\ \ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline +\isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\isacommand{end}\isamarkupfalse% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent We define the natural operation of the natural numbers + on monoids:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{primrec}\isamarkupfalse% +\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent This we use to define the discrete exponentiation function:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{definition}\isamarkupfalse% +\ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent The corresponding code in Haskell uses that language's native classes:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}module Example where {\char123}\\ +\hspace*{0pt}\\ +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\ +\hspace*{0pt}\\ +\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\ +\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\ +\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\ +\hspace*{0pt}\\ +\hspace*{0pt}class Semigroup a where {\char123}\\ +\hspace*{0pt} ~mult ::~a -> a -> a;\\ +\hspace*{0pt}{\char125};\\ +\hspace*{0pt}\\ +\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\ +\hspace*{0pt} ~neutral ::~a;\\ +\hspace*{0pt}{\char125};\\ +\hspace*{0pt}\\ +\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\ +\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\ +\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\ +\hspace*{0pt}\\ +\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\ +\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\ +\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ +\hspace*{0pt}\\ +\hspace*{0pt}neutral{\char95}nat ::~Nat;\\ +\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\ +\hspace*{0pt}\\ +\hspace*{0pt}instance Semigroup Nat where {\char123}\\ +\hspace*{0pt} ~mult = mult{\char95}nat;\\ +\hspace*{0pt}{\char125};\\ +\hspace*{0pt}\\ +\hspace*{0pt}instance Monoid Nat where {\char123}\\ +\hspace*{0pt} ~neutral = neutral{\char95}nat;\\ +\hspace*{0pt}{\char125};\\ +\hspace*{0pt}\\ +\hspace*{0pt}bexp ::~Nat -> Nat;\\ +\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\ +\hspace*{0pt}\\ +\hspace*{0pt}{\char125}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent This is a convenient place to show how explicit dictionary construction + manifests in generated code (here, the same example in \isa{SML}) + \cite{Haftmann-Nipkow:2010:code}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}structure Example :~sig\\ +\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\ +\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\ +\hspace*{0pt} ~type 'a semigroup\\ +\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\ +\hspace*{0pt} ~type 'a monoid\\ +\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\ +\hspace*{0pt} ~val neutral :~'a monoid -> 'a\\ +\hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\ +\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\ +\hspace*{0pt} ~val neutral{\char95}nat :~nat\\ +\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\ +\hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\ +\hspace*{0pt} ~val bexp :~nat -> nat\\ +\hspace*{0pt}end = struct\\ +\hspace*{0pt}\\ +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\ +\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\ +\hspace*{0pt}\\ +\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\ +\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\ +\hspace*{0pt}\\ +\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\ +\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\ +\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\ +\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\ +\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ +\hspace*{0pt}\\ +\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\ +\hspace*{0pt}\\ +\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\ +\hspace*{0pt}\\ +\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\ +\hspace*{0pt} ~:~nat monoid;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\ +\hspace*{0pt}\\ +\hspace*{0pt}end;~(*struct Example*)% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent Note the parameters with trailing underscore (\verb|A_|), + which are the dictionary parameters.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{The preprocessor \label{sec:preproc}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +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} can apply 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{unfold theorems}, which may be declared and removed using + the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del} + attribute, respectively. + + Some common applications:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{itemize} +% +\begin{isamarkuptext}% +\item replacing non-executable constructs by executable ones:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ List{\isachardot}member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}member{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\item eliminating superfluous constants:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\item replacing executable but inconvenient constructs:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}fact\ eq{\isacharunderscore}Nil{\isacharunderscore}null{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\end{itemize} +% +\begin{isamarkuptext}% +\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 \isa{{\isadigit{0}}} / \isa{Suc} + pattern elimination implemented in + theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this + interface. + + \noindent The current setup of the preprocessor may be inspected using + the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command. + \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient + mechanism to inspect the impact of a preprocessor setup + on code equations. + + \begin{warn} + + Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the + preprocessor of the ancient \isa{SML\ code\ generator}; in case + this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead. + \end{warn}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Datatypes \label{sec:datatypes}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Conceptually, any datatype is spanned by a set of + \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in + \isa{{\isasymtau}}. The HOL datatype package by default registers any new + datatype in the table of datatypes, which may be inspected using the + \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}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 is a simple, straightforward + representation of queues:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{datatype}\isamarkupfalse% +\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{primrec}\isamarkupfalse% +\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{fun}\isamarkupfalse% +\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent This we can use directly for proving; for executing, + we provide an alternative characterisation:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{definition}\isamarkupfalse% +\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse% +\ AQueue% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent Here we define a \qt{constructor} \isa{AQueue} which + is defined in terms of \isa{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:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{unfolding}\isamarkupfalse% +\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline +\ \ \isacommand{unfolding}\isamarkupfalse% +\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline +\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{unfolding}\isamarkupfalse% +\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ simp{\isacharunderscore}all% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent For completeness, we provide a substitute for the + \isa{case} combinator on queues:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{unfolding}\isamarkupfalse% +\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ simp% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent The resulting code looks as expected:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}structure Example :~sig\\ +\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\ +\hspace*{0pt} ~val rev :~'a list -> 'a list\\ +\hspace*{0pt} ~val null :~'a list -> bool\\ +\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\ +\hspace*{0pt} ~val empty :~'a queue\\ +\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\ +\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\ +\hspace*{0pt}end = struct\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun foldl f a [] = a\\ +\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun null [] = true\\ +\hspace*{0pt} ~| null (x ::~xs) = false;\\ +\hspace*{0pt}\\ +\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\ +\hspace*{0pt}\\ +\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\ +\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\ +\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\ +\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\ +\hspace*{0pt}\\ +\hspace*{0pt}end;~(*struct Example*)% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\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 alternative equations for the \isa{case} combinator. + + \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}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Equality% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Surely you have already noticed how equality is treated + by the code generator:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{primrec}\isamarkupfalse% +\ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline +\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline +\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline +\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline +\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent During preprocessing, the membership test is rewritten, + resulting in \isa{List{\isachardot}member}, which itself + performs an explicit equality check.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}structure Example :~sig\\ +\hspace*{0pt} ~type 'a eq\\ +\hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\ +\hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\ +\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\ +\hspace*{0pt} ~val collect{\char95}duplicates :\\ +\hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\ +\hspace*{0pt}end = struct\\ +\hspace*{0pt}\\ +\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ +\hspace*{0pt}val eq = {\char35}eq :~'a eq -> 'a -> 'a -> bool;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun member A{\char95}~[] y = false\\ +\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\ +\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\ +\hspace*{0pt} ~~~(if member A{\char95}~xs z\\ +\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\ +\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\ +\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\ +\hspace*{0pt}\\ +\hspace*{0pt}end;~(*struct Example*)% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent Obviously, polymorphic equality is implemented the Haskell + way using a type class. How is this achieved? HOL introduces + an explicit class \isa{eq} with a corresponding operation + \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}. + The preprocessing framework does the rest by propagating the + \isa{eq} constraints through all dependent code equations. + For datatypes, instances of \isa{eq} are implicitly derived + when possible. For other types, you may instantiate \isa{eq} + manually like any other type class.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Explicit partiality% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Partiality usually enters the game by partial patterns, as + in the following example, again for amortised queues:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{definition}\isamarkupfalse% +\ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline +\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent In the corresponding code, there is no equation + for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ +\hspace*{0pt} ~let {\char123}\\ +\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\ +\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\ +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent In some cases it is desirable to have this + pseudo-\qt{partiality} more explicitly, e.g.~as follows:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{axiomatization}\isamarkupfalse% +\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isacharbar}\ {\isacharunderscore}\ {\isasymRightarrow}\ empty{\isacharunderscore}queue{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline +\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}}, the unspecified constant \isa{empty{\isacharunderscore}queue} occurs. + + Normally, if constants without any code equations occur in a + program, the code generator complains (since in most cases this is + indeed an error). But such constants can also be thought + of as function definitions 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 \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{code{\isacharunderscore}abort}\isamarkupfalse% +\ empty{\isacharunderscore}queue% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent Then the code generator will just insert an error or + exception at the appropriate position:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\ +\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\ +\hspace*{0pt}\\ +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\ +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ +\hspace*{0pt} ~(if null xs then empty{\char95}queue\\ +\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent This feature however is rarely needed in practice. + Note also that the \isa{HOL} default setup already declares + \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most + likely to be used in such situations.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/Thy/document/Further.tex --- a/doc-src/Codegen/Thy/document/Further.tex Fri Aug 13 12:15:25 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Further.tex Fri Aug 13 14:41:27 2010 +0200 @@ -389,6 +389,179 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsection{ML system interfaces \label{sec:ml}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Since the code generator framework not only aims to provide + a nice Isar interface but also to form a base for + code-generation-based applications, here a short + description of the most important ML interfaces.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsubsection{Managing executable content% +} +\isamarkuptrue% +% +\isadelimmlref +% +\endisadelimmlref +% +\isatagmlref +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\ + \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\ + \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\ + \indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\ + \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline% +\verb| -> theory -> theory| \\ + \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\ + \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\ + \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline% +\verb| -> (string * sort) list * ((string * string list) * typ list) list| \\ + \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option| + \end{mldecls} + + \begin{description} + + \item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function + theorem \isa{thm} to executable content. + + \item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function + theorem \isa{thm} from executable content, if present. + + \item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes + the preprocessor simpset. + + \item \verb|Code_Preproc.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds + function transformer \isa{f} (named \isa{name}) to executable content; + \isa{f} is a transformer of the code equations belonging + to a certain function definition, depending on the + current theory context. Returning \isa{NONE} indicates that no + transformation took place; otherwise, the whole process will be iterated + with the new code equations. + + \item \verb|Code_Preproc.del_functrans|~\isa{name}~\isa{thy} removes + function transformer named \isa{name} from executable content. + + \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds + a datatype to executable content, with generation + set \isa{cs}. + + \item \verb|Code.get_type_of_constr_or_abstr|~\isa{thy}~\isa{const} + returns type constructor corresponding to + constructor \isa{const}; returns \isa{NONE} + if \isa{const} is no constructor. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagmlref +{\isafoldmlref}% +% +\isadelimmlref +% +\endisadelimmlref +% +\isamarkupsubsubsection{Auxiliary% +} +\isamarkuptrue% +% +\isadelimmlref +% +\endisadelimmlref +% +\isatagmlref +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| + \end{mldecls} + + \begin{description} + + \item \verb|Code.read_const|~\isa{thy}~\isa{s} + reads a constant as a concrete term expression \isa{s}. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagmlref +{\isafoldmlref}% +% +\isadelimmlref +% +\endisadelimmlref +% +\isamarkupsubsubsection{Data depending on the theory's executable content% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Implementing code generator applications on top + of the framework set out so far usually not only + involves using those primitive interfaces + but also storing code-dependent data and various + other things. + + Due to incrementality of code generation, changes in the + theory's executable content have to be propagated in a + certain fashion. Additionally, such changes may occur + not only during theory extension but also during theory + merge, which is a little bit nasty from an implementation + point of view. The framework provides a solution + to this technical challenge by providing a functorial + data slot \verb|Code_Data|; on instantiation + of this functor, the following types and operations + are required: + + \medskip + \begin{tabular}{l} + \isa{type\ T} \\ + \isa{val\ empty{\isacharcolon}\ T} \\ + \end{tabular} + + \begin{description} + + \item \isa{T} the type of data to store. + + \item \isa{empty} initial (empty) data. + + \end{description} + + \noindent An instance of \verb|Code_Data| provides the following + interface: + + \medskip + \begin{tabular}{l} + \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\ + \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T} + \end{tabular} + + \begin{description} + + \item \isa{change} update of current data (cached!) + by giving a continuation. + + \item \isa{change{\isacharunderscore}yield} update with side result. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{isamarkuptext}% +\bigskip + + \emph{Happy proving, happy hacking!}% +\end{isamarkuptext}% +\isamarkuptrue% +% \isadelimtheory % \endisadelimtheory diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/Thy/document/Inductive_Predicate.tex --- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Fri Aug 13 12:15:25 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Fri Aug 13 14:41:27 2010 +0200 @@ -18,7 +18,7 @@ % \endisadelimtheory % -\isamarkupsubsection{Inductive Predicates% +\isamarkupsection{Inductive Predicates% } \isamarkuptrue% % diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/Thy/document/Introduction.tex --- a/doc-src/Codegen/Thy/document/Introduction.tex Fri Aug 13 12:15:25 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Fri Aug 13 14:41:27 2010 +0200 @@ -18,7 +18,27 @@ % \endisadelimtheory % -\isamarkupsection{Introduction and Overview% +\isamarkupsection{Introduction% +} +\isamarkuptrue% +% +\isamarkupsubsection{Code generation fundamental: shallow embedding% +} +\isamarkuptrue% +% +\isamarkupsubsection{A quick start with the \isa{Isabelle{\isacharslash}HOL} toolbox% +} +\isamarkuptrue% +% +\isamarkupsubsection{Type classes% +} +\isamarkuptrue% +% +\isamarkupsubsection{How to continue from here% +} +\isamarkuptrue% +% +\isamarkupsubsection{If something goes utterly wrong% } \isamarkuptrue% % @@ -263,6 +283,32 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsection{If something utterly fails% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Under certain circumstances, the code generator fails to produce + code entirely. + + \begin{description} + + \ditem{generate only one module} + + \ditem{check with a different target language} + + \ditem{inspect code equations} + + \ditem{inspect preprocessor setup} + + \ditem{generate exceptions} + + \ditem{remove offending code equations} + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsubsection{Code generator architecture \label{sec:concept}% } \isamarkuptrue% diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/Thy/document/ML.tex --- a/doc-src/Codegen/Thy/document/ML.tex Fri Aug 13 12:15:25 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,240 +0,0 @@ -% -\begin{isabellebody}% -\def\isabellecontext{ML}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -\isacommand{theory}\isamarkupfalse% -\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\isanewline -\isakeyword{imports}\ Setup\isanewline -\isakeyword{begin}% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isamarkupsection{ML system interfaces \label{sec:ml}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Since the code generator framework not only aims to provide - a nice Isar interface but also to form a base for - code-generation-based applications, here a short - description of the most important ML interfaces.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Executable theory content: \isa{Code}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -This Pure module implements the core notions of - executable content of a theory.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{Managing executable content% -} -\isamarkuptrue% -% -\isadelimmlref -% -\endisadelimmlref -% -\isatagmlref -% -\begin{isamarkuptext}% -\begin{mldecls} - \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\ - \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\ - \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\ - \indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\ - \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline% -\verb| -> theory -> theory| \\ - \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\ - \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\ - \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline% -\verb| -> (string * sort) list * ((string * string list) * typ list) list| \\ - \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option| - \end{mldecls} - - \begin{description} - - \item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function - theorem \isa{thm} to executable content. - - \item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function - theorem \isa{thm} from executable content, if present. - - \item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes - the preprocessor simpset. - - \item \verb|Code_Preproc.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds - function transformer \isa{f} (named \isa{name}) to executable content; - \isa{f} is a transformer of the code equations belonging - to a certain function definition, depending on the - current theory context. Returning \isa{NONE} indicates that no - transformation took place; otherwise, the whole process will be iterated - with the new code equations. - - \item \verb|Code_Preproc.del_functrans|~\isa{name}~\isa{thy} removes - function transformer named \isa{name} from executable content. - - \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds - a datatype to executable content, with generation - set \isa{cs}. - - \item \verb|Code.get_type_of_constr_or_abstr|~\isa{thy}~\isa{const} - returns type constructor corresponding to - constructor \isa{const}; returns \isa{NONE} - if \isa{const} is no constructor. - - \end{description}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagmlref -{\isafoldmlref}% -% -\isadelimmlref -% -\endisadelimmlref -% -\isamarkupsubsection{Auxiliary% -} -\isamarkuptrue% -% -\isadelimmlref -% -\endisadelimmlref -% -\isatagmlref -% -\begin{isamarkuptext}% -\begin{mldecls} - \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| - \end{mldecls} - - \begin{description} - - \item \verb|Code.read_const|~\isa{thy}~\isa{s} - reads a constant as a concrete term expression \isa{s}. - - \end{description}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagmlref -{\isafoldmlref}% -% -\isadelimmlref -% -\endisadelimmlref -% -\isamarkupsubsection{Implementing code generator applications% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Implementing code generator applications on top - of the framework set out so far usually not only - involves using those primitive interfaces - but also storing code-dependent data and various - other things.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{Data depending on the theory's executable content% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Due to incrementality of code generation, changes in the - theory's executable content have to be propagated in a - certain fashion. Additionally, such changes may occur - not only during theory extension but also during theory - merge, which is a little bit nasty from an implementation - point of view. The framework provides a solution - to this technical challenge by providing a functorial - data slot \verb|Code_Data|; on instantiation - of this functor, the following types and operations - are required: - - \medskip - \begin{tabular}{l} - \isa{type\ T} \\ - \isa{val\ empty{\isacharcolon}\ T} \\ - \isa{val\ purge{\isacharcolon}\ theory\ {\isasymrightarrow}\ string\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T} - \end{tabular} - - \begin{description} - - \item \isa{T} the type of data to store. - - \item \isa{empty} initial (empty) data. - - \item \isa{purge}~\isa{thy}~\isa{consts} propagates changes in executable content; - \isa{consts} indicates the kind - of change: \verb|NONE| stands for a fundamental change - which invalidates any existing code, \isa{SOME\ consts} - hints that executable content for constants \isa{consts} - has changed. - - \end{description} - - \noindent An instance of \verb|Code_Data| provides the following - interface: - - \medskip - \begin{tabular}{l} - \isa{get{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\ - \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\ - \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T} - \end{tabular} - - \begin{description} - - \item \isa{get} retrieval of the current data. - - \item \isa{change} update of current data (cached!) - by giving a continuation. - - \item \isa{change{\isacharunderscore}yield} update with side result. - - \end{description}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\begin{isamarkuptext}% -\bigskip - - \emph{Happy proving, happy hacking!}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -\isacommand{end}\isamarkupfalse% -% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -\isanewline -\end{isabellebody}% -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "root" -%%% End: diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/Thy/document/Program.tex --- a/doc-src/Codegen/Thy/document/Program.tex Fri Aug 13 12:15:25 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1013 +0,0 @@ -% -\begin{isabellebody}% -\def\isabellecontext{Program}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -\isacommand{theory}\isamarkupfalse% -\ Program\isanewline -\isakeyword{imports}\ Introduction\isanewline -\isakeyword{begin}% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isamarkupsection{Turning Theories into Programs \label{sec:program}% -} -\isamarkuptrue% -% -\isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -We have already seen how by default equations stemming from - \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}, \hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}} and \hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} - statements are used for code generation. This default behaviour - can be changed, e.g.\ by providing different code equations. - The customisations shown in this section are \emph{safe} - as regards correctness: all programs that can be generated are partially - correct.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Selecting code equations% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Coming back to our introductory example, we - could provide an alternative code equations for \isa{dequeue} - explicitly:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline -\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline -\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline -\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar} - \isa{attribute} which states that the given theorems should be - considered as code equations for a \isa{fun} statement -- - the corresponding constant is determined syntactically. The resulting code:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ -\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ -\hspace*{0pt}dequeue (AQueue xs []) =\\ -\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\ -\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been - replaced by the predicate \isa{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. - This collection - may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{code{\isacharunderscore}thms}\isamarkupfalse% -\ dequeue% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent prints a table with \emph{all} code equations - for \isa{dequeue}, including - \emph{all} code equations those equations depend - on recursively. - - Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph - visualising dependencies between code equations.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{\isa{class} and \isa{instantiation}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Concerning type classes and code generation, let us examine an example - from abstract algebra:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{class}\isamarkupfalse% -\ semigroup\ {\isacharequal}\isanewline -\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline -\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{class}\isamarkupfalse% -\ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline -\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline -\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline -\ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{instantiation}\isamarkupfalse% -\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline -\isakeyword{begin}\isanewline -\isanewline -\isacommand{primrec}\isamarkupfalse% -\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline -\ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{definition}\isamarkupfalse% -\ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{lemma}\isamarkupfalse% -\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline -\ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline -\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline -\ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline -\isanewline -\isacommand{instance}\isamarkupfalse% -\ \isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{fix}\isamarkupfalse% -\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline -\isacommand{qed}\isamarkupfalse% -\isanewline -\isanewline -\isacommand{end}\isamarkupfalse% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent We define the natural operation of the natural numbers - on monoids:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{primrec}\isamarkupfalse% -\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline -\ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent This we use to define the discrete exponentiation function:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{definition}\isamarkupfalse% -\ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent The corresponding code in Haskell uses that language's native classes:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}module Example where {\char123}\\ -\hspace*{0pt}\\ -\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}class Semigroup a where {\char123}\\ -\hspace*{0pt} ~mult ::~a -> a -> a;\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\ -\hspace*{0pt} ~neutral ::~a;\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\ -\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\ -\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\ -\hspace*{0pt}\\ -\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\ -\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\ -\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\ -\hspace*{0pt}\\ -\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\ -\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\ -\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ -\hspace*{0pt}\\ -\hspace*{0pt}neutral{\char95}nat ::~Nat;\\ -\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}instance Semigroup Nat where {\char123}\\ -\hspace*{0pt} ~mult = mult{\char95}nat;\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\hspace*{0pt}instance Monoid Nat where {\char123}\\ -\hspace*{0pt} ~neutral = neutral{\char95}nat;\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\hspace*{0pt}bexp ::~Nat -> Nat;\\ -\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\ -\hspace*{0pt}\\ -\hspace*{0pt}{\char125}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent This is a convenient place to show how explicit dictionary construction - manifests in generated code (here, the same example in \isa{SML}) - \cite{Haftmann-Nipkow:2010:code}:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example :~sig\\ -\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\ -\hspace*{0pt} ~type 'a semigroup\\ -\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\ -\hspace*{0pt} ~type 'a monoid\\ -\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\ -\hspace*{0pt} ~val neutral :~'a monoid -> 'a\\ -\hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\ -\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\ -\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\ -\hspace*{0pt} ~val neutral{\char95}nat :~nat\\ -\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\ -\hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\ -\hspace*{0pt} ~val bexp :~nat -> nat\\ -\hspace*{0pt}end = struct\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\ -\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\ -\hspace*{0pt}\\ -\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\ -\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\ -\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\ -\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\ -\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\ -\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ -\hspace*{0pt}\\ -\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\ -\hspace*{0pt} ~:~nat monoid;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\ -\hspace*{0pt}\\ -\hspace*{0pt}end;~(*struct Example*)% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent Note the parameters with trailing underscore (\verb|A_|), - which are the dictionary parameters.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{The preprocessor \label{sec:preproc}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -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} can apply 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{unfold theorems}, which may be declared and removed using - the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del} - attribute, respectively. - - Some common applications:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\begin{itemize} -% -\begin{isamarkuptext}% -\item replacing non-executable constructs by executable ones:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ List{\isachardot}member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}member{\isacharparenright}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\item eliminating superfluous constants:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\item replacing executable but inconvenient constructs:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}fact\ eq{\isacharunderscore}Nil{\isacharunderscore}null{\isacharparenright}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\end{itemize} -% -\begin{isamarkuptext}% -\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 \isa{{\isadigit{0}}} / \isa{Suc} - pattern elimination implemented in - theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this - interface. - - \noindent The current setup of the preprocessor may be inspected using - the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command. - \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient - mechanism to inspect the impact of a preprocessor setup - on code equations. - - \begin{warn} - - Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the - preprocessor of the ancient \isa{SML\ code\ generator}; in case - this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead. - \end{warn}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Datatypes \label{sec:datatypes}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Conceptually, any datatype is spanned by a set of - \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in - \isa{{\isasymtau}}. The HOL datatype package by default registers any new - datatype in the table of datatypes, which may be inspected using the - \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}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 is a simple, straightforward - representation of queues:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{datatype}\isamarkupfalse% -\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{definition}\isamarkupfalse% -\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{primrec}\isamarkupfalse% -\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{fun}\isamarkupfalse% -\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent This we can use directly for proving; for executing, - we provide an alternative characterisation:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{definition}\isamarkupfalse% -\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse% -\ AQueue% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent Here we define a \qt{constructor} \isa{AQueue} which - is defined in terms of \isa{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:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{lemma}\isamarkupfalse% -\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline -\ \ \isacommand{unfolding}\isamarkupfalse% -\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\isanewline -\isacommand{lemma}\isamarkupfalse% -\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline -\ \ \isacommand{unfolding}\isamarkupfalse% -\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\isanewline -\isacommand{lemma}\isamarkupfalse% -\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline -\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline -\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \isacommand{unfolding}\isamarkupfalse% -\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% -\ simp{\isacharunderscore}all% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent For completeness, we provide a substitute for the - \isa{case} combinator on queues:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{lemma}\isamarkupfalse% -\ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \isacommand{unfolding}\isamarkupfalse% -\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% -\ simp% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent The resulting code looks as expected:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example :~sig\\ -\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\ -\hspace*{0pt} ~val rev :~'a list -> 'a list\\ -\hspace*{0pt} ~val null :~'a list -> bool\\ -\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\ -\hspace*{0pt} ~val empty :~'a queue\\ -\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\ -\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\ -\hspace*{0pt}end = struct\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun foldl f a [] = a\\ -\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun null [] = true\\ -\hspace*{0pt} ~| null (x ::~xs) = false;\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\ -\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\ -\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\ -\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\ -\hspace*{0pt}\\ -\hspace*{0pt}end;~(*struct Example*)% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\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 alternative equations for the \isa{case} combinator. - - \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}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Equality% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Surely you have already noticed how equality is treated - by the code generator:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{primrec}\isamarkupfalse% -\ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline -\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline -\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline -\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline -\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline -\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent During preprocessing, the membership test is rewritten, - resulting in \isa{List{\isachardot}member}, which itself - performs an explicit equality check.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example :~sig\\ -\hspace*{0pt} ~type 'a eq\\ -\hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\ -\hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\ -\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\ -\hspace*{0pt} ~val collect{\char95}duplicates :\\ -\hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\ -\hspace*{0pt}end = struct\\ -\hspace*{0pt}\\ -\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ -\hspace*{0pt}val eq = {\char35}eq :~'a eq -> 'a -> 'a -> bool;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun member A{\char95}~[] y = false\\ -\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\ -\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\ -\hspace*{0pt} ~~~(if member A{\char95}~xs z\\ -\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\ -\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\ -\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\ -\hspace*{0pt}\\ -\hspace*{0pt}end;~(*struct Example*)% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent Obviously, polymorphic equality is implemented the Haskell - way using a type class. How is this achieved? HOL introduces - an explicit class \isa{eq} with a corresponding operation - \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}. - The preprocessing framework does the rest by propagating the - \isa{eq} constraints through all dependent code equations. - For datatypes, instances of \isa{eq} are implicitly derived - when possible. For other types, you may instantiate \isa{eq} - manually like any other type class.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Explicit partiality% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Partiality usually enters the game by partial patterns, as - in the following example, again for amortised queues:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{definition}\isamarkupfalse% -\ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline -\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{lemma}\isamarkupfalse% -\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline -\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent In the corresponding code, there is no equation - for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ -\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ -\hspace*{0pt} ~let {\char123}\\ -\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\ -\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\ -\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent In some cases it is desirable to have this - pseudo-\qt{partiality} more explicitly, e.g.~as follows:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{axiomatization}\isamarkupfalse% -\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline -\isanewline -\isacommand{definition}\isamarkupfalse% -\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isacharbar}\ {\isacharunderscore}\ {\isasymRightarrow}\ empty{\isacharunderscore}queue{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{lemma}\isamarkupfalse% -\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline -\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline -\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}}, the unspecified constant \isa{empty{\isacharunderscore}queue} occurs. - - Normally, if constants without any code equations occur in a - program, the code generator complains (since in most cases this is - indeed an error). But such constants can also be thought - of as function definitions 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 \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{code{\isacharunderscore}abort}\isamarkupfalse% -\ empty{\isacharunderscore}queue% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent Then the code generator will just insert an error or - exception at the appropriate position:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\ -\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\ -\hspace*{0pt}\\ -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ -\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\ -\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ -\hspace*{0pt} ~(if null xs then empty{\char95}queue\\ -\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent This feature however is rarely needed in practice. - Note also that the \isa{HOL} default setup already declares - \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most - likely to be used in such situations.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -\isacommand{end}\isamarkupfalse% -% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -\isanewline -\end{isabellebody}% -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "root" -%%% End: diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/Thy/document/Refinement.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Codegen/Thy/document/Refinement.tex Fri Aug 13 14:41:27 2010 +0200 @@ -0,0 +1,43 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Refinement}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Refinement\isanewline +\isakeyword{imports}\ Setup\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupsection{Program and datatype refinement \label{sec:refinement}% +} +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/codegen.tex --- a/doc-src/Codegen/codegen.tex Fri Aug 13 12:15:25 2010 +0200 +++ b/doc-src/Codegen/codegen.tex Fri Aug 13 14:41:27 2010 +0200 @@ -20,9 +20,9 @@ \maketitle \begin{abstract} - \noindent This tutorial gives an introduction to a generic code generator framework in Isabelle - for generating executable code in functional programming languages from logical - specifications in Isabelle/HOL. + \noindent This tutorial introduces the code generator facilities of Isabelle/HOL. + They empower the user to turn HOL specifications into corresponding executable + programs in the languages SML, OCaml and Haskell. \end{abstract} \thispagestyle{empty}\clearpage @@ -31,11 +31,11 @@ \clearfirst \input{Thy/document/Introduction.tex} -\input{Thy/document/Program.tex} +\input{Thy/document/Foundations.tex} +\input{Thy/document/Refinement.tex} \input{Thy/document/Inductive_Predicate.tex} \input{Thy/document/Adaptation.tex} \input{Thy/document/Further.tex} -\input{Thy/document/ML.tex} \begingroup \bibliographystyle{plain} \small\raggedright\frenchspacing diff -r c4de81b7fdec -r 0dbbb511634d doc-src/Codegen/style.sty --- a/doc-src/Codegen/style.sty Fri Aug 13 12:15:25 2010 +0200 +++ b/doc-src/Codegen/style.sty Fri Aug 13 14:41:27 2010 +0200 @@ -15,6 +15,7 @@ %% typographic conventions \newcommand{\qt}[1]{``{#1}''} +\newcommand{\ditem}[1]{\item[\isastyletext #1]} %% verbatim text \newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}