# HG changeset patch # User haftmann # Date 1222777844 -7200 # Node ID fd007794561fe2929a2e71e725eec0b28ef7b679 # Parent cc9f7d99fb7327cc7eb9e5c28ef48b7c72d5137b tuned diff -r cc9f7d99fb73 -r fd007794561f doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy --- 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") diff -r cc9f7d99fb73 -r fd007794561f doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy --- 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. diff -r cc9f7d99fb73 -r fd007794561f doc-src/IsarAdvanced/Codegen/Thy/Program.thy --- 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 [\ \<^bvec>\\s\<^isub>k\<^evec>]"} a \emph{shadow constant} @{text "f\<^isub>\ [\<^bvec>\\s\<^isub>k\<^evec>]"} is declared satisfying @{text "f [\ \<^bvec>\\s\<^isub>k\<^evec>] \ f\<^isub>\ [\<^bvec>\\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 \ (let (x1, y1) = p1; (x2, y2) = p2 in - x1 < x2 \ (x1 = x2 \ y1 < y2))" +definition %quoteme [code func del]: + "p1 < p2 \ (let (x1, y1) = p1; (x2, y2) = p2 in x1 < x2 \ (x1 = x2 \ y1 < y2))" + +definition %quoteme [code func del]: + "p1 \ p2 \ (let (x1, y1) = p1; (x2, y2) = p2 in x1 < x2 \ (x1 = x2 \ y1 \ y2))" -definition - [code func del]: "p1 \ p2 \ (let (x1, y1) = p1; (x2, y2) = p2 in - x1 < x2 \ (x1 = x2 \ y1 \ y2))" +instance %quoteme .. -instance .. +end %quoteme -end - -lemma ord_prod [code func(*<*), code func del(*>*)]: +lemma %quoteme ord_prod [code func]: "(x1 \ 'a\ord, y1 \ 'b\ord) < (x2, y2) \ x1 < x2 \ (x1 = x2 \ y1 < y2)" "(x1 \ 'a\ord, y1 \ 'b\ord) \ (x2, y2) \ x1 < x2 \ (x1 = x2 \ y1 \ 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 \"} 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 \ \ 'a\{eq, ord} \ 'b\ord \ 'a \ 'b \ 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 \ 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 diff -r cc9f7d99fb73 -r fd007794561f doc-src/IsarAdvanced/Codegen/Thy/Setup.thy --- 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); *} diff -r cc9f7d99fb73 -r fd007794561f doc-src/IsarAdvanced/Codegen/codegen.tex --- 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}"{}}