doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy
author haftmann
Tue Sep 30 11:19:47 2008 +0200 (2008-09-30)
changeset 28419 f65e8b318581
parent 28213 b52f9205a02d
child 28420 293b166c45c5
permissions -rw-r--r--
re-canibalised manual
haftmann@28213
     1
theory Adaption
haftmann@28213
     2
imports Setup
haftmann@28213
     3
begin
haftmann@28213
     4
haftmann@28419
     5
section {* Adaption to target languages \label{sec:adaption} *}
haftmann@28419
     6
haftmann@28419
     7
subsection {* Common adaption cases *}
haftmann@28419
     8
haftmann@28419
     9
text {*
haftmann@28419
    10
  The @{text HOL} @{text Main} theory already provides a code
haftmann@28419
    11
  generator setup
haftmann@28419
    12
  which should be suitable for most applications. Common extensions
haftmann@28419
    13
  and modifications are available by certain theories of the @{text HOL}
haftmann@28419
    14
  library; beside being useful in applications, they may serve
haftmann@28419
    15
  as a tutorial for customising the code generator setup (see below
haftmann@28419
    16
  \secref{sec:adaption_mechanisms}).
haftmann@28419
    17
haftmann@28419
    18
  \begin{description}
haftmann@28419
    19
haftmann@28419
    20
    \item[@{theory "Code_Integer"}] represents @{text HOL} integers by big
haftmann@28419
    21
       integer literals in target languages.
haftmann@28419
    22
    \item[@{theory "Code_Char"}] represents @{text HOL} characters by 
haftmann@28419
    23
       character literals in target languages.
haftmann@28419
    24
    \item[@{theory "Code_Char_chr"}] like @{text "Code_Char"},
haftmann@28419
    25
       but also offers treatment of character codes; includes
haftmann@28419
    26
       @{theory "Code_Char_chr"}.
haftmann@28419
    27
    \item[@{theory "Efficient_Nat"}] \label{eff_nat} implements natural numbers by integers,
haftmann@28419
    28
       which in general will result in higher efficiency; pattern
haftmann@28419
    29
       matching with @{term "0\<Colon>nat"} / @{const "Suc"}
haftmann@28419
    30
       is eliminated;  includes @{theory "Code_Integer"}.
haftmann@28419
    31
    \item[@{theory "Code_Index"}] provides an additional datatype
haftmann@28419
    32
       @{typ index} which is mapped to target-language built-in integers.
haftmann@28419
    33
       Useful for code setups which involve e.g. indexing of
haftmann@28419
    34
       target-language arrays.
haftmann@28419
    35
    \item[@{theory "Code_Message"}] provides an additional datatype
haftmann@28419
    36
       @{typ message_string} which is isomorphic to strings;
haftmann@28419
    37
       @{typ message_string}s are mapped to target-language strings.
haftmann@28419
    38
       Useful for code setups which involve e.g. printing (error) messages.
haftmann@28419
    39
haftmann@28419
    40
  \end{description}
haftmann@28419
    41
haftmann@28419
    42
  \begin{warn}
haftmann@28419
    43
    When importing any of these theories, they should form the last
haftmann@28419
    44
    items in an import list.  Since these theories adapt the
haftmann@28419
    45
    code generator setup in a non-conservative fashion,
haftmann@28419
    46
    strange effects may occur otherwise.
haftmann@28419
    47
  \end{warn}
haftmann@28419
    48
*}
haftmann@28419
    49
haftmann@28419
    50
haftmann@28419
    51
subsection {* Adaption mechanisms \label{sec:adaption_mechanisms} *}
haftmann@28419
    52
haftmann@28419
    53
text {*
haftmann@28419
    54
  \begin{warn}
haftmann@28419
    55
    The mechanisms shown here are especially for the curious;  the user
haftmann@28419
    56
    rarely needs to do anything on his own beyond the defaults in @{text HOL}.
haftmann@28419
    57
    Adaption is a delicated task which requires a lot of dilligence since
haftmann@28419
    58
    it happend \emph{completely} outside the logic.
haftmann@28419
    59
  \end{warn}
haftmann@28419
    60
*}
haftmann@28419
    61
haftmann@28419
    62
text {*
haftmann@28419
    63
  Consider the following function and its corresponding
haftmann@28419
    64
  SML code:
haftmann@28419
    65
*}
haftmann@28419
    66
