# HG changeset patch # User haftmann # Date 1186667558 -7200 # Node ID 926dde4d96de206481ac99854c7bb84e8bf0f4b9 # Parent 4eccd4bb8b64ccd42de55b74a222703d71919422 updated diff -r 4eccd4bb8b64 -r 926dde4d96de doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- 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. *} diff -r 4eccd4bb8b64 -r 926dde4d96de doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- 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% diff -r 4eccd4bb8b64 -r 926dde4d96de doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML --- 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; diff -r 4eccd4bb8b64 -r 926dde4d96de doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML --- 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*) diff -r 4eccd4bb8b64 -r 926dde4d96de doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML --- 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 [] = []; diff -r 4eccd4bb8b64 -r 926dde4d96de doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML --- 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 = diff -r 4eccd4bb8b64 -r 926dde4d96de doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML --- 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)))); diff -r 4eccd4bb8b64 -r 926dde4d96de doc-src/manual.bib --- 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},