# HG changeset patch # User haftmann # Date 1222860834 -7200 # Node ID df77ed974a789430242cfc50c153bbcd3f0486f5 # Parent a01de3b3fa2edf94a973da645657a2fceb23f7b8 fixed diff -r a01de3b3fa2e -r df77ed974a78 doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy Wed Oct 01 12:18:18 2008 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy Wed Oct 01 13:33:54 2008 +0200 @@ -66,12 +66,12 @@ primrec %quoteme in_interval :: "nat \ nat \ nat \ bool" where "in_interval (k, l) n \ k \ n \ n \ l" - +(*<*) code_type %invisible bool (SML) code_const %invisible True and False and "op \" and Not (SML and and and) - +(*>*) text %quoteme {*@{code_stmts in_interval (SML)}*} text {* @@ -92,7 +92,7 @@ (SML "true" and "false" and "_ andalso _") text {* - The @{command code_type} command takes a type constructor + \noindent The @{command code_type} command takes a type constructor as arguments together with a list of custom serialisations. Each custom serialisation starts with a target language identifier followed by an expression, which during @@ -120,22 +120,22 @@ text %quoteme {*@{code_stmts in_interval (SML)}*} text {* - Next, we try to map HOL pairs to SML pairs, using the + \noindent Next, we try to map HOL pairs to SML pairs, using the infix ``@{verbatim "*"}'' type constructor and parentheses: *} - +(*<*) code_type %invisible * (SML) code_const %invisible Pair (SML) - +(*>*) code_type %tt * (SML infix 2 "*") code_const %tt Pair (SML "!((_),/ (_))") text {* - The initial bang ``@{verbatim "!"}'' tells the serializer to never put + \noindent The initial bang ``@{verbatim "!"}'' tells the serializer to never put parentheses around the whole expression (they are already present), while the parentheses around argument place holders tell not to put parentheses around the arguments. @@ -178,7 +178,7 @@ (Haskell infixl 4 "==") text {* - A problem now occurs whenever a type which + \noindent A problem now occurs whenever a type which is an instance of @{class eq} in @{text HOL} is mapped on a @{text Haskell}-built-in type which is also an instance of @{text Haskell} @{text Eq}: @@ -199,7 +199,7 @@ (Haskell "Integer") text {* - The code generator would produce + \noindent The code generator would produce an additional instance, which of course is rejectedby the @{text Haskell} compiler. To suppress this additional instance, use diff -r a01de3b3fa2e -r df77ed974a78 doc-src/IsarAdvanced/Codegen/Thy/Further.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Further.thy Wed Oct 01 12:18:18 2008 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Further.thy Wed Oct 01 13:33:54 2008 +0200 @@ -2,7 +2,7 @@ imports Setup begin -section {* Further topics \label{sec:further} *} +section {* Further issues \label{sec:further} *} subsection {* Further reading *} diff -r a01de3b3fa2e -r df77ed974a78 doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Wed Oct 01 12:18:18 2008 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Wed Oct 01 13:33:54 2008 +0200 @@ -28,19 +28,21 @@ The code generator aims to be usable with no further ado in most cases while allowing for detailed customisation. This manifests in the structure of this tutorial: after a short - conceptual introduction with an example \secref{sec:intro}, - we discuss the generic customisation facilities \secref{sec:program}. - A further section \secref{sec:adaption} is dedicated to the matter of + conceptual introduction with an example (\secref{sec:intro}), + we discuss the generic customisation facilities (\secref{sec:program}). + A further section (\secref{sec:adaption}) is dedicated to the matter of \qn{adaption} to specific target language environments. After some - further issues \secref{sec:further} we conclude with an overview - of some ML programming interfaces \secref{sec:ml}. + further issues (\secref{sec:further}) we conclude with an overview + of some ML programming interfaces (\secref{sec:ml}). \begin{warn} Ultimately, the code generator which this tutorial deals with - is supposed to replace the already established code generator + is supposed to replace the existing code generator by Stefan Berghofer \cite{Berghofer-Nipkow:2002}. So, for the moment, there are two distinct code generators - in Isabelle. + in Isabelle. In case of ambiguity, we will refer to the framework + described here as @{text "generic code generator"}, to the + other as @{text "SML code generator"}. Also note that while the framework itself is object-logic independent, only @{theory HOL} provides a reasonable framework setup. @@ -59,7 +61,6 @@ @{command definition}/@{command primrec}/@{command fun} declarations form the core of a functional programming language. The default code generator setup allows to turn those into functional programs immediately. - This means that \qt{naive} code generation can proceed without further ado. For example, here a simple \qt{implementation} of amortised queues: *} @@ -75,11 +76,13 @@ fun %quoteme dequeue :: "'a queue \ 'a option \ 'a queue" where "dequeue (Queue [] []) = (None, Queue [] [])" | "dequeue (Queue xs (y # ys)) = (Some y, Queue xs ys)" - | "dequeue (Queue xs []) = (case rev xs of y # ys \ (Some y, Queue [] ys))" + | "dequeue (Queue xs []) = + (case rev xs of y # ys \ (Some y, Queue [] ys))" text {* \noindent Then we can generate code e.g.~for @{text SML} as follows: *} -export_code %quoteme empty dequeue enqueue in SML module_name Example file "examples/example.ML" +export_code %quoteme empty dequeue enqueue in SML + module_name Example file "examples/example.ML" text {* \noindent resulting in the following code: *} @@ -88,7 +91,7 @@ text {* \noindent The @{command export_code} command takes a space-separated list of constants for which code shall be generated; anything else needed for those - is added implicitly. Then follows by a target language identifier + is added implicitly. Then follows a target language identifier (@{text SML}, @{text OCaml} or @{text Haskell}) and a freely chosen module name. A file name denotes the destination to store the generated code. Note that the semantics of the destination depends on the target language: for @@ -97,7 +100,8 @@ (with extension @{text ".hs"}) is written: *} -export_code %quoteme empty dequeue enqueue in Haskell module_name Example file "examples/" +export_code %quoteme empty dequeue enqueue in Haskell + module_name Example file "examples/" text {* \noindent This is how the corresponding code in @{text Haskell} looks like: @@ -107,10 +111,10 @@ text {* \noindent This demonstrates the basic usage of the @{command export_code} command; - for more details see \secref{sec:serializer}. + for more details see \secref{sec:further}. *} -subsection {* Code generator architecture *} +subsection {* Code generator architecture \label{sec:concept} *} text {* What you have seen so far should be already enough in a lot of cases. If you @@ -125,10 +129,6 @@ \label{fig:arch} \end{figure} - The code generator itself consists of three major components - which operate sequentially, i.e. the result of one is the input - of the next in the chain, see diagram \ref{fig:arch}: - The code generator employs a notion of executability for three foundational executable ingredients known from functional programming: @@ -138,8 +138,10 @@ (an equation headed by a constant @{text f} with arguments @{text "t\<^isub>1 t\<^isub>2 \ t\<^isub>n"} and right hand side @{text t}). Code generation aims to turn defining equations - into a functional program by running through the following - process: + into a functional program. This is achieved by three major + components which operate sequentially, i.e. the result of one is + the input + of the next in the chain, see diagram \ref{fig:arch}: \begin{itemize} @@ -165,7 +167,10 @@ of defining equations. \item These defining equations are \qn{translated} to a program - in an abstract intermediate language. + in an abstract intermediate language. Think of it as a kind + of \qt{Mini-Haskell} with four \qn{statements}: @{text data} + (for datatypes), @{text fun} (stemming from defining equations), + also @{text class} and @{text inst} (for type classes). \item Finally, the abstract program is \qn{serialised} into concrete source code of a target language. diff -r a01de3b3fa2e -r df77ed974a78 doc-src/IsarAdvanced/Codegen/Thy/ML.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/ML.thy Wed Oct 01 12:18:18 2008 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/ML.thy Wed Oct 01 13:33:54 2008 +0200 @@ -108,12 +108,6 @@ involves using those primitive interfaces but also storing code-dependent data and various other things. - - \begin{warn} - Some interfaces discussed here have not reached - a final state yet. - Changes likely to occur in future. - \end{warn} *} subsubsection {* Data depending on the theory's executable content *} @@ -152,7 +146,7 @@ \end{description} - An instance of @{ML_functor CodeDataFun} provides the following + \noindent An instance of @{ML_functor CodeDataFun} provides the following interface: \medskip @@ -175,6 +169,8 @@ *} text {* + \bigskip + \emph{Happy proving, happy hacking!} *} diff -r a01de3b3fa2e -r df77ed974a78 doc-src/IsarAdvanced/Codegen/Thy/Program.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Wed Oct 01 12:18:18 2008 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Wed Oct 01 13:33:54 2008 +0200 @@ -6,20 +6,30 @@ subsection {* The @{text "Isabelle/HOL"} default setup *} -subsection {* Selecting code equations *} - text {* We have already seen how by default equations stemming from @{command definition}/@{command primrec}/@{command fun} - statements are used for code generation. Deviating from this - \emph{default} behaviour is always possible -- e.g.~we - could provide an alternative @{text fun} for @{const dequeue} proving - the following equations explicitly: + statements are used for code generation. This default behaviour + can be changed, e.g. by providing different defining equations. + All kinds of customization shown in this section is \emph{safe} + in the sense that the user does not have to worry about + correctness -- all programs generatable that way are partially + correct. +*} + +subsection {* Selecting code equations *} + +text {* + Coming back to our introductory example, we + could provide an alternative defining equations for @{const dequeue} + explicitly: *} lemma %quoteme [code func]: - "dequeue (Queue xs []) = (if xs = [] then (None, Queue [] []) else dequeue (Queue [] (rev xs)))" - "dequeue (Queue xs (y # ys)) = (Some y, Queue xs ys)" + "dequeue (Queue xs []) = + (if xs = [] then (None, Queue [] []) else dequeue (Queue [] (rev xs)))" + "dequeue (Queue xs (y # ys)) = + (Some y, Queue xs ys)" by (cases xs, simp_all) (cases "rev xs", simp_all) text {* @@ -60,7 +70,7 @@ subsection {* @{text class} and @{text instantiation} *} text {* - Concerning type classes and code generation, let us again examine an example + Concerning type classes and code generation, let us examine an example from abstract algebra: *} @@ -105,7 +115,7 @@ on monoids: *} -primrec %quoteme pow :: "nat \ 'a\monoid \ 'a\monoid" where +primrec %quoteme (in monoid) pow :: "nat \ 'a \ 'a" where "pow 0 a = \" | "pow (Suc n) a = a \ pow n a" @@ -123,31 +133,16 @@ text %quoteme {*@{code_stmts bexp (Haskell)}*} text {* - \noindent An inspection reveals that the equations stemming from the - @{command primrec} statement within instantiation of class - @{class semigroup} with type @{typ nat} are mapped to a separate - function declaration @{verbatim mult_nat} which in turn is used - to provide the right hand side for the @{verbatim "instance Semigroup Nat"}. - This perfectly - agrees with the restriction that @{text inst} statements may - only contain one single equation for each class class parameter - The @{command instantiation} mechanism manages that for each - overloaded constant @{text "f [\ \<^bvec>\\s\<^isub>k\<^evec>]"} - a \emph{shadow constant} @{text "f\<^isub>\ [\<^bvec>\\s\<^isub>k\<^evec>]"} is - declared satisfying @{text "f [\ \<^bvec>\\s\<^isub>k\<^evec>] \ f\<^isub>\ [\<^bvec>\\s\<^isub>k\<^evec>]"}. - this equation is indeed the one used for the statement; - using it as a rewrite rule, defining equations for - @{text "f [\ \<^bvec>\\s\<^isub>k\<^evec>]"} can be turned into - defining equations for @{text "f\<^isub>\ [\<^bvec>\\s\<^isub>k\<^evec>]"}. This - happens transparently, providing the illusion that class parameters - can be instantiated with more than one equation. - - This is a convenient place to show how explicit dictionary construction + \noindent This is a convenient place to show how explicit dictionary construction manifests in generated code (here, the same example in @{text SML}): *} text %quoteme {*@{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} *} @@ -199,7 +194,7 @@ *} text {* - \emph{Function transformers} provide a very general interface, + \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} @@ -215,8 +210,9 @@ \begin{warn} The attribute \emph{code unfold} - associated with the existing code generator also applies to - the new one: \emph{code unfold} implies \emph{code inline}. + associated with the @{text "SML code generator"} also applies to + the @{text "generic code generator"}: + \emph{code unfold} implies \emph{code inline}. \end{warn} *} @@ -246,7 +242,7 @@ "Dig1 n = Suc (2 * n)" text {* - \noindent We will use these two ">digits"< to represent natural numbers + \noindent We will use these two \qt{digits} to represent natural numbers in binary digits, e.g.: *} @@ -299,9 +295,7 @@ text %quoteme {*@{code_stmts "op + \ nat \ nat \ nat" (SML)}*} text {* - \medskip - - From this example, it can be easily glimpsed that using own constructor sets + \noindent From this example, it can be easily 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: @@ -334,9 +328,8 @@ by the code generator: *} -primrec %quoteme - collect_duplicates :: "'a list \ 'a list \ 'a list \ 'a list" where - "collect_duplicates xs ys [] = xs" +primrec %quoteme 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 @@ -356,7 +349,8 @@ 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. + The preprocessing framework does the rest by propagating the + @{class eq} constraints through all dependent defining 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. @@ -365,50 +359,54 @@ the way, a subtlety enters the stage when definitions of overloaded constants are dependent on operational equality. For example, let - us define a lexicographic ordering on tuples: + us define a lexicographic ordering on tuples + (also see theory @{theory Product_ord}): *} -instantiation %quoteme * :: (ord, ord) ord +instantiation %quoteme "*" :: (order, order) order begin definition %quoteme [code func del]: - "p1 < p2 \ (let (x1, y1) = p1; (x2, y2) = p2 in x1 < x2 \ (x1 = x2 \ y1 < y2))" + "x \ y \ fst x < fst y \ fst x = fst y \ snd x \ snd y" definition %quoteme [code func del]: - "p1 \ p2 \ (let (x1, y1) = p1; (x2, y2) = p2 in x1 < x2 \ (x1 = x2 \ y1 \ y2))" + "x < y \ fst x < fst y \ fst x = fst y \ snd x < snd y" -instance %quoteme .. +instance %quoteme proof +qed (auto simp: less_eq_prod_def less_prod_def intro: order_less_trans) end %quoteme -lemma %quoteme ord_prod [code func]: - "(x1 \ 'a\ord, y1 \ 'b\ord) < (x2, y2) \ x1 < x2 \ (x1 = x2 \ y1 < y2)" - "(x1 \ 'a\ord, y1 \ 'b\ord) \ (x2, y2) \ x1 < x2 \ (x1 = x2 \ y1 \ y2)" - unfolding less_prod_def less_eq_prod_def by simp_all +lemma %quoteme order_prod [code func]: + "(x1 \ 'a\order, y1 \ 'b\order) < (x2, y2) \ + x1 < x2 \ x1 = x2 \ y1 < y2" + "(x1 \ 'a\order, y1 \ 'b\order) \ (x2, y2) \ + x1 < x2 \ x1 = x2 \ y1 \ y2" + by (simp_all add: less_prod_def less_eq_prod_def) text {* \noindent Then code generation will fail. Why? The definition of @{term "op \"} depends on equality on both arguments, which are polymorphic and impose an additional @{class eq} - class constraint, which the preprocessort does not propagate for technical - reasons. + class constraint, which the preprocessor does not propagate + (for technical reasons). The solution is to add @{class eq} explicitly to the first sort arguments in the code theorems: *} -lemma ord_prod_code [code func]: - "(x1 \ 'a\{ord, eq}, y1 \ 'b\ord) < (x2, y2) \ - x1 < x2 \ (x1 = x2 \ y1 < y2)" - "(x1 \ 'a\{ord, eq}, y1 \ 'b\ord) \ (x2, y2) \ - x1 < x2 \ (x1 = x2 \ y1 \ y2)" - unfolding ord_prod by rule+ +lemma %quoteme order_prod_code [code func]: + "(x1 \ 'a\{order, eq}, y1 \ 'b\order) < (x2, y2) \ + x1 < x2 \ x1 = x2 \ y1 < y2" + "(x1 \ 'a\{order, eq}, y1 \ 'b\order) \ (x2, y2) \ + x1 < x2 \ x1 = x2 \ y1 \ y2" + by (simp_all add: less_prod_def less_eq_prod_def) text {* \noindent Then code generation succeeds: *} -text %quoteme {*@{code_stmts "op \ \ 'a\{eq, ord} \ 'b\ord \ 'a \ 'b \ bool" (SML)}*} +text %quoteme {*@{code_stmts "op \ \ _ \ _ \ _ \ _ \ bool" (SML)}*} text {* In some cases, the automatically derived defining equations @@ -434,7 +432,7 @@ recursive @{text inst} and @{text fun} definitions, but the SML serializer does not support this. - In such cases, you have to provide you own equality equations + In such cases, you have to provide your own equality equations involving auxiliary constants. In our case, @{const [show_types] list_all2} can do the job: *} diff -r a01de3b3fa2e -r df77ed974a78 doc-src/IsarAdvanced/Codegen/Thy/Setup.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Wed Oct 01 12:18:18 2008 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Wed Oct 01 13:33:54 2008 +0200 @@ -3,7 +3,8 @@ uses "../../../antiquote_setup.ML" "../../../more_antiquote.ML" begin -ML {* no_document use_thys ["Efficient_Nat", "Code_Char_chr"] *} +ML {* no_document use_thys + ["Efficient_Nat", "Code_Char_chr", "Product_ord"] *} ML_val {* Code_Target.code_width := 74 *} diff -r a01de3b3fa2e -r df77ed974a78 doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex Wed Oct 01 13:33:54 2008 +0200 @@ -0,0 +1,484 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Adaption}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Adaption\isanewline +\isakeyword{imports}\ Setup\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupsection{Adaption to target languages \label{sec:adaption}% +} +\isamarkuptrue% +% +\isamarkupsubsection{Common adaption cases% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code + generator setup + which should be suitable for most applications. Common extensions + and modifications are available by certain theories of the \isa{HOL} + library; beside being useful in applications, they may serve + as a tutorial for customising the code generator setup (see below + \secref{sec:adaption_mechanisms}). + + \begin{description} + + \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by big + integer literals in target languages. + \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by + character literals in target languages. + \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char}, + but also offers treatment of character codes; includes + \hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}. + \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements natural numbers by integers, + which in general will result in higher efficiency; pattern + matching with \isa{{\isadigit{0}}} / \isa{Suc} + is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}. + \item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] provides an additional datatype + \isa{index} which is mapped to target-language built-in integers. + Useful for code setups which involve e.g. indexing of + target-language arrays. + \item[\hyperlink{theory.Code-Message}{\mbox{\isa{Code{\isacharunderscore}Message}}}] provides an additional datatype + \isa{message{\isacharunderscore}string} which is isomorphic to strings; + \isa{message{\isacharunderscore}string}s are mapped to target-language strings. + Useful for code setups which involve e.g. printing (error) messages. + + \end{description} + + \begin{warn} + When importing any of these theories, they should form the last + items in an import list. Since these theories adapt the + code generator setup in a non-conservative fashion, + strange effects may occur otherwise. + \end{warn}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Adaption mechanisms \label{sec:adaption_mechanisms}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{warn} + The mechanisms shown here are especially for the curious; the user + rarely needs to do anything on his own beyond the defaults in \isa{HOL}. + Adaption is a delicated task which requires a lot of dilligence since + it happend \emph{completely} outside the logic. + \end{warn}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{isamarkuptext}% +Consider the following function and its corresponding + SML code:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{primrec}\isamarkupfalse% +\ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isadeliminvisible +% +\endisadeliminvisible +% +\isataginvisible +% +\endisataginvisible +{\isafoldinvisible}% +% +\isadeliminvisible +% +\endisadeliminvisible +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +% +\begin{isamarkuptext}% +\isaverbatim% +\noindent% +\verb|structure Example = |\newline% +\verb|struct|\newline% +\newline% +\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline% +\newline% +\verb|datatype boola = False |\verb,|,\verb| True;|\newline% +\newline% +\verb|fun anda x True = x|\newline% +\verb| |\verb,|,\verb| anda x False = False|\newline% +\verb| |\verb,|,\verb| anda True x = x|\newline% +\verb| |\verb,|,\verb| anda False x = False;|\newline% +\newline% +\verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline% +\verb| |\verb,|,\verb| less_nat n Zero_nat = False|\newline% +\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline% +\verb| |\verb,|,\verb| less_eq_nat Zero_nat n = True;|\newline% +\newline% +\verb|fun in_interval (k, l) n = anda (less_eq_nat k n) (less_eq_nat n l);|\newline% +\newline% +\verb|end; (*struct Example*)|% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent Though this is correct code, it is a little bit unsatisfactory: + boolean values and operators are materialised as distinguished + entities with have nothing to do with the SML-built-in notion + of \qt{bool}. This results in less readable code; + additionally, eager evaluation may cause programs to + loop or break which would perfectly terminate when + the existing SML \verb|bool| would be used. To map + the HOL \isa{bool} on SML \verb|bool|, we may use + \qn{custom serialisations}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtt +% +\endisadelimtt +% +\isatagtt +\isacommand{code{\isacharunderscore}type}\isamarkupfalse% +\ bool\isanewline +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline +\isacommand{code{\isacharunderscore}const}\isamarkupfalse% +\ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +% +\begin{isamarkuptext}% +\noindent The \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor + as arguments together with a list of custom serialisations. + Each custom serialisation starts with a target language + identifier followed by an expression, which during + code serialisation is inserted whenever the type constructor + would occur. For constants, \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements + the corresponding mechanism. Each ``\verb|_|'' in + a serialisation expression is treated as a placeholder + for the type constructor's (the constant's) arguments.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +% +\begin{isamarkuptext}% +\isaverbatim% +\noindent% +\verb|structure Example = |\newline% +\verb|struct|\newline% +\newline% +\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline% +\newline% +\verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline% +\verb| |\verb,|,\verb| less_nat n Zero_nat = false|\newline% +\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline% +\verb| |\verb,|,\verb| less_eq_nat Zero_nat n = true;|\newline% +\newline% +\verb|fun in_interval (k, l) n = (less_eq_nat k n) andalso (less_eq_nat n l);|\newline% +\newline% +\verb|end; (*struct Example*)|% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent This still is not perfect: the parentheses + around the \qt{andalso} expression are superfluous. + Though the serializer + by no means attempts to imitate the rich Isabelle syntax + framework, it provides some common idioms, notably + associative infixes with precedences which may be used here:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtt +% +\endisadelimtt +% +\isatagtt +\isacommand{code{\isacharunderscore}const}\isamarkupfalse% +\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline +\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +% +\begin{isamarkuptext}% +\isaverbatim% +\noindent% +\verb|structure Example = |\newline% +\verb|struct|\newline% +\newline% +\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline% +\newline% +\verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline% +\verb| |\verb,|,\verb| less_nat n Zero_nat = false|\newline% +\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline% +\verb| |\verb,|,\verb| less_eq_nat Zero_nat n = true;|\newline% +\newline% +\verb|fun in_interval (k, l) n = less_eq_nat k n andalso less_eq_nat n l;|\newline% +\newline% +\verb|end; (*struct Example*)|% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent Next, we try to map HOL pairs to SML pairs, using the + infix ``\verb|*|'' type constructor and parentheses:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadeliminvisible +% +\endisadeliminvisible +% +\isataginvisible +% +\endisataginvisible +{\isafoldinvisible}% +% +\isadeliminvisible +% +\endisadeliminvisible +% +\isadelimtt +% +\endisadelimtt +% +\isatagtt +\isacommand{code{\isacharunderscore}type}\isamarkupfalse% +\ {\isacharasterisk}\isanewline +\ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline +\isacommand{code{\isacharunderscore}const}\isamarkupfalse% +\ Pair\isanewline +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +% +\begin{isamarkuptext}% +\noindent The initial bang ``\verb|!|'' tells the serializer to never put + parentheses around the whole expression (they are already present), + while the parentheses around argument place holders + tell not to put parentheses around the arguments. + The slash ``\verb|/|'' (followed by arbitrary white space) + inserts a space which may be used as a break if necessary + during pretty printing. + + These examples give a glimpse what mechanisms + custom serialisations provide; however their usage + requires careful thinking in order not to introduce + inconsistencies -- or, in other words: + custom serialisations are completely axiomatic. + + A further noteworthy details is that any special + character in a custom serialisation may be quoted + using ``\verb|'|''; thus, in + ``\verb|fn '_ => _|'' the first + ``\verb|_|'' is a proper underscore while the + second ``\verb|_|'' is a placeholder. + + The HOL theories provide further + examples for custom serialisations.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{\isa{Haskell} serialisation% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +For convenience, the default + \isa{HOL} setup for \isa{Haskell} maps the \isa{eq} class to + its counterpart in \isa{Haskell}, giving custom serialisations + for the class \isa{eq} (by command \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation + \isa{eq{\isacharunderscore}class{\isachardot}eq}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtt +% +\endisadelimtt +% +\isatagtt +\isacommand{code{\isacharunderscore}class}\isamarkupfalse% +\ eq\isanewline +\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ {\isachardoublequoteopen}HOL{\isachardot}eq{\isachardoublequoteclose}\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline +\isanewline +\isacommand{code{\isacharunderscore}const}\isamarkupfalse% +\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline +\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +% +\begin{isamarkuptext}% +\noindent A problem now occurs whenever a type which + is an instance of \isa{eq} in \isa{HOL} is mapped + on a \isa{Haskell}-built-in type which is also an instance + of \isa{Haskell} \isa{Eq}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{typedecl}\isamarkupfalse% +\ bar\isanewline +\isanewline +\isacommand{instantiation}\isamarkupfalse% +\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline +\isakeyword{begin}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{instance}\isamarkupfalse% +\ \isacommand{by}\isamarkupfalse% +\ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline +\isanewline +\isacommand{end}\isamarkupfalse% +% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +\isanewline +% +\isadelimtt +\isanewline +% +\endisadelimtt +% +\isatagtt +\isacommand{code{\isacharunderscore}type}\isamarkupfalse% +\ bar\isanewline +\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +% +\begin{isamarkuptext}% +\noindent The code generator would produce + an additional instance, which of course is rejectedby the \isa{Haskell} + compiler. + To suppress this additional instance, use + \isa{code{\isacharunderscore}instance}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtt +% +\endisadelimtt +% +\isatagtt +\isacommand{code{\isacharunderscore}instance}\isamarkupfalse% +\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline +\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +\isanewline +% +\isadelimtheory +\isanewline +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r a01de3b3fa2e -r df77ed974a78 doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex Wed Oct 01 13:33:54 2008 +0200 @@ -0,0 +1,108 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Further}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Further\isanewline +\isakeyword{imports}\ Setup\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupsection{Further issues \label{sec:further}% +} +\isamarkuptrue% +% +\isamarkupsubsection{Further reading% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Do dive deeper into the issue of code generation, you should visit + the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} which + constains exhaustive syntax diagrams.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Modules% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command it is possible to leave + out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} part; then code is distributed over + different modules, where the module name space roughly is induced + by the \isa{Isabelle} theory namespace. + + Then sometimes the awkward situation occurs that dependencies between + definitions introduce cyclic dependencies between modules, which in the + \isa{Haskell} world leaves you to the mercy of the \isa{Haskell} implementation + you are using, while for \isa{SML}/\isa{OCaml} code generation is not possible. + + A solution is to declare module names explicitly. + Let use assume the three cyclically dependent + modules are named \emph{A}, \emph{B} and \emph{C}. + Then, by stating% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{code{\isacharunderscore}modulename}\isamarkupfalse% +\ SML\isanewline +\ \ A\ ABC\isanewline +\ \ B\ ABC\isanewline +\ \ C\ ABC% +\begin{isamarkuptext}% +we explicitly map all those modules on \emph{ABC}, + resulting in an ad-hoc merge of this three modules + at serialisation time.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Evaluation oracle% +} +\isamarkuptrue% +% +\isamarkupsubsection{Code antiquotation% +} +\isamarkuptrue% +% +\isamarkupsubsection{Creating new targets% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +extending targets, adding targets% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Imperative data structures% +} +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r a01de3b3fa2e -r df77ed974a78 doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex Wed Oct 01 13:33:54 2008 +0200 @@ -0,0 +1,369 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Introduction}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Introduction\isanewline +\isakeyword{imports}\ Setup\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupchapter{Code generation from \isa{Isabelle{\isacharslash}HOL} theories% +} +\isamarkuptrue% +% +\isamarkupsection{Introduction and Overview% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +This tutorial introduces a generic code generator for the + \isa{Isabelle} system. + Generic in the sense that the + \qn{target language} for which code shall ultimately be + generated is not fixed but may be an arbitrary state-of-the-art + functional programming language (currently, the implementation + supports \isa{SML} \cite{SML}, \isa{OCaml} \cite{OCaml} and \isa{Haskell} + \cite{haskell-revised-report}). + + Conceptually the code generator framework is part + of Isabelle's \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} meta logic framework; the logic + \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} which is an extension of \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} + already comes with a reasonable framework setup and thus provides + a good working horse for raising code-generation-driven + applications. So, we assume some familiarity and experience + with the ingredients of the \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} distribution theories. + (see also \cite{isa-tutorial}). + + The code generator aims to be usable with no further ado + in most cases while allowing for detailed customisation. + This manifests in the structure of this tutorial: after a short + conceptual introduction with an example (\secref{sec:intro}), + we discuss the generic customisation facilities (\secref{sec:program}). + A further section (\secref{sec:adaption}) is dedicated to the matter of + \qn{adaption} to specific target language environments. After some + further issues (\secref{sec:further}) we conclude with an overview + of some ML programming interfaces (\secref{sec:ml}). + + \begin{warn} + Ultimately, the code generator which this tutorial deals with + is supposed to replace the existing code generator + by Stefan Berghofer \cite{Berghofer-Nipkow:2002}. + So, for the moment, there are two distinct code generators + in Isabelle. In case of ambiguity, we will refer to the framework + described here as \isa{generic\ code\ generator}, to the + other as \isa{SML\ code\ generator}. + Also note that while the framework itself is + object-logic independent, only \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} provides a reasonable + framework setup. + \end{warn}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Code generation via shallow embedding \label{sec:intro}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The key concept for understanding \isa{Isabelle}'s code generation is + \emph{shallow embedding}, i.e.~logical entities like constants, types and + classes are identified with corresponding concepts in the target language. + + Inside \hyperlink{theory.HOL}{\mbox{\isa{HOL}}}, the \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}} and + \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} declarations form + the core of a functional programming language. The default code generator setup + allows to turn those into functional programs immediately. + This means that \qt{naive} code generation can proceed without further ado. + For example, here a simple \qt{implementation} of amortised queues:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{datatype}\isamarkupfalse% +\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ {\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}\ {\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\ ys{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\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}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent Then we can generate code e.g.~for \isa{SML} as follows:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{export{\isacharunderscore}code}\isamarkupfalse% +\ empty\ dequeue\ enqueue\ \isakeyword{in}\ SML\isanewline +\ \ \isakeyword{module{\isacharunderscore}name}\ Example\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}example{\isachardot}ML{\isachardoublequoteclose}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent resulting in the following code:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +% +\begin{isamarkuptext}% +\isaverbatim% +\noindent% +\verb|structure Example = |\newline% +\verb|struct|\newline% +\newline% +\verb|fun foldl f a [] = a|\newline% +\verb| |\verb,|,\verb| foldl f a (x :: xs) = foldl f (f a x) xs;|\newline% +\newline% +\verb|fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;|\newline% +\newline% +\verb|fun list_case f1 f2 (a :: lista) = f2 a lista|\newline% +\verb| |\verb,|,\verb| list_case f1 f2 [] = f1;|\newline% +\newline% +\verb|datatype 'a queue = Queue of 'a list * 'a list;|\newline% +\newline% +\verb|val empty : 'a queue = Queue ([], []);|\newline% +\newline% +\verb|fun dequeue (Queue ([], [])) = (NONE, Queue ([], []))|\newline% +\verb| |\verb,|,\verb| dequeue (Queue (xs, y :: ys)) = (SOME y, Queue (xs, ys))|\newline% +\verb| |\verb,|,\verb| dequeue (Queue (v :: va, [])) =|\newline% +\verb| let|\newline% +\verb| val y :: ys = rev (v :: va);|\newline% +\verb| in|\newline% +\verb| (SOME y, Queue ([], ys))|\newline% +\verb| end;|\newline% +\newline% +\verb|fun enqueue x (Queue (xs, ys)) = Queue (x :: xs, ys);|\newline% +\newline% +\verb|end; (*struct Example*)|% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent The \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command takes a space-separated list of + constants for which code shall be generated; anything else needed for those + is added implicitly. Then follows a target language identifier + (\isa{SML}, \isa{OCaml} or \isa{Haskell}) and a freely chosen module name. + A file name denotes the destination to store the generated code. Note that + the semantics of the destination depends on the target language: for + \isa{SML} and \isa{OCaml} it denotes a \emph{file}, for \isa{Haskell} + it denotes a \emph{directory} where a file named as the module name + (with extension \isa{{\isachardot}hs}) is written:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{export{\isacharunderscore}code}\isamarkupfalse% +\ empty\ dequeue\ enqueue\ \isakeyword{in}\ Haskell\isanewline +\ \ \isakeyword{module{\isacharunderscore}name}\ Example\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent This is how the corresponding code in \isa{Haskell} looks like:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +% +\begin{isamarkuptext}% +\isaverbatim% +\noindent% +\verb|module Example where {|\newline% +\newline% +\newline% +\verb|foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;|\newline% +\verb|foldla f a [] = a;|\newline% +\verb|foldla f a (x : xs) = foldla f (f a x) xs;|\newline% +\newline% +\verb|rev :: forall a. [a] -> [a];|\newline% +\verb|rev xs = foldla (\ xsa x -> x : xsa) [] xs;|\newline% +\newline% +\verb|list_case :: forall t a. t -> (a -> [a] -> t) -> [a] -> t;|\newline% +\verb|list_case f1 f2 (a : list) = f2 a list;|\newline% +\verb|list_case f1 f2 [] = f1;|\newline% +\newline% +\verb|data Queue a = Queue [a] [a];|\newline% +\newline% +\verb|empty :: forall a. Queue a;|\newline% +\verb|empty = Queue [] [];|\newline% +\newline% +\verb|dequeue :: forall a. Queue a -> (Maybe a, Queue a);|\newline% +\verb|dequeue (Queue [] []) = (Nothing, Queue [] []);|\newline% +\verb|dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);|\newline% +\verb|dequeue (Queue (v : va) []) =|\newline% +\verb| let {|\newline% +\verb| (y : ys) = rev (v : va);|\newline% +\verb| } in (Just y, Queue [] ys);|\newline% +\newline% +\verb|enqueue :: forall a. a -> Queue a -> Queue a;|\newline% +\verb|enqueue x (Queue xs ys) = Queue (x : xs) ys;|\newline% +\newline% +\verb|}|% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent This demonstrates the basic usage of the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command; + for more details see \secref{sec:further}.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Code generator architecture \label{sec:concept}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +What you have seen so far should be already enough in a lot of cases. If you + are content with this, you can quit reading here. Anyway, in order to customise + and adapt the code generator, it is inevitable to gain some understanding + how it works. + + \begin{figure}[h] + \centering + \includegraphics[width=0.7\textwidth]{codegen_process} + \caption{Code generator architecture} + \label{fig:arch} + \end{figure} + + The code generator employs a notion of executability + for three foundational executable ingredients known + from functional programming: + \emph{defining equations}, \emph{datatypes}, and + \emph{type classes}. A defining equation as a first approximation + is a theorem of the form \isa{f\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n\ {\isasymequiv}\ t} + (an equation headed by a constant \isa{f} with arguments + \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right hand side \isa{t}). + Code generation aims to turn defining equations + into a functional program. This is achieved by three major + components which operate sequentially, i.e. the result of one is + the input + of the next in the chain, see diagram \ref{fig:arch}: + + \begin{itemize} + + \item Out of the vast collection of theorems proven in a + \qn{theory}, a reasonable subset modelling + defining equations is \qn{selected}. + + \item On those selected theorems, certain + transformations are carried out + (\qn{preprocessing}). Their purpose is to turn theorems + representing non- or badly executable + specifications into equivalent but executable counterparts. + The result is a structured collection of \qn{code theorems}. + + \item Before the selected defining equations are continued with, + they can be \qn{preprocessed}, i.e. subjected to theorem + transformations. This \qn{preprocessor} is an interface which + allows to apply + the full expressiveness of ML-based theorem transformations + to code generation; motivating examples are shown below, see + \secref{sec:preproc}. + The result of the preprocessing step is a structured collection + of defining equations. + + \item These defining equations are \qn{translated} to a program + in an abstract intermediate language. Think of it as a kind + of \qt{Mini-Haskell} with four \qn{statements}: \isa{data} + (for datatypes), \isa{fun} (stemming from defining equations), + also \isa{class} and \isa{inst} (for type classes). + + \item Finally, the abstract program is \qn{serialised} into concrete + source code of a target language. + + \end{itemize} + + \noindent From these steps, only the two last are carried out outside the logic; by + keeping this layer as thin as possible, the amount of code to trust is + kept to a minimum.% +\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 a01de3b3fa2e -r df77ed974a78 doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex Wed Oct 01 13:33:54 2008 +0200 @@ -0,0 +1,255 @@ +% +\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} + \indexml{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\ + \indexml{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\ + \indexml{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list Susp.T -> theory -> theory| \\ + \indexml{Code.map\_pre}\verb|Code.map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\ + \indexml{Code.map\_post}\verb|Code.map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\ + \indexml{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline% +\verb| -> theory -> theory| \\ + \indexml{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\ + \indexml{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\ + \indexml{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline% +\verb| -> (string * sort) list * (string * typ list) list| \\ + \indexml{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string 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.add_eqnl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds + suspended defining equations \isa{lthms} for constant + \isa{const} to executable content. + + \item \verb|Code.map_pre|~\isa{f}~\isa{thy} changes + the preprocessor simpset. + + \item \verb|Code.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 defining 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 defining equations. + + \item \verb|Code.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_datatype_of_constr|~\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} + \indexml{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\ + \indexml{Code\_Unit.head\_eqn}\verb|Code_Unit.head_eqn: theory -> thm -> string * ((string * sort) list * typ)| \\ + \indexml{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: MetaSimplifier.simpset -> thm -> thm| \\ + \end{mldecls} + + \begin{description} + + \item \verb|Code_Unit.read_const|~\isa{thy}~\isa{s} + reads a constant as a concrete term expression \isa{s}. + + \item \verb|Code_Unit.head_eqn|~\isa{thy}~\isa{thm} + extracts the constant and its type from a defining equation \isa{thm}. + + \item \verb|Code_Unit.rewrite_eqn|~\isa{ss}~\isa{thm} + rewrites a defining equation \isa{thm} with a simpset \isa{ss}; + only arguments and right hand side are rewritten, + not the head of the defining equation. + + \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|CodeDataFun|; 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}\ CodeUnit{\isachardot}const\ 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|CodeDataFun| 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 a01de3b3fa2e -r df77ed974a78 doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Wed Oct 01 13:33:54 2008 +0200 @@ -0,0 +1,1127 @@ +% +\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}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} + statements are used for code generation. This default behaviour + can be changed, e.g. by providing different defining equations. + All kinds of customization shown in this section is \emph{safe} + in the sense that the user does not have to worry about + correctness -- all programs generatable that way are partially + correct.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Selecting code equations% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Coming back to our introductory example, we + could provide an alternative defining equations for \isa{dequeue} + explicitly:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ else\ dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ 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}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent The annotation \isa{{\isacharbrackleft}code\ func{\isacharbrackright}} is an \isa{Isar} + \isa{attribute} which states that the given theorems should be + considered as defining equations for a \isa{fun} statement -- + the corresponding constant is determined syntactically. The resulting code:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +% +\begin{isamarkuptext}% +\isaverbatim% +\noindent% +\verb|module Example where {|\newline% +\newline% +\newline% +\verb|foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;|\newline% +\verb|foldla f a [] = a;|\newline% +\verb|foldla f a (x : xs) = foldla f (f a x) xs;|\newline% +\newline% +\verb|rev :: forall a. [a] -> [a];|\newline% +\verb|rev xs = foldla (\ xsa x -> x : xsa) [] xs;|\newline% +\newline% +\verb|nulla :: forall a. [a] -> Bool;|\newline% +\verb|nulla (x : xs) = False;|\newline% +\verb|nulla [] = True;|\newline% +\newline% +\verb|data Queue a = Queue [a] [a];|\newline% +\newline% +\verb|empty :: forall a. Queue a;|\newline% +\verb|empty = Queue [] [];|\newline% +\newline% +\verb|dequeue :: forall a. Queue a -> (Maybe a, Queue a);|\newline% +\verb|dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);|\newline% +\verb|dequeue (Queue xs []) =|\newline% +\verb| (if nulla xs then (Nothing, Queue [] [])|\newline% +\verb| else dequeue (Queue [] (rev xs)));|\newline% +\newline% +\verb|enqueue :: forall a. a -> Queue a -> Queue a;|\newline% +\verb|enqueue x (Queue xs ys) = Queue (x : xs) ys;|\newline% +\newline% +\verb|}|% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\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 but rarely desired in practice. See \secref{sec:datatypes} for an example. + + As told in \secref{sec:concept}, code generation is based + on a structured collection of code theorems. + For explorative purpose, this collection + may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{code{\isacharunderscore}thms}\isamarkupfalse% +\ dequeue% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent prints a table with \emph{all} defining equations + for \isa{dequeue}, including + \emph{all} defining 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 defining 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% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{class}\isamarkupfalse% +\ semigroup\ {\isacharequal}\ type\ {\isacharplus}\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% +% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent We define the natural operation of the natural numbers + on monoids:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\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}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent This we use to define the discrete exponentiation function:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\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}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent The corresponding code:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +% +\begin{isamarkuptext}% +\isaverbatim% +\noindent% +\verb|module Example where {|\newline% +\newline% +\newline% +\verb|data Nat = Suc Nat |\verb,|,\verb| Zero_nat;|\newline% +\newline% +\verb|class Semigroup a where {|\newline% +\verb| mult :: a -> a -> a;|\newline% +\verb|};|\newline% +\newline% +\verb|class (Semigroup a) => Monoid a where {|\newline% +\verb| neutral :: a;|\newline% +\verb|};|\newline% +\newline% +\verb|pow :: forall a. (Monoid a) => Nat -> a -> a;|\newline% +\verb|pow (Suc n) a = mult a (pow n a);|\newline% +\verb|pow Zero_nat a = neutral;|\newline% +\newline% +\verb|plus_nat :: Nat -> Nat -> Nat;|\newline% +\verb|plus_nat (Suc m) n = plus_nat m (Suc n);|\newline% +\verb|plus_nat Zero_nat n = n;|\newline% +\newline% +\verb|neutral_nat :: Nat;|\newline% +\verb|neutral_nat = Suc Zero_nat;|\newline% +\newline% +\verb|mult_nat :: Nat -> Nat -> Nat;|\newline% +\verb|mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline% +\verb|mult_nat Zero_nat n = Zero_nat;|\newline% +\newline% +\verb|instance Semigroup Nat where {|\newline% +\verb| mult = mult_nat;|\newline% +\verb|};|\newline% +\newline% +\verb|instance Monoid Nat where {|\newline% +\verb| neutral = neutral_nat;|\newline% +\verb|};|\newline% +\newline% +\verb|bexp :: Nat -> Nat;|\newline% +\verb|bexp n = pow n (Suc (Suc Zero_nat));|\newline% +\newline% +\verb|}|% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\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}):% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +% +\begin{isamarkuptext}% +\isaverbatim% +\noindent% +\verb|structure Example = |\newline% +\verb|struct|\newline% +\newline% +\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline% +\newline% +\verb|type 'a semigroup = {mult : 'a -> 'a -> 'a};|\newline% +\verb|fun mult (A_:'a semigroup) = #mult A_;|\newline% +\newline% +\verb|type 'a monoid = {Program__semigroup_monoid : 'a semigroup, neutral : 'a};|\newline% +\verb|fun semigroup_monoid (A_:'a monoid) = #Program__semigroup_monoid A_;|\newline% +\verb|fun neutral (A_:'a monoid) = #neutral A_;|\newline% +\newline% +\verb|fun pow A_ (Suc n) a = mult (semigroup_monoid A_) a (pow A_ n a)|\newline% +\verb| |\verb,|,\verb| pow A_ Zero_nat a = neutral A_;|\newline% +\newline% +\verb|fun plus_nat (Suc m) n = plus_nat m (Suc n)|\newline% +\verb| |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline% +\newline% +\verb|val neutral_nat : nat = Suc Zero_nat;|\newline% +\newline% +\verb|fun mult_nat (Suc m) n = plus_nat n (mult_nat m n)|\newline% +\verb| |\verb,|,\verb| mult_nat Zero_nat n = Zero_nat;|\newline% +\newline% +\verb|val semigroup_nat = {mult = mult_nat} : nat semigroup;|\newline% +\newline% +\verb|val monoid_nat =|\newline% +\verb| {Program__semigroup_monoid = semigroup_nat, neutral = neutral_nat} :|\newline% +\verb| nat monoid;|\newline% +\newline% +\verb|fun bexp n = pow monoid_nat n (Suc (Suc Zero_nat));|\newline% +\newline% +\verb|end; (*struct Example*)|% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\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} allows to employ the full generality of the Isabelle + simplifier. Due to the interpretation of theorems + as defining equations, rewrites are applied to the right + hand side and the arguments of the left hand side of an + equation, but never to the constant heading the left hand side. + An important special case are \emph{inline theorems} which may be + declared and undeclared using the + \emph{code inline} or \emph{code inline del} attribute respectively. + + Some common applications:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{itemize} +% +\begin{isamarkuptext}% +\item replacing non-executable constructs by executable ones:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\item eliminating superfluous constants:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ simp% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\item replacing executable but inconvenient constructs:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\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-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command. + \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient + mechanism to inspect the impact of a preprocessor setup + on defining equations. + + \begin{warn} + The attribute \emph{code unfold} + associated with the \isa{SML\ code\ generator} also applies to + the \isa{generic\ code\ generator}: + \emph{code unfold} implies \emph{code inline}. + \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 excactly 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 may be convenient to alter or + extend this table; as an example, we will develop an alternative + representation of natural numbers as binary digits, whose + size does increase logarithmically with its value, not linear + \footnote{Indeed, the \hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}} theory (see \ref{eff_nat}) + does something similar}. First, the digit representation:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{definition}\isamarkupfalse% +\ Dig{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ n{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ \ Dig{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent We will use these two \qt{digits} to represent natural numbers + in binary digits, e.g.:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{lemma}\isamarkupfalse% +\ {\isadigit{4}}{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent Of course we also have to provide proper code equations for + the operations, e.g. \isa{op\ {\isacharplus}}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{lemma}\isamarkupfalse% +\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}m\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ n{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{1}}\ m{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent We then instruct the code generator to view \isa{{\isadigit{0}}}, + \isa{{\isadigit{1}}}, \isa{Dig{\isadigit{0}}} and \isa{Dig{\isadigit{1}}} as + datatype constructors:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isadigit{0}}{\isasymColon}nat{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{1}}{\isasymColon}nat{\isachardoublequoteclose}\ Dig{\isadigit{0}}\ Dig{\isadigit{1}}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent For the former constructor \isa{Suc}, we provide a code + equation and remove some parts of the default code generator setup + which are an obstacle here:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{lemma}\isamarkupfalse% +\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\isanewline +\isacommand{declare}\isamarkupfalse% +\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline +\isacommand{declare}\isamarkupfalse% +\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent This yields the following code:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +% +\begin{isamarkuptext}% +\isaverbatim% +\noindent% +\verb|structure Example = |\newline% +\verb|struct|\newline% +\newline% +\verb|datatype nat = Dig1 of nat |\verb,|,\verb| Dig0 of nat |\verb,|,\verb| One_nat |\verb,|,\verb| Zero_nat;|\newline% +\newline% +\verb|fun plus_nat (Dig1 m) (Dig1 n) = Dig0 (plus_nat (plus_nat m n) One_nat)|\newline% +\verb| |\verb,|,\verb| plus_nat (Dig1 m) (Dig0 n) = Dig1 (plus_nat m n)|\newline% +\verb| |\verb,|,\verb| plus_nat (Dig0 m) (Dig1 n) = Dig1 (plus_nat m n)|\newline% +\verb| |\verb,|,\verb| plus_nat (Dig0 m) (Dig0 n) = Dig0 (plus_nat m n)|\newline% +\verb| |\verb,|,\verb| plus_nat (Dig1 m) One_nat = Dig0 (plus_nat m One_nat)|\newline% +\verb| |\verb,|,\verb| plus_nat One_nat (Dig1 n) = Dig0 (plus_nat n One_nat)|\newline% +\verb| |\verb,|,\verb| plus_nat (Dig0 m) One_nat = Dig1 m|\newline% +\verb| |\verb,|,\verb| plus_nat One_nat (Dig0 n) = Dig1 n|\newline% +\verb| |\verb,|,\verb| plus_nat m Zero_nat = m|\newline% +\verb| |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline% +\newline% +\verb|end; (*struct Example*)|% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent From this example, it can be easily glimpsed that using own constructor sets + is a little delicate since it changes the set of valid patterns for values + of that type. Without going into much detail, here some practical hints: + + \begin{itemize} + \item When changing the constructor set for datatypes, take care to + provide an alternative for the \isa{case} combinator (e.g.~by replacing + it using the preprocessor). + \item Values in the target language need not to be normalised -- different + values in the target language may represent the same value in the + logic (e.g. \isa{Dig{\isadigit{1}}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}}). + \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% +% +\isadeliminvisible +% +\endisadeliminvisible +% +\isataginvisible +\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}\ Suc\isanewline +\isacommand{declare}\isamarkupfalse% +\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\isanewline +\isacommand{declare}\isamarkupfalse% +\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline{\isacharbrackright}\isanewline +\isacommand{declare}\isamarkupfalse% +\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func{\isacharbrackright}\ \isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ simp% +\endisataginvisible +{\isafoldinvisible}% +% +\isadeliminvisible +% +\endisadeliminvisible +% +\isamarkupsubsection{Equality and wellsortedness% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Surely you have already noticed how equality is treated + by the code generator:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\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}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent The membership test during preprocessing is rewritten, + resulting in \isa{op\ mem}, which itself + performs an explicit equality check.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +% +\begin{isamarkuptext}% +\isaverbatim% +\noindent% +\verb|structure Example = |\newline% +\verb|struct|\newline% +\newline% +\verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline% +\verb|fun eq (A_:'a eq) = #eq A_;|\newline% +\newline% +\verb|fun eqop A_ a b = eq A_ a b;|\newline% +\newline% +\verb|fun member A_ x (y :: ys) = (if eqop A_ y x then true else member A_ x ys)|\newline% +\verb| |\verb,|,\verb| member A_ x [] = false;|\newline% +\newline% +\verb|fun collect_duplicates A_ xs ys (z :: zs) =|\newline% +\verb| (if member A_ z xs|\newline% +\verb| then (if member A_ z ys then collect_duplicates A_ xs ys zs|\newline% +\verb| else collect_duplicates A_ xs (z :: ys) zs)|\newline% +\verb| else collect_duplicates A_ (z :: xs) (z :: ys) zs)|\newline% +\verb| |\verb,|,\verb| collect_duplicates A_ xs ys [] = xs;|\newline% +\newline% +\verb|end; (*struct Example*)|% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\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 defining 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. + + Though this \isa{eq} class is designed to get rarely in + the way, a subtlety + enters the stage when definitions of overloaded constants + are dependent on operational equality. For example, let + us define a lexicographic ordering on tuples + (also see theory \hyperlink{theory.Product-ord}{\mbox{\isa{Product{\isacharunderscore}ord}}}):% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{instantiation}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}order{\isacharcomma}\ order{\isacharparenright}\ order\isanewline +\isakeyword{begin}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}x\ {\isasymle}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isasymle}\ snd\ y{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}x\ {\isacharless}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isacharless}\ snd\ y{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{instance}\isamarkupfalse% +\ \isacommand{proof}\isamarkupfalse% +\isanewline +\isacommand{qed}\isamarkupfalse% +\ {\isacharparenleft}auto\ simp{\isacharcolon}\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}prod{\isacharunderscore}def\ intro{\isacharcolon}\ order{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}\isanewline +\isanewline +\isacommand{end}\isamarkupfalse% +\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ order{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline +\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline +\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent Then code generation will fail. Why? The definition + of \isa{op\ {\isasymle}} depends on equality on both arguments, + which are polymorphic and impose an additional \isa{eq} + class constraint, which the preprocessor does not propagate + (for technical reasons). + + The solution is to add \isa{eq} explicitly to the first sort arguments in the + code theorems:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{lemma}\isamarkupfalse% +\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline +\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline +\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent Then code generation succeeds:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +% +\begin{isamarkuptext}% +\isaverbatim% +\noindent% +\verb|structure Example = |\newline% +\verb|struct|\newline% +\newline% +\verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline% +\verb|fun eq (A_:'a eq) = #eq A_;|\newline% +\newline% +\verb|type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};|\newline% +\verb|fun less_eq (A_:'a ord) = #less_eq A_;|\newline% +\verb|fun less (A_:'a ord) = #less A_;|\newline% +\newline% +\verb|fun eqop A_ a b = eq A_ a b;|\newline% +\newline% +\verb|type 'a preorder = {Orderings__ord_preorder : 'a ord};|\newline% +\verb|fun ord_preorder (A_:'a preorder) = #Orderings__ord_preorder A_;|\newline% +\newline% +\verb|type 'a order = {Orderings__preorder_order : 'a preorder};|\newline% +\verb|fun preorder_order (A_:'a order) = #Orderings__preorder_order A_;|\newline% +\newline% +\verb|fun less_eqa (A1_, A2_) B_ (x1, y1) (x2, y2) =|\newline% +\verb| less ((ord_preorder o preorder_order) A2_) x1 x2 orelse|\newline% +\verb| eqop A1_ x1 x2 andalso|\newline% +\verb| less_eq ((ord_preorder o preorder_order) B_) y1 y2|\newline% +\verb| |\verb,|,\verb| less_eqa (A1_, A2_) B_ (x1, y1) (x2, y2) =|\newline% +\verb| less ((ord_preorder o preorder_order) A2_) x1 x2 orelse|\newline% +\verb| eqop A1_ x1 x2 andalso|\newline% +\verb| less_eq ((ord_preorder o preorder_order) B_) y1 y2;|\newline% +\newline% +\verb|end; (*struct Example*)|% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +In some cases, the automatically derived defining equations + for equality on a particular type may not be appropriate. + As example, watch the following datatype representing + monomorphic parametric types (where type constructors + are referred to by natural numbers):% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{datatype}\isamarkupfalse% +\ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +Then code generation for SML would fail with a message + that the generated code contains illegal mutual dependencies: + the theorem \isa{Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymequiv}\ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ typargs{\isadigit{1}}\ {\isacharequal}\ typargs{\isadigit{2}}} already requires the + instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires + \isa{Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymequiv}\ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ typargs{\isadigit{1}}\ {\isacharequal}\ typargs{\isadigit{2}}}; Haskell has no problem with mutually + recursive \isa{inst} and \isa{fun} definitions, + but the SML serializer does not support this. + + In such cases, you have to provide your own equality equations + involving auxiliary constants. In our case, + \isa{list{\isacharunderscore}all{\isadigit{2}}} can do the job:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +\isacommand{lemma}\isamarkupfalse% +\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline +\ \ \ \ \ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\begin{isamarkuptext}% +\noindent does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isatagquoteme +% +\begin{isamarkuptext}% +\isaverbatim% +\noindent% +\verb|structure Example = |\newline% +\verb|struct|\newline% +\newline% +\verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline% +\verb|fun eq (A_:'a eq) = #eq A_;|\newline% +\newline% +\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline% +\newline% +\verb|fun eqop A_ a b = eq A_ a b;|\newline% +\newline% +\verb|fun null (x :: xs) = false|\newline% +\verb| |\verb,|,\verb| null [] = true;|\newline% +\newline% +\verb|fun eq_nat (Suc a) Zero_nat = false|\newline% +\verb| |\verb,|,\verb| eq_nat Zero_nat (Suc a) = false|\newline% +\verb| |\verb,|,\verb| eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'|\newline% +\verb| |\verb,|,\verb| eq_nat Zero_nat Zero_nat = true;|\newline% +\newline% +\verb|val eq_nata = {eq = eq_nat} : nat eq;|\newline% +\newline% +\verb|datatype monotype = Mono of nat * monotype list;|\newline% +\newline% +\verb|fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys|\newline% +\verb| |\verb,|,\verb| list_all2 p xs [] = null xs|\newline% +\verb| |\verb,|,\verb| list_all2 p [] ys = null ys;|\newline% +\newline% +\verb|fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =|\newline% +\verb| eqop eq_nata tyco1 tyco2 andalso|\newline% +\verb| list_all2 eq_monotype typargs1 typargs2;|\newline% +\newline% +\verb|end; (*struct Example*)|% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquoteme +{\isafoldquoteme}% +% +\isadelimquoteme +% +\endisadelimquoteme +% +\isamarkupsubsection{Partiality% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, examples: maps% +\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 a01de3b3fa2e -r df77ed974a78 doc-src/IsarAdvanced/Codegen/codegen.tex --- a/doc-src/IsarAdvanced/Codegen/codegen.tex Wed Oct 01 12:18:18 2008 +0200 +++ b/doc-src/IsarAdvanced/Codegen/codegen.tex Wed Oct 01 13:33:54 2008 +0200 @@ -48,7 +48,7 @@ \maketitle \begin{abstract} - This tutorial gives am introduction to a generic code generator framework in Isabelle + 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. \end{abstract}