# HG changeset patch
# User haftmann
# Date 1190105042 -7200
# Node ID 33137422d7fd4d3fac4c30a307227f40e1ecf09c
# Parent  cc6768509ed3d4c22efaed960beca0270cd7515a
updated

diff -r cc6768509ed3 -r 33137422d7fd doc-src/IsarAdvanced/Classes/Thy/Classes.thy
--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Tue Sep 18 08:28:47 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Tue Sep 18 10:44:02 2007 +0200
@@ -1,4 +1,3 @@
-
 (* $Id$ *)
 
 (*<*)
@@ -7,7 +6,7 @@
 begin
 
 ML {*
-CodegenSerializer.code_width := 74;
+CodeTarget.code_width := 74;
 *}
 
 syntax
@@ -189,7 +188,7 @@
 *}
 
     instance int :: semigroup
-      mult_int_def: "\<And>i j \<Colon> int. i \<otimes> j \<equiv> i + j"
+      mult_int_def: "i \<otimes> j \<equiv> i + j"
     proof
       fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
       then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)" unfolding mult_int_def .
@@ -504,7 +503,7 @@
   \noindent This maps to Haskell as:
 *}
 
-export_code example in Haskell to Classes file "code_examples/"
+export_code example in Haskell module_name Classes file "code_examples/"
   (* NOTE: you may use Haskell only once in this document, otherwise
   you have to work in distinct subdirectories *)
 
@@ -514,7 +513,7 @@
   \noindent The whole code in SML with explicit dictionary passing:
 *}
 
-export_code example (*<*)in SML to Classes(*>*)in SML to Classes file "code_examples/classes.ML"
+export_code example (*<*)in SML module_name Classes(*>*)in SML module_name Classes file "code_examples/classes.ML"
 
 text {*
   \lstsml{Thy/code_examples/classes.ML}
diff -r cc6768509ed3 -r 33137422d7fd doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs
--- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs	Tue Sep 18 08:28:47 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs	Tue Sep 18 10:44:02 2007 +0200
@@ -1,25 +1,26 @@
 module Classes where {
 
 
-data Nat = Zero_nat | Suc Nat;
+data Nat = Suc Classes.Nat | Zero_nat;
 
-data Bit = B0 | B1;
+data Bit = B1 | B0;
 
-nat_aux :: Integer -> Nat -> Nat;
-nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n));
+nat_aux :: Integer -> Classes.Nat -> Classes.Nat;
+nat_aux i n =
+  (if i <= 0 then n else Classes.nat_aux (i - 1) (Classes.Suc n));
 
-nat :: Integer -> Nat;
-nat i = nat_aux i Zero_nat;
+nat :: Integer -> Classes.Nat;
+nat i = Classes.nat_aux i Classes.Zero_nat;
 
 class Semigroup a where {
   mult :: a -> a -> a;
 };
 