haftmann@28419
    67
primrec %quoteme in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
haftmann@28419
    68
  "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
haftmann@28419
    69
haftmann@28419
    70
code_type %invisible bool
haftmann@28419
    71
  (SML)
haftmann@28419
    72
code_const %invisible True and False and "op \<and>" and Not
haftmann@28419
    73
  (SML and and and)
haftmann@28419
    74
haftmann@28419
    75
text %quoteme {*@{code_stmts in_interval (SML)}*}
haftmann@28419
    76
haftmann@28419
    77
text {*
haftmann@28419
    78
  \noindent Though this is correct code, it is a little bit unsatisfactory:
haftmann@28419
    79
  boolean values and operators are materialised as distinguished
haftmann@28419
    80
  entities with have nothing to do with the SML-built-in notion
haftmann@28419
    81
  of \qt{bool}.  This results in less readable code;
haftmann@28419
    82
  additionally, eager evaluation may cause programs to
haftmann@28419
    83
  loop or break which would perfectly terminate when
haftmann@28419
    84
  the existing SML @{verbatim "bool"} would be used.  To map
haftmann@28419
    85
  the HOL @{typ bool} on SML @{verbatim "bool"}, we may use
haftmann@28419
    86
  \qn{custom serialisations}:
haftmann@28419
    87
*}
haftmann@28419
    88
haftmann@28419
    89
code_type %tt bool
haftmann@28419
    90
  (SML "bool")
haftmann@28419
    91
code_const %tt True and False and "op \<and>"
haftmann@28419
    92
  (SML "true" and "false" and "_ andalso _")
haftmann@28213
    93
haftmann@28419
    94
text {*
haftmann@28419
    95
  The @{command code_type} command takes a type constructor
haftmann@28419
    96
  as arguments together with a list of custom serialisations.
haftmann@28419
    97
  Each custom serialisation starts with a target language
haftmann@28419
    98
  identifier followed by an expression, which during
haftmann@28419
    99
  code serialisation is inserted whenever the type constructor
haftmann@28419
   100
  would occur.  For constants, @{command code_const} implements
haftmann@28419
   101
  the corresponding mechanism.  Each ``@{verbatim "_"}'' in
haftmann@28419
   102
  a serialisation expression is treated as a placeholder
haftmann@28419
   103
  for the type constructor's (the constant's) arguments.
haftmann@28419
   104
*}
haftmann@28419
   105
haftmann@28419
   106
text %quoteme {*@{code_stmts in_interval (SML)}*}
haftmann@28419
   107
haftmann@28419
   108
text {*
haftmann@28419
   109
  \lstsml{Thy/examples/bool_mlbool.ML}
haftmann@28419
   110
haftmann@28419
   111
  \noindent This still is not perfect: the parentheses
haftmann@28419
   112
  around the \qt{andalso} expression are superfluous.
haftmann@28419
   113
  Though the serializer
haftmann@28419
   114
  by no means attempts to imitate the rich Isabelle syntax
haftmann@28419
   115
  framework, it provides some common idioms, notably
haftmann@28419
   116
  associative infixes with precedences which may be used here:
haftmann@28419
   117
*}
haftmann@28419
   118
haftmann@28419
   119
code_const %tt "op \<and>"
haftmann@28419
   120
  (SML infixl 1 "andalso")
haftmann@28419
   121
haftmann@28419
   122
text %quoteme {*@{code_stmts in_interval (SML)}*}
haftmann@28419
   123
haftmann@28419
   124
text {*
haftmann@28419
   125
  Next, we try to map HOL pairs to SML pairs, using the
haftmann@28419
   126
  infix ``@{verbatim "*"}'' type constructor and parentheses:
haftmann@28419
   127
*}
haftmann@28419
   128
haftmann@28419
   129
code_type %invisible *
haftmann@28419
   130
  (SML)
haftmann@28419
   131
code_const %invisible Pair
haftmann@28419
   132
  (SML)
haftmann@28419
   133
haftmann@28419
   134
code_type %tt *
haftmann@28419
   135
  (SML infix 2 "*")
haftmann@28419
   136
code_const %tt Pair
haftmann@28419
   137
  (SML "!((_),/ (_))")
haftmann@28419
   138
haftmann@28419
   139
