--- a/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy Tue Sep 30 14:19:28 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy Tue Sep 30 14:30:44 2008 +0200
@@ -7,7 +7,7 @@
subsection {* Common adaption cases *}
text {*
- The @{text HOL} @{text Main} theory already provides a code
+ The @{theory HOL} @{theory Main} theory already provides a code
generator setup
which should be suitable for most applications. Common extensions
and modifications are available by certain theories of the @{text HOL}
@@ -193,7 +193,7 @@
instance %quoteme by default (simp add: eq_bar_def)
-end
+end %quoteme
code_type %tt bar
(Haskell "Integer")
--- a/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Tue Sep 30 14:19:28 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Tue Sep 30 14:30:44 2008 +0200
@@ -17,12 +17,12 @@
\cite{haskell-revised-report}).
Conceptually the code generator framework is part
- of Isabelle's @{text Pure} meta logic framework; the logic
- @{text HOL} which is an extension of @{text Pure}
+ of Isabelle's @{theory Pure} meta logic framework; the logic
+ @{theory HOL} which is an extension of @{theory Pure}
already comes with a reasonable framework setup and thus provides
a good working horse for raising code-generation-driven
applications. So, we assume some familiarity and experience
- with the ingredients of the @{text HOL} distribution theories.
+ with the ingredients of the @{theory HOL} distribution theories.
(see also \cite{isa-tutorial}).
The code generator aims to be usable with no further ado
@@ -42,7 +42,7 @@
So, for the moment, there are two distinct code generators
in Isabelle.
Also note that while the framework itself is
- object-logic independent, only @{text HOL} provides a reasonable
+ object-logic independent, only @{theory HOL} provides a reasonable
framework setup.
\end{warn}
@@ -55,7 +55,7 @@
\emph{shallow embedding}, i.e.~logical entities like constants, types and
classes are identified with corresponding concepts in the target language.
- Inside @{text HOL}, the @{command datatype} and
+ Inside @{theory HOL}, the @{command datatype} and
@{command definition}/@{command primrec}/@{command fun} declarations form
the core of a functional programming language. The default code generator setup
allows to turn those into functional programs immediately.
--- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Tue Sep 30 14:19:28 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Tue Sep 30 14:30:44 2008 +0200
@@ -124,14 +124,14 @@
text {*
\noindent An inspection reveals that the equations stemming from the
- @{text primrec} statement within instantiation of class
+ @{command primrec} statement within instantiation of class
@{class semigroup} with type @{typ nat} are mapped to a separate
- function declaration @{text mult_nat} which in turn is used
- to provide the right hand side for the @{text "instance Semigroup Nat"}
- \fixme[courier fuer code text, isastyle fuer class]. This perfectly
+ function declaration @{verbatim mult_nat} which in turn is used
+ to provide the right hand side for the @{verbatim "instance Semigroup Nat"}.
+ This perfectly
agrees with the restriction that @{text inst} statements may
only contain one single equation for each class class parameter
- The @{text instantiation} mechanism manages that for each
+ The @{command instantiation} mechanism manages that for each
overloaded constant @{text "f [\<kappa> \<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"}
a \emph{shadow constant} @{text "f\<^isub>\<kappa> [\<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"} is
declared satisfying @{text "f [\<kappa> \<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>] \<equiv> f\<^isub>\<kappa> [\<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"}.
@@ -344,7 +344,7 @@
else collect_duplicates (z#xs) (z#ys) zs)"
text {*
- The membership test during preprocessing is rewritten,
+ \noindent The membership test during preprocessing is rewritten,
resulting in @{const List.member}, which itself
performs an explicit equality check.
*}
@@ -368,32 +368,30 @@
us define a lexicographic ordering on tuples:
*}
-instantiation * :: (ord, ord) ord
+instantiation %quoteme * :: (ord, ord) ord
begin
-definition
- [code func del]: "p1 < p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in
- x1 < x2 \<or> (x1 = x2 \<and> y1 < y2))"
+definition %quoteme [code func del]:
+ "p1 < p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in x1 < x2 \<or> (x1 = x2 \<and> y1 < y2))"
+
+definition %quoteme [code func del]:
+ "p1 \<le> p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2))"
-definition
- [code func del]: "p1 \<le> p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in
- x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2))"
+instance %quoteme ..
-instance ..
+end %quoteme
-end
-
-lemma ord_prod [code func(*<*), code func del(*>*)]:
+lemma %quoteme ord_prod [code func]:
"(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
"(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
unfolding less_prod_def less_eq_prod_def by simp_all
text {*
- Then code generation will fail. Why? The definition
+ \noindent Then code generation will fail. Why? The definition
of @{term "op \<le>"} depends on equality on both arguments,
which are polymorphic and impose an additional @{class eq}
- class constraint, thus violating the type discipline
- for class operations.
+ class constraint, which the preprocessort does not propagate for technical
+ reasons.
The solution is to add @{class eq} explicitly to the first sort arguments in the
code theorems:
@@ -413,15 +411,6 @@
text %quoteme {*@{code_stmts "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" (SML)}*}
text {*
- In general, code theorems for overloaded constants may have more
- restrictive sort constraints than the underlying instance relation
- between class and type constructor as long as the whole system of
- constraints is coregular; code theorems violating coregularity
- are rejected immediately. Consequently, it might be necessary
- to delete disturbing theorems in the code theorem table,
- as we have done here with the original definitions @{fact less_prod_def}
- and @{fact less_eq_prod_def}.
-
In some cases, the automatically derived defining equations
for equality on a particular type may not be appropriate.
As example, watch the following datatype representing
@@ -442,7 +431,7 @@
the theorem @{thm monotype_eq [no_vars]} already requires the
instance @{text "monotype \<Colon> eq"}, which itself requires
@{thm monotype_eq [no_vars]}; Haskell has no problem with mutually
- recursive @{text instance} and @{text function} definitions,
+ recursive @{text inst} and @{text fun} definitions,
but the SML serializer does not support this.
In such cases, you have to provide you own equality equations
--- a/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Tue Sep 30 14:19:28 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Tue Sep 30 14:30:44 2008 +0200
@@ -8,7 +8,7 @@
ML_val {* Code_Target.code_width := 74 *}
ML {*
-fun pr_class ctxt = Sign.extern_class (ProofContext.theory_of ctxt)
+fun pr_class ctxt = enclose "\\isa{" "}" o Sign.extern_class (ProofContext.theory_of ctxt)
o Sign.read_class (ProofContext.theory_of ctxt);
*}
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex Tue Sep 30 14:19:28 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex Tue Sep 30 14:30:44 2008 +0200
@@ -10,19 +10,23 @@
\usepackage{style}
\usepackage{../../pdfsetup}
+\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
+
\makeatletter
-\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
\isakeeptag{quoteme}
\newenvironment{quoteme}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
\renewcommand{\isatagquoteme}{\begin{quoteme}}
\renewcommand{\endisatagquoteme}{\end{quoteme}}
+\isakeeptag{tt}
+\renewcommand{\isatagtt}{\begin{quoteme}\isabellestyle{tt}\isastyle}
+\renewcommand{\endisatagtt}{\end{quoteme}\isabellestyle{it}\isastyle}
+
\makeatother
-\isakeeptag{tt}
-\renewcommand{\isatagtt}{\isabellestyle{tt}\isastyle}
-\renewcommand{\endisatagtt}{\isabellestyle{it}\isastyle}
+\newcommand{\isactrlbvec}{\emph\bgroup\begin{math}{}\overline\bgroup\mbox\bgroup\isastylescript}
+\newcommand{\isactrlevec}{\egroup\egroup\end{math}\egroup}
\newcommand{\qt}[1]{``#1''}
\newcommand{\qtt}[1]{"{}{#1}"{}}