src/Doc/Codegen/Adaptation.thy
author blanchet
Tue, 07 Nov 2017 15:16:42 +0100
changeset 67022 49309fe530fd
parent 66453 cc19f7ca2ed6
child 68028 1f9f973eed2a
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31050
555b56b66fcf adaptation replaces adaption
haftmann
parents: 30882
diff changeset
     1
theory Adaptation
66453
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents: 65041
diff changeset
     2
imports Codegen_Basics.Setup
28213
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents:
diff changeset
     3
begin
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents:
diff changeset
     4
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
     5
setup %invisible \<open>Code_Target.add_derived_target ("\<SML>", [("SML", I)])
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
     6
  #> Code_Target.add_derived_target ("\<SMLdummy>", [("Haskell", I)])\<close>
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
     7
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
     8
section \<open>Adaptation to target languages \label{sec:adaptation}\<close>
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
     9
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
    10
subsection \<open>Adapting code generation\<close>
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    11
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
    12
text \<open>
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    13
  The aspects of code generation introduced so far have two aspects
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    14
  in common:
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    15
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    16
  \begin{itemize}
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    17
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    18
    \item They act uniformly, without reference to a specific target
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    19
       language.
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    20
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    21
    \item They are \emph{safe} in the sense that as long as you trust
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    22
       the code generator meta theory and implementation, you cannot
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    23
       produce programs that yield results which are not derivable in
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    24
       the logic.
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    25
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    26
  \end{itemize}
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    27
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    28
  \noindent In this section we will introduce means to \emph{adapt}
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    29
  the serialiser to a specific target language, i.e.~to print program
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    30
  fragments in a way which accommodates \qt{already existing}
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    31
  ingredients of a target language environment, for three reasons:
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    32
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    33
  \begin{itemize}
28593
f087237af65d continued codegen tutorial
haftmann
parents: 28564
diff changeset
    34
    \item improving readability and aesthetics of generated code
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    35
    \item gaining efficiency
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    36
    \item interface with language parts which have no direct counterpart
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    37
      in @{text "HOL"} (say, imperative data structures)
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    38
  \end{itemize}
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    39
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    40
  \noindent Generally, you should avoid using those features yourself
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    41
  \emph{at any cost}:
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    42
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    43
  \begin{itemize}
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    44
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    45
    \item The safe configuration methods act uniformly on every target
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    46
      language, whereas for adaptation you have to treat each target
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    47
      language separately.
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    48
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    49
    \item Application is extremely tedious since there is no
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    50
      abstraction which would allow for a static check, making it easy
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    51
      to produce garbage.
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    52
34155
14aaccb399b3 Polishing up the English
paulson
parents: 31206
diff changeset
    53
    \item Subtle errors can be introduced unconsciously.
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    54
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    55
  \end{itemize}
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    56
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    57
  \noindent However, even if you ought refrain from setting up
51162
310b94ed1815 dropped now obsolete hint;
haftmann
parents: 51160
diff changeset
    58
  adaptation yourself, already @{text "HOL"} comes with some
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    59
  reasonable default adaptations (say, using target language list
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    60
  syntax).  There also some common adaptation cases which you can
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    61
  setup by importing particular library theories.  In order to
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    62
  understand these, we provide some clues here; these however are not
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    63
  supposed to replace a careful study of the sources.
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
    64
\<close>
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    65
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    66
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
    67
subsection \<open>The adaptation principle\<close>
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
    68
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
    69
text \<open>
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    70
  Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
    71
  conceptually supposed to be:
28601
b72589374396 figure for adaption
haftmann
parents: 28593
diff changeset
    72
60768
f47bd91fdc75 proper latex;
wenzelm
parents: 59482
diff changeset
    73
  \begin{figure}[h]
