diff options
Diffstat (limited to 'dev/ocamlweb-doc/proofs.dep.ps')
-rw-r--r-- | dev/ocamlweb-doc/proofs.dep.ps | 857 |
1 files changed, 434 insertions, 423 deletions
diff --git a/dev/ocamlweb-doc/proofs.dep.ps b/dev/ocamlweb-doc/proofs.dep.ps index 0e78f422..4dd045ce 100644 --- a/dev/ocamlweb-doc/proofs.dep.ps +++ b/dev/ocamlweb-doc/proofs.dep.ps @@ -1,9 +1,9 @@ %!PS-Adobe-2.0 -%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) -%%For: (herbelin) Hugo Herbelin +%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007) +%%For: (notin) Jean-Marc Notin,,, %%Title: G %%Pages: (atend) -%%BoundingBox: 35 35 577 136 +%%BoundingBox: (atend) %%EndComments save %%BeginProlog @@ -16,57 +16,7 @@ mark 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 +EncodingVector 45 /hyphen put % Set up ISO Latin 1 character encoding /starnetISO { @@ -98,8 +48,8 @@ cleartomark /InvScaleFactor 1.0 def /set_scale { - dup 1 exch div /InvScaleFactor exch def - dup scale + dup 1 exch div /InvScaleFactor exch def + scale } bind def % styles @@ -229,403 +179,463 @@ def } if %%EndSetup +setupLatin1 %%Page: 1 1 -%%PageBoundingBox: 36 36 577 136 -%%PageOrientation: Portrait +%%PageBoundingBox: 36 36 576 753 +%%PageOrientation: Landscape gsave -35 35 542 101 boxprim clip newpath -36 36 translate +36 36 576 753 boxprim clip newpath 0 0 1 beginpage -0.6923 set_scale -0 0 translate 0 rotate -0.000 0.000 0.000 graphcolor +0.870968 0.870968 set_scale 90 rotate 45.3333 -657.333 translate +0.000 0.000 1.000 graphcolor +newpath -4 -4 moveto +-4 616 lineto +819 616 lineto +819 -4 lineto +closepath fill +0.870968 setlinewidth +0.000 0.000 1.000 graphcolor +newpath -4 -4 moveto +-4 616 lineto +819 616 lineto +819 -4 lineto +closepath stroke +% Clenvtac +gsave +0.502 1.000 0.820 nodecolor +451 522 37.1753 18 ellipse_path fill +0.870968 setlinewidth +filled +0.502 1.000 0.820 nodecolor +451 522 37.1753 18 ellipse_path stroke +0.000 0.000 0.000 nodecolor 14.00 /Times-Roman set_font - -% Tactic_debug -gsave 10 dict begin -163 72 51 18 ellipse_path -stroke -gsave 10 dict begin -125 67 moveto -(Tactic_debug) -[7.44 6.24 6.24 3.84 3.84 6.24 6.96 6.96 6.24 6.96 6.96 6.96] -xshow -end grestore -end grestore - -% Refiner -gsave 10 dict begin -287 72 34 18 ellipse_path -stroke -gsave 10 dict begin -266 67 moveto -(Refiner) -[9.12 6.24 4.8 3.84 6.96 6.24 4.56] -xshow -end grestore -end grestore - -% Tactic_debug -> Refiner -newpath 214 72 moveto -223 72 233 72 243 72 curveto +451 517 moveto 49 -0.5 (Clenvtac) alignedtext +grestore +% Evar_refiner +gsave +0.502 1.000 0.820 nodecolor +439 450 49.1777 18 ellipse_path fill +0.870968 setlinewidth +filled +0.502 1.000 0.820 nodecolor +439 450 49.1777 18 ellipse_path stroke +0.000 0.000 0.000 nodecolor +14.00 /Times-Roman set_font +439 445 moveto 72 -0.5 (Evar_refiner) alignedtext +grestore +% Clenvtac->Evar_refiner +gsave +0.870968 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 448 504 moveto +447 496 445 487 444 478 curveto stroke -gsave 10 dict begin +0.000 0.000 0.000 edgecolor +newpath 447.393 477.119 moveto +442 468 lineto +440.529 478.492 lineto +closepath fill +0.870968 setlinewidth solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 243 76 moveto -253 72 lineto -243 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 243 76 moveto -253 72 lineto -243 69 lineto -closepath -stroke -end grestore - -% Logic -gsave 10 dict begin -390 72 30 18 ellipse_path -stroke -gsave 10 dict begin -373 67 moveto -(Logic) -[8.4 6.96 6.96 3.84 6.24] -xshow -end grestore -end grestore - -% Refiner -> Logic -newpath 321 72 moveto -330 72 340 72 350 72 curveto +0.000 0.000 0.000 edgecolor +newpath 447.393 477.119 moveto +442 468 lineto +440.529 478.492 lineto +closepath stroke +grestore +% Tacmach +gsave +0.502 1.000 0.820 nodecolor +711 450 38.1754 18 ellipse_path fill +0.870968 setlinewidth +filled +0.502 1.000 0.820 nodecolor +711 450 38.1754 18 ellipse_path stroke +0.000 0.000 0.000 nodecolor +14.00 /Times-Roman set_font +711 445 moveto 51 -0.5 (Tacmach) alignedtext +grestore +% Clenvtac->Tacmach +gsave +0.870968 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 483 513 moveto +530 500 616 476 668 462 curveto stroke -gsave 10 dict begin +0.000 0.000 0.000 edgecolor +newpath 669.427 465.226 moveto +678 459 lineto +667.416 458.521 lineto +closepath fill +0.870968 setlinewidth solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 350 76 moveto -360 72 lineto -350 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 350 76 moveto -360 72 lineto -350 69 lineto -closepath -stroke -end grestore - -% Tacmach -gsave 10 dict begin -163 126 38 18 ellipse_path -stroke -gsave 10 dict begin -137 121 moveto -(Tacmach) -[7.44 6.24 6.24 10.8 6.24 6 6.96] -xshow -end grestore -end grestore - -% Tacmach -> Refiner -newpath 191 114 moveto -209 106 232 96 251 88 curveto +0.000 0.000 0.000 edgecolor +newpath 669.427 465.226 moveto +678 459 lineto +667.416 458.521 lineto +closepath stroke +grestore +% Refiner +gsave +0.502 1.000 0.820 nodecolor +439 378 34.1777 18 ellipse_path fill +0.870968 setlinewidth +filled +0.502 1.000 0.820 nodecolor +439 378 34.1777 18 ellipse_path stroke +0.000 0.000 0.000 nodecolor +14.00 /Times-Roman set_font +439 373 moveto 42 -0.5 (Refiner) alignedtext +grestore +% Evar_refiner->Refiner +gsave +0.870968 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 439 432 moveto +439 424 439 415 439 406 curveto stroke -gsave 10 dict begin +0.000 0.000 0.000 edgecolor +newpath 442.5 406 moveto +439 396 lineto +435.5 406 lineto +closepath fill +0.870968 setlinewidth solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 253 91 moveto -261 84 lineto -250 84 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 253 91 moveto -261 84 lineto -250 84 lineto -closepath -stroke -end grestore - -% Redexpr -gsave 10 dict begin -287 126 36 18 ellipse_path -stroke -gsave 10 dict begin -263 121 moveto -(Redexpr) -[9.12 6.24 6.96 5.76 6.96 6.96 4.56] -xshow -end grestore -end grestore - -% Tacmach -> Redexpr -newpath 202 126 moveto -214 126 227 126 240 126 curveto +0.000 0.000 0.000 edgecolor +newpath 442.5 406 moveto +439 396 lineto +435.5 406 lineto +closepath stroke +grestore +% Tacmach->Refiner +gsave +0.870968 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 678 441 moveto +628 428 533 403 480 389 curveto stroke -gsave 10 dict begin +0.000 0.000 0.000 edgecolor +newpath 480.584 385.521 moveto +470 386 lineto +478.573 392.226 lineto +closepath fill +0.870968 setlinewidth solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 240 130 moveto -250 126 lineto -240 123 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 240 130 moveto -250 126 lineto -240 123 lineto -closepath -stroke -end grestore - -% Proof_trees -gsave 10 dict begin -502 72 45 18 ellipse_path -stroke -gsave 10 dict begin -469 67 moveto -(Proof_trees) -[7.68 4.56 6.96 6.96 4.56 6.96 3.84 4.56 6.24 6.24 5.52] -xshow -end grestore -end grestore - -% Logic -> Proof_trees -newpath 420 72 moveto -428 72 437 72 446 72 curveto +0.000 0.000 0.000 edgecolor +newpath 480.584 385.521 moveto +470 386 lineto +478.573 392.226 lineto +closepath stroke +grestore +% Redexpr +gsave +0.502 1.000 0.820 nodecolor +711 378 36.1752 18 ellipse_path fill +0.870968 setlinewidth +filled +0.502 1.000 0.820 nodecolor +711 378 36.1752 18 ellipse_path stroke +0.000 0.000 0.000 nodecolor +14.00 /Times-Roman set_font +711 373 moveto 47 -0.5 (Redexpr) alignedtext +grestore +% Tacmach->Redexpr +gsave +0.870968 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 711 432 moveto +711 424 711 415 711 406 curveto stroke -gsave 10 dict begin +0.000 0.000 0.000 edgecolor +newpath 714.5 406 moveto +711 396 lineto +707.5 406 lineto +closepath fill +0.870968 setlinewidth solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 446 76 moveto -456 72 lineto -446 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 446 76 moveto -456 72 lineto -446 69 lineto -closepath -stroke -end grestore - -% Proof_type -gsave 10 dict begin -628 72 44 18 ellipse_path -stroke -gsave 10 dict begin -597 67 moveto -(Proof_type) -[7.68 4.56 6.96 6.96 4.56 6.96 3.84 6.96 6.96 6.24] -xshow -end grestore -end grestore - -% Tacexpr -gsave 10 dict begin -744 72 35 18 ellipse_path -stroke -gsave 10 dict begin -721 67 moveto -(Tacexpr) -[7.44 6.24 6.24 5.76 6.96 6.96 4.56] -xshow -end grestore -end grestore - -% Proof_type -> Tacexpr -newpath 672 72 moveto -680 72 689 72 698 72 curveto +0.000 0.000 0.000 edgecolor +newpath 714.5 406 moveto +711 396 lineto +707.5 406 lineto +closepath stroke +grestore +% Decl_mode +gsave +0.502 1.000 0.820 nodecolor +698 594 45.1777 18 ellipse_path fill +0.870968 setlinewidth +filled +0.502 1.000 0.820 nodecolor +698 594 45.1777 18 ellipse_path stroke +0.000 0.000 0.000 nodecolor +14.00 /Times-Roman set_font +698 589 moveto 64 -0.5 (Decl_mode) alignedtext +grestore +% Pfedit +gsave +0.502 1.000 0.820 nodecolor +698 522 30.1777 18 ellipse_path fill +0.870968 setlinewidth +filled +0.502 1.000 0.820 nodecolor +698 522 30.1777 18 ellipse_path stroke +0.000 0.000 0.000 nodecolor +14.00 /Times-Roman set_font +698 517 moveto 34 -0.5 (Pfedit) alignedtext +grestore +% Decl_mode->Pfedit +gsave +0.870968 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 698 576 moveto +698 568 698 559 698 550 curveto stroke -gsave 10 dict begin +0.000 0.000 0.000 edgecolor +newpath 701.5 550 moveto +698 540 lineto +694.5 550 lineto +closepath fill +0.870968 setlinewidth solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 698 76 moveto -708 72 lineto -698 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 698 76 moveto -708 72 lineto -698 69 lineto -closepath -stroke -end grestore - -% Proof_trees -> Proof_type -newpath 548 72 moveto -557 72 565 72 574 72 curveto +0.000 0.000 0.000 edgecolor +newpath 701.5 550 moveto +698 540 lineto +694.5 550 lineto +closepath stroke +grestore +% Pfedit->Evar_refiner +gsave +0.870968 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 671 514 moveto +628 503 543 479 488 464 curveto stroke -gsave 10 dict begin +0.000 0.000 0.000 edgecolor +newpath 488.584 460.521 moveto +478 461 lineto +486.573 467.226 lineto +closepath fill +0.870968 setlinewidth solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 574 76 moveto -584 72 lineto -574 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 574 76 moveto -584 72 lineto -574 69 lineto -closepath -stroke -end grestore - -% Pfedit -gsave 10 dict begin -38 112 29 18 ellipse_path -stroke -gsave 10 dict begin -21 107 moveto -(Pfedit) -[7.68 4.08 6.24 6.96 3.84 3.84] -xshow -end grestore -end grestore - -% Pfedit -> Tacmach -newpath 67 115 moveto -81 117 99 118 115 120 curveto +0.000 0.000 0.000 edgecolor +newpath 488.584 460.521 moveto +478 461 lineto +486.573 467.226 lineto +closepath stroke +grestore +% Pfedit->Tacmach +gsave +0.870968 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 701 504 moveto +702 496 704 487 706 478 curveto stroke -gsave 10 dict begin +0.000 0.000 0.000 edgecolor +newpath 709.471 478.492 moveto +708 468 lineto +702.607 477.119 lineto +closepath fill +0.870968 setlinewidth solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 115 123 moveto -125 122 lineto -116 117 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 115 123 moveto -125 122 lineto -116 117 lineto -closepath -stroke -end grestore - -% Evar_refiner -gsave 10 dict begin -163 18 49 18 ellipse_path -stroke -gsave 10 dict begin -127 13 moveto -(Evar_refiner) -[8.4 6.72 6.24 4.56 6.96 4.56 6.24 4.8 3.84 6.96 6.24 4.56] -xshow -end grestore -end grestore - -% Pfedit -> Evar_refiner -newpath 53 96 moveto -67 82 90 60 112 45 curveto -116 42 120 40 124 37 curveto +0.000 0.000 0.000 edgecolor +newpath 709.471 478.492 moveto +708 468 lineto +702.607 477.119 lineto +closepath stroke +grestore +% Logic +gsave +0.502 1.000 0.820 nodecolor +439 306 29.1747 18 ellipse_path fill +0.870968 setlinewidth +filled +0.502 1.000 0.820 nodecolor +439 306 29.1747 18 ellipse_path stroke +0.000 0.000 0.000 nodecolor +14.00 /Times-Roman set_font +439 301 moveto 33 -0.5 (Logic) alignedtext +grestore +% Refiner->Logic +gsave +0.870968 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 439 360 moveto +439 352 439 343 439 334 curveto stroke -gsave 10 dict begin +0.000 0.000 0.000 edgecolor +newpath 442.5 334 moveto +439 324 lineto +435.5 334 lineto +closepath fill +0.870968 setlinewidth solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 126 40 moveto -133 32 lineto -123 34 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 126 40 moveto -133 32 lineto -123 34 lineto -closepath -stroke -end grestore - -% Evar_refiner -> Refiner -newpath 195 32 moveto -212 40 233 49 251 57 curveto +0.000 0.000 0.000 edgecolor +newpath 442.5 334 moveto +439 324 lineto +435.5 334 lineto +closepath stroke +grestore +% Proof_trees +gsave +0.502 1.000 0.820 nodecolor +439 234 45.1757 18 ellipse_path fill +0.870968 setlinewidth +filled +0.502 1.000 0.820 nodecolor +439 234 45.1757 18 ellipse_path stroke +0.000 0.000 0.000 nodecolor +14.00 /Times-Roman set_font +439 229 moveto 65 -0.5 (Proof_trees) alignedtext +grestore +% Logic->Proof_trees +gsave +0.870968 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 439 288 moveto +439 280 439 271 439 262 curveto stroke -gsave 10 dict begin +0.000 0.000 0.000 edgecolor +newpath 442.5 262 moveto +439 252 lineto +435.5 262 lineto +closepath fill +0.870968 setlinewidth solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 249 60 moveto -260 61 lineto -252 54 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 249 60 moveto -260 61 lineto -252 54 lineto -closepath -stroke -end grestore - -% Clenvtac -gsave 10 dict begin -38 45 38 18 ellipse_path -stroke -gsave 10 dict begin -13 40 moveto -(Clenvtac) -[9.36 3.84 6.24 6.48 6.96 4.08 6.24 6.24] -xshow -end grestore -end grestore - -% Clenvtac -> Tacmach -newpath 58 61 moveto -73 72 93 87 112 99 curveto -117 102 123 105 128 108 curveto +0.000 0.000 0.000 edgecolor +newpath 442.5 262 moveto +439 252 lineto +435.5 262 lineto +closepath stroke +grestore +% Proof_type +gsave +0.502 1.000 0.820 nodecolor +439 162 44.1757 18 ellipse_path fill +0.870968 setlinewidth +filled +0.502 1.000 0.820 nodecolor +439 162 44.1757 18 ellipse_path stroke +0.000 0.000 0.000 nodecolor +14.00 /Times-Roman set_font +439 157 moveto 63 -0.5 (Proof_type) alignedtext +grestore +% Proof_trees->Proof_type +gsave +0.870968 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 439 216 moveto +439 208 439 199 439 190 curveto stroke -gsave 10 dict begin +0.000 0.000 0.000 edgecolor +newpath 442.5 190 moveto +439 180 lineto +435.5 190 lineto +closepath fill +0.870968 setlinewidth solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 127 111 moveto -137 113 lineto -130 105 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 127 111 moveto -137 113 lineto -130 105 lineto -closepath +0.000 0.000 0.000 edgecolor +newpath 442.5 190 moveto +439 180 lineto +435.5 190 lineto +closepath stroke +grestore +% Decl_expr +gsave +0.502 1.000 0.820 nodecolor +439 90 42.1777 18 ellipse_path fill +0.870968 setlinewidth +filled +0.502 1.000 0.820 nodecolor +439 90 42.1777 18 ellipse_path stroke +0.000 0.000 0.000 nodecolor +14.00 /Times-Roman set_font +439 85 moveto 58 -0.5 (Decl_expr) alignedtext +grestore +% Proof_type->Decl_expr +gsave +0.870968 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 439 144 moveto +439 136 439 127 439 118 curveto stroke -end grestore - -% Clenvtac -> Evar_refiner -newpath 73 37 moveto -85 35 98 32 110 29 curveto +0.000 0.000 0.000 edgecolor +newpath 442.5 118 moveto +439 108 lineto +435.5 118 lineto +closepath fill +0.870968 setlinewidth +solid +0.000 0.000 0.000 edgecolor +newpath 442.5 118 moveto +439 108 lineto +435.5 118 lineto +closepath stroke +grestore +% Tacexpr +gsave +0.502 1.000 0.820 nodecolor +439 18 36.1777 18 ellipse_path fill +0.870968 setlinewidth +filled +0.502 1.000 0.820 nodecolor +439 18 36.1777 18 ellipse_path stroke +0.000 0.000 0.000 nodecolor +14.00 /Times-Roman set_font +439 13 moveto 46 -0.5 (Tacexpr) alignedtext +grestore +% Decl_expr->Tacexpr +gsave +0.870968 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 439 72 moveto +439 64 439 55 439 46 curveto stroke -gsave 10 dict begin +0.000 0.000 0.000 edgecolor +newpath 442.5 46 moveto +439 36 lineto +435.5 46 lineto +closepath fill +0.870968 setlinewidth solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 111 32 moveto -120 27 lineto -110 26 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 111 32 moveto -120 27 lineto -110 26 lineto -closepath +0.000 0.000 0.000 edgecolor +newpath 442.5 46 moveto +439 36 lineto +435.5 46 lineto +closepath stroke +grestore +% Tactic_debug +gsave +0.502 1.000 0.820 nodecolor +133 450 51.1777 18 ellipse_path fill +0.870968 setlinewidth +filled +0.502 1.000 0.820 nodecolor +133 450 51.1777 18 ellipse_path stroke +0.000 0.000 0.000 nodecolor +14.00 /Times-Roman set_font +133 445 moveto 76 -0.5 (Tactic_debug) alignedtext +grestore +% Tactic_debug->Refiner +gsave +0.870968 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 176 440 moveto +234 426 339 401 398 387 curveto stroke -end grestore +0.000 0.000 0.000 edgecolor +newpath 398.881 390.393 moveto +408 385 lineto +397.508 383.529 lineto +closepath fill +0.870968 setlinewidth +solid +0.000 0.000 0.000 edgecolor +newpath 398.881 390.393 moveto +408 385 lineto +397.508 383.529 lineto +closepath stroke +grestore endpage showpage grestore @@ -633,6 +643,7 @@ grestore %%EndPage: 1 %%Trailer %%Pages: 1 +%%BoundingBox: 36 36 576 753 end restore %%EOF |