--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Oct 19 09:11:16 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Oct 19 09:11:18 2011 +0200
@@ -1956,242 +1956,6 @@
*}
-subsection {* The old code generator (S. Berghofer) *}
-
-text {* This framework generates code from both functional and
- relational programs to SML, as explained below.
-
- \begin{matharray}{rcl}
- @{command_def "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "types_code"} & : & @{text "theory \<rightarrow> theory"} \\
- @{attribute_def code} & : & @{text attribute} \\
- \end{matharray}
-
- @{rail "
- ( @@{command code_module} | @@{command code_library} ) modespec? @{syntax name}? \\
- ( @'file' name ) ? ( @'imports' ( @{syntax name} + ) ) ? \\
- @'contains' ( ( @{syntax name} '=' @{syntax term} ) + | @{syntax term} + )
- ;
-
- modespec: '(' ( @{syntax name} * ) ')'
- ;
-
- @@{command (HOL) consts_code} (codespec +)
- ;
-
- codespec: const template attachment ?
- ;
-
- @@{command (HOL) types_code} (tycodespec +)
- ;
-
- tycodespec: @{syntax name} template attachment ?
- ;
-
- const: @{syntax term}
- ;
-
- template: '(' @{syntax string} ')'
- ;
-
- attachment: 'attach' modespec? '{' @{syntax text} '}'
- ;
-
- @@{attribute code} name?
- "}
-*}
-
-
-subsubsection {* Invoking the code generator *}
-
-text {* The code generator is invoked via the @{command code_module}
- and @{command code_library} commands, which correspond to
- \emph{incremental} and \emph{modular} code generation, respectively.
-
- \begin{description}
-
- \item [Modular] For each theory, an ML structure is generated,
- containing the code generated from the constants defined in this
- theory.
-
- \item [Incremental] All the generated code is emitted into the same
- structure. This structure may import code from previously generated
- structures, which can be specified via @{keyword "imports"}.
- Moreover, the generated structure may also be referred to in later
- invocations of the code generator.
-
- \end{description}
-
- After the @{command code_module} and @{command code_library}
- keywords, the user may specify an optional list of ``modes'' in
- parentheses. These can be used to instruct the code generator to
- emit additional code for special purposes, e.g.\ functions for
- converting elements of generated datatypes to Isabelle terms, or
- test data generators. The list of modes is followed by a module
- name. The module name is optional for modular code generation, but
- must be specified for incremental code generation.
-
- The code can either be written to a file, in which case a file name
- has to be specified after the @{keyword "file"} keyword, or be loaded
- directly into Isabelle's ML environment. In the latter case, the
- @{command ML} theory command can be used to inspect the results
- interactively, for example.
-
- The terms from which to generate code can be specified after the
- @{keyword "contains"} keyword, either as a list of bindings, or just
- as a list of terms. In the latter case, the code generator just
- produces code for all constants and types occuring in the term, but
- does not bind the compiled terms to ML identifiers.
-
- Here is an example:
-*}
-
-code_module Test
-contains test = "foldl op + (0 :: int) [1, 2, 3, 4, 5]"
-
-text {* \noindent This binds the result of compiling the given term to
- the ML identifier @{ML Test.test}. *}
-
-ML {* @{assert} (Test.test = 15) *}
-
-
-subsubsection {* Configuring the code generator *}
-
-text {* When generating code for a complex term, the code generator
- recursively calls itself for all subterms. When it arrives at a
- constant, the default strategy of the code generator is to look up
- its definition and try to generate code for it. Constants which
- have no definitions that are immediately executable, may be
- associated with a piece of ML code manually using the @{command_ref
- consts_code} command. It takes a list whose elements consist of a
- constant (given in usual term syntax -- an explicit type constraint
- accounts for overloading), and a mixfix template describing the ML
- code. The latter is very much the same as the mixfix templates used
- when declaring new constants. The most notable difference is that
- terms may be included in the ML template using antiquotation
- brackets @{verbatim "{"}@{verbatim "*"}~@{text "..."}~@{verbatim
- "*"}@{verbatim "}"}.
-
- A similar mechanism is available for types: @{command_ref
- types_code} associates type constructors with specific ML code.
-
- For example, the following declarations copied from @{file
- "~~/src/HOL/Product_Type.thy"} describe how the product type of
- Isabelle/HOL should be compiled to ML. *}
-
-typedecl ('a, 'b) prod
-consts Pair :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) prod"
-
-types_code prod ("(_ */ _)")
-consts_code Pair ("(_,/ _)")
-
-text {* Sometimes, the code associated with a constant or type may
- need to refer to auxiliary functions, which have to be emitted when
- the constant is used. Code for such auxiliary functions can be
- declared using @{keyword "attach"}. For example, the @{const wfrec}
- function can be implemented as follows:
-*}
-
-consts_code wfrec ("\<module>wfrec?") (* FIXME !? *)
-attach {* fun wfrec f x = f (wfrec f) x *}
-
-text {* If the code containing a call to @{const wfrec} resides in an
- ML structure different from the one containing the function
- definition attached to @{const wfrec}, the name of the ML structure
- (followed by a ``@{text "."}'') is inserted in place of ``@{text
- "\<module>"}'' in the above template. The ``@{text "?"}'' means that
- the code generator should ignore the first argument of @{const
- wfrec}, i.e.\ the termination relation, which is usually not
- executable.
-
- \medskip Another possibility of configuring the code generator is to
- register theorems to be used for code generation. Theorems can be
- registered via the @{attribute code} attribute. It takes an optional
- name as an argument, which indicates the format of the
- theorem. Currently supported formats are equations (this is the
- default when no name is specified) and horn clauses (this is
- indicated by the name \texttt{ind}). The left-hand sides of
- equations may only contain constructors and distinct variables,
- whereas horn clauses must have the same format as introduction rules
- of inductive definitions.
-
- The following example specifies three equations from which to
- generate code for @{term "op <"} on natural numbers (see also
- @{"file" "~~/src/HOL/Nat.thy"}). *}
-
-lemma [code]: "(Suc m < Suc n) = (m < n)"
- and [code]: "((n::nat) < 0) = False"
- and [code]: "(0 < Suc n) = True" by simp_all
-
-
-subsubsection {* Specific HOL code generators *}
-
-text {* The basic code generator framework offered by Isabelle/Pure
- has already been extended with additional code generators for
- specific HOL constructs. These include datatypes, recursive
- functions and inductive relations. The code generator for inductive
- relations can handle expressions of the form @{text "(t\<^sub>1, \<dots>, t\<^sub>n) \<in>
- r"}, where @{text "r"} is an inductively defined relation. If at
- least one of the @{text "t\<^sub>i"} is a dummy pattern ``@{text "_"}'',
- the above expression evaluates to a sequence of possible answers. If
- all of the @{text "t\<^sub>i"} are proper terms, the expression evaluates
- to a boolean value.
-
- The following example demonstrates this for beta-reduction on lambda
- terms (see also @{"file" "~~/src/HOL/Proofs/Lambda/Lambda.thy"}).
-*}
-
-datatype dB =
- Var nat
- | App dB dB (infixl "\<degree>" 200)
- | Abs dB
-
-primrec lift :: "dB \<Rightarrow> nat \<Rightarrow> dB"
-where
- "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
- | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
- | "lift (Abs s) k = Abs (lift s (k + 1))"
-
-primrec subst :: "dB \<Rightarrow> dB \<Rightarrow> nat \<Rightarrow> dB" ("_[_'/_]" [300, 0, 0] 300)
-where
- "(Var i)[s/k] =
- (if k < i then Var (i - 1) else if i = k then s else Var i)"
- | "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
- | "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
-
-inductive beta :: "dB \<Rightarrow> dB \<Rightarrow> bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
-where
- beta: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
- | appL: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
- | appR: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
- | abs: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
-
-code_module Test
-contains
- test1 = "Abs (Var 0) \<degree> Var 0 \<rightarrow>\<^sub>\<beta> Var 0"
- test2 = "Abs (Abs (Var 0 \<degree> Var 0) \<degree> (Abs (Var 0) \<degree> Var 0)) \<rightarrow>\<^sub>\<beta> _"
-
-text {*
- In the above example, @{ML Test.test1} evaluates to a boolean,
- whereas @{ML Test.test2} is a lazy sequence whose elements can be
- inspected separately.
-*}
-
-ML {* @{assert} Test.test1 *}
-ML {* val results = DSeq.list_of Test.test2 *}
-ML {* @{assert} (length results = 2) *}
-
-text {*
- \medskip The theory underlying the HOL code generator is described
- more detailed in \cite{Berghofer-Nipkow:2002}. More examples that
- illustrate the usage of the code generator can be found e.g.\ in
- @{"file" "~~/src/HOL/MicroJava/J/JListExample.thy"} and @{"file"
- "~~/src/HOL/MicroJava/JVM/JVMListExample.thy"}.
-*}
-
-
section {* Definition by specification \label{sec:hol-specification} *}
text {*