1.1 --- a/doc-src/Codegen/Thy/document/Evaluation.tex Sat Nov 27 18:51:04 2010 +0100
1.2 +++ b/doc-src/Codegen/Thy/document/Evaluation.tex Sat Nov 27 18:51:15 2010 +0100
1.3 @@ -18,7 +18,7 @@
1.4 %
1.5 \endisadelimtheory
1.6 %
1.7 -\isamarkupsection{Evaluation%
1.8 +\isamarkupsection{Evaluation \label{sec:evaluation}%
1.9 }
1.10 \isamarkuptrue%
1.11 %
2.1 --- a/doc-src/Codegen/Thy/document/Further.tex Sat Nov 27 18:51:04 2010 +0100
2.2 +++ b/doc-src/Codegen/Thy/document/Further.tex Sat Nov 27 18:51:15 2010 +0100
2.3 @@ -27,20 +27,19 @@
2.4 \isamarkuptrue%
2.5 %
2.6 \begin{isamarkuptext}%
2.7 -When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}} command it is possible to leave
2.8 - out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}}}} part; then code is distributed over
2.9 - different modules, where the module name space roughly is induced
2.10 - by the Isabelle theory name space.
2.11 +When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}} command it is possible to
2.12 + leave out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}}}} part; then code is
2.13 + distributed over different modules, where the module name space
2.14 + roughly is induced by the Isabelle theory name space.
2.15
2.16 - Then sometimes the awkward situation occurs that dependencies between
2.17 - definitions introduce cyclic dependencies between modules, which in the
2.18 - \isa{Haskell} world leaves you to the mercy of the \isa{Haskell} implementation
2.19 - you are using, while for \isa{SML}/\isa{OCaml} code generation is not possible.
2.20 + Then sometimes the awkward situation occurs that dependencies
2.21 + between definitions introduce cyclic dependencies between modules,
2.22 + which in the \isa{Haskell} world leaves you to the mercy of the
2.23 + \isa{Haskell} implementation you are using, while for \isa{SML}/\isa{OCaml} code generation is not possible.
2.24
2.25 - A solution is to declare module names explicitly.
2.26 - Let use assume the three cyclically dependent
2.27 - modules are named \emph{A}, \emph{B} and \emph{C}.
2.28 - Then, by stating%
2.29 + A solution is to declare module names explicitly. Let use assume
2.30 + the three cyclically dependent modules are named \emph{A}, \emph{B}
2.31 + and \emph{C}. Then, by stating%
2.32 \end{isamarkuptext}%
2.33 \isamarkuptrue%
2.34 %
2.35 @@ -62,10 +61,9 @@
2.36 \endisadelimquote
2.37 %
2.38 \begin{isamarkuptext}%
2.39 -\noindent
2.40 - we explicitly map all those modules on \emph{ABC},
2.41 - resulting in an ad-hoc merge of this three modules
2.42 - at serialisation time.%
2.43 +\noindent we explicitly map all those modules on \emph{ABC},
2.44 + resulting in an ad-hoc merge of this three modules at serialisation
2.45 + time.%
2.46 \end{isamarkuptext}%
2.47 \isamarkuptrue%
2.48 %
2.49 @@ -77,8 +75,8 @@
2.50 A technical issue comes to surface when generating code from
2.51 specifications stemming from locale interpretation.
2.52
2.53 - Let us assume a locale specifying a power operation
2.54 - on arbitrary types:%
2.55 + Let us assume a locale specifying a power operation on arbitrary
2.56 + types:%
2.57 \end{isamarkuptext}%
2.58 \isamarkuptrue%
2.59 %
2.60 @@ -100,8 +98,8 @@
2.61 \endisadelimquote
2.62 %
2.63 \begin{isamarkuptext}%
2.64 -\noindent Inside that locale we can lift \isa{power} to exponent lists
2.65 - by means of specification relative to that locale:%
2.66 +\noindent Inside that locale we can lift \isa{power} to exponent
2.67 + lists by means of specification relative to that locale:%
2.68 \end{isamarkuptext}%
2.69 \isamarkuptrue%
2.70 %
2.71 @@ -151,9 +149,10 @@
2.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}}}
2.73 (see \cite{isabelle-locale} for the details behind).
2.74
2.75 - Fortunately, with minor effort the desired behaviour can be achieved.
2.76 - First, a dedicated definition of the constant on which the local \isa{powers}
2.77 - after interpretation is supposed to be mapped on:%
2.78 + Fortunately, with minor effort the desired behaviour can be
2.79 + achieved. First, a dedicated definition of the constant on which
2.80 + the local \isa{powers} after interpretation is supposed to be
2.81 + mapped on:%
2.82 \end{isamarkuptext}%
2.83 \isamarkuptrue%
2.84 %
2.85 @@ -173,9 +172,9 @@
2.86 \endisadelimquote
2.87 %
2.88 \begin{isamarkuptext}%
2.89 -\noindent In general, the pattern is \isa{c\ {\isaliteral{3D}{\isacharequal}}\ t} where \isa{c} is
2.90 - the name of the future constant and \isa{t} the foundational term
2.91 - corresponding to the local constant after interpretation.
2.92 +\noindent In general, the pattern is \isa{c\ {\isaliteral{3D}{\isacharequal}}\ t} where \isa{c}
2.93 + is the name of the future constant and \isa{t} the foundational
2.94 + term corresponding to the local constant after interpretation.
2.95
2.96 The interpretation itself is enriched with an equation \isa{t\ {\isaliteral{3D}{\isacharequal}}\ c}:%
2.97 \end{isamarkuptext}%
2.98 @@ -200,8 +199,8 @@
2.99 \endisadelimquote
2.100 %
2.101 \begin{isamarkuptext}%
2.102 -\noindent This additional equation is trivially proved by the definition
2.103 - itself.
2.104 +\noindent This additional equation is trivially proved by the
2.105 + definition itself.
2.106
2.107 After this setup procedure, code generation can continue as usual:%
2.108 \end{isamarkuptext}%
2.109 @@ -240,8 +239,8 @@
2.110 specific application, you should consider \emph{Imperative
2.111 Functional Programming with Isabelle/HOL}
2.112 \cite{bulwahn-et-al:2008:imperative}; the framework described there
2.113 - is available in session \isa{Imperative{\isaliteral{5F}{\isacharunderscore}}HOL}, together with a short
2.114 - primer document.%
2.115 + is available in session \isa{Imperative{\isaliteral{5F}{\isacharunderscore}}HOL}, together with a
2.116 + short primer document.%
2.117 \end{isamarkuptext}%
2.118 \isamarkuptrue%
2.119 %
2.120 @@ -280,7 +279,7 @@
2.121 \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
2.122 \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
2.123 \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
2.124 -\verb| -> (string * sort) list * ((string * string list) * typ list) list| \\
2.125 +\verb| -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool| \\
2.126 \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option|
2.127 \end{mldecls}
2.128
2.129 @@ -334,22 +333,19 @@
2.130 \isamarkuptrue%
2.131 %
2.132 \begin{isamarkuptext}%
2.133 -Implementing code generator applications on top
2.134 - of the framework set out so far usually not only
2.135 - involves using those primitive interfaces
2.136 - but also storing code-dependent data and various
2.137 - other things.
2.138 +Implementing code generator applications on top of the framework set
2.139 + out so far usually not only involves using those primitive
2.140 + interfaces but also storing code-dependent data and various other
2.141 + things.
2.142
2.143 - Due to incrementality of code generation, changes in the
2.144 - theory's executable content have to be propagated in a
2.145 - certain fashion. Additionally, such changes may occur
2.146 - not only during theory extension but also during theory
2.147 - merge, which is a little bit nasty from an implementation
2.148 - point of view. The framework provides a solution
2.149 - to this technical challenge by providing a functorial
2.150 - data slot \verb|Code_Data|; on instantiation
2.151 - of this functor, the following types and operations
2.152 - are required:
2.153 + Due to incrementality of code generation, changes in the theory's
2.154 + executable content have to be propagated in a certain fashion.
2.155 + Additionally, such changes may occur not only during theory
2.156 + extension but also during theory merge, which is a little bit nasty
2.157 + from an implementation point of view. The framework provides a
2.158 + solution to this technical challenge by providing a functorial data
2.159 + slot \verb|Code_Data|; on instantiation of this functor, the
2.160 + following types and operations are required:
2.161
2.162 \medskip
2.163 \begin{tabular}{l}
2.164 @@ -365,8 +361,8 @@
2.165
2.166 \end{description}
2.167
2.168 - \noindent An instance of \verb|Code_Data| provides the following
2.169 - interface:
2.170 + \noindent An instance of \verb|Code_Data| provides the
2.171 + following interface:
2.172
2.173 \medskip
2.174 \begin{tabular}{l}
2.175 @@ -376,8 +372,8 @@
2.176
2.177 \begin{description}
2.178
2.179 - \item \isa{change} update of current data (cached!)
2.180 - by giving a continuation.
2.181 + \item \isa{change} update of current data (cached!) by giving a
2.182 + continuation.
2.183
2.184 \item \isa{change{\isaliteral{5F}{\isacharunderscore}}yield} update with side result.
2.185
3.1 --- a/doc-src/Codegen/Thy/document/Introduction.tex Sat Nov 27 18:51:04 2010 +0100
3.2 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Sat Nov 27 18:51:15 2010 +0100
3.3 @@ -539,6 +539,10 @@
3.4 \item Inductive predicates can be turned executable using an
3.5 extension of the code generator \secref{sec:inductive}.
3.6
3.7 + \item If you want to utilize code generation to obtain fast
3.8 + evaluators e.g.~for decision procedures, have a look at
3.9 + \secref{sec:evaluation}.
3.10 +
3.11 \item You may want to skim over the more technical sections
3.12 \secref{sec:adaptation} and \secref{sec:further}.
3.13
4.1 --- a/doc-src/Codegen/Thy/document/Refinement.tex Sat Nov 27 18:51:04 2010 +0100
4.2 +++ b/doc-src/Codegen/Thy/document/Refinement.tex Sat Nov 27 18:51:15 2010 +0100
4.3 @@ -281,16 +281,14 @@
4.4 \isacommand{lemma}\isamarkupfalse%
4.5 \ empty{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
4.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
4.7 -\ \ \isacommand{unfolding}\isamarkupfalse%
4.8 -\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ empty{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
4.9 -\ simp\isanewline
4.10 +\ \ \isacommand{by}\isamarkupfalse%
4.11 +\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ empty{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
4.12 \isanewline
4.13 \isacommand{lemma}\isamarkupfalse%
4.14 \ enqueue{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
4.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
4.16 -\ \ \isacommand{unfolding}\isamarkupfalse%
4.17 -\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
4.18 -\ simp\isanewline
4.19 +\ \ \isacommand{by}\isamarkupfalse%
4.20 +\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ AQueue{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
4.21 \isanewline
4.22 \isacommand{lemma}\isamarkupfalse%
4.23 \ dequeue{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
4.24 @@ -298,9 +296,8 @@
4.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
4.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
4.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
4.28 -\ \ \isacommand{unfolding}\isamarkupfalse%
4.29 -\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
4.30 -\ simp{\isaliteral{5F}{\isacharunderscore}}all%
4.31 +\ \ \isacommand{by}\isamarkupfalse%
4.32 +\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ AQueue{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
4.33 \endisatagquote
4.34 {\isafoldquote}%
4.35 %
4.36 @@ -309,8 +306,10 @@
4.37 \endisadelimquote
4.38 %
4.39 \begin{isamarkuptext}%
4.40 -\noindent For completeness, we provide a substitute for the
4.41 - \isa{case} combinator on queues:%
4.42 +\noindent It is good style, although no absolute requirement, to
4.43 + provide code equations for the original artefacts of the implemented
4.44 + type, if possible; in our case, these are the datatype constructor
4.45 + \isa{Queue} and the case combinator \isa{queue{\isaliteral{5F}{\isacharunderscore}}case}:%
4.46 \end{isamarkuptext}%
4.47 \isamarkuptrue%
4.48 %
4.49 @@ -320,11 +319,16 @@
4.50 %
4.51 \isatagquote
4.52 \isacommand{lemma}\isamarkupfalse%
4.53 +\ Queue{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
4.54 +\ \ {\isaliteral{22}{\isachardoublequoteopen}}Queue\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
4.55 +\ \ \isacommand{by}\isamarkupfalse%
4.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
4.57 +\isanewline
4.58 +\isacommand{lemma}\isamarkupfalse%
4.59 \ queue{\isaliteral{5F}{\isacharunderscore}}case{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
4.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
4.61 -\ \ \isacommand{unfolding}\isamarkupfalse%
4.62 -\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
4.63 -\ simp%
4.64 +\ \ \isacommand{by}\isamarkupfalse%
4.65 +\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ AQueue{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
4.66 \endisatagquote
4.67 {\isafoldquote}%
4.68 %
4.69 @@ -351,8 +355,10 @@
4.70 \ \ val\ null\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ bool\isanewline
4.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
4.72 \ \ val\ empty\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ queue\isanewline
4.73 +\ \ val\ queue\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ queue\isanewline
4.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
4.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
4.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
4.77 end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline
4.78 \isanewline
4.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
4.80 @@ -369,6 +375,8 @@
4.81 \isanewline
4.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
4.83 \isanewline
4.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
4.85 +\isanewline
4.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
4.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
4.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
4.89 @@ -376,6 +384,8 @@
4.90 \isanewline
4.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
4.92 \isanewline
4.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
4.94 +\isanewline
4.95 end{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}struct\ Example{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline%
4.96 \end{isamarkuptext}%
4.97 \isamarkuptrue%
4.98 @@ -618,7 +628,7 @@
4.99 %
4.100 \begin{isamarkuptext}%
4.101 Typical data structures implemented by representations involving
4.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
4.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
4.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;
4.105 these can be implemented by distinct lists as presented here as
4.106 example (theory \hyperlink{theory.Dlist}{\mbox{\isa{Dlist}}}) and red-black-trees respectively