# HG changeset patch # User haftmann # Date 1171095970 -3600 # Node ID 3b118010ec088a0e193962e6ea0049ea1ffec99c # Parent bfaba62cc92c8e47530ea1f670ebb3229843c1dd adjusted to new code generator Isar commands and changes in implementation diff -r bfaba62cc92c -r 3b118010ec08 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- 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 "\"} command: + using the @{text "\"} 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 "\"} command may prove useful: + For explorative purpose, the + @{text "\"} 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 "\"} command. + the @{text "\"} 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 {* diff -r bfaba62cc92c -r 3b118010ec08 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- 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}.