--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Sat Feb 10 09:26:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Sat Feb 10 09:26:10 2007 +0100
@@ -38,7 +38,7 @@
\qn{target language} for which code shall ultimately be
generated is not fixed but may be an arbitrary state-of-the-art
functional programming language (currently, the implementation
- supports SML \cite{web:sml} and Haskell \cite{web:haskell}).
+ supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell \cite{haskell-revised-report}).
We aim to provide a
versatile environment
suitable for software development and verification,
@@ -48,7 +48,7 @@
with maximum flexibility.
For readers, some familiarity and experience
- with the the ingredients
+ with the ingredients
of the HOL \emph{Main} theory is assumed.
*}
@@ -230,10 +230,10 @@
text {*
The list of all defining equations in a theory may be inspected
- using the @{text "\<PRINTCODETHMS>"} command:
+ using the @{text "\<PRINTCODESETUP>"} command:
*}
-print_codethms
+print_codesetup
text {*
\noindent which displays a table of constant with corresponding
@@ -303,11 +303,7 @@
\lstsml{Thy/examples/fac_case.ML}
\begin{warn}
- Some statements in this section have to be treated with some
- caution. First, since the HOL function package is still
- under development, its setup with respect to code generation
- may differ from what is presumed here.
- Further, the attributes \emph{code} and \emph{code del}
+ The attributes \emph{code} and \emph{code del}
associated with the existing code generator also apply to
the new one: \emph{code} implies \emph{code func},
and \emph{code del} implies \emph{code nofunc}.
@@ -364,7 +360,6 @@
the file system, with root given by the user.
*}
-ML {* set Toplevel.debug *}
code_gen dummy (Haskell "examples/")
(* NOTE: you may use Haskell only once in this document, otherwise
you have to work in distinct subdirectories *)
@@ -383,6 +378,16 @@
\lstsml{Thy/examples/class.ML}
*}
+text {*
+ or in OCaml:
+*}
+
+code_gen dummy (OCaml "examples/class.ocaml")
+
+text {*
+ \lstsml{Thy/examples/class.ocaml}
+*}
+
subsection {* Incremental code generation *}
text {*
@@ -399,15 +404,15 @@
is generated and cached; if no constants are given, the
current cache is serialized.
- For explorative purpose, an extended version of the
- @{text "\<CODEGEN>"} command may prove useful:
+ For explorative purpose, the
+ @{text "\<CODETHMS>"} command may prove useful:
*}
-print_codethms ()
+code_thms
text {*
\noindent print all cached defining equations (i.e.~\emph{after}
- any applied transformation). Inside the brackets a
+ any applied transformation). A
list of constants may be given; their function
equations are added to the cache if not already present.
*}
@@ -507,7 +512,7 @@
text {*
The current set of inline theorems may be inspected using
- the @{text "\<PRINTCODETHMS>"} command.
+ the @{text "\<PRINTCODESETUP>"} command.
\emph{Inline procedures} are a generalized version of inline
theorems written in ML -- rewrite rules are generated dependent
@@ -650,7 +655,7 @@
So far, we did only provide more idiomatic serializations for
constructs which would be executable on their own. Target-specific
serializations may also be used to \emph{implement} constructs
- which have no implicit notion of executability. For example,
+ which have no explicit notion of executability. For example,
take the HOL integers:
*}
@@ -940,7 +945,7 @@
Why? A glimpse at the defining equations will offer:
*}
-print_codethms (insert)
+code_thms insert
text {*
This reveals the defining equation @{thm insert_def}
@@ -976,7 +981,7 @@
used as defining equations:
*}
-print_codethms (insert)
+code_thms insert
text {*
will show \emph{no} defining equations for insert.
@@ -1168,7 +1173,7 @@
\end{description}
*}
-subsubsection {* Executable content *}
+subsubsection {* Managing executable content *}
text %mlref {*
\begin{mldecls}
@@ -1248,56 +1253,7 @@
\end{description}
*}
-subsection {* defining equation systems: codegen\_funcgr.ML *}
-
-text {*
- Out of the executable content of a theory, a normalized
- defining equation systems may be constructed containing
- function definitions for constants. The system is cached
- until its underlying executable content changes.
-*}
-
-text %mlref {*
- \begin{mldecls}
- @{index_ML_type CodegenFuncgr.T} \\
- @{index_ML CodegenFuncgr.make: "theory -> CodegenConsts.const list -> CodegenFuncgr.T"} \\
- @{index_ML CodegenFuncgr.funcs: "CodegenFuncgr.T -> CodegenConsts.const -> thm list"} \\
- @{index_ML CodegenFuncgr.typ: "CodegenFuncgr.T -> CodegenConsts.const -> typ"} \\
- @{index_ML CodegenFuncgr.deps: "CodegenFuncgr.T
- -> CodegenConsts.const list -> CodegenConsts.const list list"} \\
- @{index_ML CodegenFuncgr.all: "CodegenFuncgr.T -> CodegenConsts.const list"}
- \end{mldecls}
-
- \begin{description}
-
- \item @{ML_type CodegenFuncgr.T} represents
- a normalized defining equation system.
-
- \item @{ML CodegenFuncgr.make}~@{text thy}~@{text cs}
- returns a normalized defining equation system,
- with the assertion that it contains any function
- definition for constants @{text cs} (if existing).
-
- \item @{ML CodegenFuncgr.funcs}~@{text funcgr}~@{text c}
- retrieves function definition for constant @{text c}.
-
- \item @{ML CodegenFuncgr.typ}~@{text funcgr}~@{text c}
- retrieves function type for constant @{text c}.
-
- \item @{ML CodegenFuncgr.deps}~@{text funcgr}~@{text cs}
- returns the transitive closure of dependencies for
- constants @{text cs} as a partitioning where each partition
- corresponds to a strongly connected component of
- dependencies and any partition does \emph{not}
- depend on partitions further left.
-
- \item @{ML CodegenFuncgr.all}~@{text funcgr}
- returns all currently represented constants.
-
- \end{description}
-*}
-
-subsection {* Further auxiliary *}
+subsection {* Auxiliary *}
text %mlref {*
\begin{mldecls}
@@ -1306,7 +1262,6 @@
@{index_ML CodegenConsts.consts_of: "theory -> term -> CodegenConsts.const list"} \\
@{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\
@{index_ML_structure CodegenConsts.Consttab} \\
- @{index_ML_structure CodegenFuncgr.Constgraph} \\
@{index_ML CodegenFunc.typ_func: "thm -> typ"} \\
@{index_ML CodegenFunc.rewrite_func: "thm list -> thm -> thm"} \\
\end{mldecls}
@@ -1316,8 +1271,8 @@
\item @{ML CodegenConsts.const_ord},~@{ML CodegenConsts.eq_const}
provide order and equality on constant identifiers.
- \item @{ML_struct CodegenConsts.Consttab},~@{ML_struct CodegenFuncgr.Constgraph}
- provide advanced data structures with constant identifiers as keys.
+ \item @{ML_struct CodegenConsts.Consttab}
+ provides table structures with constant identifiers as keys.
\item @{ML CodegenConsts.consts_of}~@{text thy}~@{text t}
returns all constant identifiers mentioned in a term @{text t}.
@@ -1422,6 +1377,55 @@
\end{description}
*}
+(* subsubsection {* Building implementable systems fo defining equations *}
+
+text {*
+ Out of the executable content of a theory, a normalized
+ defining equation systems may be constructed containing
+ function definitions for constants. The system is cached
+ until its underlying executable content changes.
+*}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML_type CodegenFuncgr.T} \\
+ @{index_ML CodegenFuncgr.make: "theory -> CodegenConsts.const list -> CodegenFuncgr.T"} \\
+ @{index_ML CodegenFuncgr.funcs: "CodegenFuncgr.T -> CodegenConsts.const -> thm list"} \\
+ @{index_ML CodegenFuncgr.typ: "CodegenFuncgr.T -> CodegenConsts.const -> typ"} \\
+ @{index_ML CodegenFuncgr.deps: "CodegenFuncgr.T
+ -> CodegenConsts.const list -> CodegenConsts.const list list"} \\
+ @{index_ML CodegenFuncgr.all: "CodegenFuncgr.T -> CodegenConsts.const list"}
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML_type CodegenFuncgr.T} represents
+ a normalized defining equation system.
+
+ \item @{ML CodegenFuncgr.make}~@{text thy}~@{text cs}
+ returns a normalized defining equation system,
+ with the assertion that it contains any function
+ definition for constants @{text cs} (if existing).
+
+ \item @{ML CodegenFuncgr.funcs}~@{text funcgr}~@{text c}
+ retrieves function definition for constant @{text c}.
+
+ \item @{ML CodegenFuncgr.typ}~@{text funcgr}~@{text c}
+ retrieves function type for constant @{text c}.
+
+ \item @{ML CodegenFuncgr.deps}~@{text funcgr}~@{text cs}
+ returns the transitive closure of dependencies for
+ constants @{text cs} as a partitioning where each partition
+ corresponds to a strongly connected component of
+ dependencies and any partition does \emph{not}
+ depend on partitions further left.
+
+ \item @{ML CodegenFuncgr.all}~@{text funcgr}
+ returns all currently represented constants.
+
+ \end{description}
+*} *)
+
subsubsection {* Datatype hooks *}
text {*
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Sat Feb 10 09:26:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Sat Feb 10 09:26:10 2007 +0100
@@ -61,7 +61,7 @@
\qn{target language} for which code shall ultimately be
generated is not fixed but may be an arbitrary state-of-the-art
functional programming language (currently, the implementation
- supports SML \cite{web:sml} and Haskell \cite{web:haskell}).
+ supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell \cite{haskell-revised-report}).
We aim to provide a
versatile environment
suitable for software development and verification,
@@ -71,7 +71,7 @@
with maximum flexibility.
For readers, some familiarity and experience
- with the the ingredients
+ with the ingredients
of the HOL \emph{Main} theory is assumed.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -289,10 +289,10 @@
%
\begin{isamarkuptext}%
The list of all defining equations in a theory may be inspected
- using the \isa{{\isasymPRINTCODETHMS}} command:%
+ using the \isa{{\isasymPRINTCODESETUP}} command:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{print{\isacharunderscore}codethms}\isamarkupfalse%
+\isacommand{print{\isacharunderscore}codesetup}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent which displays a table of constant with corresponding
@@ -394,11 +394,7 @@
\lstsml{Thy/examples/fac_case.ML}
\begin{warn}
- Some statements in this section have to be treated with some
- caution. First, since the HOL function package is still
- under development, its setup with respect to code generation
- may differ from what is presumed here.
- Further, the attributes \emph{code} and \emph{code del}
+ The attributes \emph{code} and \emph{code del}
associated with the existing code generator also apply to
the new one: \emph{code} implies \emph{code func},
and \emph{code del} implies \emph{code nofunc}.
@@ -489,21 +485,6 @@
the file system, with root given by the user.%
\end{isamarkuptext}%
\isamarkuptrue%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-\isacommand{ML}\isamarkupfalse%
-\ {\isacharverbatimopen}\ set\ Toplevel{\isachardot}debug\ {\isacharverbatimclose}%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-\isanewline
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
\ dummy\ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}{\isacharparenright}%
\begin{isamarkuptext}%
@@ -521,6 +502,17 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\begin{isamarkuptext}%
+or in OCaml:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ dummy\ {\isacharparenleft}OCaml\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ocaml{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/class.ocaml}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsubsection{Incremental code generation%
}
\isamarkuptrue%
@@ -539,15 +531,15 @@
is generated and cached; if no constants are given, the
current cache is serialized.
- For explorative purpose, an extended version of the
- \isa{{\isasymCODEGEN}} command may prove useful:%
+ For explorative purpose, the
+ \isa{{\isasymCODETHMS}} command may prove useful:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{print{\isacharunderscore}codethms}\isamarkupfalse%
-\ {\isacharparenleft}{\isacharparenright}%
+\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
+%
\begin{isamarkuptext}%
\noindent print all cached defining equations (i.e.~\emph{after}
- any applied transformation). Inside the brackets a
+ any applied transformation). A
list of constants may be given; their function
equations are added to the cache if not already present.%
\end{isamarkuptext}%
@@ -687,7 +679,7 @@
%
\begin{isamarkuptext}%
The current set of inline theorems may be inspected using
- the \isa{{\isasymPRINTCODETHMS}} command.
+ the \isa{{\isasymPRINTCODESETUP}} command.
\emph{Inline procedures} are a generalized version of inline
theorems written in ML -- rewrite rules are generated dependent
@@ -872,7 +864,7 @@
So far, we did only provide more idiomatic serializations for
constructs which would be executable on their own. Target-specific
serializations may also be used to \emph{implement} constructs
- which have no implicit notion of executability. For example,
+ which have no explicit notion of executability. For example,
take the HOL integers:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -1378,8 +1370,8 @@
Why? A glimpse at the defining equations will offer:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{print{\isacharunderscore}codethms}\isamarkupfalse%
-\ {\isacharparenleft}insert{\isacharparenright}%
+\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
+\ insert%
\begin{isamarkuptext}%
This reveals the defining equation \isa{insert\ {\isacharquery}a\ {\isacharquery}B\ {\isasymequiv}\ {\isacharbraceleft}x{\isachardot}\ x\ {\isacharequal}\ {\isacharquery}a{\isacharbraceright}\ {\isasymunion}\ {\isacharquery}B}
for \isa{insert}, which is operationally meaningless
@@ -1429,8 +1421,8 @@
used as defining equations:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{print{\isacharunderscore}codethms}\isamarkupfalse%
-\ {\isacharparenleft}insert{\isacharparenright}%
+\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
+\ insert%
\begin{isamarkuptext}%
will show \emph{no} defining equations for insert.
@@ -1677,7 +1669,7 @@
%
\endisadelimmlref
%
-\isamarkupsubsubsection{Executable content%
+\isamarkupsubsubsection{Managing executable content%
}
\isamarkuptrue%
%
@@ -1773,73 +1765,7 @@
%
\endisadelimmlref
%
-\isamarkupsubsection{defining equation systems: codegen\_funcgr.ML%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Out of the executable content of a theory, a normalized
- defining equation systems may be constructed containing
- function definitions for constants. The system is cached
- until its underlying executable content changes.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexmltype{CodegenFuncgr.T}\verb|type CodegenFuncgr.T| \\
- \indexml{CodegenFuncgr.make}\verb|CodegenFuncgr.make: theory -> CodegenConsts.const list -> CodegenFuncgr.T| \\
- \indexml{CodegenFuncgr.funcs}\verb|CodegenFuncgr.funcs: CodegenFuncgr.T -> CodegenConsts.const -> thm list| \\
- \indexml{CodegenFuncgr.typ}\verb|CodegenFuncgr.typ: CodegenFuncgr.T -> CodegenConsts.const -> typ| \\
- \indexml{CodegenFuncgr.deps}\verb|CodegenFuncgr.deps: CodegenFuncgr.T|\isasep\isanewline%
-\verb| -> CodegenConsts.const list -> CodegenConsts.const list list| \\
- \indexml{CodegenFuncgr.all}\verb|CodegenFuncgr.all: CodegenFuncgr.T -> CodegenConsts.const list|
- \end{mldecls}
-
- \begin{description}
-
- \item \verb|CodegenFuncgr.T| represents
- a normalized defining equation system.
-
- \item \verb|CodegenFuncgr.make|~\isa{thy}~\isa{cs}
- returns a normalized defining equation system,
- with the assertion that it contains any function
- definition for constants \isa{cs} (if existing).
-
- \item \verb|CodegenFuncgr.funcs|~\isa{funcgr}~\isa{c}
- retrieves function definition for constant \isa{c}.
-
- \item \verb|CodegenFuncgr.typ|~\isa{funcgr}~\isa{c}
- retrieves function type for constant \isa{c}.
-
- \item \verb|CodegenFuncgr.deps|~\isa{funcgr}~\isa{cs}
- returns the transitive closure of dependencies for
- constants \isa{cs} as a partitioning where each partition
- corresponds to a strongly connected component of
- dependencies and any partition does \emph{not}
- depend on partitions further left.
-
- \item \verb|CodegenFuncgr.all|~\isa{funcgr}
- returns all currently represented constants.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isamarkupsubsection{Further auxiliary%
+\isamarkupsubsection{Auxiliary%
}
\isamarkuptrue%
%
@@ -1856,7 +1782,6 @@
\indexml{CodegenConsts.consts-of}\verb|CodegenConsts.consts_of: theory -> term -> CodegenConsts.const list| \\
\indexml{CodegenConsts.read-const}\verb|CodegenConsts.read_const: theory -> string -> CodegenConsts.const| \\
\indexmlstructure{CodegenConsts.Consttab}\verb|structure CodegenConsts.Consttab| \\
- \indexmlstructure{CodegenFuncgr.Constgraph}\verb|structure CodegenFuncgr.Constgraph| \\
\indexml{CodegenFunc.typ-func}\verb|CodegenFunc.typ_func: thm -> typ| \\
\indexml{CodegenFunc.rewrite-func}\verb|CodegenFunc.rewrite_func: thm list -> thm -> thm| \\
\end{mldecls}
@@ -1866,8 +1791,8 @@
\item \verb|CodegenConsts.const_ord|,~\verb|CodegenConsts.eq_const|
provide order and equality on constant identifiers.
- \item \verb|CodegenConsts.Consttab|,~\verb|CodegenFuncgr.Constgraph|
- provide advanced data structures with constant identifiers as keys.
+ \item \verb|CodegenConsts.Consttab|
+ provides table structures with constant identifiers as keys.
\item \verb|CodegenConsts.consts_of|~\isa{thy}~\isa{t}
returns all constant identifiers mentioned in a term \isa{t}.