--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Jan 11 16:53:12 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Jan 12 09:58:29 2007 +0100
@@ -94,12 +94,12 @@
The code generator employs a notion of executability
for three foundational executable ingredients known
from functional programming:
- \emph{function equations}, \emph{datatypes}, and
- \emph{type classes}. A function equation as a first approximation
+ \emph{defining equations}, \emph{datatypes}, and
+ \emph{type classes}. A defining equation as a first approximation
is a theorem of the form @{text "f t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n \<equiv> t"}
(an equation headed by a constant @{text f} with arguments
@{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right hand side @{text t}.
- Code generation aims to turn function equations
+ Code generation aims to turn defining equations
into a functional program by running through
a process (see figure \ref{fig:process}):
@@ -107,7 +107,7 @@
\item Out of the vast collection of theorems proven in a
\qn{theory}, a reasonable subset modeling
- function equations is \qn{selected}.
+ defining equations is \qn{selected}.
\item On those selected theorems, certain
transformations are carried out
@@ -163,7 +163,7 @@
depending on the target. In the SML case, a filename
is given where to write the generated code to.
- Internally, the function equations for all selected
+ Internally, the defining equations for all selected
constants are taken, including any transitively required
constants, datatypes and classes, resulting in the following
code:
@@ -203,7 +203,7 @@
text {*
\noindent will result in an error. Likewise, generating code
for constants not yielding
- a function equation will fail, e.g.~the Hilbert choice
+ a defining equation will fail, e.g.~the Hilbert choice
operation @{text "SOME"}:
*}
@@ -230,7 +230,7 @@
subsection {* Theorem selection *}
text {*
- The list of all function equations in a theory may be inspected
+ The list of all defining equations in a theory may be inspected
using the @{text "\<PRINTCODETHMS>"} command:
*}
@@ -238,7 +238,7 @@
text {*
\noindent which displays a table of constant with corresponding
- function equations (the additional stuff displayed
+ defining equations (the additional stuff displayed
shall not bother us for the moment). If this table does
not provide at least one function
equation, the table of primitive definitions is searched
@@ -248,7 +248,7 @@
function definitions introduced by @{text "\<FUN>"},
@{text "\<FUNCTION>"}, @{text "\<PRIMREC>"}
@{text "\<RECDEF>"} are implicitly propagated
- to this function equation table. Specific theorems may be
+ to this defining equation table. Specific theorems may be
selected using an attribute: \emph{code func}. As example,
a weight selector function:
*}
@@ -272,7 +272,7 @@
code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick1.ML")
text {*
- This theorem is now added to the function equation table:
+ This theorem is now added to the defining equation table:
\lstsml{Thy/examples/pick1.ML}
@@ -289,8 +289,8 @@
Syntactic redundancies are implicitly dropped. For example,
using a modified version of the @{const fac} function
- as function equation, the then redundant (since
- syntactically subsumed) original function equations
+ as defining equation, the then redundant (since
+ syntactically subsumed) original defining equations
are dropped, resulting in a warning:
*}
@@ -406,7 +406,7 @@
print_codethms ()
text {*
- \noindent print all cached function equations (i.e.~\emph{after}
+ \noindent print all cached defining equations (i.e.~\emph{after}
any applied transformation). Inside the brackets a
list of constants may be given; their function
equations are added to the cache if not already present.
@@ -469,8 +469,8 @@
\emph{inline procedures} and \emph{generic preprocessors}.
\emph{Inline theorems} are rewriting rules applied to each
- function equation. Due to the interpretation of theorems
- of function equations, rewrites are applied to the right
+ defining equation. Due to the interpretation of theorems
+ of defining equations, rewrites are applied to the right
hand side and the arguments of the left hand side of an
equation, but never to the constant heading the left hand side.
Inline theorems may be declared an undeclared using the
@@ -931,13 +931,13 @@
text {*
Then code generation for @{const dummy_set} will fail.
- Why? A glimpse at the function equations will offer:
+ Why? A glimpse at the defining equations will offer:
*}
print_codethms (insert)
text {*
- This reveals the function equation @{thm insert_def}
+ This reveals the defining equation @{thm insert_def}
for @{const insert}, which is operationally meaningless
but forces an equality constraint on the set members
(which is not satisfiable if the set members are functions).
@@ -965,15 +965,15 @@
text {*
\lstsml{Thy/examples/dirty_set.ML}
- Reflexive function equations by convention are dropped.
+ Reflexive defining equations by convention are dropped.
But their presence prevents primitive definitions to be
- used as function equations:
+ used as defining equations:
*}
print_codethms (insert)
text {*
- will show \emph{no} function equations for insert.
+ will show \emph{no} defining equations for insert.
Note that the sort constraints of reflexive equations
are considered; so
@@ -1058,7 +1058,7 @@
text {*
By that, we replace any @{const arbitrary} with option type
- by @{const arbitrary_option} in function equations.
+ by @{const arbitrary_option} in defining equations.
For technical reasons, we further have to provide a
synonym for @{const None} which in code generator view
@@ -1194,7 +1194,7 @@
theorem @{text "thm"} from executable content, if present.
\item @{ML CodegenData.add_funcl}~@{text "(const, lthms)"}~@{text "thy"} adds
- suspended function equations @{text lthms} for constant
+ suspended defining equations @{text lthms} for constant
@{text const} to executable content.
\item @{ML CodegenData.add_inline}~@{text "thm"}~@{text "thy"} adds
@@ -1207,7 +1207,7 @@
inline procedure @{text f} (named @{text name}) to executable content;
@{text f} is a computation of rewrite rules dependent on
the current theory context and the list of all arguments
- and right hand sides of the function equations belonging
+ and right hand sides of the defining equations belonging
to a certain function definition.
\item @{ML CodegenData.del_inline_proc}~@{text "name"}~@{text "thy"} removes
@@ -1215,11 +1215,11 @@
\item @{ML CodegenData.add_preproc}~@{text "(name, f)"}~@{text "thy"} adds
generic preprocessor @{text f} (named @{text name}) to executable content;
- @{text f} is a transformation of the function equations belonging
+ @{text f} is a transformation of the defining equations belonging
to a certain function definition, depending on the
current theory context.
- \item @{ML CodegenData.del_prepproc}~@{text "name"}~@{text "thy"} removes
+ \item @{ML CodegenData.del_preproc}~@{text "name"}~@{text "thy"} removes
generic preprcoessor named @{text name} from executable content.
\item @{ML CodegenData.add_datatype}~@{text "(name, (spec, cert))"}~@{text "thy"} adds
@@ -1242,11 +1242,11 @@
\end{description}
*}
-subsection {* Function equation systems: codegen\_funcgr.ML *}
+subsection {* defining equation systems: codegen\_funcgr.ML *}
text {*
Out of the executable content of a theory, a normalized
- function equation systems may be constructed containing
+ defining equation systems may be constructed containing
function definitions for constants. The system is cached
until its underlying executable content changes.
*}
@@ -1265,10 +1265,10 @@
\begin{description}
\item @{ML_type CodegenFuncgr.T} represents
- a normalized function equation system.
+ a normalized defining equation system.
\item @{ML CodegenFuncgr.make}~@{text thy}~@{text cs}
- returns a normalized function equation system,
+ returns a normalized defining equation system,
with the assertion that it contains any function
definition for constants @{text cs} (if existing).
@@ -1301,8 +1301,8 @@
@{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\
@{index_ML_structure CodegenConsts.Consttab} \\
@{index_ML_structure CodegenFuncgr.Constgraph} \\
- @{index_ML CodegenData.typ_func: "theory -> thm -> typ"} \\
- @{index_ML CodegenData.rewrite_func: "thm list -> thm -> thm"} \\
+ @{index_ML CodegenFunc.typ_func: "thm -> typ"} \\
+ @{index_ML CodegenFunc.rewrite_func: "thm list -> thm -> thm"} \\
\end{mldecls}
\begin{description}
@@ -1319,13 +1319,13 @@
\item @{ML CodegenConsts.read_const}~@{text thy}~@{text s}
reads a constant as a concrete term expression @{text s}.
- \item @{ML CodegenData.typ_func}~@{text thy}~@{text thm}
- extracts the type of a constant in a function equation @{text thm}.
+ \item @{ML CodegenFunc.typ_func}~@{text thm}
+ extracts the type of a constant in a defining equation @{text thm}.
- \item @{ML CodegenData.rewrite_func}~@{text rews}~@{text thm}
- rewrites a function equation @{text thm} with a set of rewrite
+ \item @{ML CodegenFunc.rewrite_func}~@{text rews}~@{text thm}
+ rewrites a defining equation @{text thm} with a set of rewrite
rules @{text rews}; only arguments and right hand side are rewritten,
- not the head of the function equation.
+ not the head of the defining equation.
\end{description}
@@ -1422,7 +1422,7 @@
Isabelle/HOL's datatype package provides a mechanism to
extend theories depending on datatype declarations:
\emph{datatype hooks}. For example, when declaring a new
- datatype, a hook proves function equations for equality on
+ datatype, a hook proves defining equations for equality on
that datatype (if possible).
*}
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Jan 11 16:53:12 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Jan 12 09:58:29 2007 +0100
@@ -121,12 +121,12 @@
The code generator employs a notion of executability
for three foundational executable ingredients known
from functional programming:
- \emph{function equations}, \emph{datatypes}, and
- \emph{type classes}. A function equation as a first approximation
+ \emph{defining equations}, \emph{datatypes}, and
+ \emph{type classes}. A defining equation as a first approximation
is a theorem of the form \isa{f\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n\ {\isasymequiv}\ t}
(an equation headed by a constant \isa{f} with arguments
\isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right hand side \isa{t}.
- Code generation aims to turn function equations
+ Code generation aims to turn defining equations
into a functional program by running through
a process (see figure \ref{fig:process}):
@@ -134,7 +134,7 @@
\item Out of the vast collection of theorems proven in a
\qn{theory}, a reasonable subset modeling
- function equations is \qn{selected}.
+ defining equations is \qn{selected}.
\item On those selected theorems, certain
transformations are carried out
@@ -194,7 +194,7 @@
depending on the target. In the SML case, a filename
is given where to write the generated code to.
- Internally, the function equations for all selected
+ Internally, the defining equations for all selected
constants are taken, including any transitively required
constants, datatypes and classes, resulting in the following
code:
@@ -246,7 +246,7 @@
\begin{isamarkuptext}%
\noindent will result in an error. Likewise, generating code
for constants not yielding
- a function equation will fail, e.g.~the Hilbert choice
+ a defining equation will fail, e.g.~the Hilbert choice
operation \isa{SOME}:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -289,7 +289,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The list of all function equations in a theory may be inspected
+The list of all defining equations in a theory may be inspected
using the \isa{{\isasymPRINTCODETHMS}} command:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -297,7 +297,7 @@
%
\begin{isamarkuptext}%
\noindent which displays a table of constant with corresponding
- function equations (the additional stuff displayed
+ defining equations (the additional stuff displayed
shall not bother us for the moment). If this table does
not provide at least one function
equation, the table of primitive definitions is searched
@@ -307,7 +307,7 @@
function definitions introduced by \isa{{\isasymFUN}},
\isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}}
\isa{{\isasymRECDEF}} are implicitly propagated
- to this function equation table. Specific theorems may be
+ to this defining equation table. Specific theorems may be
selected using an attribute: \emph{code func}. As example,
a weight selector function:%
\end{isamarkuptext}%
@@ -347,7 +347,7 @@
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
\ pick\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
\begin{isamarkuptext}%
-This theorem is now added to the function equation table:
+This theorem is now added to the defining equation table:
\lstsml{Thy/examples/pick1.ML}
@@ -365,8 +365,8 @@
Syntactic redundancies are implicitly dropped. For example,
using a modified version of the \isa{fac} function
- as function equation, the then redundant (since
- syntactically subsumed) original function equations
+ as defining equation, the then redundant (since
+ syntactically subsumed) original defining equations
are dropped, resulting in a warning:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -532,7 +532,7 @@
\isacommand{print{\isacharunderscore}codethms}\isamarkupfalse%
\ {\isacharparenleft}{\isacharparenright}%
\begin{isamarkuptext}%
-\noindent print all cached function equations (i.e.~\emph{after}
+\noindent print all cached defining equations (i.e.~\emph{after}
any applied transformation). Inside the brackets a
list of constants may be given; their function
equations are added to the cache if not already present.%
@@ -603,8 +603,8 @@
\emph{inline procedures} and \emph{generic preprocessors}.
\emph{Inline theorems} are rewriting rules applied to each
- function equation. Due to the interpretation of theorems
- of function equations, rewrites are applied to the right
+ defining equation. Due to the interpretation of theorems
+ of defining equations, rewrites are applied to the right
hand side and the arguments of the left hand side of an
equation, but never to the constant heading the left hand side.
Inline theorems may be declared an undeclared using the
@@ -1355,13 +1355,13 @@
\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}Suc{\isacharbraceright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
Then code generation for \isa{dummy{\isacharunderscore}set} will fail.
- Why? A glimpse at the function equations will offer:%
+ Why? A glimpse at the defining equations will offer:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{print{\isacharunderscore}codethms}\isamarkupfalse%
\ {\isacharparenleft}insert{\isacharparenright}%
\begin{isamarkuptext}%
-This reveals the function equation \isa{insert\ {\isacharquery}a\ {\isacharquery}B\ {\isasymequiv}\ {\isacharbraceleft}x{\isachardot}\ x\ {\isacharequal}\ {\isacharquery}a{\isacharbraceright}\ {\isasymunion}\ {\isacharquery}B}
+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
but forces an equality constraint on the set members
(which is not satisfiable if the set members are functions).
@@ -1404,15 +1404,15 @@
\begin{isamarkuptext}%
\lstsml{Thy/examples/dirty_set.ML}
- Reflexive function equations by convention are dropped.
+ Reflexive defining equations by convention are dropped.
But their presence prevents primitive definitions to be
- used as function equations:%
+ used as defining equations:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{print{\isacharunderscore}codethms}\isamarkupfalse%
\ {\isacharparenleft}insert{\isacharparenright}%
\begin{isamarkuptext}%
-will show \emph{no} function equations for insert.
+will show \emph{no} defining equations for insert.
Note that the sort constraints of reflexive equations
are considered; so%
@@ -1517,7 +1517,7 @@
\ \ {\isacharbrackleft}symmetric{\isacharcomma}\ code\ inline{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}arbitrary{\isacharunderscore}option\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}%
\begin{isamarkuptext}%
By that, we replace any \isa{arbitrary} with option type
- by \isa{arbitrary{\isacharunderscore}option} in function equations.
+ by \isa{arbitrary{\isacharunderscore}option} in defining equations.
For technical reasons, we further have to provide a
synonym for \isa{None} which in code generator view
@@ -1674,10 +1674,12 @@
\indexml{CodegenData.add-funcl}\verb|CodegenData.add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory| \\
\indexml{CodegenData.add-inline}\verb|CodegenData.add_inline: thm -> theory -> theory| \\
\indexml{CodegenData.del-inline}\verb|CodegenData.del_inline: thm -> theory -> theory| \\
- \indexml{CodegenData.add-inline-proc}\verb|CodegenData.add_inline_proc: (theory -> cterm list -> thm list)|\isasep\isanewline%
+ \indexml{CodegenData.add-inline-proc}\verb|CodegenData.add_inline_proc: string * (theory -> cterm list -> thm list)|\isasep\isanewline%
\verb| -> theory -> theory| \\
- \indexml{CodegenData.add-preproc}\verb|CodegenData.add_preproc: (theory -> thm list -> thm list)|\isasep\isanewline%
+ \indexml{CodegenData.del-inline-proc}\verb|CodegenData.del_inline_proc: string -> theory -> theory| \\
+ \indexml{CodegenData.add-preproc}\verb|CodegenData.add_preproc: string * (theory -> thm list -> thm list)|\isasep\isanewline%
\verb| -> theory -> theory| \\
+ \indexml{CodegenData.del-preproc}\verb|CodegenData.del_preproc: string -> theory -> theory| \\
\indexml{CodegenData.add-datatype}\verb|CodegenData.add_datatype: string * (((string * sort) list * (string * typ list) list)|\isasep\isanewline%
\verb| * thm list Susp.T) -> theory -> theory| \\
\indexml{CodegenData.del-datatype}\verb|CodegenData.del_datatype: string -> theory -> theory| \\
@@ -1695,7 +1697,7 @@
theorem \isa{thm} from executable content, if present.
\item \verb|CodegenData.add_funcl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds
- suspended function equations \isa{lthms} for constant
+ suspended defining equations \isa{lthms} for constant
\isa{const} to executable content.
\item \verb|CodegenData.add_inline|~\isa{thm}~\isa{thy} adds
@@ -1704,19 +1706,25 @@
\item \verb|CodegenData.del_inline|~\isa{thm}~\isa{thy} remove
inlining theorem \isa{thm} from executable content, if present.
- \item \verb|CodegenData.add_inline_proc|~\isa{f}~\isa{thy} adds
- inline procedure \isa{f} to executable content;
+ \item \verb|CodegenData.add_inline_proc|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
+ inline procedure \isa{f} (named \isa{name}) to executable content;
\isa{f} is a computation of rewrite rules dependent on
the current theory context and the list of all arguments
- and right hand sides of the function equations belonging
+ and right hand sides of the defining equations belonging
to a certain function definition.
- \item \verb|CodegenData.add_preproc|~\isa{f}~\isa{thy} adds
- generic preprocessor \isa{f} to executable content;
- \isa{f} is a transformation of the function equations belonging
+ \item \verb|CodegenData.del_inline_proc|~\isa{name}~\isa{thy} removes
+ inline procedure named \isa{name} from executable content.
+
+ \item \verb|CodegenData.add_preproc|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
+ generic preprocessor \isa{f} (named \isa{name}) to executable content;
+ \isa{f} is a transformation of the defining equations belonging
to a certain function definition, depending on the
current theory context.
+ \item \verb|CodegenData.del_preproc|~\isa{name}~\isa{thy} removes
+ generic preprcoessor named \isa{name} from executable content.
+
\item \verb|CodegenData.add_datatype|~\isa{{\isacharparenleft}name{\isacharcomma}\ {\isacharparenleft}spec{\isacharcomma}\ cert{\isacharparenright}{\isacharparenright}}~\isa{thy} adds
a datatype to executable content, with type constructor
\isa{name} and specification \isa{spec}; \isa{spec} is
@@ -1745,13 +1753,13 @@
%
\endisadelimmlref
%
-\isamarkupsubsection{Function equation systems: codegen\_funcgr.ML%
+\isamarkupsubsection{defining equation systems: codegen\_funcgr.ML%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Out of the executable content of a theory, a normalized
- function equation systems may be constructed containing
+ defining equation systems may be constructed containing
function definitions for constants. The system is cached
until its underlying executable content changes.%
\end{isamarkuptext}%
@@ -1777,10 +1785,10 @@
\begin{description}
\item \verb|CodegenFuncgr.T| represents
- a normalized function equation system.
+ a normalized defining equation system.
\item \verb|CodegenFuncgr.make|~\isa{thy}~\isa{cs}
- returns a normalized function equation system,
+ returns a normalized defining equation system,
with the assertion that it contains any function
definition for constants \isa{cs} (if existing).
@@ -1829,8 +1837,8 @@
\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{CodegenData.typ-func}\verb|CodegenData.typ_func: theory -> thm -> typ| \\
- \indexml{CodegenData.rewrite-func}\verb|CodegenData.rewrite_func: thm list -> thm -> thm| \\
+ \indexml{CodegenFunc.typ-func}\verb|CodegenFunc.typ_func: thm -> typ| \\
+ \indexml{CodegenFunc.rewrite-func}\verb|CodegenFunc.rewrite_func: thm list -> thm -> thm| \\
\end{mldecls}
\begin{description}
@@ -1847,13 +1855,13 @@
\item \verb|CodegenConsts.read_const|~\isa{thy}~\isa{s}
reads a constant as a concrete term expression \isa{s}.
- \item \verb|CodegenData.typ_func|~\isa{thy}~\isa{thm}
- extracts the type of a constant in a function equation \isa{thm}.
+ \item \verb|CodegenFunc.typ_func|~\isa{thm}
+ extracts the type of a constant in a defining equation \isa{thm}.
- \item \verb|CodegenData.rewrite_func|~\isa{rews}~\isa{thm}
- rewrites a function equation \isa{thm} with a set of rewrite
+ \item \verb|CodegenFunc.rewrite_func|~\isa{rews}~\isa{thm}
+ rewrites a defining equation \isa{thm} with a set of rewrite
rules \isa{rews}; only arguments and right hand side are rewritten,
- not the head of the function equation.
+ not the head of the defining equation.
\end{description}%
\end{isamarkuptext}%
@@ -1965,7 +1973,7 @@
Isabelle/HOL's datatype package provides a mechanism to
extend theories depending on datatype declarations:
\emph{datatype hooks}. For example, when declaring a new
- datatype, a hook proves function equations for equality on
+ datatype, a hook proves defining equations for equality on
that datatype (if possible).%
\end{isamarkuptext}%
\isamarkuptrue%