author haftmann Sat, 27 Nov 2010 18:51:04 +0100 changeset 40752 aae9a020fa77 parent 40751 6975c4d83ffd child 40753 5288144b4358
tuned formatting; adjustments to changes on ML level
--- a/doc-src/Codegen/Thy/Further.thy	Sat Nov 27 18:51:04 2010 +0100
+++ b/doc-src/Codegen/Thy/Further.thy	Sat Nov 27 18:51:04 2010 +0100
@@ -7,20 +7,20 @@
subsection {* Modules namespace *}

text {*
-  When invoking the @{command export_code} command it is possible to leave
-  out the @{keyword "module_name"} part;  then code is distributed over
-  different modules, where the module name space roughly is induced
-  by the Isabelle theory name space.
+  When invoking the @{command export_code} command it is possible to
+  leave out the @{keyword "module_name"} part; then code is
+  distributed over different modules, where the module name space
+  roughly is induced by the Isabelle theory name space.

-  Then sometimes the awkward situation occurs that dependencies between
-  definitions introduce cyclic dependencies between modules, which in the
-  @{text Haskell} world leaves you to the mercy of the @{text Haskell} implementation
-  you are using,  while for @{text SML}/@{text OCaml} code generation is not possible.
+  Then sometimes the awkward situation occurs that dependencies
+  between definitions introduce cyclic dependencies between modules,
+  which in the @{text Haskell} world leaves you to the mercy of the
+  @{text Haskell} implementation you are using, while for @{text
+  SML}/@{text OCaml} code generation is not possible.

-  A solution is to declare module names explicitly.
-  Let use assume the three cyclically dependent
-  modules are named \emph{A}, \emph{B} and \emph{C}.
-  Then, by stating
+  A solution is to declare module names explicitly.  Let use assume
+  the three cyclically dependent modules are named \emph{A}, \emph{B}
+  and \emph{C}.  Then, by stating
*}

code_modulename %quote SML
@@ -28,10 +28,10 @@
B ABC
C ABC

-text {*\noindent
-  we explicitly map all those modules on \emph{ABC},
-  resulting in an ad-hoc merge of this three modules
-  at serialisation time.
+text {*
+  \noindent we explicitly map all those modules on \emph{ABC},
+  resulting in an ad-hoc merge of this three modules at serialisation
+  time.
*}

subsection {* Locales and interpretation *}
@@ -40,8 +40,8 @@
A technical issue comes to surface when generating code from
specifications stemming from locale interpretation.

-  Let us assume a locale specifying a power operation
-  on arbitrary types:
+  Let us assume a locale specifying a power operation on arbitrary
+  types:
*}

locale %quote power =
@@ -50,8 +50,8 @@
begin

text {*
-  \noindent Inside that locale we can lift @{text power} to exponent lists
-  by means of specification relative to that locale:
+  \noindent Inside that locale we can lift @{text power} to exponent
+  lists by means of specification relative to that locale:
*}

primrec %quote powers :: "'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
@@ -76,26 +76,27 @@

text {*
After an interpretation of this locale (say, @{command_def
-  interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f ::
-  'a \<Rightarrow> 'a). f ^^ n)"}), one would expect to have a constant @{text
+  interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f
+  :: 'a \<Rightarrow> 'a). f ^^ n)"}), one would expect to have a constant @{text
"fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"} for which code
can be generated.  But this not the case: internally, the term
@{text "fun_power.powers"} is an abbreviation for the foundational
term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"}
(see \cite{isabelle-locale} for the details behind).

-  Fortunately, with minor effort the desired behaviour can be achieved.
-  First, a dedicated definition of the constant on which the local @{text "powers"}
-  after interpretation is supposed to be mapped on:
+  Fortunately, with minor effort the desired behaviour can be
+  achieved.  First, a dedicated definition of the constant on which
+  the local @{text "powers"} after interpretation is supposed to be
+  mapped on:
*}

definition %quote funpows :: "nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
[code del]: "funpows = power.powers (\<lambda>n f. f ^^ n)"

text {*
-  \noindent In general, the pattern is @{text "c = t"} where @{text c} is
-  the name of the future constant and @{text t} the foundational term
-  corresponding to the local constant after interpretation.
+  \noindent In general, the pattern is @{text "c = t"} where @{text c}
+  is the name of the future constant and @{text t} the foundational
+  term corresponding to the local constant after interpretation.

The interpretation itself is enriched with an equation @{text "t = c"}:
*}
@@ -106,8 +107,8 @@
(simp_all add: fun_eq_iff funpow_mult mult_commute funpows_def)

text {*
-  \noindent This additional equation is trivially proved by the definition
-  itself.
+  \noindent This additional equation is trivially proved by the
+  definition itself.

After this setup procedure, code generation can continue as usual:
*}
@@ -124,8 +125,8 @@
specific application, you should consider \emph{Imperative
Functional Programming with Isabelle/HOL}
\cite{bulwahn-et-al:2008:imperative}; the framework described there
-  is available in session @{text Imperative_HOL}, together with a short
-  primer document.
+  is available in session @{text Imperative_HOL}, together with a
+  short primer document.
*}

@@ -153,7 +154,7 @@
@{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
@{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
@{index_ML Code.get_type: "theory -> string
-    -> (string * sort) list * ((string * string list) * typ list) list"} \\
+    -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool"} \\
@{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"}
\end{mldecls}

@@ -198,22 +199,19 @@
subsubsection {* Data depending on the theory's executable content *}

text {*
-  Implementing code generator applications on top
-  of the framework set out so far usually not only
-  involves using those primitive interfaces
-  but also storing code-dependent data and various
-  other things.
+  Implementing code generator applications on top of the framework set
+  out so far usually not only involves using those primitive
+  interfaces but also storing code-dependent data and various other
+  things.

-  Due to incrementality of code generation, changes in the
-  theory's executable content have to be propagated in a
-  certain fashion.  Additionally, such changes may occur
-  not only during theory extension but also during theory
-  merge, which is a little bit nasty from an implementation
-  point of view.  The framework provides a solution
-  to this technical challenge by providing a functorial
-  data slot @{ML_functor Code_Data}; on instantiation
-  of this functor, the following types and operations
-  are required:
+  Due to incrementality of code generation, changes in the theory's
+  executable content have to be propagated in a certain fashion.
+  Additionally, such changes may occur not only during theory
+  extension but also during theory merge, which is a little bit nasty
+  from an implementation point of view.  The framework provides a
+  solution to this technical challenge by providing a functorial data
+  slot @{ML_functor Code_Data}; on instantiation of this functor, the
+  following types and operations are required:

\medskip
\begin{tabular}{l}
@@ -229,8 +227,8 @@

\end{description}

-  \noindent An instance of @{ML_functor Code_Data} provides the following
-  interface:
+  \noindent An instance of @{ML_functor Code_Data} provides the
+  following interface:

\medskip
\begin{tabular}{l}
@@ -240,8 +238,8 @@

\begin{description}

-  \item @{text change} update of current data (cached!)
-    by giving a continuation.
+  \item @{text change} update of current data (cached!) by giving a
+    continuation.

\item @{text change_yield} update with side result.