updated
authorhaftmann
Thu Aug 09 15:52:38 2007 +0200 (2007-08-09)
changeset 24193926dde4d96de
parent 24192 4eccd4bb8b64
child 24194 96013f81faef
updated
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML
doc-src/manual.bib
     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},