# HG changeset patch # User haftmann # Date 1186758260 -7200 # Node ID 5c4913b478f5cee1ffc7536febdce12e76ce472e # Parent 2e2d81b4f1849f45c23dfaaa9354da8cbd81f66a updated diff -r 2e2d81b4f184 -r 5c4913b478f5 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- 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 "\"}: -*} - -code_axioms - arbitrary_option \ None' - -text {* - A dummy example: -*} - -fun - dummy_option :: "'a list \ '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 \ T * T \ T"} \\ - @{text "val purge: theory option \ CodegenConsts.const list option \ T \ T"} + @{text "val purge: theory option \ CodeUnit.const list option \ T \ 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 \ CodegenConsts.const list \ CodegenFuncgr.T"} \\ + @{text "make: theory \ CodeUnit.const list \ 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} diff -r 2e2d81b4f184 -r 5c4913b478f5 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- 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}%