# HG changeset patch # User haftmann # Date 1290891705 -3600 # Node ID 4dd4901a724289b09ad730b61d0ccfc52f0847f0 # Parent 1a8875eacacdf528b1087b9be2afe7a5bacfdbf3# Parent c0bfead42774a2613e522c0ac672f24f4d4fa282 merged diff -r 1a8875eacacd -r 4dd4901a7242 Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Sat Nov 27 22:01:27 2010 +0100 +++ b/Admin/isatest/isatest-makedist Sat Nov 27 22:01:45 2010 +0100 @@ -80,7 +80,9 @@ fi cd $DISTPREFIX >> $DISTLOG 2>&1 -$TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1 +ISABELLE_DIST=`cat $DISTPREFIX/ISABELLE_DIST` +$TAR xvzf $ISABELLE_DIST >> $DISTLOG 2>&1 +ln -sf $(basename $ISABELLE_DIST .tar.gz) Isabelle ssh atbroy102 "rm -rf /home/isatest/isadist && mkdir -p /home/isatest/isadist" && \ rsync -a "$HOME/isadist/." atbroy102:/home/isatest/isadist/. diff -r 1a8875eacacd -r 4dd4901a7242 Admin/isatest/settings/at-sml --- a/Admin/isatest/settings/at-sml Sat Nov 27 22:01:27 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -# -*- shell-script -*- :mode=shellscript: - -# Standard ML of New Jersey 110 or later -ML_SYSTEM=smlnj-110.0.7 -ML_HOME="/home/smlnj/110.0.7/bin" -ML_OPTIONS="@SMLdebug=/dev/null" -ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") - -ISABELLE_HOME_USER=~/isabelle-at-sml - -# Where to look for isabelle tools (multiple dirs separated by ':'). -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" - -# Location for temporary files (should be on a local file system). -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" - - -# Heap input locations. ML system identifier is included in lookup. -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" - -# Heap output location. ML system identifier is appended automatically later on. -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" - -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true" - -unset KODKODI - diff -r 1a8875eacacd -r 4dd4901a7242 Admin/isatest/settings/at-sml-dev-p --- a/Admin/isatest/settings/at-sml-dev-p Sat Nov 27 22:01:27 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -# -*- shell-script -*- :mode=shellscript: - -# Standard ML of New Jersey 110 or later -ML_SYSTEM=smlnj -ML_HOME="/home/smlnj/110.60/bin" -ML_OPTIONS="@SMLdebug=/dev/null" -ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") - -ISABELLE_HOME_USER="$HOME/isabelle-at-sml-dev" # /tmp/isatest/isabelle-at-sml-dev - -# Where to look for isabelle tools (multiple dirs separated by ':'). -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" - -# Location for temporary files (should be on a local file system). -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" - - -# Heap input locations. ML system identifier is included in lookup. -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" - -# Heap output location. ML system identifier is appended automatically later on. -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" - -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true" - -unset KODKODI - diff -r 1a8875eacacd -r 4dd4901a7242 Admin/isatest/settings/at64-poly-5.1-para --- a/Admin/isatest/settings/at64-poly-5.1-para Sat Nov 27 22:01:27 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -# -*- shell-script -*- :mode=shellscript: - - POLYML_HOME="/home/polyml/polyml-5.3.0" - ML_SYSTEM="polyml-5.3.0" - ML_PLATFORM="x86_64-linux" - ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="-H 1000" - -ISABELLE_HOME_USER=~/isabelle-at64-poly-para-e - -# Where to look for isabelle tools (multiple dirs separated by ':'). -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" - -# Location for temporary files (should be on a local file system). -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" - - -# Heap input locations. ML system identifier is included in lookup. -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" - -# Heap output location. ML system identifier is appended automatically later on. -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" - -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 2" - -unset KODKODI - diff -r 1a8875eacacd -r 4dd4901a7242 Admin/isatest/settings/at64-sml-dev --- a/Admin/isatest/settings/at64-sml-dev Sat Nov 27 22:01:27 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -# -*- shell-script -*- :mode=shellscript: - -# Standard ML of New Jersey 110 or later -ML_SYSTEM=smlnj -ML_HOME="/home/smlnj/110.60/bin" -ML_OPTIONS="@SMLdebug=/dev/null" -ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") - -ISABELLE_HOME_USER=~/isabelle-at64-sml-dev - -# Where to look for isabelle tools (multiple dirs separated by ':'). -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" - -# Location for temporary files (should be on a local file system). -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" - - -# Heap input locations. ML system identifier is included in lookup. -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" - -# Heap output location. ML system identifier is appended automatically later on. -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" - -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true" - -unset KODKODI - diff -r 1a8875eacacd -r 4dd4901a7242 Admin/isatest/settings/mac-sml-dev --- a/Admin/isatest/settings/mac-sml-dev Sat Nov 27 22:01:27 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -# -*- shell-script -*- :mode=shellscript: - -# Standard ML of New Jersey 110 or later -ML_SYSTEM=smlnj -ML_HOME="/home/proj/smlnj/110.60/bin" -ML_OPTIONS="@SMLdebug=/dev/null" -ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") - -ISABELLE_HOME_USER="$HOME/isabelle-mac-sml-dev" - -# Where to look for isabelle tools (multiple dirs separated by ':'). -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" - -# Location for temporary files (should be on a local file system). -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" - - -# Heap input locations. ML system identifier is included in lookup. -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" - -# Heap output location. ML system identifier is appended automatically later on. -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" - -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true" - -unset KODKODI - diff -r 1a8875eacacd -r 4dd4901a7242 doc-src/Codegen/Thy/Evaluation.thy --- a/doc-src/Codegen/Thy/Evaluation.thy Sat Nov 27 22:01:27 2010 +0100 +++ b/doc-src/Codegen/Thy/Evaluation.thy Sat Nov 27 22:01:45 2010 +0100 @@ -2,7 +2,7 @@ imports Setup begin -section {* Evaluation *} +section {* Evaluation \label{sec:evaluation} *} text {* Recalling \secref{sec:principle}, code generation turns a system of diff -r 1a8875eacacd -r 4dd4901a7242 doc-src/Codegen/Thy/Further.thy --- a/doc-src/Codegen/Thy/Further.thy Sat Nov 27 22:01:27 2010 +0100 +++ b/doc-src/Codegen/Thy/Further.thy Sat Nov 27 22:01:45 2010 +0100 @@ -7,20 +7,20 @@ subsection {* Modules namespace *} text {* - When invoking the @{command export_code} command it is possible to leave - out the @{keyword "module_name"} part; then code is distributed over - different modules, where the module name space roughly is induced - by the Isabelle theory name space. + When invoking the @{command export_code} command it is possible to + leave out the @{keyword "module_name"} part; then code is + distributed over different modules, where the module name space + roughly is induced by the Isabelle theory name space. - Then sometimes the awkward situation occurs that dependencies between - definitions introduce cyclic dependencies between modules, which in the - @{text Haskell} world leaves you to the mercy of the @{text Haskell} implementation - you are using, while for @{text SML}/@{text OCaml} code generation is not possible. + Then sometimes the awkward situation occurs that dependencies + between definitions introduce cyclic dependencies between modules, + which in the @{text Haskell} world leaves you to the mercy of the + @{text Haskell} implementation you are using, while for @{text + SML}/@{text 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 + 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 *} code_modulename %quote SML @@ -28,10 +28,10 @@ B ABC C ABC -text {*\noindent - we explicitly map all those modules on \emph{ABC}, - resulting in an ad-hoc merge of this three modules - at serialisation time. +text {* + \noindent we explicitly map all those modules on \emph{ABC}, + resulting in an ad-hoc merge of this three modules at serialisation + time. *} subsection {* Locales and interpretation *} @@ -40,8 +40,8 @@ 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: + Let us assume a locale specifying a power operation on arbitrary + types: *} locale %quote power = @@ -50,8 +50,8 @@ begin text {* - \noindent Inside that locale we can lift @{text power} to exponent lists - by means of specification relative to that locale: + \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 @@ -76,26 +76,27 @@ text {* After an interpretation of this locale (say, @{command_def - interpretation} @{text "fun_power:"} @{term [source] "power (\n (f :: - 'a \ 'a). f ^^ n)"}), one would expect to have a constant @{text + 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). - Fortunately, 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: + Fortunately, 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. + \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"}: *} @@ -106,8 +107,8 @@ (simp_all add: fun_eq_iff funpow_mult mult_commute funpows_def) text {* - \noindent This additional equation is trivially proved by the definition - itself. + \noindent This additional equation is trivially proved by the + definition itself. After this setup procedure, code generation can continue as usual: *} @@ -124,8 +125,8 @@ specific application, you should consider \emph{Imperative Functional Programming with Isabelle/HOL} \cite{bulwahn-et-al:2008:imperative}; the framework described there - is available in session @{text Imperative_HOL}, together with a short - primer document. + is available in session @{text Imperative_HOL}, together with a + short primer document. *} @@ -153,7 +154,7 @@ @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\ @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\ @{index_ML Code.get_type: "theory -> string - -> (string * sort) list * ((string * string list) * typ list) list"} \\ + -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool"} \\ @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"} \end{mldecls} @@ -198,22 +199,19 @@ subsubsection {* Data depending on the theory's executable content *} text {* - Implementing code generator applications on top - of the framework set out so far usually not only - involves using those primitive interfaces - but also storing code-dependent data and various - other things. + Implementing code generator applications on top of the framework set + out so far usually not only involves using those primitive + interfaces but also storing code-dependent data and various other + things. - Due to incrementality of code generation, changes in the - theory's executable content have to be propagated in a - certain fashion. Additionally, such changes may occur - not only during theory extension but also during theory - merge, which is a little bit nasty from an implementation - point of view. The framework provides a solution - to this technical challenge by providing a functorial - data slot @{ML_functor Code_Data}; on instantiation - of this functor, the following types and operations - are required: + Due to incrementality of code generation, changes in the theory's + executable content have to be propagated in a certain fashion. + Additionally, such changes may occur not only during theory + extension but also during theory merge, which is a little bit nasty + from an implementation point of view. The framework provides a + solution to this technical challenge by providing a functorial data + slot @{ML_functor Code_Data}; on instantiation of this functor, the + following types and operations are required: \medskip \begin{tabular}{l} @@ -229,8 +227,8 @@ \end{description} - \noindent An instance of @{ML_functor Code_Data} provides the following - interface: + \noindent An instance of @{ML_functor Code_Data} provides the + following interface: \medskip \begin{tabular}{l} @@ -240,8 +238,8 @@ \begin{description} - \item @{text change} update of current data (cached!) - by giving a continuation. + \item @{text change} update of current data (cached!) by giving a + continuation. \item @{text change_yield} update with side result. diff -r 1a8875eacacd -r 4dd4901a7242 doc-src/Codegen/Thy/Introduction.thy --- a/doc-src/Codegen/Thy/Introduction.thy Sat Nov 27 22:01:27 2010 +0100 +++ b/doc-src/Codegen/Thy/Introduction.thy Sat Nov 27 22:01:45 2010 +0100 @@ -214,6 +214,10 @@ \item Inductive predicates can be turned executable using an extension of the code generator \secref{sec:inductive}. + \item If you want to utilize code generation to obtain fast + evaluators e.g.~for decision procedures, have a look at + \secref{sec:evaluation}. + \item You may want to skim over the more technical sections \secref{sec:adaptation} and \secref{sec:further}. diff -r 1a8875eacacd -r 4dd4901a7242 doc-src/Codegen/Thy/Refinement.thy --- a/doc-src/Codegen/Thy/Refinement.thy Sat Nov 27 22:01:27 2010 +0100 +++ b/doc-src/Codegen/Thy/Refinement.thy Sat Nov 27 22:01:45 2010 +0100 @@ -131,34 +131,40 @@ lemma %quote empty_AQueue [code]: "empty = AQueue [] []" - unfolding AQueue_def empty_def by simp + by (simp add: AQueue_def empty_def) lemma %quote enqueue_AQueue [code]: "enqueue x (AQueue xs ys) = AQueue (x # xs) ys" - unfolding AQueue_def by simp + by (simp add: AQueue_def) lemma %quote dequeue_AQueue [code]: "dequeue (AQueue xs []) = (if xs = [] then (None, AQueue [] []) else dequeue (AQueue [] (rev xs)))" "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)" - unfolding AQueue_def by simp_all + by (simp_all add: AQueue_def) text {* - \noindent For completeness, we provide a substitute for the - @{text case} combinator on queues: + \noindent It is good style, although no absolute requirement, to + provide code equations for the original artefacts of the implemented + type, if possible; in our case, these are the datatype constructor + @{const Queue} and the case combinator @{const queue_case}: *} +lemma %quote Queue_AQueue [code]: + "Queue = AQueue []" + by (simp add: AQueue_def fun_eq_iff) + lemma %quote queue_case_AQueue [code]: "queue_case f (AQueue xs ys) = f (ys @ rev xs)" - unfolding AQueue_def by simp + by (simp add: AQueue_def) text {* \noindent The resulting code looks as expected: *} text %quotetypewriter {* - @{code_stmts empty enqueue dequeue (SML)} + @{code_stmts empty enqueue dequeue Queue queue_case (SML)} *} text {* @@ -260,7 +266,7 @@ text {* Typical data structures implemented by representations involving invariants are available in the library, e.g.~theories @{theory - Fset} and @{theory Mapping} specify sets (type @{typ "'a fset"}) and + Cset} and @{theory Mapping} specify sets (type @{typ "'a Cset.set"}) and key-value-mappings (type @{typ "('a, 'b) mapping"}) respectively; these can be implemented by distinct lists as presented here as example (theory @{theory Dlist}) and red-black-trees respectively diff -r 1a8875eacacd -r 4dd4901a7242 doc-src/Codegen/Thy/document/Evaluation.tex --- a/doc-src/Codegen/Thy/document/Evaluation.tex Sat Nov 27 22:01:27 2010 +0100 +++ b/doc-src/Codegen/Thy/document/Evaluation.tex Sat Nov 27 22:01:45 2010 +0100 @@ -18,7 +18,7 @@ % \endisadelimtheory % -\isamarkupsection{Evaluation% +\isamarkupsection{Evaluation \label{sec:evaluation}% } \isamarkuptrue% % diff -r 1a8875eacacd -r 4dd4901a7242 doc-src/Codegen/Thy/document/Further.tex --- a/doc-src/Codegen/Thy/document/Further.tex Sat Nov 27 22:01:27 2010 +0100 +++ b/doc-src/Codegen/Thy/document/Further.tex Sat Nov 27 22:01:45 2010 +0100 @@ -27,20 +27,19 @@ \isamarkuptrue% % \begin{isamarkuptext}% -When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}} command it is possible to leave - out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}}}} part; then code is distributed over - different modules, where the module name space roughly is induced - by the Isabelle theory name space. +When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}} command it is possible to + leave out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}}}} part; then code is + distributed over different modules, where the module name space + roughly is induced by the Isabelle theory name space. - 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. + 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% + 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% % @@ -62,10 +61,9 @@ \endisadelimquote % \begin{isamarkuptext}% -\noindent - we explicitly map all those modules on \emph{ABC}, - resulting in an ad-hoc merge of this three modules - at serialisation time.% +\noindent 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% % @@ -77,8 +75,8 @@ 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:% + Let us assume a locale specifying a power operation on arbitrary + types:% \end{isamarkuptext}% \isamarkuptrue% % @@ -100,8 +98,8 @@ \endisadelimquote % \begin{isamarkuptext}% -\noindent Inside that locale we can lift \isa{power} to exponent lists - by means of specification relative to that locale:% +\noindent Inside that locale we can lift \isa{power} to exponent + lists by means of specification relative to that locale:% \end{isamarkuptext}% \isamarkuptrue% % @@ -151,9 +149,10 @@ term \isa{{\isaliteral{22}{\isachardoublequote}}power{\isaliteral{2E}{\isachardot}}powers\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}n\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ f\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} (see \cite{isabelle-locale} for the details behind). - Fortunately, 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:% + Fortunately, 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% % @@ -173,9 +172,9 @@ \endisadelimquote % \begin{isamarkuptext}% -\noindent In general, the pattern is \isa{c\ {\isaliteral{3D}{\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. +\noindent In general, the pattern is \isa{c\ {\isaliteral{3D}{\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\ {\isaliteral{3D}{\isacharequal}}\ c}:% \end{isamarkuptext}% @@ -200,8 +199,8 @@ \endisadelimquote % \begin{isamarkuptext}% -\noindent This additional equation is trivially proved by the definition - itself. +\noindent This additional equation is trivially proved by the + definition itself. After this setup procedure, code generation can continue as usual:% \end{isamarkuptext}% @@ -240,8 +239,8 @@ specific application, you should consider \emph{Imperative Functional Programming with Isabelle/HOL} \cite{bulwahn-et-al:2008:imperative}; the framework described there - is available in session \isa{Imperative{\isaliteral{5F}{\isacharunderscore}}HOL}, together with a short - primer document.% + is available in session \isa{Imperative{\isaliteral{5F}{\isacharunderscore}}HOL}, together with a + short primer document.% \end{isamarkuptext}% \isamarkuptrue% % @@ -280,7 +279,7 @@ \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\ \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\ \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline% -\verb| -> (string * sort) list * ((string * string list) * typ list) list| \\ +\verb| -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool| \\ \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option| \end{mldecls} @@ -334,22 +333,19 @@ \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. +Implementing code generator applications on top of the framework set + out so far usually not only involves using those primitive + interfaces but also storing code-dependent data and various other + things. - Due to incrementality of code generation, changes in the - theory's executable content have to be propagated in a - certain fashion. Additionally, such changes may occur - not only during theory extension but also during theory - merge, which is a little bit nasty from an implementation - point of view. The framework provides a solution - to this technical challenge by providing a functorial - data slot \verb|Code_Data|; on instantiation - of this functor, the following types and operations - are required: + Due to incrementality of code generation, changes in the theory's + executable content have to be propagated in a certain fashion. + Additionally, such changes may occur not only during theory + extension but also during theory merge, which is a little bit nasty + from an implementation point of view. The framework provides a + solution to this technical challenge by providing a functorial data + slot \verb|Code_Data|; on instantiation of this functor, the + following types and operations are required: \medskip \begin{tabular}{l} @@ -365,8 +361,8 @@ \end{description} - \noindent An instance of \verb|Code_Data| provides the following - interface: + \noindent An instance of \verb|Code_Data| provides the + following interface: \medskip \begin{tabular}{l} @@ -376,8 +372,8 @@ \begin{description} - \item \isa{change} update of current data (cached!) - by giving a continuation. + \item \isa{change} update of current data (cached!) by giving a + continuation. \item \isa{change{\isaliteral{5F}{\isacharunderscore}}yield} update with side result. diff -r 1a8875eacacd -r 4dd4901a7242 doc-src/Codegen/Thy/document/Introduction.tex --- a/doc-src/Codegen/Thy/document/Introduction.tex Sat Nov 27 22:01:27 2010 +0100 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Sat Nov 27 22:01:45 2010 +0100 @@ -539,6 +539,10 @@ \item Inductive predicates can be turned executable using an extension of the code generator \secref{sec:inductive}. + \item If you want to utilize code generation to obtain fast + evaluators e.g.~for decision procedures, have a look at + \secref{sec:evaluation}. + \item You may want to skim over the more technical sections \secref{sec:adaptation} and \secref{sec:further}. diff -r 1a8875eacacd -r 4dd4901a7242 doc-src/Codegen/Thy/document/Refinement.tex --- a/doc-src/Codegen/Thy/document/Refinement.tex Sat Nov 27 22:01:27 2010 +0100 +++ b/doc-src/Codegen/Thy/document/Refinement.tex Sat Nov 27 22:01:45 2010 +0100 @@ -281,16 +281,14 @@ \isacommand{lemma}\isamarkupfalse% \ empty{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline \ \ {\isaliteral{22}{\isachardoublequoteopen}}empty\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{unfolding}\isamarkupfalse% -\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ empty{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ empty{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline \isanewline \isacommand{lemma}\isamarkupfalse% \ enqueue{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline \ \ {\isaliteral{22}{\isachardoublequoteopen}}enqueue\ x\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{unfolding}\isamarkupfalse% -\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ AQueue{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline \isanewline \isacommand{lemma}\isamarkupfalse% \ dequeue{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline @@ -298,9 +296,8 @@ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ then\ {\isaliteral{28}{\isacharparenleft}}None{\isaliteral{2C}{\isacharcomma}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline \ \ \ \ else\ dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline \ \ {\isaliteral{22}{\isachardoublequoteopen}}dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{23}{\isacharhash}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Some\ y{\isaliteral{2C}{\isacharcomma}}\ AQueue\ xs\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{unfolding}\isamarkupfalse% -\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% -\ simp{\isaliteral{5F}{\isacharunderscore}}all% +\ \ \isacommand{by}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ AQueue{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}% \endisatagquote {\isafoldquote}% % @@ -309,8 +306,10 @@ \endisadelimquote % \begin{isamarkuptext}% -\noindent For completeness, we provide a substitute for the - \isa{case} combinator on queues:% +\noindent It is good style, although no absolute requirement, to + provide code equations for the original artefacts of the implemented + type, if possible; in our case, these are the datatype constructor + \isa{Queue} and the case combinator \isa{queue{\isaliteral{5F}{\isacharunderscore}}case}:% \end{isamarkuptext}% \isamarkuptrue% % @@ -320,11 +319,16 @@ % \isatagquote \isacommand{lemma}\isamarkupfalse% +\ Queue{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline +\ \ {\isaliteral{22}{\isachardoublequoteopen}}Queue\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ fun{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}iff{\isaliteral{29}{\isacharparenright}}\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% \ queue{\isaliteral{5F}{\isacharunderscore}}case{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline \ \ {\isaliteral{22}{\isachardoublequoteopen}}queue{\isaliteral{5F}{\isacharunderscore}}case\ f\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{28}{\isacharparenleft}}ys\ {\isaliteral{40}{\isacharat}}\ rev\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{unfolding}\isamarkupfalse% -\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% -\ simp% +\ \ \isacommand{by}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ AQueue{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}% \endisatagquote {\isafoldquote}% % @@ -351,8 +355,10 @@ \ \ val\ null\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ bool\isanewline \ \ datatype\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ of\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}a\ list\isanewline \ \ val\ empty\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ queue\isanewline +\ \ val\ queue\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ queue\isanewline \ \ val\ dequeue\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}a\ queue\isanewline \ \ val\ enqueue\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ queue\isanewline +\ \ val\ queue{\isaliteral{5F}{\isacharunderscore}}case\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b\isanewline end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline \isanewline fun\ id\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}fn\ xa\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ xa{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{3B}{\isacharsemicolon}}\isanewline @@ -369,6 +375,8 @@ \isanewline val\ empty\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline \isanewline +fun\ queue\ x\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\isanewline fun\ dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}SOME\ y{\isaliteral{2C}{\isacharcomma}}\ AQueue\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline \ \ {\isaliteral{7C}{\isacharbar}}\ dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ null\ xs\ then\ {\isaliteral{28}{\isacharparenleft}}NONE{\isaliteral{2C}{\isacharcomma}}\ AQueue\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline @@ -376,6 +384,8 @@ \isanewline fun\ enqueue\ x\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline \isanewline +fun\ queue{\isaliteral{5F}{\isacharunderscore}}case\ f\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{28}{\isacharparenleft}}ys\ {\isaliteral{40}{\isacharat}}\ rev\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\isanewline end{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}struct\ Example{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline% \end{isamarkuptext}% \isamarkuptrue% @@ -618,7 +628,7 @@ % \begin{isamarkuptext}% Typical data structures implemented by representations involving - invariants are available in the library, e.g.~theories \hyperlink{theory.Fset}{\mbox{\isa{Fset}}} and \hyperlink{theory.Mapping}{\mbox{\isa{Mapping}}} specify sets (type \isa{{\isaliteral{27}{\isacharprime}}a\ fset}) and + invariants are available in the library, e.g.~theories \hyperlink{theory.Cset}{\mbox{\isa{Cset}}} and \hyperlink{theory.Mapping}{\mbox{\isa{Mapping}}} specify sets (type \isa{{\isaliteral{27}{\isacharprime}}a\ Cset{\isaliteral{2E}{\isachardot}}set}) and key-value-mappings (type \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ mapping}) respectively; these can be implemented by distinct lists as presented here as example (theory \hyperlink{theory.Dlist}{\mbox{\isa{Dlist}}}) and red-black-trees respectively