# HG changeset patch # User haftmann # Date 1276580568 -7200 # Node ID a2a89563bfcb52c2d9ed642c652d5c20386e484b # Parent 4656ef45fedfd1476ee012cda8908a20ea45ab98# Parent e732b4f8fddf1643c443f41c62d57570b375b3dd merged diff -r 4656ef45fedf -r a2a89563bfcb NEWS --- a/NEWS Mon Jun 14 21:49:25 2010 +0200 +++ b/NEWS Tue Jun 15 07:42:48 2010 +0200 @@ -28,6 +28,14 @@ * Removed simplifier congruence rule of "prod_case", as has for long been the case with "split". +* Datatype package: theorems generated for executable equality +(class eq) carry proper names and are treated as default code +equations. + +* List.thy: use various operations from the Haskell prelude when +generating Haskell code. + + New in Isabelle2009-2 (June 2010) --------------------------------- diff -r 4656ef45fedf -r a2a89563bfcb doc-src/Codegen/Thy/Further.thy --- a/doc-src/Codegen/Thy/Further.thy Mon Jun 14 21:49:25 2010 +0200 +++ b/doc-src/Codegen/Thy/Further.thy Tue Jun 15 07:42:48 2010 +0200 @@ -12,6 +12,87 @@ contains exhaustive syntax diagrams. *} +subsection {* Locales and interpretation *} + +text {* + A technical issue comes to surface when generating code from + specifications stemming from locale interpretation. + + Let us assume a locale specifying a power operation + on arbitrary types: +*} + +locale %quote power = + fixes power :: "'a \ 'b \ 'b" + assumes power_commute: "power x \ power y = power y \ power x" +begin + +text {* + \noindent Inside that locale we can lift @{text power} to exponent lists + by means of specification relative to that locale: +*} + +primrec %quote powers :: "'a list \ 'b \ 'b" where + "powers [] = id" +| "powers (x # xs) = power x \ powers xs" + +lemma %quote powers_append: + "powers (xs @ ys) = powers xs \ powers ys" + by (induct xs) simp_all + +lemma %quote powers_power: + "powers xs \ power x = power x \ powers xs" + by (induct xs) + (simp_all del: o_apply id_apply add: o_assoc [symmetric], + simp del: o_apply add: o_assoc power_commute) + +lemma %quote powers_rev: + "powers (rev xs) = powers xs" + by (induct xs) (simp_all add: powers_append powers_power) + +end %quote + +text {* + After an interpretation of this locale (say, @{command + interpretation} @{text "fun_power:"} @{term [source] "power (\n (f :: + 'a \ 'a). f ^^ n)"}), one would expect to have a constant @{text + "fun_power.powers :: nat list \ ('a \ 'a) \ 'a \ 'a"} for which code + can be generated. But this not the case: internally, the term + @{text "fun_power.powers"} is an abbreviation for the foundational + term @{term [source] "power.powers (\n (f :: 'a \ 'a). f ^^ n)"} + (see \cite{isabelle-locale} for the details behind). + + Furtunately, with minor effort the desired behaviour can be achieved. + First, a dedicated definition of the constant on which the local @{text "powers"} + after interpretation is supposed to be mapped on: +*} + +definition %quote funpows :: "nat list \ ('a \ 'a) \ 'a \ 'a" where + [code del]: "funpows = power.powers (\n f. f ^^ n)" + +text {* + \noindent In general, the pattern is @{text "c = t"} where @{text c} is + the name of the future constant and @{text t} the foundational term + corresponding to the local constant after interpretation. + + The interpretation itself is enriched with an equation @{text "t = c"}: +*} + +interpretation %quote fun_power: power "\n (f :: 'a \ 'a). f ^^ n" where + "power.powers (\n f. f ^^ n) = funpows" + by unfold_locales + (simp_all add: expand_fun_eq funpow_mult mult_commute funpows_def) + +text {* + \noindent This additional equation is trivially proved by the definition + itself. + + After this setup procedure, code generation can continue as usual: +*} + +text %quote {*@{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}*} + + subsection {* Modules *} text {* diff -r 4656ef45fedf -r a2a89563bfcb doc-src/Codegen/Thy/Program.thy --- a/doc-src/Codegen/Thy/Program.thy Mon Jun 14 21:49:25 2010 +0200 +++ b/doc-src/Codegen/Thy/Program.thy Tue Jun 15 07:42:48 2010 +0200 @@ -134,7 +134,8 @@ text {* \noindent This is a convenient place to show how explicit dictionary construction - manifests in generated code (here, the same example in @{text SML}): + manifests in generated code (here, the same example in @{text SML}) + \cite{Haftmann-Nipkow:2010:code}: *} text %quote {*@{code_stmts bexp (SML)}*} diff -r 4656ef45fedf -r a2a89563bfcb doc-src/Codegen/Thy/document/Further.tex --- a/doc-src/Codegen/Thy/document/Further.tex Mon Jun 14 21:49:25 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Further.tex Tue Jun 15 07:42:48 2010 +0200 @@ -33,6 +33,170 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsection{Locales and interpretation% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +A technical issue comes to surface when generating code from + specifications stemming from locale interpretation. + + Let us assume a locale specifying a power operation + on arbitrary types:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{locale}\isamarkupfalse% +\ power\ {\isacharequal}\isanewline +\ \ \isakeyword{fixes}\ power\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{assumes}\ power{\isacharunderscore}commute{\isacharcolon}\ {\isachardoublequoteopen}power\ x\ {\isasymcirc}\ power\ y\ {\isacharequal}\ power\ y\ {\isasymcirc}\ power\ x{\isachardoublequoteclose}\isanewline +\isakeyword{begin}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent Inside that locale we can lift \isa{power} to exponent lists + by means of specification relative to that locale:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{primrec}\isamarkupfalse% +\ powers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}powers\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}powers\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharequal}\ power\ x\ {\isasymcirc}\ powers\ xs{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ powers{\isacharunderscore}append{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}powers\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ powers\ xs\ {\isasymcirc}\ powers\ ys{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ powers{\isacharunderscore}power{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}powers\ xs\ {\isasymcirc}\ power\ x\ {\isacharequal}\ power\ x\ {\isasymcirc}\ powers\ xs{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ xs{\isacharparenright}\isanewline +\ \ \ \ {\isacharparenleft}simp{\isacharunderscore}all\ del{\isacharcolon}\ o{\isacharunderscore}apply\ id{\isacharunderscore}apply\ add{\isacharcolon}\ o{\isacharunderscore}assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcomma}\isanewline +\ \ \ \ \ \ simp\ del{\isacharcolon}\ o{\isacharunderscore}apply\ add{\isacharcolon}\ o{\isacharunderscore}assoc\ power{\isacharunderscore}commute{\isacharparenright}\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ powers{\isacharunderscore}rev{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}powers\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ powers\ xs{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ xs{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ powers{\isacharunderscore}append\ powers{\isacharunderscore}power{\isacharparenright}\isanewline +\isanewline +\isacommand{end}\isamarkupfalse% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +After an interpretation of this locale (say, \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} \isa{fun{\isacharunderscore}power{\isacharcolon}} \isa{{\isachardoublequote}power\ {\isacharparenleft}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequote}}), one would expect to have a constant \isa{fun{\isacharunderscore}power{\isachardot}powers\ {\isacharcolon}{\isacharcolon}\ nat\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} for which code + can be generated. But this not the case: internally, the term + \isa{fun{\isacharunderscore}power{\isachardot}powers} is an abbreviation for the foundational + term \isa{{\isachardoublequote}power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequote}} + (see \cite{isabelle-locale} for the details behind). + + Furtunately, with minor effort the desired behaviour can be achieved. + First, a dedicated definition of the constant on which the local \isa{powers} + after interpretation is supposed to be mapped on:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{definition}\isamarkupfalse% +\ funpows\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}funpows\ {\isacharequal}\ power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ f{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent In general, the pattern is \isa{c\ {\isacharequal}\ t} where \isa{c} is + the name of the future constant and \isa{t} the foundational term + corresponding to the local constant after interpretation. + + The interpretation itself is enriched with an equation \isa{t\ {\isacharequal}\ c}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{interpretation}\isamarkupfalse% +\ fun{\isacharunderscore}power{\isacharcolon}\ power\ {\isachardoublequoteopen}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ f{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}\ {\isacharequal}\ funpows{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ unfold{\isacharunderscore}locales\isanewline +\ \ \ \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq\ funpow{\isacharunderscore}mult\ mult{\isacharunderscore}commute\ funpows{\isacharunderscore}def{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent This additional equation is trivially proved by the definition + itself. + + After this setup procedure, code generation can continue as usual:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}funpow ::~forall a.~Nat -> (a -> a) -> a -> a;\\ +\hspace*{0pt}funpow Zero{\char95}nat f = id;\\ +\hspace*{0pt}funpow (Suc n) f = f .~funpow n f;\\ +\hspace*{0pt}\\ +\hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\ +\hspace*{0pt}funpows [] = id;\\ +\hspace*{0pt}funpows (x :~xs) = funpow x .~funpows xs;% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% \isamarkupsubsection{Modules% } \isamarkuptrue% diff -r 4656ef45fedf -r a2a89563bfcb doc-src/Codegen/Thy/document/Introduction.tex --- a/doc-src/Codegen/Thy/document/Introduction.tex Mon Jun 14 21:49:25 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Tue Jun 15 07:42:48 2010 +0200 @@ -234,13 +234,6 @@ \noindent% \hspace*{0pt}module Example where {\char123}\\ \hspace*{0pt}\\ -\hspace*{0pt}foldla ::~forall a b.~(a -> b -> a) -> a -> [b] -> a;\\ -\hspace*{0pt}foldla f a [] = a;\\ -\hspace*{0pt}foldla f a (x :~xs) = foldla f (f a x) xs;\\ -\hspace*{0pt}\\ -\hspace*{0pt}rev ::~forall a.~[a] -> [a];\\ -\hspace*{0pt}rev xs = foldla ({\char92}~xsa x -> x :~xsa) [] xs;\\ -\hspace*{0pt}\\ \hspace*{0pt}list{\char95}case ::~forall a b.~a -> (b -> [b] -> a) -> [b] -> a;\\ \hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\ \hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\ diff -r 4656ef45fedf -r a2a89563bfcb doc-src/Codegen/Thy/document/Program.tex --- a/doc-src/Codegen/Thy/document/Program.tex Mon Jun 14 21:49:25 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Program.tex Tue Jun 15 07:42:48 2010 +0200 @@ -323,7 +323,8 @@ % \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}):% + manifests in generated code (here, the same example in \isa{SML}) + \cite{Haftmann-Nipkow:2010:code}:% \end{isamarkuptext}% \isamarkuptrue% % diff -r 4656ef45fedf -r a2a89563bfcb doc-src/Codegen/Thy/examples/Example.hs --- a/doc-src/Codegen/Thy/examples/Example.hs Mon Jun 14 21:49:25 2010 +0200 +++ b/doc-src/Codegen/Thy/examples/Example.hs Tue Jun 15 07:42:48 2010 +0200 @@ -2,13 +2,6 @@ module Example where { -foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a; -foldla f a [] = a; -foldla f a (x : xs) = foldla f (f a x) xs; - -rev :: forall a. [a] -> [a]; -rev xs = foldla (\ xsa x -> x : xsa) [] xs; - list_case :: forall a b. a -> (b -> [b] -> a) -> [b] -> a; list_case f1 f2 (a : list) = f2 a list; list_case f1 f2 [] = f1; diff -r 4656ef45fedf -r a2a89563bfcb doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Jun 14 21:49:25 2010 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Jun 15 07:42:48 2010 +0200 @@ -965,7 +965,214 @@ instantiates these mechanisms in a way that is amenable to end-user applications. - One framework generates code from both functional and relational + \medskip One framework generates code from functional programs + (including overloading using type classes) to SML \cite{SML}, OCaml + \cite{OCaml} and Haskell \cite{haskell-revised-report}. + Conceptually, code generation is split up in three steps: + \emph{selection} of code theorems, \emph{translation} into an + abstract executable view and \emph{serialization} to a specific + \emph{target language}. Inductive specifications can be executed + using the predicate compiler which operates within HOL. + See \cite{isabelle-codegen} for an introduction. + + \begin{matharray}{rcl} + @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{attribute_def (HOL) code} & : & @{text attribute} \\ + @{command_def (HOL) "code_abort"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_datatype"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{attribute_def (HOL) code_inline} & : & @{text attribute} \\ + @{attribute_def (HOL) code_post} & : & @{text attribute} \\ + @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def (HOL) "code_const"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_type"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_class"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_instance"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_reserved"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_monad"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_include"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_modulename"} & : & @{text "theory \ theory"} \\ + \end{matharray} + + \begin{rail} + 'export\_code' ( constexpr + ) \\ + ( ( 'in' target ( 'module\_name' string ) ? \\ + ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ? + ; + + const: term + ; + + constexpr: ( const | 'name.*' | '*' ) + ; + + typeconstructor: nameref + ; + + class: nameref + ; + + target: 'OCaml' | 'SML' | 'Haskell' + ; + + 'code' ( 'del' ) ? + ; + + 'code\_abort' ( const + ) + ; + + 'code\_datatype' ( const + ) + ; + + 'code_inline' ( 'del' ) ? + ; + + 'code_post' ( 'del' ) ? + ; + + 'code\_thms' ( constexpr + ) ? + ; + + 'code\_deps' ( constexpr + ) ? + ; + + 'code\_const' (const + 'and') \\ + ( ( '(' target ( syntax ? + 'and' ) ')' ) + ) + ; + + 'code\_type' (typeconstructor + 'and') \\ + ( ( '(' target ( syntax ? + 'and' ) ')' ) + ) + ; + + 'code\_class' (class + 'and') \\ + ( ( '(' target \\ ( string ? + 'and' ) ')' ) + ) + ; + + 'code\_instance' (( typeconstructor '::' class ) + 'and') \\ + ( ( '(' target ( '-' ? + 'and' ) ')' ) + ) + ; + + 'code\_reserved' target ( string + ) + ; + + 'code\_monad' const const target + ; + + 'code\_include' target ( string ( string | '-') ) + ; + + 'code\_modulename' target ( ( string string ) + ) + ; + + syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string + ; + + \end{rail} + + \begin{description} + + \item @{command (HOL) "export_code"} generates code for a given list + of constants in the specified target language(s). If no serialization + instruction is given, only abstract code is generated internally. + + Constants may be specified by giving them literally, referring to + all executable contants within a certain theory by giving @{text + "name.*"}, or referring to \emph{all} executable constants currently + available by giving @{text "*"}. + + By default, for each involved theory one corresponding name space + module is generated. Alternativly, a module name may be specified + after the @{keyword "module_name"} keyword; then \emph{all} code is + placed in this module. + + For \emph{SML} and \emph{OCaml}, the file specification refers to a + single file; for \emph{Haskell}, it refers to a whole directory, + where code is generated in multiple files reflecting the module + hierarchy. The file specification ``@{text "-"}'' denotes standard + output. For \emph{SML}, omitting the file specification compiles + code internally in the context of the current ML session. + + Serializers take an optional list of arguments in parentheses. For + \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits + explicit module signatures. + + For \emph{Haskell} a module name prefix may be given using the ``@{text + "root:"}'' argument; ``@{text string_classes}'' adds a ``@{verbatim + "deriving (Read, Show)"}'' clause to each appropriate datatype + declaration. + + \item @{attribute (HOL) code} explicitly selects (or with option + ``@{text "del"}'' deselects) a code equation for code + generation. Usually packages introducing code equations provide + a reasonable default setup for selection. + + \item @{command (HOL) "code_abort"} declares constants which are not + required to have a definition by means of code equations; if + needed these are implemented by program abort instead. + + \item @{command (HOL) "code_datatype"} specifies a constructor set + for a logical type. + + \item @{command (HOL) "print_codesetup"} gives an overview on + selected code equations and code generator datatypes. + + \item @{attribute (HOL) code_inline} declares (or with + option ``@{text "del"}'' removes) inlining theorems which are + applied as rewrite rules to any code equation during + preprocessing. + + \item @{attribute (HOL) code_post} declares (or with + option ``@{text "del"}'' removes) theorems which are + applied as rewrite rules to any result of an evaluation. + + \item @{command (HOL) "print_codeproc"} prints the setup + of the code generator preprocessor. + + \item @{command (HOL) "code_thms"} prints a list of theorems + representing the corresponding program containing all given + constants after preprocessing. + + \item @{command (HOL) "code_deps"} visualizes dependencies of + theorems representing the corresponding program containing all given + constants after preprocessing. + + \item @{command (HOL) "code_const"} associates a list of constants + with target-specific serializations; omitting a serialization + deletes an existing serialization. + + \item @{command (HOL) "code_type"} associates a list of type + constructors with target-specific serializations; omitting a + serialization deletes an existing serialization. + + \item @{command (HOL) "code_class"} associates a list of classes + with target-specific class names; omitting a serialization deletes + an existing serialization. This applies only to \emph{Haskell}. + + \item @{command (HOL) "code_instance"} declares a list of type + constructor / class instance relations as ``already present'' for a + given target. Omitting a ``@{text "-"}'' deletes an existing + ``already present'' declaration. This applies only to + \emph{Haskell}. + + \item @{command (HOL) "code_reserved"} declares a list of names as + reserved for a given target, preventing it to be shadowed by any + generated code. + + \item @{command (HOL) "code_monad"} provides an auxiliary mechanism + to generate monadic code for Haskell. + + \item @{command (HOL) "code_include"} adds arbitrary named content + (``include'') to generated code. A ``@{text "-"}'' as last argument + will remove an already added ``include''. + + \item @{command (HOL) "code_modulename"} declares aliasings from one + module name onto another. + + \end{description} + + The other framework generates code from both functional and relational programs to SML. See \cite{isabelle-HOL} for further information (this actually covers the new-style theory format as well). @@ -1011,209 +1218,6 @@ ; \end{rail} - \medskip The other framework generates code from functional programs - (including overloading using type classes) to SML \cite{SML}, OCaml - \cite{OCaml} and Haskell \cite{haskell-revised-report}. - Conceptually, code generation is split up in three steps: - \emph{selection} of code theorems, \emph{translation} into an - abstract executable view and \emph{serialization} to a specific - \emph{target language}. See \cite{isabelle-codegen} for an - introduction on how to use it. - - \begin{matharray}{rcl} - @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{command_def (HOL) "code_datatype"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_const"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_type"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_class"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_instance"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_monad"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_reserved"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_include"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_modulename"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_abort"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{attribute_def (HOL) code} & : & @{text attribute} \\ - \end{matharray} - - \begin{rail} - 'export\_code' ( constexpr + ) \\ - ( ( 'in' target ( 'module\_name' string ) ? \\ - ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ? - ; - - 'code\_thms' ( constexpr + ) ? - ; - - 'code\_deps' ( constexpr + ) ? - ; - - const: term - ; - - constexpr: ( const | 'name.*' | '*' ) - ; - - typeconstructor: nameref - ; - - class: nameref - ; - - target: 'OCaml' | 'SML' | 'Haskell' - ; - - 'code\_datatype' const + - ; - - 'code\_const' (const + 'and') \\ - ( ( '(' target ( syntax ? + 'and' ) ')' ) + ) - ; - - 'code\_type' (typeconstructor + 'and') \\ - ( ( '(' target ( syntax ? + 'and' ) ')' ) + ) - ; - - 'code\_class' (class + 'and') \\ - ( ( '(' target \\ ( string ? + 'and' ) ')' ) + ) - ; - - 'code\_instance' (( typeconstructor '::' class ) + 'and') \\ - ( ( '(' target ( '-' ? + 'and' ) ')' ) + ) - ; - - 'code\_monad' const const target - ; - - 'code\_reserved' target ( string + ) - ; - - 'code\_include' target ( string ( string | '-') ) - ; - - 'code\_modulename' target ( ( string string ) + ) - ; - - 'code\_abort' ( const + ) - ; - - syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string - ; - - 'code' ( 'del' ) ? - ; - - 'code_unfold' ( 'del' ) ? - ; - - 'code_post' ( 'del' ) ? - ; - \end{rail} - - \begin{description} - - \item @{command (HOL) "export_code"} is the canonical interface for - generating and serializing code: for a given list of constants, code - is generated for the specified target languages. If no serialization - instruction is given, only abstract code is generated internally. - - Constants may be specified by giving them literally, referring to - all executable contants within a certain theory by giving @{text - "name.*"}, or referring to \emph{all} executable constants currently - available by giving @{text "*"}. - - By default, for each involved theory one corresponding name space - module is generated. Alternativly, a module name may be specified - after the @{keyword "module_name"} keyword; then \emph{all} code is - placed in this module. - - For \emph{SML} and \emph{OCaml}, the file specification refers to a - single file; for \emph{Haskell}, it refers to a whole directory, - where code is generated in multiple files reflecting the module - hierarchy. The file specification ``@{text "-"}'' denotes standard - output. For \emph{SML}, omitting the file specification compiles - code internally in the context of the current ML session. - - Serializers take an optional list of arguments in parentheses. For - \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits - explicit module signatures. - - For \emph{Haskell} a module name prefix may be given using the ``@{text - "root:"}'' argument; ``@{text string_classes}'' adds a ``@{verbatim - "deriving (Read, Show)"}'' clause to each appropriate datatype - declaration. - - \item @{command (HOL) "code_thms"} prints a list of theorems - representing the corresponding program containing all given - constants. - - \item @{command (HOL) "code_deps"} visualizes dependencies of - theorems representing the corresponding program containing all given - constants. - - \item @{command (HOL) "code_datatype"} specifies a constructor set - for a logical type. - - \item @{command (HOL) "code_const"} associates a list of constants - with target-specific serializations; omitting a serialization - deletes an existing serialization. - - \item @{command (HOL) "code_type"} associates a list of type - constructors with target-specific serializations; omitting a - serialization deletes an existing serialization. - - \item @{command (HOL) "code_class"} associates a list of classes - with target-specific class names; omitting a serialization deletes - an existing serialization. This applies only to \emph{Haskell}. - - \item @{command (HOL) "code_instance"} declares a list of type - constructor / class instance relations as ``already present'' for a - given target. Omitting a ``@{text "-"}'' deletes an existing - ``already present'' declaration. This applies only to - \emph{Haskell}. - - \item @{command (HOL) "code_monad"} provides an auxiliary mechanism - to generate monadic code for Haskell. - - \item @{command (HOL) "code_reserved"} declares a list of names as - reserved for a given target, preventing it to be shadowed by any - generated code. - - \item @{command (HOL) "code_include"} adds arbitrary named content - (``include'') to generated code. A ``@{text "-"}'' as last argument - will remove an already added ``include''. - - \item @{command (HOL) "code_modulename"} declares aliasings from one - module name onto another. - - \item @{command (HOL) "code_abort"} declares constants which are not - required to have a definition by means of code equations; if - needed these are implemented by program abort instead. - - \item @{attribute (HOL) code} explicitly selects (or with option - ``@{text "del"}'' deselects) a code equation for code - generation. Usually packages introducing code equations provide - a reasonable default setup for selection. - - \item @{attribute (HOL) code_inline} declares (or with - option ``@{text "del"}'' removes) inlining theorems which are - applied as rewrite rules to any code equation during - preprocessing. - - \item @{attribute (HOL) code_post} declares (or with - option ``@{text "del"}'' removes) theorems which are - applied as rewrite rules to any result of an evaluation. - - \item @{command (HOL) "print_codesetup"} gives an overview on - selected code equations and code generator datatypes. - - \item @{command (HOL) "print_codeproc"} prints the setup - of the code generator preprocessor. - - \end{description} *} diff -r 4656ef45fedf -r a2a89563bfcb doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Jun 14 21:49:25 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Jun 15 07:42:48 2010 +0200 @@ -981,7 +981,211 @@ instantiates these mechanisms in a way that is amenable to end-user applications. - One framework generates code from both functional and relational + \medskip One framework generates code from functional programs + (including overloading using type classes) to SML \cite{SML}, OCaml + \cite{OCaml} and Haskell \cite{haskell-revised-report}. + Conceptually, code generation is split up in three steps: + \emph{selection} of code theorems, \emph{translation} into an + abstract executable view and \emph{serialization} to a specific + \emph{target language}. Inductive specifications can be executed + using the predicate compiler which operates within HOL. + See \cite{isabelle-codegen} for an introduction. + + \begin{matharray}{rcl} + \indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export-code}{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ + \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\ + \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ + \indexdef{HOL}{attribute}{code\_inline}\hypertarget{attribute.HOL.code-inline}{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}}} & : & \isa{attribute} \\ + \indexdef{HOL}{attribute}{code\_post}\hypertarget{attribute.HOL.code-post}{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}}} & : & \isa{attribute} \\ + \indexdef{HOL}{command}{print\_codeproc}\hypertarget{command.HOL.print-codeproc}{\hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ + \indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code-thms}{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ + \indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code-deps}{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ + \indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.code-const}{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.code-type}{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.code-class}{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.code-instance}{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code-reserved}{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \end{matharray} + + \begin{rail} + 'export\_code' ( constexpr + ) \\ + ( ( 'in' target ( 'module\_name' string ) ? \\ + ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ? + ; + + const: term + ; + + constexpr: ( const | 'name.*' | '*' ) + ; + + typeconstructor: nameref + ; + + class: nameref + ; + + target: 'OCaml' | 'SML' | 'Haskell' + ; + + 'code' ( 'del' ) ? + ; + + 'code\_abort' ( const + ) + ; + + 'code\_datatype' ( const + ) + ; + + 'code_inline' ( 'del' ) ? + ; + + 'code_post' ( 'del' ) ? + ; + + 'code\_thms' ( constexpr + ) ? + ; + + 'code\_deps' ( constexpr + ) ? + ; + + 'code\_const' (const + 'and') \\ + ( ( '(' target ( syntax ? + 'and' ) ')' ) + ) + ; + + 'code\_type' (typeconstructor + 'and') \\ + ( ( '(' target ( syntax ? + 'and' ) ')' ) + ) + ; + + 'code\_class' (class + 'and') \\ + ( ( '(' target \\ ( string ? + 'and' ) ')' ) + ) + ; + + 'code\_instance' (( typeconstructor '::' class ) + 'and') \\ + ( ( '(' target ( '-' ? + 'and' ) ')' ) + ) + ; + + 'code\_reserved' target ( string + ) + ; + + 'code\_monad' const const target + ; + + 'code\_include' target ( string ( string | '-') ) + ; + + 'code\_modulename' target ( ( string string ) + ) + ; + + syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string + ; + + \end{rail} + + \begin{description} + + \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} generates code for a given list + of constants in the specified target language(s). If no serialization + instruction is given, only abstract code is generated internally. + + Constants may be specified by giving them literally, referring to + all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently + available by giving \isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}. + + By default, for each involved theory one corresponding name space + module is generated. Alternativly, a module name may be specified + after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is + placed in this module. + + For \emph{SML} and \emph{OCaml}, the file specification refers to a + single file; for \emph{Haskell}, it refers to a whole directory, + where code is generated in multiple files reflecting the module + hierarchy. The file specification ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' denotes standard + output. For \emph{SML}, omitting the file specification compiles + code internally in the context of the current ML session. + + Serializers take an optional list of arguments in parentheses. For + \emph{SML} and \emph{OCaml}, ``\isa{no{\isacharunderscore}signatures}`` omits + explicit module signatures. + + For \emph{Haskell} a module name prefix may be given using the ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verb|deriving (Read, Show)|'' clause to each appropriate datatype + declaration. + + \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option + ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code + generation. Usually packages introducing code equations provide + a reasonable default setup for selection. + + \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not + required to have a definition by means of code equations; if + needed these are implemented by program abort instead. + + \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}} specifies a constructor set + for a logical type. + + \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on + selected code equations and code generator datatypes. + + \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with + option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are + applied as rewrite rules to any code equation during + preprocessing. + + \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with + option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are + applied as rewrite rules to any result of an evaluation. + + \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup + of the code generator preprocessor. + + \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} prints a list of theorems + representing the corresponding program containing all given + constants after preprocessing. + + \item \hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} visualizes dependencies of + theorems representing the corresponding program containing all given + constants after preprocessing. + + \item \hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} associates a list of constants + with target-specific serializations; omitting a serialization + deletes an existing serialization. + + \item \hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} associates a list of type + constructors with target-specific serializations; omitting a + serialization deletes an existing serialization. + + \item \hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}} associates a list of classes + with target-specific class names; omitting a serialization deletes + an existing serialization. This applies only to \emph{Haskell}. + + \item \hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}} declares a list of type + constructor / class instance relations as ``already present'' for a + given target. Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing + ``already present'' declaration. This applies only to + \emph{Haskell}. + + \item \hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} declares a list of names as + reserved for a given target, preventing it to be shadowed by any + generated code. + + \item \hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}} provides an auxiliary mechanism + to generate monadic code for Haskell. + + \item \hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} adds arbitrary named content + (``include'') to generated code. A ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' as last argument + will remove an already added ``include''. + + \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}} declares aliasings from one + module name onto another. + + \end{description} + + The other framework generates code from both functional and relational programs to SML. See \cite{isabelle-HOL} for further information (this actually covers the new-style theory format as well). @@ -1025,208 +1229,7 @@ 'code' (name)? ; - \end{rail} - - \medskip The other framework generates code from functional programs - (including overloading using type classes) to SML \cite{SML}, OCaml - \cite{OCaml} and Haskell \cite{haskell-revised-report}. - Conceptually, code generation is split up in three steps: - \emph{selection} of code theorems, \emph{translation} into an - abstract executable view and \emph{serialization} to a specific - \emph{target language}. See \cite{isabelle-codegen} for an - introduction on how to use it. - - \begin{matharray}{rcl} - \indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export-code}{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ - \indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code-thms}{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ - \indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code-deps}{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ - \indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ - \indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.code-const}{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ - \indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.code-type}{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ - \indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.code-class}{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ - \indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.code-instance}{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ - \indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ - \indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code-reserved}{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ - \indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ - \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ - \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ - \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ - \indexdef{HOL}{command}{print\_codeproc}\hypertarget{command.HOL.print-codeproc}{\hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ - \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\ - \end{matharray} - - \begin{rail} - 'export\_code' ( constexpr + ) \\ - ( ( 'in' target ( 'module\_name' string ) ? \\ - ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ? - ; - - 'code\_thms' ( constexpr + ) ? - ; - - 'code\_deps' ( constexpr + ) ? - ; - - const: term - ; - - constexpr: ( const | 'name.*' | '*' ) - ; - - typeconstructor: nameref - ; - - class: nameref - ; - - target: 'OCaml' | 'SML' | 'Haskell' - ; - - 'code\_datatype' const + - ; - - 'code\_const' (const + 'and') \\ - ( ( '(' target ( syntax ? + 'and' ) ')' ) + ) - ; - - 'code\_type' (typeconstructor + 'and') \\ - ( ( '(' target ( syntax ? + 'and' ) ')' ) + ) - ; - - 'code\_class' (class + 'and') \\ - ( ( '(' target \\ ( string ? + 'and' ) ')' ) + ) - ; - - 'code\_instance' (( typeconstructor '::' class ) + 'and') \\ - ( ( '(' target ( '-' ? + 'and' ) ')' ) + ) - ; - - 'code\_monad' const const target - ; - - 'code\_reserved' target ( string + ) - ; - - 'code\_include' target ( string ( string | '-') ) - ; - - 'code\_modulename' target ( ( string string ) + ) - ; - - 'code\_abort' ( const + ) - ; - - syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string - ; - - 'code' ( 'del' ) ? - ; - - 'code_unfold' ( 'del' ) ? - ; - - 'code_post' ( 'del' ) ? - ; - \end{rail} - - \begin{description} - - \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} is the canonical interface for - generating and serializing code: for a given list of constants, code - is generated for the specified target languages. If no serialization - instruction is given, only abstract code is generated internally. - - Constants may be specified by giving them literally, referring to - all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently - available by giving \isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}. - - By default, for each involved theory one corresponding name space - module is generated. Alternativly, a module name may be specified - after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is - placed in this module. - - For \emph{SML} and \emph{OCaml}, the file specification refers to a - single file; for \emph{Haskell}, it refers to a whole directory, - where code is generated in multiple files reflecting the module - hierarchy. The file specification ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' denotes standard - output. For \emph{SML}, omitting the file specification compiles - code internally in the context of the current ML session. - - Serializers take an optional list of arguments in parentheses. For - \emph{SML} and \emph{OCaml}, ``\isa{no{\isacharunderscore}signatures}`` omits - explicit module signatures. - - For \emph{Haskell} a module name prefix may be given using the ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verb|deriving (Read, Show)|'' clause to each appropriate datatype - declaration. - - \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} prints a list of theorems - representing the corresponding program containing all given - constants. - - \item \hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} visualizes dependencies of - theorems representing the corresponding program containing all given - constants. - - \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}} specifies a constructor set - for a logical type. - - \item \hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} associates a list of constants - with target-specific serializations; omitting a serialization - deletes an existing serialization. - - \item \hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} associates a list of type - constructors with target-specific serializations; omitting a - serialization deletes an existing serialization. - - \item \hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}} associates a list of classes - with target-specific class names; omitting a serialization deletes - an existing serialization. This applies only to \emph{Haskell}. - - \item \hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}} declares a list of type - constructor / class instance relations as ``already present'' for a - given target. Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing - ``already present'' declaration. This applies only to - \emph{Haskell}. - - \item \hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}} provides an auxiliary mechanism - to generate monadic code for Haskell. - - \item \hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} declares a list of names as - reserved for a given target, preventing it to be shadowed by any - generated code. - - \item \hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} adds arbitrary named content - (``include'') to generated code. A ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' as last argument - will remove an already added ``include''. - - \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}} declares aliasings from one - module name onto another. - - \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not - required to have a definition by means of code equations; if - needed these are implemented by program abort instead. - - \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option - ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code - generation. Usually packages introducing code equations provide - a reasonable default setup for selection. - - \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with - option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are - applied as rewrite rules to any code equation during - preprocessing. - - \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with - option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are - applied as rewrite rules to any result of an evaluation. - - \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on - selected code equations and code generator datatypes. - - \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup - of the code generator preprocessor. - - \end{description}% + \end{rail}% \end{isamarkuptext}% \isamarkuptrue% % diff -r 4656ef45fedf -r a2a89563bfcb doc-src/manual.bib --- a/doc-src/manual.bib Mon Jun 14 21:49:25 2010 +0200 +++ b/doc-src/manual.bib Tue Jun 15 07:42:48 2010 +0200 @@ -130,6 +130,13 @@ @book{Baader-Nipkow,author={Franz Baader and Tobias Nipkow}, title="Term Rewriting and All That",publisher=CUP,year=1998} +@manual{isabelle-locale, + author = {Clemens Ballarin}, + title = {Tutorial to Locales and Locale Interpretation}, + institution = TUM, + note = {\url{http://isabelle.in.tum.de/doc/locales.pdf}} +} + @InCollection{Barendregt-Geuvers:2001, author = {H. Barendregt and H. Geuvers}, title = {Proof Assistants using Dependent Type Systems}, @@ -508,15 +515,15 @@ year = {2007} } -@TechReport{Haftmann-Nipkow:2007:codegen, - author = {Florian Haftmann and Tobias Nipkow}, - title = {A Code Generator Framework for {Isabelle/HOL}}, - editor = {Klaus Schneider and Jens Brandt}, - booktitle = {Theorem Proving in Higher Order Logics: Emerging Trends Proceedings}, - month = {08}, - year = {2007}, - institution = {Department of Computer Science, University of Kaiserslautern}, - number = {364/07} +@inproceedings{Haftmann-Nipkow:2010:code, + author = {Florian Haftmann and Tobias Nipkow}, + title = {Code Generation via Higher-Order Rewrite Systems}, + booktitle = {Functional and Logic Programming: 10th International Symposium: FLOPS 2010}, + year = 2010, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + editor = {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal}, + volume = {6009} } @InProceedings{Haftmann-Wenzel:2009, diff -r 4656ef45fedf -r a2a89563bfcb src/HOL/HOL.thy --- a/src/HOL/HOL.thy Mon Jun 14 21:49:25 2010 +0200 +++ b/src/HOL/HOL.thy Tue Jun 15 07:42:48 2010 +0200 @@ -1800,8 +1800,8 @@ setup {* Code_Preproc.map_pre (fn simpset => simpset addsimprocs [Simplifier.simproc_i @{theory} "eq" [@{term "op ="}] - (fn thy => fn _ => fn t as Const (_, T) => case strip_type T - of ((T as Type _) :: _, _) => SOME @{thm equals_eq} + (fn thy => fn _ => fn Const (_, T) => case strip_type T + of (Type _ :: _, _) => SOME @{thm equals_eq} | _ => NONE)]) *} diff -r 4656ef45fedf -r a2a89563bfcb src/HOL/List.thy --- a/src/HOL/List.thy Mon Jun 14 21:49:25 2010 +0200 +++ b/src/HOL/List.thy Tue Jun 15 07:42:48 2010 +0200 @@ -4929,4 +4929,40 @@ "list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)" by(simp add: all_from_to_int_iff_ball list_ex_iff) + +subsubsection {* Use convenient predefined operations *} + +code_const "op @" + (SML infixr 7 "@") + (OCaml infixr 6 "@") + (Haskell infixr 5 "++") + (Scala infixl 7 "++") + +code_const map + (Haskell "map") + +code_const filter + (Haskell "filter") + +code_const concat + (Haskell "concat") + +code_const rev + (Haskell "rev") + +code_const zip + (Haskell "zip") + +code_const takeWhile + (Haskell "takeWhile") + +code_const dropWhile + (Haskell "dropWhile") + +code_const hd + (Haskell "head") + +code_const last + (Haskell "last") + end diff -r 4656ef45fedf -r a2a89563bfcb src/HOL/Nat.thy --- a/src/HOL/Nat.thy Mon Jun 14 21:49:25 2010 +0200 +++ b/src/HOL/Nat.thy Tue Jun 15 07:42:48 2010 +0200 @@ -1203,9 +1203,9 @@ lemmas [code_unfold] = funpow_code_def [symmetric] lemma [code]: + "funpow (Suc n) f = f o funpow n f" "funpow 0 f = id" - "funpow (Suc n) f = f o funpow n f" - unfolding funpow_code_def by simp_all + by (simp_all add: funpow_code_def) hide_const (open) funpow @@ -1213,6 +1213,11 @@ "f ^^ (m + n) = f ^^ m \ f ^^ n" by (induct m) simp_all +lemma funpow_mult: + fixes f :: "'a \ 'a" + shows "(f ^^ m) ^^ n = f ^^ (m * n)" + by (induct n) (simp_all add: funpow_add) + lemma funpow_swap1: "f ((f ^^ n) x) = (f ^^ n) (f x)" proof - diff -r 4656ef45fedf -r a2a89563bfcb src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Jun 14 21:49:25 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Jun 15 07:42:48 2010 +0200 @@ -105,12 +105,14 @@ in (thm', lthy') end; fun tac thms = Class.intro_classes_tac [] THEN ALLGOALS (ProofContext.fact_tac thms); + fun prefix dtco = Binding.qualify true (Long_Name.base_name dtco) o Binding.qualify true "eq" o Binding.name; fun add_eq_thms dtco = Theory.checkpoint #> `(fn thy => mk_eq_eqns thy dtco) - #-> (fn (thms, thm) => - Code.add_nbe_eqn thm - #> fold_rev Code.add_eqn thms); + #-> (fn (thms, thm) => PureThy.note_thmss Thm.lemmaK + [((prefix dtco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]), + ((prefix dtco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])]) + #> snd in thy |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq]) diff -r 4656ef45fedf -r a2a89563bfcb src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Mon Jun 14 21:49:25 2010 +0200 +++ b/src/Pure/Isar/code.ML Tue Jun 15 07:42:48 2010 +0200 @@ -59,6 +59,9 @@ val add_default_eqn: thm -> theory -> theory val add_default_eqn_attribute: attribute val add_default_eqn_attrib: Attrib.src + val add_nbe_default_eqn: thm -> theory -> theory + val add_nbe_default_eqn_attribute: attribute + val add_nbe_default_eqn_attrib: Attrib.src val del_eqn: thm -> theory -> theory val del_eqns: string -> theory -> theory val add_case: thm -> theory -> theory @@ -1066,18 +1069,25 @@ of SOME eqn => gen_add_eqn false eqn thy | NONE => thy; +fun add_nbe_eqn thm thy = + gen_add_eqn false (mk_eqn thy (thm, false)) thy; + fun add_default_eqn thm thy = case mk_eqn_liberal thy thm of SOME eqn => gen_add_eqn true eqn thy | NONE => thy; -fun add_nbe_eqn thm thy = - gen_add_eqn false (mk_eqn thy (thm, false)) thy; - val add_default_eqn_attribute = Thm.declaration_attribute (fn thm => Context.mapping (add_default_eqn thm) I); val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute); +fun add_nbe_default_eqn thm thy = + gen_add_eqn true (mk_eqn thy (thm, false)) thy; + +val add_nbe_default_eqn_attribute = Thm.declaration_attribute + (fn thm => Context.mapping (add_nbe_default_eqn thm) I); +val add_nbe_default_eqn_attrib = Attrib.internal (K add_nbe_default_eqn_attribute); + fun add_abs_eqn raw_thm thy = let val (abs_thm, tyco) = (apfst Thm.close_derivation o mk_abs_eqn thy) raw_thm; diff -r 4656ef45fedf -r a2a89563bfcb src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Mon Jun 14 21:49:25 2010 +0200 +++ b/src/Tools/Code/code_thingol.ML Tue Jun 15 07:42:48 2010 +0200 @@ -278,7 +278,7 @@ fun namify_class thy = namify thy Long_Name.base_name thyname_of_class; fun namify_classrel thy = namify thy (fn (sub_class, super_class) => - Long_Name.base_name sub_class ^ "_" ^ Long_Name.base_name super_class) + Long_Name.base_name super_class ^ "_" ^ Long_Name.base_name sub_class) (fn thy => thyname_of_class thy o fst); (*order fits nicely with composed projections*) fun namify_tyco thy "fun" = "Pure.fun"