1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Tue Sep 18 08:28:47 2007 +0200
1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Tue Sep 18 10:44:02 2007 +0200
1.3 @@ -1,4 +1,3 @@
1.4 -
1.5 (* $Id$ *)
1.6
1.7 (*<*)
1.8 @@ -7,7 +6,7 @@
1.9 begin
1.10
1.11 ML {*
1.12 -CodegenSerializer.code_width := 74;
1.13 +CodeTarget.code_width := 74;
1.14 *}
1.15
1.16 syntax
1.17 @@ -189,7 +188,7 @@
1.18 *}
1.19
1.20 instance int :: semigroup
1.21 - mult_int_def: "\<And>i j \<Colon> int. i \<otimes> j \<equiv> i + j"
1.22 + mult_int_def: "i \<otimes> j \<equiv> i + j"
1.23 proof
1.24 fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
1.25 then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)" unfolding mult_int_def .
1.26 @@ -504,7 +503,7 @@
1.27 \noindent This maps to Haskell as:
1.28 *}
1.29
1.30 -export_code example in Haskell to Classes file "code_examples/"
1.31 +export_code example in Haskell module_name Classes file "code_examples/"
1.32 (* NOTE: you may use Haskell only once in this document, otherwise
1.33 you have to work in distinct subdirectories *)
1.34
1.35 @@ -514,7 +513,7 @@
1.36 \noindent The whole code in SML with explicit dictionary passing:
1.37 *}
1.38
1.39 -export_code example (*<*)in SML to Classes(*>*)in SML to Classes file "code_examples/classes.ML"
1.40 +export_code example (*<*)in SML module_name Classes(*>*)in SML module_name Classes file "code_examples/classes.ML"
1.41
1.42 text {*
1.43 \lstsml{Thy/code_examples/classes.ML}
2.1 --- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs Tue Sep 18 08:28:47 2007 +0200
2.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs Tue Sep 18 10:44:02 2007 +0200
2.3 @@ -1,25 +1,26 @@
2.4 module Classes where {
2.5
2.6
2.7 -data Nat = Zero_nat | Suc Nat;
2.8 +data Nat = Suc Classes.Nat | Zero_nat;
2.9
2.10 -data Bit = B0 | B1;
2.11 +data Bit = B1 | B0;
2.12
2.13 -nat_aux :: Integer -> Nat -> Nat;
2.14 -nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n));
2.15 +nat_aux :: Integer -> Classes.Nat -> Classes.Nat;
2.16 +nat_aux i n =
2.17 + (if i <= 0 then n else Classes.nat_aux (i - 1) (Classes.Suc n));
2.18
2.19 -nat :: Integer -> Nat;
2.20 -nat i = nat_aux i Zero_nat;
2.21 +nat :: Integer -> Classes.Nat;
2.22 +nat i = Classes.nat_aux i Classes.Zero_nat;
2.23
2.24 class Semigroup a where {
2.25 mult :: a -> a -> a;
2.26 };
2.27
2.28 -class (Semigroup a) => Monoidl a where {
2.29 +class (Classes.Semigroup a) => Monoidl a where {
2.30 neutral :: a;
2.31 };
2.32
2.33 -class (Monoidl a) => Group a where {
2.34 +class (Classes.Monoidl a) => Group a where {
2.35 inverse :: a -> a;
2.36 };
2.37
2.38 @@ -32,28 +33,28 @@
2.39 mult_int :: Integer -> Integer -> Integer;
2.40 mult_int i j = i + j;
2.41
2.42 -instance Semigroup Integer where {
2.43 - mult = mult_int;
2.44 +instance Classes.Semigroup Integer where {
2.45 + mult = Classes.mult_int;
2.46 };
2.47
2.48 -instance Monoidl Integer where {
2.49 - neutral = neutral_int;
2.50 +instance Classes.Monoidl Integer where {
2.51 + neutral = Classes.neutral_int;
2.52 };
2.53
2.54 -instance Group Integer where {
2.55 - inverse = inverse_int;
2.56 +instance Classes.Group Integer where {
2.57 + inverse = Classes.inverse_int;
2.58 };
2.59
2.60 -pow_nat :: (Group b) => Nat -> b -> b;
2.61 -pow_nat (Suc n) x = mult x (pow_nat n x);
2.62 -pow_nat Zero_nat x = neutral;
2.63 +pow_nat :: (Classes.Group b) => Classes.Nat -> b -> b;
2.64 +pow_nat (Classes.Suc n) x = Classes.mult x (Classes.pow_nat n x);
2.65 +pow_nat Classes.Zero_nat x = Classes.neutral;
2.66
2.67 -pow_int :: (Group a) => Integer -> a -> a;
2.68 +pow_int :: (Classes.Group a) => Integer -> a -> a;
2.69 pow_int k x =
2.70 - (if 0 <= k then pow_nat (nat k) x
2.71 - else inverse (pow_nat (nat (negate k)) x));
2.72 + (if 0 <= k then Classes.pow_nat (Classes.nat k) x
2.73 + else Classes.inverse (Classes.pow_nat (Classes.nat (negate k)) x));
2.74
2.75 example :: Integer;
2.76 -example = pow_int 10 (-2);
2.77 +example = Classes.pow_int 10 (-2);
2.78
2.79 }
3.1 --- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML Tue Sep 18 08:28:47 2007 +0200
3.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML Tue Sep 18 10:44:02 2007 +0200
3.3 @@ -1,9 +1,9 @@
3.4 structure Classes =
3.5 struct
3.6
3.7 -datatype nat = Zero_nat | Suc of nat;
3.8 +datatype nat = Suc of nat | Zero_nat;
3.9
3.10 -datatype bit = B0 | B1;
3.11 +datatype bit = B1 | B0;
3.12
3.13 fun nat_aux i n =
3.14 (if IntInf.<= (i, (0 : IntInf.int)) then n
4.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Tue Sep 18 08:28:47 2007 +0200
4.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Tue Sep 18 10:44:02 2007 +0200
4.3 @@ -4,7 +4,6 @@
4.4 %
4.5 \isadelimtheory
4.6 \isanewline
4.7 -\isanewline
4.8 %
4.9 \endisadelimtheory
4.10 %
4.11 @@ -172,7 +171,7 @@
4.12 \isamarkuptrue%
4.13 \ \ \ \ \isacommand{instance}\isamarkupfalse%
4.14 \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
4.15 -\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isasymColon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
4.16 +\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
4.17 %
4.18 \isadelimproof
4.19 \ \ \ \ %
4.20 @@ -733,16 +732,16 @@
4.21 \noindent This maps to Haskell as:%
4.22 \end{isamarkuptext}%
4.23 \isamarkuptrue%
4.24 -\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
4.25 -\ example\ \isakeyword{in}\ Haskell\ \isakeyword{to}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}%
4.26 +\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
4.27 +\ example\ \isakeyword{in}\ Haskell\ \isakeyword{module{\isacharunderscore}name}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}%
4.28 \begin{isamarkuptext}%
4.29 \lsthaskell{Thy/code_examples/Classes.hs}
4.30
4.31 \noindent The whole code in SML with explicit dictionary passing:%
4.32 \end{isamarkuptext}%
4.33 \isamarkuptrue%
4.34 -\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
4.35 -\ example\ \isakeyword{in}\ SML\ \isakeyword{to}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}%
4.36 +\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
4.37 +\ example\ \isakeyword{in}\ SML\ \isakeyword{module{\isacharunderscore}name}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}%
4.38 \begin{isamarkuptext}%
4.39 \lstsml{Thy/code_examples/classes.ML}%
4.40 \end{isamarkuptext}%
5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Tue Sep 18 08:28:47 2007 +0200
5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Tue Sep 18 10:44:02 2007 +0200
5.3 @@ -1198,7 +1198,7 @@
5.4 \end{description}
5.5 *}
5.6
5.7 -subsubsection {* Datatype hooks *}
5.8 +(*subsubsection {* Datatype hooks *}
5.9
5.10 text {*
5.11 Isabelle/HOL's datatype package provides a mechanism to
5.12 @@ -1311,7 +1311,9 @@
5.13 the block.
5.14
5.15 \end{description}
5.16 +*}*)
5.17
5.18 +text {*
5.19 \emph{Happy proving, happy hacking!}
5.20 *}
5.21
6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Tue Sep 18 08:28:47 2007 +0200
6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Tue Sep 18 10:44:02 2007 +0200
6.3 @@ -1707,171 +1707,8 @@
6.4 \end{isamarkuptext}%
6.5 \isamarkuptrue%
6.6 %
6.7 -\isamarkupsubsubsection{Datatype hooks%
6.8 -}
6.9 -\isamarkuptrue%
6.10 -%
6.11 \begin{isamarkuptext}%
6.12 -Isabelle/HOL's datatype package provides a mechanism to
6.13 - extend theories depending on datatype declarations:
6.14 - \emph{datatype hooks}. For example, when declaring a new
6.15 - datatype, a hook proves defining equations for equality on
6.16 - that datatype (if possible).%
6.17 -\end{isamarkuptext}%
6.18 -\isamarkuptrue%
6.19 -%
6.20 -\isadelimmlref
6.21 -%
6.22 -\endisadelimmlref
6.23 -%
6.24 -\isatagmlref
6.25 -%
6.26 -\begin{isamarkuptext}%
6.27 -\begin{mldecls}
6.28 - \indexmltype{DatatypeHooks.hook}\verb|type DatatypeHooks.hook = string list -> theory -> theory| \\
6.29 - \indexml{DatatypeHooks.add}\verb|DatatypeHooks.add: DatatypeHooks.hook -> theory -> theory|
6.30 - \end{mldecls}
6.31 -
6.32 - \begin{description}
6.33 -
6.34 - \item \verb|DatatypeHooks.hook| specifies the interface
6.35 - of \emph{datatype hooks}: a theory update
6.36 - depending on the list of newly introduced
6.37 - datatype names.
6.38 -
6.39 - \item \verb|DatatypeHooks.add| adds a hook to the
6.40 - chain of all hooks.
6.41 -
6.42 - \end{description}%
6.43 -\end{isamarkuptext}%
6.44 -\isamarkuptrue%
6.45 -%
6.46 -\endisatagmlref
6.47 -{\isafoldmlref}%
6.48 -%
6.49 -\isadelimmlref
6.50 -%
6.51 -\endisadelimmlref
6.52 -%
6.53 -\isamarkupsubsubsection{Trivial typedefs -- type copies%
6.54 -}
6.55 -\isamarkuptrue%
6.56 -%
6.57 -\begin{isamarkuptext}%
6.58 -Sometimes packages will introduce new types
6.59 - as \emph{marked type copies} similar to Haskell's
6.60 - \isa{newtype} declaration (e.g. the HOL record package)
6.61 - \emph{without} tinkering with the overhead of datatypes.
6.62 - Technically, these type copies are trivial forms of typedefs.
6.63 - Since these type copies in code generation view are nothing
6.64 - else than datatypes, they have been given a own package
6.65 - in order to faciliate code generation:%
6.66 -\end{isamarkuptext}%
6.67 -\isamarkuptrue%
6.68 -%
6.69 -\isadelimmlref
6.70 -%
6.71 -\endisadelimmlref
6.72 -%
6.73 -\isatagmlref
6.74 -%
6.75 -\begin{isamarkuptext}%
6.76 -\begin{mldecls}
6.77 - \indexmltype{TypecopyPackage.info}\verb|type TypecopyPackage.info| \\
6.78 - \indexml{TypecopyPackage.add-typecopy}\verb|TypecopyPackage.add_typecopy: |\isasep\isanewline%
6.79 -\verb| bstring * string list -> typ -> (bstring * bstring) option|\isasep\isanewline%
6.80 -\verb| -> theory -> (string * TypecopyPackage.info) * theory| \\
6.81 - \indexml{TypecopyPackage.get-typecopy-info}\verb|TypecopyPackage.get_typecopy_info: theory|\isasep\isanewline%
6.82 -\verb| -> string -> TypecopyPackage.info option| \\
6.83 - \indexml{TypecopyPackage.get-spec}\verb|TypecopyPackage.get_spec: theory -> string|\isasep\isanewline%
6.84 -\verb| -> (string * sort) list * (string * typ list) list| \\
6.85 - \indexmltype{TypecopyPackage.hook}\verb|type TypecopyPackage.hook = string * TypecopyPackage.info -> theory -> theory| \\
6.86 - \indexml{TypecopyPackage.add-hook}\verb|TypecopyPackage.add_hook: TypecopyPackage.hook -> theory -> theory| \\
6.87 - \end{mldecls}
6.88 -
6.89 - \begin{description}
6.90 -
6.91 - \item \verb|TypecopyPackage.info| a record containing
6.92 - the specification and further data of a type copy.
6.93 -
6.94 - \item \verb|TypecopyPackage.add_typecopy| defines a new
6.95 - type copy.
6.96 -
6.97 - \item \verb|TypecopyPackage.get_typecopy_info| retrieves
6.98 - data of an existing type copy.
6.99 -
6.100 - \item \verb|TypecopyPackage.get_spec| retrieves datatype-like
6.101 - specification of a type copy.
6.102 -
6.103 - \item \verb|TypecopyPackage.hook|,~\verb|TypecopyPackage.add_hook|
6.104 - provide a hook mechanism corresponding to the hook mechanism
6.105 - on datatypes.
6.106 -
6.107 - \end{description}%
6.108 -\end{isamarkuptext}%
6.109 -\isamarkuptrue%
6.110 -%
6.111 -\endisatagmlref
6.112 -{\isafoldmlref}%
6.113 -%
6.114 -\isadelimmlref
6.115 -%
6.116 -\endisadelimmlref
6.117 -%
6.118 -\isamarkupsubsubsection{Unifying type copies and datatypes%
6.119 -}
6.120 -\isamarkuptrue%
6.121 -%
6.122 -\begin{isamarkuptext}%
6.123 -Since datatypes and type copies are mapped to the same concept (datatypes)
6.124 - by code generation, the view on both is unified \qt{code types}:%
6.125 -\end{isamarkuptext}%
6.126 -\isamarkuptrue%
6.127 -%
6.128 -\isadelimmlref
6.129 -%
6.130 -\endisadelimmlref
6.131 -%
6.132 -\isatagmlref
6.133 -%
6.134 -\begin{isamarkuptext}%
6.135 -\begin{mldecls}
6.136 - \indexmltype{DatatypeCodegen.hook}\verb|type DatatypeCodegen.hook = (string * (bool * ((string * sort) list|\isasep\isanewline%
6.137 -\verb| * (string * typ list) list))) list|\isasep\isanewline%
6.138 -\verb| -> theory -> theory| \\
6.139 - \indexml{DatatypeCodegen.add-codetypes-hook-bootstrap}\verb|DatatypeCodegen.add_codetypes_hook_bootstrap: |\isasep\isanewline%
6.140 -\verb| DatatypeCodegen.hook -> theory -> theory|
6.141 - \end{mldecls}%
6.142 -\end{isamarkuptext}%
6.143 -\isamarkuptrue%
6.144 -%
6.145 -\endisatagmlref
6.146 -{\isafoldmlref}%
6.147 -%
6.148 -\isadelimmlref
6.149 -%
6.150 -\endisadelimmlref
6.151 -%
6.152 -\begin{isamarkuptext}%
6.153 -\begin{description}
6.154 -
6.155 - \item \verb|DatatypeCodegen.hook| specifies the code type hook
6.156 - interface: a theory transformation depending on a list of
6.157 - mutual recursive code types; each entry in the list
6.158 - has the structure \isa{{\isacharparenleft}name{\isacharcomma}\ {\isacharparenleft}is{\isacharunderscore}data{\isacharcomma}\ {\isacharparenleft}vars{\isacharcomma}\ cons{\isacharparenright}{\isacharparenright}{\isacharparenright}}
6.159 - where \isa{name} is the name of the code type, \isa{is{\isacharunderscore}data}
6.160 - is true iff \isa{name} is a datatype rather then a type copy,
6.161 - and \isa{{\isacharparenleft}vars{\isacharcomma}\ cons{\isacharparenright}} is the specification of the code type.
6.162 -
6.163 - \item \verb|DatatypeCodegen.add_codetypes_hook_bootstrap| adds a code
6.164 - type hook; the hook is immediately processed for all already
6.165 - existing datatypes, in blocks of mutual recursive datatypes,
6.166 - where all datatypes a block depends on are processed before
6.167 - the block.
6.168 -
6.169 - \end{description}
6.170 -
6.171 - \emph{Happy proving, happy hacking!}%
6.172 +\emph{Happy proving, happy hacking!}%
6.173 \end{isamarkuptext}%
6.174 \isamarkuptrue%
6.175 %
7.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Tue Sep 18 08:28:47 2007 +0200
7.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Tue Sep 18 10:44:02 2007 +0200
7.3 @@ -10,7 +10,7 @@
7.4 heada (x : xs) = x;
7.5 heada [] = Codegen.nulla;
7.6
7.7 -instance Codegen.Null (Maybe b) where {
7.8 +instance Codegen.Null (Maybe a) where {
7.9 nulla = Nothing;
7.10 };
7.11
8.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Tue Sep 18 08:28:47 2007 +0200
8.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Tue Sep 18 10:44:02 2007 +0200
8.3 @@ -14,7 +14,7 @@
8.4 fun head B_ (x :: xs) = x
8.5 | head B_ [] = null B_;
8.6
8.7 -fun null_option () = {null = NONE} : ('b option) null;
8.8 +fun null_option () = {null = NONE} : ('a option) null;
8.9
8.10 val dummy : Nat.nat option =
8.11 head (null_option ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
9.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml Tue Sep 18 08:28:47 2007 +0200
9.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml Tue Sep 18 10:44:02 2007 +0200
9.3 @@ -14,7 +14,7 @@
9.4 let rec head _B = function x :: xs -> x
9.5 | [] -> null _B;;
9.6
9.7 -let null_option () = ({null = None} : ('b option) null);;
9.8 +let null_option () = ({null = None} : ('a option) null);;
9.9
9.10 let rec dummy
9.11 = head (null_option ()) [Some (Nat.Suc Nat.Zero_nat); None];;
10.1 --- a/doc-src/manual.bib Tue Sep 18 08:28:47 2007 +0200
10.2 +++ b/doc-src/manual.bib Tue Sep 18 10:44:02 2007 +0200
10.3 @@ -444,15 +444,23 @@
10.4 @InProceedings{Haftmann-Wenzel:2006:classes,
10.5 author = {Florian Haftmann and Makarius Wenzel},
10.6 title = {Constructive Type Classes in {Isabelle}},
10.7 - year = 2006,
10.8 - note = {To appear; \url{http://www4.in.tum.de/~haftmann/pdf/constructive_type_classes_haftmann_wenzel.pdf}}
10.9 + editor = {T. Altenkirch and C. McBride},
10.10 + booktitle = {Types for Proofs and Programs, TYPES 2006},
10.11 + publisher = {Springer},
10.12 + series = {LNCS},
10.13 + volume = {4502},
10.14 + year = {2007}
10.15 }
10.16
10.17 @TechReport{Haftmann-Nipkow:2007:codegen,
10.18 author = {Florian Haftmann and Tobias Nipkow},
10.19 title = {A Code Generator Framework for {Isabelle/HOL}},
10.20 - year = 2007,
10.21 - note = {\url{http://www4.in.tum.de/~haftmann/pdf/codegen_isabelle_haftmann_nipkow_16pp.pdf}}
10.22 + editor = {Klaus Schneider and Jens Brandt},
10.23 + booktitle = {Theorem Proving in Higher Order Logics: Emerging Trends Proceedings},
10.24 + month = {08},
10.25 + year = {2007},
10.26 + institution = {Department of Computer Science, University of Kaiserslautern},
10.27 + number = {364/07}
10.28 }
10.29
10.30 @manual{isabelle-classes,