# HG changeset patch # User haftmann # Date 1232368644 -3600 # Node ID fa6c5d62adf59d2fb9d79147f84975f1256eaf1f # Parent fe9cfe076c23fcb27604da83a602d62c5ea883a2 "code equation" replaces "defining equation" diff -r fe9cfe076c23 -r fa6c5d62adf5 doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Mon Jan 19 08:16:43 2009 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Mon Jan 19 13:37:24 2009 +0100 @@ -128,7 +128,7 @@ \tikzstyle process=[ellipse, draw, thick, color = green, fill = white]; \tikzstyle process_arrow=[->, semithick, color = green]; \node (HOL) at (0, 4) [style=entity] {@{text "Isabelle/HOL"} theory}; - \node (eqn) at (2, 2) [style=entity] {defining equations}; + \node (eqn) at (2, 2) [style=entity] {code equations}; \node (iml) at (2, 0) [style=entity] {intermediate language}; \node (seri) at (1, 0) [style=process] {serialisation}; \node (SML) at (0, 3) [style=entity] {@{text SML}}; @@ -153,12 +153,12 @@ The code generator employs a notion of executability for three foundational executable ingredients known from functional programming: - \emph{defining equations}, \emph{datatypes}, and - \emph{type classes}. A defining equation as a first approximation + \emph{code equations}, \emph{datatypes}, and + \emph{type classes}. A code equation as a first approximation is a theorem of the form @{text "f t\<^isub>1 t\<^isub>2 \ t\<^isub>n \ t"} (an equation headed by a constant @{text f} with arguments @{text "t\<^isub>1 t\<^isub>2 \ t\<^isub>n"} and right hand side @{text t}). - Code generation aims to turn defining equations + Code generation aims to turn code equations into a functional program. This is achieved by three major components which operate sequentially, i.e. the result of one is the input @@ -168,7 +168,7 @@ \item Out of the vast collection of theorems proven in a \qn{theory}, a reasonable subset modelling - defining equations is \qn{selected}. + code equations is \qn{selected}. \item On those selected theorems, certain transformations are carried out @@ -177,7 +177,7 @@ specifications into equivalent but executable counterparts. The result is a structured collection of \qn{code theorems}. - \item Before the selected defining equations are continued with, + \item Before the selected code equations are continued with, they can be \qn{preprocessed}, i.e. subjected to theorem transformations. This \qn{preprocessor} is an interface which allows to apply @@ -185,12 +185,12 @@ to code generation; motivating examples are shown below, see \secref{sec:preproc}. The result of the preprocessing step is a structured collection - of defining equations. + of code equations. - \item These defining equations are \qn{translated} to a program + \item These code equations are \qn{translated} to a program in an abstract intermediate language. Think of it as a kind of \qt{Mini-Haskell} with four \qn{statements}: @{text data} - (for datatypes), @{text fun} (stemming from defining equations), + (for datatypes), @{text fun} (stemming from code equations), also @{text class} and @{text inst} (for type classes). \item Finally, the abstract program is \qn{serialised} into concrete diff -r fe9cfe076c23 -r fa6c5d62adf5 doc-src/IsarAdvanced/Codegen/Thy/ML.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/ML.thy Mon Jan 19 08:16:43 2009 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/ML.thy Mon Jan 19 13:37:24 2009 +0100 @@ -45,7 +45,7 @@ theorem @{text "thm"} from executable content, if present. \item @{ML Code.add_eqnl}~@{text "(const, lthms)"}~@{text "thy"} adds - suspended defining equations @{text lthms} for constant + suspended code equations @{text lthms} for constant @{text const} to executable content. \item @{ML Code.map_pre}~@{text "f"}~@{text "thy"} changes @@ -53,11 +53,11 @@ \item @{ML Code.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds function transformer @{text f} (named @{text name}) to executable content; - @{text f} is a transformer of the defining equations belonging + @{text f} is a transformer of the code equations belonging to a certain function definition, depending on the current theory context. Returning @{text NONE} indicates that no transformation took place; otherwise, the whole process will be iterated - with the new defining equations. + with the new code equations. \item @{ML Code.del_functrans}~@{text "name"}~@{text "thy"} removes function transformer named @{text name} from executable content. @@ -89,12 +89,12 @@ reads a constant as a concrete term expression @{text s}. \item @{ML Code_Unit.head_eqn}~@{text thy}~@{text thm} - extracts the constant and its type from a defining equation @{text thm}. + extracts the constant and its type from a code equation @{text thm}. \item @{ML Code_Unit.rewrite_eqn}~@{text ss}~@{text thm} - rewrites a defining equation @{text thm} with a simpset @{text ss}; + rewrites a code equation @{text thm} with a simpset @{text ss}; only arguments and right hand side are rewritten, - not the head of the defining equation. + not the head of the code equation. \end{description} diff -r fe9cfe076c23 -r fa6c5d62adf5 doc-src/IsarAdvanced/Codegen/Thy/Program.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Mon Jan 19 08:16:43 2009 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Mon Jan 19 13:37:24 2009 +0100 @@ -10,7 +10,7 @@ We have already seen how by default equations stemming from @{command definition}/@{command primrec}/@{command fun} statements are used for code generation. This default behaviour - can be changed, e.g. by providing different defining equations. + can be changed, e.g. by providing different code equations. All kinds of customisation shown in this section is \emph{safe} in the sense that the user does not have to worry about correctness -- all programs generatable that way are partially @@ -21,7 +21,7 @@ text {* Coming back to our introductory example, we - could provide an alternative defining equations for @{const dequeue} + could provide an alternative code equations for @{const dequeue} explicitly: *} @@ -36,7 +36,7 @@ text {* \noindent The annotation @{text "[code]"} is an @{text Isar} @{text attribute} which states that the given theorems should be - considered as defining equations for a @{text fun} statement -- + considered as code equations for a @{text fun} statement -- the corresponding constant is determined syntactically. The resulting code: *} @@ -59,13 +59,13 @@ code_thms %quote dequeue text {* - \noindent prints a table with \emph{all} defining equations + \noindent prints a table with \emph{all} code equations for @{const dequeue}, including - \emph{all} defining equations those equations depend + \emph{all} code equations those equations depend on recursively. Similarly, the @{command code_deps} command shows a graph - visualising dependencies between defining equations. + visualising dependencies between code equations. *} subsection {* @{text class} and @{text instantiation} *} @@ -155,7 +155,7 @@ The \emph{simpset} allows to employ the full generality of the Isabelle simplifier. Due to the interpretation of theorems - as defining equations, rewrites are applied to the right + as code 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. An important special case are \emph{inline theorems} which may be @@ -207,7 +207,7 @@ the @{command print_codesetup} command. @{command code_thms} provides a convenient mechanism to inspect the impact of a preprocessor setup - on defining equations. + on code equations. \begin{warn} The attribute \emph{code unfold} @@ -351,7 +351,7 @@ an explicit class @{class eq} with a corresponding operation @{const eq_class.eq} such that @{thm eq [no_vars]}. The preprocessing framework does the rest by propagating the - @{class eq} constraints through all dependent defining equations. + @{class eq} constraints through all dependent code equations. For datatypes, instances of @{class eq} are implicitly derived when possible. For other types, you may instantiate @{text eq} manually like any other type class. @@ -410,7 +410,7 @@ text %quote {*@{code_stmts "op \ \ _ \ _ \ _ \ _ \ bool" (SML)}*} text {* - In some cases, the automatically derived defining equations + In some cases, the automatically derived code equations for equality on a particular type may not be appropriate. As example, watch the following datatype representing monomorphic parametric types (where type constructors @@ -493,7 +493,7 @@ on the right hand side of its first equation the constant @{const empty_queue} occurs which is unspecified. - Normally, if constants without any defining equations occur in + Normally, if constants without any code equations occur in a program, the code generator complains (since in most cases this is not what the user expects). But such constants can also be thought of as function definitions with no equations which diff -r fe9cfe076c23 -r fa6c5d62adf5 doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex Mon Jan 19 08:16:43 2009 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex Mon Jan 19 13:37:24 2009 +0100 @@ -293,7 +293,7 @@ \tikzstyle process=[ellipse, draw, thick, color = green, fill = white]; \tikzstyle process_arrow=[->, semithick, color = green]; \node (HOL) at (0, 4) [style=entity] {\isa{Isabelle{\isacharslash}HOL} theory}; - \node (eqn) at (2, 2) [style=entity] {defining equations}; + \node (eqn) at (2, 2) [style=entity] {code equations}; \node (iml) at (2, 0) [style=entity] {intermediate language}; \node (seri) at (1, 0) [style=process] {serialisation}; \node (SML) at (0, 3) [style=entity] {\isa{SML}}; @@ -318,12 +318,12 @@ The code generator employs a notion of executability for three foundational executable ingredients known from functional programming: - \emph{defining equations}, \emph{datatypes}, and - \emph{type classes}. A defining equation as a first approximation + \emph{code equations}, \emph{datatypes}, and + \emph{type classes}. A code 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 defining equations + Code generation aims to turn code equations into a functional program. This is achieved by three major components which operate sequentially, i.e. the result of one is the input @@ -333,7 +333,7 @@ \item Out of the vast collection of theorems proven in a \qn{theory}, a reasonable subset modelling - defining equations is \qn{selected}. + code equations is \qn{selected}. \item On those selected theorems, certain transformations are carried out @@ -342,7 +342,7 @@ specifications into equivalent but executable counterparts. The result is a structured collection of \qn{code theorems}. - \item Before the selected defining equations are continued with, + \item Before the selected code equations are continued with, they can be \qn{preprocessed}, i.e. subjected to theorem transformations. This \qn{preprocessor} is an interface which allows to apply @@ -350,12 +350,12 @@ to code generation; motivating examples are shown below, see \secref{sec:preproc}. The result of the preprocessing step is a structured collection - of defining equations. + of code equations. - \item These defining equations are \qn{translated} to a program + \item These code equations are \qn{translated} to a program in an abstract intermediate language. Think of it as a kind of \qt{Mini-Haskell} with four \qn{statements}: \isa{data} - (for datatypes), \isa{fun} (stemming from defining equations), + (for datatypes), \isa{fun} (stemming from code equations), also \isa{class} and \isa{inst} (for type classes). \item Finally, the abstract program is \qn{serialised} into concrete diff -r fe9cfe076c23 -r fa6c5d62adf5 doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex Mon Jan 19 08:16:43 2009 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex Mon Jan 19 13:37:24 2009 +0100 @@ -75,7 +75,7 @@ theorem \isa{thm} from executable content, if present. \item \verb|Code.add_eqnl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds - suspended defining equations \isa{lthms} for constant + suspended code equations \isa{lthms} for constant \isa{const} to executable content. \item \verb|Code.map_pre|~\isa{f}~\isa{thy} changes @@ -83,11 +83,11 @@ \item \verb|Code.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds function transformer \isa{f} (named \isa{name}) to executable content; - \isa{f} is a transformer of the defining equations belonging + \isa{f} is a transformer of the code equations belonging to a certain function definition, depending on the current theory context. Returning \isa{NONE} indicates that no transformation took place; otherwise, the whole process will be iterated - with the new defining equations. + with the new code equations. \item \verb|Code.del_functrans|~\isa{name}~\isa{thy} removes function transformer named \isa{name} from executable content. @@ -135,12 +135,12 @@ reads a constant as a concrete term expression \isa{s}. \item \verb|Code_Unit.head_eqn|~\isa{thy}~\isa{thm} - extracts the constant and its type from a defining equation \isa{thm}. + extracts the constant and its type from a code equation \isa{thm}. \item \verb|Code_Unit.rewrite_eqn|~\isa{ss}~\isa{thm} - rewrites a defining equation \isa{thm} with a simpset \isa{ss}; + rewrites a code equation \isa{thm} with a simpset \isa{ss}; only arguments and right hand side are rewritten, - not the head of the defining equation. + not the head of the code equation. \end{description}% \end{isamarkuptext}% diff -r fe9cfe076c23 -r fa6c5d62adf5 doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Mon Jan 19 08:16:43 2009 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Mon Jan 19 13:37:24 2009 +0100 @@ -30,7 +30,7 @@ We have already seen how by default equations stemming from \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} statements are used for code generation. This default behaviour - can be changed, e.g. by providing different defining equations. + can be changed, e.g. by providing different code equations. All kinds of customisation shown in this section is \emph{safe} in the sense that the user does not have to worry about correctness -- all programs generatable that way are partially @@ -44,7 +44,7 @@ % \begin{isamarkuptext}% Coming back to our introductory example, we - could provide an alternative defining equations for \isa{dequeue} + could provide an alternative code equations for \isa{dequeue} explicitly:% \end{isamarkuptext}% \isamarkuptrue% @@ -73,7 +73,7 @@ \begin{isamarkuptext}% \noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar} \isa{attribute} which states that the given theorems should be - considered as defining equations for a \isa{fun} statement -- + considered as code equations for a \isa{fun} statement -- the corresponding constant is determined syntactically. The resulting code:% \end{isamarkuptext}% \isamarkuptrue% @@ -132,13 +132,13 @@ \endisadelimquote % \begin{isamarkuptext}% -\noindent prints a table with \emph{all} defining equations +\noindent prints a table with \emph{all} code equations for \isa{dequeue}, including - \emph{all} defining equations those equations depend + \emph{all} code equations those equations depend on recursively. Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph - visualising dependencies between defining equations.% + visualising dependencies between code equations.% \end{isamarkuptext}% \isamarkuptrue% % @@ -398,7 +398,7 @@ The \emph{simpset} allows to employ the full generality of the Isabelle simplifier. Due to the interpretation of theorems - as defining equations, rewrites are applied to the right + as code 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. An important special case are \emph{inline theorems} which may be @@ -489,7 +489,7 @@ the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command. \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient mechanism to inspect the impact of a preprocessor setup - on defining equations. + on code equations. \begin{warn} The attribute \emph{code unfold} @@ -811,7 +811,7 @@ an explicit class \isa{eq} with a corresponding operation \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}. The preprocessing framework does the rest by propagating the - \isa{eq} constraints through all dependent defining equations. + \isa{eq} constraints through all dependent code equations. For datatypes, instances of \isa{eq} are implicitly derived when possible. For other types, you may instantiate \isa{eq} manually like any other type class. @@ -951,7 +951,7 @@ \endisadelimquote % \begin{isamarkuptext}% -In some cases, the automatically derived defining equations +In some cases, the automatically derived code equations for equality on a particular type may not be appropriate. As example, watch the following datatype representing monomorphic parametric types (where type constructors @@ -1165,7 +1165,7 @@ on the right hand side of its first equation the constant \isa{empty{\isacharunderscore}queue} occurs which is unspecified. - Normally, if constants without any defining equations occur in + Normally, if constants without any code equations occur in a program, the code generator complains (since in most cases this is not what the user expects). But such constants can also be thought of as function definitions with no equations which diff -r fe9cfe076c23 -r fa6c5d62adf5 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Jan 19 08:16:43 2009 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Jan 19 13:37:24 2009 +0100 @@ -1,5 +1,3 @@ -(* $Id$ *) - theory HOL_Specific imports Main begin @@ -1163,21 +1161,21 @@ module name onto another. \item @{command (HOL) "code_abort"} declares constants which are not - required to have a definition by means of defining equations; if + required to have a definition by means of code equations; if needed these are implemented by program abort instead. \item @{attribute (HOL) code} explicitly selects (or with option - ``@{text "del"}'' deselects) a defining equation for code - generation. Usually packages introducing defining equations provide + ``@{text "del"}'' deselects) a code equation for code + generation. Usually packages introducing code equations provide a reasonable default setup for selection. \item @{attribute (HOL) code}~@{text inline} declares (or with option ``@{text "del"}'' removes) inlining theorems which are - applied as rewrite rules to any defining equation during + applied as rewrite rules to any code equation during preprocessing. \item @{command (HOL) "print_codesetup"} gives an overview on - selected defining equations, code generator datatypes and + selected code equations, code generator datatypes and preprocessor setup. \end{description} diff -r fe9cfe076c23 -r fa6c5d62adf5 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Mon Jan 19 08:16:43 2009 +0100 +++ b/doc-src/IsarRef/Thy/Spec.thy Mon Jan 19 13:37:24 2009 +0100 @@ -1,5 +1,3 @@ -(* $Id$ *) - theory Spec imports Main begin diff -r fe9cfe076c23 -r fa6c5d62adf5 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Jan 19 08:16:43 2009 +0100 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Jan 19 13:37:24 2009 +0100 @@ -3,8 +3,6 @@ \def\isabellecontext{HOL{\isacharunderscore}Specific}% % \isadelimtheory -\isanewline -\isanewline % \endisadelimtheory % @@ -1166,21 +1164,21 @@ module name onto another. \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not - required to have a definition by means of defining equations; if + required to have a definition by means of code equations; if needed these are implemented by program abort instead. \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option - ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a defining equation for code - generation. Usually packages introducing defining equations provide + ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code + generation. Usually packages introducing code equations provide a reasonable default setup for selection. \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{inline} declares (or with option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are - applied as rewrite rules to any defining equation during + applied as rewrite rules to any code equation during preprocessing. \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on - selected defining equations, code generator datatypes and + selected code equations, code generator datatypes and preprocessor setup. \end{description}% diff -r fe9cfe076c23 -r fa6c5d62adf5 doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Jan 19 08:16:43 2009 +0100 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Jan 19 13:37:24 2009 +0100 @@ -3,8 +3,6 @@ \def\isabellecontext{Spec}% % \isadelimtheory -\isanewline -\isanewline % \endisadelimtheory %