author | haftmann |
Sat, 18 Feb 2012 20:13:38 +0100 | |
changeset 46523 | 7ca897381b26 |
parent 45211 | 3dd426ae6bea |
child 46563 | 0ad69b30b39c |
permissions | -rw-r--r-- |
28447 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Introduction}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
11 |
\ Introduction\isanewline |
|
12 |
\isakeyword{imports}\ Setup\isanewline |
|
13 |
\isakeyword{begin}% |
|
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
38405 | 21 |
\isamarkupsection{Introduction% |
22 |
} |
|
23 |
\isamarkuptrue% |
|
24 |
% |
|
38437 | 25 |
\begin{isamarkuptext}% |
40406 | 26 |
This tutorial introduces the code generator facilities of \isa{Isabelle{\isaliteral{2F}{\isacharslash}}HOL}. It allows to turn (a certain class of) HOL |
38437 | 27 |
specifications into corresponding executable code in the programming |
38813 | 28 |
languages \isa{SML} \cite{SML}, \isa{OCaml} \cite{OCaml}, |
29 |
\isa{Haskell} \cite{haskell-revised-report} and \isa{Scala} |
|
30 |
\cite{scala-overview-tech-report}. |
|
38437 | 31 |
|
32 |
To profit from this tutorial, some familiarity and experience with |
|
33 |
\hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \cite{isa-tutorial} and its basic theories is assumed.% |
|
34 |
\end{isamarkuptext}% |
|
38405 | 35 |
\isamarkuptrue% |
36 |
% |
|
38437 | 37 |
\isamarkupsubsection{Code generation principle: shallow embedding \label{sec:principle}% |
28447 | 38 |
} |
39 |
\isamarkuptrue% |
|
40 |
% |
|
41 |
\begin{isamarkuptext}% |
|
38437 | 42 |
The key concept for understanding Isabelle's code generation is |
43 |
\emph{shallow embedding}: logical entities like constants, types and |
|
44 |
classes are identified with corresponding entities in the target |
|
45 |
language. In particular, the carrier of a generated program's |
|
46 |
semantics are \emph{equational theorems} from the logic. If we view |
|
47 |
a generated program as an implementation of a higher-order rewrite |
|
48 |
system, then every rewrite step performed by the program can be |
|
49 |
simulated in the logic, which guarantees partial correctness |
|
50 |
\cite{Haftmann-Nipkow:2010:code}.% |
|
28447 | 51 |
\end{isamarkuptext}% |
52 |
\isamarkuptrue% |
|
53 |
% |
|
38437 | 54 |
\isamarkupsubsection{A quick start with the Isabelle/HOL toolbox \label{sec:queue_example}% |
28447 | 55 |
} |
56 |
\isamarkuptrue% |
|
57 |
% |
|
58 |
\begin{isamarkuptext}% |
|
38505 | 59 |
In a HOL theory, the \indexdef{}{command}{datatype}\hypertarget{command.datatype}{\hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}}} and \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}}/\indexdef{}{command}{primrec}\hypertarget{command.primrec}{\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}}/\indexdef{}{command}{fun}\hypertarget{command.fun}{\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}} declarations |
60 |
form the core of a functional programming language. By default |
|
61 |
equational theorems stemming from those are used for generated code, |
|
62 |
therefore \qt{naive} code generation can proceed without further |
|
63 |
ado. |
|
28447 | 64 |
|
65 |
For example, here a simple \qt{implementation} of amortised queues:% |
|
66 |
\end{isamarkuptext}% |
|
67 |
\isamarkuptrue% |
|
68 |
% |
|
28564 | 69 |
\isadelimquote |
28447 | 70 |
% |
28564 | 71 |
\endisadelimquote |
28447 | 72 |
% |
28564 | 73 |
\isatagquote |
28447 | 74 |
\isacommand{datatype}\isamarkupfalse% |
40406 | 75 |
\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
28447 | 76 |
\isanewline |
77 |
\isacommand{definition}\isamarkupfalse% |
|
40406 | 78 |
\ empty\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ queue{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
79 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}empty\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
28447 | 80 |
\isanewline |
81 |
\isacommand{primrec}\isamarkupfalse% |
|
40406 | 82 |
\ enqueue\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ queue{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
83 |
\ \ {\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 |
|
28447 | 84 |
\isanewline |
85 |
\isacommand{fun}\isamarkupfalse% |
|
40406 | 86 |
\ dequeue\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a\ queue{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
87 |
\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}None{\isaliteral{2C}{\isacharcomma}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
88 |
\ \ {\isaliteral{7C}{\isacharbar}}\ {\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 |
|
89 |
\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
90 |
\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}case\ rev\ xs\ of\ y\ {\isaliteral{23}{\isacharhash}}\ ys\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Some\ y{\isaliteral{2C}{\isacharcomma}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ % |
|
28564 | 91 |
\endisatagquote |
92 |
{\isafoldquote}% |
|
28447 | 93 |
% |
28564 | 94 |
\isadelimquote |
28447 | 95 |
% |
28564 | 96 |
\endisadelimquote |
28447 | 97 |
% |
38437 | 98 |
\isadeliminvisible |
99 |
% |
|
100 |
\endisadeliminvisible |
|
101 |
% |
|
102 |
\isataginvisible |
|
103 |
% |
|
104 |
\endisataginvisible |
|
105 |
{\isafoldinvisible}% |
|
106 |
% |
|
107 |
\isadeliminvisible |
|
108 |
% |
|
109 |
\endisadeliminvisible |
|
110 |
% |
|
28447 | 111 |
\begin{isamarkuptext}% |
112 |
\noindent Then we can generate code e.g.~for \isa{SML} as follows:% |
|
113 |
\end{isamarkuptext}% |
|
114 |
\isamarkuptrue% |
|
115 |
% |
|
28564 | 116 |
\isadelimquote |
28447 | 117 |
% |
28564 | 118 |
\endisadelimquote |
28447 | 119 |
% |
28564 | 120 |
\isatagquote |
40406 | 121 |
\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse% |
28447 | 122 |
\ empty\ dequeue\ enqueue\ \isakeyword{in}\ SML\isanewline |
40406 | 123 |
\ \ \isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}\ Example\ \isakeyword{file}\ {\isaliteral{22}{\isachardoublequoteopen}}examples{\isaliteral{2F}{\isacharslash}}example{\isaliteral{2E}{\isachardot}}ML{\isaliteral{22}{\isachardoublequoteclose}}% |
28564 | 124 |
\endisatagquote |
125 |
{\isafoldquote}% |
|
28447 | 126 |
% |
28564 | 127 |
\isadelimquote |
28447 | 128 |
% |
28564 | 129 |
\endisadelimquote |
28447 | 130 |
% |
131 |
\begin{isamarkuptext}% |
|
132 |
\noindent resulting in the following code:% |
|
133 |
\end{isamarkuptext}% |
|
134 |
\isamarkuptrue% |
|
135 |
% |
|
39745 | 136 |
\isadelimquotetypewriter |
28447 | 137 |
% |
39745 | 138 |
\endisadelimquotetypewriter |
28447 | 139 |
% |
39745 | 140 |
\isatagquotetypewriter |
28447 | 141 |
% |
142 |
\begin{isamarkuptext}% |
|
40406 | 143 |
structure\ Example\ {\isaliteral{3A}{\isacharcolon}}\ sig\isanewline |
144 |
\ \ val\ id\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline |
|
145 |
\ \ val\ fold\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b\isanewline |
|
146 |
\ \ val\ rev\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ list\isanewline |
|
147 |
\ \ 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 |
|
148 |
\ \ val\ empty\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ queue\isanewline |
|
149 |
\ \ 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 |
|
150 |
\ \ 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 |
|
151 |
end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
152 |
\isanewline |
40406 | 153 |
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 |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
154 |
\isanewline |
40406 | 155 |
fun\ fold\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ id\isanewline |
156 |
\ \ {\isaliteral{7C}{\isacharbar}}\ fold\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ fold\ f\ xs\ o\ f\ x{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
157 |
\isanewline |
40406 | 158 |
fun\ rev\ xs\ {\isaliteral{3D}{\isacharequal}}\ fold\ {\isaliteral{28}{\isacharparenleft}}fn\ a\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ b\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ b{\isaliteral{29}{\isacharparenright}}\ xs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
159 |
\isanewline |
40406 | 160 |
datatype\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ of\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
161 |
\isanewline |
40406 | 162 |
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 |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
163 |
\isanewline |
40406 | 164 |
fun\ dequeue\ {\isaliteral{28}{\isacharparenleft}}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}}\ {\isaliteral{3D}{\isacharequal}}\ {\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 |
165 |
\ \ {\isaliteral{7C}{\isacharbar}}\ 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 |
|
166 |
\ \ {\isaliteral{7C}{\isacharbar}}\ dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{28}{\isacharparenleft}}v\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ va{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
167 |
\ \ \ \ let\isanewline |
40406 | 168 |
\ \ \ \ \ \ val\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ rev\ {\isaliteral{28}{\isacharparenleft}}v\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ va{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
169 |
\ \ \ \ in\isanewline |
40406 | 170 |
\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}SOME\ y{\isaliteral{2C}{\isacharcomma}}\ AQueue\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
171 |
\ \ \ \ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
172 |
\isanewline |
40406 | 173 |
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 |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
174 |
\isanewline |
40406 | 175 |
end{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}struct\ Example{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline% |
28447 | 176 |
\end{isamarkuptext}% |
177 |
\isamarkuptrue% |
|
178 |
% |
|
39745 | 179 |
\endisatagquotetypewriter |
180 |
{\isafoldquotetypewriter}% |
|
28447 | 181 |
% |
39745 | 182 |
\isadelimquotetypewriter |
28447 | 183 |
% |
39745 | 184 |
\endisadelimquotetypewriter |
28447 | 185 |
% |
186 |
\begin{isamarkuptext}% |
|
40406 | 187 |
\noindent The \indexdef{}{command}{export\_code}\hypertarget{command.export-code}{\hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}}} command takes a |
38505 | 188 |
space-separated list of constants for which code shall be generated; |
189 |
anything else needed for those is added implicitly. Then follows a |
|
190 |
target language identifier and a freely chosen module name. A file |
|
191 |
name denotes the destination to store the generated code. Note that |
|
192 |
the semantics of the destination depends on the target language: for |
|
38813 | 193 |
\isa{SML}, \isa{OCaml} and \isa{Scala} it denotes a \emph{file}, |
194 |
for \isa{Haskell} it denotes a \emph{directory} where a file named as the |
|
40406 | 195 |
module name (with extension \isa{{\isaliteral{2E}{\isachardot}}hs}) is written:% |
28447 | 196 |
\end{isamarkuptext}% |
197 |
\isamarkuptrue% |
|
198 |
% |
|
28564 | 199 |
\isadelimquote |
28447 | 200 |
% |
28564 | 201 |
\endisadelimquote |
28447 | 202 |
% |
28564 | 203 |
\isatagquote |
40406 | 204 |
\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse% |
28447 | 205 |
\ empty\ dequeue\ enqueue\ \isakeyword{in}\ Haskell\isanewline |
40406 | 206 |
\ \ \isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}\ Example\ \isakeyword{file}\ {\isaliteral{22}{\isachardoublequoteopen}}examples{\isaliteral{2F}{\isacharslash}}{\isaliteral{22}{\isachardoublequoteclose}}% |
28564 | 207 |
\endisatagquote |
208 |
{\isafoldquote}% |
|
28447 | 209 |
% |
28564 | 210 |
\isadelimquote |
28447 | 211 |
% |
28564 | 212 |
\endisadelimquote |
28447 | 213 |
% |
214 |
\begin{isamarkuptext}% |
|
38437 | 215 |
\noindent This is the corresponding code:% |
28447 | 216 |
\end{isamarkuptext}% |
217 |
\isamarkuptrue% |
|
218 |
% |
|
39745 | 219 |
\isadelimquotetypewriter |
28447 | 220 |
% |
39745 | 221 |
\endisadelimquotetypewriter |
28447 | 222 |
% |
39745 | 223 |
\isatagquotetypewriter |
28447 | 224 |
% |
225 |
\begin{isamarkuptext}% |
|
40406 | 226 |
module\ Example\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
227 |
\isanewline |
40406 | 228 |
data\ Queue\ a\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
229 |
\isanewline |
40406 | 230 |
empty\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ Queue\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
231 |
empty\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
232 |
\isanewline |
40406 | 233 |
dequeue\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ Queue\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}Maybe\ a{\isaliteral{2C}{\isacharcomma}}\ Queue\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
234 |
dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Nothing{\isaliteral{2C}{\isacharcomma}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
235 |
dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{3A}{\isacharcolon}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Just\ y{\isaliteral{2C}{\isacharcomma}}\ AQueue\ xs\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
236 |
dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{28}{\isacharparenleft}}v\ {\isaliteral{3A}{\isacharcolon}}\ va{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
237 |
\ \ let\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
238 |
\ \ \ \ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{3A}{\isacharcolon}}\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ reverse\ {\isaliteral{28}{\isacharparenleft}}v\ {\isaliteral{3A}{\isacharcolon}}\ va{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
239 |
\ \ {\isaliteral{7D}{\isacharbraceright}}\ in\ {\isaliteral{28}{\isacharparenleft}}Just\ y{\isaliteral{2C}{\isacharcomma}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
240 |
\isanewline |
40406 | 241 |
enqueue\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Queue\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Queue\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
242 |
enqueue\ x\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{29}{\isacharparenright}}\ ys{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
243 |
\isanewline |
40406 | 244 |
{\isaliteral{7D}{\isacharbraceright}}\isanewline% |
28447 | 245 |
\end{isamarkuptext}% |
246 |
\isamarkuptrue% |
|
247 |
% |
|
39745 | 248 |
\endisatagquotetypewriter |
249 |
{\isafoldquotetypewriter}% |
|
28447 | 250 |
% |
39745 | 251 |
\isadelimquotetypewriter |
28447 | 252 |
% |
39745 | 253 |
\endisadelimquotetypewriter |
28447 | 254 |
% |
255 |
\begin{isamarkuptext}% |
|
40406 | 256 |
\noindent For more details about \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}} see |
38437 | 257 |
\secref{sec:further}.% |
28447 | 258 |
\end{isamarkuptext}% |
259 |
\isamarkuptrue% |
|
260 |
% |
|
38437 | 261 |
\isamarkupsubsection{Type classes% |
28447 | 262 |
} |
263 |
\isamarkuptrue% |
|
264 |
% |
|
265 |
\begin{isamarkuptext}% |
|
38437 | 266 |
Code can also be generated from type classes in a Haskell-like |
267 |
manner. For illustration here an example from abstract algebra:% |
|
268 |
\end{isamarkuptext}% |
|
269 |
\isamarkuptrue% |
|
270 |
% |
|
271 |
\isadelimquote |
|
272 |
% |
|
273 |
\endisadelimquote |
|
274 |
% |
|
275 |
\isatagquote |
|
276 |
\isacommand{class}\isamarkupfalse% |
|
40406 | 277 |
\ semigroup\ {\isaliteral{3D}{\isacharequal}}\isanewline |
278 |
\ \ \isakeyword{fixes}\ mult\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{7}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
279 |
\ \ \isakeyword{assumes}\ assoc{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38437 | 280 |
\isanewline |
281 |
\isacommand{class}\isamarkupfalse% |
|
40406 | 282 |
\ monoid\ {\isaliteral{3D}{\isacharequal}}\ semigroup\ {\isaliteral{2B}{\isacharplus}}\isanewline |
283 |
\ \ \isakeyword{fixes}\ neutral\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
284 |
\ \ \isakeyword{assumes}\ neutl{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
285 |
\ \ \ \ \isakeyword{and}\ neutr{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38437 | 286 |
\isanewline |
287 |
\isacommand{instantiation}\isamarkupfalse% |
|
40406 | 288 |
\ nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ monoid\isanewline |
38437 | 289 |
\isakeyword{begin}\isanewline |
290 |
\isanewline |
|
291 |
\isacommand{primrec}\isamarkupfalse% |
|
40406 | 292 |
\ mult{\isaliteral{5F}{\isacharunderscore}}nat\ \isakeyword{where}\isanewline |
293 |
\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{0}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
294 |
\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}Suc\ m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2B}{\isacharplus}}\ m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38437 | 295 |
\isanewline |
296 |
\isacommand{definition}\isamarkupfalse% |
|
40406 | 297 |
\ neutral{\isaliteral{5F}{\isacharunderscore}}nat\ \isakeyword{where}\isanewline |
298 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38437 | 299 |
\isanewline |
300 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 301 |
\ add{\isaliteral{5F}{\isacharunderscore}}mult{\isaliteral{5F}{\isacharunderscore}}distrib{\isaliteral{3A}{\isacharcolon}}\isanewline |
302 |
\ \ \isakeyword{fixes}\ n\ m\ q\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
|
303 |
\ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ m{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ q\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ q\ {\isaliteral{2B}{\isacharplus}}\ m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ q{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38437 | 304 |
\ \ \isacommand{by}\isamarkupfalse% |
40406 | 305 |
\ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all\isanewline |
38437 | 306 |
\isanewline |
307 |
\isacommand{instance}\isamarkupfalse% |
|
308 |
\ \isacommand{proof}\isamarkupfalse% |
|
309 |
\isanewline |
|
310 |
\ \ \isacommand{fix}\isamarkupfalse% |
|
40406 | 311 |
\ m\ n\ q\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
38437 | 312 |
\ \ \isacommand{show}\isamarkupfalse% |
40406 | 313 |
\ {\isaliteral{22}{\isachardoublequoteopen}}m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ q\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ q{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
38437 | 314 |
\ \ \ \ \isacommand{by}\isamarkupfalse% |
40406 | 315 |
\ {\isaliteral{28}{\isacharparenleft}}induct\ m{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ add{\isaliteral{5F}{\isacharunderscore}}mult{\isaliteral{5F}{\isacharunderscore}}distrib{\isaliteral{29}{\isacharparenright}}\isanewline |
38437 | 316 |
\ \ \isacommand{show}\isamarkupfalse% |
40406 | 317 |
\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
38437 | 318 |
\ \ \ \ \isacommand{by}\isamarkupfalse% |
40406 | 319 |
\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline |
38437 | 320 |
\ \ \isacommand{show}\isamarkupfalse% |
40406 | 321 |
\ {\isaliteral{22}{\isachardoublequoteopen}}m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
38437 | 322 |
\ \ \ \ \isacommand{by}\isamarkupfalse% |
40406 | 323 |
\ {\isaliteral{28}{\isacharparenleft}}induct\ m{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline |
38437 | 324 |
\isacommand{qed}\isamarkupfalse% |
325 |
\isanewline |
|
326 |
\isanewline |
|
327 |
\isacommand{end}\isamarkupfalse% |
|
328 |
% |
|
329 |
\endisatagquote |
|
330 |
{\isafoldquote}% |
|
331 |
% |
|
332 |
\isadelimquote |
|
333 |
% |
|
334 |
\endisadelimquote |
|
335 |
% |
|
336 |
\begin{isamarkuptext}% |
|
337 |
\noindent We define the natural operation of the natural numbers |
|
338 |
on monoids:% |
|
339 |
\end{isamarkuptext}% |
|
340 |
\isamarkuptrue% |
|
341 |
% |
|
342 |
\isadelimquote |
|
343 |
% |
|
344 |
\endisadelimquote |
|
345 |
% |
|
346 |
\isatagquote |
|
347 |
\isacommand{primrec}\isamarkupfalse% |
|
40406 | 348 |
\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{in}\ monoid{\isaliteral{29}{\isacharparenright}}\ pow\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
349 |
\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}pow\ {\isadigit{0}}\ a\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
350 |
\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}pow\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ a\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ pow\ n\ a{\isaliteral{22}{\isachardoublequoteclose}}% |
|
38437 | 351 |
\endisatagquote |
352 |
{\isafoldquote}% |
|
353 |
% |
|
354 |
\isadelimquote |
|
355 |
% |
|
356 |
\endisadelimquote |
|
357 |
% |
|
358 |
\begin{isamarkuptext}% |
|
359 |
\noindent This we use to define the discrete exponentiation |
|
360 |
function:% |
|
361 |
\end{isamarkuptext}% |
|
362 |
\isamarkuptrue% |
|
363 |
% |
|
364 |
\isadelimquote |
|
365 |
% |
|
366 |
\endisadelimquote |
|
367 |
% |
|
368 |
\isatagquote |
|
369 |
\isacommand{definition}\isamarkupfalse% |
|
40406 | 370 |
\ bexp\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
371 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}bexp\ n\ {\isaliteral{3D}{\isacharequal}}\ pow\ n\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
38437 | 372 |
\endisatagquote |
373 |
{\isafoldquote}% |
|
374 |
% |
|
375 |
\isadelimquote |
|
376 |
% |
|
377 |
\endisadelimquote |
|
378 |
% |
|
379 |
\begin{isamarkuptext}% |
|
380 |
\noindent The corresponding code in Haskell uses that language's |
|
381 |
native classes:% |
|
382 |
\end{isamarkuptext}% |
|
383 |
\isamarkuptrue% |
|
384 |
% |
|
39745 | 385 |
\isadelimquotetypewriter |
38437 | 386 |
% |
39745 | 387 |
\endisadelimquotetypewriter |
38437 | 388 |
% |
39745 | 389 |
\isatagquotetypewriter |
38437 | 390 |
% |
391 |
\begin{isamarkuptext}% |
|
40406 | 392 |
module\ Example\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
393 |
\isanewline |
40406 | 394 |
data\ Nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
395 |
\isanewline |
40406 | 396 |
plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
397 |
plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ m\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
398 |
plus{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
399 |
\isanewline |
40406 | 400 |
class\ Semigroup\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
401 |
\ \ mult\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
402 |
{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
403 |
\isanewline |
40406 | 404 |
class\ {\isaliteral{28}{\isacharparenleft}}Semigroup\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Monoid\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
405 |
\ \ neutral\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
406 |
{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
407 |
\isanewline |
40406 | 408 |
pow\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Monoid\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
409 |
pow\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ a\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
410 |
pow\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ a\ {\isaliteral{3D}{\isacharequal}}\ mult\ a\ {\isaliteral{28}{\isacharparenleft}}pow\ n\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
411 |
\isanewline |
40406 | 412 |
mult{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
413 |
mult{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
414 |
mult{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{28}{\isacharparenleft}}mult{\isaliteral{5F}{\isacharunderscore}}nat\ m\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
415 |
\isanewline |
44548 | 416 |
neutral{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
417 |
neutral{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3D}{\isacharequal}}\ Suc\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
418 |
\isanewline |
|
40406 | 419 |
instance\ Semigroup\ Nat\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
420 |
\ \ mult\ {\isaliteral{3D}{\isacharequal}}\ mult{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
421 |
{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
422 |
\isanewline |
40406 | 423 |
instance\ Monoid\ Nat\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
424 |
\ \ neutral\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
425 |
{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
426 |
\isanewline |
40406 | 427 |
bexp\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
428 |
bexp\ n\ {\isaliteral{3D}{\isacharequal}}\ pow\ n\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
429 |
\isanewline |
40406 | 430 |
{\isaliteral{7D}{\isacharbraceright}}\isanewline% |
38437 | 431 |
\end{isamarkuptext}% |
432 |
\isamarkuptrue% |
|
433 |
% |
|
39745 | 434 |
\endisatagquotetypewriter |
435 |
{\isafoldquotetypewriter}% |
|
38437 | 436 |
% |
39745 | 437 |
\isadelimquotetypewriter |
38437 | 438 |
% |
39745 | 439 |
\endisadelimquotetypewriter |
38437 | 440 |
% |
441 |
\begin{isamarkuptext}% |
|
442 |
\noindent This is a convenient place to show how explicit dictionary |
|
443 |
construction manifests in generated code -- the same example in |
|
444 |
\isa{SML}:% |
|
445 |
\end{isamarkuptext}% |
|
446 |
\isamarkuptrue% |
|
447 |
% |
|
39745 | 448 |
\isadelimquotetypewriter |
38437 | 449 |
% |
39745 | 450 |
\endisadelimquotetypewriter |
38437 | 451 |
% |
39745 | 452 |
\isatagquotetypewriter |
38437 | 453 |
% |
454 |
\begin{isamarkuptext}% |
|
40406 | 455 |
structure\ Example\ {\isaliteral{3A}{\isacharcolon}}\ sig\isanewline |
456 |
\ \ datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat\isanewline |
|
457 |
\ \ val\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\isanewline |
|
458 |
\ \ type\ {\isaliteral{27}{\isacharprime}}a\ semigroup\isanewline |
|
459 |
\ \ val\ mult\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline |
|
460 |
\ \ type\ {\isaliteral{27}{\isacharprime}}a\ monoid\isanewline |
|
461 |
\ \ val\ semigroup{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup\isanewline |
|
462 |
\ \ val\ neutral\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline |
|
463 |
\ \ val\ pow\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline |
|
464 |
\ \ val\ mult{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\isanewline |
|
44548 | 465 |
\ \ val\ neutral{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
40406 | 466 |
\ \ val\ semigroup{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ semigroup\isanewline |
467 |
\ \ val\ monoid{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ monoid\isanewline |
|
468 |
\ \ val\ bexp\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\isanewline |
|
469 |
end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
470 |
\isanewline |
40406 | 471 |
datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
472 |
\isanewline |
40406 | 473 |
fun\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ m\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline |
474 |
\ \ {\isaliteral{7C}{\isacharbar}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
475 |
\isanewline |
40406 | 476 |
type\ {\isaliteral{27}{\isacharprime}}a\ semigroup\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}mult\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
477 |
val\ mult\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}mult\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
478 |
\isanewline |
40406 | 479 |
type\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup{\isaliteral{2C}{\isacharcomma}}\ neutral\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
480 |
val\ semigroup{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
481 |
val\ neutral\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}neutral\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
482 |
\isanewline |
40406 | 483 |
fun\ pow\ A{\isaliteral{5F}{\isacharunderscore}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ a\ {\isaliteral{3D}{\isacharequal}}\ neutral\ A{\isaliteral{5F}{\isacharunderscore}}\isanewline |
484 |
\ \ {\isaliteral{7C}{\isacharbar}}\ pow\ A{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ a\ {\isaliteral{3D}{\isacharequal}}\ mult\ {\isaliteral{28}{\isacharparenleft}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoid\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ a\ {\isaliteral{28}{\isacharparenleft}}pow\ A{\isaliteral{5F}{\isacharunderscore}}\ n\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
485 |
\isanewline |
40406 | 486 |
fun\ mult{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\isanewline |
487 |
\ \ {\isaliteral{7C}{\isacharbar}}\ mult{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{28}{\isacharparenleft}}mult{\isaliteral{5F}{\isacharunderscore}}nat\ m\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
488 |
\isanewline |
44548 | 489 |
val\ neutral{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\ Suc\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
490 |
\isanewline |
44548 | 491 |
val\ semigroup{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}mult\ {\isaliteral{3D}{\isacharequal}}\ mult{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\ nat\ semigroup{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
492 |
\isanewline |
40406 | 493 |
val\ monoid{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3D}{\isacharequal}}\ semigroup{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{2C}{\isacharcomma}}\ neutral\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{7D}{\isacharbraceright}}\isanewline |
494 |
\ \ {\isaliteral{3A}{\isacharcolon}}\ nat\ monoid{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
495 |
\isanewline |
40406 | 496 |
fun\ bexp\ n\ {\isaliteral{3D}{\isacharequal}}\ pow\ monoid{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39210
diff
changeset
|
497 |
\isanewline |
40406 | 498 |
end{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}struct\ Example{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline% |
38437 | 499 |
\end{isamarkuptext}% |
500 |
\isamarkuptrue% |
|
501 |
% |
|
39745 | 502 |
\endisatagquotetypewriter |
503 |
{\isafoldquotetypewriter}% |
|
38437 | 504 |
% |
39745 | 505 |
\isadelimquotetypewriter |
38437 | 506 |
% |
39745 | 507 |
\endisadelimquotetypewriter |
38437 | 508 |
% |
509 |
\begin{isamarkuptext}% |
|
510 |
\noindent Note the parameters with trailing underscore (\verb|A_|), which are the dictionary parameters.% |
|
511 |
\end{isamarkuptext}% |
|
512 |
\isamarkuptrue% |
|
513 |
% |
|
514 |
\isamarkupsubsection{How to continue from here% |
|
515 |
} |
|
516 |
\isamarkuptrue% |
|
517 |
% |
|
518 |
\begin{isamarkuptext}% |
|
519 |
What you have seen so far should be already enough in a lot of |
|
520 |
cases. If you are content with this, you can quit reading here. |
|
28447 | 521 |
|
38437 | 522 |
Anyway, to understand situations where problems occur or to increase |
523 |
the scope of code generation beyond default, it is necessary to gain |
|
524 |
some understanding how the code generator actually works: |
|
28447 | 525 |
|
526 |
\begin{itemize} |
|
527 |
||
38437 | 528 |
\item The foundations of the code generator are described in |
529 |
\secref{sec:foundations}. |
|
530 |
||
531 |
\item In particular \secref{sec:utterly_wrong} gives hints how to |
|
532 |
debug situations where code generation does not succeed as |
|
533 |
expected. |
|
28447 | 534 |
|
38437 | 535 |
\item The scope and quality of generated code can be increased |
536 |
dramatically by applying refinement techniques, which are |
|
537 |
introduced in \secref{sec:refinement}. |
|
28447 | 538 |
|
38437 | 539 |
\item Inductive predicates can be turned executable using an |
540 |
extension of the code generator \secref{sec:inductive}. |
|
541 |
||
40755 | 542 |
\item If you want to utilize code generation to obtain fast |
543 |
evaluators e.g.~for decision procedures, have a look at |
|
544 |
\secref{sec:evaluation}. |
|
545 |
||
38437 | 546 |
\item You may want to skim over the more technical sections |
547 |
\secref{sec:adaptation} and \secref{sec:further}. |
|
548 |
||
42096 | 549 |
\item The target language Scala \cite{scala-overview-tech-report} |
550 |
comes with some specialities discussed in \secref{sec:scala}. |
|
551 |
||
38437 | 552 |
\item For exhaustive syntax diagrams etc. you should visit the |
553 |
Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}. |
|
28447 | 554 |
|
555 |
\end{itemize} |
|
556 |
||
38437 | 557 |
\bigskip |
558 |
||
559 |
\begin{center}\fbox{\fbox{\begin{minipage}{8cm} |
|
560 |
||
561 |
\begin{center}\textit{Happy proving, happy hacking!}\end{center} |
|
562 |
||
45211
3dd426ae6bea
removed some remaining artefacts of ancient SML code generator
haftmann
parents:
44548
diff
changeset
|
563 |
\end{minipage}}}\end{center}% |
28447 | 564 |
\end{isamarkuptext}% |
565 |
\isamarkuptrue% |
|
566 |
% |
|
567 |
\isadelimtheory |
|
568 |
% |
|
569 |
\endisadelimtheory |
|
570 |
% |
|
571 |
\isatagtheory |
|
572 |
\isacommand{end}\isamarkupfalse% |
|
573 |
% |
|
574 |
\endisatagtheory |
|
575 |
{\isafoldtheory}% |
|
576 |
% |
|
577 |
\isadelimtheory |
|
578 |
% |
|
579 |
\endisadelimtheory |
|
580 |
\isanewline |
|
46523 | 581 |
\isanewline |
28447 | 582 |
\end{isabellebody}% |
583 |
%%% Local Variables: |
|
584 |
%%% mode: latex |
|
585 |
%%% TeX-master: "root" |
|
586 |
%%% End: |