1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy Tue Sep 30 14:19:28 2008 +0200
1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy Tue Sep 30 14:30:44 2008 +0200
1.3 @@ -7,7 +7,7 @@
1.4 subsection {* Common adaption cases *}
1.5
1.6 text {*
1.7 - The @{text HOL} @{text Main} theory already provides a code
1.8 + The @{theory HOL} @{theory Main} theory already provides a code
1.9 generator setup
1.10 which should be suitable for most applications. Common extensions
1.11 and modifications are available by certain theories of the @{text HOL}
1.12 @@ -193,7 +193,7 @@
1.13
1.14 instance %quoteme by default (simp add: eq_bar_def)
1.15
1.16 -end
1.17 +end %quoteme
1.18
1.19 code_type %tt bar
1.20 (Haskell "Integer")
2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Tue Sep 30 14:19:28 2008 +0200
2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Tue Sep 30 14:30:44 2008 +0200
2.3 @@ -17,12 +17,12 @@
2.4 \cite{haskell-revised-report}).
2.5
2.6 Conceptually the code generator framework is part
2.7 - of Isabelle's @{text Pure} meta logic framework; the logic
2.8 - @{text HOL} which is an extension of @{text Pure}
2.9 + of Isabelle's @{theory Pure} meta logic framework; the logic
2.10 + @{theory HOL} which is an extension of @{theory Pure}
2.11 already comes with a reasonable framework setup and thus provides
2.12 a good working horse for raising code-generation-driven
2.13 applications. So, we assume some familiarity and experience
2.14 - with the ingredients of the @{text HOL} distribution theories.
2.15 + with the ingredients of the @{theory HOL} distribution theories.
2.16 (see also \cite{isa-tutorial}).
2.17
2.18 The code generator aims to be usable with no further ado
2.19 @@ -42,7 +42,7 @@
2.20 So, for the moment, there are two distinct code generators
2.21 in Isabelle.
2.22 Also note that while the framework itself is
2.23 - object-logic independent, only @{text HOL} provides a reasonable
2.24 + object-logic independent, only @{theory HOL} provides a reasonable
2.25 framework setup.
2.26 \end{warn}
2.27
2.28 @@ -55,7 +55,7 @@
2.29 \emph{shallow embedding}, i.e.~logical entities like constants, types and
2.30 classes are identified with corresponding concepts in the target language.
2.31
2.32 - Inside @{text HOL}, the @{command datatype} and
2.33 + Inside @{theory HOL}, the @{command datatype} and
2.34 @{command definition}/@{command primrec}/@{command fun} declarations form
2.35 the core of a functional programming language. The default code generator setup
2.36 allows to turn those into functional programs immediately.
3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Tue Sep 30 14:19:28 2008 +0200
3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Tue Sep 30 14:30:44 2008 +0200
3.3 @@ -124,14 +124,14 @@
3.4
3.5 text {*
3.6 \noindent An inspection reveals that the equations stemming from the
3.7 - @{text primrec} statement within instantiation of class
3.8 + @{command primrec} statement within instantiation of class
3.9 @{class semigroup} with type @{typ nat} are mapped to a separate
3.10 - function declaration @{text mult_nat} which in turn is used
3.11 - to provide the right hand side for the @{text "instance Semigroup Nat"}
3.12 - \fixme[courier fuer code text, isastyle fuer class]. This perfectly
3.13 + function declaration @{verbatim mult_nat} which in turn is used
3.14 + to provide the right hand side for the @{verbatim "instance Semigroup Nat"}.
3.15 + This perfectly
3.16 agrees with the restriction that @{text inst} statements may
3.17 only contain one single equation for each class class parameter
3.18 - The @{text instantiation} mechanism manages that for each
3.19 + The @{command instantiation} mechanism manages that for each
3.20 overloaded constant @{text "f [\<kappa> \<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"}
3.21 a \emph{shadow constant} @{text "f\<^isub>\<kappa> [\<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"} is
3.22 declared satisfying @{text "f [\<kappa> \<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>] \<equiv> f\<^isub>\<kappa> [\<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"}.
3.23 @@ -344,7 +344,7 @@
3.24 else collect_duplicates (z#xs) (z#ys) zs)"
3.25
3.26 text {*
3.27 - The membership test during preprocessing is rewritten,
3.28 + \noindent The membership test during preprocessing is rewritten,
3.29 resulting in @{const List.member}, which itself
3.30 performs an explicit equality check.
3.31 *}
3.32 @@ -368,32 +368,30 @@
3.33 us define a lexicographic ordering on tuples:
3.34 *}
3.35
3.36 -instantiation * :: (ord, ord) ord
3.37 +instantiation %quoteme * :: (ord, ord) ord
3.38 begin
3.39
3.40 -definition
3.41 - [code func del]: "p1 < p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in
3.42 - x1 < x2 \<or> (x1 = x2 \<and> y1 < y2))"
3.43 +definition %quoteme [code func del]:
3.44 + "p1 < p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in x1 < x2 \<or> (x1 = x2 \<and> y1 < y2))"
3.45
3.46 -definition
3.47 - [code func del]: "p1 \<le> p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in
3.48 - x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2))"
3.49 +definition %quoteme [code func del]:
3.50 + "p1 \<le> p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2))"
3.51
3.52 -instance ..
3.53 +instance %quoteme ..
3.54
3.55 -end
3.56 +end %quoteme
3.57
3.58 -lemma ord_prod [code func(*<*), code func del(*>*)]:
3.59 +lemma %quoteme ord_prod [code func]:
3.60 "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
3.61 "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
3.62 unfolding less_prod_def less_eq_prod_def by simp_all
3.63
3.64 text {*
3.65 - Then code generation will fail. Why? The definition
3.66 + \noindent Then code generation will fail. Why? The definition
3.67 of @{term "op \<le>"} depends on equality on both arguments,
3.68 which are polymorphic and impose an additional @{class eq}
3.69 - class constraint, thus violating the type discipline
3.70 - for class operations.
3.71 + class constraint, which the preprocessort does not propagate for technical
3.72 + reasons.
3.73
3.74 The solution is to add @{class eq} explicitly to the first sort arguments in the
3.75 code theorems:
3.76 @@ -413,15 +411,6 @@
3.77 text %quoteme {*@{code_stmts "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" (SML)}*}
3.78
3.79 text {*
3.80 - In general, code theorems for overloaded constants may have more
3.81 - restrictive sort constraints than the underlying instance relation
3.82 - between class and type constructor as long as the whole system of
3.83 - constraints is coregular; code theorems violating coregularity
3.84 - are rejected immediately. Consequently, it might be necessary
3.85 - to delete disturbing theorems in the code theorem table,
3.86 - as we have done here with the original definitions @{fact less_prod_def}
3.87 - and @{fact less_eq_prod_def}.
3.88 -
3.89 In some cases, the automatically derived defining equations
3.90 for equality on a particular type may not be appropriate.
3.91 As example, watch the following datatype representing
3.92 @@ -442,7 +431,7 @@
3.93 the theorem @{thm monotype_eq [no_vars]} already requires the
3.94 instance @{text "monotype \<Colon> eq"}, which itself requires
3.95 @{thm monotype_eq [no_vars]}; Haskell has no problem with mutually
3.96 - recursive @{text instance} and @{text function} definitions,
3.97 + recursive @{text inst} and @{text fun} definitions,
3.98 but the SML serializer does not support this.
3.99
3.100 In such cases, you have to provide you own equality equations
4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Tue Sep 30 14:19:28 2008 +0200
4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Tue Sep 30 14:30:44 2008 +0200
4.3 @@ -8,7 +8,7 @@
4.4 ML_val {* Code_Target.code_width := 74 *}
4.5
4.6 ML {*
4.7 -fun pr_class ctxt = Sign.extern_class (ProofContext.theory_of ctxt)
4.8 +fun pr_class ctxt = enclose "\\isa{" "}" o Sign.extern_class (ProofContext.theory_of ctxt)
4.9 o Sign.read_class (ProofContext.theory_of ctxt);
4.10 *}
4.11
5.1 --- a/doc-src/IsarAdvanced/Codegen/codegen.tex Tue Sep 30 14:19:28 2008 +0200
5.2 +++ b/doc-src/IsarAdvanced/Codegen/codegen.tex Tue Sep 30 14:30:44 2008 +0200
5.3 @@ -10,19 +10,23 @@
5.4 \usepackage{style}
5.5 \usepackage{../../pdfsetup}
5.6
5.7 +\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
5.8 +
5.9 \makeatletter
5.10
5.11 -\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
5.12 \isakeeptag{quoteme}
5.13 \newenvironment{quoteme}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
5.14 \renewcommand{\isatagquoteme}{\begin{quoteme}}
5.15 \renewcommand{\endisatagquoteme}{\end{quoteme}}
5.16
5.17 +\isakeeptag{tt}
5.18 +\renewcommand{\isatagtt}{\begin{quoteme}\isabellestyle{tt}\isastyle}
5.19 +\renewcommand{\endisatagtt}{\end{quoteme}\isabellestyle{it}\isastyle}
5.20 +
5.21 \makeatother
5.22
5.23 -\isakeeptag{tt}
5.24 -\renewcommand{\isatagtt}{\isabellestyle{tt}\isastyle}
5.25 -\renewcommand{\endisatagtt}{\isabellestyle{it}\isastyle}
5.26 +\newcommand{\isactrlbvec}{\emph\bgroup\begin{math}{}\overline\bgroup\mbox\bgroup\isastylescript}
5.27 +\newcommand{\isactrlevec}{\egroup\egroup\end{math}\egroup}
5.28
5.29 \newcommand{\qt}[1]{``#1''}
5.30 \newcommand{\qtt}[1]{"{}{#1}"{}}