doc-src/IsarAdvanced/Codegen/codegen_process.ps

final draft

%!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 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

%	code_thm
gsave 10 dict begin
newpath 392 198 moveto
294 198 lineto
294 162 lineto
392 162 lineto
closepath
stroke
gsave 10 dict begin
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
end grestore
end grestore

%	preprocessing -> code_thm
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 284 184 moveto
294 180 lineto
284 177 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 284 184 moveto
294 180 lineto
284 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

%	extraction
gsave 10 dict begin
343 126 41 18 ellipse_path
stroke
gsave 10 dict begin
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
end grestore
end grestore

%	code_thm -> extraction
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

%	extraction -> 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