52742
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    74
    \begin{tikzpicture}[scale = 0.5]
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    75
      \tikzstyle water=[color = blue, thick]
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    76
      \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    77
      \tikzstyle process=[color = green, semithick, ->]
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    78
      \tikzstyle adaptation=[color = red, semithick, ->]
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    79
      \tikzstyle target=[color = black]
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    80
      \foreach \x in {0, ..., 24}
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    81
        \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    82
          + (0.25, -0.25) cos + (0.25, 0.25);
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    83
      \draw[style=ice] (1, 0) --
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    84
        (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    85
      \draw[style=ice] (9, 0) --
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    86
        (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    87
      \draw[style=ice] (15, -6) --
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    88
        (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    89
      \draw[style=process]
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    90
        (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    91
      \draw[style=process]
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    92
        (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    93
      \node (adaptation) at (11, -2) [style=adaptation] {adaptation};
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    94
      \node at (19, 3) [rotate=90] {generated};
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    95
      \node at (19.5, -5) {language};
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    96
      \node at (19.5, -3) {library};
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    97
      \node (includes) at (19.5, -1) {includes};
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    98
      \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
    99
      \draw[style=process]
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
   100
        (includes) -- (serialisation);
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
   101
      \draw[style=process]
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
   102
        (reserved) -- (serialisation);
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
   103
      \draw[style=adaptation]
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
   104
        (adaptation) -- (serialisation);
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
   105
      \draw[style=adaptation]
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
   106
        (adaptation) -- (includes);
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
   107
      \draw[style=adaptation]
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
   108
        (adaptation) -- (reserved);
e7296939fec2 more direct inclusion of tikz pictures;
wenzelm
parents: 52665
diff changeset
   109
    \end{tikzpicture}
31050
555b56b66fcf adaptation replaces adaption
haftmann
parents: 30882
diff changeset
   110
    \caption{The adaptation principle}
555b56b66fcf adaptation replaces adaption
haftmann
parents: 30882
diff changeset
   111
    \label{fig:adaptation}
28601
b72589374396 figure for adaption
haftmann
parents: 28593
diff changeset
   112
  \end{figure}
b72589374396 figure for adaption
haftmann
parents: 28593
diff changeset
   113
b72589374396 figure for adaption
haftmann
parents: 28593
diff changeset
   114
  \noindent In the tame view, code generation acts as broker between
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   115
  @{text logic}, @{text "intermediate language"} and @{text "target
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   116
  language"} by means of @{text translation} and @{text
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   117
  serialisation}; for the latter, the serialiser has to observe the
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   118
  structure of the @{text language} itself plus some @{text reserved}
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   119
  keywords which have to be avoided for generated code.  However, if
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   120
  you consider @{text adaptation} mechanisms, the code generated by
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   121
  the serializer is just the tip of the iceberg:
28601
b72589374396 figure for adaption
haftmann
parents: 28593
diff changeset
   122
b72589374396 figure for adaption
haftmann
parents: 28593
diff changeset
   123
  \begin{itemize}
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   124
28635
cc53d2ab0170 filled remaining gaps
haftmann
parents: 28609
diff changeset
   125
    \item @{text serialisation} can be \emph{parametrised} such that
cc53d2ab0170 filled remaining gaps
haftmann
parents: 28609
diff changeset
   126
      logical entities are mapped to target-specific ones
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   127
      (e.g. target-specific list syntax, see also
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   128
      \secref{sec:adaptation_mechanisms})
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   129
28635
cc53d2ab0170 filled remaining gaps
haftmann
parents: 28609
diff changeset
   130
    \item Such parametrisations can involve references to a
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   131
      target-specific standard @{text library} (e.g. using the @{text
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   132
      Haskell} @{verbatim Maybe} type instead of the @{text HOL}
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   133
      @{type "option"} type); if such are used, the corresponding
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   134
      identifiers (in our example, @{verbatim Maybe}, @{verbatim
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   135
      Nothing} and @{verbatim Just}) also have to be considered @{text
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   136
      reserved}.
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   137
28635
cc53d2ab0170 filled remaining gaps
haftmann
parents: 28609
diff changeset
   138
    \item Even more, the user can enrich the library of the
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   139
      target-language by providing code snippets (\qt{@{text
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   140
      "includes"}}) which are prepended to any generated code (see
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   141
      \secref{sec:include}); this typically also involves further
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   142
      @{text reserved} identifiers.
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   143
28601
b72589374396 figure for adaption
haftmann
parents: 28593
diff changeset
   144
  \end{itemize}
28635
cc53d2ab0170 filled remaining gaps
haftmann
parents: 28609
diff changeset
   145
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   146
  \noindent As figure \ref{fig:adaptation} illustrates, all these
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   147
  adaptation mechanisms have to act consistently; it is at the
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   148
  discretion of the user to take care for this.
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   149
\<close>
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
   150
65041
2525e680f94f basic documentation for computations
haftmann
parents: 63680
diff changeset
   151
subsection \<open>Common adaptation applications \label{sec:common_adaptation}\<close>
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   152
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   153
text \<open>
28428
haftmann
parents: 28420
diff changeset
   154
  The @{theory HOL} @{theory Main} theory already provides a code
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   155
  generator setup which should be suitable for most applications.
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   156
  Common extensions and modifications are available by certain
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   157
  theories in \<^dir>\<open>~~/src/HOL/Library\<close>; beside being useful in
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   158
  applications, they may serve as a tutorial for customising the code
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   159
  generator setup (see below \secref{sec:adaptation_mechanisms}).
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   160
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   161
  \begin{description}
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   162
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   163
    \item[@{theory "Code_Numeral"}] provides additional numeric
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   164
       types @{typ integer} and @{typ natural} isomorphic to types
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   165
       @{typ int} and @{typ nat} respectively.  Type @{typ integer}
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   166
       is mapped to target-language built-in integers; @{typ natural}
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   167
       is implemented as abstract type over @{typ integer}.
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   168
       Useful for code setups which involve e.g.~indexing
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   169
       of target-language arrays.  Part of @{text "HOL-Main"}.
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   170
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   171
    \item[@{text "Code_Target_Int"}] implements type @{typ int}
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   172
       by @{typ integer} and thus by target-language built-in integers.
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   173
51171
e8b2d90da499 corrected and clarified Code_Binary_Nat vs. Code_Target_Nat
haftmann
parents: 51162
diff changeset
   174
    \item[@{text "Code_Binary_Nat"}] implements type
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   175
       @{typ nat} using a binary rather than a linear representation,
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   176
       which yields a considerable speedup for computations.
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60768
diff changeset
   177
       Pattern matching with @{term "0::nat"} / @{const "Suc"} is eliminated
51171
e8b2d90da499 corrected and clarified Code_Binary_Nat vs. Code_Target_Nat
haftmann
parents: 51162
diff changeset
   178
       by a preprocessor.\label{abstract_nat}
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   179
51171
e8b2d90da499 corrected and clarified Code_Binary_Nat vs. Code_Target_Nat
haftmann
parents: 51162
diff changeset
   180
    \item[@{text "Code_Target_Nat"}] implements type @{typ nat}
e8b2d90da499 corrected and clarified Code_Binary_Nat vs. Code_Target_Nat
haftmann
parents: 51162
diff changeset
   181
       by @{typ integer} and thus by target-language built-in integers.
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60768
diff changeset
   182
       Pattern matching with @{term "0::nat"} / @{const "Suc"} is eliminated
51171
e8b2d90da499 corrected and clarified Code_Binary_Nat vs. Code_Target_Nat
haftmann
parents: 51162
diff changeset
   183
       by a preprocessor.
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   184
51162
310b94ed1815 dropped now obsolete hint;
haftmann
parents: 51160
diff changeset
   185
    \item[@{text "Code_Target_Numeral"}] is a convenience theory
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   186
       containing both @{text "Code_Target_Nat"} and
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   187
       @{text "Code_Target_Int"}.
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   188
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   189
    \item[@{theory "String"}] provides an additional datatype @{typ
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   190
       String.literal} which is isomorphic to strings; @{typ
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   191
       String.literal}s are mapped to target-language strings.  Useful
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   192
       for code setups which involve e.g.~printing (error) messages.
46519
17dde5feea4b clarified
haftmann
parents: 40351
diff changeset
   193
       Part of @{text "HOL-Main"}.
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   194
59482
9b590e32646a more explicit hint on import order
haftmann
parents: 59379
diff changeset
   195
    \item[@{text "Code_Char"}] represents @{text HOL} characters by
9b590e32646a more explicit hint on import order
haftmann
parents: 59379
diff changeset
   196
       character literals in target languages.  \emph{Warning:} This
9b590e32646a more explicit hint on import order
haftmann
parents: 59379
diff changeset
   197
       modifies adaptation in a non-conservative manner and thus
9b590e32646a more explicit hint on import order
haftmann
parents: 59379
diff changeset
   198
       should always be imported \emph{last} in a theory header.
9b590e32646a more explicit hint on import order
haftmann
parents: 59379
diff changeset
   199
51162
310b94ed1815 dropped now obsolete hint;
haftmann
parents: 51160
diff changeset
   200
    \item[@{theory "IArray"}] provides a type @{typ "'a iarray"}
310b94ed1815 dropped now obsolete hint;
haftmann
parents: 51160
diff changeset
   201
       isomorphic to lists but implemented by (effectively immutable)
310b94ed1815 dropped now obsolete hint;
haftmann
parents: 51160
diff changeset
   202
       arrays \emph{in SML only}.
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   203
51162
310b94ed1815 dropped now obsolete hint;
haftmann
parents: 51160
diff changeset
   204
  \end{description}
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   205
\<close>
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   206
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   207
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   208
subsection \<open>Parametrising serialisation \label{sec:adaptation_mechanisms}\<close>
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   209
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   210
text \<open>
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   211
  Consider the following function and its corresponding SML code:
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   212
\<close>
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   213
28564
haftmann
parents: 28561
diff changeset
   214
primrec %quote in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   215
  "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
28447
haftmann
parents: 28428
diff changeset
   216
(*<*)
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   217
code_printing %invisible
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   218
  type_constructor bool \<rightharpoonup> (SML)
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   219
| constant True \<rightharpoonup> (SML)
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   220
| constant False \<rightharpoonup> (SML)
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   221
| constant HOL.conj \<rightharpoonup> (SML)
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   222
| constant Not \<rightharpoonup> (SML)
28447
haftmann
parents: 28428
diff changeset
   223
(*>*)
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   224
text %quotetypewriter \<open>
39683
f75a01ee6c41 prefer typewrite tag over raw latex environment
haftmann
parents: 39664
diff changeset
   225
  @{code_stmts in_interval (SML)}
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   226
\<close>
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   227
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   228
text \<open>
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   229
  \noindent Though this is correct code, it is a little bit
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   230
  unsatisfactory: boolean values and operators are materialised as
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   231
  distinguished entities with have nothing to do with the SML-built-in
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   232
  notion of \qt{bool}.  This results in less readable code;
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   233
  additionally, eager evaluation may cause programs to loop or break
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   234
  which would perfectly terminate when the existing SML @{verbatim
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   235
  "bool"} would be used.  To map the HOL @{typ bool} on SML @{verbatim
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   236
  "bool"}, we may use \qn{custom serialisations}:
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   237
\<close>
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   238
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   239
code_printing %quotett
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   240
  type_constructor bool \<rightharpoonup> (SML) "bool"
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   241
| constant True \<rightharpoonup> (SML) "true"
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   242
| constant False \<rightharpoonup> (SML) "false"
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   243
| constant HOL.conj \<rightharpoonup> (SML) "_ andalso _"
28213
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents:
diff changeset
   244
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   245
text \<open>
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   246
  \noindent The @{command_def code_printing} command takes a series
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   247
  of symbols (contants, type constructor, \ldots)
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   248
  together with target-specific custom serialisations.  Each
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   249
  custom serialisation starts with a target language identifier
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   250
  followed by an expression, which during code serialisation is
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   251
  inserted whenever the type constructor would occur.  Each
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   252
  ``@{verbatim "_"}'' in a serialisation expression is treated as a
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   253
  placeholder for the constant's or the type constructor's arguments.
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   254
\<close>
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   255
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   256
text %quotetypewriter \<open>
39683
f75a01ee6c41 prefer typewrite tag over raw latex environment
haftmann
parents: 39664
diff changeset
   257
  @{code_stmts in_interval (SML)}
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   258
\<close>
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   259
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   260
text \<open>
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   261
  \noindent This still is not perfect: the parentheses around the
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   262
  \qt{andalso} expression are superfluous.  Though the serialiser by
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   263
  no means attempts to imitate the rich Isabelle syntax framework, it
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   264
  provides some common idioms, notably associative infixes with
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   265
  precedences which may be used here:
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   266
\<close>
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   267
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   268
code_printing %quotett
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   269
  constant HOL.conj \<rightharpoonup> (SML) infixl 1 "andalso"
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   270
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   271
text %quotetypewriter \<open>
39683
f75a01ee6c41 prefer typewrite tag over raw latex environment
haftmann
parents: 39664
diff changeset
   272
  @{code_stmts in_interval (SML)}
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   273
\<close>
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   274
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   275
text \<open>
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   276
  \noindent The attentive reader may ask how we assert that no
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   277
  generated code will accidentally overwrite.  For this reason the
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   278
  serialiser has an internal table of identifiers which have to be
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   279
  avoided to be used for new declarations.  Initially, this table
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   280
  typically contains the keywords of the target language.  It can be
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   281
  extended manually, thus avoiding accidental overwrites, using the
38505
2f8699695cf6 use command_def vs. command more consciously
haftmann
parents: 38450
diff changeset
   282
  @{command_def "code_reserved"} command:
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   283
\<close>
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
   284
40351
090dac52cfd7 SMLdummy target
haftmann
parents: 39745
diff changeset
   285
code_reserved %quote "\<SMLdummy>" bool true false andalso
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
   286
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   287
text \<open>
28447
haftmann
parents: 28428
diff changeset
   288
  \noindent Next, we try to map HOL pairs to SML pairs, using the
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   289
  infix ``@{verbatim "*"}'' type constructor and parentheses:
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   290
\<close>
28447
haftmann
parents: 28428
diff changeset
   291
(*<*)
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   292
code_printing %invisible
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   293
  type_constructor prod \<rightharpoonup> (SML)
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   294
| constant Pair \<rightharpoonup> (SML)
28447
haftmann
parents: 28428
diff changeset
   295
(*>*)
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   296
code_printing %quotett
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   297
  type_constructor prod \<rightharpoonup> (SML) infix 2 "*"
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   298
| constant Pair \<rightharpoonup> (SML) "!((_),/ (_))"
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   299
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   300
text \<open>
28593
f087237af65d continued codegen tutorial
haftmann
parents: 28564
diff changeset
   301
  \noindent The initial bang ``@{verbatim "!"}'' tells the serialiser
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   302
  never to put parentheses around the whole expression (they are
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   303
  already present), while the parentheses around argument place
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   304
  holders tell not to put parentheses around the arguments.  The slash
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   305
  ``@{verbatim "/"}'' (followed by arbitrary white space) inserts a
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   306
  space which may be used as a break if necessary during pretty
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   307
  printing.
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   308
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   309
  These examples give a glimpse what mechanisms custom serialisations
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   310
  provide; however their usage requires careful thinking in order not
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   311
  to introduce inconsistencies -- or, in other words: custom
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   312
  serialisations are completely axiomatic.
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   313
39643
29cc021398fc corrections and tuning
haftmann
parents: 39063
diff changeset
   314
  A further noteworthy detail is that any special character in a
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   315
  custom serialisation may be quoted using ``@{verbatim "'"}''; thus,
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   316
  in ``@{verbatim "fn '_ => _"}'' the first ``@{verbatim "_"}'' is a
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   317
  proper underscore while the second ``@{verbatim "_"}'' is a
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   318
  placeholder.
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   319
\<close>
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   320
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   321
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   322
subsection \<open>@{text Haskell} serialisation\<close>
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   323
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   324
text \<open>
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   325
  For convenience, the default @{text HOL} setup for @{text Haskell}
39063
5f9692dd621f adapted to change eq -> equal
haftmann
parents: 38506
diff changeset
   326
  maps the @{class equal} class to its counterpart in @{text Haskell},
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   327
  giving custom serialisations for the class @{class equal}
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   328
  and its operation @{const [source] HOL.equal}.
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   329
\<close>
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   330
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   331
code_printing %quotett
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   332
  type_class equal \<rightharpoonup> (Haskell) "Eq"
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   333
| constant HOL.equal \<rightharpoonup> (Haskell) infixl 4 "=="
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   334
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   335
text \<open>
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   336
  \noindent A problem now occurs whenever a type which is an instance
39063
5f9692dd621f adapted to change eq -> equal
haftmann
parents: 38506
diff changeset
   337
  of @{class equal} in @{text HOL} is mapped on a @{text
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   338
  Haskell}-built-in type which is also an instance of @{text Haskell}
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   339
  @{text Eq}:
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   340
\<close>
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   341
28564
haftmann
parents: 28561
diff changeset
   342
typedecl %quote bar
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   343
39063
5f9692dd621f adapted to change eq -> equal
haftmann
parents: 38506
diff changeset
   344
instantiation %quote bar :: equal
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   345
begin
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   346
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60768
diff changeset
   347
definition %quote "HOL.equal (x::bar) y \<longleftrightarrow> x = y"
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   348
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 61076
diff changeset
   349
instance %quote by standard (simp add: equal_bar_def)
28213
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents:
diff changeset
   350
30880
257cbe43faa8 tuned manual
haftmann
parents: 30836
diff changeset
   351
end %quote (*<*)
257cbe43faa8 tuned manual
haftmann
parents: 30836
diff changeset
   352
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   353
(*>*) code_printing %quotett
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   354
  type_constructor bar \<rightharpoonup> (Haskell) "Integer"
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   355
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   356
text \<open>
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   357
  \noindent The code generator would produce an additional instance,
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   358
  which of course is rejected by the @{text Haskell} compiler.  To
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   359
  suppress this additional instance:
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   360
\<close>
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   361
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   362
code_printing %quotett
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   363
  class_instance bar :: "HOL.equal" \<rightharpoonup> (Haskell) -
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   364
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
   365
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   366
subsection \<open>Enhancing the target language context \label{sec:include}\<close>
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
   367
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   368
text \<open>
28593
f087237af65d continued codegen tutorial
haftmann
parents: 28564
diff changeset
   369
  In rare cases it is necessary to \emph{enrich} the context of a
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   370
  target language; this can also be accomplished using the @{command
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   371
  "code_printing"} command:
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   372
\<close>
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
   373
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   374
code_printing %quotett
59379
haftmann
parents: 59377
diff changeset
   375
  code_module "Errno" \<rightharpoonup> (Haskell)
haftmann
parents: 59377
diff changeset
   376
    \<open>errno i = error ("Error number: " ++ show i)\<close>
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
   377
39745
3aa2bc9c5478 combine quote and typewriter/tt tag
haftmann
parents: 39711
diff changeset
   378
code_reserved %quotett Haskell Errno
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
   379
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   380
text \<open>
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   381
  \noindent Such named modules are then prepended to every
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   382
  generated code.  Inspect such code in order to find out how
52378
08dbf9ff2140 documentation on code_printing and code_identifier
haftmann
parents: 51172
diff changeset
   383
  this behaves with respect to a particular
38450
ada5814c9d87 tuned whitespace
haftmann
parents: 37836
diff changeset
   384
  target language.
59377
056945909f60 modernized cartouches
haftmann
parents: 59104
diff changeset
   385
\<close>
28561
056255ade52a some adaption
haftmann
parents: 28456
diff changeset
   386
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
   387
end
46519
17dde5feea4b clarified
haftmann
parents: 40351
diff changeset
   388