--- a/doc-src/IsarAdvanced/Codegen/Makefile Tue Nov 21 20:58:15 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Makefile Wed Nov 22 10:20:09 2006 +0100
@@ -19,7 +19,7 @@
dvi: $(NAME).dvi
-$(NAME).dvi: $(FILES) isabelle_isar.eps
+$(NAME).dvi: $(FILES) isabelle_isar.eps codegen_process.ps
$(LATEX) $(NAME)
$(BIBTEX) $(NAME)
$(LATEX) $(NAME)
@@ -27,7 +27,7 @@
pdf: $(NAME).pdf
-$(NAME).pdf: $(FILES) isabelle_isar.pdf
+$(NAME).pdf: $(FILES) isabelle_isar.pdf codegen_process.pdf
$(PDFLATEX) $(NAME)
$(BIBTEX) $(NAME)
$(PDFLATEX) $(NAME)
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Tue Nov 21 20:58:15 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Wed Nov 22 10:20:09 2006 +0100
@@ -4,7 +4,7 @@
(*<*)
theory Codegen
imports Main
-uses "../../../IsarImplementation/Thy/setup.ML"
+uses "../../../antiquote_setup.ML"
begin
ML {*
@@ -153,7 +153,7 @@
This executable specification is now turned to SML code:
*}
-code_gen fac (SML "examples/fac.ML")
+code_gen fac (*<*)(SML *)(*>*)(SML "examples/fac.ML")
text {*
The @{text "\<CODEGEN>"} command takes a space-separated list of
@@ -269,7 +269,7 @@
"pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))"
by simp
-code_gen pick (SML "examples/pick1.ML")
+code_gen pick (*<*)(SML *)(*>*)(SML "examples/pick1.ML")
text {*
This theorem is now added to the function equation table:
@@ -282,7 +282,7 @@
lemmas [code nofunc] = pick.simps
-code_gen pick (SML "examples/pick2.ML")
+code_gen pick (*<*)(SML *)(*>*)(SML "examples/pick2.ML")
text {*
\lstsml{Thy/examples/pick2.ML}
@@ -298,7 +298,7 @@
"fac n = (case n of 0 \<Rightarrow> 1 | Suc m \<Rightarrow> n * fac m)"
by (cases n) simp_all
-code_gen fac (SML "examples/fac_case.ML")
+code_gen fac (*<*)(SML *)(*>*)(SML "examples/fac_case.ML")
text {*
\lstsml{Thy/examples/fac_case.ML}
@@ -377,7 +377,7 @@
The whole code in SML with explicit dictionary passing:
*}
-code_gen dummy (SML "examples/class.ML")
+code_gen dummy (*<*)(SML *)(*>*)(SML "examples/class.ML")
text {*
\lstsml{Thy/examples/class.ML}
@@ -407,7 +407,7 @@
text {*
\noindent print all cached function equations (i.e.~\emph{after}
- any applied transformation. Inside the brackets a
+ any applied transformation). Inside the brackets a
list of constants may be given; their function
equations are added to the cache if not already present.
*}
@@ -443,15 +443,15 @@
\begin{description}
- \item[@{theory "ExecutableSet"}] allows to generate code
+ \item[@{text "ExecutableSet"}] allows to generate code
for finite sets using lists.
- \item[@{theory "ExecutableRat"}] \label{exec_rat} implements rational
+ \item[@{text "ExecutableRat"}] \label{exec_rat} implements rational
numbers as triples @{text "(sign, enumerator, denominator)"}.
- \item[@{theory "EfficientNat"}] \label{eff_nat} implements natural numbers by integers,
+ \item[@{text "EfficientNat"}] \label{eff_nat} implements natural numbers by integers,
which in general will result in higher efficency; pattern
matching with @{const "0\<Colon>nat"} / @{const "Suc"}
is eliminated.
- \item[@{theory "MLString"}] provides an additional datatype @{text "mlstring"};
+ \item[@{text "MLString"}] provides an additional datatype @{text "mlstring"};
in the HOL default setup, strings in HOL are mapped to list
of chars in SML; values of type @{text "mlstring"} are
mapped to strings in SML.
@@ -521,7 +521,7 @@
list of function theorems, provided that neither the heading
constant nor its type change. The @{const "0\<Colon>nat"} / @{const Suc}
pattern elimination implemented in
- theory @{theory "EfficientNat"} (\secref{eff_nat}) uses this
+ theory @{text "EfficientNat"} (\secref{eff_nat}) uses this
interface.
\begin{warn}
@@ -557,7 +557,7 @@
(SML and and and)
(*>*)
-code_gen in_interval (SML "examples/bool_literal.ML")
+code_gen in_interval (*<*)(SML *)(*>*)(SML "examples/bool_literal.ML")
text {*
\lstsml{Thy/examples/bool_literal.ML}
@@ -600,7 +600,7 @@
After this setup, code looks quite more readable:
*}
-code_gen in_interval (SML "examples/bool_mlbool.ML")
+code_gen in_interval (*<*)(SML *)(*>*)(SML "examples/bool_mlbool.ML")
text {*
\lstsml{Thy/examples/bool_mlbool.ML}
@@ -616,7 +616,7 @@
code_const %tt "op \<and>"
(SML infixl 1 "andalso")
-code_gen in_interval (SML "examples/bool_infix.ML")
+code_gen in_interval (*<*)(SML *)(*>*)(SML "examples/bool_infix.ML")
text {*
\lstsml{Thy/examples/bool_infix.ML}
@@ -675,7 +675,7 @@
and "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
(SML "IntInf.+ (_, _)" and "IntInf.* (_, _)")
-code_gen double_inc (SML "examples/integers.ML")
+code_gen double_inc (*<*)(SML *)(*>*)(SML "examples/integers.ML")
text {*
resulting in:
@@ -727,7 +727,7 @@
performs an explicit equality check.
*}
-code_gen collect_duplicates (SML "examples/collect_duplicates.ML")
+code_gen collect_duplicates (*<*)(SML *)(*>*)(SML "examples/collect_duplicates.ML")
text {*
\lstsml{Thy/examples/collect_duplicates.ML}
@@ -741,28 +741,21 @@
(*<*)
setup {* Sign.add_path "foo" *}
+consts "op =" :: "'a"
(*>*)
-class eq =
- fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-
-defs
- eq (*[symmetric, code inline, code func]*): "eq \<equiv> (op =)"
+axclass eq \<subseteq> type
+ attach "op ="
text {*
This merely introduces a class @{text eq} with corresponding
- operation @{const eq}, which by definition is isomorphic
- to @{const "op ="}; the preprocessing framework does the rest.
+ operation @{const "op ="};
+ the preprocessing framework does the rest.
*}
(*<*)
-lemmas [code noinline] = eq
-
hide (open) "class" eq
-hide (open) const eq
-
-lemmas [symmetric, code func] = eq_def
-
+hide (open) const "op ="
setup {* Sign.parent_path *}
(*>*)
@@ -774,26 +767,6 @@
are some cases when it suddenly comes to surface:
*}
-subsubsection {* code lemmas and customary serializations for equality *}
-
-text {*
- Examine the following:
-*}
-
-code_const %tt "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
- (SML "!(_ : IntInf.int = _)")
-
-text {*
- What is wrong here? Since @{const "op ="} is nothing else then
- a plain constant, this customary serialization will refer
- to polymorphic equality @{const "op = \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool"}.
- Instead, we want the specific equality on @{typ int},
- by using the overloaded constant @{const "Code_Generator.eq"}:
-*}
-
-code_const %tt "Code_Generator.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
- (SML "!(_ : IntInf.int = _)")
-
subsubsection {* typedecls interpreted by customary serializations *}
text {*
@@ -818,19 +791,19 @@
This, though, is not sufficient: @{typ key} is no instance
of @{text eq} since @{typ key} is no datatype; the instance
has to be declared manually, including a serialization
- for the particular instance of @{const "Code_Generator.eq"}:
+ for the particular instance of @{const "op ="}:
*}
instance key :: eq ..
-code_const %tt "Code_Generator.eq \<Colon> key \<Rightarrow> key \<Rightarrow> bool"
- (SML "!(_ : string = _)")
+code_const %tt "op = \<Colon> key \<Rightarrow> key \<Rightarrow> bool"
+ (SML "!((_ : string) = _)")
text {*
Then everything goes fine:
*}
-code_gen lookup (SML "examples/lookup.ML")
+code_gen lookup (*<*)(SML *)(*>*)(SML "examples/lookup.ML")
text {*
\lstsml{Thy/examples/lookup.ML}
@@ -847,8 +820,6 @@
(*<*)
setup {* Sign.add_path "foobar" *}
-
-class eq = fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
class ord =
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_/ \<^loc>\<le> _)" [50, 51] 50)
fixes less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_/ \<^loc>< _)" [50, 51] 50)
@@ -860,8 +831,8 @@
"p1 \<le> p2 \<equiv> p1 < p2 \<or> (p1 \<Colon> 'a\<Colon>ord \<times> 'b\<Colon>ord) = p2" ..
(*<*)
-hide "class" eq ord
-hide const eq less_eq less
+hide "class" ord
+hide const less_eq less
setup {* Sign.parent_path *}
(*>*)
@@ -885,7 +856,7 @@
*}
code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>{eq, ord} \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
- (SML "examples/lexicographic.ML")
+ (*<*)(SML *)(*>*)(SML "examples/lexicographic.ML")
text {*
\lstsml{Thy/examples/lexicographic.ML}
@@ -989,7 +960,7 @@
lemma [code func]:
"insert = insert" ..
-code_gen dummy_set foobar_set (SML "examples/dirty_set.ML")
+code_gen dummy_set foobar_set (*<*)(SML *)(*>*)(SML "examples/dirty_set.ML")
text {*
\lstsml{Thy/examples/dirty_set.ML}
@@ -1091,7 +1062,7 @@
For technical reasons, we further have to provide a
synonym for @{const None} which in code generator view
- is a function rather than a datatype constructor
+ is a function rather than a datatype constructor:
*}
definition
@@ -1116,14 +1087,14 @@
declare dummy_option.simps [code func]
(*>*)
-code_gen dummy_option (SML "examples/arbitrary.ML")
+code_gen dummy_option (*<*)(SML *)(*>*)(SML "examples/arbitrary.ML")
text {*
\lstsml{Thy/examples/arbitrary.ML}
Another axiomatic extension is code generation
for abstracted types. For this, the
- @{theory "ExecutableRat"} (see \secref{exec_rat})
+ @{text "ExecutableRat"} (see \secref{exec_rat})
forms a good example.
*}
@@ -1366,13 +1337,22 @@
a final state yet.
Changes likely to occur in future.
\end{warn}
-
- \fixme
*}
subsubsection {* Data depending on the theory's executable content *}
text {*
+ Due to incrementality of code generation, changes in the
+ theory's executable content have to be propagated in a
+ certain fashion. Additionally, such changes may occur
+ not only during theory extension but also during theory
+ merge, which is a little bit nasty from an implementation
+ point of view. The framework provides a solution
+ to this technical challenge by providing a functorial
+ data slot @{ML_functor CodeDataFun}; on instantiation
+ of this functor, the following types and operations
+ are required:
+
\medskip
\begin{tabular}{l}
@{text "val name: string"} \\
@@ -1382,66 +1362,141 @@
@{text "val purge: theory option \<rightarrow> CodegenConsts.const list option \<rightarrow> T \<rightarrow> T"}
\end{tabular}
+ \begin{description}
+
+ \item @{text name} is a system-wide unique name identifying the data.
+
+ \item @{text T} the type of data to store.
+
+ \item @{text empty} initial (empty) data.
+
+ \item @{text merge} merging two data slots.
+
+ \item @{text purge}~@{text thy}~@{text cs} propagates changes in executable content;
+ if possible, the current theory context is handed over
+ as argument @{text thy} (if there is no current theory context (e.g.~during
+ theory merge, @{ML NONE}); @{text cs} indicates the kind
+ of change: @{ML NONE} stands for a fundamental change
+ which invalidates any existing code, @{text "SOME cs"}
+ hints that executable content for constants @{text cs}
+ has changed.
+
+ \end{description}
+
+ An instance of @{ML_functor CodeDataFun} provides the following
+ interface:
+
\medskip
-
\begin{tabular}{l}
@{text "init: theory \<rightarrow> theory"} \\
@{text "get: theory \<rightarrow> T"} \\
@{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\
@{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"}
\end{tabular}
-*}
-
-text %mlref {*
- \begin{mldecls}
- @{index_ML_functor CodeDataFun}
- \end{mldecls}
\begin{description}
- \item @{ML_functor CodeDataFun}@{text "(spec)"} declares code
- dependent data according to the specification provided as
- argument structure. The resulting structure provides data init and
- access operations as described above.
+ \item @{text init} initialization during theory setup.
+
+ \item @{text get} retrieval of the current data.
+
+ \item @{text change} update of current data (cached!)
+ by giving a continuation.
+
+ \item @{text change_yield} update with side result.
\end{description}
*}
subsubsection {* Datatype hooks *}
+text {*
+ Isabelle/HOL's datatype package provides a mechanism to
+ extend theories depending on datatype declarations:
+ \emph{datatype hooks}. For example, when declaring a new
+ datatype, a hook proves function equations for equality on
+ that datatype (if possible).
+*}
+
text %mlref {*
\begin{mldecls}
@{index_ML_type DatatypeHooks.hook: "string list -> theory -> theory"} \\
@{index_ML DatatypeHooks.add: "DatatypeHooks.hook -> theory -> theory"}
\end{mldecls}
+
+ \begin{description}
+
+ \item @{ML_type DatatypeHooks.hook} specifies the interface
+ of \emph{datatype hooks}: a theory update
+ depending on the list of newly introduced
+ datatype names.
+
+ \item @{ML DatatypeHooks.add} adds a hook to the
+ chain of all hooks.
+
+ \end{description}
+*}
+
+subsubsection {* Trivial typedefs -- type copies *}
+
+text {*
+ Sometimes packages will introduce new types
+ as \emph{marked type copies} similar to Haskell's
+ @{text newtype} declaration (e.g. the HOL record package)
+ \emph{without} tinkering with the overhead of datatypes.
+ Technically, these type copies are trivial forms of typedefs.
+ Since these type copies in code generation view are nothing
+ else than datatypes, they have been given a own package
+ in order to faciliate code generation:
*}
text %mlref {*
\begin{mldecls}
- @{index_ML_type TypecopyPackage.info: "{
- vs: (string * sort) list,
- constr: string,
- typ: typ,
- inject: thm,
- proj: string * typ,
- proj_def: thm
- }"} \\
+ @{index_ML_type TypecopyPackage.info} \\
@{index_ML TypecopyPackage.add_typecopy: "
bstring * string list -> typ -> (bstring * bstring) option
-> theory -> (string * TypecopyPackage.info) * theory"} \\
- @{index_ML TypecopyPackage.get_typecopies: "theory -> string list"} \\
@{index_ML TypecopyPackage.get_typecopy_info: "theory
-> string -> TypecopyPackage.info option"} \\
- @{index_ML_type TypecopyPackage.hook} \\
- @{index_ML TypecopyPackage.add_hook: "TypecopyPackage.hook -> theory -> theory"} \\
@{index_ML TypecopyPackage.get_spec: "theory -> string
- -> (string * sort) list * (string * typ list) list"}
+ -> (string * sort) list * (string * typ list) list"} \\
+ @{index_ML_type TypecopyPackage.hook: "string * TypecopyPackage.info -> theory -> theory"} \\
+ @{index_ML TypecopyPackage.add_hook:
+ "TypecopyPackage.hook -> theory -> theory"} \\
\end{mldecls}
+
+ \begin{description}
+
+ \item @{ML_type TypecopyPackage.info} a record containing
+ the specification and further data of a type copy.
+
+ \item @{ML TypecopyPackage.add_typecopy} defines a new
+ type copy.
+
+ \item @{ML TypecopyPackage.get_typecopy_info} retrieves
+ data of an existing type copy.
+
+ \item @{ML TypecopyPackage.get_spec} retrieves datatype-like
+ specification of a type copy.
+
+ \item @{ML_type TypecopyPackage.hook},~@{ML TypecopyPackage.add_hook}
+ provide a hook mechanism corresponding to the hook mechanism
+ on datatypes.
+
+ \end{description}
+*}
+
+subsubsection {* Unifying type copies and datatypes *}
+
+text {*
+ Since datatypes and type copies are mapped to the same concept (datatypes)
+ by code generation, the view on both is unified \qt{code types}:
*}
text %mlref {*
\begin{mldecls}
- @{index_ML_type DatatypeCodegen.hook: "(string * (bool * ((string * sort) list * (string * typ list) list))) list
+ @{index_ML_type DatatypeCodegen.hook: "(string * (bool * ((string * sort) list
+ * (string * typ list) list))) list
-> theory -> theory"} \\
@{index_ML DatatypeCodegen.add_codetypes_hook_bootstrap: "
DatatypeCodegen.hook -> theory -> theory"}
@@ -1449,8 +1504,25 @@
*}
text {*
- \fixme
-% \emph{Happy proving, happy hacking!}
+ \begin{description}
+
+ \item @{ML_type DatatypeCodegen.hook} specifies the code type hook
+ interface: a theory transformation depending on a list of
+ mutual recursive code types; each entry in the list
+ has the structure @{text "(name, (is_data, (vars, cons)))"}
+ where @{text name} is the name of the code type, @{text is_data}
+ is true iff @{text name} is a datatype rather then a type copy,
+ and @{text "(vars, cons)"} is the specification of the code type.
+
+ \item @{ML DatatypeCodegen.add_codetypes_hook_bootstrap} adds a code
+ type hook; the hook is immediately processed for all already
+ existing datatypes, in blocks of mutual recursive datatypes,
+ where all datatypes a block depends on are processed before
+ the block.
+
+ \end{description}
+
+ \emph{Happy proving, happy hacking!}
*}
end
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Tue Nov 21 20:58:15 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Wed Nov 22 10:20:09 2006 +0100
@@ -533,7 +533,7 @@
\ {\isacharparenleft}{\isacharparenright}%
\begin{isamarkuptext}%
\noindent print all cached function equations (i.e.~\emph{after}
- any applied transformation. Inside the brackets a
+ any applied transformation). Inside the brackets a
list of constants may be given; their function
equations are added to the cache if not already present.%
\end{isamarkuptext}%
@@ -574,15 +574,15 @@
\begin{description}
- \item[ExecutableSet] allows to generate code
+ \item[\isa{ExecutableSet}] allows to generate code
for finite sets using lists.
- \item[ExecutableRat] \label{exec_rat} implements rational
+ \item[\isa{ExecutableRat}] \label{exec_rat} implements rational
numbers as triples \isa{{\isacharparenleft}sign{\isacharcomma}\ enumerator{\isacharcomma}\ denominator{\isacharparenright}}.
- \item[EfficientNat] \label{eff_nat} implements natural numbers by integers,
+ \item[\isa{EfficientNat}] \label{eff_nat} implements natural numbers by integers,
which in general will result in higher efficency; pattern
matching with \isa{{\isadigit{0}}} / \isa{Suc}
is eliminated.
- \item[MLString] provides an additional datatype \isa{mlstring};
+ \item[\isa{MLString}] provides an additional datatype \isa{mlstring};
in the HOL default setup, strings in HOL are mapped to list
of chars in SML; values of type \isa{mlstring} are
mapped to strings in SML.
@@ -687,7 +687,7 @@
list of function theorems, provided that neither the heading
constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc}
pattern elimination implemented in
- theory EfficientNat (\secref{eff_nat}) uses this
+ theory \isa{EfficientNat} (\secref{eff_nat}) uses this
interface.
\begin{warn}
@@ -976,20 +976,16 @@
{\isafoldML}%
%
\isadelimML
-\isanewline
%
\endisadelimML
-\isacommand{class}\isamarkupfalse%
-\ eq\ {\isacharequal}\isanewline
-\ \ \isakeyword{fixes}\ eq\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
\isanewline
-\isacommand{defs}\isamarkupfalse%
-\isanewline
-\ \ eq\ {\isacharcolon}\ {\isachardoublequoteopen}eq\ {\isasymequiv}\ {\isacharparenleft}op\ {\isacharequal}{\isacharparenright}{\isachardoublequoteclose}%
+\isacommand{axclass}\isamarkupfalse%
+\ eq\ {\isasymsubseteq}\ type\isanewline
+\ \ \isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
This merely introduces a class \isa{eq} with corresponding
- operation \isa{eq}, which by definition is isomorphic
- to \isa{op\ {\isacharequal}}; the preprocessing framework does the rest.%
+ operation \isa{foo{\isachardot}op\ {\isacharequal}};
+ the preprocessing framework does the rest.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1015,54 +1011,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{code lemmas and customary serializations for equality%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Examine the following:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtt
-%
-\endisadelimtt
-%
-\isatagtt
-\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
-\ {\isachardoublequoteopen}op\ {\isacharequal}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
-%
-\isadelimtt
-%
-\endisadelimtt
-%
-\begin{isamarkuptext}%
-What is wrong here? Since \isa{op\ {\isacharequal}} is nothing else then
- a plain constant, this customary serialization will refer
- to polymorphic equality \isa{op\ {\isacharequal}}.
- Instead, we want the specific equality on \isa{int},
- by using the overloaded constant \isa{Code{\isacharunderscore}Generator{\isachardot}eq}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtt
-%
-\endisadelimtt
-%
-\isatagtt
-\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
-\ {\isachardoublequoteopen}Code{\isacharunderscore}Generator{\isachardot}eq\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
-%
-\isadelimtt
-%
-\endisadelimtt
-%
\isamarkupsubsubsection{typedecls interpreted by customary serializations%
}
\isamarkuptrue%
@@ -1100,7 +1048,7 @@
This, though, is not sufficient: \isa{key} is no instance
of \isa{eq} since \isa{key} is no datatype; the instance
has to be declared manually, including a serialization
- for the particular instance of \isa{Code{\isacharunderscore}Generator{\isachardot}eq}:%
+ for the particular instance of \isa{op\ {\isacharequal}}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{instance}\isamarkupfalse%
@@ -1127,8 +1075,8 @@
%
\isatagtt
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
-\ {\isachardoublequoteopen}Code{\isacharunderscore}Generator{\isachardot}eq\ {\isasymColon}\ key\ {\isasymRightarrow}\ key\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ string\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\ {\isachardoublequoteopen}op\ {\isacharequal}\ {\isasymColon}\ key\ {\isasymRightarrow}\ key\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ string{\isacharparenright}\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
\endisatagtt
{\isafoldtt}%
%
@@ -1573,7 +1521,7 @@
For technical reasons, we further have to provide a
synonym for \isa{None} which in code generator view
- is a function rather than a datatype constructor%
+ is a function rather than a datatype constructor:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
@@ -1602,7 +1550,7 @@
Another axiomatic extension is code generation
for abstracted types. For this, the
- ExecutableRat (see \secref{exec_rat})
+ \isa{ExecutableRat} (see \secref{exec_rat})
forms a good example.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -1933,9 +1881,7 @@
Some interfaces discussed here have not reached
a final state yet.
Changes likely to occur in future.
- \end{warn}
-
- \fixme%
+ \end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1944,7 +1890,18 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\medskip
+Due to incrementality of code generation, changes in the
+ theory's executable content have to be propagated in a
+ certain fashion. Additionally, such changes may occur
+ not only during theory extension but also during theory
+ merge, which is a little bit nasty from an implementation
+ point of view. The framework provides a solution
+ to this technical challenge by providing a functorial
+ data slot \verb|CodeDataFun|; on instantiation
+ of this functor, the following types and operations
+ are required:
+
+ \medskip
\begin{tabular}{l}
\isa{val\ name{\isacharcolon}\ string} \\
\isa{type\ T} \\
@@ -1953,14 +1910,63 @@
\isa{val\ purge{\isacharcolon}\ theory\ option\ {\isasymrightarrow}\ CodegenConsts{\isachardot}const\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
\end{tabular}
+ \begin{description}
+
+ \item \isa{name} is a system-wide unique name identifying the data.
+
+ \item \isa{T} the type of data to store.
+
+ \item \isa{empty} initial (empty) data.
+
+ \item \isa{merge} merging two data slots.
+
+ \item \isa{purge}~\isa{thy}~\isa{cs} propagates changes in executable content;
+ if possible, the current theory context is handed over
+ as argument \isa{thy} (if there is no current theory context (e.g.~during
+ theory merge, \verb|NONE|); \isa{cs} indicates the kind
+ of change: \verb|NONE| stands for a fundamental change
+ which invalidates any existing code, \isa{SOME\ cs}
+ hints that executable content for constants \isa{cs}
+ has changed.
+
+ \end{description}
+
+ An instance of \verb|CodeDataFun| provides the following
+ interface:
+
\medskip
-
\begin{tabular}{l}
\isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ theory} \\
\isa{get{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\
\isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\
\isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T}
- \end{tabular}%
+ \end{tabular}
+
+ \begin{description}
+
+ \item \isa{init} initialization during theory setup.
+
+ \item \isa{get} retrieval of the current data.
+
+ \item \isa{change} update of current data (cached!)
+ by giving a continuation.
+
+ \item \isa{change{\isacharunderscore}yield} update with side result.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Datatype hooks%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle/HOL's datatype package provides a mechanism to
+ extend theories depending on datatype declarations:
+ \emph{datatype hooks}. For example, when declaring a new
+ datatype, a hook proves function equations for equality on
+ that datatype (if possible).%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1972,15 +1978,19 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexmlfunctor{CodeDataFun}\verb|functor CodeDataFun|
+ \indexmltype{DatatypeHooks.hook}\verb|type DatatypeHooks.hook = string list -> theory -> theory| \\
+ \indexml{DatatypeHooks.add}\verb|DatatypeHooks.add: DatatypeHooks.hook -> theory -> theory|
\end{mldecls}
\begin{description}
- \item \verb|CodeDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares code
- dependent data according to the specification provided as
- argument structure. The resulting structure provides data init and
- access operations as described above.
+ \item \verb|DatatypeHooks.hook| specifies the interface
+ of \emph{datatype hooks}: a theory update
+ depending on the list of newly introduced
+ datatype names.
+
+ \item \verb|DatatypeHooks.add| adds a hook to the
+ chain of all hooks.
\end{description}%
\end{isamarkuptext}%
@@ -1993,10 +2003,22 @@
%
\endisadelimmlref
%
-\isamarkupsubsubsection{Datatype hooks%
+\isamarkupsubsubsection{Trivial typedefs -- type copies%
}
\isamarkuptrue%
%
+\begin{isamarkuptext}%
+Sometimes packages will introduce new types
+ as \emph{marked type copies} similar to Haskell's
+ \isa{newtype} declaration (e.g. the HOL record package)
+ \emph{without} tinkering with the overhead of datatypes.
+ Technically, these type copies are trivial forms of typedefs.
+ Since these type copies in code generation view are nothing
+ else than datatypes, they have been given a own package
+ in order to faciliate code generation:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimmlref
%
\endisadelimmlref
@@ -2005,39 +2027,67 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexmltype{DatatypeHooks.hook}\verb|type DatatypeHooks.hook = string list -> theory -> theory| \\
- \indexml{DatatypeHooks.add}\verb|DatatypeHooks.add: DatatypeHooks.hook -> theory -> theory|
- \end{mldecls}%
+ \indexmltype{TypecopyPackage.info}\verb|type TypecopyPackage.info| \\
+ \indexml{TypecopyPackage.add-typecopy}\verb|TypecopyPackage.add_typecopy: |\isasep\isanewline%
+\verb| bstring * string list -> typ -> (bstring * bstring) option|\isasep\isanewline%
+\verb| -> theory -> (string * TypecopyPackage.info) * theory| \\
+ \indexml{TypecopyPackage.get-typecopy-info}\verb|TypecopyPackage.get_typecopy_info: theory|\isasep\isanewline%
+\verb| -> string -> TypecopyPackage.info option| \\
+ \indexml{TypecopyPackage.get-spec}\verb|TypecopyPackage.get_spec: theory -> string|\isasep\isanewline%
+\verb| -> (string * sort) list * (string * typ list) list| \\
+ \indexmltype{TypecopyPackage.hook}\verb|type TypecopyPackage.hook = string * TypecopyPackage.info -> theory -> theory| \\
+ \indexml{TypecopyPackage.add-hook}\verb|TypecopyPackage.add_hook: TypecopyPackage.hook -> theory -> theory| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|TypecopyPackage.info| a record containing
+ the specification and further data of a type copy.
+
+ \item \verb|TypecopyPackage.add_typecopy| defines a new
+ type copy.
+
+ \item \verb|TypecopyPackage.get_typecopy_info| retrieves
+ data of an existing type copy.
+
+ \item \verb|TypecopyPackage.get_spec| retrieves datatype-like
+ specification of a type copy.
+
+ \item \verb|TypecopyPackage.hook|,~\verb|TypecopyPackage.add_hook|
+ provide a hook mechanism corresponding to the hook mechanism
+ on datatypes.
+
+ \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsubsection{Unifying type copies and datatypes%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Since datatypes and type copies are mapped to the same concept (datatypes)
+ by code generation, the view on both is unified \qt{code types}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexmltype{TypecopyPackage.info}\verb|type TypecopyPackage.info = {|\isasep\isanewline%
-\verb| vs: (string * sort) list,|\isasep\isanewline%
-\verb| constr: string,|\isasep\isanewline%
-\verb| typ: typ,|\isasep\isanewline%
-\verb| inject: thm,|\isasep\isanewline%
-\verb| proj: string * typ,|\isasep\isanewline%
-\verb| proj_def: thm|\isasep\isanewline%
-\verb| }| \\
- \indexml{TypecopyPackage.add-typecopy}\verb|TypecopyPackage.add_typecopy: |\isasep\isanewline%
-\verb| bstring * string list -> typ -> (bstring * bstring) option|\isasep\isanewline%
-\verb| -> theory -> (string * TypecopyPackage.info) * theory| \\
- \indexml{TypecopyPackage.get-typecopies}\verb|TypecopyPackage.get_typecopies: theory -> string list| \\
- \indexml{TypecopyPackage.get-typecopy-info}\verb|TypecopyPackage.get_typecopy_info: theory|\isasep\isanewline%
-\verb| -> string -> TypecopyPackage.info option| \\
- \indexmltype{TypecopyPackage.hook}\verb|type TypecopyPackage.hook| \\
- \indexml{TypecopyPackage.add-hook}\verb|TypecopyPackage.add_hook: TypecopyPackage.hook -> theory -> theory| \\
- \indexml{TypecopyPackage.get-spec}\verb|TypecopyPackage.get_spec: theory -> string|\isasep\isanewline%
-\verb| -> (string * sort) list * (string * typ list) list|
- \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexmltype{DatatypeCodegen.hook}\verb|type DatatypeCodegen.hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list|\isasep\isanewline%
+ \indexmltype{DatatypeCodegen.hook}\verb|type DatatypeCodegen.hook = (string * (bool * ((string * sort) list|\isasep\isanewline%
+\verb| * (string * typ list) list))) list|\isasep\isanewline%
\verb| -> theory -> theory| \\
\indexml{DatatypeCodegen.add-codetypes-hook-bootstrap}\verb|DatatypeCodegen.add_codetypes_hook_bootstrap: |\isasep\isanewline%
\verb| DatatypeCodegen.hook -> theory -> theory|
@@ -2053,8 +2103,25 @@
\endisadelimmlref
%
\begin{isamarkuptext}%
-\fixme
-% \emph{Happy proving, happy hacking!}%
+\begin{description}
+
+ \item \verb|DatatypeCodegen.hook| specifies the code type hook
+ interface: a theory transformation depending on a list of
+ mutual recursive code types; each entry in the list
+ has the structure \isa{{\isacharparenleft}name{\isacharcomma}\ {\isacharparenleft}is{\isacharunderscore}data{\isacharcomma}\ {\isacharparenleft}vars{\isacharcomma}\ cons{\isacharparenright}{\isacharparenright}{\isacharparenright}}
+ where \isa{name} is the name of the code type, \isa{is{\isacharunderscore}data}
+ is true iff \isa{name} is a datatype rather then a type copy,
+ and \isa{{\isacharparenleft}vars{\isacharcomma}\ cons{\isacharparenright}} is the specification of the code type.
+
+ \item \verb|DatatypeCodegen.add_codetypes_hook_bootstrap| adds a code
+ type hook; the hook is immediately processed for all already
+ existing datatypes, in blocks of mutual recursive datatypes,
+ where all datatypes a block depends on are processed before
+ the block.
+
+ \end{description}
+
+ \emph{Happy proving, happy hacking!}%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Tue Nov 21 20:58:15 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Wed Nov 22 10:20:09 2006 +0100
@@ -4,23 +4,16 @@
structure Code_Generator =
struct
-type 'a eq = {eq_ : 'a -> 'a -> bool};
-fun eq (A_:'a eq) = #eq_ A_;
+type 'a eq = {op_eq_ : 'a -> 'a -> bool};
+fun op_eq (A_:'a eq) = #op_eq_ A_;
end; (*struct Code_Generator*)
-structure HOL =
-struct
-
-fun op_eq (A_:'a Code_Generator.eq) a b = Code_Generator.eq A_ a b;
-
-end; (*struct HOL*)
-
structure List =
struct
fun memberl (A_1_:'a_1 Code_Generator.eq) x (y :: ys) =
- HOL.op_eq A_1_ x y orelse memberl A_1_ x ys
+ Code_Generator.op_eq A_1_ x y orelse memberl A_1_ x ys
| memberl (A_1_:'a_1 Code_Generator.eq) x [] = false;
end; (*struct List*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML Tue Nov 21 20:58:15 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML Wed Nov 22 10:20:09 2006 +0100
@@ -11,7 +11,7 @@
structure Codegen =
struct
-val dummy_set : Nat.nat -> Nat.nat list = Nat.Suc :: [];
+val dummy_set : (Nat.nat -> Nat.nat) list = Nat.Suc :: [];
val foobar_set : Nat.nat list =
Nat.Zero_nat ::
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Tue Nov 21 20:58:15 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Wed Nov 22 10:20:09 2006 +0100
@@ -4,16 +4,17 @@
structure Code_Generator =
struct
-type 'a eq = {eq_ : 'a -> 'a -> bool};
-fun eq (A_:'a eq) = #eq_ A_;
+type 'a eq = {op_eq_ : 'a -> 'a -> bool};
+fun op_eq (A_:'a eq) = #op_eq_ A_;
end; (*struct Code_Generator*)
structure Product_Type =
struct
-fun eq_prod (A_:'a Code_Generator.eq) (B_:'b Code_Generator.eq) (x1, y1)
- (x2, y2) = Code_Generator.eq A_ x1 x2 andalso Code_Generator.eq B_ y1 y2;
+fun op_eq_prod (A_:'a Code_Generator.eq) (B_:'b Code_Generator.eq) (x1, y1)
+ (x2, y2) =
+ Code_Generator.op_eq A_ x1 x2 andalso Code_Generator.op_eq B_ y1 y2;
end; (*struct Product_Type*)
@@ -36,14 +37,14 @@
val (x2a, y2a) = p2;
in
Orderings.less (#2 B_) x1a x2a orelse
- Code_Generator.eq (#1 B_) x1a x2a andalso
+ Code_Generator.op_eq (#1 B_) x1a x2a andalso
Orderings.less (#2 C_) y1a y2a
end;
fun less_eq_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
(C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
less_prod ((#1 B_), (#2 B_)) ((#1 C_), (#2 C_)) p1 p2 orelse
- Product_Type.eq_prod (#1 B_) (#1 C_) p1 p2;
+ Product_Type.op_eq_prod (#1 B_) (#1 C_) p1 p2;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML Tue Nov 21 20:58:15 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML Wed Nov 22 10:20:09 2006 +0100
@@ -5,7 +5,7 @@
struct
fun lookup ((k, v) :: xs) l =
- (if (k : string = l) then SOME v else lookup xs l)
+ (if ((k : string) = l) then SOME v else lookup xs l)
| lookup [] l = NONE;
end; (*struct Codegen*)
Binary file doc-src/IsarAdvanced/Codegen/codegen_process.pdf has changed
--- a/doc-src/IsarAdvanced/Codegen/codegen_process.ps Tue Nov 21 20:58:15 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/codegen_process.ps Wed Nov 22 10:20:09 2006 +0100
@@ -3,7 +3,7 @@
%%For: (haftmann) Florian Haftmann
%%Title: _anonymous_0
%%Pages: (atend)
-%%BoundingBox: 35 35 417 289
+%%BoundingBox: 35 35 451 291
%%EndComments
save
%%BeginProlog
@@ -230,39 +230,43 @@
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 417 289
+%%PageBoundingBox: 36 36 451 291
%%PageOrientation: Portrait
gsave
-35 35 382 254 boxprim clip newpath
+35 35 416 256 boxprim clip newpath
36 36 translate
0 0 1 beginpage
0 0 translate 0 rotate
-[ /CropBox [36 36 417 289] /PAGES pdfmark
+[ /CropBox [36 36 451 291] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
% theory
gsave 10 dict begin
-newpath 57 252 moveto
-3 252 lineto
-3 216 lineto
-57 216 lineto
+newpath 93 254 moveto
+1 254 lineto
+1 214 lineto
+93 214 lineto
closepath
stroke
gsave 10 dict begin
-11 229 moveto
-(theory)
-[4.08 6.96 6.24 6.96 4.8 6.96]
+8 237 moveto
+(Isabelle/HOL)
+[4.56 5.52 6.24 6.96 6.24 3.84 3.84 6.24 3.84 10.08 10.08 8.64]
+xshow
+16 221 moveto
+(Isar theory)
+[4.56 5.52 6.24 4.56 3.6 4.08 6.96 6.24 6.96 4.8 6.96]
xshow
end grestore
end grestore
% selection
gsave 10 dict begin
-149 234 38 18 ellipse_path
+183 234 38 18 ellipse_path
stroke
gsave 10 dict begin
-124 229 moveto
+158 229 moveto
(selection)
[5.52 6.24 3.84 6.24 6.24 3.84 3.84 6.96 6.96]
xshow
@@ -270,36 +274,36 @@
end grestore
% theory -> selection
-newpath 57 234 moveto
-70 234 86 234 101 234 curveto
+newpath 94 234 moveto
+107 234 121 234 135 234 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
-newpath 101 238 moveto
-111 234 lineto
-101 231 lineto
+newpath 135 238 moveto
+145 234 lineto
+135 231 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-newpath 101 238 moveto
-111 234 lineto
-101 231 lineto
+newpath 135 238 moveto
+145 234 lineto
+135 231 lineto
closepath
stroke
end grestore
% sml
gsave 10 dict begin
-newpath 57 144 moveto
-3 144 lineto
-3 108 lineto
-57 108 lineto
+newpath 74 144 moveto
+20 144 lineto
+20 108 lineto
+74 108 lineto
closepath
stroke
gsave 10 dict begin
-15 121 moveto
+32 121 moveto
(SML)
[7.68 12.48 8.64]
xshow
@@ -309,7 +313,7 @@
% other
gsave 10 dict begin
gsave 10 dict begin
-24 67 moveto
+41 67 moveto
(...)
[3.6 3.6 3.6]
xshow
@@ -318,14 +322,14 @@
% haskell
gsave 10 dict begin
-newpath 60 36 moveto
-0 36 lineto
-0 0 lineto
-60 0 lineto
+newpath 77 36 moveto
+17 36 lineto
+17 0 lineto
+77 0 lineto
closepath
stroke
gsave 10 dict begin
-8 13 moveto
+25 13 moveto
(Haskell)
[10.08 6.24 5.52 6.72 6.24 3.84 3.84]
xshow
@@ -334,10 +338,10 @@
% preprocessing
gsave 10 dict begin
-149 180 52 18 ellipse_path
+183 180 52 18 ellipse_path
stroke
gsave 10 dict begin
-109 175 moveto
+143 175 moveto
(preprocessing)
[6.96 4.56 6.24 6.96 4.56 6.96 6.24 6.24 5.52 5.52 3.84 6.96 6.96]
xshow
@@ -345,36 +349,36 @@
end grestore
% selection -> preprocessing
-newpath 149 216 moveto
-149 213 149 211 149 208 curveto
+newpath 183 216 moveto
+183 213 183 211 183 208 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
-newpath 153 208 moveto
-149 198 lineto
-146 208 lineto
+newpath 187 208 moveto
+183 198 lineto
+180 208 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-newpath 153 208 moveto
-149 198 lineto
-146 208 lineto
+newpath 187 208 moveto
+183 198 lineto
+180 208 lineto
closepath
stroke
end grestore
% code_thm
gsave 10 dict begin
-newpath 358 198 moveto
-260 198 lineto
-260 162 lineto
-358 162 lineto
+newpath 392 198 moveto
+294 198 lineto
+294 162 lineto
+392 162 lineto
closepath
stroke
gsave 10 dict begin
-268 175 moveto
+302 175 moveto
(code theorems)
[6.24 6.96 6.96 6.24 3.6 4.08 6.96 6.24 6.96 4.56 6.24 10.8 5.52]
xshow
@@ -382,32 +386,32 @@
end grestore
% preprocessing -> code_thm
-newpath 202 180 moveto
-218 180 234 180 250 180 curveto
+newpath 236 180 moveto
+252 180 268 180 284 180 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
-newpath 250 184 moveto
-260 180 lineto
-250 177 lineto
+newpath 284 184 moveto
+294 180 lineto
+284 177 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-newpath 250 184 moveto
-260 180 lineto
-250 177 lineto
+newpath 284 184 moveto
+294 180 lineto
+284 177 lineto
closepath
stroke
end grestore
% serialization
gsave 10 dict begin
-149 72 47 18 ellipse_path
+183 72 47 18 ellipse_path
stroke
gsave 10 dict begin
-114 67 moveto
+148 67 moveto
(serialization)
[5.52 6.24 4.8 3.84 6.24 3.84 3.84 6.24 6.24 3.84 3.84 6.96 6.96]
xshow
@@ -415,22 +419,22 @@
end grestore
% serialization -> sml
-newpath 118 86 moveto
-102 94 83 102 66 110 curveto
+newpath 150 85 moveto
+129 93 104 103 83 111 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
-newpath 65 107 moveto
-57 114 lineto
-68 113 lineto
+newpath 82 108 moveto
+74 115 lineto
+85 114 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-newpath 65 107 moveto
-57 114 lineto
-68 113 lineto
+newpath 82 108 moveto
+74 115 lineto
+85 114 lineto
closepath
stroke
end grestore
@@ -438,54 +442,54 @@
% serialization -> other
gsave 10 dict begin
dotted
-newpath 101 72 moveto
-90 72 78 72 67 72 curveto
+newpath 135 72 moveto
+119 72 100 72 84 72 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
-newpath 67 69 moveto
-57 72 lineto
-67 76 lineto
+newpath 84 69 moveto
+74 72 lineto
+84 76 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-newpath 67 69 moveto
-57 72 lineto
-67 76 lineto
+newpath 84 69 moveto
+74 72 lineto
+84 76 lineto
closepath
stroke
end grestore
end grestore
% serialization -> haskell
-newpath 118 58 moveto
-103 51 85 43 69 36 curveto
+newpath 150 59 moveto
+131 51 107 42 86 34 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
-newpath 71 33 moveto
-60 32 lineto
-68 39 lineto
+newpath 88 31 moveto
+77 30 lineto
+85 37 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-newpath 71 33 moveto
-60 32 lineto
-68 39 lineto
+newpath 88 31 moveto
+77 30 lineto
+85 37 lineto
closepath
stroke
end grestore
% extraction
gsave 10 dict begin
-309 126 41 18 ellipse_path
+343 126 41 18 ellipse_path
stroke
gsave 10 dict begin
-281 121 moveto
+315 121 moveto
(extraction)
[5.76 6.96 3.84 4.56 6.24 6.24 3.84 3.84 6.96 6.96]
xshow
@@ -493,36 +497,36 @@
end grestore
% code_thm -> extraction
-newpath 309 162 moveto
-309 159 309 157 309 154 curveto
+newpath 343 162 moveto
+343 159 343 157 343 154 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
-newpath 313 154 moveto
-309 144 lineto
-306 154 lineto
+newpath 347 154 moveto
+343 144 lineto
+340 154 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-newpath 313 154 moveto
-309 144 lineto
-306 154 lineto
+newpath 347 154 moveto
+343 144 lineto
+340 154 lineto
closepath
stroke
end grestore
% iml
gsave 10 dict begin
-newpath 379 90 moveto
-239 90 lineto
-239 54 lineto
-379 54 lineto
+newpath 413 90 moveto
+273 90 lineto
+273 54 lineto
+413 54 lineto
closepath
stroke
gsave 10 dict begin
-246 67 moveto
+280 67 moveto
(intermediate language)
[3.84 6.96 3.84 6.24 4.8 10.8 6.24 6.96 3.84 6.24 3.84 6.24 3.6 3.84 6.24 6.96 6.96 6.96 6.24 6.72 6.24]
xshow
@@ -530,43 +534,43 @@
end grestore
% extraction -> iml
-newpath 309 108 moveto
-309 105 309 103 309 100 curveto
+newpath 343 108 moveto
+343 105 343 103 343 100 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
-newpath 313 100 moveto
-309 90 lineto
-306 100 lineto
+newpath 347 100 moveto
+343 90 lineto
+340 100 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-newpath 313 100 moveto
-309 90 lineto
-306 100 lineto
+newpath 347 100 moveto
+343 90 lineto
+340 100 lineto
closepath
stroke
end grestore
% iml -> serialization
-newpath 238 72 moveto
-228 72 217 72 207 72 curveto
+newpath 272 72 moveto
+262 72 251 72 241 72 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
-newpath 207 69 moveto
-197 72 lineto
-207 76 lineto
+newpath 241 69 moveto
+231 72 lineto
+241 76 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-newpath 207 69 moveto
-197 72 lineto
-207 76 lineto
+newpath 241 69 moveto
+231 72 lineto
+241 76 lineto
closepath
stroke
end grestore