-class (Semigroup a) => Monoidl a where {
+class (Classes.Semigroup a) => Monoidl a where {
   neutral :: a;
 };
 
-class (Monoidl a) => Group a where {
+class (Classes.Monoidl a) => Group a where {
   inverse :: a -> a;
 };
 
@@ -32,28 +33,28 @@
 mult_int :: Integer -> Integer -> Integer;
 mult_int i j = i + j;
 
-instance Semigroup Integer where {
-  mult = mult_int;
+instance Classes.Semigroup Integer where {
+  mult = Classes.mult_int;
 };
 
-instance Monoidl Integer where {
-  neutral = neutral_int;
+instance Classes.Monoidl Integer where {
+  neutral = Classes.neutral_int;
 };
 
-instance Group Integer where {
-  inverse = inverse_int;
+instance Classes.Group Integer where {
+  inverse = Classes.inverse_int;
 };
 
-pow_nat :: (Group b) => Nat -> b -> b;
-pow_nat (Suc n) x = mult x (pow_nat n x);
-pow_nat Zero_nat x = neutral;
+pow_nat :: (Classes.Group b) => Classes.Nat -> b -> b;
+pow_nat (Classes.Suc n) x = Classes.mult x (Classes.pow_nat n x);
+pow_nat Classes.Zero_nat x = Classes.neutral;
 
-pow_int :: (Group a) => Integer -> a -> a;
+pow_int :: (Classes.Group a) => Integer -> a -> a;
 pow_int k x =
-  (if 0 <= k then pow_nat (nat k) x
-    else inverse (pow_nat (nat (negate k)) x));
+  (if 0 <= k then Classes.pow_nat (Classes.nat k) x
+    else Classes.inverse (Classes.pow_nat (Classes.nat (negate k)) x));
 
 example :: Integer;
-example = pow_int 10 (-2);
+example = Classes.pow_int 10 (-2);
 
 }
diff -r cc6768509ed3 -r 33137422d7fd doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML
--- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML	Tue Sep 18 08:28:47 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML	Tue Sep 18 10:44:02 2007 +0200
@@ -1,9 +1,9 @@
 structure Classes = 
 struct
 
-datatype nat = Zero_nat | Suc of nat;
+datatype nat = Suc of nat | Zero_nat;
 
-datatype bit = B0 | B1;
+datatype bit = B1 | B0;
 
 fun nat_aux i n =
   (if IntInf.<= (i, (0 : IntInf.int)) then n
diff -r cc6768509ed3 -r 33137422d7fd doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Tue Sep 18 08:28:47 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Tue Sep 18 10:44:02 2007 +0200
@@ -4,7 +4,6 @@
 %
 \isadelimtheory
 \isanewline
-\isanewline
 %
 \endisadelimtheory
 %
@@ -172,7 +171,7 @@
 \isamarkuptrue%
 \ \ \ \ \isacommand{instance}\isamarkupfalse%
 \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
-\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isasymColon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
 %
 \isadelimproof
 \ \ \ \ %
@@ -733,16 +732,16 @@
 \noindent This maps to Haskell as:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ example\ \isakeyword{in}\ Haskell\ \isakeyword{to}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
+\ example\ \isakeyword{in}\ Haskell\ \isakeyword{module{\isacharunderscore}name}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lsthaskell{Thy/code_examples/Classes.hs}
 
   \noindent The whole code in SML with explicit dictionary passing:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ example\ \isakeyword{in}\ SML\ \isakeyword{to}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
+\ example\ \isakeyword{in}\ SML\ \isakeyword{module{\isacharunderscore}name}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lstsml{Thy/code_examples/classes.ML}%
 \end{isamarkuptext}%
diff -r cc6768509ed3 -r 33137422d7fd doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Sep 18 08:28:47 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Sep 18 10:44:02 2007 +0200
@@ -1198,7 +1198,7 @@
   \end{description}
 *}
 
-subsubsection {* Datatype hooks *}
+(*subsubsection {* Datatype hooks *}
 
 text {*
   Isabelle/HOL's datatype package provides a mechanism to
@@ -1311,7 +1311,9 @@
      the block.
 
   \end{description}
+*}*)
 
+text {*
   \emph{Happy proving, happy hacking!}
 *}
 
diff -r cc6768509ed3 -r 33137422d7fd doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Tue Sep 18 08:28:47 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Tue Sep 18 10:44:02 2007 +0200
@@ -1707,171 +1707,8 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsubsection{Datatype hooks%
-}
-\isamarkuptrue%
-%
 \begin{isamarkuptext}%
-Isabelle/HOL's datatype package provides a mechanism to
-  extend theories depending on datatype declarations:
-  \emph{datatype hooks}.  For example, when declaring a new
-  datatype, a hook proves defining equations for equality on
-  that datatype (if possible).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexmltype{DatatypeHooks.hook}\verb|type DatatypeHooks.hook = string list -> theory -> theory| \\
-  \indexml{DatatypeHooks.add}\verb|DatatypeHooks.add: DatatypeHooks.hook -> theory -> theory|
-  \end{mldecls}
-
-  \begin{description}
-
-  \item \verb|DatatypeHooks.hook| specifies the interface
-     of \emph{datatype hooks}: a theory update
-     depending on the list of newly introduced
-     datatype names.
-
-  \item \verb|DatatypeHooks.add| adds a hook to the
-     chain of all hooks.
-
-  \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isamarkupsubsubsection{Trivial typedefs -- type copies%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Sometimes packages will introduce new types
-  as \emph{marked type copies} similar to Haskell's
-  \isa{newtype} declaration (e.g. the HOL record package)
-  \emph{without} tinkering with the overhead of datatypes.
-  Technically, these type copies are trivial forms of typedefs.
-  Since these type copies in code generation view are nothing
-  else than datatypes, they have been given a own package
-  in order to faciliate code generation:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexmltype{TypecopyPackage.info}\verb|type TypecopyPackage.info| \\
-  \indexml{TypecopyPackage.add-typecopy}\verb|TypecopyPackage.add_typecopy: |\isasep\isanewline%
-\verb|    bstring * string list -> typ -> (bstring * bstring) option|\isasep\isanewline%
-\verb|    -> theory -> (string * TypecopyPackage.info) * theory| \\
-  \indexml{TypecopyPackage.get-typecopy-info}\verb|TypecopyPackage.get_typecopy_info: theory|\isasep\isanewline%
-\verb|    -> string -> TypecopyPackage.info option| \\
-  \indexml{TypecopyPackage.get-spec}\verb|TypecopyPackage.get_spec: theory -> string|\isasep\isanewline%
-\verb|    -> (string * sort) list * (string * typ list) list| \\
-  \indexmltype{TypecopyPackage.hook}\verb|type TypecopyPackage.hook = string * TypecopyPackage.info -> theory -> theory| \\
-  \indexml{TypecopyPackage.add-hook}\verb|TypecopyPackage.add_hook: TypecopyPackage.hook -> theory -> theory| \\
-  \end{mldecls}
-
-  \begin{description}
-
-  \item \verb|TypecopyPackage.info| a record containing
-     the specification and further data of a type copy.
-
-  \item \verb|TypecopyPackage.add_typecopy| defines a new
-     type copy.
-
-  \item \verb|TypecopyPackage.get_typecopy_info| retrieves
-     data of an existing type copy.
-
-  \item \verb|TypecopyPackage.get_spec| retrieves datatype-like
-     specification of a type copy.
-
-  \item \verb|TypecopyPackage.hook|,~\verb|TypecopyPackage.add_hook|
-     provide a hook mechanism corresponding to the hook mechanism
-     on datatypes.
-
-  \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isamarkupsubsubsection{Unifying type copies and datatypes%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Since datatypes and type copies are mapped to the same concept (datatypes)
-  by code generation, the view on both is unified \qt{code types}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexmltype{DatatypeCodegen.hook}\verb|type DatatypeCodegen.hook = (string * (bool * ((string * sort) list|\isasep\isanewline%
-\verb|    * (string * typ list) list))) list|\isasep\isanewline%
-\verb|    -> theory -> theory| \\
-  \indexml{DatatypeCodegen.add-codetypes-hook-bootstrap}\verb|DatatypeCodegen.add_codetypes_hook_bootstrap: |\isasep\isanewline%
-\verb|      DatatypeCodegen.hook -> theory -> theory|
-  \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\begin{isamarkuptext}%
-\begin{description}
-
-  \item \verb|DatatypeCodegen.hook| specifies the code type hook
-     interface: a theory transformation depending on a list of
-     mutual recursive code types; each entry in the list
-     has the structure \isa{{\isacharparenleft}name{\isacharcomma}\ {\isacharparenleft}is{\isacharunderscore}data{\isacharcomma}\ {\isacharparenleft}vars{\isacharcomma}\ cons{\isacharparenright}{\isacharparenright}{\isacharparenright}}
-     where \isa{name} is the name of the code type, \isa{is{\isacharunderscore}data}
-     is true iff \isa{name} is a datatype rather then a type copy,
-     and \isa{{\isacharparenleft}vars{\isacharcomma}\ cons{\isacharparenright}} is the specification of the code type.
-
-  \item \verb|DatatypeCodegen.add_codetypes_hook_bootstrap| adds a code
-     type hook;  the hook is immediately processed for all already
-     existing datatypes, in blocks of mutual recursive datatypes,
-     where all datatypes a block depends on are processed before
-     the block.
-
-  \end{description}
-
-  \emph{Happy proving, happy hacking!}%
+\emph{Happy proving, happy hacking!}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r cc6768509ed3 -r 33137422d7fd doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Tue Sep 18 08:28:47 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Tue Sep 18 10:44:02 2007 +0200
@@ -10,7 +10,7 @@
 heada (x : xs) = x;
 heada [] = Codegen.nulla;
 
-instance Codegen.Null (Maybe b) where {
+instance Codegen.Null (Maybe a) where {
   nulla = Nothing;
 };
 
diff -r cc6768509ed3 -r 33137422d7fd doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Tue Sep 18 08:28:47 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Tue Sep 18 10:44:02 2007 +0200
@@ -14,7 +14,7 @@
 fun head B_ (x :: xs) = x
   | head B_ [] = null B_;
 
-fun null_option () = {null = NONE} : ('b option) null;
+fun null_option () = {null = NONE} : ('a option) null;
 
 val dummy : Nat.nat option =
   head (null_option ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
diff -r cc6768509ed3 -r 33137422d7fd doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Tue Sep 18 08:28:47 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Tue Sep 18 10:44:02 2007 +0200
@@ -14,7 +14,7 @@
 let rec head _B = function x :: xs -> x
                   | [] -> null _B;;
 
-let null_option () = ({null = None} : ('b option) null);;
+let null_option () = ({null = None} : ('a option) null);;
 
 let rec dummy
   = head (null_option ()) [Some (Nat.Suc Nat.Zero_nat); None];;
diff -r cc6768509ed3 -r 33137422d7fd doc-src/manual.bib
--- a/doc-src/manual.bib	Tue Sep 18 08:28:47 2007 +0200
+++ b/doc-src/manual.bib	Tue Sep 18 10:44:02 2007 +0200
@@ -444,15 +444,23 @@
 @InProceedings{Haftmann-Wenzel:2006:classes,
   author        = {Florian Haftmann and Makarius Wenzel},
   title         = {Constructive Type Classes in {Isabelle}},
-  year          = 2006,
-  note          = {To appear; \url{http://www4.in.tum.de/~haftmann/pdf/constructive_type_classes_haftmann_wenzel.pdf}}
+  editor        = {T. Altenkirch and C. McBride},
+  booktitle     = {Types for Proofs and Programs, TYPES 2006},
+  publisher     = {Springer},
+  series        = {LNCS},
+  volume        = {4502},
+  year          = {2007}
 }
 
 @TechReport{Haftmann-Nipkow:2007:codegen,
   author        = {Florian Haftmann and Tobias Nipkow},
   title         = {A Code Generator Framework for {Isabelle/HOL}},
-  year          = 2007,
-  note          = {\url{http://www4.in.tum.de/~haftmann/pdf/codegen_isabelle_haftmann_nipkow_16pp.pdf}}
+  editor        = {Klaus Schneider and Jens Brandt},
+  booktitle     = {Theorem Proving in Higher Order Logics: Emerging Trends Proceedings},
+  month         = {08},
+  year          = {2007},
+  institution   = {Department of Computer Science, University of Kaiserslautern},
+  number        = {364/07}
 }
 
 @manual{isabelle-classes,