--- 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/.
--- 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
-
--- 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
-
--- 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
-
--- 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
-
--- 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
-
--- 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
--- 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 \<Rightarrow> 'b \<Rightarrow> 'b" where
@@ -76,26 +76,27 @@
text {*
After an interpretation of this locale (say, @{command_def
- interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f ::
- 'a \<Rightarrow> 'a). f ^^ n)"}), one would expect to have a constant @{text
+ interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f
+ :: 'a \<Rightarrow> 'a). f ^^ n)"}), one would expect to have a constant @{text
"fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> '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 (\<lambda>n (f :: 'a \<Rightarrow> '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 \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
[code del]: "funpows = power.powers (\<lambda>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.
--- 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}.
--- 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
--- 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%
%
--- 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.
--- 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}.
--- 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