doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
author haftmann
Tue, 07 Nov 2006 15:07:02 +0100
changeset 21223 b3bdc1abc7d3
parent 21222 6dfdb69e83ef
child 21323 74ab7c0980c7
permissions -rw-r--r--
some corrections
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     1
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     2
(* $Id$ *)
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     3
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
     4
(*<*)
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     5
theory Codegen
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     6
imports Main
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
     7
uses "../../../IsarImplementation/Thy/setup.ML"
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     8
begin
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     9
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
    10
ML {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
    11
CodegenSerializer.sml_code_width := 74;
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
    12
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
    13
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
    14
(*>*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
    15
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    16
chapter {* Code generation from Isabelle theories *}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    17
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    18
section {* Introduction *}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    19
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    20
subsection {* Motivation *}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    21
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    22
text {*
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    23
  Executing formal specifications as programs is a well-established
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    24
  topic in the theorem proving community.  With increasing
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    25
  application of theorem proving systems in the area of
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    26
  software development and verification, its relevance manifests
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    27
  for running test cases and rapid prototyping.  In logical
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    28
  calculi like constructive type theory,
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    29
  a notion of executability is implicit due to the nature
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    30
  of the calculus.  In contrast, specifications in Isabelle/HOL
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    31
  can be highly non-executable.  In order to bridge
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    32
  the gap between logic and executable specifications,
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    33
  an explicit non-trivial transformation has to be applied:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    34
  code generation.
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    35
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    36
  This tutorial introduces a generic code generator for the
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    37
  Isabelle system \cite{isa-tutorial}.
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    38
  Generic in the sense that the
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    39
  \qn{target language} for which code shall ultimately be
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    40
  generated is not fixed but may be an arbitrary state-of-the-art
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    41
  functional programming language (currently, the implementation
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    42
  supports SML \cite{web:sml} and Haskell \cite{web:haskell}).
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    43
  We aim to provide a
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    44
  versatile environment
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    45
  suitable for software development and verification,
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    46
  structuring the process
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    47
  of code generation into a small set of orthogonal principles
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    48
  while achieving a big coverage of application areas
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    49
  with maximum flexibility.
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
    50
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
    51
  For readers, some familiarity and experience
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
    52
  with the the ingredients
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
    53
  of the HOL \emph{Main} theory is assumed.
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    54
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    55
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    56
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    57
subsection {* Overview *}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    58
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    59
text {*
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    60
  The code generator aims to be usable with no further ado
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    61
  in most cases while allowing for detailed customization.
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    62
  This manifests in the structure of this tutorial: this introduction
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
    63
  continues with a short introduction of concepts.  Section
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
    64
  \secref{sec:basics} explains how to use the framework naively,
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    65
  presuming a reasonable default setup.  Then, section
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    66
  \secref{sec:advanced} deals with advanced topics,
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    67
  introducing further aspects of the code generator framework
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    68
  in a motivation-driven manner.  Last, section \secref{sec:ml}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    69
  introduces the framework's internal programming interfaces.
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    70
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    71
  \begin{warn}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    72
    Ultimately, the code generator which this tutorial deals with
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    73
    is supposed to replace the already established code generator
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    74
    by Stefan Berghofer \cite{Berghofer-Nipkow:2002}.
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
    75
    So, for the moment, there are two distinct code generators
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    76
    in Isabelle.
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    77
    Also note that while the framework itself is largely
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    78
    object-logic independent, only HOL provides a reasonable
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    79
    framework setup.    
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    80
  \end{warn}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    81
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    82
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    83
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    84
subsection {* Code generation process *}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    85
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    86
text {*
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
    87
  \begin{figure}[h]
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
    88
  \centering
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
    89
  \includegraphics[width=0.7\textwidth]{codegen_process}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
    90
  \caption{code generator -- processing overview}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
    91
  \label{fig:process}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
    92
  \end{figure}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
    93
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    94
  The code generator employs a notion of executability
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    95
  for three foundational executable ingredients known
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    96
  from functional programming:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    97
  \emph{function equations}, \emph{datatypes}, and
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    98
  \emph{type classes}. A function equation as a first approximation
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
    99
  is a theorem of the form @{text "f t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n \<equiv> t"}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   100
  (an equation headed by a constant @{text f} with arguments
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   101
  @{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right hand side @{text t}.
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   102
  Code generation aims to turn function equations
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   103
  into a functional program by running through
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   104
  a process (see figure \ref{fig:process}):
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   105
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   106
  \begin{itemize}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   107
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   108
    \item Out of the vast collection of theorems proven in a
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   109
      \qn{theory}, a reasonable subset modeling
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   110
      function equations is \qn{selected}.
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   111
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   112
    \item On those selected theorems, certain
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   113
      transformations are carried out
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   114
      (\qn{preprocessing}).  Their purpose is to turn theorems
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   115
      representing non- or badly executable
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   116
      specifications into equivalent but executable counterparts.
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   117
      The result is a structured collection of \qn{code theorems}.
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   118
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   119
    \item These \qn{code theorems} then are extracted
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   120
      into an Haskell-like intermediate
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   121
      language.
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   122
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   123
    \item Finally, out of the intermediate language the final
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   124
      code in the desired \qn{target language} is \qn{serialized}.
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   125
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   126
  \end{itemize}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   127
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   128
  From these steps, only the two last are carried out
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   129
  outside the logic; by keeping this layer as
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   130
  thin as possible, the amount of code to trust is
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   131
  kept to a minimum.
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   132
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   133
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   134
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   135
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   136
section {* Basics \label{sec:basics} *}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
   137
9b9910b82645 initial draft
haftmann
parents:
diff changeset
   138
subsection {* Invoking the code generator *}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
   139
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   140
text {*
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   141
  Thanks to a reasonable setup of the HOL theories, in
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   142
  most cases code generation proceeds without further ado:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   143
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   144
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   145
consts
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   146
  fac :: "nat \<Rightarrow> nat"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   147
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   148
primrec
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   149
  "fac 0 = 1"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   150
  "fac (Suc n) = Suc n * fac n"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   151
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   152
text {*
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   153
  This executable specification is now turned to SML code:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   154
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   155
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   156
code_gen fac (SML "examples/fac.ML")
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   157
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   158
text {*
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   159
  The \isasymCODEGEN command takes a space-separated list of
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   160
  constants together with \qn{serialization directives}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   161
  in parentheses. These start with a \qn{target language}
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   162
  identifier, followed by arguments, their semantics
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   163
  depending on the target. In the SML case, a filename
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   164
  is given where to write the generated code to.
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   165
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   166
  Internally, the function equations for all selected
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   167
  constants are taken, including any transitively required
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   168
  constants, datatypes and classes, resulting in the following
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   169
  code:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   170
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   171
  \lstsml{Thy/examples/fac.ML}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   172
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   173
  The code generator will complain when a required
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   174
  ingredient does not provide a executable counterpart.
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   175
  This is the case if an involved type is not a datatype:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   176
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   177
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   178
(*<*)
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   179
setup {* Sign.add_path "foo" *}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   180
(*>*)
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   181
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   182
typedecl 'a foo
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   183
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   184
definition
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   185
  bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   186
  "bar x y = y"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   187
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   188
(*<*)
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   189
hide type foo
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   190
hide const bar
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   191
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   192
setup {* Sign.parent_path *}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   193
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   194
datatype 'a foo = Foo
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   195
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   196
definition
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   197
  bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   198
  "bar x y = y"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   199
(*>*)
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   200
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   201
code_gen bar (SML "examples/fail_type.ML")
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   202
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   203
text {*
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   204
  \noindent will result in an error. Likewise, generating code
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   205
  for constants not yielding
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   206
  a function equation will fail, e.g.~the Hilbert choice
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   207
  operation @{text "SOME"}:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   208
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   209
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   210
(*<*)
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   211
setup {* Sign.add_path "foo" *}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   212
(*>*)
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   213
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   214
definition
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   215
  pick_some :: "'a list \<Rightarrow> 'a"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   216
  "pick_some xs = (SOME x. x \<in> set xs)"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   217
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   218
(*<*)
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   219
hide const pick_some
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   220
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   221
setup {* Sign.parent_path *}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   222
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   223
definition
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   224
  pick_some :: "'a list \<Rightarrow> 'a"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   225
  "pick_some = hd"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   226
(*>*)
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   227
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   228
code_gen pick_some (SML "examples/fail_const.ML")
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   229
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
   230
subsection {* Theorem selection *}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
   231
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   232
text {*
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   233
  The list of all function equations in a theory may be inspected
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   234
  using the \isasymPRINTCODETHMS command:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   235
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   236
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   237
print_codethms
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   238
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   239
text {*
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   240
  \noindent which displays a table of constant with corresponding
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   241
  function equations (the additional stuff displayed
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   242
  shall not bother us for the moment). If this table does
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   243
  not provide at least one function
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   244
  equation, the table of primitive definitions is searched
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   245
  whether it provides one.
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   246
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   247
  The typical HOL tools are already set up in a way that
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   248
  function definitions introduced by \isasymFUN, \isasymFUNCTION,
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   249
  \isasymPRIMREC, \isasymRECDEF are implicitly propagated
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   250
  to this function equation table. Specific theorems may be
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   251
  selected using an attribute: \emph{code func}. As example,
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   252
  a weight selector function:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   253
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   254
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   255
consts
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   256
  pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   257
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   258
primrec
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   259
  "pick (x#xs) n = (let (k, v) = x in
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   260
    if n < k then v else pick xs (n - k))"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   261
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   262
text {*
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   263
  We want to eliminate the explicit destruction
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   264
  of @{term x} to @{term "(k, v)"}:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   265
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   266
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   267
lemma [code func]:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   268
  "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   269
  by simp
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   270
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   271
code_gen pick (SML "examples/pick1.ML")
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   272
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   273
text {*
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   274
  This theorem is now added to the function equation table:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   275
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   276
  \lstsml{Thy/examples/pick1.ML}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   277
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   278
  It might be convenient to remove the pointless original
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   279
  equation, using the \emph{nofunc} attribute:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   280
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   281
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   282
lemmas [code nofunc] = pick.simps 
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   283
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   284
code_gen pick (SML "examples/pick2.ML")
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   285
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   286
text {*
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   287
  \lstsml{Thy/examples/pick2.ML}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   288
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   289
  Syntactic redundancies are implicitly dropped. For example,
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   290
  using a modified version of the @{const fac} function
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   291
  as function equation, the then redundant (since
21075
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   292
  syntactically subsumed) original function equations
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   293
  are dropped, resulting in a warning:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   294
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   295
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   296
lemma [code func]:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   297
  "fac n = (case n of 0 \<Rightarrow> 1 | Suc m \<Rightarrow> n * fac m)"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   298
  by (cases n) simp_all
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   299
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   300
code_gen fac (SML "examples/fac_case.ML")
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   301
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   302
text {*
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   303
  \lstsml{Thy/examples/fac_case.ML}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   304
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   305
  \begin{warn}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   306
    Some statements in this section have to be treated with some
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   307
    caution. First, since the HOL function package is still
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   308
    under development, its setup with respect to code generation
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   309
    may differ from what is presumed here.
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   310
    Further, the attributes \emph{code} and \emph{code del}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   311
    associated with the existing code generator also apply to
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   312
    the new one: \emph{code} implies \emph{code func},
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   313
    and \emph{code del} implies \emph{code nofunc}.
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   314
  \end{warn}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   315
*}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
   316
9b9910b82645 initial draft
haftmann
parents:
diff changeset
   317
subsection {* Type classes *}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
   318
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   319
text {*
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   320
  Type classes enter the game via the Isar class package.
21075
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   321
  For a short introduction how to use it, see \cite{isabelle-classes};
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   322
  here we just illustrate its impact on code generation.
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   323
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   324
  In a target language, type classes may be represented
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   325
  natively (as in the case of Haskell). For languages
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   326
  like SML, they are implemented using \emph{dictionaries}.
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   327
  Our following example specifies a class \qt{null},
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   328
  assigning to each of its inhabitants a \qt{null} value:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   329
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   330
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   331
class null =
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   332
  fixes null :: 'a
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   333
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   334
consts
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   335
  head :: "'a\<Colon>null list \<Rightarrow> 'a"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   336
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   337
primrec
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   338
  "head [] = null"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   339
  "head (x#xs) = x"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   340
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   341
text {*
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   342
  We provide some instances for our @{text null}:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   343
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   344
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   345
instance option :: (type) null
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   346
  "null \<equiv> None" ..
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   347
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   348
instance list :: (type) null
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   349
  "null \<equiv> []" ..
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   350
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   351
text {*
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   352
  Constructing a dummy example:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   353
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   354
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   355
definition
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   356
  "dummy = head [Some (Suc 0), None]"
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   357
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   358
text {*
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   359
  Type classes offer a suitable occasion to introduce
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   360
  the Haskell serializer.  Its usage is almost the same
21075
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   361
  as SML, but, in accordance with conventions
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   362
  some Haskell systems enforce, each module ends
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   363
  up in a single file. The module hierarchy is reflected in
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   364
  the file system, with root given by the user.
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   365
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   366
21075
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   367
code_gen dummy (Haskell "examples/")
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   368
  (* NOTE: you may use Haskell only once in this document, otherwise
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   369
  you have to work in distinct subdirectories *)
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   370
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   371
text {*
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   372
  \lsthaskell{Thy/examples/Codegen.hs}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   373
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   374
  (we have left out all other modules).
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   375
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   376
  The whole code in SML with explicit dictionary passing:
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   377
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   378
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   379
code_gen dummy (SML "examples/class.ML")
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   380
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   381
text {*
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   382
  \lstsml{Thy/examples/class.ML}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   383
*}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   384
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   385
subsection {* Incremental code generation *}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   386
21075
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   387
text {*
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   388
  Code generation is \emph{incremental}: theorems
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   389
  and abstract intermediate code are cached and extended on demand.
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   390
  The cache may be partially or fully dropped if the underlying
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   391
  executable content of the theory changes.
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   392
  Implementation of caching is supposed to transparently
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   393
  hid away the details from the user.  Anyway, caching
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   394
  reaches the surface by using a slightly more general form
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   395
  of the \isasymCODEGEN: either the list of constants or the
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   396
  list of serialization expressions may be dropped.  If no
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   397
  serialization expressions are given, only abstract code
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   398
  is generated and cached; if no constants are given, the
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   399
  current cache is serialized.
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   400
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   401
  For explorative reasons, an extended version of the
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   402
  \isasymCODEGEN command may prove useful:
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   403
*}
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   404
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   405
print_codethms ()
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   406
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   407
text {*
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   408
  \noindent print all cached function equations (i.e.~\emph{after}
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   409
  any applied transformation. Inside the brackets a
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   410
  list of constants may be given; their function
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   411
  equations are added to the cache if not already present.
21075
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   412
*}
d6742ff3b522 continued
haftmann
parents: 21058
diff changeset
   413
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   414
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   415
section {* Recipes and advanced topics \label{sec:advanced} *}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   416
21089
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   417
text {*
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   418
  In this tutorial, we do not attempt to give an exhaustive
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   419
  description of the code generator framework; instead,
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   420
  we cast a light on advanced topics by introducing
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   421
  them together with practically motivated examples.  Concerning
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   422
  further reading, see
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   423
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   424
  \begin{itemize}
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   425
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   426
  \item the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   427
    for exhaustive syntax diagrams.
21222
6dfdb69e83ef adjusted title
haftmann
parents: 21217
diff changeset
   428
  \item or \fixme[ref] which deals with foundational issues
21089
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   429
    of the code generator framework.
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   430
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   431
  \end{itemize}
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   432
*}
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   433
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   434
subsection {* Library theories *}
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   435
21089
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   436
text {*
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   437
  The HOL \emph{Main} theory already provides a code generator setup
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   438
  which should be suitable for most applications. Common extensions
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   439
  and modifications are available by certain theories of the HOL
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   440
  library; beside being useful in applications, they may serve
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   441
  as a tutorial for customizing the code generator setup.
21089
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   442
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   443
  \begin{description}
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   444
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   445
    \item[ExecutableSet] allows to generate code
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   446
       for finite sets using lists.
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   447
    \item[ExecutableRat] \label{exec_rat} implements rational
21089
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   448
       numbers as triples @{text "(sign, enumerator, denominator)"}.
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   449
    \item[EfficientNat] \label{eff_nat} implements natural numbers by integers,
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   450
       which in general will result in higher efficency; pattern
21089
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   451
       matching with @{const "0\<Colon>nat"} / @{const "Suc"}
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   452
       is eliminated.
21089
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   453
    \item[MLString] provides an additional datatype @{text "mlstring"};
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   454
       in the HOL default setup, strings in HOL are mapped to list
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   455
       of chars in SML; values of type @{text "mlstring"} are
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   456
       mapped to strings in SML.
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   457
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   458
  \end{description}
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   459
*}
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   460
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
   461
subsection {* Preprocessing *}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
   462
21089
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   463
text {*
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   464
  Before selected function theorems are turned into abstract
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   465
  code, a chain of definitional transformation steps is carried
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   466
  out: \emph{preprocessing}. There are three possibilities
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   467
  to customize preprocessing: \emph{inline theorems},
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   468
  \emph{inline procedures} and \emph{generic preprocessors}.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   469
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   470
  \emph{Inline theorems} are rewriting rules applied to each
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   471
  function equation.  Due to the interpretation of theorems
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   472
  of function equations, rewrites are applied to the right
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   473
  hand side and the arguments of the left hand side of an
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   474
  equation, but never to the constant heading the left hand side.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   475
  Inline theorems may be declared an undeclared using the
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   476
  \emph{code inline} or \emph{code noinline} attribute respectively.
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   477
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   478
  Some common applications:
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   479
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   480
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   481
text_raw {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   482
  \begin{itemize}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   483
     \item replacing non-executable constructs by executable ones: \\
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   484
*}     
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   485
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   486
lemma [code inline]:
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   487
  "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   488
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   489
text_raw {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   490
     \item eliminating superfluous constants: \\
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   491
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   492
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   493
lemma [code inline]:
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   494
  "1 = Suc 0" by simp
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   495
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   496
text_raw {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   497
     \item replacing executable but inconvenient constructs: \\
21089
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   498
*}
cf6defa31209 continued
haftmann
parents: 21075
diff changeset
   499
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   500
lemma [code inline]:
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   501
  "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   502
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   503
text_raw {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   504
  \end{itemize}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   505
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   506
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   507
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   508
  The current set of inline theorems may be inspected using
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   509
  the \isasymPRINTCODETHMS command.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   510
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   511
  \emph{Inline procedures} are a generalized version of inline
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   512
  theorems written in ML -- rewrite rules are generated dependent
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   513
  on the function theorems for a certain function.  One
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   514
  application is the implicit expanding of @{typ nat} numerals
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   515
  to @{const "0\<Colon>nat"} / @{const Suc} representation.  See further
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   516
  \secref{sec:ml}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   517
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   518
  \emph{Generic preprocessors} provide a most general interface,
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   519
  transforming a list of function theorems to another
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   520
  list of function theorems, provided that neither the heading
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   521
  constant nor its type change.  The @{const "0\<Colon>nat"} / @{const Suc}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   522
  pattern elimination implemented in \secref{eff_nat} uses this
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   523
  interface.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   524
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   525
  \begin{warn}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   526
    The order in which single preprocessing steps are carried
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   527
    out currently is not specified; in particular, preprocessing
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   528
    is \emph{no} fix point process.  Keep this in mind when
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   529
    setting up the preprocessor.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   530
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   531
    Further, the attribute \emph{code unfold}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   532
    associated with the existing code generator also applies to
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   533
    the new one: \emph{code unfold} implies \emph{code inline}.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   534
  \end{warn}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   535
*}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
   536
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
   537
subsection {* Customizing serialization  *}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
   538
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   539
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   540
  Consider the following function and its corresponding
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   541
  SML code:
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   542
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   543
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   544
fun
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   545
  in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   546
  "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   547
termination by (auto_term "{}")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   548
(*<*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   549
declare in_interval.simps [code func]
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   550
(*>*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   551
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   552
(*<*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   553
code_type bool
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   554
  (SML)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   555
code_const True and False and "op \<and>" and Not
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   556
  (SML and and and)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   557
(*>*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   558
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   559
code_gen in_interval (SML "examples/bool1.ML")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   560
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   561
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   562
  \lstsml{Thy/examples/bool1.ML}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   563
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   564
  Though this is correct code, it is a little bit unsatisfactory:
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   565
  boolean values and operators are materialized as distinguished
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   566
  entities with have nothing to do with the SML-builtin notion
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   567
  of \qt{bool}.  This results in less readable code;
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   568
  additionally, eager evaluation may cause programs to
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   569
  loop or break which would perfectly terminate when
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   570
  the existing SML \qt{bool} would be used.  To map
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   571
  the HOL \qt{bool} on SML \qt{bool}, we may use
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   572
  \qn{custom serializations}:
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   573
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   574
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   575
code_type bool
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   576
  (SML "bool")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   577
code_const True and False and "op \<and>"
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   578
  (SML "true" and "false" and "_ andalso _")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   579
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   580
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   581
  The \isasymCODETYPE commad takes a type constructor
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   582
  as arguments together with a list of custom serializations.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   583
  Each custom serialization starts with a target language
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   584
  identifier followed by an expression, which during
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   585
  code serialization is inserted whenever the type constructor
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   586
  would occur.  For constants, \isasymCODECONST implements
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   587
  the corresponding mechanism.  Each \qt{\_} in
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   588
  a serialization expression is treated as a placeholder
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   589
  for the type constructor's (the constant's) arguments.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   590
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   591
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   592
code_reserved SML
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   593
  bool true false
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   594
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   595
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   596
  To assert that the existing \qt{bool}, \qt{true} and \qt{false}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   597
  is not used for generated code, we use \isasymCODERESERVED.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   598
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   599
  After this setup, code looks quite more readable:
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   600
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   601
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   602
code_gen in_interval (SML "examples/bool2.ML")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   603
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   604
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   605
  \lstsml{Thy/examples/bool2.ML}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   606
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   607
  This still is not perfect: the parentheses
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   608
  around \qt{andalso} are superfluous.  Though the serializer
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   609
  by no means attempts to imitate the rich Isabelle syntax
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   610
  framework, it provides some common idioms, notably
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   611
  associative infixes with precedences which may be used here:
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   612
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   613
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   614
code_const "op \<and>"
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   615
  (SML infixl 1 "andalso")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   616
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   617
code_gen in_interval (SML "examples/bool3.ML")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   618
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   619
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   620
  \lstsml{Thy/examples/bool3.ML}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   621
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   622
  Next, we try to map HOL pairs to SML pairs, using the
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   623
  infix \qt{ * } type constructor and parentheses:
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   624
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   625
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   626
(*<*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   627
code_type *
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   628
  (SML)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   629
code_const Pair
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   630
  (SML)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   631
(*>*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   632
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   633
code_type *
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   634
  (SML infix 2 "*")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   635
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   636
code_const Pair
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   637
  (SML "!((_),/ (_))")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   638
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   639
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   640
  The initial bang \qt{!} tells the serializer to never put
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   641
  parentheses around the whole expression (they are already present),
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   642
  while the parentheses around argument place holders
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   643
  tell not to put parentheses around the arguments.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   644
  The slash \qt{/} (followed by arbitrary white space)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   645
  inserts a space which may be used as a break if necessary
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   646
  during pretty printing.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   647
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   648
  So far, we did only provide more idiomatic serializations for
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   649
  constructs which would be executable on their own.  Target-specific
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   650
  serializations may also be used to \emph{implement} constructs
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   651
  which have no implicit notion of executability.  For example,
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   652
  take the HOL integers:
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   653
*}
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   654
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   655
definition
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   656
  double_inc :: "int \<Rightarrow> int"
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   657
  "double_inc k = 2 * k + 1"
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   658
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   659
code_gen double_inc (SML "examples/integers.ML")
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   660
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   661
text {*
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   662
  will fail: @{typ int} in HOL is implemented using a quotient
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   663
  type, which does not provide any notion of executability.
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   664
  \footnote{Eventually, we also want to provide executability
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   665
  for quotients.}.  However, we could use the SML builtin
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   666
  integers:
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   667
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   668
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   669
code_type int
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   670
  (SML "IntInf.int")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   671
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   672
code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   673
    and "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   674
  (SML "IntInf.+ (_, _)" and "IntInf.* (_, _)")
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   675
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   676
code_gen double_inc (SML "examples/integers.ML")
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   677
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   678
text {*
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   679
  resulting in:
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   680
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   681
  \lstsml{Thy/examples/integers.ML}
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   682
*}
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   683
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   684
text {*
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   685
  These examples give a glimpse what powerful mechanisms
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   686
  custom serializations provide; however their usage
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   687
  requires careful thinking in order not to introduce
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   688
  inconsistencies -- or, in other words:
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   689
  custom serializations are completely axiomatic.
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   690
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   691
  A further noteworthy details is that any special
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   692
  character in a custom serialization may be quoted
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   693
  using \qt{'}; thus, in \qt{fn '\_ => \_} the first
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   694
  \qt{'\_} is a proper underscore while the
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   695
  second \qt{\_} is a placeholder.
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   696
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   697
  The HOL theories provide further
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   698
  examples for custom serializations and form
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   699
  a recommended tutorial on how to use them properly.
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   700
*}
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   701
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   702
subsection {* Concerning operational equality *}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   703
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   704
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   705
  Surely you have already noticed how equality is treated
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   706
  by the code generator:
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   707
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   708
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   709
fun
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   710
  collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   711
  "collect_duplicates xs ys [] = xs"
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   712
  "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   713
    then if z \<in> set ys
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   714
      then collect_duplicates xs ys zs
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   715
      else collect_duplicates xs (z#ys) zs
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   716
    else collect_duplicates (z#xs) (z#ys) zs)"
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   717
termination by (auto_term "measure (length o snd o snd)")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   718
(*<*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   719
lemmas [code func] = collect_duplicates.simps
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   720
(*>*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   721
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   722
text {*
21217
0425fc57510f continued
haftmann
parents: 21189
diff changeset
   723
  The membership test during preprocessing is rewritten,
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   724
  resulting in @{const List.memberl}, which itself
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   725
  performs an explicit equality check.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   726
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   727
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   728
code_gen collect_duplicates (SML "examples/collect_duplicates.ML")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   729
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   730
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   731
  \lstsml{Thy/examples/collect_duplicates.ML}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   732
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   733
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   734
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   735
  Obviously, polymorphic equality is implemented the Haskell
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   736
  way using a type class.  How is this achieved?  By an
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   737
  almost trivial definition in the HOL setup:
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   738
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   739
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   740
(*<*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   741
setup {* Sign.add_path "foo" *}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   742
(*>*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   743
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   744
class eq =
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   745
  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   746
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   747
defs
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   748
  eq (*[symmetric, code inline, code func]*): "eq \<equiv> (op =)"
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   749
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   750
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   751
  This merely introduces a class @{text eq} with corresponding
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   752
  operation @{const eq}, which by definition is isomorphic
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   753
  to @{const "op ="}; the preprocessing framework does the rest.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   754
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   755
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   756
(*<*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   757
lemmas [code noinline] = eq
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   758
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   759
hide (open) "class" eq
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   760
hide (open) const eq
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   761
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   762
lemmas [symmetric, code func] = eq_def
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   763
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   764
setup {* Sign.parent_path *}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   765
(*>*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   766
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   767
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   768
  For datatypes, instances of @{text eq} are implicitly derived
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   769
  when possible.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   770
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   771
  Though this class is designed to get rarely in the way, there
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   772
  are some cases when it suddenly comes to surface:
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   773
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   774
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   775
subsubsection {* code lemmas and customary serializations for equality *}
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   776
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   777
text {*
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   778
  Examine the following:
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   779
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   780
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   781
code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   782
  (SML "!(_ : IntInf.int = _)")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   783
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   784
text {*
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   785
  What is wrong here? Since @{const "op ="} is nothing else then
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   786
  a plain constant, this customary serialization will refer
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   787
  to polymorphic equality @{const "op = \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool"}.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   788
  Instead, we want the specific equality on @{typ int},
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   789
  by using the overloaded constant @{const "Code_Generator.eq"}:
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   790
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   791
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   792
code_const "Code_Generator.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   793
  (SML "!(_ : IntInf.int = _)")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   794
21223
b3bdc1abc7d3 some corrections
haftmann
parents: 21222
diff changeset
   795
subsubsection {* typedecls interpreted by customary serializations *}
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   796
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   797
text {*
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   798
  A common idiom is to use unspecified types for formalizations
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   799
  and interpret them for a specific target language:
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   800
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   801
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   802
typedecl key
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   803
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   804
fun
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   805
  lookup :: "(key \<times> 'a) list \<Rightarrow> key \<Rightarrow> 'a option" where
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   806
  "lookup [] l = None"
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   807
  "lookup ((k, v) # xs) l = (if k = l then Some v else lookup xs l)"
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   808
termination by (auto_term "measure (length o fst)")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   809
(*<*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   810
lemmas [code func] = lookup.simps
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   811
(*>*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   812
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   813
code_type key
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   814
  (SML "string")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   815
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   816
text {*
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   817
  This, though, is not sufficient: @{typ key} is no instance
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   818
  of @{text eq} since @{typ key} is no datatype; the instance
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   819
  has to be declared manually, including a serialization
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   820
  for the particular instance of @{const "Code_Generator.eq"}:
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   821
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   822
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   823
instance key :: eq ..
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   824
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   825
code_const "Code_Generator.eq \<Colon> key \<Rightarrow> key \<Rightarrow> bool"
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   826
  (SML "!(_ : string = _)")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   827
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   828
text {*
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   829
  Then everything goes fine:
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   830
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   831
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   832
code_gen lookup (SML "examples/lookup.ML")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   833
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   834
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   835
  \lstsml{Thy/examples/lookup.ML}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   836
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   837
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   838
subsubsection {* lexicographic orderings and coregularity *}
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   839
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   840
text {*
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   841
  Another subtlety
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   842
  enters the stage when definitions of overloaded constants
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   843
  are dependent on operational equality.  For example, let
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   844
  us define a lexicographic ordering on tuples:
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   845
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   846
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   847
(*<*)
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   848
setup {* Sign.add_path "foobar" *}
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   849
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   850
class eq = fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   851
class ord =
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   852
  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_/ \<^loc>\<le> _)" [50, 51] 50)
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   853
  fixes less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_/ \<^loc>< _)" [50, 51] 50)
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   854
(*>*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   855
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   856
instance * :: (ord, ord) ord
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   857
  "p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   858
    x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   859
  "p1 \<le> p2 \<equiv> p1 < p2 \<or> (p1 \<Colon> 'a\<Colon>ord \<times> 'b\<Colon>ord)  = p2" ..
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   860
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   861
(*<*)
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   862
hide "class" eq ord
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   863
hide const eq less_eq less
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   864
setup {* Sign.parent_path *}
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   865
(*>*)
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   866
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   867
text {*
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   868
  Then code generation will fail.  Why?  The definition
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   869
  of @{const "op \<le>"} depends on equality on both arguments,
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   870
  which are polymorphic and impose an additional @{text eq}
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   871
  class constraint, thus violating the type discipline
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   872
  for class operations.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   873
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   874
  The solution is to add @{text eq} to both sort arguments:
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   875
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   876
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   877
instance * :: ("{eq, ord}", "{eq, ord}") ord
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   878
  "p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>{eq, ord}, y1 \<Colon> 'b\<Colon>{eq, ord}) = p1; (x2, y2) = p2 in
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   879
    x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   880
  "p1 \<le> p2 \<equiv> p1 < p2 \<or> (p1 \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>{eq, ord})  = p2" ..
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   881
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   882
text {*
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   883
  Then code generation succeeds:
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   884
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   885
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   886
code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>{eq, ord} \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   887
  (SML "examples/lexicographic.ML")
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   888
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   889
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   890
  \lstsml{Thy/examples/lexicographic.ML}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   891
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   892
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   893
subsubsection {* Haskell serialization *}
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   894
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   895
text {*
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   896
  For convenience, the default
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   897
  HOL setup for Haskell maps the @{text eq} class to
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   898
  its counterpart in Haskell, giving custom serializations
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   899
  for the class (\isasymCODECLASS) and its operation:
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   900
*}
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   901
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   902
(*<*)
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   903
setup {* Sign.add_path "bar" *}
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   904
class eq = fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   905
(*>*)
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   906
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   907
code_class eq
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   908
  (Haskell "Eq" where eq \<equiv> "(==)")
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   909
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   910
code_const eq
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   911
  (Haskell infixl 4 "==")
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   912
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   913
(*<*)
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   914
hide "class" eq
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   915
hide const eq
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   916
setup {* Sign.parent_path *}
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   917
(*>*)
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   918
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   919
text {*
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   920
  A problem now occurs whenever a type which
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   921
  is an instance of @{text eq} in HOL is mapped
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   922
  on a Haskell-builtin type which is also an instance
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   923
  of Haskell @{text Eq}:
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   924
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   925
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   926
typedecl bar
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   927
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   928
instance bar :: eq ..
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   929
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   930
code_type bar
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   931
  (Haskell "Integer")
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   932
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   933
text {*
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   934
    The code generator would produce
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   935
    an additional instance, which of course is rejected.
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   936
    To suppress this additional instance, use
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   937
    \isasymCODEINSTANCE:
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   938
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
   939
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   940
code_instance bar :: eq
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   941
  (Haskell -)
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   942
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   943
subsection {* Types matter *}
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   944
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   945
text {*
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   946
  Imagine the following quick-and-dirty setup for implementing
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   947
  some kind of sets as lists in SML:
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   948
*}
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   949
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   950
code_type set
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   951
  (SML "_ list")
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   952
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   953
code_const "{}" and insert
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   954
  (SML "![]" and infixl 7 "::")
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   955
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   956
definition
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   957
  dummy_set :: "(nat \<Rightarrow> nat) set"
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   958
  "dummy_set = {Suc}"
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   959
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   960
text {*
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   961
  Then code generation for @{const dummy_set} will fail.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   962
  Why? A glimpse at the function equations will offer:
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   963
*}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   964
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   965
print_codethms (insert)
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   966
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   967
text {*
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   968
  This reveals the function equation @{thm insert_def}
21223
b3bdc1abc7d3 some corrections
haftmann
parents: 21222
diff changeset
   969
  for @{const insert}, which is operationally meaningless
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   970
  but forces an equality constraint on the set members
21223
b3bdc1abc7d3 some corrections
haftmann
parents: 21222
diff changeset
   971
  (which is not satisfiable if the set members are functions).
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   972
  Even when using set of natural numbers (which are an instance
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   973
  of \emph{eq}), we run into a problem:
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   974
*}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   975
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   976
definition
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   977
  foobar_set :: "nat set"
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   978
  "foobar_set = {0, 1, 2}"
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   979
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   980
text {*
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   981
  In this case the serializer would complain that @{const insert}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   982
  expects dictionaries (namely an \emph{eq} dictionary) but
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   983
  has also been given a customary serialization.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   984
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   985
  The solution to this dilemma:
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   986
*}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   987
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   988
lemma [code func]:
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   989
  "insert = insert" ..
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   990
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   991
code_gen dummy_set foobar_set (SML "examples/dirty_set.ML")
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   992
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   993
text {*
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   994
  \lstsml{Thy/examples/dirty_set.ML}
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
   995
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   996
  Reflexive function equations by convention are dropped.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   997
  But their presence prevents primitive definitions to be
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   998
  used as function equations:
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
   999
*}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1000
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1001
print_codethms (insert)
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1002
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1003
text {*
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1004
  will show \emph{no} function equations for insert.
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
  1005
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1006
  Note that the sort constraints of reflexive equations
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1007
  are considered; so
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1008
*}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1009
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1010
lemma [code func]:
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1011
  "(insert \<Colon> 'a\<Colon>eq \<Rightarrow> 'a set \<Rightarrow> 'a set) = insert" ..
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1012
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1013
text {*
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1014
  would mean nothing else than to introduce the evil
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1015
  sort constraint by hand.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1016
*}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1017
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1018
subsection {* Cyclic module dependencies *}
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
  1019
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1020
text {*
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1021
  Sometimes the awkward situation occurs that dependencies
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1022
  between definitions introduce cyclic dependencies
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1023
  between modules, which in the Haskell world leaves
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1024
  you to the mercy of the Haskell implementation you are using,
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1025
  while for SML code generation is not possible.
21178
c3618fc6a6f7 added gfx
haftmann
parents: 21147
diff changeset
  1026
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1027
  A solution is to declare module names explicitly.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1028
  Let use assume the three cyclically dependent
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1029
  modules are named \emph{A}, \emph{B} and \emph{C}.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1030
  Then, by stating
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1031
*}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1032
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1033
code_modulename SML
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1034
  A ABC
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1035
  B ABC
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1036
  C ABC
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1037
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1038
text {*
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1039
  we explicitly map all those modules on \emph{ABC},
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1040
  resulting in an ad-hoc merge of this three modules
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1041
  at serialization time.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1042
*}
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1043
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1044
subsection {* Axiomatic extensions *}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1045
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1046
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1047
  \begin{warn}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1048
    The extensions introduced in this section, though working
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1049
    in practice, are not the cream of the crop, as you
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1050
    will notice during reading.  They will
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1051
    eventually be replaced by more mature approaches.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1052
  \end{warn}
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1053
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1054
  Sometimes equalities are taken for granted which are
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1055
  not derivable inside the HOL logic but are silently assumed
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1056
  to hold for executable code.  For example, we may want
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1057
  to identify the famous HOL constant @{const arbitrary}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1058
  of type @{typ "'a option"} with @{const None}.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1059
  By brute force:
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1060
*}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1061
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1062
axioms
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1063
  arbitrary_option: "arbitrary = None"
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1064
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1065
text {*
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1066
  However this has to be considered harmful since this axiom,
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1067
  though probably justifiable for generated code, could
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1068
  introduce serious inconsistencies into the logic.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1069
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1070
  So, there is a distinguished construct for stating axiomatic
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1071
  equalities of constants which apply only for code generation.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1072
  Before introducing this, here is a convenient place to describe
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1073
  shortly how to deal with some restrictions the type discipline
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1074
  imposes.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1075
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1076
  By itself, the constant @{const arbitrary} is a non-overloaded
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1077
  polymorphic constant.  So, there is no way to distinguish
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1078
  different versions of @{const arbitrary} for different types
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1079
  inside the code generator framework.  However, inlining
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1080
  theorems together with auxiliary constants provide a solution:
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1081
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1082
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1083
definition
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1084
  arbitrary_option :: "'a option"
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1085
  [symmetric, code inline]: "arbitrary_option = arbitrary"
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1086
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1087
text {*
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1088
  By that, we replace any @{const arbitrary} with option type
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1089
  by @{const arbitrary_option} in function equations.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1090
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1091
  For technical reasons, we further have to provide a
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1092
  synonym for @{const None} which in code generator view
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1093
  is a function rather than a datatype constructor
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1094
*}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1095
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1096
definition
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1097
  "None' = None"
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1098
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1099
text {*
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1100
  Then finally we are enabled to use \isasymCODEAXIOMS:
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1101
*}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1102
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1103
code_axioms
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1104
  arbitrary_option \<equiv> None'
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1105
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1106
text {*
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1107
  A dummy example:
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1108
*}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1109
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1110
fun
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1111
  dummy_option :: "'a list \<Rightarrow> 'a option" where
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1112
  "dummy_option (x#xs) = Some x"
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1113
  "dummy_option [] = arbitrary"
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1114
termination by (auto_term "{}")
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1115
(*<*)
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1116
declare dummy_option.simps [code func]
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1117
(*>*)
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1118
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1119
code_gen dummy_option (SML "examples/arbitrary.ML")
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1120
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1121
text {*
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1122
  \lstsml{Thy/examples/arbitrary.ML}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1123
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1124
  Another axiomatic extension is code generation
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1125
  for abstracted types.  For this, the  
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1126
  \emph{ExecutableRat} (see \secref{exec_rat})
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1127
  forms a good example.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1128
*}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1129
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
  1130
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
  1131
section {* ML interfaces \label{sec:ml} *}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
  1132
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1133
text {*
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1134
  Since the code generator framework not only aims to provide
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1135
  a nice Isar interface but also to form a base for
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1136
  code-generation-based applications, here a short
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1137
  description of the most important ML interfaces.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1138
*}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1139
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1140
subsection {* Constants with type discipline: codegen\_consts.ML *}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1141
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1142
text {*
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1143
  This Pure module manages identification of (probably overloaded)
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1144
  constants by unique identifiers.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1145
*}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1146
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1147
text %mlref {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1148
  \begin{mldecls}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1149
  @{index_ML_type CodegenConsts.const} \\
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1150
  @{index_ML CodegenConsts.norm_of_typ: "theory -> string * typ -> CodegenConsts.const"} \\
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1151
  @{index_ML CodegenConsts.typ_of_inst: "theory -> CodegenConsts.const -> string * typ"} \\
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1152
 \end{mldecls}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1153
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1154
  \begin{description}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1155
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1156
  \item @{ML_type CodegenConsts.const} is the identifier type:
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1157
     the product of a \emph{string} with a list of \emph{typs}.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1158
     The \emph{string} is the constant name as represented inside Isabelle;
21223
b3bdc1abc7d3 some corrections
haftmann
parents: 21222
diff changeset
  1159
     the \emph{typs} are a type instantiation in the sense of System F,
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1160
     with canonical names for type variables.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1161
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1162
  \item @{ML CodegenConsts.norm_of_typ}~@{text thy}~@{text "(constname, typ)"}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1163
     maps a constant expression @{text "(constname, typ)"} to its canonical identifier.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1164
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1165
  \item @{ML CodegenConsts.typ_of_inst}~@{text thy}~@{text const}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1166
     maps a canonical identifier @{text const} to a constant
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1167
     expression with appropriate type.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1168
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1169
  \end{description}
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1170
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1171
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1172
subsection {* Executable theory content: codegen\_data.ML *}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1173
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1174
text {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1175
  This Pure module implements the core notions of
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1176
  executable content of a theory.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1177
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1178
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1179
subsubsection {* Suspended theorems *}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1180
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1181
text %mlref {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1182
  \begin{mldecls}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1183
  @{index_ML_type CodegenData.lthms} \\
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1184
  @{index_ML CodegenData.lazy: "(unit -> thm list) -> CodegenData.lthms"}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1185
  \end{mldecls}
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1186
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1187
  \begin{description}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1188
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1189
  \item @{ML_type CodegenData.lthms} is an abstract view
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1190
     on suspended theorems.  Suspensions are evaluated on demand.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1191
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1192
  \item @{ML CodegenData.lazy}~@{text f} turns an abstract
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1193
     theorem computation @{text f} into suspended theorems.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1194
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1195
  \end{description}
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1196
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1197
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1198
subsubsection {* Executable content *}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
  1199
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1200
text %mlref {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1201
  \begin{mldecls}
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1202
  @{index_ML_type CodegenData.lthms} \\
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1203
  @{index_ML CodegenData.add_func: "thm -> theory -> theory"} \\
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1204
  @{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1205
  @{index_ML CodegenData.add_funcl: "CodegenConsts.const * CodegenData.lthms -> theory -> theory"} \\
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1206
  @{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1207
  @{index_ML CodegenData.del_inline: "thm -> theory -> theory"} \\
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1208
  @{index_ML CodegenData.add_inline_proc: "(theory -> cterm list -> thm list)
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1209
    -> theory -> theory"} \\
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1210
  @{index_ML CodegenData.add_preproc: "(theory -> thm list -> thm list)
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1211
    -> theory -> theory"} \\
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1212
  @{index_ML CodegenData.add_datatype: "string * (((string * sort) list * (string * typ list) list)
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1213
    * CodegenData.lthms) -> theory -> theory"} \\
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1214
  @{index_ML CodegenData.del_datatype: "string -> theory -> theory"} \\
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1215
  @{index_ML CodegenData.get_datatype: "theory -> string
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1216
    -> ((string * sort) list * (string * typ list) list) option"} \\
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1217
  @{index_ML CodegenData.get_datatype_of_constr: "theory -> CodegenConsts.const -> string option"}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1218
  \end{mldecls}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1219
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1220
  \begin{description}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1221
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1222
  \item @{ML CodegenData.add_func}~@{text "thm"}~@{text "thy"} adds function
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1223
     theorem @{text "thm"} to executable content.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1224
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1225
  \item @{ML CodegenData.del_func}~@{text "thm"}~@{text "thy"} removes function
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1226
     theorem @{text "thm"} from executable content, if present.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1227
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1228
  \item @{ML CodegenData.add_funcl}~@{text "(const, lthms)"}~@{text "thy"} adds
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1229
     suspended function equations @{text lthms} for constant
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1230
     @{text const} to executable content.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1231
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1232
  \item @{ML CodegenData.add_inline}~@{text "thm"}~@{text "thy"} adds
21223
b3bdc1abc7d3 some corrections
haftmann
parents: 21222
diff changeset
  1233
     inlining theorem @{text thm} to executable content.
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1234
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1235
  \item @{ML CodegenData.del_inline}~@{text "thm"}~@{text "thy"} remove
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1236
     inlining theorem @{text thm} from executable content, if present.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1237
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1238
  \item @{ML CodegenData.add_inline_proc}~@{text "f"}~@{text "thy"} adds
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1239
     inline procedure @{text f} to executable content;
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1240
     @{text f} is a computation of rewrite rules dependent on
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1241
     the current theory context and the list of all arguments
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1242
     and right hand sides of the function equations belonging
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1243
     to a certain function definition.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1244
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1245
  \item @{ML CodegenData.add_preproc}~@{text "f"}~@{text "thy"} adds
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1246
     generic preprocessor @{text f} to executable content;
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1247
     @{text f} is a transformation of the function equations belonging
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1248
     to a certain function definition, depending on the
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1249
     current theory context.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1250
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1251
  \item @{ML CodegenData.add_datatype}~@{text "(name, (spec, cert))"}~@{text "thy"} adds
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1252
     a datatype to executable content, with type constructor
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1253
     @{text name} and specification @{text spec}; @{text spec} is
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1254
     a pair consisting of a list of type variable with sort
21223
b3bdc1abc7d3 some corrections
haftmann
parents: 21222
diff changeset
  1255
     constraints and a list of constructors with name
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1256
     and types of arguments.  The addition as datatype
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1257
     has to be justified giving a certificate of suspended
21223
b3bdc1abc7d3 some corrections
haftmann
parents: 21222
diff changeset
  1258
     theorems as witnesses for injectiveness and distinctness.
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1259
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1260
  \item @{ML CodegenData.del_datatype}~@{text "name"}~@{text "thy"}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1261
     remove a datatype from executable content, if present.
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1262
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1263
  \item @{ML CodegenData.get_datatype_of_constr}~@{text "thy"}~@{text "const"}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1264
     returns type constructor corresponding to
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1265
     constructor @{text const}; returns @{text NONE}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1266
     if @{text const} is no constructor.
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1267
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1268
  \end{description}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1269
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1270
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1271
subsection {* Function equation systems: codegen\_funcgr.ML *}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1272
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1273
text {*
21217
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1274
  Out of the executable content of a theory, a normalized
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1275
  function equation systems may be constructed containing
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1276
  function definitions for constants.  The system is cached
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1277
  until its underlying executable content changes.
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1278
*}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1279
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1280
text %mlref {*
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1281
  \begin{mldecls}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1282
  @{index_ML_type CodegenFuncgr.T} \\
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1283
  @{index_ML CodegenFuncgr.make: "theory -> CodegenConsts.const list -> CodegenFuncgr.T"} \\
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1284
  @{index_ML CodegenFuncgr.funcs: "CodegenFuncgr.T -> CodegenConsts.const -> thm list"} \\
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1285
  @{index_ML CodegenFuncgr.typ: "CodegenFuncgr.T -> CodegenConsts.const -> typ"} \\
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1286
  @{index_ML CodegenFuncgr.deps: "CodegenFuncgr.T
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1287
    -> CodegenConsts.const list -> CodegenConsts.const list list"} \\
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1288
  @{index_ML CodegenFuncgr.all: "CodegenFuncgr.T -> CodegenConsts.const list"}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1289
  \end{mldecls}
21217
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1290
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1291
  \begin{description}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1292
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1293
  \item @{ML_type CodegenFuncgr.T} represents
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1294
    a normalized function equation system.
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1295
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1296
  \item @{ML CodegenFuncgr.make}~@{text thy}~@{text cs}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1297
    returns a normalized function equation system,
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1298
    with the assertion that it contains any function
21223
b3bdc1abc7d3 some corrections
haftmann
parents: 21222
diff changeset
  1299
    definition for constants @{text cs} (if existing).
21217
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1300
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1301
  \item @{ML CodegenFuncgr.funcs}~@{text funcgr}~@{text c}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1302
    retrieves function definition for constant @{text c}.
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1303
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1304
  \item @{ML CodegenFuncgr.typ}~@{text funcgr}~@{text c}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1305
    retrieves function type for constant @{text c}.
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1306
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1307
  \item @{ML CodegenFuncgr.deps}~@{text funcgr}~@{text cs}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1308
    returns the transitive closure of dependencies for
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1309
    constants @{text cs} as a partitioning where each partition
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1310
    corresponds to a strongly connected component of
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1311
    dependencies and any partition does \emph{not}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1312
    depend on partitions further left.
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1313
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1314
  \item @{ML CodegenFuncgr.all}~@{text funcgr}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1315
    returns all currently represented constants.
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1316
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1317
  \end{description}
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1318
*}
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1319
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1320
subsection {* Further auxiliary *}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1321
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1322
text %mlref {*
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1323
  \begin{mldecls}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1324
  @{index_ML CodegenConsts.const_ord: "CodegenConsts.const * CodegenConsts.const -> order"} \\
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1325
  @{index_ML CodegenConsts.eq_const: "CodegenConsts.const * CodegenConsts.const -> bool"} \\
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1326
  @{index_ML CodegenConsts.consts_of: "theory -> term -> CodegenConsts.const list"} \\
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1327
  @{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1328
  @{index_ML_structure CodegenConsts.Consttab} \\
21189
5435ccdb4ea1 (continued)
haftmann
parents: 21178
diff changeset
  1329
  @{index_ML_structure CodegenFuncgr.Constgraph} \\
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1330
  @{index_ML CodegenData.typ_func: "theory -> thm -> typ"} \\
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1331
  @{index_ML CodegenData.rewrite_func: "thm list -> thm -> thm"} \\
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1332
  \end{mldecls}
21217
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1333
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1334
  \begin{description}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1335
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1336
  \item @{ML CodegenConsts.const_ord},~@{ML CodegenConsts.eq_const}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1337
     provide order and equality on constant identifiers.
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1338
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1339
  \item @{ML_struct CodegenConsts.Consttab},~@{ML_struct CodegenFuncgr.Constgraph}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1340
     provide advanced data structures with constant identifiers as keys.
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1341
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1342
  \item @{ML CodegenConsts.consts_of}~@{text thy}~@{text t}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1343
     returns all constant identifiers mentioned in a term @{text t}.
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1344
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1345
  \item @{ML CodegenConsts.read_const}~@{text thy}~@{text s}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1346
     reads a constant as a concrete term expression @{text s}.
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1347
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1348
  \item @{ML CodegenData.typ_func}~@{text thy}~@{text thm}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1349
     extracts the type of a constant in a function equation @{text thm}.
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1350
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1351
  \item @{ML CodegenData.rewrite_func}~@{text rews}~@{text thm}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1352
     rewrites a function equation @{text thm} with a set of rewrite
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1353
     rules @{text rews}; only arguments and right hand side are rewritten,
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1354
     not the head of the function equation.
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1355
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1356
  \end{description}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1357
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1358
*}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
  1359
9b9910b82645 initial draft
haftmann
parents:
diff changeset
  1360
subsection {* Implementing code generator applications *}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
  1361
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1362
text {*
21217
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1363
  Implementing code generator applications on top
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1364
  of the framework set out so far usually not only
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1365
  involves using those primitive interfaces
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1366
  but also storing code-dependent data and various
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1367
  other things.
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1368
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1369
  \begin{warn}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1370
    Some interfaces discussed here have not reached
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1371
    a final state yet.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1372
    Changes likely to occur in future.
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1373
  \end{warn}
21222
6dfdb69e83ef adjusted title
haftmann
parents: 21217
diff changeset
  1374
6dfdb69e83ef adjusted title
haftmann
parents: 21217
diff changeset
  1375
  \fixme
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1376
*}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1377
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1378
subsubsection {* Data depending on the theory's executable content *}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1379
21217
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1380
text {*
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1381
  \medskip
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1382
  \begin{tabular}{l}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1383
  @{text "val name: string"} \\
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1384
  @{text "type T"} \\
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1385
  @{text "val empty: T"} \\
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1386
  @{text "val merge: Pretty.pp \<rightarrow> T * T \<rightarrow> T"} \\
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1387
  @{text "val purge: theory option \<rightarrow> CodegenConsts.const list option \<rightarrow> T \<rightarrow> T"}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1388
  \end{tabular}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1389
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1390
  \medskip
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1391
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1392
  \begin{tabular}{l}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1393
  @{text "init: theory \<rightarrow> theory"} \\
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1394
  @{text "get: theory \<rightarrow> T"} \\
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1395
  @{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1396
  @{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1397
  \end{tabular}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1398
*}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1399
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1400
text %mlref {*
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1401
  \begin{mldecls}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1402
  @{index_ML_functor CodeDataFun}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1403
  \end{mldecls}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1404
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1405
  \begin{description}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1406
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1407
  \item @{ML_functor CodeDataFun}@{text "(spec)"} declares code
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1408
  dependent data according to the specification provided as
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1409
  argument structure.  The resulting structure provides data init and
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1410
  access operations as described above.
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1411
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1412
  \end{description}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1413
*}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1414
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1415
subsubsection {* Datatype hooks *}
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1416
21217
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1417
text %mlref {*
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1418
  \begin{mldecls}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1419
  @{index_ML_type DatatypeHooks.hook} \\
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1420
  @{index_ML DatatypeHooks.add: "DatatypeHooks.hook -> theory -> theory"}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1421
  \end{mldecls}
21147
737a94f047e3 continued tutorial
haftmann
parents: 21089
diff changeset
  1422
*}
21058
a32d357dfd70 started tutorial
haftmann
parents: 20948
diff changeset
  1423
21217
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1424
text %mlref {*
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1425
  \begin{mldecls}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1426
  @{index_ML_type TypecopyPackage.info} \\
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1427
  @{index_ML TypecopyPackage.add_typecopy: "
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1428
    bstring * string list -> typ -> (bstring * bstring) option
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1429
    -> theory -> (string * TypecopyPackage.info) * theory"} \\
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1430
  @{index_ML TypecopyPackage.get_typecopies: "theory -> string list"} \\
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1431
  @{index_ML TypecopyPackage.get_typecopy_info: "theory
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1432
    -> string -> TypecopyPackage.info option"} \\
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1433
  @{index_ML_type TypecopyPackage.hook} \\
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1434
  @{index_ML TypecopyPackage.add_hook: "TypecopyPackage.hook -> theory -> theory"} \\
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1435
  @{index_ML TypecopyPackage.get_spec: "theory -> string
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1436
    -> (string * sort) list * (string * typ list) list"}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1437
  \end{mldecls}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1438
*}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1439
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1440
text %mlref {*
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1441
  \begin{mldecls}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1442
  @{index_ML_type DatatypeCodegen.hook} \\
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1443
  @{index_ML DatatypeCodegen.add_codetypes_hook_bootstrap: "
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1444
      DatatypeCodegen.hook -> theory -> theory"}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1445
  \end{mldecls}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1446
*}
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1447
21222
6dfdb69e83ef adjusted title
haftmann
parents: 21217
diff changeset
  1448
text {*
6dfdb69e83ef adjusted title
haftmann
parents: 21217
diff changeset
  1449
  \fixme
6dfdb69e83ef adjusted title
haftmann
parents: 21217
diff changeset
  1450
%  \emph{Happy proving, happy hacking!}
6dfdb69e83ef adjusted title
haftmann
parents: 21217
diff changeset
  1451
*}
21217
0425fc57510f continued
haftmann
parents: 21189
diff changeset
  1452
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
  1453
end