# HG changeset patch # User haftmann # Date 1164187209 -3600 # Node ID f825e0b4d566a15e9b13bba95bb9f14528dd171d # Parent 28f1181c1a48cd98a01b155eeace5329f4f25584 final draft diff -r 28f1181c1a48 -r f825e0b4d566 doc-src/IsarAdvanced/Codegen/Makefile --- 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) diff -r 28f1181c1a48 -r f825e0b4d566 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- 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 "\"} 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 \ 1 | Suc m \ 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\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\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 \" (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 * \ int \ int \ 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 \ 'a \ bool" - -defs - eq (*[symmetric, code inline, code func]*): "eq \ (op =)" +axclass eq \ 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 = \ int \ int \ 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 = \ 'a \ 'a \ 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 \ int \ int \ 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 \ key \ key \ bool" - (SML "!(_ : string = _)") +code_const %tt "op = \ key \ key \ 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 \ 'a \ bool" class ord = fixes less_eq :: "'a \ 'a \ bool" ("(_/ \<^loc>\ _)" [50, 51] 50) fixes less :: "'a \ 'a \ bool" ("(_/ \<^loc>< _)" [50, 51] 50) @@ -860,8 +831,8 @@ "p1 \ p2 \ p1 < p2 \ (p1 \ 'a\ord \ 'b\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 \ \ 'a\{eq, ord} \ 'b\{eq, ord} \ 'a \ 'b \ 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 \ CodegenConsts.const list option \ T \ 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 \ theory"} \\ @{text "get: theory \ T"} \\ @{text "change: theory \ (T \ T) \ T"} \\ @{text "change_yield: theory \ (T \ 'a * T) \ '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 diff -r 28f1181c1a48 -r f825e0b4d566 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- 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% % diff -r 28f1181c1a48 -r f825e0b4d566 doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML --- 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*) diff -r 28f1181c1a48 -r f825e0b4d566 doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML --- 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 :: diff -r 28f1181c1a48 -r f825e0b4d566 doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML --- 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*) diff -r 28f1181c1a48 -r f825e0b4d566 doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML --- 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*) diff -r 28f1181c1a48 -r f825e0b4d566 doc-src/IsarAdvanced/Codegen/codegen_process.pdf Binary file doc-src/IsarAdvanced/Codegen/codegen_process.pdf has changed diff -r 28f1181c1a48 -r f825e0b4d566 doc-src/IsarAdvanced/Codegen/codegen_process.ps --- 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