--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Aug 09 11:39:29 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Aug 09 15:52:38 2007 +0200
@@ -444,7 +444,7 @@
\item the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}
for exhaustive syntax diagrams.
- \item or \fixme[ref] which deals with foundational issues
+ \item or \cite{Haftmann-Nipkow:2007:codegen} which deals with foundational issues
of the code generator framework.
\end{itemize}
@@ -469,10 +469,10 @@
\item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char"},
but also offers treatment of character codes; includes
@{text "Pretty_Int"}.
- \item[@{text "Executable_Set"}] allows to generate code
+ \item[@{text "Executable_Set"}] \label{exec_set} allows to generate code
for finite sets using lists.
- \item[@{text "Executable_Rat"}] \label{exec_rat} implements rational
- numbers as triples @{text "(sign, enumerator, denominator)"}.
+ \item[@{text "Executable_Rat"}] implements rational
+ numbers.
\item[@{text "Executable_Real"}] implements a subset of real numbers,
namly those representable by rational numbers.
\item[@{text "Efficient_Nat"}] \label{eff_nat} implements natural numbers by integers,
@@ -1082,7 +1082,7 @@
Another axiomatic extension is code generation
for abstracted types. For this, the
- @{text "ExecutableRat"} (see \secref{exec_rat})
+ @{text "Executable_Set"} theory (see \secref{exec_set})
forms a good example.
*}
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Aug 09 11:39:29 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Aug 09 15:52:38 2007 +0200
@@ -562,7 +562,7 @@
\item the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}
for exhaustive syntax diagrams.
- \item or \fixme[ref] which deals with foundational issues
+ \item or \cite{Haftmann-Nipkow:2007:codegen} which deals with foundational issues
of the code generator framework.
\end{itemize}%
@@ -1535,7 +1535,7 @@
Another axiomatic extension is code generation
for abstracted types. For this, the
- \isa{ExecutableRat} (see \secref{exec_rat})
+ \isa{Executable{\isacharunderscore}Rat} theory (see \secref{exec_rat})
forms a good example.%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Thu Aug 09 11:39:29 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Thu Aug 09 15:52:38 2007 +0200
@@ -3,6 +3,9 @@
datatype nat = Zero_nat | Suc of nat;
+fun nat_case f1 f2 Zero_nat = f1
+ | nat_case f1 f2 (Suc nat) = f2 nat;
+
fun plus_nat (Suc m) n = plus_nat m (Suc n)
| plus_nat Zero_nat n = n;
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Thu Aug 09 11:39:29 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Thu Aug 09 15:52:38 2007 +0200
@@ -4,22 +4,16 @@
type 'a eq = {eq : 'a -> 'a -> bool};
fun eq (A_:'a eq) = #eq A_;
-end; (*struct HOL*)
-
-structure Orderings =
-struct
-
type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
fun less_eq (A_:'a ord) = #less_eq A_;
fun less (A_:'a ord) = #less A_;
-end; (*struct Orderings*)
+end; (*struct HOL*)
structure Codegen =
struct
fun less_eq_product (A1_, A2_) B_ (x1, y1) (x2, y2) =
- Orderings.less A2_ x1 x2 orelse
- HOL.eq A1_ x1 x2 andalso Orderings.less_eq B_ y1 y2;
+ HOL.less A2_ x1 x2 orelse HOL.eq A1_ x1 x2 andalso HOL.less_eq B_ y1 y2;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Thu Aug 09 11:39:29 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Thu Aug 09 15:52:38 2007 +0200
@@ -11,11 +11,16 @@
fun plus_nat (Suc m) n = plus_nat m (Suc n)
| plus_nat Zero_nat n = n;
+fun prod_case f1 (a, b) = f1 a b;
+
end; (*struct Nat*)
structure List =
struct
+fun list_case f1 f2 [] = f1
+ | list_case f1 f2 (a :: lista) = f2 a lista;
+
fun zip xs (y :: ys) =
(case xs of [] => [] | z :: zs => (z, y) :: zip zs ys)
| zip xs [] = [];
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Thu Aug 09 11:39:29 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Thu Aug 09 15:52:38 2007 +0200
@@ -1,3 +1,10 @@
+structure HOL =
+struct
+
+fun leta s f = f s;
+
+end; (*struct HOL*)
+
structure Nat =
struct
@@ -12,6 +19,8 @@
| minus_nat Zero_nat n = Zero_nat
| minus_nat m Zero_nat = m;
+fun prod_case f1 (a, b) = f1 a b;
+
end; (*struct Nat*)
structure Codegen =
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Thu Aug 09 11:39:29 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Thu Aug 09 15:52:38 2007 +0200
@@ -4,20 +4,20 @@
type 'a eq = {eq : 'a -> 'a -> bool};
fun eq (A_:'a eq) = #eq A_;
+type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
+fun less_eq (A_:'a ord) = #less_eq A_;
+fun less (A_:'a ord) = #less A_;
+
end; (*struct HOL*)
structure Orderings =
struct
-type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
-fun less_eq (A_:'a ord) = #less_eq A_;
-fun less (A_:'a ord) = #less A_;
+type 'a order = {Orderings__ord_order : 'a HOL.ord};
+fun ord_order (A_:'a order) = #Orderings__ord_order A_;
-type 'a order = {Orderings__order_ord : 'a ord};
-fun order_ord (A_:'a order) = #Orderings__order_ord A_;
-
-type 'a linorder = {Orderings__linorder_order : 'a order};
-fun linorder_order (A_:'a linorder) = #Orderings__linorder_order A_;
+type 'a linorder = {Orderings__order_linorder : 'a order};
+fun order_linorder (A_:'a linorder) = #Orderings__order_linorder A_;
end; (*struct Orderings*)
@@ -38,12 +38,11 @@
and less_eq_nat (Suc n) m = less_nat n m
| less_eq_nat Zero_nat m = true;
-val ord_nat = {less_eq = less_eq_nat, less = less_nat} :
- nat Orderings.ord;
+val ord_nat = {less_eq = less_eq_nat, less = less_nat} : nat HOL.ord;
-val order_nat = {Orderings__order_ord = ord_nat} : nat Orderings.order;
+val order_nat = {Orderings__ord_order = ord_nat} : nat Orderings.order;
-val linorder_nat = {Orderings__linorder_order = order_nat} :
+val linorder_nat = {Orderings__order_linorder = order_nat} :
nat Orderings.linorder;
end; (*struct Nat*)
@@ -55,14 +54,14 @@
Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree;
fun update (C1_, C2_) (it, entry) (Branch (t1, key, t2)) =
- (if Orderings.less_eq
- ((Orderings.order_ord o Orderings.linorder_order) C2_) it key
+ (if HOL.less_eq ((Orderings.ord_order o Orderings.order_linorder) C2_)
+ it key
then Branch (update (C1_, C2_) (it, entry) t1, key, t2)
else Branch (t1, key, update (C1_, C2_) (it, entry) t2))
| update (C1_, C2_) (it, entry) (Leaf (key, vala)) =
(if HOL.eq C1_ it key then Leaf (key, entry)
- else (if Orderings.less_eq
- ((Orderings.order_ord o Orderings.linorder_order) C2_) it
+ else (if HOL.less_eq
+ ((Orderings.ord_order o Orderings.order_linorder) C2_) it
key
then Branch (Leaf (it, entry), it, Leaf (key, vala))
else Branch (Leaf (key, vala), it, Leaf (it, entry))));
--- a/doc-src/manual.bib Thu Aug 09 11:39:29 2007 +0200
+++ b/doc-src/manual.bib Thu Aug 09 15:52:38 2007 +0200
@@ -444,21 +444,30 @@
@InProceedings{Haftmann-Wenzel:2006:classes,
author = {Florian Haftmann and Makarius Wenzel},
title = {Constructive Type Classes in {Isabelle}},
- year = 2006,
- note = {To appear}
+ year = 2006,
+ note = {To appear; \url{http://www4.in.tum.de/~haftmann/pdf/constructive_type_classes_haftmann_wenzel.pdf}}
+}
+
+@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}}
}
@manual{isabelle-classes,
- author = {Florian Haftmann},
- title = {Haskell-style type classes with {Isabelle}/{Isar}},
- institution = TUM,
- note = {\url{http://isabelle.in.tum.de/doc/classes.pdf}}}
+ author = {Florian Haftmann},
+ title = {Haskell-style type classes with {Isabelle}/{Isar}},
+ institution = TUM,
+ note = {\url{http://isabelle.in.tum.de/doc/classes.pdf}}
+}
@manual{isabelle-codegen,
- author = {Florian Haftmann},
- title = {Code generation from Isabelle theories},
- institution = TUM,
- note = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}}}
+ author = {Florian Haftmann},
+ title = {Code generation from Isabelle theories},
+ institution = TUM,
+ note = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}}
+}
@Book{halmos60,
author = {Paul R. Halmos},