--- a/doc-src/Codegen/Makefile Wed May 06 19:15:40 2009 +0200
+++ b/doc-src/Codegen/Makefile Wed May 06 19:42:27 2009 +0200
@@ -17,7 +17,7 @@
dvi: $(NAME).dvi
-$(NAME).dvi: $(FILES) isabelle_isar.eps architecture.eps adaption.eps
+$(NAME).dvi: $(FILES) isabelle_isar.eps architecture.eps adaptation.eps
$(LATEX) $(NAME)
$(BIBTEX) $(NAME)
$(LATEX) $(NAME)
@@ -25,7 +25,7 @@
pdf: $(NAME).pdf
-$(NAME).pdf: $(FILES) isabelle_isar.pdf architecture.pdf adaption.pdf
+$(NAME).pdf: $(FILES) isabelle_isar.pdf architecture.pdf adaptation.pdf
$(PDFLATEX) $(NAME)
$(BIBTEX) $(NAME)
$(PDFLATEX) $(NAME)
@@ -37,17 +37,17 @@
architecture.dvi: Thy/pictures/architecture.tex
latex -output-directory=$(dir $@) $<
-adaption.dvi: Thy/pictures/adaption.tex
+adaptation.dvi: Thy/pictures/adaptation.tex
latex -output-directory=$(dir $@) $<
architecture.eps: architecture.dvi
dvips -E -o $@ $<
-adaption.eps: adaption.dvi
+adaptation.eps: adaptation.dvi
dvips -E -o $@ $<
architecture.pdf: architecture.eps
epstopdf --outfile=$@ $<
-adaption.pdf: adaption.eps
+adaptation.pdf: adaptation.eps
epstopdf --outfile=$@ $<
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Codegen/Thy/Adaptation.thy Wed May 06 19:42:27 2009 +0200
@@ -0,0 +1,326 @@
+theory Adaptation
+imports Setup
+begin
+
+setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", K I)) *}
+
+section {* Adaptation to target languages \label{sec:adaptation} *}
+
+subsection {* Adapting code generation *}
+
+text {*
+ The aspects of code generation introduced so far have two aspects
+ in common:
+
+ \begin{itemize}
+ \item They act uniformly, without reference to a specific
+ target language.
+ \item They are \emph{safe} in the sense that as long as you trust
+ the code generator meta theory and implementation, you cannot
+ produce programs that yield results which are not derivable
+ in the logic.
+ \end{itemize}
+
+ \noindent In this section we will introduce means to \emph{adapt} the serialiser
+ to a specific target language, i.e.~to print program fragments
+ in a way which accommodates \qt{already existing} ingredients of
+ a target language environment, for three reasons:
+
+ \begin{itemize}
+ \item improving readability and aesthetics of generated code
+ \item gaining efficiency
+ \item interface with language parts which have no direct counterpart
+ in @{text "HOL"} (say, imperative data structures)
+ \end{itemize}
+
+ \noindent Generally, you should avoid using those features yourself
+ \emph{at any cost}:
+
+ \begin{itemize}
+ \item The safe configuration methods act uniformly on every target language,
+ whereas for adaptation you have to treat each target language separate.
+ \item Application is extremely tedious since there is no abstraction
+ which would allow for a static check, making it easy to produce garbage.
+ \item More or less subtle errors can be introduced unconsciously.
+ \end{itemize}
+
+ \noindent However, even if you ought refrain from setting up adaptation
+ yourself, already the @{text "HOL"} comes with some reasonable default
+ adaptations (say, using target language list syntax). There also some
+ common adaptation cases which you can setup by importing particular
+ library theories. In order to understand these, we provide some clues here;
+ these however are not supposed to replace a careful study of the sources.
+*}
+
+subsection {* The adaptation principle *}
+
+text {*
+ Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is conceptually
+ supposed to be:
+
+ \begin{figure}[here]
+ \includegraphics{adaptation}
+ \caption{The adaptation principle}
+ \label{fig:adaptation}
+ \end{figure}
+
+ \noindent In the tame view, code generation acts as broker between
+ @{text logic}, @{text "intermediate language"} and
+ @{text "target language"} by means of @{text translation} and
+ @{text serialisation}; for the latter, the serialiser has to observe
+ the structure of the @{text language} itself plus some @{text reserved}
+ keywords which have to be avoided for generated code.
+ However, if you consider @{text adaptation} mechanisms, the code generated
+ by the serializer is just the tip of the iceberg:
+
+ \begin{itemize}
+ \item @{text serialisation} can be \emph{parametrised} such that
+ logical entities are mapped to target-specific ones
+ (e.g. target-specific list syntax,
+ see also \secref{sec:adaptation_mechanisms})
+ \item Such parametrisations can involve references to a
+ target-specific standard @{text library} (e.g. using
+ the @{text Haskell} @{verbatim Maybe} type instead
+ of the @{text HOL} @{type "option"} type);
+ if such are used, the corresponding identifiers
+ (in our example, @{verbatim Maybe}, @{verbatim Nothing}
+ and @{verbatim Just}) also have to be considered @{text reserved}.
+ \item Even more, the user can enrich the library of the
+ target-language by providing code snippets
+ (\qt{@{text "includes"}}) which are prepended to
+ any generated code (see \secref{sec:include}); this typically
+ also involves further @{text reserved} identifiers.
+ \end{itemize}
+
+ \noindent As figure \ref{fig:adaptation} illustrates, all these adaptation mechanisms
+ have to act consistently; it is at the discretion of the user
+ to take care for this.
+*}
+
+subsection {* Common adaptation patterns *}
+
+text {*
+ 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}
+ library; beside being useful in applications, they may serve
+ as a tutorial for customising the code generator setup (see below
+ \secref{sec:adaptation_mechanisms}).
+
+ \begin{description}
+
+ \item[@{theory "Code_Integer"}] represents @{text HOL} integers by big
+ integer literals in target languages.
+ \item[@{theory "Code_Char"}] represents @{text HOL} characters by
+ character literals in target languages.
+ \item[@{theory "Code_Char_chr"}] like @{text "Code_Char"},
+ but also offers treatment of character codes; includes
+ @{theory "Code_Char"}.
+ \item[@{theory "Efficient_Nat"}] \label{eff_nat} implements natural numbers by integers,
+ which in general will result in higher efficiency; pattern
+ matching with @{term "0\<Colon>nat"} / @{const "Suc"}
+ is eliminated; includes @{theory "Code_Integer"}
+ and @{theory "Code_Index"}.
+ \item[@{theory "Code_Index"}] provides an additional datatype
+ @{typ index} which is mapped to target-language built-in integers.
+ Useful for code setups which involve e.g. indexing of
+ target-language arrays.
+ \item[@{theory "String"}] provides an additional datatype
+ @{typ message_string} which is isomorphic to strings;
+ @{typ message_string}s are mapped to target-language strings.
+ Useful for code setups which involve e.g. printing (error) messages.
+
+ \end{description}
+
+ \begin{warn}
+ When importing any of these theories, they should form the last
+ items in an import list. Since these theories adapt the
+ code generator setup in a non-conservative fashion,
+ strange effects may occur otherwise.
+ \end{warn}
+*}
+
+
+subsection {* Parametrising serialisation \label{sec:adaptation_mechanisms} *}
+
+text {*
+ Consider the following function and its corresponding
+ SML code:
+*}
+
+primrec %quote in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
+ "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
+(*<*)
+code_type %invisible bool
+ (SML)
+code_const %invisible True and False and "op \<and>" and Not
+ (SML and and and)
+(*>*)
+text %quote {*@{code_stmts in_interval (SML)}*}
+
+text {*
+ \noindent Though this is correct code, it is a little bit unsatisfactory:
+ boolean values and operators are materialised as distinguished
+ entities with have nothing to do with the SML-built-in notion
+ of \qt{bool}. This results in less readable code;
+ additionally, eager evaluation may cause programs to
+ loop or break which would perfectly terminate when
+ the existing SML @{verbatim "bool"} would be used. To map
+ the HOL @{typ bool} on SML @{verbatim "bool"}, we may use
+ \qn{custom serialisations}:
+*}
+
+code_type %quotett bool
+ (SML "bool")
+code_const %quotett True and False and "op \<and>"
+ (SML "true" and "false" and "_ andalso _")
+
+text {*
+ \noindent The @{command code_type} command takes a type constructor
+ as arguments together with a list of custom serialisations.
+ Each custom serialisation starts with a target language
+ identifier followed by an expression, which during
+ code serialisation is inserted whenever the type constructor
+ would occur. For constants, @{command code_const} implements
+ the corresponding mechanism. Each ``@{verbatim "_"}'' in
+ a serialisation expression is treated as a placeholder
+ for the type constructor's (the constant's) arguments.
+*}
+
+text %quote {*@{code_stmts in_interval (SML)}*}
+
+text {*
+ \noindent This still is not perfect: the parentheses
+ around the \qt{andalso} expression are superfluous.
+ Though the serialiser
+ by no means attempts to imitate the rich Isabelle syntax
+ framework, it provides some common idioms, notably
+ associative infixes with precedences which may be used here:
+*}
+
+code_const %quotett "op \<and>"
+ (SML infixl 1 "andalso")
+
+text %quote {*@{code_stmts in_interval (SML)}*}
+
+text {*
+ \noindent The attentive reader may ask how we assert that no generated
+ code will accidentally overwrite. For this reason the serialiser has
+ an internal table of identifiers which have to be avoided to be used
+ for new declarations. Initially, this table typically contains the
+ keywords of the target language. It can be extended manually, thus avoiding
+ accidental overwrites, using the @{command "code_reserved"} command:
+*}
+
+code_reserved %quote "\<SML>" bool true false andalso
+
+text {*
+ \noindent Next, we try to map HOL pairs to SML pairs, using the
+ infix ``@{verbatim "*"}'' type constructor and parentheses:
+*}
+(*<*)
+code_type %invisible *
+ (SML)
+code_const %invisible Pair
+ (SML)
+(*>*)
+code_type %quotett *
+ (SML infix 2 "*")
+code_const %quotett Pair
+ (SML "!((_),/ (_))")
+
+text {*
+ \noindent The initial bang ``@{verbatim "!"}'' tells the serialiser
+ never to put
+ parentheses around the whole expression (they are already present),
+ while the parentheses around argument place holders
+ tell not to put parentheses around the arguments.
+ The slash ``@{verbatim "/"}'' (followed by arbitrary white space)
+ inserts a space which may be used as a break if necessary
+ during pretty printing.
+
+ These examples give a glimpse what mechanisms
+ custom serialisations provide; however their usage
+ requires careful thinking in order not to introduce
+ inconsistencies -- or, in other words:
+ custom serialisations are completely axiomatic.
+
+ A further noteworthy details is that any special
+ character in a custom serialisation may be quoted
+ using ``@{verbatim "'"}''; thus, in
+ ``@{verbatim "fn '_ => _"}'' the first
+ ``@{verbatim "_"}'' is a proper underscore while the
+ second ``@{verbatim "_"}'' is a placeholder.
+*}
+
+
+subsection {* @{text Haskell} serialisation *}
+
+text {*
+ For convenience, the default
+ @{text HOL} setup for @{text Haskell} maps the @{class eq} class to
+ its counterpart in @{text Haskell}, giving custom serialisations
+ for the class @{class eq} (by command @{command code_class}) and its operation
+ @{const HOL.eq}
+*}
+
+code_class %quotett eq
+ (Haskell "Eq")
+
+code_const %quotett "op ="
+ (Haskell infixl 4 "==")
+
+text {*
+ \noindent A problem now occurs whenever a type which
+ is an instance of @{class eq} in @{text HOL} is mapped
+ on a @{text Haskell}-built-in type which is also an instance
+ of @{text Haskell} @{text Eq}:
+*}
+
+typedecl %quote bar
+
+instantiation %quote bar :: eq
+begin
+
+definition %quote "eq_class.eq (x\<Colon>bar) y \<longleftrightarrow> x = y"
+
+instance %quote by default (simp add: eq_bar_def)
+
+end %quote (*<*)
+
+(*>*) code_type %quotett bar
+ (Haskell "Integer")
+
+text {*
+ \noindent The code generator would produce
+ an additional instance, which of course is rejected by the @{text Haskell}
+ compiler.
+ To suppress this additional instance, use
+ @{text "code_instance"}:
+*}
+
+code_instance %quotett bar :: eq
+ (Haskell -)
+
+
+subsection {* Enhancing the target language context \label{sec:include} *}
+
+text {*
+ In rare cases it is necessary to \emph{enrich} the context of a
+ target language; this is accomplished using the @{command "code_include"}
+ command:
+*}
+
+code_include %quotett Haskell "Errno"
+{*errno i = error ("Error number: " ++ show i)*}
+
+code_reserved %quotett Haskell Errno
+
+text {*
+ \noindent Such named @{text include}s are then prepended to every generated code.
+ Inspect such code in order to find out how @{command "code_include"} behaves
+ with respect to a particular target language.
+*}
+
+end
--- a/doc-src/Codegen/Thy/Adaption.thy Wed May 06 19:15:40 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,326 +0,0 @@
-theory Adaption
-imports Setup
-begin
-
-setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", K I)) *}
-
-section {* Adaption to target languages \label{sec:adaption} *}
-
-subsection {* Adapting code generation *}
-
-text {*
- The aspects of code generation introduced so far have two aspects
- in common:
-
- \begin{itemize}
- \item They act uniformly, without reference to a specific
- target language.
- \item They are \emph{safe} in the sense that as long as you trust
- the code generator meta theory and implementation, you cannot
- produce programs that yield results which are not derivable
- in the logic.
- \end{itemize}
-
- \noindent In this section we will introduce means to \emph{adapt} the serialiser
- to a specific target language, i.e.~to print program fragments
- in a way which accommodates \qt{already existing} ingredients of
- a target language environment, for three reasons:
-
- \begin{itemize}
- \item improving readability and aesthetics of generated code
- \item gaining efficiency
- \item interface with language parts which have no direct counterpart
- in @{text "HOL"} (say, imperative data structures)
- \end{itemize}
-
- \noindent Generally, you should avoid using those features yourself
- \emph{at any cost}:
-
- \begin{itemize}
- \item The safe configuration methods act uniformly on every target language,
- whereas for adaption you have to treat each target language separate.
- \item Application is extremely tedious since there is no abstraction
- which would allow for a static check, making it easy to produce garbage.
- \item More or less subtle errors can be introduced unconsciously.
- \end{itemize}
-
- \noindent However, even if you ought refrain from setting up adaption
- yourself, already the @{text "HOL"} comes with some reasonable default
- adaptions (say, using target language list syntax). There also some
- common adaption cases which you can setup by importing particular
- library theories. In order to understand these, we provide some clues here;
- these however are not supposed to replace a careful study of the sources.
-*}
-
-subsection {* The adaption principle *}
-
-text {*
- Figure \ref{fig:adaption} illustrates what \qt{adaption} is conceptually
- supposed to be:
-
- \begin{figure}[here]
- \includegraphics{adaption}
- \caption{The adaption principle}
- \label{fig:adaption}
- \end{figure}
-
- \noindent In the tame view, code generation acts as broker between
- @{text logic}, @{text "intermediate language"} and
- @{text "target language"} by means of @{text translation} and
- @{text serialisation}; for the latter, the serialiser has to observe
- the structure of the @{text language} itself plus some @{text reserved}
- keywords which have to be avoided for generated code.
- However, if you consider @{text adaption} mechanisms, the code generated
- by the serializer is just the tip of the iceberg:
-
- \begin{itemize}
- \item @{text serialisation} can be \emph{parametrised} such that
- logical entities are mapped to target-specific ones
- (e.g. target-specific list syntax,
- see also \secref{sec:adaption_mechanisms})
- \item Such parametrisations can involve references to a
- target-specific standard @{text library} (e.g. using
- the @{text Haskell} @{verbatim Maybe} type instead
- of the @{text HOL} @{type "option"} type);
- if such are used, the corresponding identifiers
- (in our example, @{verbatim Maybe}, @{verbatim Nothing}
- and @{verbatim Just}) also have to be considered @{text reserved}.
- \item Even more, the user can enrich the library of the
- target-language by providing code snippets
- (\qt{@{text "includes"}}) which are prepended to
- any generated code (see \secref{sec:include}); this typically
- also involves further @{text reserved} identifiers.
- \end{itemize}
-
- \noindent As figure \ref{fig:adaption} illustrates, all these adaption mechanisms
- have to act consistently; it is at the discretion of the user
- to take care for this.
-*}
-
-subsection {* Common adaption patterns *}
-
-text {*
- 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}
- library; beside being useful in applications, they may serve
- as a tutorial for customising the code generator setup (see below
- \secref{sec:adaption_mechanisms}).
-
- \begin{description}
-
- \item[@{theory "Code_Integer"}] represents @{text HOL} integers by big
- integer literals in target languages.
- \item[@{theory "Code_Char"}] represents @{text HOL} characters by
- character literals in target languages.
- \item[@{theory "Code_Char_chr"}] like @{text "Code_Char"},
- but also offers treatment of character codes; includes
- @{theory "Code_Char"}.
- \item[@{theory "Efficient_Nat"}] \label{eff_nat} implements natural numbers by integers,
- which in general will result in higher efficiency; pattern
- matching with @{term "0\<Colon>nat"} / @{const "Suc"}
- is eliminated; includes @{theory "Code_Integer"}
- and @{theory "Code_Index"}.
- \item[@{theory "Code_Index"}] provides an additional datatype
- @{typ index} which is mapped to target-language built-in integers.
- Useful for code setups which involve e.g. indexing of
- target-language arrays.
- \item[@{theory "Code_Message"}] provides an additional datatype
- @{typ message_string} which is isomorphic to strings;
- @{typ message_string}s are mapped to target-language strings.
- Useful for code setups which involve e.g. printing (error) messages.
-
- \end{description}
-
- \begin{warn}
- When importing any of these theories, they should form the last
- items in an import list. Since these theories adapt the
- code generator setup in a non-conservative fashion,
- strange effects may occur otherwise.
- \end{warn}
-*}
-
-
-subsection {* Parametrising serialisation \label{sec:adaption_mechanisms} *}
-
-text {*
- Consider the following function and its corresponding
- SML code:
-*}
-
-primrec %quote in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
- "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
-(*<*)
-code_type %invisible bool
- (SML)
-code_const %invisible True and False and "op \<and>" and Not
- (SML and and and)
-(*>*)
-text %quote {*@{code_stmts in_interval (SML)}*}
-
-text {*
- \noindent Though this is correct code, it is a little bit unsatisfactory:
- boolean values and operators are materialised as distinguished
- entities with have nothing to do with the SML-built-in notion
- of \qt{bool}. This results in less readable code;
- additionally, eager evaluation may cause programs to
- loop or break which would perfectly terminate when
- the existing SML @{verbatim "bool"} would be used. To map
- the HOL @{typ bool} on SML @{verbatim "bool"}, we may use
- \qn{custom serialisations}:
-*}
-
-code_type %quotett bool
- (SML "bool")
-code_const %quotett True and False and "op \<and>"
- (SML "true" and "false" and "_ andalso _")
-
-text {*
- \noindent The @{command code_type} command takes a type constructor
- as arguments together with a list of custom serialisations.
- Each custom serialisation starts with a target language
- identifier followed by an expression, which during
- code serialisation is inserted whenever the type constructor
- would occur. For constants, @{command code_const} implements
- the corresponding mechanism. Each ``@{verbatim "_"}'' in
- a serialisation expression is treated as a placeholder
- for the type constructor's (the constant's) arguments.
-*}
-
-text %quote {*@{code_stmts in_interval (SML)}*}
-
-text {*
- \noindent This still is not perfect: the parentheses
- around the \qt{andalso} expression are superfluous.
- Though the serialiser
- by no means attempts to imitate the rich Isabelle syntax
- framework, it provides some common idioms, notably
- associative infixes with precedences which may be used here:
-*}
-
-code_const %quotett "op \<and>"
- (SML infixl 1 "andalso")
-
-text %quote {*@{code_stmts in_interval (SML)}*}
-
-text {*
- \noindent The attentive reader may ask how we assert that no generated
- code will accidentally overwrite. For this reason the serialiser has
- an internal table of identifiers which have to be avoided to be used
- for new declarations. Initially, this table typically contains the
- keywords of the target language. It can be extended manually, thus avoiding
- accidental overwrites, using the @{command "code_reserved"} command:
-*}
-
-code_reserved %quote "\<SML>" bool true false andalso
-
-text {*
- \noindent Next, we try to map HOL pairs to SML pairs, using the
- infix ``@{verbatim "*"}'' type constructor and parentheses:
-*}
-(*<*)
-code_type %invisible *
- (SML)
-code_const %invisible Pair
- (SML)
-(*>*)
-code_type %quotett *
- (SML infix 2 "*")
-code_const %quotett Pair
- (SML "!((_),/ (_))")
-
-text {*
- \noindent The initial bang ``@{verbatim "!"}'' tells the serialiser
- never to put
- parentheses around the whole expression (they are already present),
- while the parentheses around argument place holders
- tell not to put parentheses around the arguments.
- The slash ``@{verbatim "/"}'' (followed by arbitrary white space)
- inserts a space which may be used as a break if necessary
- during pretty printing.
-
- These examples give a glimpse what mechanisms
- custom serialisations provide; however their usage
- requires careful thinking in order not to introduce
- inconsistencies -- or, in other words:
- custom serialisations are completely axiomatic.
-
- A further noteworthy details is that any special
- character in a custom serialisation may be quoted
- using ``@{verbatim "'"}''; thus, in
- ``@{verbatim "fn '_ => _"}'' the first
- ``@{verbatim "_"}'' is a proper underscore while the
- second ``@{verbatim "_"}'' is a placeholder.
-*}
-
-
-subsection {* @{text Haskell} serialisation *}
-
-text {*
- For convenience, the default
- @{text HOL} setup for @{text Haskell} maps the @{class eq} class to
- its counterpart in @{text Haskell}, giving custom serialisations
- for the class @{class eq} (by command @{command code_class}) and its operation
- @{const HOL.eq}
-*}
-
-code_class %quotett eq
- (Haskell "Eq")
-
-code_const %quotett "op ="
- (Haskell infixl 4 "==")
-
-text {*
- \noindent A problem now occurs whenever a type which
- is an instance of @{class eq} in @{text HOL} is mapped
- on a @{text Haskell}-built-in type which is also an instance
- of @{text Haskell} @{text Eq}:
-*}
-
-typedecl %quote bar
-
-instantiation %quote bar :: eq
-begin
-
-definition %quote "eq_class.eq (x\<Colon>bar) y \<longleftrightarrow> x = y"
-
-instance %quote by default (simp add: eq_bar_def)
-
-end %quote (*<*)
-
-(*>*) code_type %quotett bar
- (Haskell "Integer")
-
-text {*
- \noindent The code generator would produce
- an additional instance, which of course is rejected by the @{text Haskell}
- compiler.
- To suppress this additional instance, use
- @{text "code_instance"}:
-*}
-
-code_instance %quotett bar :: eq
- (Haskell -)
-
-
-subsection {* Enhancing the target language context \label{sec:include} *}
-
-text {*
- In rare cases it is necessary to \emph{enrich} the context of a
- target language; this is accomplished using the @{command "code_include"}
- command:
-*}
-
-code_include %quotett Haskell "Errno"
-{*errno i = error ("Error number: " ++ show i)*}
-
-code_reserved %quotett Haskell Errno
-
-text {*
- \noindent Such named @{text include}s are then prepended to every generated code.
- Inspect such code in order to find out how @{command "code_include"} behaves
- with respect to a particular target language.
-*}
-
-end
--- a/doc-src/Codegen/Thy/Further.thy Wed May 06 19:15:40 2009 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Wed May 06 19:42:27 2009 +0200
@@ -66,7 +66,7 @@
text {*
\noindent The soundness of the @{method eval} method depends crucially
on the correctness of the code generator; this is one of the reasons
- why you should not use adaption (see \secref{sec:adaption}) frivolously.
+ why you should not use adaptation (see \secref{sec:adaptation}) frivolously.
*}
subsection {* Code antiquotation *}
--- a/doc-src/Codegen/Thy/Introduction.thy Wed May 06 19:15:40 2009 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy Wed May 06 19:42:27 2009 +0200
@@ -28,8 +28,8 @@
This manifests in the structure of this tutorial: after a short
conceptual introduction with an example (\secref{sec:intro}),
we discuss the generic customisation facilities (\secref{sec:program}).
- A further section (\secref{sec:adaption}) is dedicated to the matter of
- \qn{adaption} to specific target language environments. After some
+ A further section (\secref{sec:adaptation}) is dedicated to the matter of
+ \qn{adaptation} to specific target language environments. After some
further issues (\secref{sec:further}) we conclude with an overview
of some ML programming interfaces (\secref{sec:ml}).
--- a/doc-src/Codegen/Thy/ROOT.ML Wed May 06 19:15:40 2009 +0200
+++ b/doc-src/Codegen/Thy/ROOT.ML Wed May 06 19:42:27 2009 +0200
@@ -4,6 +4,6 @@
use_thy "Introduction";
use_thy "Program";
-use_thy "Adaption";
+use_thy "Adaptation";
use_thy "Further";
use_thy "ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Wed May 06 19:42:27 2009 +0200
@@ -0,0 +1,642 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Adaptation}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Adaptation\isanewline
+\isakeyword{imports}\ Setup\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+\isanewline
+%
+\endisadelimtheory
+%
+\isadeliminvisible
+\isanewline
+%
+\endisadeliminvisible
+%
+\isataginvisible
+\isacommand{setup}\isamarkupfalse%
+\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isamarkupsection{Adaptation to target languages \label{sec:adaptation}%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Adapting code generation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The aspects of code generation introduced so far have two aspects
+ in common:
+
+ \begin{itemize}
+ \item They act uniformly, without reference to a specific
+ target language.
+ \item They are \emph{safe} in the sense that as long as you trust
+ the code generator meta theory and implementation, you cannot
+ produce programs that yield results which are not derivable
+ in the logic.
+ \end{itemize}
+
+ \noindent In this section we will introduce means to \emph{adapt} the serialiser
+ to a specific target language, i.e.~to print program fragments
+ in a way which accommodates \qt{already existing} ingredients of
+ a target language environment, for three reasons:
+
+ \begin{itemize}
+ \item improving readability and aesthetics of generated code
+ \item gaining efficiency
+ \item interface with language parts which have no direct counterpart
+ in \isa{HOL} (say, imperative data structures)
+ \end{itemize}
+
+ \noindent Generally, you should avoid using those features yourself
+ \emph{at any cost}:
+
+ \begin{itemize}
+ \item The safe configuration methods act uniformly on every target language,
+ whereas for adaptation you have to treat each target language separate.
+ \item Application is extremely tedious since there is no abstraction
+ which would allow for a static check, making it easy to produce garbage.
+ \item More or less subtle errors can be introduced unconsciously.
+ \end{itemize}
+
+ \noindent However, even if you ought refrain from setting up adaptation
+ yourself, already the \isa{HOL} comes with some reasonable default
+ adaptations (say, using target language list syntax). There also some
+ common adaptation cases which you can setup by importing particular
+ library theories. In order to understand these, we provide some clues here;
+ these however are not supposed to replace a careful study of the sources.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{The adaptation principle%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is conceptually
+ supposed to be:
+
+ \begin{figure}[here]
+ \includegraphics{adaptation}
+ \caption{The adaptation principle}
+ \label{fig:adaptation}
+ \end{figure}
+
+ \noindent In the tame view, code generation acts as broker between
+ \isa{logic}, \isa{intermediate\ language} and
+ \isa{target\ language} by means of \isa{translation} and
+ \isa{serialisation}; for the latter, the serialiser has to observe
+ the structure of the \isa{language} itself plus some \isa{reserved}
+ keywords which have to be avoided for generated code.
+ However, if you consider \isa{adaptation} mechanisms, the code generated
+ by the serializer is just the tip of the iceberg:
+
+ \begin{itemize}
+ \item \isa{serialisation} can be \emph{parametrised} such that
+ logical entities are mapped to target-specific ones
+ (e.g. target-specific list syntax,
+ see also \secref{sec:adaptation_mechanisms})
+ \item Such parametrisations can involve references to a
+ target-specific standard \isa{library} (e.g. using
+ the \isa{Haskell} \verb|Maybe| type instead
+ of the \isa{HOL} \isa{option} type);
+ if such are used, the corresponding identifiers
+ (in our example, \verb|Maybe|, \verb|Nothing|
+ and \verb|Just|) also have to be considered \isa{reserved}.
+ \item Even more, the user can enrich the library of the
+ target-language by providing code snippets
+ (\qt{\isa{includes}}) which are prepended to
+ any generated code (see \secref{sec:include}); this typically
+ also involves further \isa{reserved} identifiers.
+ \end{itemize}
+
+ \noindent As figure \ref{fig:adaptation} illustrates, all these adaptation mechanisms
+ have to act consistently; it is at the discretion of the user
+ to take care for this.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Common adaptation patterns%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{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 \isa{HOL}
+ library; beside being useful in applications, they may serve
+ as a tutorial for customising the code generator setup (see below
+ \secref{sec:adaptation_mechanisms}).
+
+ \begin{description}
+
+ \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by big
+ integer literals in target languages.
+ \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by
+ character literals in target languages.
+ \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char},
+ but also offers treatment of character codes; includes
+ \hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}.
+ \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements natural numbers by integers,
+ which in general will result in higher efficiency; pattern
+ matching with \isa{{\isadigit{0}}} / \isa{Suc}
+ is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}
+ and \hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}.
+ \item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] provides an additional datatype
+ \isa{index} which is mapped to target-language built-in integers.
+ Useful for code setups which involve e.g. indexing of
+ target-language arrays.
+ \item[\hyperlink{theory.Code-Message}{\mbox{\isa{Code{\isacharunderscore}Message}}}] provides an additional datatype
+ \isa{message{\isacharunderscore}string} which is isomorphic to strings;
+ \isa{message{\isacharunderscore}string}s are mapped to target-language strings.
+ Useful for code setups which involve e.g. printing (error) messages.
+
+ \end{description}
+
+ \begin{warn}
+ When importing any of these theories, they should form the last
+ items in an import list. Since these theories adapt the
+ code generator setup in a non-conservative fashion,
+ strange effects may occur otherwise.
+ \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Parametrising serialisation \label{sec:adaptation_mechanisms}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Consider the following function and its corresponding
+ SML code:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{primrec}\isamarkupfalse%
+\ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isataginvisible
+%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}structure Example = \\
+\hspace*{0pt}struct\\
+\hspace*{0pt}\\
+\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}datatype boola = True | False;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun anda x True = x\\
+\hspace*{0pt} ~| anda x False = False\\
+\hspace*{0pt} ~| anda True x = x\\
+\hspace*{0pt} ~| anda False x = False;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
+\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun in{\char95}interval (k,~l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
+\hspace*{0pt}\\
+\hspace*{0pt}end;~(*struct Example*)%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent Though this is correct code, it is a little bit unsatisfactory:
+ boolean values and operators are materialised as distinguished
+ entities with have nothing to do with the SML-built-in notion
+ of \qt{bool}. This results in less readable code;
+ additionally, eager evaluation may cause programs to
+ loop or break which would perfectly terminate when
+ the existing SML \verb|bool| would be used. To map
+ the HOL \isa{bool} on SML \verb|bool|, we may use
+ \qn{custom serialisations}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquotett
+%
+\endisadelimquotett
+%
+\isatagquotett
+\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
+\ bool\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
+\ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagquotett
+{\isafoldquotett}%
+%
+\isadelimquotett
+%
+\endisadelimquotett
+%
+\begin{isamarkuptext}%
+\noindent The \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor
+ as arguments together with a list of custom serialisations.
+ Each custom serialisation starts with a target language
+ identifier followed by an expression, which during
+ code serialisation is inserted whenever the type constructor
+ would occur. For constants, \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements
+ the corresponding mechanism. Each ``\verb|_|'' in
+ a serialisation expression is treated as a placeholder
+ for the type constructor's (the constant's) arguments.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}structure Example = \\
+\hspace*{0pt}struct\\
+\hspace*{0pt}\\
+\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
+\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun in{\char95}interval (k,~l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\
+\hspace*{0pt}\\
+\hspace*{0pt}end;~(*struct Example*)%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This still is not perfect: the parentheses
+ around the \qt{andalso} expression are superfluous.
+ Though the serialiser
+ by no means attempts to imitate the rich Isabelle syntax
+ framework, it provides some common idioms, notably
+ associative infixes with precedences which may be used here:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquotett
+%
+\endisadelimquotett
+%
+\isatagquotett
+\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
+\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagquotett
+{\isafoldquotett}%
+%
+\isadelimquotett
+%
+\endisadelimquotett
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}structure Example = \\
+\hspace*{0pt}struct\\
+\hspace*{0pt}\\
+\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
+\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun in{\char95}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
+\hspace*{0pt}\\
+\hspace*{0pt}end;~(*struct Example*)%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The attentive reader may ask how we assert that no generated
+ code will accidentally overwrite. For this reason the serialiser has
+ an internal table of identifiers which have to be avoided to be used
+ for new declarations. Initially, this table typically contains the
+ keywords of the target language. It can be extended manually, thus avoiding
+ accidental overwrites, using the \hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} command:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymSML}{\isachardoublequoteclose}\ bool\ true\ false\ andalso%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent Next, we try to map HOL pairs to SML pairs, using the
+ infix ``\verb|*|'' type constructor and parentheses:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isataginvisible
+%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isadelimquotett
+%
+\endisadelimquotett
+%
+\isatagquotett
+\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
+\ {\isacharasterisk}\isanewline
+\ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
+\ Pair\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagquotett
+{\isafoldquotett}%
+%
+\isadelimquotett
+%
+\endisadelimquotett
+%
+\begin{isamarkuptext}%
+\noindent The initial bang ``\verb|!|'' tells the serialiser
+ never to put
+ parentheses around the whole expression (they are already present),
+ while the parentheses around argument place holders
+ tell not to put parentheses around the arguments.
+ The slash ``\verb|/|'' (followed by arbitrary white space)
+ inserts a space which may be used as a break if necessary
+ during pretty printing.
+
+ These examples give a glimpse what mechanisms
+ custom serialisations provide; however their usage
+ requires careful thinking in order not to introduce
+ inconsistencies -- or, in other words:
+ custom serialisations are completely axiomatic.
+
+ A further noteworthy details is that any special
+ character in a custom serialisation may be quoted
+ using ``\verb|'|''; thus, in
+ ``\verb|fn '_ => _|'' the first
+ ``\verb|_|'' is a proper underscore while the
+ second ``\verb|_|'' is a placeholder.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{\isa{Haskell} serialisation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+For convenience, the default
+ \isa{HOL} setup for \isa{Haskell} maps the \isa{eq} class to
+ its counterpart in \isa{Haskell}, giving custom serialisations
+ for the class \isa{eq} (by command \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation
+ \isa{eq{\isacharunderscore}class{\isachardot}eq}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquotett
+%
+\endisadelimquotett
+%
+\isatagquotett
+\isacommand{code{\isacharunderscore}class}\isamarkupfalse%
+\ eq\isanewline
+\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\isanewline
+\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
+\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagquotett
+{\isafoldquotett}%
+%
+\isadelimquotett
+%
+\endisadelimquotett
+%
+\begin{isamarkuptext}%
+\noindent A problem now occurs whenever a type which
+ is an instance of \isa{eq} in \isa{HOL} is mapped
+ on a \isa{Haskell}-built-in type which is also an instance
+ of \isa{Haskell} \isa{Eq}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{typedecl}\isamarkupfalse%
+\ bar\isanewline
+\isanewline
+\isacommand{instantiation}\isamarkupfalse%
+\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{instance}\isamarkupfalse%
+\ \isacommand{by}\isamarkupfalse%
+\ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isadelimquotett
+\ %
+\endisadelimquotett
+%
+\isatagquotett
+\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
+\ bar\isanewline
+\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagquotett
+{\isafoldquotett}%
+%
+\isadelimquotett
+%
+\endisadelimquotett
+%
+\begin{isamarkuptext}%
+\noindent The code generator would produce
+ an additional instance, which of course is rejected by the \isa{Haskell}
+ compiler.
+ To suppress this additional instance, use
+ \isa{code{\isacharunderscore}instance}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquotett
+%
+\endisadelimquotett
+%
+\isatagquotett
+\isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
+\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
+\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
+\endisatagquotett
+{\isafoldquotett}%
+%
+\isadelimquotett
+%
+\endisadelimquotett
+%
+\isamarkupsubsection{Enhancing the target language context \label{sec:include}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In rare cases it is necessary to \emph{enrich} the context of a
+ target language; this is accomplished using the \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}
+ command:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquotett
+%
+\endisadelimquotett
+%
+\isatagquotett
+\isacommand{code{\isacharunderscore}include}\isamarkupfalse%
+\ Haskell\ {\isachardoublequoteopen}Errno{\isachardoublequoteclose}\isanewline
+{\isacharverbatimopen}errno\ i\ {\isacharequal}\ error\ {\isacharparenleft}{\isachardoublequote}Error\ number{\isacharcolon}\ {\isachardoublequote}\ {\isacharplus}{\isacharplus}\ show\ i{\isacharparenright}{\isacharverbatimclose}\isanewline
+\isanewline
+\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
+\ Haskell\ Errno%
+\endisatagquotett
+{\isafoldquotett}%
+%
+\isadelimquotett
+%
+\endisadelimquotett
+%
+\begin{isamarkuptext}%
+\noindent Such named \isa{include}s are then prepended to every generated code.
+ Inspect such code in order to find out how \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} behaves
+ with respect to a particular target language.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/Codegen/Thy/document/Adaption.tex Wed May 06 19:15:40 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,642 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Adaption}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Adaption\isanewline
-\isakeyword{imports}\ Setup\isanewline
-\isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-\isanewline
-%
-\endisadelimtheory
-%
-\isadeliminvisible
-\isanewline
-%
-\endisadeliminvisible
-%
-\isataginvisible
-\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isamarkupsection{Adaption to target languages \label{sec:adaption}%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Adapting code generation%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The aspects of code generation introduced so far have two aspects
- in common:
-
- \begin{itemize}
- \item They act uniformly, without reference to a specific
- target language.
- \item They are \emph{safe} in the sense that as long as you trust
- the code generator meta theory and implementation, you cannot
- produce programs that yield results which are not derivable
- in the logic.
- \end{itemize}
-
- \noindent In this section we will introduce means to \emph{adapt} the serialiser
- to a specific target language, i.e.~to print program fragments
- in a way which accommodates \qt{already existing} ingredients of
- a target language environment, for three reasons:
-
- \begin{itemize}
- \item improving readability and aesthetics of generated code
- \item gaining efficiency
- \item interface with language parts which have no direct counterpart
- in \isa{HOL} (say, imperative data structures)
- \end{itemize}
-
- \noindent Generally, you should avoid using those features yourself
- \emph{at any cost}:
-
- \begin{itemize}
- \item The safe configuration methods act uniformly on every target language,
- whereas for adaption you have to treat each target language separate.
- \item Application is extremely tedious since there is no abstraction
- which would allow for a static check, making it easy to produce garbage.
- \item More or less subtle errors can be introduced unconsciously.
- \end{itemize}
-
- \noindent However, even if you ought refrain from setting up adaption
- yourself, already the \isa{HOL} comes with some reasonable default
- adaptions (say, using target language list syntax). There also some
- common adaption cases which you can setup by importing particular
- library theories. In order to understand these, we provide some clues here;
- these however are not supposed to replace a careful study of the sources.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{The adaption principle%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Figure \ref{fig:adaption} illustrates what \qt{adaption} is conceptually
- supposed to be:
-
- \begin{figure}[here]
- \includegraphics{adaption}
- \caption{The adaption principle}
- \label{fig:adaption}
- \end{figure}
-
- \noindent In the tame view, code generation acts as broker between
- \isa{logic}, \isa{intermediate\ language} and
- \isa{target\ language} by means of \isa{translation} and
- \isa{serialisation}; for the latter, the serialiser has to observe
- the structure of the \isa{language} itself plus some \isa{reserved}
- keywords which have to be avoided for generated code.
- However, if you consider \isa{adaption} mechanisms, the code generated
- by the serializer is just the tip of the iceberg:
-
- \begin{itemize}
- \item \isa{serialisation} can be \emph{parametrised} such that
- logical entities are mapped to target-specific ones
- (e.g. target-specific list syntax,
- see also \secref{sec:adaption_mechanisms})
- \item Such parametrisations can involve references to a
- target-specific standard \isa{library} (e.g. using
- the \isa{Haskell} \verb|Maybe| type instead
- of the \isa{HOL} \isa{option} type);
- if such are used, the corresponding identifiers
- (in our example, \verb|Maybe|, \verb|Nothing|
- and \verb|Just|) also have to be considered \isa{reserved}.
- \item Even more, the user can enrich the library of the
- target-language by providing code snippets
- (\qt{\isa{includes}}) which are prepended to
- any generated code (see \secref{sec:include}); this typically
- also involves further \isa{reserved} identifiers.
- \end{itemize}
-
- \noindent As figure \ref{fig:adaption} illustrates, all these adaption mechanisms
- have to act consistently; it is at the discretion of the user
- to take care for this.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Common adaption patterns%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{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 \isa{HOL}
- library; beside being useful in applications, they may serve
- as a tutorial for customising the code generator setup (see below
- \secref{sec:adaption_mechanisms}).
-
- \begin{description}
-
- \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by big
- integer literals in target languages.
- \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by
- character literals in target languages.
- \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char},
- but also offers treatment of character codes; includes
- \hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}.
- \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements natural numbers by integers,
- which in general will result in higher efficiency; pattern
- matching with \isa{{\isadigit{0}}} / \isa{Suc}
- is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}
- and \hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}.
- \item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] provides an additional datatype
- \isa{index} which is mapped to target-language built-in integers.
- Useful for code setups which involve e.g. indexing of
- target-language arrays.
- \item[\hyperlink{theory.Code-Message}{\mbox{\isa{Code{\isacharunderscore}Message}}}] provides an additional datatype
- \isa{message{\isacharunderscore}string} which is isomorphic to strings;
- \isa{message{\isacharunderscore}string}s are mapped to target-language strings.
- Useful for code setups which involve e.g. printing (error) messages.
-
- \end{description}
-
- \begin{warn}
- When importing any of these theories, they should form the last
- items in an import list. Since these theories adapt the
- code generator setup in a non-conservative fashion,
- strange effects may occur otherwise.
- \end{warn}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Parametrising serialisation \label{sec:adaption_mechanisms}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Consider the following function and its corresponding
- SML code:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{primrec}\isamarkupfalse%
-\ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype boola = True | False;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun anda x True = x\\
-\hspace*{0pt} ~| anda x False = False\\
-\hspace*{0pt} ~| anda True x = x\\
-\hspace*{0pt} ~| anda False x = False;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
-\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k,~l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Though this is correct code, it is a little bit unsatisfactory:
- boolean values and operators are materialised as distinguished
- entities with have nothing to do with the SML-built-in notion
- of \qt{bool}. This results in less readable code;
- additionally, eager evaluation may cause programs to
- loop or break which would perfectly terminate when
- the existing SML \verb|bool| would be used. To map
- the HOL \isa{bool} on SML \verb|bool|, we may use
- \qn{custom serialisations}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
-\ bool\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
-\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
-\ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\begin{isamarkuptext}%
-\noindent The \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor
- as arguments together with a list of custom serialisations.
- Each custom serialisation starts with a target language
- identifier followed by an expression, which during
- code serialisation is inserted whenever the type constructor
- would occur. For constants, \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements
- the corresponding mechanism. Each ``\verb|_|'' in
- a serialisation expression is treated as a placeholder
- for the type constructor's (the constant's) arguments.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
-\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k,~l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent This still is not perfect: the parentheses
- around the \qt{andalso} expression are superfluous.
- Though the serialiser
- by no means attempts to imitate the rich Isabelle syntax
- framework, it provides some common idioms, notably
- associative infixes with precedences which may be used here:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
-\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
-\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent The attentive reader may ask how we assert that no generated
- code will accidentally overwrite. For this reason the serialiser has
- an internal table of identifiers which have to be avoided to be used
- for new declarations. Initially, this table typically contains the
- keywords of the target language. It can be extended manually, thus avoiding
- accidental overwrites, using the \hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} command:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymSML}{\isachardoublequoteclose}\ bool\ true\ false\ andalso%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Next, we try to map HOL pairs to SML pairs, using the
- infix ``\verb|*|'' type constructor and parentheses:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
-\ {\isacharasterisk}\isanewline
-\ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
-\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
-\ Pair\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\begin{isamarkuptext}%
-\noindent The initial bang ``\verb|!|'' tells the serialiser
- never to put
- parentheses around the whole expression (they are already present),
- while the parentheses around argument place holders
- tell not to put parentheses around the arguments.
- The slash ``\verb|/|'' (followed by arbitrary white space)
- inserts a space which may be used as a break if necessary
- during pretty printing.
-
- These examples give a glimpse what mechanisms
- custom serialisations provide; however their usage
- requires careful thinking in order not to introduce
- inconsistencies -- or, in other words:
- custom serialisations are completely axiomatic.
-
- A further noteworthy details is that any special
- character in a custom serialisation may be quoted
- using ``\verb|'|''; thus, in
- ``\verb|fn '_ => _|'' the first
- ``\verb|_|'' is a proper underscore while the
- second ``\verb|_|'' is a placeholder.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{\isa{Haskell} serialisation%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-For convenience, the default
- \isa{HOL} setup for \isa{Haskell} maps the \isa{eq} class to
- its counterpart in \isa{Haskell}, giving custom serialisations
- for the class \isa{eq} (by command \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation
- \isa{eq{\isacharunderscore}class{\isachardot}eq}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{code{\isacharunderscore}class}\isamarkupfalse%
-\ eq\isanewline
-\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline
-\isanewline
-\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
-\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\begin{isamarkuptext}%
-\noindent A problem now occurs whenever a type which
- is an instance of \isa{eq} in \isa{HOL} is mapped
- on a \isa{Haskell}-built-in type which is also an instance
- of \isa{Haskell} \isa{Eq}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{typedecl}\isamarkupfalse%
-\ bar\isanewline
-\isanewline
-\isacommand{instantiation}\isamarkupfalse%
-\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
-\isakeyword{begin}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{instance}\isamarkupfalse%
-\ \isacommand{by}\isamarkupfalse%
-\ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline
-\isanewline
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isadelimquotett
-\ %
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
-\ bar\isanewline
-\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\begin{isamarkuptext}%
-\noindent The code generator would produce
- an additional instance, which of course is rejected by the \isa{Haskell}
- compiler.
- To suppress this additional instance, use
- \isa{code{\isacharunderscore}instance}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
-\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
-\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isamarkupsubsection{Enhancing the target language context \label{sec:include}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-In rare cases it is necessary to \emph{enrich} the context of a
- target language; this is accomplished using the \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}
- command:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{code{\isacharunderscore}include}\isamarkupfalse%
-\ Haskell\ {\isachardoublequoteopen}Errno{\isachardoublequoteclose}\isanewline
-{\isacharverbatimopen}errno\ i\ {\isacharequal}\ error\ {\isacharparenleft}{\isachardoublequote}Error\ number{\isacharcolon}\ {\isachardoublequote}\ {\isacharplus}{\isacharplus}\ show\ i{\isacharparenright}{\isacharverbatimclose}\isanewline
-\isanewline
-\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
-\ Haskell\ Errno%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\begin{isamarkuptext}%
-\noindent Such named \isa{include}s are then prepended to every generated code.
- Inspect such code in order to find out how \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} behaves
- with respect to a particular target language.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/Codegen/Thy/document/Further.tex Wed May 06 19:15:40 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Wed May 06 19:42:27 2009 +0200
@@ -132,7 +132,7 @@
\begin{isamarkuptext}%
\noindent The soundness of the \hyperlink{method.eval}{\mbox{\isa{eval}}} method depends crucially
on the correctness of the code generator; this is one of the reasons
- why you should not use adaption (see \secref{sec:adaption}) frivolously.%
+ why you should not use adaptation (see \secref{sec:adaptation}) frivolously.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Introduction.tex Wed May 06 19:15:40 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Wed May 06 19:42:27 2009 +0200
@@ -46,8 +46,8 @@
This manifests in the structure of this tutorial: after a short
conceptual introduction with an example (\secref{sec:intro}),
we discuss the generic customisation facilities (\secref{sec:program}).
- A further section (\secref{sec:adaption}) is dedicated to the matter of
- \qn{adaption} to specific target language environments. After some
+ A further section (\secref{sec:adaptation}) is dedicated to the matter of
+ \qn{adaptation} to specific target language environments. After some
further issues (\secref{sec:further}) we conclude with an overview
of some ML programming interfaces (\secref{sec:ml}).
@@ -229,7 +229,7 @@
\hspace*{0pt}module Example where {\char123}\\
\hspace*{0pt}\\
\hspace*{0pt}\\
-\hspace*{0pt}foldla ::~forall a b.~(a -> b -> a) -> a -> [b] -> a;\\
+\hspace*{0pt}foldla ::~forall a{\char95}1 b{\char95}1.~(a{\char95}1 -> b{\char95}1 -> a{\char95}1) -> a{\char95}1 -> [b{\char95}1] -> a{\char95}1;\\
\hspace*{0pt}foldla f a [] = a;\\
\hspace*{0pt}foldla f a (x :~xs) = foldla f (f a x) xs;\\
\hspace*{0pt}\\
--- a/doc-src/Codegen/Thy/document/Program.tex Wed May 06 19:15:40 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Program.tex Wed May 06 19:42:27 2009 +0200
@@ -766,10 +766,10 @@
\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
\hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\
\hspace*{0pt}\\
-\hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\
+\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
\hspace*{0pt}\\
\hspace*{0pt}fun member A{\char95}~x [] = false\\
-\hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqop A{\char95}~x y orelse member A{\char95}~x ys;\\
+\hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqa A{\char95}~x y orelse member A{\char95}~x ys;\\
\hspace*{0pt}\\
\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
--- a/doc-src/Codegen/Thy/examples/Example.hs Wed May 06 19:15:40 2009 +0200
+++ b/doc-src/Codegen/Thy/examples/Example.hs Wed May 06 19:42:27 2009 +0200
@@ -3,7 +3,7 @@
module Example where {
-foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;
+foldla :: forall a_1 b_1. (a_1 -> b_1 -> a_1) -> a_1 -> [b_1] -> a_1;
foldla f a [] = a;
foldla f a (x : xs) = foldla f (f a x) xs;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Codegen/Thy/pictures/adaptation.tex Wed May 06 19:42:27 2009 +0200
@@ -0,0 +1,52 @@
+
+\documentclass[12pt]{article}
+\usepackage{tikz}
+
+\begin{document}
+
+\thispagestyle{empty}
+\setlength{\fboxrule}{0.01pt}
+\setlength{\fboxsep}{4pt}
+
+\fcolorbox{white}{white}{
+
+\begin{tikzpicture}[scale = 0.5]
+ \tikzstyle water=[color = blue, thick]
+ \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
+ \tikzstyle process=[color = green, semithick, ->]
+ \tikzstyle adaptation=[color = red, semithick, ->]
+ \tikzstyle target=[color = black]
+ \foreach \x in {0, ..., 24}
+ \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
+ + (0.25, -0.25) cos + (0.25, 0.25);
+ \draw[style=ice] (1, 0) --
+ (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
+ \draw[style=ice] (9, 0) --
+ (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
+ \draw[style=ice] (15, -6) --
+ (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
+ \draw[style=process]
+ (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
+ \draw[style=process]
+ (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
+ \node (adaptation) at (11, -2) [style=adaptation] {adaptation};
+ \node at (19, 3) [rotate=90] {generated};
+ \node at (19.5, -5) {language};
+ \node at (19.5, -3) {library};
+ \node (includes) at (19.5, -1) {includes};
+ \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
+ \draw[style=process]
+ (includes) -- (serialisation);
+ \draw[style=process]
+ (reserved) -- (serialisation);
+ \draw[style=adaptation]
+ (adaptation) -- (serialisation);
+ \draw[style=adaptation]
+ (adaptation) -- (includes);
+ \draw[style=adaptation]
+ (adaptation) -- (reserved);
+\end{tikzpicture}
+
+}
+
+\end{document}
--- a/doc-src/Codegen/Thy/pictures/adaption.tex Wed May 06 19:15:40 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-
-\documentclass[12pt]{article}
-\usepackage{tikz}
-
-\begin{document}
-
-\thispagestyle{empty}
-\setlength{\fboxrule}{0.01pt}
-\setlength{\fboxsep}{4pt}
-
-\fcolorbox{white}{white}{
-
-\begin{tikzpicture}[scale = 0.5]
- \tikzstyle water=[color = blue, thick]
- \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
- \tikzstyle process=[color = green, semithick, ->]
- \tikzstyle adaption=[color = red, semithick, ->]
- \tikzstyle target=[color = black]
- \foreach \x in {0, ..., 24}
- \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
- + (0.25, -0.25) cos + (0.25, 0.25);
- \draw[style=ice] (1, 0) --
- (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
- \draw[style=ice] (9, 0) --
- (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
- \draw[style=ice] (15, -6) --
- (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
- \draw[style=process]
- (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
- \draw[style=process]
- (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
- \node (adaption) at (11, -2) [style=adaption] {adaption};
- \node at (19, 3) [rotate=90] {generated};
- \node at (19.5, -5) {language};
- \node at (19.5, -3) {library};
- \node (includes) at (19.5, -1) {includes};
- \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
- \draw[style=process]
- (includes) -- (serialisation);
- \draw[style=process]
- (reserved) -- (serialisation);
- \draw[style=adaption]
- (adaption) -- (serialisation);
- \draw[style=adaption]
- (adaption) -- (includes);
- \draw[style=adaption]
- (adaption) -- (reserved);
-\end{tikzpicture}
-
-}
-
-\end{document}
--- a/doc-src/Codegen/codegen.tex Wed May 06 19:15:40 2009 +0200
+++ b/doc-src/Codegen/codegen.tex Wed May 06 19:42:27 2009 +0200
@@ -32,7 +32,7 @@
\input{Thy/document/Introduction.tex}
\input{Thy/document/Program.tex}
-\input{Thy/document/Adaption.tex}
+\input{Thy/document/Adaptation.tex}
\input{Thy/document/Further.tex}
\input{Thy/document/ML.tex}
--- a/doc-src/IsarRef/Thy/Spec.thy Wed May 06 19:15:40 2009 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Wed May 06 19:42:27 2009 +0200
@@ -752,7 +752,11 @@
text {*
Isabelle/Pure's definitional schemes support certain forms of
- overloading (see \secref{sec:consts}). At most occassions
+ overloading (see \secref{sec:consts}). Overloading means that a
+ constant being declared as @{text "c :: \<alpha> decl"} may be
+ defined separately on type instances
+ @{text "c :: (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"}
+ for each type constructor @{text t}. At most occassions
overloading will be used in a Haskell-like fashion together with
type classes by means of @{command "instantiation"} (see
\secref{sec:class}). Sometimes low-level overloading is desirable.
@@ -782,7 +786,8 @@
A @{text "(unchecked)"} option disables global dependency checks for
the corresponding definition, which is occasionally useful for
- exotic overloading. It is at the discretion of the user to avoid
+ exotic overloading (see \secref{sec:consts} for a precise description).
+ It is at the discretion of the user to avoid
malformed theory specifications!
\end{description}
@@ -1065,10 +1070,7 @@
\end{itemize}
- Overloading means that a constant being declared as @{text "c :: \<alpha>
- decl"} may be defined separately on type instances @{text "c ::
- (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"} for each type constructor @{text
- t}. The right-hand side may mention overloaded constants
+ The right-hand side of overloaded definitions may mention overloaded constants
recursively at type instances corresponding to the immediate
argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}. Incomplete
specification patterns impose global constraints on all occurrences,
--- a/doc-src/IsarRef/Thy/document/Spec.tex Wed May 06 19:15:40 2009 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Wed May 06 19:42:27 2009 +0200
@@ -759,7 +759,11 @@
%
\begin{isamarkuptext}%
Isabelle/Pure's definitional schemes support certain forms of
- overloading (see \secref{sec:consts}). At most occassions
+ overloading (see \secref{sec:consts}). Overloading means that a
+ constant being declared as \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be
+ defined separately on type instances
+ \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}}
+ for each type constructor \isa{t}. At most occassions
overloading will be used in a Haskell-like fashion together with
type classes by means of \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see
\secref{sec:class}). Sometimes low-level overloading is desirable.
@@ -788,7 +792,8 @@
A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for
the corresponding definition, which is occasionally useful for
- exotic overloading. It is at the discretion of the user to avoid
+ exotic overloading (see \secref{sec:consts} for a precise description).
+ It is at the discretion of the user to avoid
malformed theory specifications!
\end{description}%
@@ -1092,7 +1097,7 @@
\end{itemize}
- Overloading means that a constant being declared as \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be defined separately on type instances \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}} for each type constructor \isa{t}. The right-hand side may mention overloaded constants
+ The right-hand side of overloaded definitions may mention overloaded constants
recursively at type instances corresponding to the immediate
argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}. Incomplete
specification patterns impose global constraints on all occurrences,
--- a/src/HOL/Code_Eval.thy Wed May 06 19:15:40 2009 +0200
+++ b/src/HOL/Code_Eval.thy Wed May 06 19:42:27 2009 +0200
@@ -33,7 +33,7 @@
struct
fun mk_term f g (Const (c, ty)) =
- @{term Const} $ Message_String.mk c $ g ty
+ @{term Const} $ HOLogic.mk_message_string c $ g ty
| mk_term f g (t1 $ t2) =
@{term App} $ mk_term f g t1 $ mk_term f g t2
| mk_term f g (Free v) = f v
@@ -154,7 +154,9 @@
(Eval "Term.Const/ (_, _)" and "Term.$/ (_, _)")
code_const "term_of \<Colon> message_string \<Rightarrow> term"
- (Eval "Message'_String.mk")
+ (Eval "HOLogic.mk'_message'_string")
+
+code_reserved Eval HOLogic
subsection {* Evaluation setup *}
--- a/src/HOL/Code_Message.thy Wed May 06 19:15:40 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Monolithic strings (message strings) for code generation *}
-
-theory Code_Message
-imports Plain "~~/src/HOL/List"
-begin
-
-subsection {* Datatype of messages *}
-
-datatype message_string = STR string
-
-lemmas [code del] = message_string.recs message_string.cases
-
-lemma [code]: "size (s\<Colon>message_string) = 0"
- by (cases s) simp_all
-
-lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
- by (cases s) simp_all
-
-subsection {* ML interface *}
-
-ML {*
-structure Message_String =
-struct
-
-fun mk s = @{term STR} $ HOLogic.mk_string s;
-
-end;
-*}
-
-
-subsection {* Code serialization *}
-
-code_type message_string
- (SML "string")
- (OCaml "string")
- (Haskell "String")
-
-setup {*
- fold (fn target => add_literal_message @{const_name STR} target)
- ["SML", "OCaml", "Haskell"]
-*}
-
-code_reserved SML string
-code_reserved OCaml string
-
-code_instance message_string :: eq
- (Haskell -)
-
-code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
- (SML "!((_ : string) = _)")
- (OCaml "!((_ : string) = _)")
- (Haskell infixl 4 "==")
-
-end
--- a/src/HOL/IsaMakefile Wed May 06 19:15:40 2009 +0200
+++ b/src/HOL/IsaMakefile Wed May 06 19:42:27 2009 +0200
@@ -206,7 +206,6 @@
MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
ATP_Linkup.thy \
Code_Eval.thy \
- Code_Message.thy \
Equiv_Relations.thy \
Groebner_Basis.thy \
Hilbert_Choice.thy \
@@ -220,6 +219,7 @@
Presburger.thy \
Recdef.thy \
SetInterval.thy \
+ String.thy \
$(SRC)/Provers/Arith/assoc_fold.ML \
$(SRC)/Provers/Arith/cancel_numeral_factor.ML \
$(SRC)/Provers/Arith/cancel_numerals.ML \
@@ -235,6 +235,7 @@
Tools/Groebner_Basis/normalizer.ML \
Tools/atp_manager.ML \
Tools/atp_wrapper.ML \
+ Tools/list_code.ML \
Tools/meson.ML \
Tools/metis_tools.ML \
Tools/numeral.ML \
@@ -252,6 +253,7 @@
Tools/res_hol_clause.ML \
Tools/res_reconstruct.ML \
Tools/specification_package.ML \
+ Tools/string_code.ML \
Tools/string_syntax.ML \
Tools/TFL/casesplit.ML \
Tools/TFL/dcterm.ML \
--- a/src/HOL/Library/Code_Char.thy Wed May 06 19:15:40 2009 +0200
+++ b/src/HOL/Library/Code_Char.thy Wed May 06 19:42:27 2009 +0200
@@ -14,8 +14,8 @@
(Haskell "Char")
setup {*
- fold (fn target => add_literal_char target) ["SML", "OCaml", "Haskell"]
- #> add_literal_list_string "Haskell"
+ fold String_Code.add_literal_char ["SML", "OCaml", "Haskell"]
+ #> String_Code.add_literal_list_string "Haskell"
*}
code_instance char :: eq
@@ -33,6 +33,6 @@
(Haskell infixl 4 "==")
code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term"
- (SML "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
+ (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
end
--- a/src/HOL/List.thy Wed May 06 19:15:40 2009 +0200
+++ b/src/HOL/List.thy Wed May 06 19:42:27 2009 +0200
@@ -6,7 +6,7 @@
theory List
imports Plain Presburger Recdef ATP_Linkup
-uses "Tools/string_syntax.ML"
+uses ("Tools/list_code.ML")
begin
datatype 'a list =
@@ -3433,77 +3433,6 @@
by (auto simp add: set_Cons_def intro: listrel.intros)
-subsection{*Miscellany*}
-
-subsubsection {* Characters and strings *}
-
-datatype nibble =
- Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
- | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
-
-lemma UNIV_nibble:
- "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
- Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
-proof (rule UNIV_eq_I)
- fix x show "x \<in> ?A" by (cases x) simp_all
-qed
-
-instance nibble :: finite
- by default (simp add: UNIV_nibble)
-
-datatype char = Char nibble nibble
- -- "Note: canonical order of character encoding coincides with standard term ordering"
-
-lemma UNIV_char:
- "UNIV = image (split Char) (UNIV \<times> UNIV)"
-proof (rule UNIV_eq_I)
- fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
-qed
-
-instance char :: finite
- by default (simp add: UNIV_char)
-
-lemma size_char [code, simp]:
- "size (c::char) = 0" by (cases c) simp
-
-lemma char_size [code, simp]:
- "char_size (c::char) = 0" by (cases c) simp
-
-primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
- "nibble_pair_of_char (Char n m) = (n, m)"
-
-declare nibble_pair_of_char.simps [code del]
-
-setup {*
-let
- val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
- val thms = map_product
- (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
- nibbles nibbles;
-in
- PureThy.note_thmss Thm.lemmaK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
- #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
-end
-*}
-
-lemma char_case_nibble_pair [code, code inline]:
- "char_case f = split f o nibble_pair_of_char"
- by (simp add: expand_fun_eq split: char.split)
-
-lemma char_rec_nibble_pair [code, code inline]:
- "char_rec f = split f o nibble_pair_of_char"
- unfolding char_case_nibble_pair [symmetric]
- by (simp add: expand_fun_eq split: char.split)
-
-types string = "char list"
-
-syntax
- "_Char" :: "xstr => char" ("CHR _")
- "_String" :: "xstr => string" ("_")
-
-setup StringSyntax.setup
-
-
subsection {* Size function *}
lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"
@@ -3527,10 +3456,35 @@
"(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
by (induct xs) force+
+
subsection {* Code generator *}
subsubsection {* Setup *}
+use "Tools/list_code.ML"
+
+code_type list
+ (SML "_ list")
+ (OCaml "_ list")
+ (Haskell "![_]")
+
+code_const Nil
+ (SML "[]")
+ (OCaml "[]")
+ (Haskell "[]")
+
+code_instance list :: eq
+ (Haskell -)
+
+code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
+ (Haskell infixl 4 "==")
+
+code_reserved SML
+ list
+
+code_reserved OCaml
+ list
+
types_code
"list" ("_ list")
attach (term_of) {*
@@ -3546,206 +3500,23 @@
(1, fn () => ([], fn () => HOLogic.nil_const aT))] ()
and gen_list aG aT i = gen_list' aG aT i i;
*}
- "char" ("string")
-attach (term_of) {*
-val term_of_char = HOLogic.mk_char o ord;
-*}
-attach (test) {*
-fun gen_char i =
- let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
- in (chr j, fn () => HOLogic.mk_char j) end;
-*}
-
-consts_code "Cons" ("(_ ::/ _)")
-
-code_type list
- (SML "_ list")
- (OCaml "_ list")
- (Haskell "![_]")
-
-code_reserved SML
- list
-
-code_reserved OCaml
- list
-
-code_const Nil
- (SML "[]")
- (OCaml "[]")
- (Haskell "[]")
-
-ML {*
-local
-
-open Basic_Code_Thingol;
-
-fun implode_list naming t = case pairself
- (Code_Thingol.lookup_const naming) (@{const_name Nil}, @{const_name Cons})
- of (SOME nil', SOME cons') => let
- fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
- if c = cons'
- then SOME (t1, t2)
- else NONE
- | dest_cons _ = NONE;
- val (ts, t') = Code_Thingol.unfoldr dest_cons t;
- in case t'
- of IConst (c, _) => if c = nil' then SOME ts else NONE
- | _ => NONE
- end
- | _ => NONE
-
-fun decode_char naming (IConst (c1, _), IConst (c2, _)) = (case map_filter
- (Code_Thingol.lookup_const naming)[@{const_name Nibble0}, @{const_name Nibble1},
- @{const_name Nibble2}, @{const_name Nibble3},
- @{const_name Nibble4}, @{const_name Nibble5},
- @{const_name Nibble6}, @{const_name Nibble7},
- @{const_name Nibble8}, @{const_name Nibble9},
- @{const_name NibbleA}, @{const_name NibbleB},
- @{const_name NibbleC}, @{const_name NibbleD},
- @{const_name NibbleE}, @{const_name NibbleF}]
- of nibbles' as [_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _] => let
- fun idx c = find_index (curry (op =) c) nibbles';
- fun decode ~1 _ = NONE
- | decode _ ~1 = NONE
- | decode n m = SOME (chr (n * 16 + m));
- in decode (idx c1) (idx c2) end
- | _ => NONE)
- | decode_char _ _ = NONE
-
-fun implode_string naming mk_char mk_string ts = case
- Code_Thingol.lookup_const naming @{const_name Char}
- of SOME char' => let
- fun implode_char (IConst (c, _) `$ t1 `$ t2) =
- if c = char' then decode_char naming (t1, t2) else NONE
- | implode_char _ = NONE;
- val ts' = map implode_char ts;
- in if forall is_some ts'
- then (SOME o Code_Printer.str o mk_string o implode o map_filter I) ts'
- else NONE
- end
- | _ => NONE;
-
-fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
- Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
- pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
- Code_Printer.str target_cons,
- pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
- ];
-
-fun pretty_list literals =
- let
- val mk_list = Code_Printer.literal_list literals;
- fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
- case Option.map (cons t1) (implode_list naming t2)
- of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
- | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
- in (2, pretty) end;
-
-fun pretty_list_string literals =
- let
- val mk_list = Code_Printer.literal_list literals;
- val mk_char = Code_Printer.literal_char literals;
- val mk_string = Code_Printer.literal_string literals;
- fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
- case Option.map (cons t1) (implode_list naming t2)
- of SOME ts => (case implode_string naming mk_char mk_string ts
- of SOME p => p
- | NONE => mk_list (map (pr vars Code_Printer.NOBR) ts))
- | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
- in (2, pretty) end;
-
-fun pretty_char literals =
- let
- val mk_char = Code_Printer.literal_char literals;
- fun pretty _ naming thm _ _ [(t1, _), (t2, _)] =
- case decode_char naming (t1, t2)
- of SOME c => (Code_Printer.str o mk_char) c
- | NONE => Code_Printer.nerror thm "Illegal character expression";
- in (2, pretty) end;
-
-fun pretty_message literals =
- let
- val mk_char = Code_Printer.literal_char literals;
- val mk_string = Code_Printer.literal_string literals;
- fun pretty _ naming thm _ _ [(t, _)] =
- case implode_list naming t
- of SOME ts => (case implode_string naming mk_char mk_string ts
- of SOME p => p
- | NONE => Code_Printer.nerror thm "Illegal message expression")
- | NONE => Code_Printer.nerror thm "Illegal message expression";
- in (1, pretty) end;
-
-in
-
-fun add_literal_list target thy =
- let
- val pr = pretty_list (Code_Target.the_literals thy target);
- in
- thy
- |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
- end;
-
-fun add_literal_list_string target thy =
- let
- val pr = pretty_list_string (Code_Target.the_literals thy target);
- in
- thy
- |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
- end;
-
-fun add_literal_char target thy =
- let
- val pr = pretty_char (Code_Target.the_literals thy target);
- in
- thy
- |> Code_Target.add_syntax_const target @{const_name Char} (SOME pr)
- end;
-
-fun add_literal_message str target thy =
- let
- val pr = pretty_message (Code_Target.the_literals thy target);
- in
- thy
- |> Code_Target.add_syntax_const target str (SOME pr)
- end;
-
-end;
-*}
-
-setup {*
- fold (fn target => add_literal_list target) ["SML", "OCaml", "Haskell"]
-*}
-
-code_instance list :: eq
- (Haskell -)
-
-code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
- (Haskell infixl 4 "==")
+
+consts_code Cons ("(_ ::/ _)")
setup {*
let
-
-fun list_codegen thy defs dep thyname b t gr =
- let
- val ts = HOLogic.dest_list t;
- val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
- (fastype_of t) gr;
- val (ps, gr'') = fold_map
- (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
- in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
-
-fun char_codegen thy defs dep thyname b t gr =
- let
- val i = HOLogic.dest_char t;
- val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
- (fastype_of t) gr;
- in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
- end handle TERM _ => NONE;
-
+ fun list_codegen thy defs dep thyname b t gr =
+ let
+ val ts = HOLogic.dest_list t;
+ val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
+ (fastype_of t) gr;
+ val (ps, gr'') = fold_map
+ (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
+ in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
in
- Codegen.add_codegen "list_codegen" list_codegen
- #> Codegen.add_codegen "char_codegen" char_codegen
-end;
+ fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell"]
+ #> Codegen.add_codegen "list_codegen" list_codegen
+end
*}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/String.thy Wed May 06 19:42:27 2009 +0200
@@ -0,0 +1,150 @@
+(* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *)
+
+header {* Character and string types *}
+
+theory String
+imports List
+uses
+ "Tools/string_syntax.ML"
+ ("Tools/string_code.ML")
+begin
+
+subsection {* Characters *}
+
+datatype nibble =
+ Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
+ | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
+
+lemma UNIV_nibble:
+ "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
+ Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
+proof (rule UNIV_eq_I)
+ fix x show "x \<in> ?A" by (cases x) simp_all
+qed
+
+instance nibble :: finite
+ by default (simp add: UNIV_nibble)
+
+datatype char = Char nibble nibble
+ -- "Note: canonical order of character encoding coincides with standard term ordering"
+
+lemma UNIV_char:
+ "UNIV = image (split Char) (UNIV \<times> UNIV)"
+proof (rule UNIV_eq_I)
+ fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
+qed
+
+instance char :: finite
+ by default (simp add: UNIV_char)
+
+lemma size_char [code, simp]:
+ "size (c::char) = 0" by (cases c) simp
+
+lemma char_size [code, simp]:
+ "char_size (c::char) = 0" by (cases c) simp
+
+primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
+ "nibble_pair_of_char (Char n m) = (n, m)"
+
+declare nibble_pair_of_char.simps [code del]
+
+setup {*
+let
+ val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
+ val thms = map_product
+ (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
+ nibbles nibbles;
+in
+ PureThy.note_thmss Thm.lemmaK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
+ #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
+end
+*}
+
+lemma char_case_nibble_pair [code, code inline]:
+ "char_case f = split f o nibble_pair_of_char"
+ by (simp add: expand_fun_eq split: char.split)
+
+lemma char_rec_nibble_pair [code, code inline]:
+ "char_rec f = split f o nibble_pair_of_char"
+ unfolding char_case_nibble_pair [symmetric]
+ by (simp add: expand_fun_eq split: char.split)
+
+syntax
+ "_Char" :: "xstr => char" ("CHR _")
+
+
+subsection {* Strings *}
+
+types string = "char list"
+
+syntax
+ "_String" :: "xstr => string" ("_")
+
+setup StringSyntax.setup
+
+
+subsection {* Strings as dedicated datatype *}
+
+datatype message_string = STR string
+
+lemmas [code del] =
+ message_string.recs message_string.cases
+
+lemma [code]: "size (s\<Colon>message_string) = 0"
+ by (cases s) simp_all
+
+lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
+ by (cases s) simp_all
+
+
+subsection {* Code generator *}
+
+use "Tools/string_code.ML"
+
+code_type message_string
+ (SML "string")
+ (OCaml "string")
+ (Haskell "String")
+
+setup {*
+ fold String_Code.add_literal_message ["SML", "OCaml", "Haskell"]
+*}
+
+code_instance message_string :: eq
+ (Haskell -)
+
+code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
+ (SML "!((_ : string) = _)")
+ (OCaml "!((_ : string) = _)")
+ (Haskell infixl 4 "==")
+
+code_reserved SML string
+code_reserved OCaml string
+
+
+types_code
+ "char" ("string")
+attach (term_of) {*
+val term_of_char = HOLogic.mk_char o ord;
+*}
+attach (test) {*
+fun gen_char i =
+ let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
+ in (chr j, fn () => HOLogic.mk_char j) end;
+*}
+
+setup {*
+let
+
+fun char_codegen thy defs dep thyname b t gr =
+ let
+ val i = HOLogic.dest_char t;
+ val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
+ (fastype_of t) gr;
+ in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
+ end handle TERM _ => NONE;
+
+in Codegen.add_codegen "char_codegen" char_codegen end
+*}
+
+end
\ No newline at end of file
--- a/src/HOL/Tools/hologic.ML Wed May 06 19:15:40 2009 +0200
+++ b/src/HOL/Tools/hologic.ML Wed May 06 19:42:27 2009 +0200
@@ -116,6 +116,9 @@
val stringT: typ
val mk_string: string -> term
val dest_string: term -> string
+ val message_stringT: typ
+ val mk_message_string: string -> term
+ val dest_message_string: term -> string
end;
structure HOLogic: HOLOGIC =
@@ -510,44 +513,6 @@
val realT = Type ("RealDef.real", []);
-(* nibble *)
-
-val nibbleT = Type ("List.nibble", []);
-
-fun mk_nibble n =
- let val s =
- if 0 <= n andalso n <= 9 then chr (n + ord "0")
- else if 10 <= n andalso n <= 15 then chr (n + ord "A" - 10)
- else raise TERM ("mk_nibble", [])
- in Const ("List.nibble.Nibble" ^ s, nibbleT) end;
-
-fun dest_nibble t =
- let fun err () = raise TERM ("dest_nibble", [t]) in
- (case try (unprefix "List.nibble.Nibble" o fst o Term.dest_Const) t of
- NONE => err ()
- | SOME c =>
- if size c <> 1 then err ()
- else if "0" <= c andalso c <= "9" then ord c - ord "0"
- else if "A" <= c andalso c <= "F" then ord c - ord "A" + 10
- else err ())
- end;
-
-
-(* char *)
-
-val charT = Type ("List.char", []);
-
-fun mk_char n =
- if 0 <= n andalso n <= 255 then
- Const ("List.char.Char", nibbleT --> nibbleT --> charT) $
- mk_nibble (n div 16) $ mk_nibble (n mod 16)
- else raise TERM ("mk_char", []);
-
-fun dest_char (Const ("List.char.Char", _) $ t $ u) =
- dest_nibble t * 16 + dest_nibble u
- | dest_char t = raise TERM ("dest_char", [t]);
-
-
(* list *)
fun listT T = Type ("List.list", [T]);
@@ -570,11 +535,60 @@
| dest_list t = raise TERM ("dest_list", [t]);
+(* nibble *)
+
+val nibbleT = Type ("String.nibble", []);
+
+fun mk_nibble n =
+ let val s =
+ if 0 <= n andalso n <= 9 then chr (n + ord "0")
+ else if 10 <= n andalso n <= 15 then chr (n + ord "A" - 10)
+ else raise TERM ("mk_nibble", [])
+ in Const ("String.nibble.Nibble" ^ s, nibbleT) end;
+
+fun dest_nibble t =
+ let fun err () = raise TERM ("dest_nibble", [t]) in
+ (case try (unprefix "String.nibble.Nibble" o fst o Term.dest_Const) t of
+ NONE => err ()
+ | SOME c =>
+ if size c <> 1 then err ()
+ else if "0" <= c andalso c <= "9" then ord c - ord "0"
+ else if "A" <= c andalso c <= "F" then ord c - ord "A" + 10
+ else err ())
+ end;
+
+
+(* char *)
+
+val charT = Type ("String.char", []);
+
+fun mk_char n =
+ if 0 <= n andalso n <= 255 then
+ Const ("String.char.Char", nibbleT --> nibbleT --> charT) $
+ mk_nibble (n div 16) $ mk_nibble (n mod 16)
+ else raise TERM ("mk_char", []);
+
+fun dest_char (Const ("String.char.Char", _) $ t $ u) =
+ dest_nibble t * 16 + dest_nibble u
+ | dest_char t = raise TERM ("dest_char", [t]);
+
+
(* string *)
-val stringT = Type ("List.string", []);
+val stringT = Type ("String.string", []);
val mk_string = mk_list charT o map (mk_char o ord) o explode;
val dest_string = implode o map (chr o dest_char) o dest_list;
+
+(* message_string *)
+
+val message_stringT = Type ("String.message_string", []);
+
+fun mk_message_string s = Const ("String.message_string.STR", stringT --> message_stringT)
+ $ mk_string s;
+fun dest_message_string (Const ("String.message_string.STR", _) $ t) =
+ dest_string t
+ | dest_message_string t = raise TERM ("dest_message_string", [t]);
+
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/list_code.ML Wed May 06 19:42:27 2009 +0200
@@ -0,0 +1,52 @@
+(* Author: Florian Haftmann, TU Muenchen
+
+Code generation for list literals.
+*)
+
+signature LIST_CODE =
+sig
+ val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
+ val default_list: int * string
+ -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
+ -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
+ val add_literal_list: string -> theory -> theory
+end;
+
+structure List_Code : LIST_CODE =
+struct
+
+open Basic_Code_Thingol;
+
+fun implode_list nil' cons' t =
+ let
+ fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
+ if c = cons'
+ then SOME (t1, t2)
+ else NONE
+ | dest_cons _ = NONE;
+ val (ts, t') = Code_Thingol.unfoldr dest_cons t;
+ in case t'
+ of IConst (c, _) => if c = nil' then SOME ts else NONE
+ | _ => NONE
+ end;
+
+fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
+ Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
+ pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
+ Code_Printer.str target_cons,
+ pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
+ ];
+
+fun add_literal_list target =
+ let
+ fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
+ case Option.map (cons t1) (implode_list nil' cons' t2)
+ of SOME ts =>
+ Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
+ | NONE =>
+ default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
+ in Code_Target.add_syntax_const target
+ @{const_name Cons} (SOME (2, ([@{const_name Nil}, @{const_name Cons}], pretty)))
+ end
+
+end;
--- a/src/HOL/Tools/numeral.ML Wed May 06 19:15:40 2009 +0200
+++ b/src/HOL/Tools/numeral.ML Wed May 06 19:42:27 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/numeral.ML
- ID: $Id$
Author: Makarius
Logical operations on numerals (see also HOL/hologic.ML).
@@ -59,13 +58,8 @@
fun add_code number_of negative unbounded target thy =
let
- val pr_numeral = (Code_Printer.literal_numeral o Code_Target.the_literals thy) target;
- fun dest_numeral naming thm =
+ fun dest_numeral pls' min' bit0' bit1' thm =
let
- val SOME pls' = Code_Thingol.lookup_const naming @{const_name Int.Pls};
- val SOME min' = Code_Thingol.lookup_const naming @{const_name Int.Min};
- val SOME bit0' = Code_Thingol.lookup_const naming @{const_name Int.Bit0};
- val SOME bit1' = Code_Thingol.lookup_const naming @{const_name Int.Bit1};
fun dest_bit (IConst (c, _)) = if c = bit0' then 0
else if c = bit1' then 1
else Code_Printer.nerror thm "Illegal numeral expression: illegal bit"
@@ -79,11 +73,12 @@
in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
| dest_num _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
in dest_num end;
- fun pretty _ naming thm _ _ [(t, _)] =
- (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral naming thm) t;
+ fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
+ (Code_Printer.str o Code_Printer.literal_numeral literals unbounded
+ o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
in
- thy
- |> Code_Target.add_syntax_const target number_of (SOME (1, pretty))
+ thy |> Code_Target.add_syntax_const target number_of
+ (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min}, @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
end;
end; (*local*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/string_code.ML Wed May 06 19:42:27 2009 +0200
@@ -0,0 +1,88 @@
+(* Author: Florian Haftmann, TU Muenchen
+
+Code generation for character and string literals.
+*)
+
+signature STRING_CODE =
+sig
+ val add_literal_list_string: string -> theory -> theory
+ val add_literal_char: string -> theory -> theory
+ val add_literal_message: string -> theory -> theory
+end;
+
+structure String_Code : STRING_CODE =
+struct
+
+open Basic_Code_Thingol;
+
+fun decode_char nibbles' tt =
+ let
+ fun idx c = find_index (curry (op =) c) nibbles';
+ fun decode ~1 _ = NONE
+ | decode _ ~1 = NONE
+ | decode n m = SOME (chr (n * 16 + m));
+ in case tt
+ of (IConst (c1, _), IConst (c2, _)) => decode (idx c1) (idx c2)
+ | _ => NONE
+ end;
+
+fun implode_string char' nibbles' mk_char mk_string ts =
+ let
+ fun implode_char (IConst (c, _) `$ t1 `$ t2) =
+ if c = char' then decode_char nibbles' (t1, t2) else NONE
+ | implode_char _ = NONE;
+ val ts' = map_filter implode_char ts;
+ in if length ts = length ts'
+ then (SOME o Code_Printer.str o mk_string o implode) ts'
+ else NONE
+ end;
+
+val cs_nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
+ @{const_name Nibble2}, @{const_name Nibble3},
+ @{const_name Nibble4}, @{const_name Nibble5},
+ @{const_name Nibble6}, @{const_name Nibble7},
+ @{const_name Nibble8}, @{const_name Nibble9},
+ @{const_name NibbleA}, @{const_name NibbleB},
+ @{const_name NibbleC}, @{const_name NibbleD},
+ @{const_name NibbleE}, @{const_name NibbleF}];
+val cs_summa = [@{const_name Nil}, @{const_name Cons}, @{const_name Char}] @ cs_nibbles;
+
+fun add_literal_list_string target =
+ let
+ fun pretty literals (nil' :: cons' :: char' :: nibbles') pr thm vars fxy [(t1, _), (t2, _)] =
+ case Option.map (cons t1) (List_Code.implode_list nil' cons' t2)
+ of SOME ts => (case implode_string char' nibbles'
+ (Code_Printer.literal_char literals) (Code_Printer.literal_string literals) ts
+ of SOME p => p
+ | NONE =>
+ Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
+ | NONE =>
+ List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
+ in Code_Target.add_syntax_const target
+ @{const_name Cons} (SOME (2, (cs_summa, pretty)))
+ end;
+
+fun add_literal_char target =
+ let
+ fun pretty literals nibbles' _ thm _ _ [(t1, _), (t2, _)] =
+ case decode_char nibbles' (t1, t2)
+ of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
+ | NONE => Code_Printer.nerror thm "Illegal character expression";
+ in Code_Target.add_syntax_const target
+ @{const_name Char} (SOME (2, (cs_nibbles, pretty)))
+ end;
+
+fun add_literal_message target =
+ let
+ fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
+ case List_Code.implode_list nil' cons' t
+ of SOME ts => (case implode_string char' nibbles'
+ (Code_Printer.literal_char literals) (Code_Printer.literal_string literals) ts
+ of SOME p => p
+ | NONE => Code_Printer.nerror thm "Illegal message expression")
+ | NONE => Code_Printer.nerror thm "Illegal message expression";
+ in Code_Target.add_syntax_const target
+ @{const_name STR} (SOME (1, (cs_summa, pretty)))
+ end;
+
+end;
--- a/src/HOL/Tools/string_syntax.ML Wed May 06 19:15:40 2009 +0200
+++ b/src/HOL/Tools/string_syntax.ML Wed May 06 19:42:27 2009 +0200
@@ -15,12 +15,14 @@
(* nibble *)
+val nib_prefix = "String.nibble.";
+
val mk_nib =
- Syntax.Constant o unprefix "List.nibble." o
+ Syntax.Constant o unprefix nib_prefix o
fst o Term.dest_Const o HOLogic.mk_nibble;
fun dest_nib (Syntax.Constant c) =
- HOLogic.dest_nibble (Const ("List.nibble." ^ c, dummyT))
+ HOLogic.dest_nibble (Const (nib_prefix ^ c, dummyT))
handle TERM _ => raise Match;
--- a/src/HOL/Typerep.thy Wed May 06 19:15:40 2009 +0200
+++ b/src/HOL/Typerep.thy Wed May 06 19:42:27 2009 +0200
@@ -1,11 +1,9 @@
-(* Title: HOL/Typerep.thy
- Author: Florian Haftmann, TU Muenchen
-*)
+(* Author: Florian Haftmann, TU Muenchen *)
header {* Reflecting Pure types into HOL *}
theory Typerep
-imports Plain List Code_Message
+imports Plain String
begin
datatype typerep = Typerep message_string "typerep list"
@@ -42,7 +40,7 @@
struct
fun mk f (Type (tyco, tys)) =
- @{term Typerep} $ Message_String.mk tyco
+ @{term Typerep} $ HOLogic.mk_message_string tyco
$ HOLogic.mk_list @{typ typerep} (map (mk f) tys)
| mk f (TFree v) =
f v;
--- a/src/Tools/code/code_haskell.ML Wed May 06 19:15:40 2009 +0200
+++ b/src/Tools/code/code_haskell.ML Wed May 06 19:42:27 2009 +0200
@@ -31,7 +31,7 @@
| pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
in gen_pr_bind pr_bind pr_term end;
-fun pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const
+fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
init_syms deresolve is_cons contr_classparam_typs deriving_show =
let
val deresolve_base = Long_Name.base_name o deresolve;
@@ -96,7 +96,7 @@
(str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
else (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
end
- and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const naming
+ and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const
and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
let
@@ -261,7 +261,7 @@
val vars = init_syms
|> Code_Printer.intro_vars (the_list const)
|> Code_Printer.intro_vars vs;
- val lhs = IConst (classparam, ([], tys)) `$$ map IVar vs;
+ val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
(*dictionaries are not relevant at this late stage*)
in
semicolon [
@@ -336,7 +336,7 @@
fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
raw_reserved_names includes raw_module_alias
- syntax_class syntax_tyco syntax_const naming program cs destination =
+ syntax_class syntax_tyco syntax_const program cs destination =
let
val stmt_names = Code_Target.stmt_names_of_destination destination;
val module_name = if null stmt_names then raw_module_name else SOME "Code";
@@ -358,7 +358,7 @@
| deriv' _ (ITyVar _) = true
in deriv [] tyco end;
val reserved_names = Code_Printer.make_vars reserved_names;
- fun pr_stmt qualified = pr_haskell_stmt naming labelled_name
+ fun pr_stmt qualified = pr_haskell_stmt labelled_name
syntax_class syntax_tyco syntax_const reserved_names
(if qualified then deresolver else Long_Name.base_name o deresolver)
is_cons contr_classparam_typs
@@ -469,14 +469,14 @@
| pr_monad pr_bind pr (SOME (bind, false), t) vars = vars
|> pr_bind NOBR bind
|>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
- fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
+ fun pretty _ [c_bind'] pr thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
of SOME (bind, t') => let
- val (binds, t'') = implode_monad ((the o Code_Thingol.lookup_const naming) c_bind) t'
+ val (binds, t'') = implode_monad c_bind' t'
val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K pr) thm) pr) (bind :: binds) vars;
in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end
| NONE => brackify_infix (1, L) fxy
[pr vars (INFX (1, L)) t1, str ">>=", pr vars (INFX (1, X)) t2]
- in (2, pretty) end;
+ in (2, ([c_bind], pretty)) end;
fun add_monad target' raw_c_bind thy =
let
--- a/src/Tools/code/code_ml.ML Wed May 06 19:15:40 2009 +0200
+++ b/src/Tools/code/code_ml.ML Wed May 06 19:42:27 2009 +0200
@@ -45,7 +45,7 @@
(** SML serailizer **)
-fun pr_sml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
+fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
let
val pr_label_classrel = translate_string (fn "." => "__" | c => c)
o Long_Name.qualifier;
@@ -109,7 +109,7 @@
then pr_case is_closure thm vars fxy cases
else pr_app is_closure thm vars fxy c_ts
| NONE => pr_case is_closure thm vars fxy cases)
- and pr_app' is_closure thm vars (app as ((c, (iss, tys)), ts)) =
+ and pr_app' is_closure thm vars (app as ((c, ((_, iss), tys)), ts)) =
if is_cons c then
let
val k = length tys
@@ -124,7 +124,7 @@
(str o deresolve) c
:: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts
and pr_app is_closure thm vars = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
- syntax_const naming thm vars
+ syntax_const thm vars
and pr_bind' ((NONE, NONE), _) = str "_"
| pr_bind' ((SOME v, NONE), _) = str v
| pr_bind' ((NONE, SOME p), _) = p
@@ -360,7 +360,7 @@
(** OCaml serializer **)
-fun pr_ocaml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
+fun pr_ocaml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
let
fun pr_dicts fxy ds =
let
@@ -414,7 +414,7 @@
then pr_case is_closure thm vars fxy cases
else pr_app is_closure thm vars fxy c_ts
| NONE => pr_case is_closure thm vars fxy cases)
- and pr_app' is_closure thm vars (app as ((c, (iss, tys)), ts)) =
+ and pr_app' is_closure thm vars (app as ((c, ((_, iss), tys)), ts)) =
if is_cons c then
if length tys = length ts
then case ts
@@ -428,7 +428,7 @@
else (str o deresolve) c
:: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts)
and pr_app is_closure = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
- syntax_const naming
+ syntax_const
and pr_bind' ((NONE, NONE), _) = str "_"
| pr_bind' ((SOME v, NONE), _) = str v
| pr_bind' ((NONE, SOME p), _) = p
@@ -909,7 +909,7 @@
in (deresolver, nodes) end;
fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
- _ syntax_tyco syntax_const naming program stmt_names destination =
+ _ syntax_tyco syntax_const program stmt_names destination =
let
val is_cons = Code_Thingol.is_cons program;
val present_stmt_names = Code_Target.stmt_names_of_destination destination;
@@ -924,7 +924,7 @@
(null o filter (member (op =) present_stmt_names) o stmt_names_of) stmt
then NONE
else SOME
- (pr_stmt naming labelled_name syntax_tyco syntax_const reserved_names
+ (pr_stmt labelled_name syntax_tyco syntax_const reserved_names
(deresolver prefix) is_cons stmt)
| pr_node prefix (Module (module_name, (_, nodes))) =
separate (str "")
--- a/src/Tools/code/code_printer.ML Wed May 06 19:15:40 2009 +0200
+++ b/src/Tools/code/code_printer.ML Wed May 06 19:42:27 2009 +0200
@@ -23,6 +23,17 @@
val intro_vars: string list -> var_ctxt -> var_ctxt
val lookup_var: var_ctxt -> string -> string
+ type literals
+ val Literals: { literal_char: string -> string, literal_string: string -> string,
+ literal_numeral: bool -> int -> string,
+ literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
+ -> literals
+ val literal_char: literals -> string -> string
+ val literal_string: literals -> string -> string
+ val literal_numeral: literals -> bool -> int -> string
+ val literal_list: literals -> Pretty.T list -> Pretty.T
+ val infix_cons: literals -> int * string
+
type lrx
val L: lrx
val R: lrx
@@ -41,6 +52,7 @@
type dict = Code_Thingol.dict
type tyco_syntax
type const_syntax
+ type proto_const_syntax
val parse_infix: ('a -> 'b) -> lrx * int -> string
-> int * ((fixity -> 'b -> Pretty.T)
-> fixity -> 'a list -> Pretty.T)
@@ -48,26 +60,18 @@
-> (int * ((fixity -> 'b -> Pretty.T)
-> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T)
- -> fixity -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option
+ -> fixity -> (iterm * itype) list -> Pretty.T)) option -> proto_const_syntax option
+ val activate_const_syntax: theory -> literals
+ -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
val gen_pr_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list)
-> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
- -> (string -> const_syntax option) -> Code_Thingol.naming
+ -> (string -> const_syntax option)
-> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
-> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm -> fixity
-> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
- type literals
- val Literals: { literal_char: string -> string, literal_string: string -> string,
- literal_numeral: bool -> int -> string, literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
- -> literals
- val literal_char: literals -> string -> string
- val literal_string: literals -> string -> string
- val literal_numeral: literals -> bool -> int -> string
- val literal_list: literals -> Pretty.T list -> Pretty.T
- val infix_cons: literals -> int * string
-
val mk_name_module: Name.context -> string option -> (string -> string option)
-> 'a Graph.T -> string -> string
val dest_name: string -> string * string
@@ -115,6 +119,25 @@
val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
+(** pretty literals **)
+
+datatype literals = Literals of {
+ literal_char: string -> string,
+ literal_string: string -> string,
+ literal_numeral: bool -> int -> string,
+ literal_list: Pretty.T list -> Pretty.T,
+ infix_cons: int * string
+};
+
+fun dest_Literals (Literals lits) = lits;
+
+val literal_char = #literal_char o dest_Literals;
+val literal_string = #literal_string o dest_Literals;
+val literal_numeral = #literal_numeral o dest_Literals;
+val literal_list = #literal_list o dest_Literals;
+val infix_cons = #infix_cons o dest_Literals;
+
+
(** syntax printer **)
(* binding priorities *)
@@ -158,17 +181,25 @@
type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
-> fixity -> itype list -> Pretty.T);
type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
- -> Code_Thingol.naming -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+ -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+type proto_const_syntax = int * (string list * (literals -> string list
+ -> (var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
-fun simple_const_syntax x = (Option.map o apsnd)
- (fn pretty => fn pr => fn naming => fn thm => fn vars => pretty (pr vars)) x;
+fun simple_const_syntax (SOME (n, f)) = SOME (n,
+ ([], (fn _ => fn _ => fn pr => fn thm => fn vars => f (pr vars))))
+ | simple_const_syntax NONE = NONE;
-fun gen_pr_app pr_app pr_term syntax_const naming thm vars fxy (app as ((c, (_, tys)), ts)) =
+fun activate_const_syntax thy literals (n, (cs, f)) naming =
+ fold_map (Code_Thingol.ensure_declared_const thy) cs naming
+ |-> (fn cs' => pair (n, f literals cs'));
+
+fun gen_pr_app pr_app pr_term syntax_const thm vars fxy (app as ((c, (_, tys)), ts)) =
case syntax_const c
of NONE => brackify fxy (pr_app thm vars app)
| SOME (k, pr) =>
let
- fun pr' fxy ts = pr (pr_term thm) naming thm vars fxy (ts ~~ curry Library.take k tys);
+ fun pr' fxy ts = pr (pr_term thm) thm vars fxy (ts ~~ curry Library.take k tys);
in if k = length ts
then pr' fxy ts
else if k < length ts
@@ -253,25 +284,6 @@
val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK];
-(** pretty literals **)
-
-datatype literals = Literals of {
- literal_char: string -> string,
- literal_string: string -> string,
- literal_numeral: bool -> int -> string,
- literal_list: Pretty.T list -> Pretty.T,
- infix_cons: int * string
-};
-
-fun dest_Literals (Literals lits) = lits;
-
-val literal_char = #literal_char o dest_Literals;
-val literal_string = #literal_string o dest_Literals;
-val literal_numeral = #literal_numeral o dest_Literals;
-val literal_list = #literal_list o dest_Literals;
-val infix_cons = #infix_cons o dest_Literals;
-
-
(** module name spaces **)
val dest_name =
--- a/src/Tools/code/code_target.ML Wed May 06 19:15:40 2009 +0200
+++ b/src/Tools/code/code_target.ML Wed May 06 19:42:27 2009 +0200
@@ -44,7 +44,7 @@
val add_syntax_class: string -> class -> string option -> theory -> theory
val add_syntax_inst: string -> string * class -> bool -> theory -> theory
val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
- val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
+ val add_syntax_const: string -> string -> proto_const_syntax option -> theory -> theory
val add_reserved: string -> string -> theory -> theory
end;
@@ -86,7 +86,7 @@
class: string Symtab.table,
instance: unit Symreltab.table,
tyco: tyco_syntax Symtab.table,
- const: const_syntax Symtab.table
+ const: proto_const_syntax Symtab.table
};
fun mk_name_syntax_table ((class, instance), (tyco, const)) =
@@ -112,7 +112,6 @@
-> (string -> string option) (*class syntax*)
-> (string -> tyco_syntax option)
-> (string -> const_syntax option)
- -> Code_Thingol.naming
-> Code_Thingol.program
-> string list (*selected statements*)
-> serialization;
@@ -402,19 +401,34 @@
val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco
in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
-fun invoke_serializer thy abortable serializer reserved abs_includes
+fun activate_syntax lookup_name src_tab = Symtab.empty
+ |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
+ of SOME name => (SOME name,
+ Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
+ | NONE => (NONE, tab)) (Symtab.keys src_tab)
+ |>> map_filter I;
+
+fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming)
+ |> fold_map (fn thing_identifier => fn (tab, naming) =>
+ case Code_Thingol.lookup_const naming thing_identifier
+ of SOME name => let
+ val (syn, naming') = Code_Printer.activate_const_syntax thy
+ literals (the (Symtab.lookup src_tab thing_identifier)) naming
+ in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
+ | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
+ |>> map_filter I;
+
+fun invoke_serializer thy abortable serializer literals reserved abs_includes
module_alias class instance tyco const module args naming program2 names1 =
let
- fun distill_names lookup_name src_tab = Symtab.empty
- |> fold_map (fn thing_identifier => fn tab => case lookup_name naming thing_identifier
- of SOME name => (SOME name, Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
- | NONE => (NONE, tab)) (Symtab.keys src_tab)
- |>> map_filter I;
- val (names_class, class') = distill_names Code_Thingol.lookup_class class;
+ val (names_class, class') =
+ activate_syntax (Code_Thingol.lookup_class naming) class;
val names_inst = map_filter (Code_Thingol.lookup_instance naming)
(Symreltab.keys instance);
- val (names_tyco, tyco') = distill_names Code_Thingol.lookup_tyco tyco;
- val (names_const, const') = distill_names Code_Thingol.lookup_const const;
+ val (names_tyco, tyco') =
+ activate_syntax (Code_Thingol.lookup_tyco naming) tyco;
+ val (names_const, (const', _)) =
+ activate_const_syntax thy literals const naming;
val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
val names2 = subtract (op =) names_hidden names1;
val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
@@ -429,7 +443,7 @@
serializer module args (labelled_name thy program2) reserved includes
(Symtab.lookup module_alias) (Symtab.lookup class')
(Symtab.lookup tyco') (Symtab.lookup const')
- naming program4 names2
+ program4 names2
end;
fun mount_serializer thy alt_serializer target module args naming program names =
@@ -460,8 +474,9 @@
((Symtab.dest o the_includes) data);
val module_alias = the_module_alias data;
val { class, instance, tyco, const } = the_name_syntax data;
+ val literals = the_literals thy target;
in
- invoke_serializer thy abortable serializer reserved
+ invoke_serializer thy abortable serializer literals reserved
includes module_alias class instance tyco const module args naming (modify program) names
end;
--- a/src/Tools/code/code_thingol.ML Wed May 06 19:15:40 2009 +0200
+++ b/src/Tools/code/code_thingol.ML Wed May 06 19:42:27 2009 +0200
@@ -20,7 +20,7 @@
datatype itype =
`%% of string * itype list
| ITyVar of vname;
- type const = string * (dict list list * itype list (*types of arguments*))
+ type const = string * ((itype list * dict list list) * itype list (*types of arguments*))
datatype iterm =
IConst of const
| IVar of vname
@@ -44,11 +44,10 @@
val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm
val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
- val unfold_const_app: iterm ->
- ((string * (dict list list * itype list)) * iterm list) option
+ val unfold_const_app: iterm -> (const * iterm list) option
val collapse_let: ((vname * itype) * iterm) * iterm
-> (iterm * itype) * (iterm * iterm) list
- val eta_expand: int -> (string * (dict list list * itype list)) * iterm list -> iterm
+ val eta_expand: int -> const * iterm list -> iterm
val contains_dictvar: iterm -> bool
val locally_monomorphic: iterm -> bool
val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
@@ -62,6 +61,7 @@
val lookup_tyco: naming -> string -> string option
val lookup_instance: naming -> class * string -> string option
val lookup_const: naming -> string -> string option
+ val ensure_declared_const: theory -> string -> naming -> string * naming
datatype stmt =
NoStmt
@@ -122,7 +122,7 @@
`%% of string * itype list
| ITyVar of vname;
-type const = string * (dict list list * itype list (*types of arguments*))
+type const = string * ((itype list * dict list list) * itype list (*types of arguments*))
datatype iterm =
IConst of const
@@ -212,7 +212,7 @@
| contains (DictVar _) = K true;
in
fold_aiterms
- (fn IConst (_, (dss, _)) => (fold o fold) contains dss | _ => I) t false
+ (fn IConst (_, ((_, dss), _)) => (fold o fold) contains dss | _ => I) t false
end;
fun locally_monomorphic (IConst _) = false
@@ -360,6 +360,11 @@
fun declare_const thy = declare thy map_const
lookup_const Symtab.update_new namify_const;
+fun ensure_declared_const thy const naming =
+ case lookup_const naming const
+ of SOME const' => (const', naming)
+ | NONE => declare_const thy const naming;
+
val unfold_fun = unfoldr
(fn "Pure.fun.tyco" `%% [ty1, ty2] => SOME (ty1, ty2)
| _ => NONE); (*depends on suffix_tyco and namify_tyco!*)
@@ -602,9 +607,10 @@
val tys_args = (fst o Term.strip_type) ty;
in
ensure_const thy algbr funcgr c
+ ##>> fold_map (translate_typ thy algbr funcgr) tys
##>> fold_map (translate_dicts thy algbr funcgr thm) (tys ~~ sorts)
##>> fold_map (translate_typ thy algbr funcgr) tys_args
- #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
+ #>> (fn (((c, tys), iss), tys_args) => IConst (c, ((tys, iss), tys_args)))
end
and translate_app_const thy algbr funcgr thm (c_ty, ts) =
translate_const thy algbr funcgr thm c_ty
--- a/src/Tools/nbe.ML Wed May 06 19:15:40 2009 +0200
+++ b/src/Tools/nbe.ML Wed May 06 19:42:27 2009 +0200
@@ -194,7 +194,7 @@
let
val (t', ts) = Code_Thingol.unfold_app t
in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
- and of_iapp match_cont (IConst (c, (dss, _))) ts = constapp c dss ts
+ and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts
| of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound v) ts
| of_iapp match_cont ((v, _) `|-> t) ts =
nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm NONE t))) ts
@@ -299,15 +299,15 @@
val params = Name.invent_list [] "d" (length names);
fun mk (k, name) =
(name, ([(v, [])],
- [([IConst (class, ([], [])) `$$ map IVar params], IVar (nth params k))]));
+ [([IConst (class, (([], []), [])) `$$ map IVar params], IVar (nth params k))]));
in map_index mk names end
| eqns_of_stmt (_, Code_Thingol.Classrel _) =
[]
| eqns_of_stmt (_, Code_Thingol.Classparam _) =
[]
| eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arities)), (superinsts, instops))) =
- [(inst, (arities, [([], IConst (class, ([], [])) `$$
- map (fn (_, (_, (inst, dicts))) => IConst (inst, (dicts, []))) superinsts
+ [(inst, (arities, [([], IConst (class, (([], []), [])) `$$
+ map (fn (_, (_, (inst, dicts))) => IConst (inst, (([], dicts), []))) superinsts
@ map (IConst o snd o fst) instops)]))];
fun compile_stmts ctxt stmts_deps =