updated
authorhaftmann
Fri Aug 10 17:04:20 2007 +0200 (2007-08-10)
changeset 242175c4913b478f5
parent 24216 2e2d81b4f184
child 24218 fbf1646b267c
updated
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Aug 10 15:28:11 2007 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Aug 10 17:04:20 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  begin
     1.5  
     1.6  ML {*
     1.7 -CodegenSerializer.code_width := 74;
     1.8 +CodeTarget.code_width := 74;
     1.9  *}
    1.10  
    1.11  (*>*)
    1.12 @@ -469,7 +469,7 @@
    1.13      \item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char"},
    1.14         but also offers treatment of character codes; includes
    1.15         @{text "Pretty_Int"}.
    1.16 -    \item[@{text "Executable_Set"}] \label{exec_set} allows to generate code
    1.17 +    \item[@{text "Executable_Set"}] allows to generate code
    1.18         for finite sets using lists.
    1.19      \item[@{text "Executable_Rat"}] implements rational
    1.20         numbers.
    1.21 @@ -1002,88 +1002,10 @@
    1.22    in the current cache are referred to.
    1.23  *}
    1.24  
    1.25 -subsection {* Axiomatic extensions *}
    1.26 -
    1.27 -text {*
    1.28 -  \begin{warn}
    1.29 -    The extensions introduced in this section, though working
    1.30 -    in practice, are not the cream of the crop, as you
    1.31 -    will notice during reading.  They will
    1.32 -    eventually be replaced by more mature approaches.
    1.33 -  \end{warn}
    1.34 -
    1.35 -  Sometimes equalities are taken for granted which are
    1.36 -  not derivable inside the HOL logic but are silently assumed
    1.37 -  to hold for executable code.  For example, we may want
    1.38 -  to identify the famous HOL constant @{const arbitrary}
    1.39 -  of type @{typ "'a option"} with @{const None}.
    1.40 -  By brute force:
    1.41 -*}
    1.42 -
    1.43 -axiomatization where
    1.44 -  "arbitrary = None"
    1.45 +subsection {* Code generation and proof extraction *}
    1.46  
    1.47  text {*
    1.48 -  However this has to be considered harmful since this axiom,
    1.49 -  though probably justifiable for generated code, could
    1.50 -  introduce serious inconsistencies into the logic.
    1.51 -
    1.52 -  So, there is a distinguished construct for stating axiomatic
    1.53 -  equalities of constants which apply only for code generation.
    1.54 -  Before introducing this, here is a convenient place to describe
    1.55 -  shortly how to deal with some restrictions the type discipline
    1.56 -  imposes.
    1.57 -
    1.58 -  By itself, the constant @{const arbitrary} is a non-overloaded
    1.59 -  polymorphic constant.  So, there is no way to distinguish
    1.60 -  different versions of @{const arbitrary} for different types
    1.61 -  inside the code generator framework.  However, inlining
    1.62 -  theorems together with auxiliary constants provide a solution:
    1.63 -*}
    1.64 -
    1.65 -definition
    1.66 -  arbitrary_option :: "'a option" where
    1.67 -  [symmetric, code inline]: "arbitrary_option = arbitrary"
    1.68 -
    1.69 -text {*
    1.70 -  By that, we replace any @{const arbitrary} with option type
    1.71 -  by @{const arbitrary_option} in defining equations.
    1.72 -
    1.73 -  For technical reasons, we further have to provide a
    1.74 -  synonym for @{const None} which in code generator view
    1.75 -  is a function rather than a term constructor:
    1.76 -*}
    1.77 -
    1.78 -definition
    1.79 -  "None' = None"
    1.80 -
    1.81 -text {*
    1.82 -  Then finally we are enabled to use @{text "\<CODEAXIOMS>"}:
    1.83 -*}
    1.84 -
    1.85 -code_axioms
    1.86 -  arbitrary_option \<equiv> None'
    1.87 -
    1.88 -text {*
    1.89 -  A dummy example:
    1.90 -*}
    1.91 -
    1.92 -fun
    1.93 -  dummy_option :: "'a list \<Rightarrow> 'a option" where
    1.94 -    "dummy_option (x#xs) = Some x"
    1.95 -  | "dummy_option [] = arbitrary"
    1.96 -
    1.97 -code_gen dummy_option (*<*)in SML(*>*)in SML file "examples/arbitrary.ML"
    1.98 -
    1.99 -text {*
   1.100 -  \lstsml{Thy/examples/arbitrary.ML}
   1.101 -
   1.102 -  \medskip
   1.103 -
   1.104 -  Another axiomatic extension is code generation
   1.105 -  for abstracted types.  For this, the  
   1.106 -  @{text "Executable_Set"} theory (see \secref{exec_set})
   1.107 -  forms a good example.
   1.108 +  \fixme
   1.109  *}
   1.110  
   1.111  
   1.112 @@ -1096,124 +1018,109 @@
   1.113    description of the most important ML interfaces.
   1.114  *}
   1.115  
   1.116 -subsection {* Constants with type discipline: codegen\_consts.ML *}
   1.117 +subsection {* Basics: @{text CodeUnit} *}
   1.118  
   1.119  text {*
   1.120 -  This Pure module manages identification of (probably overloaded)
   1.121 +  This module provides identification of (probably overloaded)
   1.122    constants by unique identifiers.
   1.123  *}
   1.124  
   1.125  text %mlref {*
   1.126    \begin{mldecls}
   1.127 -  @{index_ML_type CodegenConsts.const: "string * string option"} \\
   1.128 -  @{index_ML CodegenConsts.const_of_cexpr: "theory -> string * typ -> CodegenConsts.const"} \\
   1.129 +  @{index_ML_type CodeUnit.const: "string * string option"} \\
   1.130 +  @{index_ML CodeUnit.const_of_cexpr: "theory -> string * typ -> CodeUnit.const"} \\
   1.131   \end{mldecls}
   1.132  
   1.133    \begin{description}
   1.134  
   1.135 -  \item @{ML_type CodegenConsts.const} is the identifier type:
   1.136 +  \item @{ML_type CodeUnit.const} is the identifier type:
   1.137       the product of a \emph{string} with a list of \emph{typs}.
   1.138       The \emph{string} is the constant name as represented inside Isabelle;
   1.139       for overloaded constants, the attached \emph{string option}
   1.140       is either @{text SOME} type constructor denoting an instance,
   1.141       or @{text NONE} for the polymorphic constant.
   1.142  
   1.143 -  \item @{ML CodegenConsts.const_of_cexpr}~@{text thy}~@{text "(constname, typ)"}
   1.144 +  \item @{ML CodeUnit.const_of_cexpr}~@{text thy}~@{text "(constname, typ)"}
   1.145       maps a constant expression @{text "(constname, typ)"}
   1.146       to its canonical identifier.
   1.147  
   1.148    \end{description}
   1.149  *}
   1.150  
   1.151 -subsection {* Executable theory content: codegen\_data.ML *}
   1.152 +subsection {* Executable theory content: @{text Code} *}
   1.153  
   1.154  text {*
   1.155    This Pure module implements the core notions of
   1.156    executable content of a theory.
   1.157  *}
   1.158  
   1.159 -subsubsection {* Suspended theorems *}
   1.160 -
   1.161 -text %mlref {*
   1.162 -  \begin{mldecls}
   1.163 -  @{index_ML CodegenData.lazy_thms: "(unit -> thm list) -> thm list Susp.T"}
   1.164 -  \end{mldecls}
   1.165 -
   1.166 -  \begin{description}
   1.167 -
   1.168 -  \item @{ML CodegenData.lazy_thms}~@{text f} turns an abstract
   1.169 -     theorem computation @{text f} into a suspension of theorems.
   1.170 -
   1.171 -  \end{description}
   1.172 -*}
   1.173 -
   1.174  subsubsection {* Managing executable content *}
   1.175  
   1.176  text %mlref {*
   1.177    \begin{mldecls}
   1.178 -  @{index_ML CodegenData.add_func: "bool -> thm -> theory -> theory"} \\
   1.179 -  @{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\
   1.180 -  @{index_ML CodegenData.add_funcl: "CodegenConsts.const * thm list Susp.T -> theory -> theory"} \\
   1.181 -  @{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\
   1.182 -  @{index_ML CodegenData.del_inline: "thm -> theory -> theory"} \\
   1.183 -  @{index_ML CodegenData.add_inline_proc: "string * (theory -> cterm list -> thm list)
   1.184 +  @{index_ML Code.add_func: "bool -> thm -> theory -> theory"} \\
   1.185 +  @{index_ML Code.del_func: "thm -> theory -> theory"} \\
   1.186 +  @{index_ML Code.add_funcl: "CodeUnit.const * thm list Susp.T -> theory -> theory"} \\
   1.187 +  @{index_ML Code.add_inline: "thm -> theory -> theory"} \\
   1.188 +  @{index_ML Code.del_inline: "thm -> theory -> theory"} \\
   1.189 +  @{index_ML Code.add_inline_proc: "string * (theory -> cterm list -> thm list)
   1.190      -> theory -> theory"} \\
   1.191 -  @{index_ML CodegenData.del_inline_proc: "string -> theory -> theory"} \\
   1.192 -  @{index_ML CodegenData.add_preproc: "string * (theory -> thm list -> thm list)
   1.193 +  @{index_ML Code.del_inline_proc: "string -> theory -> theory"} \\
   1.194 +  @{index_ML Code.add_preproc: "string * (theory -> thm list -> thm list)
   1.195      -> theory -> theory"} \\
   1.196 -  @{index_ML CodegenData.del_preproc: "string -> theory -> theory"} \\
   1.197 -  @{index_ML CodegenData.add_datatype: "string * ((string * sort) list * (string * typ list) list)
   1.198 +  @{index_ML Code.del_preproc: "string -> theory -> theory"} \\
   1.199 +  @{index_ML Code.add_datatype: "string * ((string * sort) list * (string * typ list) list)
   1.200      -> theory -> theory"} \\
   1.201 -  @{index_ML CodegenData.get_datatype: "theory -> string
   1.202 +  @{index_ML Code.get_datatype: "theory -> string
   1.203      -> (string * sort) list * (string * typ list) list"} \\
   1.204 -  @{index_ML CodegenData.get_datatype_of_constr: "theory -> CodegenConsts.const -> string option"}
   1.205 +  @{index_ML Code.get_datatype_of_constr: "theory -> CodeUnit.const -> string option"}
   1.206    \end{mldecls}
   1.207  
   1.208    \begin{description}
   1.209  
   1.210 -  \item @{ML CodegenData.add_func}~@{text "thm"}~@{text "thy"} adds function
   1.211 +  \item @{ML Code.add_func}~@{text "thm"}~@{text "thy"} adds function
   1.212       theorem @{text "thm"} to executable content.
   1.213  
   1.214 -  \item @{ML CodegenData.del_func}~@{text "thm"}~@{text "thy"} removes function
   1.215 +  \item @{ML Code.del_func}~@{text "thm"}~@{text "thy"} removes function
   1.216       theorem @{text "thm"} from executable content, if present.
   1.217  
   1.218 -  \item @{ML CodegenData.add_funcl}~@{text "(const, lthms)"}~@{text "thy"} adds
   1.219 +  \item @{ML Code.add_funcl}~@{text "(const, lthms)"}~@{text "thy"} adds
   1.220       suspended defining equations @{text lthms} for constant
   1.221       @{text const} to executable content.
   1.222  
   1.223 -  \item @{ML CodegenData.add_inline}~@{text "thm"}~@{text "thy"} adds
   1.224 +  \item @{ML Code.add_inline}~@{text "thm"}~@{text "thy"} adds
   1.225       inlining theorem @{text thm} to executable content.
   1.226  
   1.227 -  \item @{ML CodegenData.del_inline}~@{text "thm"}~@{text "thy"} remove
   1.228 +  \item @{ML Code.del_inline}~@{text "thm"}~@{text "thy"} remove
   1.229       inlining theorem @{text thm} from executable content, if present.
   1.230  
   1.231 -  \item @{ML CodegenData.add_inline_proc}~@{text "(name, f)"}~@{text "thy"} adds
   1.232 +  \item @{ML Code.add_inline_proc}~@{text "(name, f)"}~@{text "thy"} adds
   1.233       inline procedure @{text f} (named @{text name}) to executable content;
   1.234       @{text f} is a computation of rewrite rules dependent on
   1.235       the current theory context and the list of all arguments
   1.236       and right hand sides of the defining equations belonging
   1.237       to a certain function definition.
   1.238  
   1.239 -  \item @{ML CodegenData.del_inline_proc}~@{text "name"}~@{text "thy"} removes
   1.240 +  \item @{ML Code.del_inline_proc}~@{text "name"}~@{text "thy"} removes
   1.241       inline procedure named @{text name} from executable content.
   1.242  
   1.243 -  \item @{ML CodegenData.add_preproc}~@{text "(name, f)"}~@{text "thy"} adds
   1.244 +  \item @{ML Code.add_preproc}~@{text "(name, f)"}~@{text "thy"} adds
   1.245       generic preprocessor @{text f} (named @{text name}) to executable content;
   1.246       @{text f} is a transformation of the defining equations belonging
   1.247       to a certain function definition, depending on the
   1.248       current theory context.
   1.249  
   1.250 -  \item @{ML CodegenData.del_preproc}~@{text "name"}~@{text "thy"} removes
   1.251 +  \item @{ML Code.del_preproc}~@{text "name"}~@{text "thy"} removes
   1.252       generic preprcoessor named @{text name} from executable content.
   1.253  
   1.254 -  \item @{ML CodegenData.add_datatype}~@{text "(name, spec)"}~@{text "thy"} adds
   1.255 +  \item @{ML Code.add_datatype}~@{text "(name, spec)"}~@{text "thy"} adds
   1.256       a datatype to executable content, with type constructor
   1.257       @{text name} and specification @{text spec}; @{text spec} is
   1.258       a pair consisting of a list of type variable with sort
   1.259       constraints and a list of constructors with name
   1.260       and types of arguments.
   1.261  
   1.262 -  \item @{ML CodegenData.get_datatype_of_constr}~@{text "thy"}~@{text "const"}
   1.263 +  \item @{ML Code.get_datatype_of_constr}~@{text "thy"}~@{text "const"}
   1.264       returns type constructor corresponding to
   1.265       constructor @{text const}; returns @{text NONE}
   1.266       if @{text const} is no constructor.
   1.267 @@ -1225,29 +1132,29 @@
   1.268  
   1.269  text %mlref {*
   1.270    \begin{mldecls}
   1.271 -  @{index_ML CodegenConsts.const_ord: "CodegenConsts.const * CodegenConsts.const -> order"} \\
   1.272 -  @{index_ML CodegenConsts.eq_const: "CodegenConsts.const * CodegenConsts.const -> bool"} \\
   1.273 -  @{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\
   1.274 -  @{index_ML_structure CodegenConsts.Consttab} \\
   1.275 -  @{index_ML CodegenFunc.head_func: "thm -> CodegenConsts.const * typ"} \\
   1.276 -  @{index_ML CodegenFunc.rewrite_func: "thm list -> thm -> thm"} \\
   1.277 +  @{index_ML CodeUnit.const_ord: "CodeUnit.const * CodeUnit.const -> order"} \\
   1.278 +  @{index_ML CodeUnit.eq_const: "CodeUnit.const * CodeUnit.const -> bool"} \\
   1.279 +  @{index_ML CodeUnit.read_const: "theory -> string -> CodeUnit.const"} \\
   1.280 +  @{index_ML_structure CodeUnit.Consttab} \\
   1.281 +  @{index_ML CodeUnit.head_func: "thm -> CodeUnit.const * typ"} \\
   1.282 +  @{index_ML CodeUnit.rewrite_func: "thm list -> thm -> thm"} \\
   1.283    \end{mldecls}
   1.284  
   1.285    \begin{description}
   1.286  
   1.287 -  \item @{ML CodegenConsts.const_ord},~@{ML CodegenConsts.eq_const}
   1.288 +  \item @{ML CodeUnit.const_ord},~@{ML CodeUnit.eq_const}
   1.289       provide order and equality on constant identifiers.
   1.290  
   1.291 -  \item @{ML_struct CodegenConsts.Consttab}
   1.292 +  \item @{ML_struct CodeUnit.Consttab}
   1.293       provides table structures with constant identifiers as keys.
   1.294  
   1.295 -  \item @{ML CodegenConsts.read_const}~@{text thy}~@{text s}
   1.296 +  \item @{ML CodeUnit.read_const}~@{text thy}~@{text s}
   1.297       reads a constant as a concrete term expression @{text s}.
   1.298  
   1.299 -  \item @{ML CodegenFunc.head_func}~@{text thm}
   1.300 +  \item @{ML CodeUnit.head_func}~@{text thm}
   1.301       extracts the constant and its type from a defining equation @{text thm}.
   1.302  
   1.303 -  \item @{ML CodegenFunc.rewrite_func}~@{text rews}~@{text thm}
   1.304 +  \item @{ML CodeUnit.rewrite_func}~@{text rews}~@{text thm}
   1.305       rewrites a defining equation @{text thm} with a set of rewrite
   1.306       rules @{text rews}; only arguments and right hand side are rewritten,
   1.307       not the head of the defining equation.
   1.308 @@ -1291,7 +1198,7 @@
   1.309    @{text "type T"} \\
   1.310    @{text "val empty: T"} \\
   1.311    @{text "val merge: Pretty.pp \<rightarrow> T * T \<rightarrow> T"} \\
   1.312 -  @{text "val purge: theory option \<rightarrow> CodegenConsts.const list option \<rightarrow> T \<rightarrow> T"}
   1.313 +  @{text "val purge: theory option \<rightarrow> CodeUnit.const list option \<rightarrow> T \<rightarrow> T"}
   1.314    \end{tabular}
   1.315  
   1.316    \begin{description}
   1.317 @@ -1344,7 +1251,7 @@
   1.318    until its underlying executable content changes.
   1.319  
   1.320    Defining equations are retrieved by instantiation
   1.321 -  of the functor @{ML_functor CodegenFuncgrRetrieval}
   1.322 +  of the functor @{ML_functor CodeFuncgrRetrieval}
   1.323    which takes two arguments:
   1.324  
   1.325    \medskip
   1.326 @@ -1361,12 +1268,12 @@
   1.327  
   1.328    \end{description}
   1.329  
   1.330 -  An instance of @{ML_functor CodegenFuncgrRetrieval} in essence
   1.331 +  An instance of @{ML_functor CodeFuncgrRetrieval} in essence
   1.332    provides the following interface:
   1.333  
   1.334    \medskip
   1.335    \begin{tabular}{l}
   1.336 -  @{text "make: theory \<rightarrow> CodegenConsts.const list \<rightarrow> CodegenFuncgr.T"} \\
   1.337 +  @{text "make: theory \<rightarrow> CodeUnit.const list \<rightarrow> CodeFuncgr.T"} \\
   1.338    \end{tabular}
   1.339  
   1.340    \begin{description}
   1.341 @@ -1385,33 +1292,33 @@
   1.342  
   1.343  text %mlref {*
   1.344    \begin{mldecls}
   1.345 -  @{index_ML_type CodegenFuncgr.T} \\
   1.346 -  @{index_ML CodegenFuncgr.funcs: "CodegenFuncgr.T -> CodegenConsts.const -> thm list"} \\
   1.347 -  @{index_ML CodegenFuncgr.typ: "CodegenFuncgr.T -> CodegenConsts.const -> typ"} \\
   1.348 -  @{index_ML CodegenFuncgr.deps: "CodegenFuncgr.T
   1.349 -    -> CodegenConsts.const list -> CodegenConsts.const list list"} \\
   1.350 -  @{index_ML CodegenFuncgr.all: "CodegenFuncgr.T -> CodegenConsts.const list"}
   1.351 +  @{index_ML_type CodeFuncgr.T} \\
   1.352 +  @{index_ML CodeFuncgr.funcs: "CodeFuncgr.T -> CodeUnit.const -> thm list"} \\
   1.353 +  @{index_ML CodeFuncgr.typ: "CodeFuncgr.T -> CodeUnit.const -> typ"} \\
   1.354 +  @{index_ML CodeFuncgr.deps: "CodeFuncgr.T
   1.355 +    -> CodeUnit.const list -> CodeUnit.const list list"} \\
   1.356 +  @{index_ML CodeFuncgr.all: "CodeFuncgr.T -> CodeUnit.const list"}
   1.357    \end{mldecls}
   1.358  
   1.359    \begin{description}
   1.360  
   1.361 -  \item @{ML_type CodegenFuncgr.T} represents
   1.362 +  \item @{ML_type CodeFuncgr.T} represents
   1.363      a normalized defining equation system.
   1.364  
   1.365 -  \item @{ML CodegenFuncgr.funcs}~@{text funcgr}~@{text const}
   1.366 +  \item @{ML CodeFuncgr.funcs}~@{text funcgr}~@{text const}
   1.367      retrieves defining equiations for constant @{text const}.
   1.368  
   1.369 -  \item @{ML CodegenFuncgr.typ}~@{text funcgr}~@{text const}
   1.370 +  \item @{ML CodeFuncgr.typ}~@{text funcgr}~@{text const}
   1.371      retrieves function type for constant @{text const}.
   1.372  
   1.373 -  \item @{ML CodegenFuncgr.deps}~@{text funcgr}~@{text consts}
   1.374 +  \item @{ML CodeFuncgr.deps}~@{text funcgr}~@{text consts}
   1.375      returns the transitive closure of dependencies for
   1.376      constants @{text consts} as a partitioning where each partition
   1.377      corresponds to a strongly connected component of
   1.378      dependencies and any partition does \emph{not}
   1.379      depend on partitions further left.
   1.380  
   1.381 -  \item @{ML CodegenFuncgr.all}~@{text funcgr}
   1.382 +  \item @{ML CodeFuncgr.all}~@{text funcgr}
   1.383      returns all currently represented constants.
   1.384  
   1.385    \end{description}
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Fri Aug 10 15:28:11 2007 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Fri Aug 10 17:04:20 2007 +0200
     2.3 @@ -590,10 +590,10 @@
     2.4      \item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char},
     2.5         but also offers treatment of character codes; includes
     2.6         \isa{Pretty{\isacharunderscore}Int}.
     2.7 -    \item[\isa{Executable{\isacharunderscore}Set}] allows to generate code
     2.8 +    \item[\isa{Executable{\isacharunderscore}Set}] \label{exec_set} allows to generate code
     2.9         for finite sets using lists.
    2.10 -    \item[\isa{Executable{\isacharunderscore}Rat}] \label{exec_rat} implements rational
    2.11 -       numbers as triples \isa{{\isacharparenleft}sign{\isacharcomma}\ enumerator{\isacharcomma}\ denominator{\isacharparenright}}.
    2.12 +    \item[\isa{Executable{\isacharunderscore}Rat}] implements rational
    2.13 +       numbers.
    2.14      \item[\isa{Executable{\isacharunderscore}Real}] implements a subset of real numbers,
    2.15         namly those representable by rational numbers.
    2.16      \item[\isa{Efficient{\isacharunderscore}Nat}] \label{eff_nat} implements natural numbers by integers,
    2.17 @@ -1535,7 +1535,7 @@
    2.18  
    2.19    Another axiomatic extension is code generation
    2.20    for abstracted types.  For this, the  
    2.21 -  \isa{Executable{\isacharunderscore}Rat} theory (see \secref{exec_rat})
    2.22 +  \isa{Executable{\isacharunderscore}Set} theory (see \secref{exec_set})
    2.23    forms a good example.%
    2.24  \end{isamarkuptext}%
    2.25  \isamarkuptrue%
    2.26 @@ -1552,12 +1552,12 @@
    2.27  \end{isamarkuptext}%
    2.28  \isamarkuptrue%
    2.29  %
    2.30 -\isamarkupsubsection{Constants with type discipline: codegen\_consts.ML%
    2.31 +\isamarkupsubsection{Basics: \isa{CodeUnit}%
    2.32  }
    2.33  \isamarkuptrue%
    2.34  %
    2.35  \begin{isamarkuptext}%
    2.36 -This Pure module manages identification of (probably overloaded)
    2.37 +This module provides identification of (probably overloaded)
    2.38    constants by unique identifiers.%
    2.39  \end{isamarkuptext}%
    2.40  \isamarkuptrue%
    2.41 @@ -1570,20 +1570,20 @@
    2.42  %
    2.43  \begin{isamarkuptext}%
    2.44  \begin{mldecls}
    2.45 -  \indexmltype{CodegenConsts.const}\verb|type CodegenConsts.const = string * string option| \\
    2.46 -  \indexml{CodegenConsts.const-of-cexpr}\verb|CodegenConsts.const_of_cexpr: theory -> string * typ -> CodegenConsts.const| \\
    2.47 +  \indexmltype{CodeUnit.const}\verb|type CodeUnit.const = string * string option| \\
    2.48 +  \indexml{CodeUnit.const-of-cexpr}\verb|CodeUnit.const_of_cexpr: theory -> string * typ -> CodeUnit.const| \\
    2.49   \end{mldecls}
    2.50  
    2.51    \begin{description}
    2.52  
    2.53 -  \item \verb|CodegenConsts.const| is the identifier type:
    2.54 +  \item \verb|CodeUnit.const| is the identifier type:
    2.55       the product of a \emph{string} with a list of \emph{typs}.
    2.56       The \emph{string} is the constant name as represented inside Isabelle;
    2.57       for overloaded constants, the attached \emph{string option}
    2.58       is either \isa{SOME} type constructor denoting an instance,
    2.59       or \isa{NONE} for the polymorphic constant.
    2.60  
    2.61 -  \item \verb|CodegenConsts.const_of_cexpr|~\isa{thy}~\isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}}
    2.62 +  \item \verb|CodeUnit.const_of_cexpr|~\isa{thy}~\isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}}
    2.63       maps a constant expression \isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}}
    2.64       to its canonical identifier.
    2.65  
    2.66 @@ -1598,7 +1598,7 @@
    2.67  %
    2.68  \endisadelimmlref
    2.69  %
    2.70 -\isamarkupsubsection{Executable theory content: codegen\_data.ML%
    2.71 +\isamarkupsubsection{Executable theory content: \isa{Code}%
    2.72  }
    2.73  \isamarkuptrue%
    2.74  %
    2.75 @@ -1608,37 +1608,6 @@
    2.76  \end{isamarkuptext}%
    2.77  \isamarkuptrue%
    2.78  %
    2.79 -\isamarkupsubsubsection{Suspended theorems%
    2.80 -}
    2.81 -\isamarkuptrue%
    2.82 -%
    2.83 -\isadelimmlref
    2.84 -%
    2.85 -\endisadelimmlref
    2.86 -%
    2.87 -\isatagmlref
    2.88 -%
    2.89 -\begin{isamarkuptext}%
    2.90 -\begin{mldecls}
    2.91 -  \indexml{CodegenData.lazy-thms}\verb|CodegenData.lazy_thms: (unit -> thm list) -> thm list Susp.T|
    2.92 -  \end{mldecls}
    2.93 -
    2.94 -  \begin{description}
    2.95 -
    2.96 -  \item \verb|CodegenData.lazy_thms|~\isa{f} turns an abstract
    2.97 -     theorem computation \isa{f} into a suspension of theorems.
    2.98 -
    2.99 -  \end{description}%
   2.100 -\end{isamarkuptext}%
   2.101 -\isamarkuptrue%
   2.102 -%
   2.103 -\endisatagmlref
   2.104 -{\isafoldmlref}%
   2.105 -%
   2.106 -\isadelimmlref
   2.107 -%
   2.108 -\endisadelimmlref
   2.109 -%
   2.110  \isamarkupsubsubsection{Managing executable content%
   2.111  }
   2.112  \isamarkuptrue%
   2.113 @@ -1651,69 +1620,69 @@
   2.114  %
   2.115  \begin{isamarkuptext}%
   2.116  \begin{mldecls}
   2.117 -  \indexml{CodegenData.add-func}\verb|CodegenData.add_func: bool -> thm -> theory -> theory| \\
   2.118 -  \indexml{CodegenData.del-func}\verb|CodegenData.del_func: thm -> theory -> theory| \\
   2.119 -  \indexml{CodegenData.add-funcl}\verb|CodegenData.add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory| \\
   2.120 -  \indexml{CodegenData.add-inline}\verb|CodegenData.add_inline: thm -> theory -> theory| \\
   2.121 -  \indexml{CodegenData.del-inline}\verb|CodegenData.del_inline: thm -> theory -> theory| \\
   2.122 -  \indexml{CodegenData.add-inline-proc}\verb|CodegenData.add_inline_proc: string * (theory -> cterm list -> thm list)|\isasep\isanewline%
   2.123 +  \indexml{Code.add-func}\verb|Code.add_func: bool -> thm -> theory -> theory| \\
   2.124 +  \indexml{Code.del-func}\verb|Code.del_func: thm -> theory -> theory| \\
   2.125 +  \indexml{Code.add-funcl}\verb|Code.add_funcl: CodeUnit.const * thm list Susp.T -> theory -> theory| \\
   2.126 +  \indexml{Code.add-inline}\verb|Code.add_inline: thm -> theory -> theory| \\
   2.127 +  \indexml{Code.del-inline}\verb|Code.del_inline: thm -> theory -> theory| \\
   2.128 +  \indexml{Code.add-inline-proc}\verb|Code.add_inline_proc: string * (theory -> cterm list -> thm list)|\isasep\isanewline%
   2.129  \verb|    -> theory -> theory| \\
   2.130 -  \indexml{CodegenData.del-inline-proc}\verb|CodegenData.del_inline_proc: string -> theory -> theory| \\
   2.131 -  \indexml{CodegenData.add-preproc}\verb|CodegenData.add_preproc: string * (theory -> thm list -> thm list)|\isasep\isanewline%
   2.132 +  \indexml{Code.del-inline-proc}\verb|Code.del_inline_proc: string -> theory -> theory| \\
   2.133 +  \indexml{Code.add-preproc}\verb|Code.add_preproc: string * (theory -> thm list -> thm list)|\isasep\isanewline%
   2.134  \verb|    -> theory -> theory| \\
   2.135 -  \indexml{CodegenData.del-preproc}\verb|CodegenData.del_preproc: string -> theory -> theory| \\
   2.136 -  \indexml{CodegenData.add-datatype}\verb|CodegenData.add_datatype: string * ((string * sort) list * (string * typ list) list)|\isasep\isanewline%
   2.137 +  \indexml{Code.del-preproc}\verb|Code.del_preproc: string -> theory -> theory| \\
   2.138 +  \indexml{Code.add-datatype}\verb|Code.add_datatype: string * ((string * sort) list * (string * typ list) list)|\isasep\isanewline%
   2.139  \verb|    -> theory -> theory| \\
   2.140 -  \indexml{CodegenData.get-datatype}\verb|CodegenData.get_datatype: theory -> string|\isasep\isanewline%
   2.141 +  \indexml{Code.get-datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
   2.142  \verb|    -> (string * sort) list * (string * typ list) list| \\
   2.143 -  \indexml{CodegenData.get-datatype-of-constr}\verb|CodegenData.get_datatype_of_constr: theory -> CodegenConsts.const -> string option|
   2.144 +  \indexml{Code.get-datatype-of-constr}\verb|Code.get_datatype_of_constr: theory -> CodeUnit.const -> string option|
   2.145    \end{mldecls}
   2.146  
   2.147    \begin{description}
   2.148  
   2.149 -  \item \verb|CodegenData.add_func|~\isa{thm}~\isa{thy} adds function
   2.150 +  \item \verb|Code.add_func|~\isa{thm}~\isa{thy} adds function
   2.151       theorem \isa{thm} to executable content.
   2.152  
   2.153 -  \item \verb|CodegenData.del_func|~\isa{thm}~\isa{thy} removes function
   2.154 +  \item \verb|Code.del_func|~\isa{thm}~\isa{thy} removes function
   2.155       theorem \isa{thm} from executable content, if present.
   2.156  
   2.157 -  \item \verb|CodegenData.add_funcl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds
   2.158 +  \item \verb|Code.add_funcl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds
   2.159       suspended defining equations \isa{lthms} for constant
   2.160       \isa{const} to executable content.
   2.161  
   2.162 -  \item \verb|CodegenData.add_inline|~\isa{thm}~\isa{thy} adds
   2.163 +  \item \verb|Code.add_inline|~\isa{thm}~\isa{thy} adds
   2.164       inlining theorem \isa{thm} to executable content.
   2.165  
   2.166 -  \item \verb|CodegenData.del_inline|~\isa{thm}~\isa{thy} remove
   2.167 +  \item \verb|Code.del_inline|~\isa{thm}~\isa{thy} remove
   2.168       inlining theorem \isa{thm} from executable content, if present.
   2.169  
   2.170 -  \item \verb|CodegenData.add_inline_proc|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
   2.171 +  \item \verb|Code.add_inline_proc|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
   2.172       inline procedure \isa{f} (named \isa{name}) to executable content;
   2.173       \isa{f} is a computation of rewrite rules dependent on
   2.174       the current theory context and the list of all arguments
   2.175       and right hand sides of the defining equations belonging
   2.176       to a certain function definition.
   2.177  
   2.178 -  \item \verb|CodegenData.del_inline_proc|~\isa{name}~\isa{thy} removes
   2.179 +  \item \verb|Code.del_inline_proc|~\isa{name}~\isa{thy} removes
   2.180       inline procedure named \isa{name} from executable content.
   2.181  
   2.182 -  \item \verb|CodegenData.add_preproc|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
   2.183 +  \item \verb|Code.add_preproc|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
   2.184       generic preprocessor \isa{f} (named \isa{name}) to executable content;
   2.185       \isa{f} is a transformation of the defining equations belonging
   2.186       to a certain function definition, depending on the
   2.187       current theory context.
   2.188  
   2.189 -  \item \verb|CodegenData.del_preproc|~\isa{name}~\isa{thy} removes
   2.190 +  \item \verb|Code.del_preproc|~\isa{name}~\isa{thy} removes
   2.191       generic preprcoessor named \isa{name} from executable content.
   2.192  
   2.193 -  \item \verb|CodegenData.add_datatype|~\isa{{\isacharparenleft}name{\isacharcomma}\ spec{\isacharparenright}}~\isa{thy} adds
   2.194 +  \item \verb|Code.add_datatype|~\isa{{\isacharparenleft}name{\isacharcomma}\ spec{\isacharparenright}}~\isa{thy} adds
   2.195       a datatype to executable content, with type constructor
   2.196       \isa{name} and specification \isa{spec}; \isa{spec} is
   2.197       a pair consisting of a list of type variable with sort
   2.198       constraints and a list of constructors with name
   2.199       and types of arguments.
   2.200  
   2.201 -  \item \verb|CodegenData.get_datatype_of_constr|~\isa{thy}~\isa{const}
   2.202 +  \item \verb|Code.get_datatype_of_constr|~\isa{thy}~\isa{const}
   2.203       returns type constructor corresponding to
   2.204       constructor \isa{const}; returns \isa{NONE}
   2.205       if \isa{const} is no constructor.
   2.206 @@ -1741,29 +1710,29 @@
   2.207  %
   2.208  \begin{isamarkuptext}%
   2.209  \begin{mldecls}
   2.210 -  \indexml{CodegenConsts.const-ord}\verb|CodegenConsts.const_ord: CodegenConsts.const * CodegenConsts.const -> order| \\
   2.211 -  \indexml{CodegenConsts.eq-const}\verb|CodegenConsts.eq_const: CodegenConsts.const * CodegenConsts.const -> bool| \\
   2.212 -  \indexml{CodegenConsts.read-const}\verb|CodegenConsts.read_const: theory -> string -> CodegenConsts.const| \\
   2.213 -  \indexmlstructure{CodegenConsts.Consttab}\verb|structure CodegenConsts.Consttab| \\
   2.214 -  \indexml{CodegenFunc.head-func}\verb|CodegenFunc.head_func: thm -> CodegenConsts.const * typ| \\
   2.215 -  \indexml{CodegenFunc.rewrite-func}\verb|CodegenFunc.rewrite_func: thm list -> thm -> thm| \\
   2.216 +  \indexml{CodeUnit.const-ord}\verb|CodeUnit.const_ord: CodeUnit.const * CodeUnit.const -> order| \\
   2.217 +  \indexml{CodeUnit.eq-const}\verb|CodeUnit.eq_const: CodeUnit.const * CodeUnit.const -> bool| \\
   2.218 +  \indexml{CodeUnit.read-const}\verb|CodeUnit.read_const: theory -> string -> CodeUnit.const| \\
   2.219 +  \indexmlstructure{CodeUnit.Consttab}\verb|structure CodeUnit.Consttab| \\
   2.220 +  \indexml{CodeUnit.head-func}\verb|CodeUnit.head_func: thm -> CodeUnit.const * typ| \\
   2.221 +  \indexml{CodeUnit.rewrite-func}\verb|CodeUnit.rewrite_func: thm list -> thm -> thm| \\
   2.222    \end{mldecls}
   2.223  
   2.224    \begin{description}
   2.225  
   2.226 -  \item \verb|CodegenConsts.const_ord|,~\verb|CodegenConsts.eq_const|
   2.227 +  \item \verb|CodeUnit.const_ord|,~\verb|CodeUnit.eq_const|
   2.228       provide order and equality on constant identifiers.
   2.229  
   2.230 -  \item \verb|CodegenConsts.Consttab|
   2.231 +  \item \verb|CodeUnit.Consttab|
   2.232       provides table structures with constant identifiers as keys.
   2.233  
   2.234 -  \item \verb|CodegenConsts.read_const|~\isa{thy}~\isa{s}
   2.235 +  \item \verb|CodeUnit.read_const|~\isa{thy}~\isa{s}
   2.236       reads a constant as a concrete term expression \isa{s}.
   2.237  
   2.238 -  \item \verb|CodegenFunc.head_func|~\isa{thm}
   2.239 +  \item \verb|CodeUnit.head_func|~\isa{thm}
   2.240       extracts the constant and its type from a defining equation \isa{thm}.
   2.241  
   2.242 -  \item \verb|CodegenFunc.rewrite_func|~\isa{rews}~\isa{thm}
   2.243 +  \item \verb|CodeUnit.rewrite_func|~\isa{rews}~\isa{thm}
   2.244       rewrites a defining equation \isa{thm} with a set of rewrite
   2.245       rules \isa{rews}; only arguments and right hand side are rewritten,
   2.246       not the head of the defining equation.
   2.247 @@ -1819,7 +1788,7 @@
   2.248    \isa{type\ T} \\
   2.249    \isa{val\ empty{\isacharcolon}\ T} \\
   2.250    \isa{val\ merge{\isacharcolon}\ Pretty{\isachardot}pp\ {\isasymrightarrow}\ T\ {\isacharasterisk}\ T\ {\isasymrightarrow}\ T} \\
   2.251 -  \isa{val\ purge{\isacharcolon}\ theory\ option\ {\isasymrightarrow}\ CodegenConsts{\isachardot}const\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
   2.252 +  \isa{val\ purge{\isacharcolon}\ theory\ option\ {\isasymrightarrow}\ CodeUnit{\isachardot}const\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
   2.253    \end{tabular}
   2.254  
   2.255    \begin{description}
   2.256 @@ -1875,7 +1844,7 @@
   2.257    until its underlying executable content changes.
   2.258  
   2.259    Defining equations are retrieved by instantiation
   2.260 -  of the functor \verb|CodegenFuncgrRetrieval|
   2.261 +  of the functor \verb|CodeFuncgrRetrieval|
   2.262    which takes two arguments:
   2.263  
   2.264    \medskip
   2.265 @@ -1892,12 +1861,12 @@
   2.266  
   2.267    \end{description}
   2.268  
   2.269 -  An instance of \verb|CodegenFuncgrRetrieval| in essence
   2.270 +  An instance of \verb|CodeFuncgrRetrieval| in essence
   2.271    provides the following interface:
   2.272  
   2.273    \medskip
   2.274    \begin{tabular}{l}
   2.275 -  \isa{make{\isacharcolon}\ theory\ {\isasymrightarrow}\ CodegenConsts{\isachardot}const\ list\ {\isasymrightarrow}\ CodegenFuncgr{\isachardot}T} \\
   2.276 +  \isa{make{\isacharcolon}\ theory\ {\isasymrightarrow}\ CodeUnit{\isachardot}const\ list\ {\isasymrightarrow}\ CodeFuncgr{\isachardot}T} \\
   2.277    \end{tabular}
   2.278  
   2.279    \begin{description}
   2.280 @@ -1923,33 +1892,33 @@
   2.281  %
   2.282  \begin{isamarkuptext}%
   2.283  \begin{mldecls}
   2.284 -  \indexmltype{CodegenFuncgr.T}\verb|type CodegenFuncgr.T| \\
   2.285 -  \indexml{CodegenFuncgr.funcs}\verb|CodegenFuncgr.funcs: CodegenFuncgr.T -> CodegenConsts.const -> thm list| \\
   2.286 -  \indexml{CodegenFuncgr.typ}\verb|CodegenFuncgr.typ: CodegenFuncgr.T -> CodegenConsts.const -> typ| \\
   2.287 -  \indexml{CodegenFuncgr.deps}\verb|CodegenFuncgr.deps: CodegenFuncgr.T|\isasep\isanewline%
   2.288 -\verb|    -> CodegenConsts.const list -> CodegenConsts.const list list| \\
   2.289 -  \indexml{CodegenFuncgr.all}\verb|CodegenFuncgr.all: CodegenFuncgr.T -> CodegenConsts.const list|
   2.290 +  \indexmltype{CodeFuncgr.T}\verb|type CodeFuncgr.T| \\
   2.291 +  \indexml{CodeFuncgr.funcs}\verb|CodeFuncgr.funcs: CodeFuncgr.T -> CodeUnit.const -> thm list| \\
   2.292 +  \indexml{CodeFuncgr.typ}\verb|CodeFuncgr.typ: CodeFuncgr.T -> CodeUnit.const -> typ| \\
   2.293 +  \indexml{CodeFuncgr.deps}\verb|CodeFuncgr.deps: CodeFuncgr.T|\isasep\isanewline%
   2.294 +\verb|    -> CodeUnit.const list -> CodeUnit.const list list| \\
   2.295 +  \indexml{CodeFuncgr.all}\verb|CodeFuncgr.all: CodeFuncgr.T -> CodeUnit.const list|
   2.296    \end{mldecls}
   2.297  
   2.298    \begin{description}
   2.299  
   2.300 -  \item \verb|CodegenFuncgr.T| represents
   2.301 +  \item \verb|CodeFuncgr.T| represents
   2.302      a normalized defining equation system.
   2.303  
   2.304 -  \item \verb|CodegenFuncgr.funcs|~\isa{funcgr}~\isa{const}
   2.305 +  \item \verb|CodeFuncgr.funcs|~\isa{funcgr}~\isa{const}
   2.306      retrieves defining equiations for constant \isa{const}.
   2.307  
   2.308 -  \item \verb|CodegenFuncgr.typ|~\isa{funcgr}~\isa{const}
   2.309 +  \item \verb|CodeFuncgr.typ|~\isa{funcgr}~\isa{const}
   2.310      retrieves function type for constant \isa{const}.
   2.311  
   2.312 -  \item \verb|CodegenFuncgr.deps|~\isa{funcgr}~\isa{consts}
   2.313 +  \item \verb|CodeFuncgr.deps|~\isa{funcgr}~\isa{consts}
   2.314      returns the transitive closure of dependencies for
   2.315      constants \isa{consts} as a partitioning where each partition
   2.316      corresponds to a strongly connected component of
   2.317      dependencies and any partition does \emph{not}
   2.318      depend on partitions further left.
   2.319  
   2.320 -  \item \verb|CodegenFuncgr.all|~\isa{funcgr}
   2.321 +  \item \verb|CodeFuncgr.all|~\isa{funcgr}
   2.322      returns all currently represented constants.
   2.323  
   2.324    \end{description}%