path: root/doc/pretyping.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 159
%%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 159
%%PageOrientation: Portrait
gsave
35 35 542 124 boxprim clip newpath
36 36 translate
0 0 1 beginpage
0.3634 set_scale
0 0 translate 0 rotate
[ /CropBox [36 36 577 159] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font

%	Typing
gsave 10 dict begin
523 241 36 18 ellipse_path
stroke
gsave 10 dict begin
523 236 moveto 50 -0.5 (Typing) alignedtext
end grestore
end grestore

%	Pretype_errors
gsave 10 dict begin
898 264 62 18 ellipse_path
stroke
gsave 10 dict begin
898 259 moveto 102 -0.5 (Pretype_errors) alignedtext
end grestore
end grestore

%	Typing -> Pretype_errors
newpath 559 243 moveto
621 247 750 255 830 260 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 827 258 moveto
837 260 lineto
827 263 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Rawterm
gsave 10 dict begin
1051 114 43 18 ellipse_path
stroke
gsave 10 dict begin
1051 109 moveto 65 -0.5 (Rawterm) alignedtext
end grestore
end grestore

%	Pretype_errors -> Rawterm
newpath 939 250 moveto
946 247 954 242 960 237 curveto
983 218 979 206 996 183 curveto
1008 168 1021 151 1032 138 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1029 138 moveto
1037 131 lineto
1033 141 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Inductiveops
gsave 10 dict begin
1051 210 54 18 ellipse_path
stroke
gsave 10 dict begin
1051 205 moveto 87 -0.5 (Inductiveops) alignedtext
end grestore
end grestore

%	Pretype_errors -> Inductiveops
newpath 937 250 moveto
958 243 984 234 1005 226 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1004 224 moveto
1014 223 lineto
1005 229 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Tacred
gsave 10 dict begin
761 120 34 18 ellipse_path
stroke
gsave 10 dict begin
761 115 moveto 47 -0.5 (Tacred) alignedtext
end grestore
end grestore

%	Cbv
gsave 10 dict begin
1200 18 27 18 ellipse_path
stroke
gsave 10 dict begin
1200 13 moveto 29 -0.5 (Cbv) alignedtext
end grestore
end grestore

%	Tacred -> Cbv
newpath 775 103 moveto
794 80 828 41 836 37 curveto
852 30 1077 22 1165 19 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1163 17 moveto
1173 19 lineto
1163 22 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Tacred -> Rawterm
newpath 796 119 moveto
847 118 941 116 999 115 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 997 113 moveto
1007 115 lineto
997 118 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Retyping
gsave 10 dict begin
898 210 43 18 ellipse_path
stroke
gsave 10 dict begin
898 205 moveto 64 -0.5 (Retyping) alignedtext
end grestore
end grestore

%	Tacred -> Retyping
newpath 779 135 moveto
801 154 835 182 836 183 curveto
837 183 847 188 859 193 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 860 191 moveto
868 197 lineto
858 195 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Instantiate
gsave 10 dict begin
1341 18 46 18 ellipse_path
stroke
gsave 10 dict begin
1341 13 moveto 71 -0.5 (Instantiate) alignedtext
end grestore
end grestore

%	Cbv -> Instantiate
newpath 1227 18 moveto
1243 18 1264 18 1284 18 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1284 16 moveto
1294 18 lineto
1284 21 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Retyping -> Inductiveops
newpath 941 210 moveto
955 210 971 210 986 210 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 986 208 moveto
996 210 lineto
986 213 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Reductionops
gsave 10 dict begin
1200 72 58 18 ellipse_path
stroke
gsave 10 dict begin
1200 67 moveto 94 -0.5 (Reductionops) alignedtext
end grestore
end grestore

%	Inductiveops -> Reductionops
newpath 1070 193 moveto
1097 169 1146 123 1175 95 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1172 94 moveto
1181 89 lineto
1176 98 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Reductionops -> Instantiate
newpath 1237 58 moveto
1256 51 1279 42 1299 34 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1298 32 moveto
1308 31 lineto
1299 37 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Termops
gsave 10 dict begin
1341 72 41 18 ellipse_path
stroke
gsave 10 dict begin
1341 67 moveto 60 -0.5 (Termops) alignedtext
end grestore
end grestore

%	Reductionops -> Termops
newpath 1258 72 moveto
1269 72 1280 72 1290 72 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1290 70 moveto
1300 72 lineto
1290 75 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Evd
gsave 10 dict begin
1451 18 27 18 ellipse_path
stroke
gsave 10 dict begin
1451 13 moveto 28 -0.5 (Evd) alignedtext
end grestore
end grestore

%	Instantiate -> Evd
newpath 1388 18 moveto
1397 18 1406 18 1414 18 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1414 16 moveto
1424 18 lineto
1414 21 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Recordops
gsave 10 dict begin
523 149 47 18 ellipse_path
stroke
gsave 10 dict begin
523 144 moveto 72 -0.5 (Recordops) alignedtext
end grestore
end grestore

%	Classops
gsave 10 dict begin
646 139 39 18 ellipse_path
stroke
gsave 10 dict begin
646 134 moveto 57 -0.5 (Classops) alignedtext
end grestore
end grestore

%	Recordops -> Classops
newpath 569 145 moveto
578 144 588 144 597 143 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 597 141 moveto
607 142 lineto
597 145 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Classops -> Tacred
newpath 683 133 moveto
694 131 707 129 718 127 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 718 125 moveto
728 125 lineto
719 129 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Pretyping
gsave 10 dict begin
53 241 44 18 ellipse_path
stroke
gsave 10 dict begin
53 236 moveto 67 -0.5 (Pretyping) alignedtext
end grestore
end grestore

%	Cases
gsave 10 dict begin
164 241 29 18 ellipse_path
stroke
gsave 10 dict begin
164 236 moveto 37 -0.5 (Cases) alignedtext
end grestore
end grestore

%	Pretyping -> Cases
newpath 98 241 moveto
107 241 116 241 124 241 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 124 239 moveto
134 241 lineto
124 244 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Coercion
gsave 10 dict begin
272 241 41 18 ellipse_path
stroke
gsave 10 dict begin
272 236 moveto 61 -0.5 (Coercion) alignedtext
end grestore
end grestore

%	Cases -> Coercion
newpath 194 241 moveto
202 241 211 241 220 241 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 220 239 moveto
230 241 lineto
220 244 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Pattern
gsave 10 dict begin
898 64 35 18 ellipse_path
stroke
gsave 10 dict begin
898 59 moveto 49 -0.5 (Pattern) alignedtext
end grestore
end grestore

%	Pattern -> Rawterm
newpath 928 74 moveto
950 81 982 91 1008 100 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1008 97 moveto
1017 103 lineto
1007 102 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Pattern -> Reductionops
newpath 934 65 moveto
983 66 1072 69 1134 70 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1132 68 moveto
1142 70 lineto
1132 73 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Indrec
gsave 10 dict begin
898 318 32 18 ellipse_path
stroke
gsave 10 dict begin
898 313 moveto 43 -0.5 (Indrec) alignedtext
end grestore
end grestore

%	Indrec -> Inductiveops
newpath 926 308 moveto
937 304 949 298 960 291 curveto
973 282 1004 255 1026 234 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1024 232 moveto
1033 227 lineto
1028 236 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Evarutil
gsave 10 dict begin
761 287 39 18 ellipse_path
stroke
gsave 10 dict begin
761 282 moveto 56 -0.5 (Evarutil) alignedtext
end grestore
end grestore

%	Evarutil -> Pretype_errors
newpath 798 281 moveto
809 279 822 277 834 275 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 834 273 moveto
844 273 lineto
835 277 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Evarutil -> Indrec
newpath 796 295 moveto
815 299 839 304 859 309 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 859 306 moveto
868 311 lineto
858 311 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Evarconv
gsave 10 dict begin
395 241 44 18 ellipse_path
stroke
gsave 10 dict begin
395 236 moveto 67 -0.5 (Evarconv) alignedtext
end grestore
end grestore

%	Evarconv -> Typing
newpath 440 241 moveto
452 241 465 241 477 241 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 477 239 moveto
487 241 lineto
477 244 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Evarconv -> Recordops
newpath 417 225 moveto
439 210 471 187 494 170 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 491 169 moveto
501 165 lineto
494 173 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Evarconv -> Evarutil
newpath 427 254 moveto
442 259 460 264 476 268 curveto
482 269 636 278 715 284 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 712 282 moveto
722 284 lineto
712 287 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Detyping
gsave 10 dict begin
898 156 43 18 ellipse_path
stroke
gsave 10 dict begin
898 151 moveto 64 -0.5 (Detyping) alignedtext
end grestore
end grestore

%	Detyping -> Rawterm
newpath 934 146 moveto
956 141 983 133 1006 127 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1005 125 moveto
1015 124 lineto
1006 130 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Detyping -> Inductiveops
newpath 931 168 moveto
952 176 981 185 1004 194 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 1004 191 moveto
1013 197 lineto
1003 196 lineto
closepath
fill
0.000 0.000 0.000 edgecolor

%	Coercion -> Evarconv
newpath 314 241 moveto
323 241 331 241 340 241 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 340 239 moveto
350 241 lineto
340 244 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
endpage
grestore
%%PageTrailer
%%EndPage: 1
%%Trailer
%%Pages: 1
end
restore
%%EOF