path: root/doc/kernel.dep.ps

%!PS-Adobe-2.0
%%Creator: dot version 1.7.16 (Wed Feb  6 02:14:52 MST 2002)
%%For: (filliatr) Jean-Christophe Filliatre
%%Title: G
%%Pages: (atend)
%%BoundingBox: 35 35 577 88
%%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
/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 { } 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

/layercolorseq
	[	% layer color sequence - darkest to lightest
		[0 0 0]
		[.2 .8 .8]
		[.4 .8 .8]
		[.6 .8 .8]
		[.8 .8 .8]
	]
def

/setlayer {/maxlayer exch def /curlayer exch def
	layercolorseq curlayer 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 577 88
%%PageOrientation: Portrait
gsave
35 35 542 53 boxprim clip newpath
36 36 translate
0 0 1 beginpage
0.2736 set_scale
0 0 translate 0 rotate
[ /CropBox [36 36 577 88] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font

%	Univ
gsave 10 dict begin
1826 172 28 18 ellipse_path
stroke
gsave 10 dict begin
1826 167 moveto 35 -0.5 (Univ) alignedtext
end grestore
end grestore

%	Names
gsave 10 dict begin
1931 172 35 18 ellipse_path
stroke
gsave 10 dict begin
1931 167 moveto 48 -0.5 (Names) alignedtext
end grestore
end grestore

%	Univ -> Names
newpath 1855 172 moveto
1865 172 1875 172 1886 172 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1886 170 moveto
1896 172 lineto
1886 175 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Typeops
gsave 10 dict begin
613 149 40 18 ellipse_path
stroke
gsave 10 dict begin
613 144 moveto 58 -0.5 (Typeops) alignedtext
end grestore
end grestore

%	Entries
gsave 10 dict begin
872 168 35 18 ellipse_path
stroke
gsave 10 dict begin
872 163 moveto 48 -0.5 (Entries) alignedtext
end grestore
end grestore

%	Typeops -> Entries
newpath 653 152 moveto
701 155 781 161 830 165 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 827 163 moveto
837 165 lineto
827 168 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Inductive
gsave 10 dict begin
739 72 43 18 ellipse_path
stroke
gsave 10 dict begin
739 67 moveto 64 -0.5 (Inductive) alignedtext
end grestore
end grestore

%	Typeops -> Inductive
newpath 637 134 moveto
657 122 685 105 706 92 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 704 90 moveto
714 87 lineto
707 94 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Sign
gsave 10 dict begin
1633 145 27 18 ellipse_path
stroke
gsave 10 dict begin
1633 140 moveto 30 -0.5 (Sign) alignedtext
end grestore
end grestore

%	Entries -> Sign
newpath 907 168 moveto
976 168 1124 167 1147 168 curveto
1147 168 1147 168 1387 168 curveto
1462 167 1549 157 1597 150 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1597 148 moveto
1607 149 lineto
1597 152 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Type_errors
gsave 10 dict begin
872 72 53 18 ellipse_path
stroke
gsave 10 dict begin
872 67 moveto 85 -0.5 (Type_errors) alignedtext
end grestore
end grestore

%	Inductive -> Type_errors
newpath 782 72 moveto
791 72 799 72 808 72 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 808 70 moveto
818 72 lineto
808 75 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Reduction
gsave 10 dict begin
1009 72 46 18 ellipse_path
stroke
gsave 10 dict begin
1009 67 moveto 71 -0.5 (Reduction) alignedtext
end grestore
end grestore

%	Type_errors -> Reduction
newpath 926 72 moveto
935 72 943 72 952 72 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 952 70 moveto
962 72 lineto
952 75 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Conv_oracle
gsave 10 dict begin
1147 74 55 18 ellipse_path
stroke
gsave 10 dict begin
1147 69 moveto 88 -0.5 (Conv_oracle) alignedtext
end grestore
end grestore

%	Reduction -> Conv_oracle
newpath 1056 73 moveto
1065 73 1073 73 1082 73 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1082 71 moveto
1092 73 lineto
1082 76 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Term_typing
gsave 10 dict begin
355 95 57 18 ellipse_path
stroke
gsave 10 dict begin
355 90 moveto 92 -0.5 (Term_typing) alignedtext
end grestore
end grestore

%	Cooking
gsave 10 dict begin
489 95 40 18 ellipse_path
stroke
gsave 10 dict begin
489 90 moveto 58 -0.5 (Cooking) alignedtext
end grestore
end grestore

%	Term_typing -> Cooking
newpath 412 95 moveto
421 95 430 95 439 95 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 439 93 moveto
449 95 lineto
439 98 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Indtypes
gsave 10 dict begin
489 149 40 18 ellipse_path
stroke
gsave 10 dict begin
489 144 moveto 59 -0.5 (Indtypes) alignedtext
end grestore
end grestore

%	Term_typing -> Indtypes
newpath 390 109 moveto
409 117 432 126 451 134 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 451 131 moveto
459 137 lineto
449 136 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Cooking -> Reduction
newpath 511 80 moveto
532 66 560 47 566 45 curveto
720 0 768 20 926 45 curveto
935 47 951 52 968 58 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 966 55 moveto
975 60 lineto
965 60 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Indtypes -> Typeops
newpath 530 149 moveto
541 149 552 149 563 149 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 563 147 moveto
573 149 lineto
563 152 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Term
gsave 10 dict begin
1726 145 30 18 ellipse_path
stroke
gsave 10 dict begin
1726 140 moveto 38 -0.5 (Term) alignedtext
end grestore
end grestore

%	Term -> Univ
newpath 1754 152 moveto
1765 155 1779 159 1791 162 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1791 159 moveto
1800 165 lineto
1790 164 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Esubst
gsave 10 dict begin
1826 118 33 18 ellipse_path
stroke
gsave 10 dict begin
1826 113 moveto 45 -0.5 (Esubst) alignedtext
end grestore
end grestore

%	Term -> Esubst
newpath 1754 138 moveto
1764 135 1776 132 1787 129 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1786 127 moveto
1796 126 lineto
1787 132 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Subtyping
gsave 10 dict begin
613 72 46 18 ellipse_path
stroke
gsave 10 dict begin
613 67 moveto 71 -0.5 (Subtyping) alignedtext
end grestore
end grestore

%	Subtyping -> Inductive
newpath 660 72 moveto
669 72 677 72 686 72 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 686 70 moveto
696 72 lineto
686 75 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Modops
gsave 10 dict begin
739 126 38 18 ellipse_path
stroke
gsave 10 dict begin
739 121 moveto 55 -0.5 (Modops) alignedtext
end grestore
end grestore

%	Subtyping -> Modops
newpath 644 85 moveto
662 93 684 102 702 110 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 703 108 moveto
711 114 lineto
701 112 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Modops -> Entries
newpath 771 136 moveto
790 142 814 150 833 156 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 833 153 moveto
842 159 lineto
832 158 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Environ
gsave 10 dict begin
1387 122 39 18 ellipse_path
stroke
gsave 10 dict begin
1387 117 moveto 56 -0.5 (Environ) alignedtext
end grestore
end grestore

%	Modops -> Environ
newpath 777 125 moveto
830 124 926 122 1009 122 curveto
1009 122 1009 122 1147 122 curveto
1152 122 1270 122 1339 122 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1338 120 moveto
1348 122 lineto
1338 125 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Sign -> Term
newpath 1660 145 moveto
1668 145 1677 145 1686 145 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1686 143 moveto
1696 145 lineto
1686 148 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Safe_typing
gsave 10 dict begin
62 72 53 18 ellipse_path
stroke
gsave 10 dict begin
62 67 moveto 85 -0.5 (Safe_typing) alignedtext
end grestore
end grestore

%	Mod_typing
gsave 10 dict begin
207 72 54 18 ellipse_path
stroke
gsave 10 dict begin
207 67 moveto 87 -0.5 (Mod_typing) alignedtext
end grestore
end grestore

%	Safe_typing -> Mod_typing
newpath 116 72 moveto
125 72 133 72 142 72 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 142 70 moveto
152 72 lineto
142 75 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Mod_typing -> Term_typing
newpath 257 80 moveto
269 82 282 84 294 86 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 294 84 moveto
304 87 lineto
294 88 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Mod_typing -> Subtyping
newpath 261 69 moveto
273 69 286 68 298 68 curveto
402 66 427 66 530 68 curveto
536 68 547 69 559 69 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 557 66 moveto
567 70 lineto
557 71 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Closure
gsave 10 dict begin
1275 75 37 18 ellipse_path
stroke
gsave 10 dict begin
1275 70 moveto 52 -0.5 (Closure) alignedtext
end grestore
end grestore

%	Conv_oracle -> Closure
newpath 1202 74 moveto
1211 74 1220 75 1228 75 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1228 73 moveto
1238 75 lineto
1228 78 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Declarations
gsave 10 dict begin
1516 122 53 18 ellipse_path
stroke
gsave 10 dict begin
1516 117 moveto 85 -0.5 (Declarations) alignedtext
end grestore
end grestore

%	Environ -> Declarations
newpath 1426 122 moveto
1434 122 1443 122 1452 122 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1452 120 moveto
1462 122 lineto
1452 125 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Declarations -> Sign
newpath 1562 131 moveto
1574 133 1587 136 1598 138 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1598 135 moveto
1607 140 lineto
1597 140 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Closure -> Environ
newpath 1303 87 moveto
1317 93 1334 100 1349 106 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1350 104 moveto
1358 110 lineto
1348 108 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
endpage
grestore
%%PageTrailer
%%EndPage: 1
%%Trailer
%%Pages: 1
end
restore
%%EOF