1.1 --- a/Admin/isatest/isatest-makedist Sat Nov 27 22:01:27 2010 +0100
1.2 +++ b/Admin/isatest/isatest-makedist Sat Nov 27 22:01:45 2010 +0100
1.3 @@ -80,7 +80,9 @@
1.4 fi
1.5
1.6 cd $DISTPREFIX >> $DISTLOG 2>&1
1.7 -$TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
1.8 +ISABELLE_DIST=`cat $DISTPREFIX/ISABELLE_DIST`
1.9 +$TAR xvzf $ISABELLE_DIST >> $DISTLOG 2>&1
1.10 +ln -sf $(basename $ISABELLE_DIST .tar.gz) Isabelle
1.11
1.12 ssh atbroy102 "rm -rf /home/isatest/isadist && mkdir -p /home/isatest/isadist" && \
1.13 rsync -a "$HOME/isadist/." atbroy102:/home/isatest/isadist/.
2.1 --- a/Admin/isatest/settings/at-sml Sat Nov 27 22:01:27 2010 +0100
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,28 +0,0 @@
2.4 -# -*- shell-script -*- :mode=shellscript:
2.5 -
2.6 -# Standard ML of New Jersey 110 or later
2.7 -ML_SYSTEM=smlnj-110.0.7
2.8 -ML_HOME="/home/smlnj/110.0.7/bin"
2.9 -ML_OPTIONS="@SMLdebug=/dev/null"
2.10 -ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
2.11 -
2.12 -ISABELLE_HOME_USER=~/isabelle-at-sml
2.13 -
2.14 -# Where to look for isabelle tools (multiple dirs separated by ':').
2.15 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
2.16 -
2.17 -# Location for temporary files (should be on a local file system).
2.18 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
2.19 -
2.20 -
2.21 -# Heap input locations. ML system identifier is included in lookup.
2.22 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
2.23 -
2.24 -# Heap output location. ML system identifier is appended automatically later on.
2.25 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
2.26 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
2.27 -
2.28 -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
2.29 -
2.30 -unset KODKODI
2.31 -
3.1 --- a/Admin/isatest/settings/at-sml-dev-p Sat Nov 27 22:01:27 2010 +0100
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,28 +0,0 @@
3.4 -# -*- shell-script -*- :mode=shellscript:
3.5 -
3.6 -# Standard ML of New Jersey 110 or later
3.7 -ML_SYSTEM=smlnj
3.8 -ML_HOME="/home/smlnj/110.60/bin"
3.9 -ML_OPTIONS="@SMLdebug=/dev/null"
3.10 -ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
3.11 -
3.12 -ISABELLE_HOME_USER="$HOME/isabelle-at-sml-dev" # /tmp/isatest/isabelle-at-sml-dev
3.13 -
3.14 -# Where to look for isabelle tools (multiple dirs separated by ':').
3.15 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
3.16 -
3.17 -# Location for temporary files (should be on a local file system).
3.18 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
3.19 -
3.20 -
3.21 -# Heap input locations. ML system identifier is included in lookup.
3.22 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
3.23 -
3.24 -# Heap output location. ML system identifier is appended automatically later on.
3.25 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
3.26 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
3.27 -
3.28 -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
3.29 -
3.30 -unset KODKODI
3.31 -
4.1 --- a/Admin/isatest/settings/at64-poly-5.1-para Sat Nov 27 22:01:27 2010 +0100
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,28 +0,0 @@
4.4 -# -*- shell-script -*- :mode=shellscript:
4.5 -
4.6 - POLYML_HOME="/home/polyml/polyml-5.3.0"
4.7 - ML_SYSTEM="polyml-5.3.0"
4.8 - ML_PLATFORM="x86_64-linux"
4.9 - ML_HOME="$POLYML_HOME/$ML_PLATFORM"
4.10 - ML_OPTIONS="-H 1000"
4.11 -
4.12 -ISABELLE_HOME_USER=~/isabelle-at64-poly-para-e
4.13 -
4.14 -# Where to look for isabelle tools (multiple dirs separated by ':').
4.15 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
4.16 -
4.17 -# Location for temporary files (should be on a local file system).
4.18 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
4.19 -
4.20 -
4.21 -# Heap input locations. ML system identifier is included in lookup.
4.22 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
4.23 -
4.24 -# Heap output location. ML system identifier is appended automatically later on.
4.25 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
4.26 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
4.27 -
4.28 -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 2"
4.29 -
4.30 -unset KODKODI
4.31 -
5.1 --- a/Admin/isatest/settings/at64-sml-dev Sat Nov 27 22:01:27 2010 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,28 +0,0 @@
5.4 -# -*- shell-script -*- :mode=shellscript:
5.5 -
5.6 -# Standard ML of New Jersey 110 or later
5.7 -ML_SYSTEM=smlnj
5.8 -ML_HOME="/home/smlnj/110.60/bin"
5.9 -ML_OPTIONS="@SMLdebug=/dev/null"
5.10 -ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
5.11 -
5.12 -ISABELLE_HOME_USER=~/isabelle-at64-sml-dev
5.13 -
5.14 -# Where to look for isabelle tools (multiple dirs separated by ':').
5.15 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
5.16 -
5.17 -# Location for temporary files (should be on a local file system).
5.18 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
5.19 -
5.20 -
5.21 -# Heap input locations. ML system identifier is included in lookup.
5.22 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
5.23 -
5.24 -# Heap output location. ML system identifier is appended automatically later on.
5.25 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
5.26 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
5.27 -
5.28 -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
5.29 -
5.30 -unset KODKODI
5.31 -
6.1 --- a/Admin/isatest/settings/mac-sml-dev Sat Nov 27 22:01:27 2010 +0100
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,28 +0,0 @@
6.4 -# -*- shell-script -*- :mode=shellscript:
6.5 -
6.6 -# Standard ML of New Jersey 110 or later
6.7 -ML_SYSTEM=smlnj
6.8 -ML_HOME="/home/proj/smlnj/110.60/bin"
6.9 -ML_OPTIONS="@SMLdebug=/dev/null"
6.10 -ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
6.11 -
6.12 -ISABELLE_HOME_USER="$HOME/isabelle-mac-sml-dev"
6.13 -
6.14 -# Where to look for isabelle tools (multiple dirs separated by ':').
6.15 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
6.16 -
6.17 -# Location for temporary files (should be on a local file system).
6.18 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
6.19 -
6.20 -
6.21 -# Heap input locations. ML system identifier is included in lookup.
6.22 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
6.23 -
6.24 -# Heap output location. ML system identifier is appended automatically later on.
6.25 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
6.26 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
6.27 -
6.28 -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
6.29 -
6.30 -unset KODKODI
6.31 -
7.1 --- a/doc-src/Codegen/Thy/Evaluation.thy Sat Nov 27 22:01:27 2010 +0100
7.2 +++ b/doc-src/Codegen/Thy/Evaluation.thy Sat Nov 27 22:01:45 2010 +0100
7.3 @@ -2,7 +2,7 @@
7.4 imports Setup
7.5 begin
7.6
7.7 -section {* Evaluation *}
7.8 +section {* Evaluation \label{sec:evaluation} *}
7.9
7.10 text {*
7.11 Recalling \secref{sec:principle}, code generation turns a system of
8.1 --- a/doc-src/Codegen/Thy/Further.thy Sat Nov 27 22:01:27 2010 +0100
8.2 +++ b/doc-src/Codegen/Thy/Further.thy Sat Nov 27 22:01:45 2010 +0100
8.3 @@ -7,20 +7,20 @@
8.4 subsection {* Modules namespace *}
8.5
8.6 text {*
8.7 - When invoking the @{command export_code} command it is possible to leave
8.8 - out the @{keyword "module_name"} part; then code is distributed over
8.9 - different modules, where the module name space roughly is induced
8.10 - by the Isabelle theory name space.
8.11 + When invoking the @{command export_code} command it is possible to
8.12 + leave out the @{keyword "module_name"} part; then code is
8.13 + distributed over different modules, where the module name space
8.14 + roughly is induced by the Isabelle theory name space.
8.15
8.16 - Then sometimes the awkward situation occurs that dependencies between
8.17 - definitions introduce cyclic dependencies between modules, which in the
8.18 - @{text Haskell} world leaves you to the mercy of the @{text Haskell} implementation
8.19 - you are using, while for @{text SML}/@{text OCaml} code generation is not possible.
8.20 + Then sometimes the awkward situation occurs that dependencies
8.21 + between definitions introduce cyclic dependencies between modules,
8.22 + which in the @{text Haskell} world leaves you to the mercy of the
8.23 + @{text Haskell} implementation you are using, while for @{text
8.24 + SML}/@{text OCaml} code generation is not possible.
8.25
8.26 - A solution is to declare module names explicitly.
8.27 - Let use assume the three cyclically dependent
8.28 - modules are named \emph{A}, \emph{B} and \emph{C}.
8.29 - Then, by stating
8.30 + A solution is to declare module names explicitly. Let use assume
8.31 + the three cyclically dependent modules are named \emph{A}, \emph{B}
8.32 + and \emph{C}. Then, by stating
8.33 *}
8.34
8.35 code_modulename %quote SML
8.36 @@ -28,10 +28,10 @@
8.37 B ABC
8.38 C ABC
8.39
8.40 -text {*\noindent
8.41 - we explicitly map all those modules on \emph{ABC},
8.42 - resulting in an ad-hoc merge of this three modules
8.43 - at serialisation time.
8.44 +text {*
8.45 + \noindent we explicitly map all those modules on \emph{ABC},
8.46 + resulting in an ad-hoc merge of this three modules at serialisation
8.47 + time.
8.48 *}
8.49
8.50 subsection {* Locales and interpretation *}
8.51 @@ -40,8 +40,8 @@
8.52 A technical issue comes to surface when generating code from
8.53 specifications stemming from locale interpretation.
8.54
8.55 - Let us assume a locale specifying a power operation
8.56 - on arbitrary types:
8.57 + Let us assume a locale specifying a power operation on arbitrary
8.58 + types:
8.59 *}
8.60
8.61 locale %quote power =
8.62 @@ -50,8 +50,8 @@
8.63 begin
8.64
8.65 text {*
8.66 - \noindent Inside that locale we can lift @{text power} to exponent lists
8.67 - by means of specification relative to that locale:
8.68 + \noindent Inside that locale we can lift @{text power} to exponent
8.69 + lists by means of specification relative to that locale:
8.70 *}
8.71
8.72 primrec %quote powers :: "'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
8.73 @@ -76,26 +76,27 @@
8.74
8.75 text {*
8.76 After an interpretation of this locale (say, @{command_def
8.77 - interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f ::
8.78 - 'a \<Rightarrow> 'a). f ^^ n)"}), one would expect to have a constant @{text
8.79 + interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f
8.80 + :: 'a \<Rightarrow> 'a). f ^^ n)"}), one would expect to have a constant @{text
8.81 "fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"} for which code
8.82 can be generated. But this not the case: internally, the term
8.83 @{text "fun_power.powers"} is an abbreviation for the foundational
8.84 term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"}
8.85 (see \cite{isabelle-locale} for the details behind).
8.86
8.87 - Fortunately, with minor effort the desired behaviour can be achieved.
8.88 - First, a dedicated definition of the constant on which the local @{text "powers"}
8.89 - after interpretation is supposed to be mapped on:
8.90 + Fortunately, with minor effort the desired behaviour can be
8.91 + achieved. First, a dedicated definition of the constant on which
8.92 + the local @{text "powers"} after interpretation is supposed to be
8.93 + mapped on:
8.94 *}
8.95
8.96 definition %quote funpows :: "nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
8.97 [code del]: "funpows = power.powers (\<lambda>n f. f ^^ n)"
8.98
8.99 text {*
8.100 - \noindent In general, the pattern is @{text "c = t"} where @{text c} is
8.101 - the name of the future constant and @{text t} the foundational term
8.102 - corresponding to the local constant after interpretation.
8.103 + \noindent In general, the pattern is @{text "c = t"} where @{text c}
8.104 + is the name of the future constant and @{text t} the foundational
8.105 + term corresponding to the local constant after interpretation.
8.106
8.107 The interpretation itself is enriched with an equation @{text "t = c"}:
8.108 *}
8.109 @@ -106,8 +107,8 @@
8.110 (simp_all add: fun_eq_iff funpow_mult mult_commute funpows_def)
8.111
8.112 text {*
8.113 - \noindent This additional equation is trivially proved by the definition
8.114 - itself.
8.115 + \noindent This additional equation is trivially proved by the
8.116 + definition itself.
8.117
8.118 After this setup procedure, code generation can continue as usual:
8.119 *}
8.120 @@ -124,8 +125,8 @@
8.121 specific application, you should consider \emph{Imperative
8.122 Functional Programming with Isabelle/HOL}
8.123 \cite{bulwahn-et-al:2008:imperative}; the framework described there
8.124 - is available in session @{text Imperative_HOL}, together with a short
8.125 - primer document.
8.126 + is available in session @{text Imperative_HOL}, together with a
8.127 + short primer document.
8.128 *}
8.129
8.130
8.131 @@ -153,7 +154,7 @@
8.132 @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
8.133 @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
8.134 @{index_ML Code.get_type: "theory -> string
8.135 - -> (string * sort) list * ((string * string list) * typ list) list"} \\
8.136 + -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool"} \\
8.137 @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"}
8.138 \end{mldecls}
8.139
8.140 @@ -198,22 +199,19 @@
8.141 subsubsection {* Data depending on the theory's executable content *}
8.142
8.143 text {*
8.144 - Implementing code generator applications on top
8.145 - of the framework set out so far usually not only
8.146 - involves using those primitive interfaces
8.147 - but also storing code-dependent data and various
8.148 - other things.
8.149 + Implementing code generator applications on top of the framework set
8.150 + out so far usually not only involves using those primitive
8.151 + interfaces but also storing code-dependent data and various other
8.152 + things.
8.153
8.154 - Due to incrementality of code generation, changes in the
8.155 - theory's executable content have to be propagated in a
8.156 - certain fashion. Additionally, such changes may occur
8.157 - not only during theory extension but also during theory
8.158 - merge, which is a little bit nasty from an implementation
8.159 - point of view. The framework provides a solution
8.160 - to this technical challenge by providing a functorial
8.161 - data slot @{ML_functor Code_Data}; on instantiation
8.162 - of this functor, the following types and operations
8.163 - are required:
8.164 + Due to incrementality of code generation, changes in the theory's
8.165 + executable content have to be propagated in a certain fashion.
8.166 + Additionally, such changes may occur not only during theory
8.167 + extension but also during theory merge, which is a little bit nasty
8.168 + from an implementation point of view. The framework provides a
8.169 + solution to this technical challenge by providing a functorial data
8.170 + slot @{ML_functor Code_Data}; on instantiation of this functor, the
8.171 + following types and operations are required:
8.172
8.173 \medskip
8.174 \begin{tabular}{l}
8.175 @@ -229,8 +227,8 @@
8.176
8.177 \end{description}
8.178
8.179 - \noindent An instance of @{ML_functor Code_Data} provides the following
8.180 - interface:
8.181 + \noindent An instance of @{ML_functor Code_Data} provides the
8.182 + following interface:
8.183
8.184 \medskip
8.185 \begin{tabular}{l}
8.186 @@ -240,8 +238,8 @@
8.187
8.188 \begin{description}
8.189
8.190 - \item @{text change} update of current data (cached!)
8.191 - by giving a continuation.
8.192 + \item @{text change} update of current data (cached!) by giving a
8.193 + continuation.
8.194
8.195 \item @{text change_yield} update with side result.
8.196
9.1 --- a/doc-src/Codegen/Thy/Introduction.thy Sat Nov 27 22:01:27 2010 +0100
9.2 +++ b/doc-src/Codegen/Thy/Introduction.thy Sat Nov 27 22:01:45 2010 +0100
9.3 @@ -214,6 +214,10 @@
9.4 \item Inductive predicates can be turned executable using an
9.5 extension of the code generator \secref{sec:inductive}.
9.6
9.7 + \item If you want to utilize code generation to obtain fast
9.8 + evaluators e.g.~for decision procedures, have a look at
9.9 + \secref{sec:evaluation}.
9.10 +
9.11 \item You may want to skim over the more technical sections
9.12 \secref{sec:adaptation} and \secref{sec:further}.
9.13
10.1 --- a/doc-src/Codegen/Thy/Refinement.thy Sat Nov 27 22:01:27 2010 +0100
10.2 +++ b/doc-src/Codegen/Thy/Refinement.thy Sat Nov 27 22:01:45 2010 +0100
10.3 @@ -131,34 +131,40 @@
10.4
10.5 lemma %quote empty_AQueue [code]:
10.6 "empty = AQueue [] []"
10.7 - unfolding AQueue_def empty_def by simp
10.8 + by (simp add: AQueue_def empty_def)
10.9
10.10 lemma %quote enqueue_AQueue [code]:
10.11 "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
10.12 - unfolding AQueue_def by simp
10.13 + by (simp add: AQueue_def)
10.14
10.15 lemma %quote dequeue_AQueue [code]:
10.16 "dequeue (AQueue xs []) =
10.17 (if xs = [] then (None, AQueue [] [])
10.18 else dequeue (AQueue [] (rev xs)))"
10.19 "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
10.20 - unfolding AQueue_def by simp_all
10.21 + by (simp_all add: AQueue_def)
10.22
10.23 text {*
10.24 - \noindent For completeness, we provide a substitute for the
10.25 - @{text case} combinator on queues:
10.26 + \noindent It is good style, although no absolute requirement, to
10.27 + provide code equations for the original artefacts of the implemented
10.28 + type, if possible; in our case, these are the datatype constructor
10.29 + @{const Queue} and the case combinator @{const queue_case}:
10.30 *}
10.31
10.32 +lemma %quote Queue_AQueue [code]:
10.33 + "Queue = AQueue []"
10.34 + by (simp add: AQueue_def fun_eq_iff)
10.35 +
10.36 lemma %quote queue_case_AQueue [code]:
10.37 "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
10.38 - unfolding AQueue_def by simp
10.39 + by (simp add: AQueue_def)
10.40
10.41 text {*
10.42 \noindent The resulting code looks as expected:
10.43 *}
10.44
10.45 text %quotetypewriter {*
10.46 - @{code_stmts empty enqueue dequeue (SML)}
10.47 + @{code_stmts empty enqueue dequeue Queue queue_case (SML)}
10.48 *}
10.49
10.50 text {*
10.51 @@ -260,7 +266,7 @@
10.52 text {*
10.53 Typical data structures implemented by representations involving
10.54 invariants are available in the library, e.g.~theories @{theory
10.55 - Fset} and @{theory Mapping} specify sets (type @{typ "'a fset"}) and
10.56 + Cset} and @{theory Mapping} specify sets (type @{typ "'a Cset.set"}) and
10.57 key-value-mappings (type @{typ "('a, 'b) mapping"}) respectively;
10.58 these can be implemented by distinct lists as presented here as
10.59 example (theory @{theory Dlist}) and red-black-trees respectively
11.1 --- a/doc-src/Codegen/Thy/document/Evaluation.tex Sat Nov 27 22:01:27 2010 +0100
11.2 +++ b/doc-src/Codegen/Thy/document/Evaluation.tex Sat Nov 27 22:01:45 2010 +0100
11.3 @@ -18,7 +18,7 @@
11.4 %
11.5 \endisadelimtheory
11.6 %
11.7 -\isamarkupsection{Evaluation%
11.8 +\isamarkupsection{Evaluation \label{sec:evaluation}%
11.9 }
11.10 \isamarkuptrue%
11.11 %
12.1 --- a/doc-src/Codegen/Thy/document/Further.tex Sat Nov 27 22:01:27 2010 +0100
12.2 +++ b/doc-src/Codegen/Thy/document/Further.tex Sat Nov 27 22:01:45 2010 +0100
12.3 @@ -27,20 +27,19 @@
12.4 \isamarkuptrue%
12.5 %
12.6 \begin{isamarkuptext}%
12.7 -When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}} command it is possible to leave
12.8 - out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}}}} part; then code is distributed over
12.9 - different modules, where the module name space roughly is induced
12.10 - by the Isabelle theory name space.
12.11 +When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}} command it is possible to
12.12 + leave out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}}}} part; then code is
12.13 + distributed over different modules, where the module name space
12.14 + roughly is induced by the Isabelle theory name space.
12.15
12.16 - Then sometimes the awkward situation occurs that dependencies between
12.17 - definitions introduce cyclic dependencies between modules, which in the
12.18 - \isa{Haskell} world leaves you to the mercy of the \isa{Haskell} implementation
12.19 - you are using, while for \isa{SML}/\isa{OCaml} code generation is not possible.
12.20 + Then sometimes the awkward situation occurs that dependencies
12.21 + between definitions introduce cyclic dependencies between modules,
12.22 + which in the \isa{Haskell} world leaves you to the mercy of the
12.23 + \isa{Haskell} implementation you are using, while for \isa{SML}/\isa{OCaml} code generation is not possible.
12.24
12.25 - A solution is to declare module names explicitly.
12.26 - Let use assume the three cyclically dependent
12.27 - modules are named \emph{A}, \emph{B} and \emph{C}.
12.28 - Then, by stating%
12.29 + A solution is to declare module names explicitly. Let use assume
12.30 + the three cyclically dependent modules are named \emph{A}, \emph{B}
12.31 + and \emph{C}. Then, by stating%
12.32 \end{isamarkuptext}%
12.33 \isamarkuptrue%
12.34 %
12.35 @@ -62,10 +61,9 @@
12.36 \endisadelimquote
12.37 %
12.38 \begin{isamarkuptext}%
12.39 -\noindent
12.40 - we explicitly map all those modules on \emph{ABC},
12.41 - resulting in an ad-hoc merge of this three modules
12.42 - at serialisation time.%
12.43 +\noindent we explicitly map all those modules on \emph{ABC},
12.44 + resulting in an ad-hoc merge of this three modules at serialisation
12.45 + time.%
12.46 \end{isamarkuptext}%
12.47 \isamarkuptrue%
12.48 %
12.49 @@ -77,8 +75,8 @@
12.50 A technical issue comes to surface when generating code from
12.51 specifications stemming from locale interpretation.
12.52
12.53 - Let us assume a locale specifying a power operation
12.54 - on arbitrary types:%
12.55 + Let us assume a locale specifying a power operation on arbitrary
12.56 + types:%
12.57 \end{isamarkuptext}%
12.58 \isamarkuptrue%
12.59 %
12.60 @@ -100,8 +98,8 @@
12.61 \endisadelimquote
12.62 %
12.63 \begin{isamarkuptext}%
12.64 -\noindent Inside that locale we can lift \isa{power} to exponent lists
12.65 - by means of specification relative to that locale:%
12.66 +\noindent Inside that locale we can lift \isa{power} to exponent
12.67 + lists by means of specification relative to that locale:%
12.68 \end{isamarkuptext}%
12.69 \isamarkuptrue%
12.70 %
12.71 @@ -151,9 +149,10 @@
12.72 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}}}
12.73 (see \cite{isabelle-locale} for the details behind).
12.74
12.75 - Fortunately, with minor effort the desired behaviour can be achieved.
12.76 - First, a dedicated definition of the constant on which the local \isa{powers}
12.77 - after interpretation is supposed to be mapped on:%
12.78 + Fortunately, with minor effort the desired behaviour can be
12.79 + achieved. First, a dedicated definition of the constant on which
12.80 + the local \isa{powers} after interpretation is supposed to be
12.81 + mapped on:%
12.82 \end{isamarkuptext}%
12.83 \isamarkuptrue%
12.84 %
12.85 @@ -173,9 +172,9 @@
12.86 \endisadelimquote
12.87 %
12.88 \begin{isamarkuptext}%
12.89 -\noindent In general, the pattern is \isa{c\ {\isaliteral{3D}{\isacharequal}}\ t} where \isa{c} is
12.90 - the name of the future constant and \isa{t} the foundational term
12.91 - corresponding to the local constant after interpretation.
12.92 +\noindent In general, the pattern is \isa{c\ {\isaliteral{3D}{\isacharequal}}\ t} where \isa{c}
12.93 + is the name of the future constant and \isa{t} the foundational
12.94 + term corresponding to the local constant after interpretation.
12.95
12.96 The interpretation itself is enriched with an equation \isa{t\ {\isaliteral{3D}{\isacharequal}}\ c}:%
12.97 \end{isamarkuptext}%
12.98 @@ -200,8 +199,8 @@
12.99 \endisadelimquote
12.100 %
12.101 \begin{isamarkuptext}%
12.102 -\noindent This additional equation is trivially proved by the definition
12.103 - itself.
12.104 +\noindent This additional equation is trivially proved by the
12.105 + definition itself.
12.106
12.107 After this setup procedure, code generation can continue as usual:%
12.108 \end{isamarkuptext}%
12.109 @@ -240,8 +239,8 @@
12.110 specific application, you should consider \emph{Imperative
12.111 Functional Programming with Isabelle/HOL}
12.112 \cite{bulwahn-et-al:2008:imperative}; the framework described there
12.113 - is available in session \isa{Imperative{\isaliteral{5F}{\isacharunderscore}}HOL}, together with a short
12.114 - primer document.%
12.115 + is available in session \isa{Imperative{\isaliteral{5F}{\isacharunderscore}}HOL}, together with a
12.116 + short primer document.%
12.117 \end{isamarkuptext}%
12.118 \isamarkuptrue%
12.119 %
12.120 @@ -280,7 +279,7 @@
12.121 \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
12.122 \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
12.123 \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
12.124 -\verb| -> (string * sort) list * ((string * string list) * typ list) list| \\
12.125 +\verb| -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool| \\
12.126 \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option|
12.127 \end{mldecls}
12.128
12.129 @@ -334,22 +333,19 @@
12.130 \isamarkuptrue%
12.131 %
12.132 \begin{isamarkuptext}%
12.133 -Implementing code generator applications on top
12.134 - of the framework set out so far usually not only
12.135 - involves using those primitive interfaces
12.136 - but also storing code-dependent data and various
12.137 - other things.
12.138 +Implementing code generator applications on top of the framework set
12.139 + out so far usually not only involves using those primitive
12.140 + interfaces but also storing code-dependent data and various other
12.141 + things.
12.142
12.143 - Due to incrementality of code generation, changes in the
12.144 - theory's executable content have to be propagated in a
12.145 - certain fashion. Additionally, such changes may occur
12.146 - not only during theory extension but also during theory
12.147 - merge, which is a little bit nasty from an implementation
12.148 - point of view. The framework provides a solution
12.149 - to this technical challenge by providing a functorial
12.150 - data slot \verb|Code_Data|; on instantiation
12.151 - of this functor, the following types and operations
12.152 - are required:
12.153 + Due to incrementality of code generation, changes in the theory's
12.154 + executable content have to be propagated in a certain fashion.
12.155 + Additionally, such changes may occur not only during theory
12.156 + extension but also during theory merge, which is a little bit nasty
12.157 + from an implementation point of view. The framework provides a
12.158 + solution to this technical challenge by providing a functorial data
12.159 + slot \verb|Code_Data|; on instantiation of this functor, the
12.160 + following types and operations are required:
12.161
12.162 \medskip
12.163 \begin{tabular}{l}
12.164 @@ -365,8 +361,8 @@
12.165
12.166 \end{description}
12.167
12.168 - \noindent An instance of \verb|Code_Data| provides the following
12.169 - interface:
12.170 + \noindent An instance of \verb|Code_Data| provides the
12.171 + following interface:
12.172
12.173 \medskip
12.174 \begin{tabular}{l}
12.175 @@ -376,8 +372,8 @@
12.176
12.177 \begin{description}
12.178
12.179 - \item \isa{change} update of current data (cached!)
12.180 - by giving a continuation.
12.181 + \item \isa{change} update of current data (cached!) by giving a
12.182 + continuation.
12.183
12.184 \item \isa{change{\isaliteral{5F}{\isacharunderscore}}yield} update with side result.
12.185
13.1 --- a/doc-src/Codegen/Thy/document/Introduction.tex Sat Nov 27 22:01:27 2010 +0100
13.2 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Sat Nov 27 22:01:45 2010 +0100
13.3 @@ -539,6 +539,10 @@
13.4 \item Inductive predicates can be turned executable using an
13.5 extension of the code generator \secref{sec:inductive}.
13.6
13.7 + \item If you want to utilize code generation to obtain fast
13.8 + evaluators e.g.~for decision procedures, have a look at
13.9 + \secref{sec:evaluation}.
13.10 +
13.11 \item You may want to skim over the more technical sections
13.12 \secref{sec:adaptation} and \secref{sec:further}.
13.13
14.1 --- a/doc-src/Codegen/Thy/document/Refinement.tex Sat Nov 27 22:01:27 2010 +0100
14.2 +++ b/doc-src/Codegen/Thy/document/Refinement.tex Sat Nov 27 22:01:45 2010 +0100
14.3 @@ -281,16 +281,14 @@
14.4 \isacommand{lemma}\isamarkupfalse%
14.5 \ empty{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
14.6 \ \ {\isaliteral{22}{\isachardoublequoteopen}}empty\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
14.7 -\ \ \isacommand{unfolding}\isamarkupfalse%
14.8 -\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ empty{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
14.9 -\ simp\isanewline
14.10 +\ \ \isacommand{by}\isamarkupfalse%
14.11 +\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ empty{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
14.12 \isanewline
14.13 \isacommand{lemma}\isamarkupfalse%
14.14 \ enqueue{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
14.15 \ \ {\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
14.16 -\ \ \isacommand{unfolding}\isamarkupfalse%
14.17 -\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
14.18 -\ simp\isanewline
14.19 +\ \ \isacommand{by}\isamarkupfalse%
14.20 +\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ AQueue{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
14.21 \isanewline
14.22 \isacommand{lemma}\isamarkupfalse%
14.23 \ dequeue{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
14.24 @@ -298,9 +296,8 @@
14.25 \ \ \ \ {\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
14.26 \ \ \ \ 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
14.27 \ \ {\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
14.28 -\ \ \isacommand{unfolding}\isamarkupfalse%
14.29 -\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
14.30 -\ simp{\isaliteral{5F}{\isacharunderscore}}all%
14.31 +\ \ \isacommand{by}\isamarkupfalse%
14.32 +\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ AQueue{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
14.33 \endisatagquote
14.34 {\isafoldquote}%
14.35 %
14.36 @@ -309,8 +306,10 @@
14.37 \endisadelimquote
14.38 %
14.39 \begin{isamarkuptext}%
14.40 -\noindent For completeness, we provide a substitute for the
14.41 - \isa{case} combinator on queues:%
14.42 +\noindent It is good style, although no absolute requirement, to
14.43 + provide code equations for the original artefacts of the implemented
14.44 + type, if possible; in our case, these are the datatype constructor
14.45 + \isa{Queue} and the case combinator \isa{queue{\isaliteral{5F}{\isacharunderscore}}case}:%
14.46 \end{isamarkuptext}%
14.47 \isamarkuptrue%
14.48 %
14.49 @@ -320,11 +319,16 @@
14.50 %
14.51 \isatagquote
14.52 \isacommand{lemma}\isamarkupfalse%
14.53 +\ Queue{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
14.54 +\ \ {\isaliteral{22}{\isachardoublequoteopen}}Queue\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
14.55 +\ \ \isacommand{by}\isamarkupfalse%
14.56 +\ {\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
14.57 +\isanewline
14.58 +\isacommand{lemma}\isamarkupfalse%
14.59 \ queue{\isaliteral{5F}{\isacharunderscore}}case{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
14.60 \ \ {\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
14.61 -\ \ \isacommand{unfolding}\isamarkupfalse%
14.62 -\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
14.63 -\ simp%
14.64 +\ \ \isacommand{by}\isamarkupfalse%
14.65 +\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ AQueue{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
14.66 \endisatagquote
14.67 {\isafoldquote}%
14.68 %
14.69 @@ -351,8 +355,10 @@
14.70 \ \ val\ null\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ bool\isanewline
14.71 \ \ 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
14.72 \ \ val\ empty\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ queue\isanewline
14.73 +\ \ val\ queue\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ queue\isanewline
14.74 \ \ 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
14.75 \ \ 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
14.76 +\ \ 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
14.77 end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline
14.78 \isanewline
14.79 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
14.80 @@ -369,6 +375,8 @@
14.81 \isanewline
14.82 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
14.83 \isanewline
14.84 +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
14.85 +\isanewline
14.86 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
14.87 \ \ {\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
14.88 \ \ \ \ {\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
14.89 @@ -376,6 +384,8 @@
14.90 \isanewline
14.91 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
14.92 \isanewline
14.93 +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
14.94 +\isanewline
14.95 end{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}struct\ Example{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline%
14.96 \end{isamarkuptext}%
14.97 \isamarkuptrue%
14.98 @@ -618,7 +628,7 @@
14.99 %
14.100 \begin{isamarkuptext}%
14.101 Typical data structures implemented by representations involving
14.102 - 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
14.103 + 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
14.104 key-value-mappings (type \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ mapping}) respectively;
14.105 these can be implemented by distinct lists as presented here as
14.106 example (theory \hyperlink{theory.Dlist}{\mbox{\isa{Dlist}}}) and red-black-trees respectively