# HG changeset patch # User haftmann # Date 1162715785 -3600 # Node ID c3618fc6a6f752bdfa87c3d713822376b479fe6d # Parent e8228486aa03335d181562e37ed5a76ee4c5e177 added gfx diff -r e8228486aa03 -r c3618fc6a6f7 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Sat Nov 04 19:25:43 2006 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Sun Nov 05 09:36:25 2006 +0100 @@ -57,7 +57,7 @@ in most cases while allowing for detailed customization. This manifests in the structure of this tutorial: this introduction continues with a short introduction of concepts. Section - \secref{sec:basics} explains how to use the framework naivly, + \secref{sec:basics} explains how to use the framework naively, presuming a reasonable default setup. Then, section \secref{sec:advanced} deals with advanced topics, introducing further aspects of the code generator framework @@ -152,15 +152,15 @@ code_gen fac (SML "examples/fac.ML") text {* - The \isasymCODEGEN command takes a space-seperated list of + The \isasymCODEGEN command takes a space-separated list of constants together with \qn{serialization directives} in parentheses. These start with a \qn{target language} - identifer, followed by arguments, their semantics + identifier, followed by arguments, their semantics depending on the target. In the SML case, a filename is given where to write the generated code to. Internally, the function equations for all selected - constants are taken, including any tranitivly required + constants are taken, including any transitively required constants, datatypes and classes, resulting in the following code: @@ -237,7 +237,7 @@ function equations (the additional stuff displayed shall not bother us for the moment). If this table does not provide at least one function - equation, the table of primititve definitions is searched + equation, the table of primitive definitions is searched whether it provides one. The typical HOL tools are already set up in a way that @@ -318,9 +318,9 @@ here we just illustrate its impact on code generation. In a target language, type classes may be represented - nativly (as in the case of Haskell). For languages + natively (as in the case of Haskell). For languages like SML, they are implemented using \emph{dictionaries}. - Our following example specifiedsa class \qt{null}, + Our following example specifies a class \qt{null}, assigning to each of its inhabitants a \qt{null} value: *} @@ -352,7 +352,7 @@ "dummy = head [Some (Suc 0), None]" text {* - Type classes offer a suitable occassion to introduce + Type classes offer a suitable occasion to introduce the Haskell serializer. Its usage is almost the same as SML, but, in accordance with conventions some Haskell systems enforce, each module ends @@ -404,7 +404,7 @@ \noindent print all cached function equations (i.e.~\emph{after} any applied transformation. Inside the brackets a list of constants may be given; their function - euqations are added to the cache if not already present. + equations are added to the cache if not already present. *} @@ -434,7 +434,7 @@ which should be suitable for most applications. Common extensions and modifications are available by certain theories of the HOL library; beside being useful in applications, they may serve - as a tutorial for cutomizing the code generator setup. + as a tutorial for customizing the code generator setup. \begin{description} @@ -443,7 +443,7 @@ \item[ExecutableRat] implements rational numbers as triples @{text "(sign, enumerator, denominator)"}. \item[EfficientNat] implements natural numbers by integers, - which in geneal will result in higher efficency; pattern + which in general will result in higher efficency; pattern matching with @{const "0\nat"} / @{const "Suc"} is eliminated. \label{eff_nat} \item[MLString] provides an additional datatype @{text "mlstring"}; @@ -459,7 +459,7 @@ text {* Before selected function theorems are turned into abstract code, a chain of definitional transformation steps is carried - out: \emph{preprocessing}. There are three possibilites + out: \emph{preprocessing}. There are three possibilities to customize preprocessing: \emph{inline theorems}, \emph{inline procedures} and \emph{generic preprocessors}. @@ -469,7 +469,7 @@ hand side and the arguments of the left hand side of an equation, but never to the constant heading the left hand side. Inline theorems may be declared an undeclared using the - \emph{code inline} or \emph{code noinline} attribute respectivly. + \emph{code inline} or \emph{code noinline} attribute respectively. Some common applications: *} @@ -521,7 +521,7 @@ \begin{warn} The order in which single preprocessing steps are carried out currently is not specified; in particular, preprocessing - is \emph{no} fixpoint process. Keep this in mind when + is \emph{no} fix point process. Keep this in mind when setting up the preprocessor. Further, the attribute \emph{code unfold} @@ -601,7 +601,7 @@ \lstsml{Thy/examples/bool2.ML} This still is not perfect: the parentheses - around \qt{andalso} are superfluos. Though the serializer + around \qt{andalso} are superfluous. Though the serializer by no means attempts to imitate the rich Isabelle syntax framework, it provides some common idioms, notably associative infixes with precedences which may be used here: @@ -641,30 +641,59 @@ inserts a space which may be used as a break if necessary during pretty printing. - So far, + So far, we did only provide more idiomatic serializations for + constructs which would be executable on their own. Target-specific + serializations may also be used to \emph{implement} constructs + which have no implicit notion of executability. For example, + take the HOL integers: +*} + +definition + double_inc :: "int \ int" + "double_inc k = 2 * k + 1" + +code_gen double_inc (SML "examples/integers.ML") + +text {* + will fail: @{typ int} in HOL is implemented using a quotient + type, which does not provide any notion of executability. + \footnote{Eventually, we also want to provide executability + for quotients.}. However, we could use the SML builtin + integers: *} code_type int (SML "IntInf.int") - (Haskell "Integer") code_const "op + \ int \ int \ int" - and "op - \ int \ int \ int" and "op * \ int \ int \ int" - (SML "IntInf.+ (_, _)" and "IntInf.- (_, _)" and "IntInf.* (_, _)") - (Haskell infixl 6 "+" and infixl 6 "-" and infixl 7 "*") + (SML "IntInf.+ (_, _)" and "IntInf.* (_, _)") + +code_gen double_inc (SML "examples/integers.ML") -(* quote with ' HOL Setup, careful *) +text {* + resulting in: + \lstsml{Thy/examples/integers.ML} +*} -(* Better ops, code_moduleprolog *) -(* code_modulename *) - +text {* + These examples give a glimpse what powerful mechanisms + custom serializations provide; however their usage + requires careful thinking in order not to introduce + inconsistencies -- or, in other words: + custom serializations are completely axiomatic. -subsection {* Types matter *} + A further noteworthy details is that any special + character in a custom serialization may be quoted + using \qt{'}; thus, in \qt{fn '\_ => \_} the first + \qt{'\_} is a proper underscore while the + second \qt{\_} is a placeholder. -(* shadowing by user-defined serilizations, understanding the type game, -reflexive equations, dangerous equations *) + The HOL theories provide further + examples for custom serializations and form + a recommended tutorial on how to use them properly. +*} subsection {* Concerning operational equality *} @@ -687,7 +716,7 @@ (*>*) text {* - The membership test during preprocessing is rewritting, + The membership test during preprocessing is rewriting, resulting in @{const List.memberl}, which itself performs an explicit equality check. *} @@ -712,7 +741,7 @@ fixes eq :: "'a \ 'a \ bool" defs - eq [symmetric(*, code inline, code func*)]: "eq \ (op =)" + eq (*[symmetric, code inline, code func]*): "eq \ (op =)" text {* This merely introduces a class @{text eq} with corresponding @@ -739,30 +768,31 @@ are some cases when it suddenly comes to surface: *} -text_raw {* - \begin {description} - \item[code lemmas and customary serializations for equality] - Examine the following: \\ +subsubsection {* code lemmas and customary serializations for equality *} + +text {* + Examine the following: *} code_const "op = \ int \ int \ bool" (SML "!(_ : IntInf.int = _)") -text_raw {* - \\ What is wrong here? Since @{const "op ="} is nothing else then +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"}: \\ + by using the overloaded constant @{const "Code_Generator.eq"}: *} code_const "Code_Generator.eq \ int \ int \ bool" (SML "!(_ : IntInf.int = _)") -text_raw {* - \\ \item[typedecls interpretated by customary serializations] A - common idiom is to use unspecified types for formalizations - and interpret them for a specific target language: \\ +subsubsection {* typedecls interpretated by customary serializations *} + +text {* + A common idiom is to use unspecified types for formalizations + and interpret them for a specific target language: *} typedecl key @@ -779,11 +809,11 @@ code_type key (SML "string") -text_raw {* - \\ This, though, is not sufficient: @{typ key} is no instance +text {* + 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 "Code_Generator.eq"}: *} instance key :: eq .. @@ -791,8 +821,8 @@ code_const "Code_Generator.eq \ key \ key \ bool" (SML "!(_ : string = _)") -text_raw {* - \\ Then everything goes fine: \\ +text {* + Then everything goes fine: *} code_gen lookup (SML "examples/lookup.ML") @@ -801,48 +831,52 @@ \lstsml{Thy/examples/lookup.ML} *} -text_raw {* - \item[lexicographic orderings and corregularity] Another sublety +subsubsection {* lexicographic orderings and coregularity *} + +text {* + Another subtlety enters the stage when definitions of overloaded constants are dependent on operational equality. For example, let us define a lexicographic ordering on tuples: \\ *} (*<*) -(*setup {* Sign.add_path "foo" *} +setup {* Sign.add_path "foobar" *} -class ord = ord*) +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) (*>*) -(* -instance * :: ("{eq, ord}", ord) ord - "p1 < p2 \ let (x1, y1) = p1; (x2, y2) = p2 in +instance * :: (ord, ord) ord + "p1 < p2 \ let (x1 \ 'a\ord, y1 \ 'b\ord) = p1; (x2, y2) = p2 in x1 < x2 \ (x1 = x2 \ y1 < y2)" - "p1 \ p2 \ p1 < p2 \ p1 = p2" .. -*) + "p1 \ p2 \ p1 < p2 \ (p1 \ 'a\ord \ 'b\ord) = p2" .. (*<*) -(*hide (open) "class" ord -setup {* Sign.parent_path *}*) +hide "class" eq ord +hide const eq less_eq less +setup {* Sign.parent_path *} (*>*) -text_raw {* - \\ Then code generation will fail. Why? The definition +text {* + Then code generation will fail. Why? The definition of @{const "op \"} depends on equality on both arguments, - which are polymorhpic and impose an additional @{text eq} + which are polymorphic and impose an additional @{text eq} class constraint, thus violating the type discipline for class operations. - The solution is to add @{text eq} to both sort arguments: \\ + The solution is to add @{text eq} to both sort arguments: *} instance * :: ("{eq, ord}", "{eq, ord}") ord - "p1 < p2 \ let (x1, y1) = p1; (x2, y2) = p2 in + "p1 < p2 \ let (x1 \ 'a\{eq, ord}, y1 \ 'b\{eq, ord}) = p1; (x2, y2) = p2 in x1 < x2 \ (x1 = x2 \ y1 < y2)" - "p1 \ p2 \ p1 < p2 \ p1 = p2" .. + "p1 \ p2 \ p1 < p2 \ (p1 \ 'a\{eq, ord} \ 'b\{eq, ord}) = p2" .. -text_raw {* - \\ Then code generation succeeds: \\ +text {* + Then code generation succeeds: *} code_gen "op \ \ 'a\{eq, ord} \ 'b\{eq, ord} \ 'a \ 'b \ bool" @@ -852,14 +886,80 @@ \lstsml{Thy/examples/lexicographic.ML} *} -text_raw {* - \item[Haskell serialization] +subsubsection {* Haskell serialization *} + +text {* + For convenience, the default + HOL setup for Haskell maps the @{text eq} class to + its counterpart in Haskell, giving custom serializations + for the class (\isasymCODECLASS) and its operation: +*} + +(*<*) +setup {* Sign.add_path "bar" *} +class eq = fixes eq :: "'a \ 'a \ bool" +(*>*) + +code_class eq + (Haskell "Eq" where eq \ "(==)") + +code_const eq + (Haskell infixl 4 "==") + +(*<*) +hide "class" eq +hide const eq +setup {* Sign.parent_path *} +(*>*) + +text {* + A problem now occurs whenever a type which + is an instance of @{text eq} in HOL is mapped + on a Haskell-builtin type which is also an instance + of Haskell @{text Eq}: *} -text_raw {* - \end {description} +typedecl bar + +instance bar :: eq .. + +code_type bar + (Haskell "Integer") + +text {* + The code generator would produce + an additional instance, which of course is rejected. + To suppress this additional instance, use + \isasymCODEINSTANCE: *} +code_instance bar :: eq + (Haskell -) + +subsection {* Types matter *} + +text {* + Imagine the following quick-and-dirty setup for implementing + some sets as lists: +*} + +code_type set + (SML "_ list") + +code_const "{}" and insert + (SML "![]" and infixl 7 "::") + +definition + dummy_set :: "nat set" + "dummy_set = {1, 2, 3}" + +(*print_codethms (dummy_set) +code_gen dummy_set (SML -)*) + + +(* shadowing by user-defined serializations, understanding the type game, +reflexive equations, dangerous equations *) + subsection {* Axiomatic extensions *} @@ -871,6 +971,7 @@ \end{warn} *} +(* code_modulename *) (* existing libraries, code inline code_constsubst, code_abstype*) section {* ML interfaces \label{sec:ml} *} diff -r e8228486aa03 -r c3618fc6a6f7 doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML Sun Nov 05 09:36:25 2006 +0100 @@ -0,0 +1,12 @@ +structure ROOT = +struct + +structure Codegen = +struct + +fun double_inc a = + IntInf.+ ((IntInf.* ((2 : IntInf.int), a)), (1 : IntInf.int)); + +end; (*struct Codegen*) + +end; (*struct ROOT*) diff -r e8228486aa03 -r c3618fc6a6f7 doc-src/IsarAdvanced/Codegen/codegen_process.eps --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/codegen_process.eps Sun Nov 05 09:36:25 2006 +0100 @@ -0,0 +1,582 @@ +%!PS-Adobe-2.0 +%%Creator: dot version 2.2 (Tue Mar 22 18:02:44 UTC 2005) +%%For: (haftmann) Florian Haftmann +%%Title: _anonymous_0 +%%Pages: (atend) +%%BoundingBox: 35 35 241 577 +%%EndComments +save +%%BeginProlog +/DotDict 200 dict def +DotDict begin + +/setupLatin1 { +mark +/EncodingVector 256 array def + EncodingVector 0 + +ISOLatin1Encoding 0 255 getinterval putinterval + +EncodingVector + dup 306 /AE + dup 301 /Aacute + dup 302 /Acircumflex + dup 304 /Adieresis + dup 300 /Agrave + dup 305 /Aring + dup 303 /Atilde + dup 307 /Ccedilla + dup 311 /Eacute + dup 312 /Ecircumflex + dup 313 /Edieresis + dup 310 /Egrave + dup 315 /Iacute + dup 316 /Icircumflex + dup 317 /Idieresis + dup 314 /Igrave + dup 334 /Udieresis + dup 335 /Yacute + dup 376 /thorn + dup 337 /germandbls + dup 341 /aacute + dup 342 /acircumflex + dup 344 /adieresis + dup 346 /ae + dup 340 /agrave + dup 345 /aring + dup 347 /ccedilla + dup 351 /eacute + dup 352 /ecircumflex + dup 353 /edieresis + dup 350 /egrave + dup 355 /iacute + dup 356 /icircumflex + dup 357 /idieresis + dup 354 /igrave + dup 360 /dcroat + dup 361 /ntilde + dup 363 /oacute + dup 364 /ocircumflex + dup 366 /odieresis + dup 362 /ograve + dup 365 /otilde + dup 370 /oslash + dup 372 /uacute + dup 373 /ucircumflex + dup 374 /udieresis + dup 371 /ugrave + dup 375 /yacute + dup 377 /ydieresis + +% Set up ISO Latin 1 character encoding +/starnetISO { + dup dup findfont dup length dict begin + { 1 index /FID ne { def }{ pop pop } ifelse + } forall + /Encoding EncodingVector def + currentdict end definefont +} def +/Times-Roman starnetISO def +/Times-Italic starnetISO def +/Times-Bold starnetISO def +/Times-BoldItalic starnetISO def +/Helvetica starnetISO def +/Helvetica-Oblique starnetISO def +/Helvetica-Bold starnetISO def +/Helvetica-BoldOblique starnetISO def +/Courier starnetISO def +/Courier-Oblique starnetISO def +/Courier-Bold starnetISO def +/Courier-BoldOblique starnetISO def +cleartomark +} bind def + +%%BeginResource: procset graphviz 0 0 +/coord-font-family /Times-Roman def +/default-font-family /Times-Roman def +/coordfont coord-font-family findfont 8 scalefont def + +/InvScaleFactor 1.0 def +/set_scale { + dup 1 exch div /InvScaleFactor exch def + dup scale +} bind def + +% styles +/solid { [] 0 setdash } bind def +/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def +/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def +/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def +/bold { 2 setlinewidth } bind def +/filled { } bind def +/unfilled { } bind def +/rounded { } bind def +/diagonals { } bind def + +% hooks for setting color +/nodecolor { sethsbcolor } bind def +/edgecolor { sethsbcolor } bind def +/graphcolor { sethsbcolor } bind def +/nopcolor {pop pop pop} bind def + +/beginpage { % i j npages + /npages exch def + /j exch def + /i exch def + /str 10 string def + npages 1 gt { + gsave + coordfont setfont + 0 0 moveto + (\() show i str cvs show (,) show j str cvs show (\)) show + grestore + } if +} bind def + +/set_font { + findfont exch + scalefont setfont +} def + +% draw aligned label in bounding box aligned to current point +/alignedtext { % width adj text + /text exch def + /adj exch def + /width exch def + gsave + width 0 gt { + text stringwidth pop adj mul 0 rmoveto + } if + [] 0 setdash + text show + grestore +} def + +/boxprim { % xcorner ycorner xsize ysize + 4 2 roll + moveto + 2 copy + exch 0 rlineto + 0 exch rlineto + pop neg 0 rlineto + closepath +} bind def + +/ellipse_path { + /ry exch def + /rx exch def + /y exch def + /x exch def + matrix currentmatrix + newpath + x y translate + rx ry scale + 0 0 1 0 360 arc + setmatrix +} bind def + +/endpage { showpage } bind def +/showpage { } def + +/layercolorseq + [ % layer color sequence - darkest to lightest + [0 0 0] + [.2 .8 .8] + [.4 .8 .8] + [.6 .8 .8] + [.8 .8 .8] + ] +def + +/layerlen layercolorseq length def + +/setlayer {/maxlayer exch def /curlayer exch def + layercolorseq curlayer 1 sub layerlen mod get + aload pop sethsbcolor + /nodecolor {nopcolor} def + /edgecolor {nopcolor} def + /graphcolor {nopcolor} def +} bind def + +/onlayer { curlayer ne {invis} if } def + +/onlayers { + /myupper exch def + /mylower exch def + curlayer mylower lt + curlayer myupper gt + or + {invis} if +} def + +/curlayer 0 def + +%%EndResource +%%EndProlog +%%BeginSetup +14 default-font-family set_font +1 setmiterlimit +% /arrowlength 10 def +% /arrowwidth 5 def + +% make sure pdfmark is harmless for PS-interpreters other than Distiller +/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse +% make '<<' and '>>' safe on PS Level 1 devices +/languagelevel where {pop languagelevel}{1} ifelse +2 lt { + userdict (<<) cvn ([) cvn load put + userdict (>>) cvn ([) cvn load put +} if + +%%EndSetup +%%Page: 1 1 +%%PageBoundingBox: 36 36 241 577 +%%PageOrientation: Portrait +gsave +35 35 206 542 boxprim clip newpath +36 36 translate +0 0 1 beginpage +0 0 translate 0 rotate +[ /CropBox [36 36 241 577] /PAGES pdfmark +0.000 0.000 0.000 graphcolor +14.00 /Times-Roman set_font + +% theory +gsave 10 dict begin +newpath 126 540 moveto +72 540 lineto +72 504 lineto +126 504 lineto +closepath +stroke +gsave 10 dict begin +80 517 moveto +(theory) +[4.08 6.96 6.24 6.96 4.8 6.96] +xshow +end grestore +end grestore + +% selection +gsave 10 dict begin +99 450 38 18 ellipse_path +stroke +gsave 10 dict begin +74 445 moveto +(selection) +[5.52 6.24 3.84 6.24 6.24 3.84 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% theory -> selection +newpath 99 504 moveto +99 496 99 487 99 478 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 103 478 moveto +99 468 lineto +96 478 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 103 478 moveto +99 468 lineto +96 478 lineto +closepath +stroke +end grestore + +% preprocessing +gsave 10 dict begin +99 378 52 18 ellipse_path +stroke +gsave 10 dict begin +59 373 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 +end grestore +end grestore + +% selection -> preprocessing +newpath 99 432 moveto +99 424 99 415 99 406 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 103 406 moveto +99 396 lineto +96 406 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 103 406 moveto +99 396 lineto +96 406 lineto +closepath +stroke +end grestore + +% code_thm +gsave 10 dict begin +newpath 148 324 moveto +50 324 lineto +50 288 lineto +148 288 lineto +closepath +stroke +gsave 10 dict begin +58 301 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 +end grestore +end grestore + +% preprocessing -> code_thm +newpath 99 360 moveto +99 352 99 343 99 334 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 103 334 moveto +99 324 lineto +96 334 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 103 334 moveto +99 324 lineto +96 334 lineto +closepath +stroke +end grestore + +% extraction +gsave 10 dict begin +99 234 41 18 ellipse_path +stroke +gsave 10 dict begin +71 229 moveto +(extraction) +[5.76 6.96 3.84 4.56 6.24 6.24 3.84 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% code_thm -> extraction +newpath 99 288 moveto +99 280 99 271 99 262 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 103 262 moveto +99 252 lineto +96 262 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 103 262 moveto +99 252 lineto +96 262 lineto +closepath +stroke +end grestore + +% iml +gsave 10 dict begin +newpath 169 180 moveto +29 180 lineto +29 144 lineto +169 144 lineto +closepath +stroke +gsave 10 dict begin +36 157 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 +end grestore +end grestore + +% extraction -> iml +newpath 99 216 moveto +99 208 99 199 99 190 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 103 190 moveto +99 180 lineto +96 190 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 103 190 moveto +99 180 lineto +96 190 lineto +closepath +stroke +end grestore + +% serialization +gsave 10 dict begin +99 90 47 18 ellipse_path +stroke +gsave 10 dict begin +64 85 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 +end grestore +end grestore + +% iml -> serialization +newpath 99 144 moveto +99 136 99 127 99 118 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 103 118 moveto +99 108 lineto +96 118 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 103 118 moveto +99 108 lineto +96 118 lineto +closepath +stroke +end grestore + +% sml +gsave 10 dict begin +newpath 54 36 moveto +0 36 lineto +0 0 lineto +54 0 lineto +closepath +stroke +gsave 10 dict begin +12 13 moveto +(SML) +[7.68 12.48 8.64] +xshow +end grestore +end grestore + +% serialization -> sml +newpath 82 73 moveto +73 64 62 53 52 43 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 55 41 moveto +45 36 lineto +50 46 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 55 41 moveto +45 36 lineto +50 46 lineto +closepath +stroke +end grestore + +% other +gsave 10 dict begin +gsave 10 dict begin +93 13 moveto +(...) +[3.6 3.6 3.6] +xshow +end grestore +end grestore + +% serialization -> other +gsave 10 dict begin +dotted +newpath 99 72 moveto +99 64 99 55 99 46 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 103 46 moveto +99 36 lineto +96 46 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 103 46 moveto +99 36 lineto +96 46 lineto +closepath +stroke +end grestore +end grestore + +% haskell +gsave 10 dict begin +newpath 204 36 moveto +144 36 lineto +144 0 lineto +204 0 lineto +closepath +stroke +gsave 10 dict begin +152 13 moveto +(Haskell) +[10.08 6.24 5.52 6.72 6.24 3.84 3.84] +xshow +end grestore +end grestore + +% serialization -> haskell +newpath 117 73 moveto +127 64 138 53 148 43 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 150 46 moveto +155 36 lineto +145 41 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 150 46 moveto +155 36 lineto +145 41 lineto +closepath +stroke +end grestore +endpage +showpage +grestore +%%PageTrailer +%%EndPage: 1 +%%Trailer +%%Pages: 1 +end +restore +%%EOF diff -r e8228486aa03 -r c3618fc6a6f7 doc-src/IsarAdvanced/Codegen/codegen_process.pdf Binary file doc-src/IsarAdvanced/Codegen/codegen_process.pdf has changed