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}