text {*
haftmann@28419
   140
  The initial bang ``@{verbatim "!"}'' tells the serializer to never put
haftmann@28419
   141
  parentheses around the whole expression (they are already present),
haftmann@28419
   142
  while the parentheses around argument place holders
haftmann@28419
   143
  tell not to put parentheses around the arguments.
haftmann@28419
   144
  The slash ``@{verbatim "/"}'' (followed by arbitrary white space)
haftmann@28419
   145
  inserts a space which may be used as a break if necessary
haftmann@28419
   146
  during pretty printing.
haftmann@28419
   147
haftmann@28419
   148
  These examples give a glimpse what mechanisms
haftmann@28419
   149
  custom serialisations provide; however their usage
haftmann@28419
   150
  requires careful thinking in order not to introduce
haftmann@28419
   151
  inconsistencies -- or, in other words:
haftmann@28419
   152
  custom serialisations are completely axiomatic.
haftmann@28419
   153
haftmann@28419
   154
  A further noteworthy details is that any special
haftmann@28419
   155
  character in a custom serialisation may be quoted
haftmann@28419
   156
  using ``@{verbatim "'"}''; thus, in
haftmann@28419
   157
  ``@{verbatim "fn '_ => _"}'' the first
haftmann@28419
   158
  ``@{verbatim "_"}'' is a proper underscore while the
haftmann@28419
   159
  second ``@{verbatim "_"}'' is a placeholder.
haftmann@28419
   160
haftmann@28419
   161
  The HOL theories provide further
haftmann@28419
   162
  examples for custom serialisations.
haftmann@28419
   163
*}
haftmann@28419
   164
haftmann@28419
   165
haftmann@28419
   166
subsection {* @{text Haskell} serialisation *}
haftmann@28419
   167
haftmann@28419
   168
text {*
haftmann@28419
   169
  For convenience, the default
haftmann@28419
   170
  @{text HOL} setup for @{text Haskell} maps the @{class eq} class to
haftmann@28419
   171
  its counterpart in @{text Haskell}, giving custom serialisations
haftmann@28419
   172
  for the class @{class eq} (by command @{command code_class}) and its operation
haftmann@28419
   173
  @{const HOL.eq}
haftmann@28419
   174
*}
haftmann@28419
   175
haftmann@28419
   176
code_class %tt eq
haftmann@28419
   177
  (Haskell "Eq" where "HOL.eq" \<equiv> "(==)")
haftmann@28419
   178
haftmann@28419
   179
code_const %tt "op ="
haftmann@28419
   180
  (Haskell infixl 4 "==")
haftmann@28419
   181
haftmann@28419
   182
text {*
haftmann@28419
   183
  A problem now occurs whenever a type which
haftmann@28419
   184
  is an instance of @{class eq} in @{text HOL} is mapped
haftmann@28419
   185
  on a @{text Haskell}-built-in type which is also an instance
haftmann@28419
   186
  of @{text Haskell} @{text Eq}:
haftmann@28419
   187
*}
haftmann@28419
   188
haftmann@28419
   189
typedecl %quoteme bar
haftmann@28419
   190
haftmann@28419
   191
instantiation %quoteme bar :: eq
haftmann@28419
   192
begin
haftmann@28419
   193
haftmann@28419
   194
definition %quoteme "eq_class.eq (x\<Colon>bar) y \<longleftrightarrow> x = y"
haftmann@28419
   195
haftmann@28419
   196
instance %quoteme by default (simp add: eq_bar_def)
haftmann@28213
   197
haftmann@28213
   198
end
haftmann@28419
   199
haftmann@28419
   200
code_type %tt bar
haftmann@28419
   201
  (Haskell "Integer")
haftmann@28419
   202
haftmann@28419
   203
text {*
haftmann@28419
   204
  The code generator would produce
haftmann@28419
   205
  an additional instance, which of course is rejectedby the @{text Haskell}
haftmann@28419
   206
  compiler.
haftmann@28419
   207
  To suppress this additional instance, use
haftmann@28419
   208
  @{text "code_instance"}:
haftmann@28419
   209
*}
haftmann@28419
   210
haftmann@28419
   211
code_instance %tt bar :: eq
haftmann@28419
   212
  (Haskell -)
haftmann@28419
   213
haftmann@28419
   214
end