--- a/doc-src/IsarAdvanced/Codegen/codegen_process.ps Mon Mar 02 16:58:39 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,586 +0,0 @@
-%!PS-Adobe-2.0
-%%Creator: dot version 2.2 (Mon Sep 12 23:33:36 UTC 2005)
-%%For: (haftmann) Florian Haftmann
-%%Title: _anonymous_0
-%%Pages: (atend)
-%%BoundingBox: 35 35 451 291
-%%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 451 291
-%%PageOrientation: Portrait
-gsave
-35 35 416 256 boxprim clip newpath
-36 36 translate
-0 0 1 beginpage
-0 0 translate 0 rotate
-[ /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 93 254 moveto
-1 254 lineto
-1 214 lineto
-93 214 lineto
-closepath
-stroke
-gsave 10 dict begin
-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
-183 234 38 18 ellipse_path
-stroke
-gsave 10 dict begin
-158 229 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 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 135 238 moveto
-145 234 lineto
-135 231 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 135 238 moveto
-145 234 lineto
-135 231 lineto
-closepath
-stroke
-end grestore
-
-% sml
-gsave 10 dict begin
-newpath 74 144 moveto
-20 144 lineto
-20 108 lineto
-74 108 lineto
-closepath
-stroke
-gsave 10 dict begin
-32 121 moveto
-(SML)
-[7.68 12.48 8.64]
-xshow
-end grestore
-end grestore
-
-% other
-gsave 10 dict begin
-gsave 10 dict begin
-41 67 moveto
-(...)
-[3.6 3.6 3.6]
-xshow
-end grestore
-end grestore
-
-% haskell
-gsave 10 dict begin
-newpath 77 36 moveto
-17 36 lineto
-17 0 lineto
-77 0 lineto
-closepath
-stroke
-gsave 10 dict begin
-25 13 moveto
-(Haskell)
-[10.08 6.24 5.52 6.72 6.24 3.84 3.84]
-xshow
-end grestore
-end grestore
-
-% preprocessing
-gsave 10 dict begin
-183 180 52 18 ellipse_path
-stroke
-gsave 10 dict begin
-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
-end grestore
-end grestore
-
-% selection -> preprocessing
-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 187 208 moveto
-183 198 lineto
-180 208 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 187 208 moveto
-183 198 lineto
-180 208 lineto
-closepath
-stroke
-end grestore
-
-% def_eqn
-gsave 10 dict begin
-newpath 403 198 moveto
-283 198 lineto
-283 162 lineto
-403 162 lineto
-closepath
-stroke
-gsave 10 dict begin
-291 175 moveto
-(defining equations)
-[6.96 6.24 4.8 3.84 6.96 3.84 6.96 6.96 3.6 6.24 6.72 6.96 6.24 3.84 3.84 6.96 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-% preprocessing -> def_eqn
-newpath 236 180 moveto
-248 180 260 180 273 180 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 273 184 moveto
-283 180 lineto
-273 177 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 273 184 moveto
-283 180 lineto
-273 177 lineto
-closepath
-stroke
-end grestore
-
-% serialization
-gsave 10 dict begin
-183 72 47 18 ellipse_path
-stroke
-gsave 10 dict begin
-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
-end grestore
-end grestore
-
-% serialization -> sml
-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 82 108 moveto
-74 115 lineto
-85 114 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 82 108 moveto
-74 115 lineto
-85 114 lineto
-closepath
-stroke
-end grestore
-
-% serialization -> other
-gsave 10 dict begin
-dotted
-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 84 69 moveto
-74 72 lineto
-84 76 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 84 69 moveto
-74 72 lineto
-84 76 lineto
-closepath
-stroke
-end grestore
-end grestore
-
-% serialization -> haskell
-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 88 31 moveto
-77 30 lineto
-85 37 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 88 31 moveto
-77 30 lineto
-85 37 lineto
-closepath
-stroke
-end grestore
-
-% translation
-gsave 10 dict begin
-343 126 43 18 ellipse_path
-stroke
-gsave 10 dict begin
-313 121 moveto
-(translation)
-[3.84 4.56 6.24 6.96 5.52 3.84 6.24 3.84 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% def_eqn -> translation
-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 347 154 moveto
-343 144 lineto
-340 154 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 347 154 moveto
-343 144 lineto
-340 154 lineto
-closepath
-stroke
-end grestore
-
-% iml
-gsave 10 dict begin
-newpath 413 90 moveto
-273 90 lineto
-273 54 lineto
-413 54 lineto
-closepath
-stroke
-gsave 10 dict begin
-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
-end grestore
-end grestore
-
-% translation -> iml
-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 347 100 moveto
-343 90 lineto
-340 100 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 347 100 moveto
-343 90 lineto
-340 100 lineto
-closepath
-stroke
-end grestore
-
-% iml -> serialization
-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 241 69 moveto
-231 72 lineto
-241 76 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 241 69 moveto
-231 72 lineto
-241 76 lineto
-closepath
-stroke
-end grestore
-endpage
-showpage
-grestore
-%%PageTrailer
-%%EndPage: 1
-%%Trailer
-%%Pages: 1
-end
-restore
-%%EOF