1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Aug 09 11:39:29 2007 +0200
1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Aug 09 15:52:38 2007 +0200
1.3 @@ -444,7 +444,7 @@
1.4
1.5 \item the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}
1.6 for exhaustive syntax diagrams.
1.7 - \item or \fixme[ref] which deals with foundational issues
1.8 + \item or \cite{Haftmann-Nipkow:2007:codegen} which deals with foundational issues
1.9 of the code generator framework.
1.10
1.11 \end{itemize}
1.12 @@ -469,10 +469,10 @@
1.13 \item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char"},
1.14 but also offers treatment of character codes; includes
1.15 @{text "Pretty_Int"}.
1.16 - \item[@{text "Executable_Set"}] allows to generate code
1.17 + \item[@{text "Executable_Set"}] \label{exec_set} allows to generate code
1.18 for finite sets using lists.
1.19 - \item[@{text "Executable_Rat"}] \label{exec_rat} implements rational
1.20 - numbers as triples @{text "(sign, enumerator, denominator)"}.
1.21 + \item[@{text "Executable_Rat"}] implements rational
1.22 + numbers.
1.23 \item[@{text "Executable_Real"}] implements a subset of real numbers,
1.24 namly those representable by rational numbers.
1.25 \item[@{text "Efficient_Nat"}] \label{eff_nat} implements natural numbers by integers,
1.26 @@ -1082,7 +1082,7 @@
1.27
1.28 Another axiomatic extension is code generation
1.29 for abstracted types. For this, the
1.30 - @{text "ExecutableRat"} (see \secref{exec_rat})
1.31 + @{text "Executable_Set"} theory (see \secref{exec_set})
1.32 forms a good example.
1.33 *}
1.34
2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Aug 09 11:39:29 2007 +0200
2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Aug 09 15:52:38 2007 +0200
2.3 @@ -562,7 +562,7 @@
2.4
2.5 \item the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}
2.6 for exhaustive syntax diagrams.
2.7 - \item or \fixme[ref] which deals with foundational issues
2.8 + \item or \cite{Haftmann-Nipkow:2007:codegen} which deals with foundational issues
2.9 of the code generator framework.
2.10
2.11 \end{itemize}%
2.12 @@ -1535,7 +1535,7 @@
2.13
2.14 Another axiomatic extension is code generation
2.15 for abstracted types. For this, the
2.16 - \isa{ExecutableRat} (see \secref{exec_rat})
2.17 + \isa{Executable{\isacharunderscore}Rat} theory (see \secref{exec_rat})
2.18 forms a good example.%
2.19 \end{isamarkuptext}%
2.20 \isamarkuptrue%
3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Thu Aug 09 11:39:29 2007 +0200
3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Thu Aug 09 15:52:38 2007 +0200
3.3 @@ -3,6 +3,9 @@
3.4
3.5 datatype nat = Zero_nat | Suc of nat;
3.6
3.7 +fun nat_case f1 f2 Zero_nat = f1
3.8 + | nat_case f1 f2 (Suc nat) = f2 nat;
3.9 +
3.10 fun plus_nat (Suc m) n = plus_nat m (Suc n)
3.11 | plus_nat Zero_nat n = n;
3.12
4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Thu Aug 09 11:39:29 2007 +0200
4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Thu Aug 09 15:52:38 2007 +0200
4.3 @@ -4,22 +4,16 @@
4.4 type 'a eq = {eq : 'a -> 'a -> bool};
4.5 fun eq (A_:'a eq) = #eq A_;
4.6
4.7 -end; (*struct HOL*)
4.8 -
4.9 -structure Orderings =
4.10 -struct
4.11 -
4.12 type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
4.13 fun less_eq (A_:'a ord) = #less_eq A_;
4.14 fun less (A_:'a ord) = #less A_;
4.15
4.16 -end; (*struct Orderings*)
4.17 +end; (*struct HOL*)
4.18
4.19 structure Codegen =
4.20 struct
4.21
4.22 fun less_eq_product (A1_, A2_) B_ (x1, y1) (x2, y2) =
4.23 - Orderings.less A2_ x1 x2 orelse
4.24 - HOL.eq A1_ x1 x2 andalso Orderings.less_eq B_ y1 y2;
4.25 + HOL.less A2_ x1 x2 orelse HOL.eq A1_ x1 x2 andalso HOL.less_eq B_ y1 y2;
4.26
4.27 end; (*struct Codegen*)
5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Thu Aug 09 11:39:29 2007 +0200
5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Thu Aug 09 15:52:38 2007 +0200
5.3 @@ -11,11 +11,16 @@
5.4 fun plus_nat (Suc m) n = plus_nat m (Suc n)
5.5 | plus_nat Zero_nat n = n;
5.6
5.7 +fun prod_case f1 (a, b) = f1 a b;
5.8 +
5.9 end; (*struct Nat*)
5.10
5.11 structure List =
5.12 struct
5.13
5.14 +fun list_case f1 f2 [] = f1
5.15 + | list_case f1 f2 (a :: lista) = f2 a lista;
5.16 +
5.17 fun zip xs (y :: ys) =
5.18 (case xs of [] => [] | z :: zs => (z, y) :: zip zs ys)
5.19 | zip xs [] = [];
6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Thu Aug 09 11:39:29 2007 +0200
6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Thu Aug 09 15:52:38 2007 +0200
6.3 @@ -1,3 +1,10 @@
6.4 +structure HOL =
6.5 +struct
6.6 +
6.7 +fun leta s f = f s;
6.8 +
6.9 +end; (*struct HOL*)
6.10 +
6.11 structure Nat =
6.12 struct
6.13
6.14 @@ -12,6 +19,8 @@
6.15 | minus_nat Zero_nat n = Zero_nat
6.16 | minus_nat m Zero_nat = m;
6.17
6.18 +fun prod_case f1 (a, b) = f1 a b;
6.19 +
6.20 end; (*struct Nat*)
6.21
6.22 structure Codegen =
7.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Thu Aug 09 11:39:29 2007 +0200
7.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Thu Aug 09 15:52:38 2007 +0200
7.3 @@ -4,20 +4,20 @@
7.4 type 'a eq = {eq : 'a -> 'a -> bool};
7.5 fun eq (A_:'a eq) = #eq A_;
7.6
7.7 +type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
7.8 +fun less_eq (A_:'a ord) = #less_eq A_;
7.9 +fun less (A_:'a ord) = #less A_;
7.10 +
7.11 end; (*struct HOL*)
7.12
7.13 structure Orderings =
7.14 struct
7.15
7.16 -type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
7.17 -fun less_eq (A_:'a ord) = #less_eq A_;
7.18 -fun less (A_:'a ord) = #less A_;
7.19 +type 'a order = {Orderings__ord_order : 'a HOL.ord};
7.20 +fun ord_order (A_:'a order) = #Orderings__ord_order A_;
7.21
7.22 -type 'a order = {Orderings__order_ord : 'a ord};
7.23 -fun order_ord (A_:'a order) = #Orderings__order_ord A_;
7.24 -
7.25 -type 'a linorder = {Orderings__linorder_order : 'a order};
7.26 -fun linorder_order (A_:'a linorder) = #Orderings__linorder_order A_;
7.27 +type 'a linorder = {Orderings__order_linorder : 'a order};
7.28 +fun order_linorder (A_:'a linorder) = #Orderings__order_linorder A_;
7.29
7.30 end; (*struct Orderings*)
7.31
7.32 @@ -38,12 +38,11 @@
7.33 and less_eq_nat (Suc n) m = less_nat n m
7.34 | less_eq_nat Zero_nat m = true;
7.35
7.36 -val ord_nat = {less_eq = less_eq_nat, less = less_nat} :
7.37 - nat Orderings.ord;
7.38 +val ord_nat = {less_eq = less_eq_nat, less = less_nat} : nat HOL.ord;
7.39
7.40 -val order_nat = {Orderings__order_ord = ord_nat} : nat Orderings.order;
7.41 +val order_nat = {Orderings__ord_order = ord_nat} : nat Orderings.order;
7.42
7.43 -val linorder_nat = {Orderings__linorder_order = order_nat} :
7.44 +val linorder_nat = {Orderings__order_linorder = order_nat} :
7.45 nat Orderings.linorder;
7.46
7.47 end; (*struct Nat*)
7.48 @@ -55,14 +54,14 @@
7.49 Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree;
7.50
7.51 fun update (C1_, C2_) (it, entry) (Branch (t1, key, t2)) =
7.52 - (if Orderings.less_eq
7.53 - ((Orderings.order_ord o Orderings.linorder_order) C2_) it key
7.54 + (if HOL.less_eq ((Orderings.ord_order o Orderings.order_linorder) C2_)
7.55 + it key
7.56 then Branch (update (C1_, C2_) (it, entry) t1, key, t2)
7.57 else Branch (t1, key, update (C1_, C2_) (it, entry) t2))
7.58 | update (C1_, C2_) (it, entry) (Leaf (key, vala)) =
7.59 (if HOL.eq C1_ it key then Leaf (key, entry)
7.60 - else (if Orderings.less_eq
7.61 - ((Orderings.order_ord o Orderings.linorder_order) C2_) it
7.62 + else (if HOL.less_eq
7.63 + ((Orderings.ord_order o Orderings.order_linorder) C2_) it
7.64 key
7.65 then Branch (Leaf (it, entry), it, Leaf (key, vala))
7.66 else Branch (Leaf (key, vala), it, Leaf (it, entry))));
8.1 --- a/doc-src/manual.bib Thu Aug 09 11:39:29 2007 +0200
8.2 +++ b/doc-src/manual.bib Thu Aug 09 15:52:38 2007 +0200
8.3 @@ -444,21 +444,30 @@
8.4 @InProceedings{Haftmann-Wenzel:2006:classes,
8.5 author = {Florian Haftmann and Makarius Wenzel},
8.6 title = {Constructive Type Classes in {Isabelle}},
8.7 - year = 2006,
8.8 - note = {To appear}
8.9 + year = 2006,
8.10 + note = {To appear; \url{http://www4.in.tum.de/~haftmann/pdf/constructive_type_classes_haftmann_wenzel.pdf}}
8.11 +}
8.12 +
8.13 +@TechReport{Haftmann-Nipkow:2007:codegen,
8.14 + author = {Florian Haftmann and Tobias Nipkow},
8.15 + title = {A Code Generator Framework for {Isabelle/HOL}},
8.16 + year = 2007,
8.17 + note = {\url{http://www4.in.tum.de/~haftmann/pdf/codegen_isabelle_haftmann_nipkow_16pp.pdf}}
8.18 }
8.19
8.20 @manual{isabelle-classes,
8.21 - author = {Florian Haftmann},
8.22 - title = {Haskell-style type classes with {Isabelle}/{Isar}},
8.23 - institution = TUM,
8.24 - note = {\url{http://isabelle.in.tum.de/doc/classes.pdf}}}
8.25 + author = {Florian Haftmann},
8.26 + title = {Haskell-style type classes with {Isabelle}/{Isar}},
8.27 + institution = TUM,
8.28 + note = {\url{http://isabelle.in.tum.de/doc/classes.pdf}}
8.29 +}
8.30
8.31 @manual{isabelle-codegen,
8.32 - author = {Florian Haftmann},
8.33 - title = {Code generation from Isabelle theories},
8.34 - institution = TUM,
8.35 - note = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}}}
8.36 + author = {Florian Haftmann},
8.37 + title = {Code generation from Isabelle theories},
8.38 + institution = TUM,
8.39 + note = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}}
8.40 +}
8.41
8.42 @Book{halmos60,
8.43 author = {Paul R. Halmos},