--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Aug 10 15:28:11 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Aug 10 17:04:20 2007 +0200
@@ -7,7 +7,7 @@
begin
ML {*
-CodegenSerializer.code_width := 74;
+CodeTarget.code_width := 74;
*}
(*>*)
@@ -469,7 +469,7 @@
\item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char"},
but also offers treatment of character codes; includes
@{text "Pretty_Int"}.
- \item[@{text "Executable_Set"}] \label{exec_set} allows to generate code
+ \item[@{text "Executable_Set"}] allows to generate code
for finite sets using lists.
\item[@{text "Executable_Rat"}] implements rational
numbers.
@@ -1002,88 +1002,10 @@
in the current cache are referred to.
*}
-subsection {* Axiomatic extensions *}
-
-text {*
- \begin{warn}
- The extensions introduced in this section, though working
- in practice, are not the cream of the crop, as you
- will notice during reading. They will
- eventually be replaced by more mature approaches.
- \end{warn}
-
- Sometimes equalities are taken for granted which are
- not derivable inside the HOL logic but are silently assumed
- to hold for executable code. For example, we may want
- to identify the famous HOL constant @{const arbitrary}
- of type @{typ "'a option"} with @{const None}.
- By brute force:
-*}
-
-axiomatization where
- "arbitrary = None"
+subsection {* Code generation and proof extraction *}
text {*
- However this has to be considered harmful since this axiom,
- though probably justifiable for generated code, could
- introduce serious inconsistencies into the logic.
-
- So, there is a distinguished construct for stating axiomatic
- equalities of constants which apply only for code generation.
- Before introducing this, here is a convenient place to describe
- shortly how to deal with some restrictions the type discipline
- imposes.
-
- By itself, the constant @{const arbitrary} is a non-overloaded
- polymorphic constant. So, there is no way to distinguish
- different versions of @{const arbitrary} for different types
- inside the code generator framework. However, inlining
- theorems together with auxiliary constants provide a solution:
-*}
-
-definition
- arbitrary_option :: "'a option" where
- [symmetric, code inline]: "arbitrary_option = arbitrary"
-
-text {*
- By that, we replace any @{const arbitrary} with option type
- 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
- is a function rather than a term constructor:
-*}
-
-definition
- "None' = None"
-
-text {*
- Then finally we are enabled to use @{text "\<CODEAXIOMS>"}:
-*}
-
-code_axioms
- arbitrary_option \<equiv> None'
-
-text {*
- A dummy example:
-*}
-
-fun
- dummy_option :: "'a list \<Rightarrow> 'a option" where
- "dummy_option (x#xs) = Some x"
- | "dummy_option [] = arbitrary"
-
-code_gen dummy_option (*<*)in SML(*>*)in SML file "examples/arbitrary.ML"
-
-text {*
- \lstsml{Thy/examples/arbitrary.ML}
-
- \medskip
-
- Another axiomatic extension is code generation
- for abstracted types. For this, the
- @{text "Executable_Set"} theory (see \secref{exec_set})
- forms a good example.
+ \fixme
*}
@@ -1096,124 +1018,109 @@
description of the most important ML interfaces.
*}
-subsection {* Constants with type discipline: codegen\_consts.ML *}
+subsection {* Basics: @{text CodeUnit} *}
text {*
- This Pure module manages identification of (probably overloaded)
+ This module provides identification of (probably overloaded)
constants by unique identifiers.
*}
text %mlref {*
\begin{mldecls}
- @{index_ML_type CodegenConsts.const: "string * string option"} \\
- @{index_ML CodegenConsts.const_of_cexpr: "theory -> string * typ -> CodegenConsts.const"} \\
+ @{index_ML_type CodeUnit.const: "string * string option"} \\
+ @{index_ML CodeUnit.const_of_cexpr: "theory -> string * typ -> CodeUnit.const"} \\
\end{mldecls}
\begin{description}
- \item @{ML_type CodegenConsts.const} is the identifier type:
+ \item @{ML_type CodeUnit.const} is the identifier type:
the product of a \emph{string} with a list of \emph{typs}.
The \emph{string} is the constant name as represented inside Isabelle;
for overloaded constants, the attached \emph{string option}
is either @{text SOME} type constructor denoting an instance,
or @{text NONE} for the polymorphic constant.
- \item @{ML CodegenConsts.const_of_cexpr}~@{text thy}~@{text "(constname, typ)"}
+ \item @{ML CodeUnit.const_of_cexpr}~@{text thy}~@{text "(constname, typ)"}
maps a constant expression @{text "(constname, typ)"}
to its canonical identifier.
\end{description}
*}
-subsection {* Executable theory content: codegen\_data.ML *}
+subsection {* Executable theory content: @{text Code} *}
text {*
This Pure module implements the core notions of
executable content of a theory.
*}
-subsubsection {* Suspended theorems *}
-
-text %mlref {*
- \begin{mldecls}
- @{index_ML CodegenData.lazy_thms: "(unit -> thm list) -> thm list Susp.T"}
- \end{mldecls}
-
- \begin{description}
-
- \item @{ML CodegenData.lazy_thms}~@{text f} turns an abstract
- theorem computation @{text f} into a suspension of theorems.
-
- \end{description}
-*}
-
subsubsection {* Managing executable content *}
text %mlref {*
\begin{mldecls}
- @{index_ML CodegenData.add_func: "bool -> thm -> theory -> theory"} \\
- @{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\
- @{index_ML CodegenData.add_funcl: "CodegenConsts.const * thm list Susp.T -> theory -> theory"} \\
- @{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\
- @{index_ML CodegenData.del_inline: "thm -> theory -> theory"} \\
- @{index_ML CodegenData.add_inline_proc: "string * (theory -> cterm list -> thm list)
+ @{index_ML Code.add_func: "bool -> thm -> theory -> theory"} \\
+ @{index_ML Code.del_func: "thm -> theory -> theory"} \\
+ @{index_ML Code.add_funcl: "CodeUnit.const * thm list Susp.T -> theory -> theory"} \\
+ @{index_ML Code.add_inline: "thm -> theory -> theory"} \\
+ @{index_ML Code.del_inline: "thm -> theory -> theory"} \\
+ @{index_ML Code.add_inline_proc: "string * (theory -> cterm list -> thm list)
-> theory -> theory"} \\
- @{index_ML CodegenData.del_inline_proc: "string -> theory -> theory"} \\
- @{index_ML CodegenData.add_preproc: "string * (theory -> thm list -> thm list)
+ @{index_ML Code.del_inline_proc: "string -> theory -> theory"} \\
+ @{index_ML Code.add_preproc: "string * (theory -> thm list -> thm list)
-> theory -> theory"} \\
- @{index_ML CodegenData.del_preproc: "string -> theory -> theory"} \\
- @{index_ML CodegenData.add_datatype: "string * ((string * sort) list * (string * typ list) list)
+ @{index_ML Code.del_preproc: "string -> theory -> theory"} \\
+ @{index_ML Code.add_datatype: "string * ((string * sort) list * (string * typ list) list)
-> theory -> theory"} \\
- @{index_ML CodegenData.get_datatype: "theory -> string
+ @{index_ML Code.get_datatype: "theory -> string
-> (string * sort) list * (string * typ list) list"} \\
- @{index_ML CodegenData.get_datatype_of_constr: "theory -> CodegenConsts.const -> string option"}
+ @{index_ML Code.get_datatype_of_constr: "theory -> CodeUnit.const -> string option"}
\end{mldecls}
\begin{description}
- \item @{ML CodegenData.add_func}~@{text "thm"}~@{text "thy"} adds function
+ \item @{ML Code.add_func}~@{text "thm"}~@{text "thy"} adds function
theorem @{text "thm"} to executable content.
- \item @{ML CodegenData.del_func}~@{text "thm"}~@{text "thy"} removes function
+ \item @{ML Code.del_func}~@{text "thm"}~@{text "thy"} removes function
theorem @{text "thm"} from executable content, if present.
- \item @{ML CodegenData.add_funcl}~@{text "(const, lthms)"}~@{text "thy"} adds
+ \item @{ML Code.add_funcl}~@{text "(const, lthms)"}~@{text "thy"} adds
suspended defining equations @{text lthms} for constant
@{text const} to executable content.
- \item @{ML CodegenData.add_inline}~@{text "thm"}~@{text "thy"} adds
+ \item @{ML Code.add_inline}~@{text "thm"}~@{text "thy"} adds
inlining theorem @{text thm} to executable content.
- \item @{ML CodegenData.del_inline}~@{text "thm"}~@{text "thy"} remove
+ \item @{ML Code.del_inline}~@{text "thm"}~@{text "thy"} remove
inlining theorem @{text thm} from executable content, if present.
- \item @{ML CodegenData.add_inline_proc}~@{text "(name, f)"}~@{text "thy"} adds
+ \item @{ML Code.add_inline_proc}~@{text "(name, f)"}~@{text "thy"} adds
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 defining equations belonging
to a certain function definition.
- \item @{ML CodegenData.del_inline_proc}~@{text "name"}~@{text "thy"} removes
+ \item @{ML Code.del_inline_proc}~@{text "name"}~@{text "thy"} removes
inline procedure named @{text name} from executable content.
- \item @{ML CodegenData.add_preproc}~@{text "(name, f)"}~@{text "thy"} adds
+ \item @{ML Code.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 defining equations belonging
to a certain function definition, depending on the
current theory context.
- \item @{ML CodegenData.del_preproc}~@{text "name"}~@{text "thy"} removes
+ \item @{ML Code.del_preproc}~@{text "name"}~@{text "thy"} removes
generic preprcoessor named @{text name} from executable content.
- \item @{ML CodegenData.add_datatype}~@{text "(name, spec)"}~@{text "thy"} adds
+ \item @{ML Code.add_datatype}~@{text "(name, spec)"}~@{text "thy"} adds
a datatype to executable content, with type constructor
@{text name} and specification @{text spec}; @{text spec} is
a pair consisting of a list of type variable with sort
constraints and a list of constructors with name
and types of arguments.
- \item @{ML CodegenData.get_datatype_of_constr}~@{text "thy"}~@{text "const"}
+ \item @{ML Code.get_datatype_of_constr}~@{text "thy"}~@{text "const"}
returns type constructor corresponding to
constructor @{text const}; returns @{text NONE}
if @{text const} is no constructor.
@@ -1225,29 +1132,29 @@
text %mlref {*
\begin{mldecls}
- @{index_ML CodegenConsts.const_ord: "CodegenConsts.const * CodegenConsts.const -> order"} \\
- @{index_ML CodegenConsts.eq_const: "CodegenConsts.const * CodegenConsts.const -> bool"} \\
- @{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\
- @{index_ML_structure CodegenConsts.Consttab} \\
- @{index_ML CodegenFunc.head_func: "thm -> CodegenConsts.const * typ"} \\
- @{index_ML CodegenFunc.rewrite_func: "thm list -> thm -> thm"} \\
+ @{index_ML CodeUnit.const_ord: "CodeUnit.const * CodeUnit.const -> order"} \\
+ @{index_ML CodeUnit.eq_const: "CodeUnit.const * CodeUnit.const -> bool"} \\
+ @{index_ML CodeUnit.read_const: "theory -> string -> CodeUnit.const"} \\
+ @{index_ML_structure CodeUnit.Consttab} \\
+ @{index_ML CodeUnit.head_func: "thm -> CodeUnit.const * typ"} \\
+ @{index_ML CodeUnit.rewrite_func: "thm list -> thm -> thm"} \\
\end{mldecls}
\begin{description}
- \item @{ML CodegenConsts.const_ord},~@{ML CodegenConsts.eq_const}
+ \item @{ML CodeUnit.const_ord},~@{ML CodeUnit.eq_const}
provide order and equality on constant identifiers.
- \item @{ML_struct CodegenConsts.Consttab}
+ \item @{ML_struct CodeUnit.Consttab}
provides table structures with constant identifiers as keys.
- \item @{ML CodegenConsts.read_const}~@{text thy}~@{text s}
+ \item @{ML CodeUnit.read_const}~@{text thy}~@{text s}
reads a constant as a concrete term expression @{text s}.
- \item @{ML CodegenFunc.head_func}~@{text thm}
+ \item @{ML CodeUnit.head_func}~@{text thm}
extracts the constant and its type from a defining equation @{text thm}.
- \item @{ML CodegenFunc.rewrite_func}~@{text rews}~@{text thm}
+ \item @{ML CodeUnit.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 defining equation.
@@ -1291,7 +1198,7 @@
@{text "type T"} \\
@{text "val empty: T"} \\
@{text "val merge: Pretty.pp \<rightarrow> T * T \<rightarrow> T"} \\
- @{text "val purge: theory option \<rightarrow> CodegenConsts.const list option \<rightarrow> T \<rightarrow> T"}
+ @{text "val purge: theory option \<rightarrow> CodeUnit.const list option \<rightarrow> T \<rightarrow> T"}
\end{tabular}
\begin{description}
@@ -1344,7 +1251,7 @@
until its underlying executable content changes.
Defining equations are retrieved by instantiation
- of the functor @{ML_functor CodegenFuncgrRetrieval}
+ of the functor @{ML_functor CodeFuncgrRetrieval}
which takes two arguments:
\medskip
@@ -1361,12 +1268,12 @@
\end{description}
- An instance of @{ML_functor CodegenFuncgrRetrieval} in essence
+ An instance of @{ML_functor CodeFuncgrRetrieval} in essence
provides the following interface:
\medskip
\begin{tabular}{l}
- @{text "make: theory \<rightarrow> CodegenConsts.const list \<rightarrow> CodegenFuncgr.T"} \\
+ @{text "make: theory \<rightarrow> CodeUnit.const list \<rightarrow> CodeFuncgr.T"} \\
\end{tabular}
\begin{description}
@@ -1385,33 +1292,33 @@
text %mlref {*
\begin{mldecls}
- @{index_ML_type 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"}
+ @{index_ML_type CodeFuncgr.T} \\
+ @{index_ML CodeFuncgr.funcs: "CodeFuncgr.T -> CodeUnit.const -> thm list"} \\
+ @{index_ML CodeFuncgr.typ: "CodeFuncgr.T -> CodeUnit.const -> typ"} \\
+ @{index_ML CodeFuncgr.deps: "CodeFuncgr.T
+ -> CodeUnit.const list -> CodeUnit.const list list"} \\
+ @{index_ML CodeFuncgr.all: "CodeFuncgr.T -> CodeUnit.const list"}
\end{mldecls}
\begin{description}
- \item @{ML_type CodegenFuncgr.T} represents
+ \item @{ML_type CodeFuncgr.T} represents
a normalized defining equation system.
- \item @{ML CodegenFuncgr.funcs}~@{text funcgr}~@{text const}
+ \item @{ML CodeFuncgr.funcs}~@{text funcgr}~@{text const}
retrieves defining equiations for constant @{text const}.
- \item @{ML CodegenFuncgr.typ}~@{text funcgr}~@{text const}
+ \item @{ML CodeFuncgr.typ}~@{text funcgr}~@{text const}
retrieves function type for constant @{text const}.
- \item @{ML CodegenFuncgr.deps}~@{text funcgr}~@{text consts}
+ \item @{ML CodeFuncgr.deps}~@{text funcgr}~@{text consts}
returns the transitive closure of dependencies for
constants @{text consts} 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}
+ \item @{ML CodeFuncgr.all}~@{text funcgr}
returns all currently represented constants.
\end{description}
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Aug 10 15:28:11 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Aug 10 17:04:20 2007 +0200
@@ -590,10 +590,10 @@
\item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char},
but also offers treatment of character codes; includes
\isa{Pretty{\isacharunderscore}Int}.
- \item[\isa{Executable{\isacharunderscore}Set}] allows to generate code
+ \item[\isa{Executable{\isacharunderscore}Set}] \label{exec_set} allows to generate code
for finite sets using lists.
- \item[\isa{Executable{\isacharunderscore}Rat}] \label{exec_rat} implements rational
- numbers as triples \isa{{\isacharparenleft}sign{\isacharcomma}\ enumerator{\isacharcomma}\ denominator{\isacharparenright}}.
+ \item[\isa{Executable{\isacharunderscore}Rat}] implements rational
+ numbers.
\item[\isa{Executable{\isacharunderscore}Real}] implements a subset of real numbers,
namly those representable by rational numbers.
\item[\isa{Efficient{\isacharunderscore}Nat}] \label{eff_nat} implements natural numbers by integers,
@@ -1535,7 +1535,7 @@
Another axiomatic extension is code generation
for abstracted types. For this, the
- \isa{Executable{\isacharunderscore}Rat} theory (see \secref{exec_rat})
+ \isa{Executable{\isacharunderscore}Set} theory (see \secref{exec_set})
forms a good example.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -1552,12 +1552,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Constants with type discipline: codegen\_consts.ML%
+\isamarkupsubsection{Basics: \isa{CodeUnit}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-This Pure module manages identification of (probably overloaded)
+This module provides identification of (probably overloaded)
constants by unique identifiers.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -1570,20 +1570,20 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexmltype{CodegenConsts.const}\verb|type CodegenConsts.const = string * string option| \\
- \indexml{CodegenConsts.const-of-cexpr}\verb|CodegenConsts.const_of_cexpr: theory -> string * typ -> CodegenConsts.const| \\
+ \indexmltype{CodeUnit.const}\verb|type CodeUnit.const = string * string option| \\
+ \indexml{CodeUnit.const-of-cexpr}\verb|CodeUnit.const_of_cexpr: theory -> string * typ -> CodeUnit.const| \\
\end{mldecls}
\begin{description}
- \item \verb|CodegenConsts.const| is the identifier type:
+ \item \verb|CodeUnit.const| is the identifier type:
the product of a \emph{string} with a list of \emph{typs}.
The \emph{string} is the constant name as represented inside Isabelle;
for overloaded constants, the attached \emph{string option}
is either \isa{SOME} type constructor denoting an instance,
or \isa{NONE} for the polymorphic constant.
- \item \verb|CodegenConsts.const_of_cexpr|~\isa{thy}~\isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}}
+ \item \verb|CodeUnit.const_of_cexpr|~\isa{thy}~\isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}}
maps a constant expression \isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}}
to its canonical identifier.
@@ -1598,7 +1598,7 @@
%
\endisadelimmlref
%
-\isamarkupsubsection{Executable theory content: codegen\_data.ML%
+\isamarkupsubsection{Executable theory content: \isa{Code}%
}
\isamarkuptrue%
%
@@ -1608,37 +1608,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Suspended theorems%
-}
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexml{CodegenData.lazy-thms}\verb|CodegenData.lazy_thms: (unit -> thm list) -> thm list Susp.T|
- \end{mldecls}
-
- \begin{description}
-
- \item \verb|CodegenData.lazy_thms|~\isa{f} turns an abstract
- theorem computation \isa{f} into a suspension of theorems.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
\isamarkupsubsubsection{Managing executable content%
}
\isamarkuptrue%
@@ -1651,69 +1620,69 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexml{CodegenData.add-func}\verb|CodegenData.add_func: bool -> thm -> theory -> theory| \\
- \indexml{CodegenData.del-func}\verb|CodegenData.del_func: thm -> theory -> theory| \\
- \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: string * (theory -> cterm list -> thm list)|\isasep\isanewline%
+ \indexml{Code.add-func}\verb|Code.add_func: bool -> thm -> theory -> theory| \\
+ \indexml{Code.del-func}\verb|Code.del_func: thm -> theory -> theory| \\
+ \indexml{Code.add-funcl}\verb|Code.add_funcl: CodeUnit.const * thm list Susp.T -> theory -> theory| \\
+ \indexml{Code.add-inline}\verb|Code.add_inline: thm -> theory -> theory| \\
+ \indexml{Code.del-inline}\verb|Code.del_inline: thm -> theory -> theory| \\
+ \indexml{Code.add-inline-proc}\verb|Code.add_inline_proc: string * (theory -> cterm list -> thm list)|\isasep\isanewline%
\verb| -> theory -> theory| \\
- \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%
+ \indexml{Code.del-inline-proc}\verb|Code.del_inline_proc: string -> theory -> theory| \\
+ \indexml{Code.add-preproc}\verb|Code.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%
+ \indexml{Code.del-preproc}\verb|Code.del_preproc: string -> theory -> theory| \\
+ \indexml{Code.add-datatype}\verb|Code.add_datatype: string * ((string * sort) list * (string * typ list) list)|\isasep\isanewline%
\verb| -> theory -> theory| \\
- \indexml{CodegenData.get-datatype}\verb|CodegenData.get_datatype: theory -> string|\isasep\isanewline%
+ \indexml{Code.get-datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
\verb| -> (string * sort) list * (string * typ list) list| \\
- \indexml{CodegenData.get-datatype-of-constr}\verb|CodegenData.get_datatype_of_constr: theory -> CodegenConsts.const -> string option|
+ \indexml{Code.get-datatype-of-constr}\verb|Code.get_datatype_of_constr: theory -> CodeUnit.const -> string option|
\end{mldecls}
\begin{description}
- \item \verb|CodegenData.add_func|~\isa{thm}~\isa{thy} adds function
+ \item \verb|Code.add_func|~\isa{thm}~\isa{thy} adds function
theorem \isa{thm} to executable content.
- \item \verb|CodegenData.del_func|~\isa{thm}~\isa{thy} removes function
+ \item \verb|Code.del_func|~\isa{thm}~\isa{thy} removes function
theorem \isa{thm} from executable content, if present.
- \item \verb|CodegenData.add_funcl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds
+ \item \verb|Code.add_funcl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds
suspended defining equations \isa{lthms} for constant
\isa{const} to executable content.
- \item \verb|CodegenData.add_inline|~\isa{thm}~\isa{thy} adds
+ \item \verb|Code.add_inline|~\isa{thm}~\isa{thy} adds
inlining theorem \isa{thm} to executable content.
- \item \verb|CodegenData.del_inline|~\isa{thm}~\isa{thy} remove
+ \item \verb|Code.del_inline|~\isa{thm}~\isa{thy} remove
inlining theorem \isa{thm} from executable content, if present.
- \item \verb|CodegenData.add_inline_proc|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
+ \item \verb|Code.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 defining equations belonging
to a certain function definition.
- \item \verb|CodegenData.del_inline_proc|~\isa{name}~\isa{thy} removes
+ \item \verb|Code.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
+ \item \verb|Code.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
+ \item \verb|Code.del_preproc|~\isa{name}~\isa{thy} removes
generic preprcoessor named \isa{name} from executable content.
- \item \verb|CodegenData.add_datatype|~\isa{{\isacharparenleft}name{\isacharcomma}\ spec{\isacharparenright}}~\isa{thy} adds
+ \item \verb|Code.add_datatype|~\isa{{\isacharparenleft}name{\isacharcomma}\ spec{\isacharparenright}}~\isa{thy} adds
a datatype to executable content, with type constructor
\isa{name} and specification \isa{spec}; \isa{spec} is
a pair consisting of a list of type variable with sort
constraints and a list of constructors with name
and types of arguments.
- \item \verb|CodegenData.get_datatype_of_constr|~\isa{thy}~\isa{const}
+ \item \verb|Code.get_datatype_of_constr|~\isa{thy}~\isa{const}
returns type constructor corresponding to
constructor \isa{const}; returns \isa{NONE}
if \isa{const} is no constructor.
@@ -1741,29 +1710,29 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexml{CodegenConsts.const-ord}\verb|CodegenConsts.const_ord: CodegenConsts.const * CodegenConsts.const -> order| \\
- \indexml{CodegenConsts.eq-const}\verb|CodegenConsts.eq_const: CodegenConsts.const * CodegenConsts.const -> bool| \\
- \indexml{CodegenConsts.read-const}\verb|CodegenConsts.read_const: theory -> string -> CodegenConsts.const| \\
- \indexmlstructure{CodegenConsts.Consttab}\verb|structure CodegenConsts.Consttab| \\
- \indexml{CodegenFunc.head-func}\verb|CodegenFunc.head_func: thm -> CodegenConsts.const * typ| \\
- \indexml{CodegenFunc.rewrite-func}\verb|CodegenFunc.rewrite_func: thm list -> thm -> thm| \\
+ \indexml{CodeUnit.const-ord}\verb|CodeUnit.const_ord: CodeUnit.const * CodeUnit.const -> order| \\
+ \indexml{CodeUnit.eq-const}\verb|CodeUnit.eq_const: CodeUnit.const * CodeUnit.const -> bool| \\
+ \indexml{CodeUnit.read-const}\verb|CodeUnit.read_const: theory -> string -> CodeUnit.const| \\
+ \indexmlstructure{CodeUnit.Consttab}\verb|structure CodeUnit.Consttab| \\
+ \indexml{CodeUnit.head-func}\verb|CodeUnit.head_func: thm -> CodeUnit.const * typ| \\
+ \indexml{CodeUnit.rewrite-func}\verb|CodeUnit.rewrite_func: thm list -> thm -> thm| \\
\end{mldecls}
\begin{description}
- \item \verb|CodegenConsts.const_ord|,~\verb|CodegenConsts.eq_const|
+ \item \verb|CodeUnit.const_ord|,~\verb|CodeUnit.eq_const|
provide order and equality on constant identifiers.
- \item \verb|CodegenConsts.Consttab|
+ \item \verb|CodeUnit.Consttab|
provides table structures with constant identifiers as keys.
- \item \verb|CodegenConsts.read_const|~\isa{thy}~\isa{s}
+ \item \verb|CodeUnit.read_const|~\isa{thy}~\isa{s}
reads a constant as a concrete term expression \isa{s}.
- \item \verb|CodegenFunc.head_func|~\isa{thm}
+ \item \verb|CodeUnit.head_func|~\isa{thm}
extracts the constant and its type from a defining equation \isa{thm}.
- \item \verb|CodegenFunc.rewrite_func|~\isa{rews}~\isa{thm}
+ \item \verb|CodeUnit.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 defining equation.
@@ -1819,7 +1788,7 @@
\isa{type\ T} \\
\isa{val\ empty{\isacharcolon}\ T} \\
\isa{val\ merge{\isacharcolon}\ Pretty{\isachardot}pp\ {\isasymrightarrow}\ T\ {\isacharasterisk}\ T\ {\isasymrightarrow}\ T} \\
- \isa{val\ purge{\isacharcolon}\ theory\ option\ {\isasymrightarrow}\ CodegenConsts{\isachardot}const\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
+ \isa{val\ purge{\isacharcolon}\ theory\ option\ {\isasymrightarrow}\ CodeUnit{\isachardot}const\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
\end{tabular}
\begin{description}
@@ -1875,7 +1844,7 @@
until its underlying executable content changes.
Defining equations are retrieved by instantiation
- of the functor \verb|CodegenFuncgrRetrieval|
+ of the functor \verb|CodeFuncgrRetrieval|
which takes two arguments:
\medskip
@@ -1892,12 +1861,12 @@
\end{description}
- An instance of \verb|CodegenFuncgrRetrieval| in essence
+ An instance of \verb|CodeFuncgrRetrieval| in essence
provides the following interface:
\medskip
\begin{tabular}{l}
- \isa{make{\isacharcolon}\ theory\ {\isasymrightarrow}\ CodegenConsts{\isachardot}const\ list\ {\isasymrightarrow}\ CodegenFuncgr{\isachardot}T} \\
+ \isa{make{\isacharcolon}\ theory\ {\isasymrightarrow}\ CodeUnit{\isachardot}const\ list\ {\isasymrightarrow}\ CodeFuncgr{\isachardot}T} \\
\end{tabular}
\begin{description}
@@ -1923,33 +1892,33 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexmltype{CodegenFuncgr.T}\verb|type 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|
+ \indexmltype{CodeFuncgr.T}\verb|type CodeFuncgr.T| \\
+ \indexml{CodeFuncgr.funcs}\verb|CodeFuncgr.funcs: CodeFuncgr.T -> CodeUnit.const -> thm list| \\
+ \indexml{CodeFuncgr.typ}\verb|CodeFuncgr.typ: CodeFuncgr.T -> CodeUnit.const -> typ| \\
+ \indexml{CodeFuncgr.deps}\verb|CodeFuncgr.deps: CodeFuncgr.T|\isasep\isanewline%
+\verb| -> CodeUnit.const list -> CodeUnit.const list list| \\
+ \indexml{CodeFuncgr.all}\verb|CodeFuncgr.all: CodeFuncgr.T -> CodeUnit.const list|
\end{mldecls}
\begin{description}
- \item \verb|CodegenFuncgr.T| represents
+ \item \verb|CodeFuncgr.T| represents
a normalized defining equation system.
- \item \verb|CodegenFuncgr.funcs|~\isa{funcgr}~\isa{const}
+ \item \verb|CodeFuncgr.funcs|~\isa{funcgr}~\isa{const}
retrieves defining equiations for constant \isa{const}.
- \item \verb|CodegenFuncgr.typ|~\isa{funcgr}~\isa{const}
+ \item \verb|CodeFuncgr.typ|~\isa{funcgr}~\isa{const}
retrieves function type for constant \isa{const}.
- \item \verb|CodegenFuncgr.deps|~\isa{funcgr}~\isa{consts}
+ \item \verb|CodeFuncgr.deps|~\isa{funcgr}~\isa{consts}
returns the transitive closure of dependencies for
constants \isa{consts} 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}
+ \item \verb|CodeFuncgr.all|~\isa{funcgr}
returns all currently represented constants.
\end{description}%