From: Stefano Zacchiroli Date: Mon, 19 Dec 2005 12:49:24 +0000 (+0000) Subject: upgraded dependency figures X-Git-Tag: make_still_working~7985 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=39c621e194112d5695c39d070909a3ee957b387f;p=helm.git upgraded dependency figures --- diff --git a/helm/papers/matita/libraries.ps b/helm/papers/matita/libraries.ps index 2ef6381e4..1d47f4b35 100644 --- a/helm/papers/matita/libraries.ps +++ b/helm/papers/matita/libraries.ps @@ -1,9 +1,9 @@ %!PS-Adobe-2.0 %%Creator: dot version 2.2.1 (Fri Sep 30 13:22:44 UTC 2005) -%%For: (zacchiro) Stefano Zacchiroli,,, +%%For: (sacerdot) Claudio Sacerdoti Coen,,, %%Title: G %%Pages: (atend) -%%BoundingBox: 35 35 680 885 +%%BoundingBox: 35 35 606 873 %%EndComments save %%BeginProlog @@ -230,1153 +230,1418 @@ def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 680 885 +%%PageBoundingBox: 36 36 606 873 %%PageOrientation: Portrait gsave -35 35 645 850 boxprim clip newpath +35 35 571 838 boxprim clip newpath 36 36 translate 0 0 1 beginpage 0 0 translate 0 rotate 0.000 0.000 0.000 graphcolor -24.00 /Times-Roman set_font +14.00 /Times-Roman set_font -% acic_content +% DependencyAnalyzer gsave 10 dict begin -497 574 75 25 ellipse_path +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 287 476 moveto +201 476 lineto +201 436 lineto +287 436 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 287 476 moveto +201 476 lineto +201 436 lineto +287 436 lineto +closepath stroke gsave 10 dict begin -436 566 moveto -(acic_content) -[10.56 10.56 6.72 10.56 12 10.56 12 12 6.72 10.56 12 6.72] +0.000 0.000 0.000 nodecolor +209 459 moveto +(Dependency) +[10.08 6.24 6.96 6.24 6.96 6.96 6.24 6.96 6.24 6.96] +xshow +217 443 moveto +(Analyzer) +[10.08 6.96 6.24 3.84 6.96 6.24 6.24 4.56] xshow end grestore end grestore -% cic_acic +% metadata gsave 10 dict begin -432 480 54 25 ellipse_path +191 380 38 18 ellipse_path stroke gsave 10 dict begin -392 472 moveto -(cic_acic) -[10.56 6.72 10.56 12 10.56 10.56 6.72 10.56] +165 375 moveto +(metadata) +[10.8 6.24 3.84 6.24 6.96 6.24 3.84 6.24] xshow end grestore end grestore -% acic_content -> cic_acic -newpath 480 549 moveto -472 538 463 525 455 513 curveto +% DependencyAnalyzer -> metadata +newpath 230 436 moveto +223 427 215 416 209 406 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 457 510 moveto -449 504 lineto -452 514 lineto +newpath 211 403 moveto +203 397 lineto +206 407 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 457 510 moveto -449 504 lineto -452 514 lineto +newpath 211 403 moveto +203 397 lineto +206 407 lineto closepath stroke end grestore -% cic_proof_checking +% Getter gsave 10 dict begin -441 386 110 25 ellipse_path +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 408 324 moveto +354 324 lineto +354 288 lineto +408 288 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 408 324 moveto +354 324 lineto +354 288 lineto +408 288 lineto +closepath stroke gsave 10 dict begin -345 378 moveto -(cic_proof_checking) -[10.56 6.72 10.56 12 12 7.92 12 12 7.92 12 10.56 12 10.56 10.56 12 6.72 12 12] +0.000 0.000 0.000 nodecolor +363 301 moveto +(Getter) +[10.08 6.24 3.84 3.84 6.24 4.56] xshow end grestore end grestore -% cic_acic -> cic_proof_checking -newpath 434 454 moveto -435 444 436 433 437 422 curveto +% getter +gsave 10 dict begin +275 234 29 18 ellipse_path +stroke +gsave 10 dict begin +259 229 moveto +(getter) +[6.96 6.24 3.84 3.84 6.24 4.56] +xshow +end grestore +end grestore + +% Getter -> getter +newpath 354 288 moveto +339 278 319 264 303 254 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 440 422 moveto -438 412 lineto -434 422 lineto +newpath 305 251 moveto +295 248 lineto +301 257 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 440 422 moveto -438 412 lineto -434 422 lineto +newpath 305 251 moveto +295 248 lineto +301 257 lineto +closepath +stroke +end grestore + +% Matita +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 259 836 moveto +205 836 lineto +205 800 lineto +259 800 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 259 836 moveto +205 836 lineto +205 800 lineto +259 800 lineto closepath stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +213 813 moveto +(Matita) +[12.48 6.24 3.84 3.84 3.84 6.24] +xshow +end grestore end grestore % cic_disambiguation gsave 10 dict begin -318 662 109 25 ellipse_path +313 602 68 18 ellipse_path stroke gsave 10 dict begin -223 654 moveto +258 597 moveto (cic_disambiguation) -[10.56 6.72 10.56 12 12 6.72 9.36 10.56 18.72 12 6.72 12 12 10.56 6.72 6.72 12 12] +[6.24 3.84 6.24 6.96 6.96 3.84 5.52 6.24 10.8 6.96 3.84 6.96 6.96 6.24 3.84 3.84 6.96 6.96] xshow end grestore end grestore -% cic_disambiguation -> acic_content -newpath 365 639 moveto -390 627 420 612 445 599 curveto +% Matita -> cic_disambiguation +newpath 259 801 moveto +272 792 286 779 294 764 curveto +316 721 317 664 316 630 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 446 602 moveto -454 595 lineto -443 596 lineto +newpath 319 630 moveto +315 620 lineto +313 630 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 446 602 moveto -454 595 lineto -443 596 lineto +newpath 319 630 moveto +315 620 lineto +313 630 lineto closepath stroke end grestore -% cic_unification +% grafite_engine gsave 10 dict begin -316 574 86 25 ellipse_path +232 746 53 18 ellipse_path stroke gsave 10 dict begin -244 566 moveto -(cic_unification) -[10.56 6.72 10.56 12 12 12 6.72 7.92 6.72 10.56 10.56 6.72 6.72 12 12] +191 741 moveto +(grafite_engine) +[6.96 4.56 6.24 4.56 3.84 3.84 6.24 6.96 6.24 6.96 6.96 3.84 6.96 6.24] xshow end grestore end grestore -% cic_disambiguation -> cic_unification -newpath 317 636 moveto -317 628 317 619 317 610 curveto +% Matita -> grafite_engine +newpath 232 800 moveto +232 792 232 783 232 774 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 321 610 moveto -317 600 lineto -314 610 lineto +newpath 236 774 moveto +232 764 lineto +229 774 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 321 610 moveto -317 600 lineto -314 610 lineto +newpath 236 774 moveto +232 764 lineto +229 774 lineto closepath stroke end grestore -% whelp +% grafite_parser gsave 10 dict begin -164 574 44 25 ellipse_path +393 746 52 18 ellipse_path stroke gsave 10 dict begin -134 566 moveto -(whelp) -[17.28 12 10.56 6.72 12] +354 741 moveto +(grafite_parser) +[6.96 4.56 6.24 4.56 3.84 3.84 6.24 6.96 6.96 6.24 4.56 5.52 6.24 4.56] xshow end grestore end grestore -% cic_disambiguation -> whelp -newpath 276 638 moveto -254 626 227 610 205 597 curveto +% Matita -> grafite_parser +newpath 259 806 moveto +284 794 322 777 351 764 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 206 594 moveto -196 592 lineto -203 600 lineto +newpath 353 767 moveto +361 760 lineto +350 760 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 206 594 moveto -196 592 lineto -203 600 lineto +newpath 353 767 moveto +361 760 lineto +350 760 lineto closepath stroke end grestore -% content_pres +% hgdome gsave 10 dict begin -523 662 76 25 ellipse_path +36 602 36 18 ellipse_path stroke gsave 10 dict begin -461 654 moveto -(content_pres) -[10.56 12 12 6.72 10.56 12 6.72 12 12 7.92 10.56 9.36] +12 597 moveto +(hgdome) +[6.96 6.96 6.96 6.96 10.8 6.24] xshow end grestore end grestore -% content_pres -> acic_content -newpath 515 637 moveto -513 628 510 619 508 610 curveto +% Matita -> hgdome +newpath 205 816 moveto +129 801 85 826 38 764 curveto +9 725 19 665 27 630 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 511 609 moveto -505 600 lineto -505 611 lineto +newpath 30 631 moveto +30 620 lineto +24 629 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 511 609 moveto -505 600 lineto -505 611 lineto +newpath 30 631 moveto +30 620 lineto +24 629 lineto closepath stroke end grestore -% grafite +% paramodulation gsave 10 dict begin -554 750 46 25 ellipse_path +104 746 57 18 ellipse_path stroke gsave 10 dict begin -522 742 moveto -(grafite) -[12 7.92 10.56 7.92 6.72 6.72 10.56] +59 741 moveto +(paramodulation) +[6.96 6.24 4.56 6.24 10.8 6.96 6.96 6.96 3.84 6.24 3.84 3.84 6.96 6.96] xshow end grestore end grestore -% grafite -> content_pres -newpath 545 725 moveto -542 716 539 706 535 697 curveto +% Matita -> paramodulation +newpath 205 803 moveto +186 793 161 778 141 767 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 538 696 moveto -532 687 lineto -532 698 lineto +newpath 142 764 moveto +132 762 lineto +139 770 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 538 696 moveto -532 687 lineto -532 698 lineto +newpath 142 764 moveto +132 762 lineto +139 770 lineto closepath stroke end grestore -% cic_unification -> cic_proof_checking -newpath 323 549 moveto -330 522 345 479 368 448 curveto -376 437 387 426 397 417 curveto -stroke +% ProofChecker gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 400 419 moveto -405 410 lineto -395 414 lineto +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 309 400 moveto +247 400 lineto +247 360 lineto +309 360 lineto closepath fill -0.000 0.000 0.000 edgecolor -newpath 400 419 moveto -405 410 lineto -395 414 lineto +0.584 0.220 0.933 nodecolor +newpath 309 400 moveto +247 400 lineto +247 360 lineto +309 360 lineto closepath stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +262 383 moveto +(Proof) +[7.68 4.56 6.96 6.96 4.56] +xshow +254 367 moveto +(Checker) +[9.36 6.96 6.24 6.24 6.96 6.24 4.56] +xshow +end grestore end grestore -% tactics +% cic_proof_checking gsave 10 dict begin -144 662 45 25 ellipse_path +268 306 68 18 ellipse_path stroke gsave 10 dict begin -113 654 moveto -(tactics) -[6.72 10.56 10.56 6.72 6.72 10.56 9.36] +212 301 moveto +(cic_proof_checking) +[6.24 3.84 6.24 6.96 6.96 4.56 6.96 6.96 4.56 6.96 6.24 6.96 6.24 6.24 6.96 3.84 6.96 6.96] xshow end grestore end grestore -% tactics -> cic_unification -newpath 178 645 moveto -202 632 236 615 264 601 curveto +% ProofChecker -> cic_proof_checking +newpath 275 360 moveto +274 352 273 343 272 334 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 266 604 moveto -273 596 lineto -263 598 lineto +newpath 275 333 moveto +270 324 lineto +269 334 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 266 604 moveto -273 596 lineto -263 598 lineto +newpath 275 333 moveto +270 324 lineto +269 334 lineto closepath stroke end grestore -% tactics -> whelp -newpath 150 637 moveto -152 628 154 618 156 609 curveto +% Uwobo +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 489 692 moveto +431 692 lineto +431 656 lineto +489 656 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 489 692 moveto +431 692 lineto +431 656 lineto +489 656 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +438 669 moveto +(Uwobo) +[10.08 10.08 6.96 6.96 6.96] +xshow +end grestore +end grestore + +% content_pres +gsave 10 dict begin +454 602 49 18 ellipse_path +stroke +gsave 10 dict begin +418 597 moveto +(content_pres) +[6.24 6.96 6.96 3.84 6.24 6.96 3.84 6.96 6.96 4.56 6.24 5.52] +xshow +end grestore +end grestore + +% Uwobo -> content_pres +newpath 458 656 moveto +457 648 457 639 456 630 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 159 609 moveto -158 599 lineto -153 608 lineto +newpath 460 630 moveto +456 620 lineto +453 630 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 159 609 moveto -158 599 lineto -153 608 lineto +newpath 460 630 moveto +456 620 lineto +453 630 lineto closepath stroke end grestore -% paramodulation +% Whelp gsave 10 dict begin -151 750 90 25 ellipse_path +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 420 836 moveto +366 836 lineto +366 800 lineto +420 800 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 420 836 moveto +366 836 lineto +366 800 lineto +420 800 lineto +closepath stroke gsave 10 dict begin -75 742 moveto -(paramodulation) -[12 10.56 7.92 10.56 18.72 12 12 12 6.72 10.56 6.72 6.72 12 12] +0.000 0.000 0.000 nodecolor +373 813 moveto +(Whelp) +[13.2 6.96 6.24 3.84 6.96] xshow end grestore end grestore -% paramodulation -> tactics -newpath 149 724 moveto -148 716 148 707 147 698 curveto +% Whelp -> grafite_parser +newpath 393 800 moveto +393 792 393 783 393 774 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 150 698 moveto -146 688 lineto -144 698 lineto +newpath 397 774 moveto +393 764 lineto +390 774 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 150 698 moveto -146 688 lineto -144 698 lineto +newpath 397 774 moveto +393 764 lineto +390 774 lineto closepath stroke end grestore % cic gsave 10 dict begin -412 298 28 25 ellipse_path +172 234 27 18 ellipse_path stroke gsave 10 dict begin -398 290 moveto +163 229 moveto (cic) -[10.56 6.72 10.56] +[6.24 3.84 6.24] xshow end grestore end grestore -% urimanager +% metadata -> cic +newpath 189 362 moveto +185 337 179 292 175 262 curveto +stroke gsave 10 dict begin -332 210 70 25 ellipse_path +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 178 262 moveto +174 252 lineto +172 262 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 178 262 moveto +174 252 lineto +172 262 lineto +closepath stroke +end grestore + +% hmysql gsave 10 dict begin -276 202 moveto -(urimanager) -[12 7.92 6.72 18.72 10.56 12 10.56 12 10.56 7.92] +401 234 34 18 ellipse_path +stroke +gsave 10 dict begin +379 229 moveto +(hmysql) +[6.96 10.8 6.96 5.52 6.96 3.84] xshow end grestore end grestore -% cic -> urimanager -newpath 394 278 moveto -384 267 372 254 361 241 curveto +% metadata -> hmysql +newpath 218 367 moveto +225 364 232 362 238 360 curveto +316 335 365 386 417 324 curveto +431 306 425 280 416 261 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 364 239 moveto -354 234 lineto -359 244 lineto +newpath 419 259 moveto +411 252 lineto +413 262 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 364 239 moveto -354 234 lineto -359 244 lineto +newpath 419 259 moveto +411 252 lineto +413 262 lineto closepath stroke end grestore -% xml +% urimanager gsave 10 dict begin -431 122 33 25 ellipse_path +181 162 45 18 ellipse_path stroke gsave 10 dict begin -412 114 moveto -(xml) -[12 18.72 6.72] +148 157 moveto +(urimanager) +[6.96 4.56 3.84 10.8 6.24 6.96 6.24 6.96 6.24 4.56] xshow end grestore end grestore -% cic -> xml -newpath 415 272 moveto -418 242 424 192 427 158 curveto +% getter -> urimanager +newpath 256 220 moveto +242 210 225 196 210 184 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 430 158 moveto -428 148 lineto -424 158 lineto +newpath 212 181 moveto +202 178 lineto +208 187 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 430 158 moveto -428 148 lineto -424 158 lineto +newpath 212 181 moveto +202 178 lineto +208 187 lineto closepath stroke end grestore -% cic_proof_checking -> cic -newpath 433 361 moveto -430 352 427 342 423 333 curveto +% registry +gsave 10 dict begin +359 162 35 18 ellipse_path +stroke +gsave 10 dict begin +337 157 moveto +(registry) +[4.56 6.24 6.96 3.84 5.52 3.84 4.56 6.96] +xshow +end grestore +end grestore + +% getter -> registry +newpath 292 219 moveto +304 209 319 196 333 185 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 426 332 moveto -420 323 lineto -420 334 lineto +newpath 336 187 moveto +341 178 lineto +331 182 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 426 332 moveto -420 323 lineto -420 334 lineto +newpath 336 187 moveto +341 178 lineto +331 182 lineto closepath stroke end grestore -% getter +% logger gsave 10 dict begin -274 298 42 25 ellipse_path +275 162 31 18 ellipse_path stroke gsave 10 dict begin -246 290 moveto -(getter) -[12 10.56 6.72 6.72 10.56 7.92] +257 157 moveto +(logger) +[3.84 6.96 6.96 6.96 6.24 4.56] xshow end grestore end grestore -% cic_proof_checking -> getter -newpath 396 362 moveto -371 349 340 332 315 320 curveto +% getter -> logger +newpath 275 216 moveto +275 208 275 199 275 190 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 316 317 moveto -306 315 lineto -313 323 lineto +newpath 279 190 moveto +275 180 lineto +272 190 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 316 317 moveto -306 315 lineto -313 323 lineto +newpath 279 190 moveto +275 180 lineto +272 190 lineto closepath stroke end grestore -% getter -> urimanager -newpath 290 274 moveto -296 265 304 254 310 244 curveto +% cic_unification +gsave 10 dict begin +286 530 55 18 ellipse_path +stroke +gsave 10 dict begin +244 525 moveto +(cic_unification) +[6.24 3.84 6.24 6.96 6.96 6.96 3.84 4.56 3.84 6.24 6.24 3.84 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% cic_disambiguation -> cic_unification +newpath 306 584 moveto +303 576 300 566 296 558 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 313 245 moveto -316 235 lineto -308 241 lineto +newpath 299 557 moveto +293 548 lineto +293 559 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 313 245 moveto -316 235 lineto -308 241 lineto +newpath 299 557 moveto +293 548 lineto +293 559 lineto closepath stroke end grestore -% registry +% acic_content gsave 10 dict begin -190 210 52 25 ellipse_path +407 530 48 18 ellipse_path stroke gsave 10 dict begin -152 202 moveto -(registry) -[7.92 10.56 12 6.72 9.36 6.72 7.92 12] +371 525 moveto +(acic_content) +[6.24 6.24 3.84 6.24 6.96 6.24 6.96 6.96 3.84 6.24 6.96 3.84] xshow end grestore end grestore -% getter -> registry -newpath 253 276 moveto -243 265 230 252 219 240 curveto +% cic_disambiguation -> acic_content +newpath 335 585 moveto +347 575 364 563 378 552 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 222 238 moveto -212 233 lineto -217 243 lineto +newpath 380 555 moveto +386 546 lineto +376 549 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 222 238 moveto -212 233 lineto -217 243 lineto +newpath 380 555 moveto +386 546 lineto +376 549 lineto closepath stroke end grestore -% metadata +% whelp gsave 10 dict begin -159 386 58 25 ellipse_path +183 530 30 18 ellipse_path stroke gsave 10 dict begin -115 378 moveto -(metadata) -[18.72 10.56 6.72 10.56 12 10.56 6.72 10.56] +165 525 moveto +(whelp) +[10.08 6.96 6.24 3.84 6.96] xshow end grestore end grestore -% metadata -> cic -newpath 203 369 moveto -211 366 219 363 227 360 curveto -277 342 337 322 374 310 curveto +% cic_disambiguation -> whelp +newpath 284 586 moveto +263 574 235 559 214 547 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 375 313 moveto -384 307 lineto -373 307 lineto +newpath 215 544 moveto +205 542 lineto +212 550 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 375 313 moveto -384 307 lineto -373 307 lineto +newpath 215 544 moveto +205 542 lineto +212 550 lineto closepath stroke end grestore -% metadata -> getter -newpath 188 364 moveto -203 352 223 337 240 324 curveto +% grafite +gsave 10 dict begin +243 674 31 18 ellipse_path +stroke +gsave 10 dict begin +224 669 moveto +(grafite) +[6.96 4.56 6.24 4.56 3.84 3.84 6.24] +xshow +end grestore +end grestore + +% grafite_engine -> grafite +newpath 235 728 moveto +236 720 238 711 239 702 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 242 327 moveto -248 318 lineto -238 321 lineto +newpath 242 702 moveto +240 692 lineto +236 702 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 242 327 moveto -248 318 lineto -238 321 lineto +newpath 242 702 moveto +240 692 lineto +236 702 lineto closepath stroke end grestore -% hmysql +% tactics gsave 10 dict begin -161 298 50 25 ellipse_path +184 602 31 18 ellipse_path stroke gsave 10 dict begin -125 290 moveto -(hmysql) -[12 18.72 12 9.36 12 6.72] +165 597 moveto +(tactics) +[3.84 6.24 6.24 3.84 3.84 6.24 5.52] xshow end grestore end grestore -% metadata -> hmysql -newpath 160 360 moveto -160 352 160 343 160 334 curveto +% grafite_engine -> tactics +newpath 221 728 moveto +215 718 208 704 203 692 curveto +195 672 191 648 188 630 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 164 334 moveto -160 324 lineto -157 334 lineto +newpath 191 629 moveto +186 620 lineto +185 630 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 164 334 moveto -160 324 lineto -157 334 lineto +newpath 191 629 moveto +186 620 lineto +185 630 lineto closepath stroke end grestore -% whelp -> metadata -newpath 163 548 moveto -162 515 161 459 160 422 curveto +% grafite_parser -> grafite +newpath 362 731 moveto +337 719 302 702 276 690 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 164 422 moveto -160 412 lineto -157 422 lineto +newpath 278 687 moveto +267 686 lineto +275 693 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 164 422 moveto -160 412 lineto -157 422 lineto +newpath 278 687 moveto +267 686 lineto +275 693 lineto closepath stroke end grestore -% extlib +% sheath gsave 10 dict begin -431 34 42 25 ellipse_path +382 674 31 18 ellipse_path stroke gsave 10 dict begin -403 26 moveto -(extlib) -[10.56 12 6.72 6.72 6.72 12] +364 669 moveto +(sheath) +[5.52 6.96 6.24 6.24 3.84 6.96] xshow end grestore end grestore -% hgdome +% grafite_parser -> sheath +newpath 390 728 moveto +389 720 387 711 386 702 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 389 702 moveto +385 692 lineto +383 702 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 389 702 moveto +385 692 lineto +383 702 lineto +closepath +stroke +end grestore + +% xml gsave 10 dict begin -571 210 54 25 ellipse_path +108 90 27 18 ellipse_path stroke gsave 10 dict begin -531 202 moveto -(hgdome) -[12 12 12 12 18.72 10.56] +96 85 moveto +(xml) +[6.96 10.8 3.84] xshow end grestore end grestore % hgdome -> xml -newpath 538 189 moveto -517 176 488 158 466 144 curveto +newpath 39 584 moveto +44 557 53 502 53 456 curveto +53 456 53 456 53 234 curveto +53 190 76 144 92 116 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 468 141 moveto -458 139 lineto -465 147 lineto +newpath 95 117 moveto +97 107 lineto +89 114 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 468 141 moveto -458 139 lineto -465 147 lineto +newpath 95 117 moveto +97 107 lineto +89 114 lineto closepath stroke end grestore -% hmysql -> registry -newpath 169 273 moveto -172 264 175 254 179 245 curveto +% paramodulation -> tactics +newpath 114 728 moveto +128 703 153 657 169 628 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 182 246 moveto -182 235 lineto -176 244 lineto +newpath 172 629 moveto +174 619 lineto +166 626 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 182 246 moveto -182 235 lineto -176 244 lineto +newpath 172 629 moveto +174 619 lineto +166 626 lineto closepath stroke end grestore -% registry -> xml -newpath 229 193 moveto -237 190 245 187 252 184 curveto -299 166 354 147 390 135 curveto +% cic_proof_checking -> getter +newpath 270 288 moveto +271 280 271 271 272 262 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 391 138 moveto -400 132 lineto -389 132 lineto +newpath 275 262 moveto +273 252 lineto +269 262 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 391 138 moveto -400 132 lineto -389 132 lineto +newpath 275 262 moveto +273 252 lineto +269 262 lineto closepath stroke end grestore -% xml -> extlib -newpath 431 96 moveto -431 88 431 79 431 70 curveto +% cic_proof_checking -> cic +newpath 245 289 moveto +231 279 213 265 198 254 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 435 70 moveto -431 60 lineto -428 70 lineto +newpath 200 251 moveto +190 248 lineto +196 257 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 435 70 moveto -431 60 lineto -428 70 lineto +newpath 200 251 moveto +190 248 lineto +196 257 lineto closepath stroke end grestore -% DependencyAnalyzer +% content_pres -> acic_content +newpath 442 584 moveto +437 576 430 566 424 556 curveto +stroke gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 136 512 moveto -0 512 lineto -0 448 lineto -136 448 lineto +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 427 554 moveto +418 548 lineto +421 558 lineto closepath fill -0.584 0.220 0.933 nodecolor -newpath 136 512 moveto -0 512 lineto -0 448 lineto -136 448 lineto +0.000 0.000 0.000 edgecolor +newpath 427 554 moveto +418 548 lineto +421 558 lineto closepath stroke +end grestore + +% utf8_macros gsave 10 dict begin -0.000 0.000 0.000 nodecolor -8 486 moveto -(Dependency) -[17.28 10.56 12 10.56 12 12 10.56 12 10.56 12] -xshow -24 458 moveto -(Analyzer) -[17.28 12 10.56 6.72 12 10.56 10.56 7.92] +521 530 48 18 ellipse_path +stroke +gsave 10 dict begin +485 525 moveto +(utf8_macros) +[6.96 3.84 4.56 6.96 6.96 10.8 6.24 6.24 4.56 6.96 5.52] xshow end grestore end grestore -% DependencyAnalyzer -> metadata -newpath 99 448 moveto -109 438 119 427 129 417 curveto +% content_pres -> utf8_macros +newpath 470 585 moveto +479 576 489 565 498 555 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 131 420 moveto -136 410 lineto -126 415 lineto +newpath 501 557 moveto +505 547 lineto +496 552 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 131 420 moveto -136 410 lineto -126 415 lineto +newpath 501 557 moveto +505 547 lineto +496 552 lineto closepath stroke end grestore -% Getter +% grafite -> cic +newpath 215 666 moveto +193 658 162 643 144 620 curveto +120 587 125 570 125 530 curveto +125 530 125 530 125 380 curveto +125 336 144 289 158 260 curveto +stroke gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 312 404 moveto -236 404 lineto -236 368 lineto -312 368 lineto +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 161 262 moveto +162 251 lineto +155 259 lineto closepath fill -0.584 0.220 0.933 nodecolor -newpath 312 404 moveto -236 404 lineto -236 368 lineto -312 368 lineto +0.000 0.000 0.000 edgecolor +newpath 161 262 moveto +162 251 lineto +155 259 lineto closepath stroke +end grestore + +% sheath -> cic_disambiguation +newpath 367 658 moveto +358 649 347 637 337 627 curveto +stroke gsave 10 dict begin -0.000 0.000 0.000 nodecolor -244 378 moveto -(Getter) -[17.28 10.56 6.72 6.72 10.56 7.92] -xshow +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 340 625 moveto +330 620 lineto +335 630 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 340 625 moveto +330 620 lineto +335 630 lineto +closepath +stroke end grestore + +% sheath -> content_pres +newpath 398 658 moveto +407 649 419 637 430 626 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 432 629 moveto +437 619 lineto +427 624 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 432 629 moveto +437 619 lineto +427 624 lineto +closepath +stroke end grestore -% Getter -> getter -newpath 274 368 moveto -274 358 274 346 274 334 curveto +% tactics -> cic_unification +newpath 204 588 moveto +218 578 238 564 255 553 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 278 334 moveto -274 324 lineto -271 334 lineto +newpath 257 556 moveto +263 547 lineto +253 550 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 278 334 moveto -274 324 lineto -271 334 lineto +newpath 257 556 moveto +263 547 lineto +253 550 lineto closepath stroke end grestore -% Matita +% tactics -> whelp +newpath 184 584 moveto +183 576 183 567 183 558 curveto +stroke gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 454 848 moveto -376 848 lineto -376 812 lineto -454 812 lineto +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 187 558 moveto +183 548 lineto +180 558 lineto closepath fill -0.584 0.220 0.933 nodecolor -newpath 454 848 moveto -376 848 lineto -376 812 lineto -454 812 lineto +0.000 0.000 0.000 edgecolor +newpath 187 558 moveto +183 548 lineto +180 558 lineto closepath stroke +end grestore + +% library gsave 10 dict begin -0.000 0.000 0.000 nodecolor -383 822 moveto -(Matita) -[21.36 10.56 6.72 6.72 6.72 10.56] +337 456 32 18 ellipse_path +stroke +gsave 10 dict begin +318 451 moveto +(library) +[3.84 3.84 6.96 4.56 6.24 4.56 6.96] xshow end grestore end grestore -% Matita -> cic_disambiguation -newpath 376 815 moveto -343 801 300 783 296 776 curveto -281 752 289 721 299 696 curveto +% cic_unification -> library +newpath 298 512 moveto +304 503 312 492 319 482 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 302 698 moveto -303 687 lineto -296 695 lineto +newpath 322 483 moveto +325 473 lineto +317 479 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 302 698 moveto -303 687 lineto -296 695 lineto +newpath 322 483 moveto +325 473 lineto +317 479 lineto closepath stroke end grestore -% Matita -> grafite -newpath 447 812 moveto -466 801 491 786 512 774 curveto +% cic_acic +gsave 10 dict begin +363 380 36 18 ellipse_path +stroke +gsave 10 dict begin +340 375 moveto +(cic_acic) +[6.24 3.84 6.24 6.96 6.24 6.24 3.84 6.24] +xshow +end grestore +end grestore + +% acic_content -> cic_acic +newpath 402 512 moveto +394 486 380 438 371 408 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 514 777 moveto -521 769 lineto -511 771 lineto +newpath 374 407 moveto +368 398 lineto +368 409 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 514 777 moveto -521 769 lineto -511 771 lineto +newpath 374 407 moveto +368 398 lineto +368 409 lineto closepath stroke end grestore -% Matita -> paramodulation -newpath 376 818 moveto -336 806 272 787 223 772 curveto +% whelp -> metadata +newpath 184 512 moveto +185 486 187 439 189 408 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 224 769 moveto -213 769 lineto -222 775 lineto +newpath 192 408 moveto +190 398 lineto +186 408 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 224 769 moveto -213 769 lineto -222 775 lineto +newpath 192 408 moveto +190 398 lineto +186 408 lineto closepath stroke end grestore -% Matita -> hgdome -newpath 454 827 moveto -524 814 562 831 610 776 curveto -643 737 629 713 629 662 curveto -629 662 629 662 629 386 curveto -629 334 606 278 590 244 curveto +% library -> metadata +newpath 313 444 moveto +290 431 253 413 226 398 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 593 242 moveto -585 235 lineto -587 245 lineto +newpath 227 395 moveto +217 393 lineto +224 401 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 593 242 moveto -585 235 lineto -587 245 lineto +newpath 227 395 moveto +217 393 lineto +224 401 lineto closepath stroke end grestore -% ProofChecker +% library -> cic_acic +newpath 343 438 moveto +346 429 350 418 354 408 curveto +stroke gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 601 512 moveto -505 512 lineto -505 448 lineto -601 448 lineto +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 357 409 moveto +357 398 lineto +351 407 lineto closepath fill -0.584 0.220 0.933 nodecolor -newpath 601 512 moveto -505 512 lineto -505 448 lineto -601 448 lineto +0.000 0.000 0.000 edgecolor +newpath 357 409 moveto +357 398 lineto +351 407 lineto closepath stroke -gsave 10 dict begin -0.000 0.000 0.000 nodecolor -526 486 moveto -(Proof) -[13.44 7.92 12 12 7.92] -xshow -513 458 moveto -(Checker) -[16.08 12 10.56 10.56 12 10.56 7.92] -xshow -end grestore end grestore -% ProofChecker -> cic_proof_checking -newpath 515 448 moveto -503 438 490 427 478 417 curveto +% cic_acic -> cic_proof_checking +newpath 343 365 moveto +330 355 312 341 298 329 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 480 414 moveto -470 411 lineto -476 420 lineto +newpath 300 326 moveto +290 323 lineto +296 332 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 480 414 moveto -470 411 lineto -476 420 lineto +newpath 300 326 moveto +290 323 lineto +296 332 lineto closepath stroke end grestore -% Uwobo +% cic -> xml +newpath 156 219 moveto +146 209 134 195 127 180 curveto +118 161 113 137 110 118 curveto +stroke gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 489 768 moveto -403 768 lineto -403 732 lineto -489 732 lineto +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 113 118 moveto +109 108 lineto +107 118 lineto closepath fill -0.584 0.220 0.933 nodecolor -newpath 489 768 moveto -403 768 lineto -403 732 lineto -489 732 lineto +0.000 0.000 0.000 edgecolor +newpath 113 118 moveto +109 108 lineto +107 118 lineto closepath stroke -gsave 10 dict begin -0.000 0.000 0.000 nodecolor -410 742 moveto -(Uwobo) -[17.28 17.28 12 12 12] -xshow -end grestore end grestore -% Uwobo -> content_pres -newpath 462 732 moveto -472 721 484 707 495 695 curveto +% cic -> urimanager +newpath 174 216 moveto +175 208 176 199 177 190 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 498 697 moveto -502 687 lineto -493 692 lineto +newpath 180 190 moveto +179 180 lineto +174 189 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 498 697 moveto -502 687 lineto -493 692 lineto +newpath 180 190 moveto +179 180 lineto +174 189 lineto closepath stroke end grestore -% Whelp +% hmysql -> registry +newpath 391 217 moveto +386 208 380 197 374 188 curveto +stroke gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 385 768 moveto -305 768 lineto -305 732 lineto -385 732 lineto +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 377 186 moveto +369 179 lineto +371 189 lineto closepath fill -0.584 0.220 0.933 nodecolor -newpath 385 768 moveto -305 768 lineto -305 732 lineto -385 732 lineto +0.000 0.000 0.000 edgecolor +newpath 377 186 moveto +369 179 lineto +371 189 lineto closepath stroke +end grestore + +% extlib gsave 10 dict begin -0.000 0.000 0.000 nodecolor -312 742 moveto -(Whelp) -[22.56 12 10.56 6.72 12] +108 18 29 18 ellipse_path +stroke +gsave 10 dict begin +92 13 moveto +(extlib) +[6.24 6.96 3.84 3.84 3.84 6.96] xshow end grestore end grestore -% Whelp -> cic_disambiguation -newpath 339 732 moveto -336 722 332 709 329 698 curveto +% xml -> extlib +newpath 108 72 moveto +108 64 108 55 108 46 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 332 697 moveto -326 688 lineto -326 699 lineto +newpath 112 46 moveto +108 36 lineto +105 46 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 332 697 moveto -326 688 lineto -326 699 lineto +newpath 112 46 moveto +108 36 lineto +105 46 lineto closepath stroke end grestore -% Whelp -> content_pres -newpath 378 732 moveto -383 729 389 726 394 724 curveto -418 712 446 699 469 687 curveto +% registry -> xml +newpath 332 150 moveto +327 148 321 146 315 144 curveto +256 124 185 107 144 97 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 470 690 moveto -478 683 lineto -467 684 lineto +newpath 144 94 moveto +134 95 lineto +143 100 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 470 690 moveto -478 683 lineto -467 684 lineto +newpath 144 94 moveto +134 95 lineto +143 100 lineto closepath stroke end grestore diff --git a/helm/papers/matita/librariesCluster.ps b/helm/papers/matita/librariesCluster.ps index 2fd94573d..94b066687 100644 --- a/helm/papers/matita/librariesCluster.ps +++ b/helm/papers/matita/librariesCluster.ps @@ -1,9 +1,9 @@ %!PS-Adobe-2.0 %%Creator: dot version 2.2.1 (Fri Sep 30 13:22:44 UTC 2005) -%%For: (zacchiro) Stefano Zacchiroli,,, +%%For: (sacerdot) Claudio Sacerdoti Coen,,, %%Title: G %%Pages: (atend) -%%BoundingBox: 35 35 1258 979 +%%BoundingBox: 35 35 1108 1263 %%EndComments save %%BeginProlog @@ -230,10 +230,10 @@ def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 1258 979 +%%PageBoundingBox: 36 36 1108 1263 %%PageOrientation: Portrait gsave -35 35 1223 944 boxprim clip newpath +35 35 1073 1228 boxprim clip newpath 36 36 translate 0 0 1 beginpage 0 0 translate 0 rotate @@ -244,22 +244,22 @@ gsave 10 dict begin filled 0.000 0.000 1.000 sethsbcolor 0.000 0.000 0.929 sethsbcolor -newpath 764 488 moveto -1193 488 lineto -1193 862 lineto -764 862 lineto +newpath 634 778 moveto +1063 778 lineto +1063 1162 lineto +634 1162 lineto closepath fill 0.000 0.000 1.000 sethsbcolor -newpath 764 488 moveto -1193 488 lineto -1193 862 lineto -764 862 lineto +newpath 634 778 moveto +1063 778 lineto +1063 1162 lineto +634 1162 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 sethsbcolor -772 498 moveto +642 788 moveto (Terms at the content and presentation level) [14.64 10.56 7.92 18.72 9.36 6 10.56 6.72 6 6.72 12 10.56 6 10.56 12 12 6.72 10.56 12 6.72 6 10.56 12 12 6 12 7.92 10.56 9.36 10.56 12 6.72 10.56 6.72 6.72 12 12 6 6.72 10.56 12 10.56 6.72] xshow @@ -270,22 +270,22 @@ gsave 10 dict begin filled 0.000 0.000 1.000 sethsbcolor 0.000 0.000 0.929 sethsbcolor -newpath 314 618 moveto -564 618 lineto -564 898 lineto -314 898 lineto +newpath 68 814 moveto +454 814 lineto +454 1094 lineto +68 1094 lineto closepath fill 0.000 0.000 1.000 sethsbcolor -newpath 314 618 moveto -564 618 lineto -564 898 lineto -314 898 lineto +newpath 68 814 moveto +454 814 lineto +454 1094 lineto +68 1094 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 sethsbcolor -322 872 moveto +76 1068 moveto (Partially specified terms) [13.44 10.56 7.92 6.72 6.72 10.56 6.72 6.72 12 6 9.36 12 10.56 10.56 6.72 7.92 6.72 10.56 12 6 6.72 10.56 7.92 18.72 9.36] xshow @@ -296,22 +296,22 @@ gsave 10 dict begin filled 0.000 0.000 1.000 sethsbcolor 0.000 0.000 0.929 sethsbcolor -newpath 86 208 moveto -460 208 lineto -460 592 lineto -86 592 lineto +newpath 289 296 moveto +551 296 lineto +551 770 lineto +289 770 lineto closepath fill 0.000 0.000 1.000 sethsbcolor -newpath 86 208 moveto -460 208 lineto -460 592 lineto -86 592 lineto +newpath 289 296 moveto +551 296 lineto +551 770 lineto +289 770 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 sethsbcolor -93 218 moveto +296 306 moveto (Fully specified terms) [13.44 12 6.72 6.72 12 6 9.36 12 10.56 10.56 6.72 7.92 6.72 10.56 12 6 6.72 10.56 7.92 18.72 9.36] xshow @@ -322,22 +322,22 @@ gsave 10 dict begin filled 0.000 0.000 1.000 sethsbcolor 0.000 0.000 0.929 sethsbcolor -newpath 468 16 moveto -718 16 lineto -718 400 lineto -468 400 lineto +newpath 559 16 moveto +957 16 lineto +957 400 lineto +559 400 lineto closepath fill 0.000 0.000 1.000 sethsbcolor -newpath 468 16 moveto -718 16 lineto -718 400 lineto -468 400 lineto +newpath 559 16 moveto +957 16 lineto +957 400 lineto +559 400 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 sethsbcolor -632 26 moveto +871 26 moveto (Utilities) [17.28 6.72 6.72 6.72 6.72 6.72 6.72 10.56 9.36] xshow @@ -346,10 +346,10 @@ end grestore % acic_content gsave 10 dict begin -849 652 75 25 ellipse_path +752 848 75 25 ellipse_path stroke gsave 10 dict begin -788 644 moveto +691 840 moveto (acic_content) [10.56 10.56 6.72 10.56 12 10.56 12 12 6.72 10.56 12 6.72] xshow @@ -358,10 +358,10 @@ end grestore % cic_acic gsave 10 dict begin -839 558 54 25 ellipse_path +352 636 54 25 ellipse_path stroke gsave 10 dict begin -799 550 moveto +312 628 moveto (cic_acic) [10.56 6.72 10.56 12 10.56 10.56 6.72 10.56] xshow @@ -369,265 +369,360 @@ end grestore end grestore % acic_content -> cic_acic -newpath 846 626 moveto -845 616 844 605 843 594 curveto +newpath 717 825 moveto +691 809 653 789 617 778 curveto +592 769 579 786 557 770 curveto +532 750 552 725 528 704 curveto +490 668 465 687 416 668 curveto +410 665 404 663 398 660 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 846 594 moveto -842 584 lineto -840 594 lineto +newpath 399 657 moveto +389 655 lineto +396 663 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 846 594 moveto -842 584 lineto -840 594 lineto +newpath 399 657 moveto +389 655 lineto +396 663 lineto closepath stroke end grestore -% cic_proof_checking +% cic_disambiguation gsave 10 dict begin -341 454 110 25 ellipse_path +752 936 109 25 ellipse_path stroke gsave 10 dict begin -245 446 moveto -(cic_proof_checking) -[10.56 6.72 10.56 12 12 7.92 12 12 7.92 12 10.56 12 10.56 10.56 12 6.72 12 12] +657 928 moveto +(cic_disambiguation) +[10.56 6.72 10.56 12 12 6.72 9.36 10.56 18.72 12 6.72 12 12 10.56 6.72 6.72 12 12] xshow end grestore end grestore -% cic_acic -> cic_proof_checking -newpath 820 534 moveto -806 518 784 497 760 488 curveto -741 480 423 491 361 482 curveto +% cic_disambiguation -> acic_content +newpath 752 910 moveto +752 902 752 893 752 884 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 361 479 moveto -351 480 lineto -360 485 lineto +newpath 756 884 moveto +752 874 lineto +749 884 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 361 479 moveto -351 480 lineto -360 485 lineto +newpath 756 884 moveto +752 874 lineto +749 884 lineto closepath stroke end grestore -% cic_disambiguation +% cic_unification gsave 10 dict begin -1054 740 109 25 ellipse_path +359 848 86 25 ellipse_path stroke gsave 10 dict begin -959 732 moveto -(cic_disambiguation) -[10.56 6.72 10.56 12 12 6.72 9.36 10.56 18.72 12 6.72 12 12 10.56 6.72 6.72 12 12] +287 840 moveto +(cic_unification) +[10.56 6.72 10.56 12 12 12 6.72 7.92 6.72 10.56 10.56 6.72 6.72 12 12] xshow end grestore end grestore -% cic_disambiguation -> acic_content -newpath 975 722 moveto -935 712 890 698 867 684 curveto +% cic_disambiguation -> cic_unification +newpath 672 918 moveto +604 903 507 881 439 865 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 869 681 moveto -859 678 lineto -865 687 lineto +newpath 439 862 moveto +429 863 lineto +438 868 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 869 681 moveto -859 678 lineto -865 687 lineto +newpath 439 862 moveto +429 863 lineto +438 868 lineto closepath stroke end grestore -% cic_unification +% whelp gsave 10 dict begin -469 652 86 25 ellipse_path +474 736 44 25 ellipse_path stroke gsave 10 dict begin -397 644 moveto -(cic_unification) -[10.56 6.72 10.56 12 12 12 6.72 7.92 6.72 10.56 10.56 6.72 6.72 12 12] +444 728 moveto +(whelp) +[17.28 12 10.56 6.72 12] xshow end grestore end grestore -% cic_disambiguation -> cic_unification -newpath 976 722 moveto -963 719 948 716 935 714 curveto -810 692 777 695 650 678 curveto -619 674 586 669 557 665 curveto +% cic_disambiguation -> whelp +newpath 718 912 moveto +666 874 565 801 510 762 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 557 662 moveto -547 663 lineto -556 668 lineto +newpath 512 759 moveto +502 756 lineto +508 765 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 557 662 moveto -547 663 lineto -556 668 lineto +newpath 512 759 moveto +502 756 lineto +508 765 lineto closepath stroke end grestore -% whelp +% content_pres gsave 10 dict begin -354 558 44 25 ellipse_path +957 936 76 25 ellipse_path stroke gsave 10 dict begin -324 550 moveto -(whelp) -[17.28 12 10.56 6.72 12] +895 928 moveto +(content_pres) +[10.56 12 12 6.72 10.56 12 6.72 12 12 7.92 10.56 9.36] xshow end grestore end grestore -% cic_disambiguation -> whelp -newpath 968 724 moveto -968 723 967 723 967 723 curveto -965 721 964 721 961 720 curveto -932 706 922 708 890 702 curveto -835 690 820 691 764 678 curveto -676 656 658 637 568 618 curveto -524 608 402 620 366 592 curveto -366 592 366 592 365 592 curveto +% content_pres -> acic_content +newpath 910 916 moveto +879 903 840 886 808 872 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 368 590 moveto -360 583 lineto -362 593 lineto +newpath 810 869 moveto +799 868 lineto +807 875 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 368 590 moveto -360 583 lineto -362 593 lineto +newpath 810 869 moveto +799 868 lineto +807 875 lineto closepath stroke end grestore -% content_pres +% utf8_macros gsave 10 dict begin -849 740 76 25 ellipse_path +873 366 75 25 ellipse_path stroke gsave 10 dict begin -787 732 moveto -(content_pres) -[10.56 12 12 6.72 10.56 12 6.72 12 12 7.92 10.56 9.36] +812 358 moveto +(utf8_macros) +[12 6.72 7.92 12 12 18.72 10.56 10.56 7.92 12 9.36] xshow end grestore end grestore -% content_pres -> acic_content -newpath 849 714 moveto -849 706 849 697 849 688 curveto +% content_pres -> utf8_macros +newpath 949 911 moveto +937 873 917 799 917 736 curveto +917 736 917 736 917 542 curveto +917 492 900 436 888 401 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 853 688 moveto -849 678 lineto -846 688 lineto +newpath 891 399 moveto +884 391 lineto +884 402 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 853 688 moveto -849 678 lineto -846 688 lineto +newpath 891 399 moveto +884 391 lineto +884 402 lineto +closepath +stroke +end grestore + +% grafite_parser +gsave 10 dict begin +724 1128 81 25 ellipse_path +stroke +gsave 10 dict begin +657 1120 moveto +(grafite_parser) +[12 7.92 10.56 7.92 6.72 6.72 10.56 12 12 10.56 7.92 9.36 10.56 7.92] +xshow +end grestore +end grestore + +% sheath +gsave 10 dict begin +752 1024 45 25 ellipse_path +stroke +gsave 10 dict begin +721 1016 moveto +(sheath) +[9.36 12 10.56 10.56 6.72 12] +xshow +end grestore +end grestore + +% grafite_parser -> sheath +newpath 731 1103 moveto +734 1090 739 1074 743 1059 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 746 1059 moveto +745 1049 lineto +740 1058 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 746 1059 moveto +745 1049 lineto +740 1058 lineto closepath stroke end grestore % grafite gsave 10 dict begin -881 828 46 25 ellipse_path +161 936 46 25 ellipse_path stroke gsave 10 dict begin -849 820 moveto +129 928 moveto (grafite) [12 7.92 10.56 7.92 6.72 6.72 10.56] xshow end grestore end grestore -% grafite -> content_pres -newpath 872 803 moveto -868 794 865 784 861 775 curveto +% grafite_parser -> grafite +newpath 670 1108 moveto +661 1106 651 1103 642 1102 curveto +625 1098 498 1104 484 1094 curveto +449 1066 489 1027 455 998 curveto +389 938 345 981 258 962 curveto +243 959 227 955 213 951 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 214 948 moveto +203 948 lineto +212 954 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 214 948 moveto +203 948 lineto +212 954 lineto +closepath +stroke +end grestore + +% sheath -> cic_disambiguation +newpath 752 998 moveto +752 990 752 981 752 972 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 864 774 moveto -858 765 lineto -858 776 lineto +newpath 756 972 moveto +752 962 lineto +749 972 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 864 774 moveto -858 765 lineto -858 776 lineto +newpath 756 972 moveto +752 962 lineto +749 972 lineto closepath stroke end grestore -% cic_unification -> cic_proof_checking -newpath 552 644 moveto -622 636 714 620 736 592 curveto -765 555 769 521 736 488 curveto -731 482 606 483 598 483 curveto -563 482 555 482 519 482 curveto -503 481 389 482 372 481 curveto -372 481 372 481 372 481 curveto +% sheath -> content_pres +newpath 789 1008 moveto +820 995 865 976 901 960 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 376 478 moveto -365 479 lineto -374 485 lineto +newpath 902 963 moveto +910 956 lineto +899 957 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 376 478 moveto -365 479 lineto -374 485 lineto +newpath 902 963 moveto +910 956 lineto +899 957 lineto +closepath +stroke +end grestore + +% library +gsave 10 dict begin +359 736 46 25 ellipse_path +stroke +gsave 10 dict begin +327 728 moveto +(library) +[6.72 6.72 12 7.92 10.56 7.92 12] +xshow +end grestore +end grestore + +% cic_unification -> library +newpath 359 822 moveto +359 807 359 788 359 772 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 363 772 moveto +359 762 lineto +356 772 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 363 772 moveto +359 762 lineto +356 772 lineto closepath stroke end grestore % tactics gsave 10 dict begin -463 740 45 25 ellipse_path +313 936 45 25 ellipse_path stroke gsave 10 dict begin -432 732 moveto +282 928 moveto (tactics) [6.72 10.56 10.56 6.72 6.72 10.56 9.36] xshow @@ -635,54 +730,56 @@ end grestore end grestore % tactics -> cic_unification -newpath 465 714 moveto -466 706 466 697 467 688 curveto +newpath 326 911 moveto +331 902 336 892 340 882 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 471 688 moveto -467 678 lineto -464 688 lineto +newpath 343 883 moveto +345 873 lineto +337 880 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 471 688 moveto -467 678 lineto -464 688 lineto +newpath 343 883 moveto +345 873 lineto +337 880 lineto closepath stroke end grestore % tactics -> whelp -newpath 427 724 moveto -408 714 386 698 373 678 curveto -357 653 353 620 353 594 curveto +newpath 289 914 moveto +279 903 268 889 263 874 curveto +249 833 234 808 263 778 curveto +275 765 399 774 415 770 curveto +423 768 430 764 437 761 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 357 594 moveto -353 584 lineto -350 594 lineto +newpath 439 764 moveto +446 756 lineto +436 758 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 357 594 moveto -353 584 lineto -350 594 lineto +newpath 439 764 moveto +446 756 lineto +436 758 lineto closepath stroke end grestore % paramodulation gsave 10 dict begin -463 828 90 25 ellipse_path +355 1024 90 25 ellipse_path stroke gsave 10 dict begin -387 820 moveto +279 1016 moveto (paramodulation) [12 10.56 7.92 10.56 18.72 12 12 12 6.72 10.56 6.72 6.72 12 12] xshow @@ -690,44 +787,123 @@ end grestore end grestore % paramodulation -> tactics -newpath 463 802 moveto -463 794 463 785 463 776 curveto +newpath 343 999 moveto +338 990 333 980 329 970 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 467 776 moveto -463 766 lineto -460 776 lineto +newpath 332 969 moveto +325 961 lineto +326 972 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 467 776 moveto -463 766 lineto -460 776 lineto +newpath 332 969 moveto +325 961 lineto +326 972 lineto closepath stroke end grestore % cic gsave 10 dict begin -248 366 28 25 ellipse_path +408 454 28 25 ellipse_path stroke gsave 10 dict begin -234 358 moveto +394 446 moveto (cic) [10.56 6.72 10.56] xshow end grestore end grestore +% grafite -> cic +newpath 160 910 moveto +158 872 155 798 155 736 curveto +155 736 155 736 155 636 curveto +155 556 219 554 288 516 curveto +327 495 343 502 379 480 curveto +379 480 380 480 380 479 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 382 482 moveto +388 473 lineto +378 476 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 382 482 moveto +388 473 lineto +378 476 lineto +closepath +stroke +end grestore + +% grafite_engine +gsave 10 dict begin +161 1024 84 25 ellipse_path +stroke +gsave 10 dict begin +91 1016 moveto +(grafite_engine) +[12 7.92 10.56 7.92 6.72 6.72 10.56 12 10.56 12 12 6.72 12 10.56] +xshow +end grestore +end grestore + +% grafite_engine -> tactics +newpath 200 1001 moveto +222 989 249 973 272 960 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 274 963 moveto +281 955 lineto +271 957 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 274 963 moveto +281 955 lineto +271 957 lineto +closepath +stroke +end grestore + +% grafite_engine -> grafite +newpath 161 998 moveto +161 990 161 981 161 972 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 165 972 moveto +161 962 lineto +158 972 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 165 972 moveto +161 962 lineto +158 972 lineto +closepath +stroke +end grestore + % urimanager gsave 10 dict begin -343 278 70 25 ellipse_path +424 366 70 25 ellipse_path stroke gsave 10 dict begin -287 270 moveto +368 358 moveto (urimanager) [12 7.92 6.72 18.72 10.56 12 10.56 12 10.56 7.92] xshow @@ -735,32 +911,32 @@ end grestore end grestore % cic -> urimanager -newpath 268 347 moveto -280 336 296 322 310 309 curveto +newpath 413 429 moveto +414 420 416 411 417 402 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 312 312 moveto -317 302 lineto -307 307 lineto +newpath 420 402 moveto +419 392 lineto +414 401 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 312 312 moveto -317 302 lineto -307 307 lineto +newpath 420 402 moveto +419 392 lineto +414 401 lineto closepath stroke end grestore % xml gsave 10 dict begin -529 174 33 25 ellipse_path +622 174 33 25 ellipse_path stroke gsave 10 dict begin -510 166 moveto +603 166 moveto (xml) [12 18.72 6.72] xshow @@ -768,54 +944,67 @@ end grestore end grestore % cic -> xml -newpath 242 341 moveto -235 306 229 243 263 208 curveto -278 192 413 181 485 177 curveto +newpath 383 440 moveto +369 431 352 417 344 400 curveto +325 358 319 334 344 296 curveto +396 216 514 188 578 178 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 485 180 moveto -495 176 lineto -485 174 lineto +newpath 578 181 moveto +588 177 lineto +578 175 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 485 180 moveto -495 176 lineto -485 174 lineto +newpath 578 181 moveto +588 177 lineto +578 175 lineto closepath stroke end grestore +% cic_proof_checking +gsave 10 dict begin +408 542 110 25 ellipse_path +stroke +gsave 10 dict begin +312 534 moveto +(cic_proof_checking) +[10.56 6.72 10.56 12 12 7.92 12 12 7.92 12 10.56 12 10.56 10.56 12 6.72 12 12] +xshow +end grestore +end grestore + % cic_proof_checking -> cic -newpath 315 429 moveto -303 417 288 404 276 392 curveto +newpath 408 516 moveto +408 508 408 499 408 490 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 278 389 moveto -268 385 lineto -273 394 lineto +newpath 412 490 moveto +408 480 lineto +405 490 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 278 389 moveto -268 385 lineto -273 394 lineto +newpath 412 490 moveto +408 480 lineto +405 490 lineto closepath stroke end grestore % getter gsave 10 dict begin -341 366 42 25 ellipse_path +500 454 42 25 ellipse_path stroke gsave 10 dict begin -313 358 moveto +472 446 moveto (getter) [12 10.56 6.72 6.72 10.56 7.92] xshow @@ -823,53 +1012,53 @@ end grestore end grestore % cic_proof_checking -> getter -newpath 341 428 moveto -341 420 341 411 341 402 curveto +newpath 418 516 moveto +430 501 446 487 460 477 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 345 402 moveto -341 392 lineto -338 402 lineto +newpath 462 480 moveto +469 472 lineto +459 474 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 345 402 moveto -341 392 lineto -338 402 lineto +newpath 462 480 moveto +469 472 lineto +459 474 lineto closepath stroke end grestore % getter -> urimanager -newpath 342 340 moveto -342 332 342 323 342 314 curveto +newpath 480 431 moveto +472 421 461 409 452 398 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 346 314 moveto -342 304 lineto -339 314 lineto +newpath 455 396 moveto +445 391 lineto +450 401 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 346 314 moveto -342 304 lineto -339 314 lineto +newpath 455 396 moveto +445 391 lineto +450 401 lineto closepath stroke end grestore % registry gsave 10 dict begin -529 278 52 25 ellipse_path +748 262 52 25 ellipse_path stroke gsave 10 dict begin -491 270 moveto +710 254 moveto (registry) [7.92 10.56 12 6.72 9.36 6.72 7.92 12] xshow @@ -877,87 +1066,102 @@ end grestore end grestore % getter -> registry -newpath 375 350 moveto -405 336 449 316 482 300 curveto +newpath 501 428 moveto +505 392 517 327 558 296 curveto +570 287 673 291 686 288 curveto +691 287 696 285 700 284 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 483 303 moveto -491 296 lineto -480 297 lineto +newpath 702 287 moveto +710 280 lineto +699 280 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 483 303 moveto -491 296 lineto -480 297 lineto +newpath 702 287 moveto +710 280 lineto +699 280 lineto closepath stroke end grestore -% metadata +% logger gsave 10 dict begin -153 454 58 25 ellipse_path +613 366 45 25 ellipse_path stroke gsave 10 dict begin -109 446 moveto -(metadata) -[18.72 10.56 6.72 10.56 12 10.56 6.72 10.56] +582 358 moveto +(logger) +[6.72 12 12 12 10.56 7.92] xshow end grestore end grestore -% metadata -> cic -newpath 178 431 moveto -191 419 207 404 220 392 curveto +% getter -> logger +newpath 526 434 moveto +541 422 561 406 578 393 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 223 394 moveto -228 385 lineto -218 389 lineto +newpath 580 396 moveto +586 387 lineto +576 390 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 223 394 moveto -228 385 lineto -218 389 lineto +newpath 580 396 moveto +586 387 lineto +576 390 lineto closepath stroke end grestore -% metadata -> getter -newpath 197 437 moveto -229 424 270 408 286 400 curveto -292 397 298 394 303 390 curveto +% metadata +gsave 10 dict begin +484 636 58 25 ellipse_path +stroke +gsave 10 dict begin +440 628 moveto +(metadata) +[18.72 10.56 6.72 10.56 12 10.56 6.72 10.56] +xshow +end grestore +end grestore + +% metadata -> cic +newpath 505 612 moveto +525 586 548 546 528 516 curveto +507 483 483 498 448 480 curveto +445 478 443 477 440 475 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 305 393 moveto -312 385 lineto -302 387 lineto +newpath 441 472 moveto +431 469 lineto +437 477 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 305 393 moveto -312 385 lineto -302 387 lineto +newpath 441 472 moveto +431 469 lineto +437 477 lineto closepath stroke end grestore % hmysql gsave 10 dict begin -528 366 50 25 ellipse_path +728 366 50 25 ellipse_path stroke gsave 10 dict begin -492 358 moveto +692 358 moveto (hmysql) [12 18.72 12 9.36 12 6.72] xshow @@ -965,55 +1169,117 @@ end grestore end grestore % metadata -> hmysql -newpath 195 436 moveto -203 433 212 430 221 428 curveto -327 402 361 432 464 400 curveto -472 397 479 394 487 390 curveto +newpath 539 626 moveto +600 616 638 623 686 568 curveto +727 521 731 446 730 402 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 488 393 moveto -496 386 lineto -485 387 lineto +newpath 734 402 moveto +730 392 lineto +727 402 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 488 393 moveto -496 386 lineto -485 387 lineto +newpath 734 402 moveto +730 392 lineto +727 402 lineto closepath stroke end grestore % whelp -> metadata -newpath 320 541 moveto -287 523 237 497 200 479 curveto +newpath 477 711 moveto +479 699 480 685 481 672 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 201 476 moveto -191 474 lineto -198 482 lineto +newpath 484 672 moveto +482 662 lineto +478 672 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 201 476 moveto -191 474 lineto -198 482 lineto +newpath 484 672 moveto +482 662 lineto +478 672 lineto +closepath +stroke +end grestore + +% library -> metadata +newpath 386 715 moveto +404 700 428 680 448 664 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 450 667 moveto +456 658 lineto +446 661 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 450 667 moveto +456 658 lineto +446 661 lineto +closepath +stroke +end grestore + +% library -> cic_acic +newpath 357 711 moveto +356 699 355 685 355 672 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 358 672 moveto +354 662 lineto +352 672 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 358 672 moveto +354 662 lineto +352 672 lineto +closepath +stroke +end grestore + +% cic_acic -> cic_proof_checking +newpath 367 611 moveto +373 600 381 587 388 576 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 391 577 moveto +393 567 lineto +385 574 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 391 577 moveto +393 567 lineto +385 574 lineto closepath stroke end grestore % extlib gsave 10 dict begin -529 86 42 25 ellipse_path +622 86 42 25 ellipse_path stroke gsave 10 dict begin -501 78 moveto +594 78 moveto (extlib) [10.56 12 6.72 6.72 6.72 12] xshow @@ -1022,10 +1288,10 @@ end grestore % hgdome gsave 10 dict begin -655 278 54 25 ellipse_path +622 262 54 25 ellipse_path stroke gsave 10 dict begin -615 270 moveto +582 254 moveto (hgdome) [12 12 12 12 18.72 10.56] xshow @@ -1033,86 +1299,85 @@ end grestore end grestore % hgdome -> xml -newpath 637 254 moveto -625 239 608 221 591 208 curveto -584 202 575 197 567 192 curveto +newpath 622 236 moveto +622 228 622 219 622 210 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 568 189 moveto -558 187 lineto -565 195 lineto +newpath 626 210 moveto +622 200 lineto +619 210 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 568 189 moveto -558 187 lineto -565 195 lineto +newpath 626 210 moveto +622 200 lineto +619 210 lineto closepath stroke end grestore % hmysql -> registry -newpath 528 340 moveto -528 332 529 323 529 314 curveto +newpath 733 341 moveto +735 328 738 312 741 298 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 533 314 moveto -529 304 lineto -526 314 lineto +newpath 744 298 moveto +743 288 lineto +738 297 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 533 314 moveto -529 304 lineto -526 314 lineto +newpath 744 298 moveto +743 288 lineto +738 297 lineto closepath stroke end grestore % registry -> xml -newpath 529 252 moveto -529 239 529 224 529 210 curveto +newpath 718 241 moveto +699 228 674 211 655 197 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 533 210 moveto -529 200 lineto -526 210 lineto +newpath 657 194 moveto +647 191 lineto +653 200 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 533 210 moveto -529 200 lineto -526 210 lineto +newpath 657 194 moveto +647 191 lineto +653 200 lineto closepath stroke end grestore % xml -> extlib -newpath 529 148 moveto -529 140 529 131 529 122 curveto +newpath 622 148 moveto +622 140 622 131 622 122 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 533 122 moveto -529 112 lineto -526 122 lineto +newpath 626 122 moveto +622 112 lineto +619 122 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 533 122 moveto -529 112 lineto -526 122 lineto +newpath 626 122 moveto +622 112 lineto +619 122 lineto closepath stroke end grestore @@ -1122,26 +1387,26 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 604 590 moveto -468 590 lineto -468 526 lineto -604 526 lineto +newpath 711 768 moveto +575 768 lineto +575 704 lineto +711 704 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 604 590 moveto -468 590 lineto -468 526 lineto -604 526 lineto +newpath 711 768 moveto +575 768 lineto +575 704 lineto +711 704 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -476 564 moveto +583 742 moveto (Dependency) [17.28 10.56 12 10.56 12 12 10.56 12 10.56 12] xshow -492 536 moveto +599 714 moveto (Analyzer) [17.28 12 10.56 6.72 12 10.56 10.56 7.92] xshow @@ -1149,24 +1414,22 @@ end grestore end grestore % DependencyAnalyzer -> metadata -newpath 513 526 moveto -500 511 483 496 464 488 curveto -440 477 248 485 221 480 curveto -216 479 210 477 205 475 curveto +newpath 592 704 moveto +570 691 546 675 526 662 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 206 472 moveto -195 472 lineto -204 478 lineto +newpath 527 659 moveto +517 657 lineto +524 665 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 206 472 moveto -195 472 lineto -204 478 lineto +newpath 527 659 moveto +517 657 lineto +524 665 lineto closepath stroke end grestore @@ -1176,22 +1439,22 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 76 472 moveto -0 472 lineto -0 436 lineto -76 436 lineto +newpath 635 560 moveto +559 560 lineto +559 524 lineto +635 524 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 76 472 moveto -0 472 lineto -0 436 lineto -76 436 lineto +newpath 635 560 moveto +559 560 lineto +559 524 lineto +635 524 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -8 446 moveto +567 534 moveto (Getter) [17.28 10.56 6.72 6.72 10.56 7.92] xshow @@ -1199,24 +1462,22 @@ end grestore end grestore % Getter -> getter -newpath 65 436 moveto -70 433 76 430 82 428 curveto -169 397 200 430 286 400 curveto -293 397 299 394 305 391 curveto +newpath 577 524 moveto +563 512 546 496 532 483 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 307 394 moveto -314 386 lineto -304 388 lineto +newpath 534 480 moveto +524 476 lineto +529 485 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 307 394 moveto -314 386 lineto -304 388 lineto +newpath 534 480 moveto +524 476 lineto +529 485 lineto closepath stroke end grestore @@ -1226,22 +1487,22 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 990 942 moveto -912 942 lineto -912 906 lineto -990 906 lineto +newpath 394 1226 moveto +316 1226 lineto +316 1190 lineto +394 1190 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 990 942 moveto -912 942 lineto -912 906 lineto -990 906 lineto +newpath 394 1226 moveto +316 1226 lineto +316 1190 lineto +394 1190 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -919 916 moveto +323 1200 moveto (Matita) [21.36 10.56 6.72 6.72 6.72 10.56] xshow @@ -1249,90 +1510,113 @@ end grestore end grestore % Matita -> cic_disambiguation -newpath 961 906 moveto -978 875 1012 813 1035 775 curveto +newpath 372 1190 moveto +393 1167 429 1129 458 1094 curveto +493 1052 487 1028 531 998 curveto +565 975 607 961 646 951 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 1038 776 moveto -1040 766 lineto -1032 773 lineto +newpath 647 954 moveto +656 949 lineto +646 948 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 1038 776 moveto -1040 766 lineto -1032 773 lineto +newpath 647 954 moveto +656 949 lineto +646 948 lineto closepath stroke end grestore -% Matita -> grafite -newpath 912 914 moveto -904 910 896 905 891 898 curveto -883 889 880 876 879 864 curveto +% Matita -> grafite_parser +newpath 394 1205 moveto +450 1199 556 1186 642 1162 curveto +651 1160 660 1156 669 1153 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 883 864 moveto -879 854 lineto -876 864 lineto +newpath 670 1156 moveto +678 1149 lineto +667 1150 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 883 864 moveto -879 854 lineto -876 864 lineto +newpath 670 1156 moveto +678 1149 lineto +667 1150 lineto closepath stroke end grestore % Matita -> paramodulation -newpath 912 923 moveto -801 921 489 912 473 898 curveto -464 889 460 877 459 864 curveto +newpath 355 1190 moveto +355 1160 355 1099 355 1060 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 463 864 moveto -459 854 lineto -456 864 lineto +newpath 359 1060 moveto +355 1050 lineto +352 1060 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 463 864 moveto -459 854 lineto -456 864 lineto +newpath 359 1060 moveto +355 1050 lineto +352 1060 lineto +closepath +stroke +end grestore + +% Matita -> grafite_engine +newpath 336 1190 moveto +303 1158 236 1094 194 1056 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 197 1054 moveto +187 1049 lineto +192 1059 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 197 1054 moveto +187 1049 lineto +192 1059 lineto closepath stroke end grestore % Matita -> hgdome -newpath 990 922 moveto -1056 919 1183 912 1197 898 curveto -1221 872 1211 775 1211 740 curveto -1211 740 1211 740 1211 454 curveto -1211 351 865 301 719 284 curveto +newpath 316 1204 moveto +253 1196 129 1171 64 1094 curveto +44 1069 48 1055 48 1024 curveto +48 1024 48 1024 48 454 curveto +48 327 166 338 285 296 curveto +334 278 473 269 557 265 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 719 281 moveto -709 283 lineto -719 287 lineto +newpath 557 268 moveto +567 264 lineto +557 262 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 719 281 moveto -709 283 lineto -719 287 lineto +newpath 557 268 moveto +567 264 lineto +557 262 lineto closepath stroke end grestore @@ -1342,26 +1626,26 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 718 590 moveto -622 590 lineto -622 526 lineto -718 526 lineto +newpath 279 668 moveto +183 668 lineto +183 604 lineto +279 604 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 718 590 moveto -622 590 lineto -622 526 lineto -718 526 lineto +newpath 279 668 moveto +183 668 lineto +183 604 lineto +279 604 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -643 564 moveto +204 642 moveto (Proof) [13.44 7.92 12 12 7.92] xshow -630 536 moveto +191 614 moveto (Checker) [16.08 12 10.56 10.56 12 10.56 7.92] xshow @@ -1369,23 +1653,23 @@ end grestore end grestore % ProofChecker -> cic_proof_checking -newpath 653 526 moveto -643 511 630 496 613 488 curveto -589 476 409 493 360 483 curveto +newpath 279 607 moveto +281 606 283 605 285 604 curveto +306 592 330 580 351 569 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 362 480 moveto -351 480 lineto -359 486 lineto +newpath 352 572 moveto +360 565 lineto +349 566 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 362 480 moveto -351 480 lineto -359 486 lineto +newpath 352 572 moveto +360 565 lineto +349 566 lineto closepath stroke end grestore @@ -1395,22 +1679,22 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 658 846 moveto -572 846 lineto -572 810 lineto -658 810 lineto +newpath 626 1042 moveto +540 1042 lineto +540 1006 lineto +626 1006 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 658 846 moveto -572 846 lineto -572 810 lineto -658 810 lineto +newpath 626 1042 moveto +540 1042 lineto +540 1006 lineto +626 1006 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -579 820 moveto +547 1016 moveto (Uwobo) [17.28 17.28 12 12 12] xshow @@ -1418,23 +1702,24 @@ end grestore end grestore % Uwobo -> content_pres -newpath 649 810 moveto -655 807 661 804 667 802 curveto -704 786 748 772 782 760 curveto +newpath 612 1006 moveto +618 1003 624 1000 630 998 curveto +733 963 766 985 871 962 curveto +878 961 884 959 891 957 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 783 763 moveto -792 757 lineto -781 757 lineto +newpath 892 960 moveto +901 954 lineto +890 954 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 783 763 moveto -792 757 lineto -781 757 lineto +newpath 892 960 moveto +901 954 lineto +890 954 lineto closepath stroke end grestore @@ -1444,68 +1729,45 @@ gsave 10 dict begin filled 0.584 0.220 0.933 nodecolor 0.584 0.220 0.933 nodecolor -newpath 756 846 moveto -676 846 lineto -676 810 lineto -756 810 lineto +newpath 764 1226 moveto +684 1226 lineto +684 1190 lineto +764 1190 lineto closepath fill 0.584 0.220 0.933 nodecolor -newpath 756 846 moveto -676 846 lineto -676 810 lineto -756 810 lineto +newpath 764 1226 moveto +684 1226 lineto +684 1190 lineto +764 1190 lineto closepath stroke gsave 10 dict begin 0.000 0.000 0.000 nodecolor -683 820 moveto +691 1200 moveto (Whelp) [22.56 12 10.56 6.72 12] xshow end grestore end grestore -% Whelp -> cic_disambiguation -newpath 743 810 moveto -749 807 754 804 760 802 curveto -835 773 858 782 935 766 curveto -944 764 954 762 963 759 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 964 762 moveto -973 757 lineto -963 756 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 964 762 moveto -973 757 lineto -963 756 lineto -closepath -stroke -end grestore - -% Whelp -> content_pres -newpath 743 810 moveto -761 798 785 782 805 769 curveto +% Whelp -> grafite_parser +newpath 724 1190 moveto +724 1182 724 1173 724 1164 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 808 771 moveto -814 763 lineto -804 766 lineto +newpath 728 1164 moveto +724 1154 lineto +721 1164 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 808 771 moveto -814 763 lineto -804 766 lineto +newpath 728 1164 moveto +724 1154 lineto +721 1164 lineto closepath stroke end grestore diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 73e68e82e..c5c0fff05 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -1,4 +1,4 @@ -\documentclass[draft]{kluwer} +\documentclass[]{kluwer} \usepackage{color} \usepackage{graphicx} % \usepackage{amssymb,amsmath} @@ -270,6 +270,14 @@ allow other developers to quickly understand our code and contribute. \end{center} \end{figure} +\begin{figure}[t] + \begin{center} + \includegraphics[width=0.9\textwidth]{libraries.ps} + \caption{\MATITA{} libraries} + \label{fig:libraries} + \end{center} +\end{figure} + \section{Overview of the Architecture} Fig.~\ref{fig:libraries} shows the architecture of the \emph{libraries} (circle nodes) and \emph{applications} (squared nodes) developed in the HELM project. @@ -1323,7 +1331,7 @@ expression and the suffix \verb+_to_Prop+. In the above example, We would like to thank all the students that during the past five years collaborated in the \HELM{} project and contributed to the development of Matita, and in particular -A.~Griggio, F.~Guidi, P.~Di~Lena, L.~Padovani, I.~Schena, M.~Selmi, +M.~Galat\`a, A.~Griggio, F.~Guidi, P.~Di~Lena, L.~Padovani, I.~Schena, M.~Selmi, and V.~Tamburrelli. \theendnotes