doc-src/Codegen/Thy/Program.thy
author haftmann
Tue May 26 12:31:01 2009 +0200 (2009-05-26)
changeset 31254 03a35fbc9dc6
parent 30938 c6c9359e474c
child 32000 6f07563dc8a9
permissions -rw-r--r--
documented print_codeproc command
     1 theory Program
     2 imports Introduction
     3 begin
     4 
     5 section {* Turning Theories into Programs \label{sec:program} *}
     6 
     7 subsection {* The @{text "Isabelle/HOL"} default setup *}
     8 
     9 text {*
    10   We have already seen how by default equations stemming from
    11   @{command definition}/@{command primrec}/@{command fun}
    12   statements are used for code generation.  This default behaviour
    13   can be changed, e.g. by providing different code equations.
    14   All kinds of customisation shown in this section is \emph{safe}
    15   in the sense that the user does not have to worry about
    16   correctness -- all programs generatable that way are partially
    17   correct.
    18 *}
    19 
    20 subsection {* Selecting code equations *}
    21 
    22 text {*
    23   Coming back to our introductory example, we
    24   could provide an alternative code equations for @{const dequeue}
    25   explicitly:
    26 *}
    27 
    28 lemma %quote [code]:
    29   "dequeue (AQueue xs []) =
    30      (if xs = [] then (None, AQueue [] [])
    31        else dequeue (AQueue [] (rev xs)))"
    32   "dequeue (AQueue xs (y # ys)) =
    33      (Some y, AQueue xs ys)"
    34   by (cases xs, simp_all) (cases "rev xs", simp_all)
    35 
    36 text {*
    37   \noindent The annotation @{text "[code]"} is an @{text Isar}
    38   @{text attribute} which states that the given theorems should be
    39   considered as code equations for a @{text fun} statement --
    40   the corresponding constant is determined syntactically.  The resulting code:
    41 *}
    42 
    43 text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
    44 
    45 text {*
    46   \noindent You may note that the equality test @{term "xs = []"} has been
    47   replaced by the predicate @{term "null xs"}.  This is due to the default
    48   setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
    49 
    50   Changing the default constructor set of datatypes is also
    51   possible.  See \secref{sec:datatypes} for an example.
    52 
    53   As told in \secref{sec:concept}, code generation is based
    54   on a structured collection of code theorems.
    55   For explorative purpose, this collection
    56   may be inspected using the @{command code_thms} command:
    57 *}
    58 
    59 code_thms %quote dequeue
    60 
    61 text {*
    62   \noindent prints a table with \emph{all} code equations
    63   for @{const dequeue}, including
    64   \emph{all} code equations those equations depend
    65   on recursively.
    66   
    67   Similarly, the @{command code_deps} command shows a graph
    68   visualising dependencies between code equations.
    69 *}
    70 
    71 subsection {* @{text class} and @{text instantiation} *}
    72 
    73 text {*
    74   Concerning type classes and code generation, let us examine an example
    75   from abstract algebra:
    76 *}
    77 
    78 class %quote semigroup =
    79   fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
    80   assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    81 
    82 class %quote monoid = semigroup +
    83   fixes neutral :: 'a ("\<one>")
    84   assumes neutl: "\<one> \<otimes> x = x"
    85     and neutr: "x \<otimes> \<one> = x"
    86 
    87 instantiation %quote nat :: monoid
    88 begin
    89 
    90 primrec %quote mult_nat where
    91     "0 \<otimes> n = (0\<Colon>nat)"
    92   | "Suc m \<otimes> n = n + m \<otimes> n"
    93 
    94 definition %quote neutral_nat where
    95   "\<one> = Suc 0"
    96 
    97 lemma %quote add_mult_distrib:
    98   fixes n m q :: nat
    99   shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q"
   100   by (induct n) simp_all
   101 
   102 instance %quote proof
   103   fix m n q :: nat
   104   show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
   105     by (induct m) (simp_all add: add_mult_distrib)
   106   show "\<one> \<otimes> n = n"
   107     by (simp add: neutral_nat_def)
   108   show "m \<otimes> \<one> = m"
   109     by (induct m) (simp_all add: neutral_nat_def)
   110 qed
   111 
   112 end %quote
   113 
   114 text {*
   115   \noindent We define the natural operation of the natural numbers
   116   on monoids:
   117 *}
   118 
   119 primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
   120     "pow 0 a = \<one>"
   121   | "pow (Suc n) a = a \<otimes> pow n a"
   122 
   123 text {*
   124   \noindent This we use to define the discrete exponentiation function:
   125 *}
   126 
   127 definition %quote bexp :: "nat \<Rightarrow> nat" where
   128   "bexp n = pow n (Suc (Suc 0))"
   129 
   130 text {*
   131   \noindent The corresponding code:
   132 *}
   133 
   134 text %quote {*@{code_stmts bexp (Haskell)}*}
   135 
   136 text {*
   137   \noindent This is a convenient place to show how explicit dictionary construction
   138   manifests in generated code (here, the same example in @{text SML}):
   139 *}
   140 
   141 text %quote {*@{code_stmts bexp (SML)}*}
   142 
   143 text {*
   144   \noindent Note the parameters with trailing underscore (@{verbatim "A_"})
   145     which are the dictionary parameters.
   146 *}
   147 
   148 subsection {* The preprocessor \label{sec:preproc} *}
   149 
   150 text {*
   151   Before selected function theorems are turned into abstract
   152   code, a chain of definitional transformation steps is carried
   153   out: \emph{preprocessing}.  In essence, the preprocessor
   154   consists of two components: a \emph{simpset} and \emph{function transformers}.
   155 
   156   The \emph{simpset} allows to employ the full generality of the Isabelle
   157   simplifier.  Due to the interpretation of theorems
   158   as code equations, rewrites are applied to the right
   159   hand side and the arguments of the left hand side of an
   160   equation, but never to the constant heading the left hand side.
   161   An important special case are \emph{inline theorems} which may be
   162   declared and undeclared using the
   163   \emph{code inline} or \emph{code inline del} attribute respectively.
   164 
   165   Some common applications:
   166 *}
   167 
   168 text_raw {*
   169   \begin{itemize}
   170 *}
   171 
   172 text {*
   173      \item replacing non-executable constructs by executable ones:
   174 *}     
   175 
   176 lemma %quote [code inline]:
   177   "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
   178 
   179 text {*
   180      \item eliminating superfluous constants:
   181 *}
   182 
   183 lemma %quote [code inline]:
   184   "1 = Suc 0" by simp
   185 
   186 text {*
   187      \item replacing executable but inconvenient constructs:
   188 *}
   189 
   190 lemma %quote [code inline]:
   191   "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
   192 
   193 text_raw {*
   194   \end{itemize}
   195 *}
   196 
   197 text {*
   198   \noindent \emph{Function transformers} provide a very general interface,
   199   transforming a list of function theorems to another
   200   list of function theorems, provided that neither the heading
   201   constant nor its type change.  The @{term "0\<Colon>nat"} / @{const Suc}
   202   pattern elimination implemented in
   203   theory @{text Efficient_Nat} (see \secref{eff_nat}) uses this
   204   interface.
   205 
   206   \noindent The current setup of the preprocessor may be inspected using
   207   the @{command print_codeproc} command.
   208   @{command code_thms} provides a convenient
   209   mechanism to inspect the impact of a preprocessor setup
   210   on code equations.
   211 
   212   \begin{warn}
   213     The attribute \emph{code unfold}
   214     associated with the @{text "SML code generator"} also applies to
   215     the @{text "generic code generator"}:
   216     \emph{code unfold} implies \emph{code inline}.
   217   \end{warn}
   218 *}
   219 
   220 subsection {* Datatypes \label{sec:datatypes} *}
   221 
   222 text {*
   223   Conceptually, any datatype is spanned by a set of
   224   \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
   225   "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
   226   @{text "\<tau>"}.  The HOL datatype package by default registers any new
   227   datatype in the table of datatypes, which may be inspected using the
   228   @{command print_codesetup} command.
   229 
   230   In some cases, it is appropriate to alter or extend this table.  As
   231   an example, we will develop an alternative representation of the
   232   queue example given in \secref{sec:intro}.  The amortised
   233   representation is convenient for generating code but exposes its
   234   \qt{implementation} details, which may be cumbersome when proving
   235   theorems about it.  Therefore, here a simple, straightforward
   236   representation of queues:
   237 *}
   238 
   239 datatype %quote 'a queue = Queue "'a list"
   240 
   241 definition %quote empty :: "'a queue" where
   242   "empty = Queue []"
   243 
   244 primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
   245   "enqueue x (Queue xs) = Queue (xs @ [x])"
   246 
   247 fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
   248     "dequeue (Queue []) = (None, Queue [])"
   249   | "dequeue (Queue (x # xs)) = (Some x, Queue xs)"
   250 
   251 text {*
   252   \noindent This we can use directly for proving;  for executing,
   253   we provide an alternative characterisation:
   254 *}
   255 
   256 definition %quote AQueue :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a queue" where
   257   "AQueue xs ys = Queue (ys @ rev xs)"
   258 
   259 code_datatype %quote AQueue
   260 
   261 text {*
   262   \noindent Here we define a \qt{constructor} @{const "AQueue"} which
   263   is defined in terms of @{text "Queue"} and interprets its arguments
   264   according to what the \emph{content} of an amortised queue is supposed
   265   to be.  Equipped with this, we are able to prove the following equations
   266   for our primitive queue operations which \qt{implement} the simple
   267   queues in an amortised fashion:
   268 *}
   269 
   270 lemma %quote empty_AQueue [code]:
   271   "empty = AQueue [] []"
   272   unfolding AQueue_def empty_def by simp
   273 
   274 lemma %quote enqueue_AQueue [code]:
   275   "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
   276   unfolding AQueue_def by simp
   277 
   278 lemma %quote dequeue_AQueue [code]:
   279   "dequeue (AQueue xs []) =
   280     (if xs = [] then (None, AQueue [] [])
   281     else dequeue (AQueue [] (rev xs)))"
   282   "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
   283   unfolding AQueue_def by simp_all
   284 
   285 text {*
   286   \noindent For completeness, we provide a substitute for the
   287   @{text case} combinator on queues:
   288 *}
   289 
   290 lemma %quote queue_case_AQueue [code]:
   291   "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
   292   unfolding AQueue_def by simp
   293 
   294 text {*
   295   \noindent The resulting code looks as expected:
   296 *}
   297 
   298 text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
   299 
   300 text {*
   301   \noindent From this example, it can be glimpsed that using own
   302   constructor sets is a little delicate since it changes the set of
   303   valid patterns for values of that type.  Without going into much
   304   detail, here some practical hints:
   305 
   306   \begin{itemize}
   307 
   308     \item When changing the constructor set for datatypes, take care
   309       to provide alternative equations for the @{text case} combinator.
   310 
   311     \item Values in the target language need not to be normalised --
   312       different values in the target language may represent the same
   313       value in the logic.
   314 
   315     \item Usually, a good methodology to deal with the subtleties of
   316       pattern matching is to see the type as an abstract type: provide
   317       a set of operations which operate on the concrete representation
   318       of the type, and derive further operations by combinations of
   319       these primitive ones, without relying on a particular
   320       representation.
   321 
   322   \end{itemize}
   323 *}
   324 
   325 
   326 subsection {* Equality *}
   327 
   328 text {*
   329   Surely you have already noticed how equality is treated
   330   by the code generator:
   331 *}
   332 
   333 primrec %quote collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   334   "collect_duplicates xs ys [] = xs"
   335   | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
   336       then if z \<in> set ys
   337         then collect_duplicates xs ys zs
   338         else collect_duplicates xs (z#ys) zs
   339       else collect_duplicates (z#xs) (z#ys) zs)"
   340 
   341 text {*
   342   \noindent The membership test during preprocessing is rewritten,
   343   resulting in @{const List.member}, which itself
   344   performs an explicit equality check.
   345 *}
   346 
   347 text %quote {*@{code_stmts collect_duplicates (SML)}*}
   348 
   349 text {*
   350   \noindent Obviously, polymorphic equality is implemented the Haskell
   351   way using a type class.  How is this achieved?  HOL introduces
   352   an explicit class @{class eq} with a corresponding operation
   353   @{const eq_class.eq} such that @{thm eq [no_vars]}.
   354   The preprocessing framework does the rest by propagating the
   355   @{class eq} constraints through all dependent code equations.
   356   For datatypes, instances of @{class eq} are implicitly derived
   357   when possible.  For other types, you may instantiate @{text eq}
   358   manually like any other type class.
   359 
   360   Though this @{text eq} class is designed to get rarely in
   361   the way, in some cases the automatically derived code equations
   362   for equality on a particular type may not be appropriate.
   363   As example, watch the following datatype representing
   364   monomorphic parametric types (where type constructors
   365   are referred to by natural numbers):
   366 *}
   367 
   368 datatype %quote monotype = Mono nat "monotype list"
   369 (*<*)
   370 lemma monotype_eq:
   371   "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<equiv> 
   372      eq_class.eq tyco1 tyco2 \<and> eq_class.eq typargs1 typargs2" by (simp add: eq)
   373 (*>*)
   374 
   375 text {*
   376   \noindent Then code generation for SML would fail with a message
   377   that the generated code contains illegal mutual dependencies:
   378   the theorem @{thm monotype_eq [no_vars]} already requires the
   379   instance @{text "monotype \<Colon> eq"}, which itself requires
   380   @{thm monotype_eq [no_vars]};  Haskell has no problem with mutually
   381   recursive @{text instance} and @{text function} definitions,
   382   but the SML serialiser does not support this.
   383 
   384   In such cases, you have to provide your own equality equations
   385   involving auxiliary constants.  In our case,
   386   @{const [show_types] list_all2} can do the job:
   387 *}
   388 
   389 lemma %quote monotype_eq_list_all2 [code]:
   390   "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<longleftrightarrow>
   391      eq_class.eq tyco1 tyco2 \<and> list_all2 eq_class.eq typargs1 typargs2"
   392   by (simp add: eq list_all2_eq [symmetric])
   393 
   394 text {*
   395   \noindent does not depend on instance @{text "monotype \<Colon> eq"}:
   396 *}
   397 
   398 text %quote {*@{code_stmts "eq_class.eq :: monotype \<Rightarrow> monotype \<Rightarrow> bool" (SML)}*}
   399 
   400 
   401 subsection {* Explicit partiality *}
   402 
   403 text {*
   404   Partiality usually enters the game by partial patterns, as
   405   in the following example, again for amortised queues:
   406 *}
   407 
   408 definition %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
   409   "strict_dequeue q = (case dequeue q
   410     of (Some x, q') \<Rightarrow> (x, q'))"
   411 
   412 lemma %quote strict_dequeue_AQueue [code]:
   413   "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
   414   "strict_dequeue (AQueue xs []) =
   415     (case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
   416   by (simp_all add: strict_dequeue_def dequeue_AQueue split: list.splits)
   417 
   418 text {*
   419   \noindent In the corresponding code, there is no equation
   420   for the pattern @{term "AQueue [] []"}:
   421 *}
   422 
   423 text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*}
   424 
   425 text {*
   426   \noindent In some cases it is desirable to have this
   427   pseudo-\qt{partiality} more explicitly, e.g.~as follows:
   428 *}
   429 
   430 axiomatization %quote empty_queue :: 'a
   431 
   432 definition %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
   433   "strict_dequeue' q = (case dequeue q of (Some x, q') \<Rightarrow> (x, q') | _ \<Rightarrow> empty_queue)"
   434 
   435 lemma %quote strict_dequeue'_AQueue [code]:
   436   "strict_dequeue' (AQueue xs []) = (if xs = [] then empty_queue
   437      else strict_dequeue' (AQueue [] (rev xs)))"
   438   "strict_dequeue' (AQueue xs (y # ys)) =
   439      (y, AQueue xs ys)"
   440   by (simp_all add: strict_dequeue'_def dequeue_AQueue split: list.splits)
   441 
   442 text {*
   443   Observe that on the right hand side of the definition of @{const
   444   "strict_dequeue'"} the constant @{const empty_queue} occurs
   445   which is unspecified.
   446 
   447   Normally, if constants without any code equations occur in a
   448   program, the code generator complains (since in most cases this is
   449   not what the user expects).  But such constants can also be thought
   450   of as function definitions with no equations which always fail,
   451   since there is never a successful pattern match on the left hand
   452   side.  In order to categorise a constant into that category
   453   explicitly, use @{command "code_abort"}:
   454 *}
   455 
   456 code_abort %quote empty_queue
   457 
   458 text {*
   459   \noindent Then the code generator will just insert an error or
   460   exception at the appropriate position:
   461 *}
   462 
   463 text %quote {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*}
   464 
   465 text {*
   466   \noindent This feature however is rarely needed in practice.
   467   Note also that the @{text HOL} default setup already declares
   468   @{const undefined} as @{command "code_abort"}, which is most
   469   likely to be used in such situations.
   470 *}
   471 
   472 end
   473